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 )