Metamath Proof Explorer

Theorem ngptgp

Description: A normed abelian group is a topological group (with the topology induced by the metric induced by the norm). (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion ngptgp 
|- ( ( G e. NrmGrp /\ G e. Abel ) -> G e. TopGrp )

Proof

Step Hyp Ref Expression
1 ngpgrp 
 |-  ( G e. NrmGrp -> G e. Grp )
2 1 adantr 
 |-  ( ( G e. NrmGrp /\ G e. Abel ) -> G e. Grp )
3 ngpms 
 |-  ( G e. NrmGrp -> G e. MetSp )
4 3 adantr 
 |-  ( ( G e. NrmGrp /\ G e. Abel ) -> G e. MetSp )
5 mstps 
 |-  ( G e. MetSp -> G e. TopSp )
6 4 5 syl 
 |-  ( ( G e. NrmGrp /\ G e. Abel ) -> G e. TopSp )
7 eqid 
 |-  ( Base ` G ) = ( Base ` G )
8 eqid 
 |-  ( -g ` G ) = ( -g ` G )
9 7 8 grpsubf 
 |-  ( G e. Grp -> ( -g ` G ) : ( ( Base ` G ) X. ( Base ` G ) ) --> ( Base ` G ) )
10 2 9 syl 
 |-  ( ( G e. NrmGrp /\ G e. Abel ) -> ( -g ` G ) : ( ( Base ` G ) X. ( Base ` G ) ) --> ( Base ` G ) )
11 rphalfcl 
 |-  ( z e. RR+ -> ( z / 2 ) e. RR+ )
12 simplll 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( G e. NrmGrp /\ G e. Abel ) )
13 12 4 syl 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> G e. MetSp )
14 simpllr 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) )
15 14 simpld 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> x e. ( Base ` G ) )
16 simprl 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> u e. ( Base ` G ) )
17 eqid 
 |-  ( dist ` G ) = ( dist ` G )
18 7 17 mscl 
 |-  ( ( G e. MetSp /\ x e. ( Base ` G ) /\ u e. ( Base ` G ) ) -> ( x ( dist ` G ) u ) e. RR )
19 13 15 16 18 syl3anc 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( x ( dist ` G ) u ) e. RR )
20 14 simprd 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> y e. ( Base ` G ) )
21 simprr 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> v e. ( Base ` G ) )
22 7 17 mscl 
 |-  ( ( G e. MetSp /\ y e. ( Base ` G ) /\ v e. ( Base ` G ) ) -> ( y ( dist ` G ) v ) e. RR )
23 13 20 21 22 syl3anc 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( y ( dist ` G ) v ) e. RR )
24 rpre 
 |-  ( z e. RR+ -> z e. RR )
25 24 ad2antlr 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> z e. RR )
26 lt2halves 
 |-  ( ( ( x ( dist ` G ) u ) e. RR /\ ( y ( dist ` G ) v ) e. RR /\ z e. RR ) -> ( ( ( x ( dist ` G ) u ) < ( z / 2 ) /\ ( y ( dist ` G ) v ) < ( z / 2 ) ) -> ( ( x ( dist ` G ) u ) + ( y ( dist ` G ) v ) ) < z ) )
