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 e. TopMod -> W e. TopGrp )

Proof

Step Hyp Ref Expression
1 tlmlmod 
 |-  ( W e. TopMod -> W e. LMod )
2 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
3 1 2 syl 
 |-  ( W e. TopMod -> W e. Grp )
4 tlmtmd 
 |-  ( W e. TopMod -> W e. TopMnd )
5 eqid 
 |-  ( Base ` W ) = ( Base ` W )
6 eqid 
 |-  ( invg ` W ) = ( invg ` W )
7 5 6 grpinvf 
 |-  ( W e. Grp -> ( invg ` W ) : ( Base ` W ) --> ( Base ` W ) )
8 3 7 syl 
 |-  ( W e. TopMod -> ( invg ` W ) : ( Base ` W ) --> ( Base ` W ) )
9 8 feqmptd 
 |-  ( W e. TopMod -> ( invg ` W ) = ( x e. ( Base ` W ) |-> ( ( invg ` W ) ` x ) ) )
10 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
11 eqid 
 |-  ( .s ` W ) = ( .s ` W )
12 eqid 
 |-  ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) )
13 eqid 
 |-  ( invg ` ( Scalar ` W ) ) = ( invg ` ( Scalar ` W ) )
14 5 6 10 11 12 13 lmodvneg1 
 |-  ( ( W e. LMod /\ x e. ( Base ` W ) ) -> ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) x ) = ( ( invg ` W ) ` x ) )
15 1 14 sylan 
 |-  ( ( W e. TopMod /\ x e. ( Base ` W ) ) -> ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) x ) = ( ( invg ` W ) ` x ) )
16 15 mpteq2dva 
 |-  ( W e. TopMod -> ( x e. ( Base ` W ) |-> ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) x ) ) = ( x e. ( Base ` W ) |-> ( ( invg ` W ) ` x ) ) )
17 9 16 eqtr4d 
 |-  ( W e. TopMod -> ( invg ` W ) = ( x e. ( Base ` W ) |-> ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) x ) ) )
18 eqid 
 |-  ( TopOpen ` W ) = ( TopOpen ` W )
19 eqid 
 |-  ( TopOpen ` ( Scalar ` W ) ) = ( TopOpen ` ( Scalar ` W ) )
20 id 
 |-  ( W e. TopMod -> W e. TopMod )
21 tlmtps 
 |-  ( W e. TopMod -> W e. TopSp )
22 5 18 istps 
 |-  ( W e. TopSp <-> ( TopOpen ` W ) e. ( TopOn ` ( Base ` W ) ) )
23 21 22 sylib 
 |-  ( W e. TopMod -> ( TopOpen ` W ) e. ( TopOn ` ( Base ` W ) ) )
24 10 tlmscatps 
 |-  ( W e. TopMod -> ( Scalar ` W ) e. TopSp )
25 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
26 25 19 istps 
 |-  ( ( Scalar ` W ) e. TopSp <-> ( TopOpen ` ( Scalar ` W ) ) e. ( TopOn ` ( Base ` ( Scalar ` W ) ) ) )
27 24 26 sylib 
 |-  ( W e. TopMod -> ( TopOpen ` ( Scalar ` W ) ) e. ( TopOn ` ( Base ` ( Scalar ` W ) ) ) )
28 10 lmodring 
 |-  ( W e. LMod -> ( Scalar ` W ) e. Ring )
29 1 28 syl 
 |-  ( W e. TopMod -> ( Scalar ` W ) e. Ring )
30 ringgrp 
 |-  ( ( Scalar ` W ) e. Ring -> ( Scalar ` W ) e. Grp )
31 29 30 syl 
 |-  ( W e. TopMod -> ( Scalar ` W ) e. Grp )
32 25 12 ringidcl 
 |-  ( ( Scalar ` W ) e. Ring -> ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) )
33 29 32 syl 
 |-  ( W e. TopMod -> ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) )
34 25 13 grpinvcl 
 |-  ( ( ( Scalar ` W ) e. Grp /\ ( 1r ` ( Scalar ` W ) ) e. ( Base ` ( Scalar ` W ) ) ) -> ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) e. ( Base ` ( Scalar ` W ) ) )
35 31 33 34 syl2anc 
 |-  ( W e. TopMod -> ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) e. ( Base ` ( Scalar ` W ) ) )
36 23 27 35 cnmptc 
 |-  ( W e. TopMod -> ( x e. ( Base ` W ) |-> ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ) e. ( ( TopOpen ` W ) Cn ( TopOpen ` ( Scalar ` W ) ) ) )
37 23 cnmptid 
 |-  ( W e. TopMod -> ( x e. ( Base ` W ) |-> x ) e. ( ( TopOpen ` W ) Cn ( TopOpen ` W ) ) )
38 10 11 18 19 20 23 36 37 cnmpt1vsca 
 |-  ( W e. TopMod -> ( x e. ( Base ` W ) |-> ( ( ( invg ` ( Scalar ` W ) ) ` ( 1r ` ( Scalar ` W ) ) ) ( .s ` W ) x ) ) e. ( ( TopOpen ` W ) Cn ( TopOpen ` W ) ) )
39 17 38 eqeltrd 
 |-  ( W e. TopMod -> ( invg ` W ) e. ( ( TopOpen ` W ) Cn ( TopOpen ` W ) ) )
40 18 6 istgp 
 |-  ( W e. TopGrp <-> ( W e. Grp /\ W e. TopMnd /\ ( invg ` W ) e. ( ( TopOpen ` W ) Cn ( TopOpen ` W ) ) ) )
41 3 4 39 40 syl3anbrc 
 |-  ( W e. TopMod -> W e. TopGrp )