This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑊 ∈ TopMod → 𝑊 ∈ TopGrp )

Proof

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