27 19 23 25 26 syl3anc 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( ( x ( dist ` G ) u ) < ( z / 2 ) /\ ( y ( dist ` G ) v ) < ( z / 2 ) ) -> ( ( x ( dist ` G ) u ) + ( y ( dist ` G ) v ) ) < z ) )
28 12 2 syl 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> G e. Grp )
29 7 8 grpsubcl 
 |-  ( ( G e. Grp /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ( -g ` G ) y ) e. ( Base ` G ) )
30 28 15 20 29 syl3anc 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( x ( -g ` G ) y ) e. ( Base ` G ) )
31 7 8 grpsubcl 
 |-  ( ( G e. Grp /\ u e. ( Base ` G ) /\ v e. ( Base ` G ) ) -> ( u ( -g ` G ) v ) e. ( Base ` G ) )
32 28 16 21 31 syl3anc 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( u ( -g ` G ) v ) e. ( Base ` G ) )
33 7 8 grpsubcl 
 |-  ( ( G e. Grp /\ u e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( u ( -g ` G ) y ) e. ( Base ` G ) )
34 28 16 20 33 syl3anc 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( u ( -g ` G ) y ) e. ( Base ` G ) )
35 7 17 mstri 
 |-  ( ( G e. MetSp /\ ( ( x ( -g ` G ) y ) e. ( Base ` G ) /\ ( u ( -g ` G ) v ) e. ( Base ` G ) /\ ( u ( -g ` G ) y ) e. ( Base ` G ) ) ) -> ( ( x ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) v ) ) <_ ( ( ( x ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) y ) ) + ( ( u ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) v ) ) ) )
36 13 30 32 34 35 syl13anc 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( x ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) v ) ) <_ ( ( ( x ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) y ) ) + ( ( u ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) v ) ) ) )
37 12 simpld 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> G e. NrmGrp )
38 7 8 17 ngpsubcan 
 |-  ( ( G e. NrmGrp /\ ( x e. ( Base ` G ) /\ u e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( ( x ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) y ) ) = ( x ( dist ` G ) u ) )
39 37 15 16 20 38 syl13anc 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( x ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) y ) ) = ( x ( dist ` G ) u ) )
40 eqid 
 |-  ( +g ` G ) = ( +g ` G )
41 eqid 
 |-  ( invg ` G ) = ( invg ` G )
42 7 40 41 8 grpsubval 
 |-  ( ( u e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( u ( -g ` G ) y ) = ( u ( +g ` G ) ( ( invg ` G ) ` y ) ) )
43 16 20 42 syl2anc 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( u ( -g ` G ) y ) = ( u ( +g ` G ) ( ( invg ` G ) ` y ) ) )
44 7 40 41 8 grpsubval 
 |-  ( ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) -> ( u ( -g ` G ) v ) = ( u ( +g ` G ) ( ( invg ` G ) ` v ) ) )
45 44 adantl 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( u ( -g ` G ) v ) = ( u ( +g ` G ) ( ( invg ` G ) ` v ) ) )
46 43 45 oveq12d 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( u ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) v ) ) = ( ( u ( +g ` G ) ( ( invg ` G ) ` y ) ) ( dist ` G ) ( u ( +g ` G ) ( ( invg ` G ) ` v ) ) ) )
47 7 41 grpinvcl 
 |-  ( ( G e. Grp /\ y e. ( Base ` G ) ) -> ( ( invg ` G ) ` y ) e. ( Base ` G ) )
