Metamath Proof Explorer

Theorem tlmtgp

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

Ref Expression
Assertion tlmtgp ⊢ W ∈ TopMod → W ∈ TopGrp

Proof

Step Hyp Ref Expression
1 tlmlmod ⊢ W ∈ TopMod → W ∈ LMod
2 lmodgrp ⊢ W ∈ LMod → W ∈ Grp
3 1 2 syl ⊢ W ∈ TopMod → W ∈ Grp
4 tlmtmd ⊢ W ∈ TopMod → W ∈ TopMnd
5 eqid ⊢ Base W = Base W
6 eqid ⊢ inv g ⁡ W = inv g ⁡ W
7 5 6 grpinvf ⊢ W ∈ Grp → inv g ⁡ W : Base W ⟶ Base W
8 3 7 syl ⊢ W ∈ TopMod → inv g ⁡ W : Base W ⟶ Base W
9 8 feqmptd ⊢ W ∈ TopMod → inv g ⁡ W = x ∈ Base W ⟼ inv g ⁡ W ⁡ x
10 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
11 eqid ⊢ ⋅ W = ⋅ W
12 eqid ⊢ 1 Scalar ⁡ W = 1 Scalar ⁡ W
13 eqid ⊢ inv g ⁡ Scalar ⁡ W = inv g ⁡ Scalar ⁡ W
14 5 6 10 11 12 13 lmodvneg1 ⊢ W ∈ LMod ∧ x ∈ Base W → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W x = inv g ⁡ W ⁡ x
15 1 14 sylan ⊢ W ∈ TopMod ∧ x ∈ Base W → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W x = inv g ⁡ W ⁡ x
16 15 mpteq2dva ⊢ W ∈ TopMod → x ∈ Base W ⟼ inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W x = x ∈ Base W ⟼ inv g ⁡ W ⁡ x
17 9 16 eqtr4d ⊢ W ∈ TopMod → inv g ⁡ W = x ∈ Base W ⟼ inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W x
18 eqid ⊢ TopOpen ⁡ W = TopOpen ⁡ W
19 eqid ⊢ TopOpen ⁡ Scalar ⁡ W = TopOpen ⁡ Scalar ⁡ W
20 id ⊢ W ∈ TopMod → W ∈ TopMod
21 tlmtps ⊢ W ∈ TopMod → W ∈ TopSp
22 5 18 istps ⊢ W ∈ TopSp ↔ TopOpen ⁡ W ∈ TopOn ⁡ Base W
23 21 22 sylib ⊢ W ∈ TopMod → TopOpen ⁡ W ∈ TopOn ⁡ Base W
24 10 tlmscatps ⊢ W ∈ TopMod → Scalar ⁡ W ∈ TopSp
25 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
26 25 19 istps ⊢ Scalar ⁡ W ∈ TopSp ↔ TopOpen ⁡ Scalar ⁡ W ∈ TopOn ⁡ Base Scalar ⁡ W
27 24 26 sylib ⊢ W ∈ TopMod → TopOpen ⁡ Scalar ⁡ W ∈ TopOn ⁡ Base Scalar ⁡ W
28 10 lmodring ⊢ W ∈ LMod → Scalar ⁡ W ∈ Ring
29 1 28 syl ⊢ W ∈ TopMod → Scalar ⁡ W ∈ Ring
30 ringgrp ⊢ Scalar ⁡ W ∈ Ring → Scalar ⁡ W ∈ Grp
31 29 30 syl ⊢ W ∈ TopMod → Scalar ⁡ W ∈ Grp
32 25 12 ringidcl ⊢ Scalar ⁡ W ∈ Ring → 1 Scalar ⁡ W ∈ Base Scalar ⁡ W
33 29 32 syl ⊢ W ∈ TopMod → 1 Scalar ⁡ W ∈ Base Scalar ⁡ W
34 25 13 grpinvcl ⊢ Scalar ⁡ W ∈ Grp ∧ 1 Scalar ⁡ W ∈ Base Scalar ⁡ W → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ∈ Base Scalar ⁡ W
35 31 33 34 syl2anc ⊢ W ∈ TopMod → inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ∈ Base Scalar ⁡ W
36 23 27 35 cnmptc ⊢ W ∈ TopMod → x ∈ Base W ⟼ inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ∈ TopOpen ⁡ W Cn TopOpen ⁡ Scalar ⁡ W
37 23 cnmptid ⊢ W ∈ TopMod → x ∈ Base W ⟼ x ∈ TopOpen ⁡ W Cn TopOpen ⁡ W
38 10 11 18 19 20 23 36 37 cnmpt1vsca ⊢ W ∈ TopMod → x ∈ Base W ⟼ inv g ⁡ Scalar ⁡ W ⁡ 1 Scalar ⁡ W ⋅ W x ∈ TopOpen ⁡ W Cn TopOpen ⁡ W
39 17 38 eqeltrd ⊢ W ∈ TopMod → inv g ⁡ W ∈ TopOpen ⁡ W Cn TopOpen ⁡ W
40 18 6 istgp ⊢ W ∈ TopGrp ↔ W ∈ Grp ∧ W ∈ TopMnd ∧ inv g ⁡ W ∈ TopOpen ⁡ W Cn TopOpen ⁡ W
41 3 4 39 40 syl3anbrc ⊢ W ∈ TopMod → W ∈ TopGrp