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 NrmGrp G Abel G TopGrp

Proof

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