48 28 20 47 syl2anc 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( invg ` G ) ` y ) e. ( Base ` G ) )
49 7 41 grpinvcl 
 |-  ( ( G e. Grp /\ v e. ( Base ` G ) ) -> ( ( invg ` G ) ` v ) e. ( Base ` G ) )
50 28 21 49 syl2anc 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( invg ` G ) ` v ) e. ( Base ` G ) )
51 7 40 17 ngplcan 
 |-  ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( ( ( invg ` G ) ` y ) e. ( Base ` G ) /\ ( ( invg ` G ) ` v ) e. ( Base ` G ) /\ u e. ( Base ` G ) ) ) -> ( ( u ( +g ` G ) ( ( invg ` G ) ` y ) ) ( dist ` G ) ( u ( +g ` G ) ( ( invg ` G ) ` v ) ) ) = ( ( ( invg ` G ) ` y ) ( dist ` G ) ( ( invg ` G ) ` v ) ) )
52 12 48 50 16 51 syl13anc 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( u ( +g ` G ) ( ( invg ` G ) ` y ) ) ( dist ` G ) ( u ( +g ` G ) ( ( invg ` G ) ` v ) ) ) = ( ( ( invg ` G ) ` y ) ( dist ` G ) ( ( invg ` G ) ` v ) ) )
53 7 41 17 ngpinvds 
 |-  ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( y e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( ( invg ` G ) ` y ) ( dist ` G ) ( ( invg ` G ) ` v ) ) = ( y ( dist ` G ) v ) )
54 12 20 21 53 syl12anc 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( ( invg ` G ) ` y ) ( dist ` G ) ( ( invg ` G ) ` v ) ) = ( y ( dist ` G ) v ) )
55 46 52 54 3eqtrd 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( u ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) v ) ) = ( y ( dist ` G ) v ) )
56 39 55 oveq12d 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( ( x ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) y ) ) + ( ( u ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) v ) ) ) = ( ( x ( dist ` G ) u ) + ( y ( dist ` G ) v ) ) )
57 36 56 breqtrd 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( x ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) v ) ) <_ ( ( x ( dist ` G ) u ) + ( y ( dist ` G ) v ) ) )
58 7 17 mscl 
 |-  ( ( G e. MetSp /\ ( x ( -g ` G ) y ) e. ( Base ` G ) /\ ( u ( -g ` G ) v ) e. ( Base ` G ) ) -> ( ( x ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) v ) ) e. RR )
59 13 30 32 58 syl3anc 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( x ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) v ) ) e. RR )
60 19 23 readdcld 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( x ( dist ` G ) u ) + ( y ( dist ` G ) v ) ) e. RR )
61 lelttr 
 |-  ( ( ( ( x ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) v ) ) e. RR /\ ( ( x ( dist ` G ) u ) + ( y ( dist ` G ) v ) ) e. RR /\ z e. RR ) -> ( ( ( ( x ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) v ) ) <_ ( ( x ( dist ` G ) u ) + ( y ( dist ` G ) v ) ) /\ ( ( x ( dist ` G ) u ) + ( y ( dist ` G ) v ) ) < z ) -> ( ( x ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) v ) ) < z ) )
62 59 60 25 61 syl3anc 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( ( ( x ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) v ) ) <_ ( ( x ( dist ` G ) u ) + ( y ( dist ` G ) v ) ) /\ ( ( x ( dist ` G ) u ) + ( y ( dist ` G ) v ) ) < z ) -> ( ( x ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) v ) ) < z ) )
63 57 62 mpand 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( ( x ( dist ` G ) u ) + ( y ( dist ` G ) v ) ) < z -> ( ( x ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) v ) ) < z ) )
64 27 63 syld 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( ( x ( dist ` G ) u ) < ( z / 2 ) /\ ( y ( dist ` G ) v ) < ( z / 2 ) ) -> ( ( x ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) v ) ) < z ) )
65 15 16 ovresd 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) = ( x ( dist ` G ) u ) )
66 65 breq1d 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) < ( z / 2 ) <-> ( x ( dist ` G ) u ) < ( z / 2 ) ) )
67 20 21 ovresd 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) = ( y ( dist ` G ) v ) )
68 67 breq1d 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) < ( z / 2 ) <-> ( y ( dist ` G ) v ) < ( z / 2 ) ) )
69 66 68 anbi12d 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) < ( z / 2 ) /\ ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) < ( z / 2 ) ) <-> ( ( x ( dist ` G ) u ) < ( z / 2 ) /\ ( y ( dist ` G ) v ) < ( z / 2 ) ) ) )
70 30 32 ovresd 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( x ( -g ` G ) y ) ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ( u ( -g ` G ) v ) ) = ( ( x ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) v ) ) )
71 70 breq1d 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( ( x ( -g ` G ) y ) ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ( u ( -g ` G ) v ) ) < z <-> ( ( x ( -g ` G ) y ) ( dist ` G ) ( u ( -g ` G ) v ) ) < z ) )
72 64 69 71 3imtr4d 
 |-  ( ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) /\ ( u e. ( Base ` G ) /\ v e. ( Base ` G ) ) ) -> ( ( ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) < ( z / 2 ) /\ ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) < ( z / 2 ) ) -> ( ( x ( -g ` G ) y ) ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ( u ( -g ` G ) v ) ) < z ) )
73 72 ralrimivva 
 |-  ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) -> A. u e. ( Base ` G ) A. v e. ( Base ` G ) ( ( ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) < ( z / 2 ) /\ ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) < ( z / 2 ) ) -> ( ( x ( -g ` G ) y ) ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ( u ( -g ` G ) v ) ) < z ) )
74 breq2 
 |-  ( r = ( z / 2 ) -> ( ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) < r <-> ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) < ( z / 2 ) ) )
75 breq2 
 |-  ( r = ( z / 2 ) -> ( ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) < r <-> ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) < ( z / 2 ) ) )
76 74 75 anbi12d 
 |-  ( r = ( z / 2 ) -> ( ( ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) < r /\ ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) < r ) <-> ( ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) < ( z / 2 ) /\ ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) < ( z / 2 ) ) ) )
77 76 imbi1d 
 |-  ( r = ( z / 2 ) -> ( ( ( ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) < r /\ ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) < r ) -> ( ( x ( -g ` G ) y ) ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ( u ( -g ` G ) v ) ) < z ) <-> ( ( ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) < ( z / 2 ) /\ ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) < ( z / 2 ) ) -> ( ( x ( -g ` G ) y ) ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ( u ( -g ` G ) v ) ) < z ) ) )
78 77 2ralbidv 
 |-  ( r = ( z / 2 ) -> ( A. u e. ( Base ` G ) A. v e. ( Base ` G ) ( ( ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) < r /\ ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) < r ) -> ( ( x ( -g ` G ) y ) ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ( u ( -g ` G ) v ) ) < z ) <-> A. u e. ( Base ` G ) A. v e. ( Base ` G ) ( ( ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) < ( z / 2 ) /\ ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) < ( z / 2 ) ) -> ( ( x ( -g ` G ) y ) ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ( u ( -g ` G ) v ) ) < z ) ) )
79 78 rspcev 
 |-  ( ( ( z / 2 ) e. RR+ /\ A. u e. ( Base ` G ) A. v e. ( Base ` G ) ( ( ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) < ( z / 2 ) /\ ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) < ( z / 2 ) ) -> ( ( x ( -g ` G ) y ) ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ( u ( -g ` G ) v ) ) < z ) ) -> E. r e. RR+ A. u e. ( Base ` G ) A. v e. ( Base ` G ) ( ( ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) < r /\ ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) < r ) -> ( ( x ( -g ` G ) y ) ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ( u ( -g ` G ) v ) ) < z ) )
80 11 73 79 syl2an2 
 |-  ( ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ z e. RR+ ) -> E. r e. RR+ A. u e. ( Base ` G ) A. v e. ( Base ` G ) ( ( ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) < r /\ ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) < r ) -> ( ( x ( -g ` G ) y ) ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ( u ( -g ` G ) v ) ) < z ) )
81 80 ralrimiva 
 |-  ( ( ( G e. NrmGrp /\ G e. Abel ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> A. z e. RR+ E. r e. RR+ A. u e. ( Base ` G ) A. v e. ( Base ` G ) ( ( ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) < r /\ ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) < r ) -> ( ( x ( -g ` G ) y ) ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ( u ( -g ` G ) v ) ) < z ) )
82 81 ralrimivva 
 |-  ( ( G e. NrmGrp /\ G e. Abel ) -> A. x e. ( Base ` G ) A. y e. ( Base ` G ) A. z e. RR+ E. r e. RR+ A. u e. ( Base ` G ) A. v e. ( Base ` G ) ( ( ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) < r /\ ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) < r ) -> ( ( x ( -g ` G ) y ) ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ( u ( -g ` G ) v ) ) < z ) )
83 msxms 
 |-  ( G e. MetSp -> G e. *MetSp )
84 eqid 
 |-  ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) = ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) )
85 7 84 xmsxmet 
 |-  ( G e. *MetSp -> ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) e. ( *Met ` ( Base ` G ) ) )
86 4 83 85 3syl 
 |-  ( ( G e. NrmGrp /\ G e. Abel ) -> ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) e. ( *Met ` ( Base ` G ) ) )
87 eqid 
 |-  ( MetOpen ` ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ) = ( MetOpen ` ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) )
88 87 87 87 txmetcn 
 |-  ( ( ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) e. ( *Met ` ( Base ` G ) ) /\ ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) e. ( *Met ` ( Base ` G ) ) /\ ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) e. ( *Met ` ( Base ` G ) ) ) -> ( ( -g ` G ) e. ( ( ( MetOpen ` ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ) tX ( MetOpen ` ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ) ) Cn ( MetOpen ` ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ) ) <-> ( ( -g ` G ) : ( ( Base ` G ) X. ( Base ` G ) ) --> ( Base ` G ) /\ A. x e. ( Base ` G ) A. y e. ( Base ` G ) A. z e. RR+ E. r e. RR+ A. u e. ( Base ` G ) A. v e. ( Base ` G ) ( ( ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) < r /\ ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) < r ) -> ( ( x ( -g ` G ) y ) ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ( u ( -g ` G ) v ) ) < z ) ) ) )
89 86 86 86 88 syl3anc 
 |-  ( ( G e. NrmGrp /\ G e. Abel ) -> ( ( -g ` G ) e. ( ( ( MetOpen ` ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ) tX ( MetOpen ` ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ) ) Cn ( MetOpen ` ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ) ) <-> ( ( -g ` G ) : ( ( Base ` G ) X. ( Base ` G ) ) --> ( Base ` G ) /\ A. x e. ( Base ` G ) A. y e. ( Base ` G ) A. z e. RR+ E. r e. RR+ A. u e. ( Base ` G ) A. v e. ( Base ` G ) ( ( ( x ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) u ) < r /\ ( y ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) v ) < r ) -> ( ( x ( -g ` G ) y ) ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ( u ( -g ` G ) v ) ) < z ) ) ) )
90 10 82 89 mpbir2and 
 |-  ( ( G e. NrmGrp /\ G e. Abel ) -> ( -g ` G ) e. ( ( ( MetOpen ` ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ) tX ( MetOpen ` ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ) ) Cn ( MetOpen ` ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ) ) )
91 eqid 
 |-  ( TopOpen ` G ) = ( TopOpen ` G )
92 91 7 84 mstopn 
 |-  ( G e. MetSp -> ( TopOpen ` G ) = ( MetOpen ` ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ) )
93 4 92 syl 
 |-  ( ( G e. NrmGrp /\ G e. Abel ) -> ( TopOpen ` G ) = ( MetOpen ` ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ) )
94 93 93 oveq12d 
 |-  ( ( G e. NrmGrp /\ G e. Abel ) -> ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) = ( ( MetOpen ` ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ) tX ( MetOpen ` ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ) ) )
95 94 93 oveq12d 
 |-  ( ( G e. NrmGrp /\ G e. Abel ) -> ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) Cn ( TopOpen ` G ) ) = ( ( ( MetOpen ` ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ) tX ( MetOpen ` ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ) ) Cn ( MetOpen ` ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) ) ) )
96 90 95 eleqtrrd 
 |-  ( ( G e. NrmGrp /\ G e. Abel ) -> ( -g ` G ) e. ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) Cn ( TopOpen ` G ) ) )
97 91 8 istgp2 
 |-  ( G e. TopGrp <-> ( G e. Grp /\ G e. TopSp /\ ( -g ` G ) e. ( ( ( TopOpen ` G ) tX ( TopOpen ` G ) ) Cn ( TopOpen ` G ) ) ) )
98 2 6 96 97 syl3anbrc 
 |-  ( ( G e. NrmGrp /\ G e. Abel ) -> G e. TopGrp )