Theorem tlmtgp 24140

Description: A topological vector space is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.)

Assertion

Ref	Expression
tlmtgp	⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopGrp)

Proof of Theorem tlmtgp

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		tlmlmod 24133	. . 3 ⊢ (𝑊 ∈ TopMod → 𝑊 ∈ LMod)
2		lmodgrp 20759	. . 3 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
3	1, 2	syl 17	. 2 ⊢ (𝑊 ∈ TopMod → 𝑊 ∈ Grp)
4		tlmtmd 24131	. 2 ⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopMnd)
5		eqid 2725	. . . . . . 7 ⊢ (Base‘𝑊) = (Base‘𝑊)
6		eqid 2725	. . . . . . 7 ⊢ (invg‘𝑊) = (invg‘𝑊)
7	5, 6	grpinvf 18949	. . . . . 6 ⊢ (𝑊 ∈ Grp → (invg‘𝑊):(Base‘𝑊)⟶(Base‘𝑊))
8	3, 7	syl 17	. . . . 5 ⊢ (𝑊 ∈ TopMod → (invg‘𝑊):(Base‘𝑊)⟶(Base‘𝑊))
9	8	feqmptd 6965	. . . 4 ⊢ (𝑊 ∈ TopMod → (invg‘𝑊) = (𝑥 ∈ (Base‘𝑊) ↦ ((invg‘𝑊)‘𝑥)))
10		eqid 2725	. . . . . . 7 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
11		eqid 2725	. . . . . . 7 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
12		eqid 2725	. . . . . . 7 ⊢ (1r‘(Scalar‘𝑊)) = (1r‘(Scalar‘𝑊))
13		eqid 2725	. . . . . . 7 ⊢ (invg‘(Scalar‘𝑊)) = (invg‘(Scalar‘𝑊))
14	5, 6, 10, 11, 12, 13	lmodvneg1 20797	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 𝑥 ∈ (Base‘𝑊)) → (((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))( ·𝑠 ‘𝑊)𝑥) = ((invg‘𝑊)‘𝑥))
15	1, 14	sylan 578	. . . . 5 ⊢ ((𝑊 ∈ TopMod ∧ 𝑥 ∈ (Base‘𝑊)) → (((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))( ·𝑠 ‘𝑊)𝑥) = ((invg‘𝑊)‘𝑥))
16	15	mpteq2dva 5249	. . . 4 ⊢ (𝑊 ∈ TopMod → (𝑥 ∈ (Base‘𝑊) ↦ (((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))( ·𝑠 ‘𝑊)𝑥)) = (𝑥 ∈ (Base‘𝑊) ↦ ((invg‘𝑊)‘𝑥)))
17	9, 16	eqtr4d 2768	. . 3 ⊢ (𝑊 ∈ TopMod → (invg‘𝑊) = (𝑥 ∈ (Base‘𝑊) ↦ (((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))( ·𝑠 ‘𝑊)𝑥)))
18		eqid 2725	. . . 4 ⊢ (TopOpen‘𝑊) = (TopOpen‘𝑊)
19		eqid 2725	. . . 4 ⊢ (TopOpen‘(Scalar‘𝑊)) = (TopOpen‘(Scalar‘𝑊))
20		id 22	. . . 4 ⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopMod)
21		tlmtps 24132	. . . . 5 ⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopSp)
22	5, 18	istps 22876	. . . . 5 ⊢ (𝑊 ∈ TopSp ↔ (TopOpen‘𝑊) ∈ (TopOn‘(Base‘𝑊)))
23	21, 22	sylib 217	. . . 4 ⊢ (𝑊 ∈ TopMod → (TopOpen‘𝑊) ∈ (TopOn‘(Base‘𝑊)))
24	10	tlmscatps 24135	. . . . . 6 ⊢ (𝑊 ∈ TopMod → (Scalar‘𝑊) ∈ TopSp)
25		eqid 2725	. . . . . . 7 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
26	25, 19	istps 22876	. . . . . 6 ⊢ ((Scalar‘𝑊) ∈ TopSp ↔ (TopOpen‘(Scalar‘𝑊)) ∈ (TopOn‘(Base‘(Scalar‘𝑊))))
27	24, 26	sylib 217	. . . . 5 ⊢ (𝑊 ∈ TopMod → (TopOpen‘(Scalar‘𝑊)) ∈ (TopOn‘(Base‘(Scalar‘𝑊))))
28	10	lmodring 20760	. . . . . . . 8 ⊢ (𝑊 ∈ LMod → (Scalar‘𝑊) ∈ Ring)
29	1, 28	syl 17	. . . . . . 7 ⊢ (𝑊 ∈ TopMod → (Scalar‘𝑊) ∈ Ring)
30		ringgrp 20187	. . . . . . 7 ⊢ ((Scalar‘𝑊) ∈ Ring → (Scalar‘𝑊) ∈ Grp)
31	29, 30	syl 17	. . . . . 6 ⊢ (𝑊 ∈ TopMod → (Scalar‘𝑊) ∈ Grp)
32	25, 12	ringidcl 20211	. . . . . . 7 ⊢ ((Scalar‘𝑊) ∈ Ring → (1r‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊)))
33	29, 32	syl 17	. . . . . 6 ⊢ (𝑊 ∈ TopMod → (1r‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊)))
34	25, 13	grpinvcl 18950	. . . . . 6 ⊢ (((Scalar‘𝑊) ∈ Grp ∧ (1r‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) → ((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊))) ∈ (Base‘(Scalar‘𝑊)))
35	31, 33, 34	syl2anc 582	. . . . 5 ⊢ (𝑊 ∈ TopMod → ((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊))) ∈ (Base‘(Scalar‘𝑊)))
36	23, 27, 35	cnmptc 23606	. . . 4 ⊢ (𝑊 ∈ TopMod → (𝑥 ∈ (Base‘𝑊) ↦ ((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))) ∈ ((TopOpen‘𝑊) Cn (TopOpen‘(Scalar‘𝑊))))
37	23	cnmptid 23605	. . . 4 ⊢ (𝑊 ∈ TopMod → (𝑥 ∈ (Base‘𝑊) ↦ 𝑥) ∈ ((TopOpen‘𝑊) Cn (TopOpen‘𝑊)))
38	10, 11, 18, 19, 20, 23, 36, 37	cnmpt1vsca 24138	. . 3 ⊢ (𝑊 ∈ TopMod → (𝑥 ∈ (Base‘𝑊) ↦ (((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))( ·𝑠 ‘𝑊)𝑥)) ∈ ((TopOpen‘𝑊) Cn (TopOpen‘𝑊)))
39	17, 38	eqeltrd 2825	. 2 ⊢ (𝑊 ∈ TopMod → (invg‘𝑊) ∈ ((TopOpen‘𝑊) Cn (TopOpen‘𝑊)))
40	18, 6	istgp 24021	. 2 ⊢ (𝑊 ∈ TopGrp ↔ (𝑊 ∈ Grp ∧ 𝑊 ∈ TopMnd ∧ (invg‘𝑊) ∈ ((TopOpen‘𝑊) Cn (TopOpen‘𝑊))))
41	3, 4, 39, 40	syl3anbrc 1340	1 ⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopGrp)

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098   ↦ cmpt 5232  ⟶wf 6544  ‘cfv 6548  (class class class)co 7418  Basecbs 17181  Scalarcsca 17237   ·_𝑠 cvsca 17238  TopOpenctopn 17404  Grpcgrp 18896  inv_gcminusg 18897  1_rcur 20130  Ringcrg 20182  LModclmod 20752  TopOnctopon 22852  TopSpctps 22874   Cn ccn 23168  TopMndctmd 24014  TopGrpctgp 24015  TopModctlm 24102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-cnex 11195  ax-resscn 11196  ax-1cn 11197  ax-icn 11198  ax-addcl 11199  ax-addrcl 11200  ax-mulcl 11201  ax-mulrcl 11202  ax-mulcom 11203  ax-addass 11204  ax-mulass 11205  ax-distr 11206  ax-i2m1 11207  ax-1ne0 11208  ax-1rid 11209  ax-rnegex 11210  ax-rrecex 11211  ax-cnre 11212  ax-pre-lttri 11213  ax-pre-lttrn 11214  ax-pre-ltadd 11215  ax-pre-mulgt0 11216

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6306  df-ord 6373  df-on 6374  df-lim 6375  df-suc 6376  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-riota 7374  df-ov 7421  df-oprab 7422  df-mpo 7423  df-om 7871  df-1st 7993  df-2nd 7994  df-frecs 8286  df-wrecs 8317  df-recs 8391  df-rdg 8430  df-er 8724  df-map 8846  df-en 8964  df-dom 8965  df-sdom 8966  df-pnf 11281  df-mnf 11282  df-xr 11283  df-ltxr 11284  df-le 11285  df-sub 11477  df-neg 11478  df-nn 12244  df-2 12306  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17182  df-plusg 17247  df-0g 17424  df-topgen 17426  df-mgm 18601  df-sgrp 18680  df-mnd 18696  df-grp 18899  df-minusg 18900  df-mgp 20084  df-ur 20131  df-ring 20184  df-lmod 20754  df-scaf 20755  df-top 22836  df-topon 22853  df-topsp 22875  df-bases 22889  df-cn 23171  df-cnp 23172  df-tx 23506  df-tmd 24016  df-tgp 24017  df-trg 24104  df-tlm 24106

This theorem is referenced by: (None)

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »