Metamath Proof Explorer


Theorem tngnm

Description: The topology generated by a normed structure. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses tngnm.t T = G toNrmGrp N
tngnm.x X = Base G
tngnm.a A V
Assertion tngnm G Grp N : X A N = norm T

Proof

Step Hyp Ref Expression
1 tngnm.t T = G toNrmGrp N
2 tngnm.x X = Base G
3 tngnm.a A V
4 simpr G Grp N : X A N : X A
5 4 feqmptd G Grp N : X A N = x X N x
6 eqid - G = - G
7 2 6 grpsubf G Grp - G : X × X X
8 7 ad2antrr G Grp N : X A x X - G : X × X X
9 simpr G Grp N : X A x X x X
10 eqid 0 G = 0 G
11 2 10 grpidcl G Grp 0 G X
12 11 ad2antrr G Grp N : X A x X 0 G X
13 9 12 opelxpd G Grp N : X A x X x 0 G X × X
14 fvco3 - G : X × X X x 0 G X × X N - G x 0 G = N - G x 0 G
15 8 13 14 syl2anc G Grp N : X A x X N - G x 0 G = N - G x 0 G
16 df-ov x N - G 0 G = N - G x 0 G
17 df-ov x - G 0 G = - G x 0 G
18 17 fveq2i N x - G 0 G = N - G x 0 G
19 15 16 18 3eqtr4g G Grp N : X A x X x N - G 0 G = N x - G 0 G
20 2 10 6 grpsubid1 G Grp x X x - G 0 G = x
21 20 adantlr G Grp N : X A x X x - G 0 G = x
22 21 fveq2d G Grp N : X A x X N x - G 0 G = N x
23 19 22 eqtr2d G Grp N : X A x X N x = x N - G 0 G
24 23 mpteq2dva G Grp N : X A x X N x = x X x N - G 0 G
25 2 fvexi X V
26 fex2 N : X A X V A V N V
27 25 3 26 mp3an23 N : X A N V
28 27 adantl G Grp N : X A N V
29 1 2 tngbas N V X = Base T
30 28 29 syl G Grp N : X A X = Base T
31 1 6 tngds N V N - G = dist T
32 28 31 syl G Grp N : X A N - G = dist T
33 eqidd G Grp N : X A x = x
34 1 10 tng0 N V 0 G = 0 T
35 28 34 syl G Grp N : X A 0 G = 0 T
36 32 33 35 oveq123d G Grp N : X A x N - G 0 G = x dist T 0 T
37 30 36 mpteq12dv G Grp N : X A x X x N - G 0 G = x Base T x dist T 0 T
38 eqid norm T = norm T
39 eqid Base T = Base T
40 eqid 0 T = 0 T
41 eqid dist T = dist T
42 38 39 40 41 nmfval norm T = x Base T x dist T 0 T
43 37 42 eqtr4di G Grp N : X A x X x N - G 0 G = norm T
44 5 24 43 3eqtrd G Grp N : X A N = norm T