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 e. _V
Assertion tngnm 
|- ( ( G e. 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 e. _V
4 simpr 
 |-  ( ( G e. Grp /\ N : X --> A ) -> N : X --> A )
5 4 feqmptd 
 |-  ( ( G e. Grp /\ N : X --> A ) -> N = ( x e. X |-> ( N ` x ) ) )
6 eqid 
 |-  ( -g ` G ) = ( -g ` G )
7 2 6 grpsubf 
 |-  ( G e. Grp -> ( -g ` G ) : ( X X. X ) --> X )
8 7 ad2antrr 
 |-  ( ( ( G e. Grp /\ N : X --> A ) /\ x e. X ) -> ( -g ` G ) : ( X X. X ) --> X )
9 simpr 
 |-  ( ( ( G e. Grp /\ N : X --> A ) /\ x e. X ) -> x e. X )
10 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
11 2 10 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. X )
12 11 ad2antrr 
 |-  ( ( ( G e. Grp /\ N : X --> A ) /\ x e. X ) -> ( 0g ` G ) e. X )
13 9 12 opelxpd 
 |-  ( ( ( G e. Grp /\ N : X --> A ) /\ x e. X ) -> <. x , ( 0g ` G ) >. e. ( X X. X ) )
14 fvco3 
 |-  ( ( ( -g ` G ) : ( X X. X ) --> X /\ <. x , ( 0g ` G ) >. e. ( X X. X ) ) -> ( ( N o. ( -g ` G ) ) ` <. x , ( 0g ` G ) >. ) = ( N ` ( ( -g ` G ) ` <. x , ( 0g ` G ) >. ) ) )
15 8 13 14 syl2anc 
 |-  ( ( ( G e. Grp /\ N : X --> A ) /\ x e. X ) -> ( ( N o. ( -g ` G ) ) ` <. x , ( 0g ` G ) >. ) = ( N ` ( ( -g ` G ) ` <. x , ( 0g ` G ) >. ) ) )
16 df-ov 
 |-  ( x ( N o. ( -g ` G ) ) ( 0g ` G ) ) = ( ( N o. ( -g ` G ) ) ` <. x , ( 0g ` G ) >. )
17 df-ov 
 |-  ( x ( -g ` G ) ( 0g ` G ) ) = ( ( -g ` G ) ` <. x , ( 0g ` G ) >. )
18 17 fveq2i 
 |-  ( N ` ( x ( -g ` G ) ( 0g ` G ) ) ) = ( N ` ( ( -g ` G ) ` <. x , ( 0g ` G ) >. ) )
19 15 16 18 3eqtr4g 
 |-  ( ( ( G e. Grp /\ N : X --> A ) /\ x e. X ) -> ( x ( N o. ( -g ` G ) ) ( 0g ` G ) ) = ( N ` ( x ( -g ` G ) ( 0g ` G ) ) ) )
20 2 10 6 grpsubid1 
 |-  ( ( G e. Grp /\ x e. X ) -> ( x ( -g ` G ) ( 0g ` G ) ) = x )
21 20 adantlr 
 |-  ( ( ( G e. Grp /\ N : X --> A ) /\ x e. X ) -> ( x ( -g ` G ) ( 0g ` G ) ) = x )
22 21 fveq2d 
 |-  ( ( ( G e. Grp /\ N : X --> A ) /\ x e. X ) -> ( N ` ( x ( -g ` G ) ( 0g ` G ) ) ) = ( N ` x ) )
23 19 22 eqtr2d 
 |-  ( ( ( G e. Grp /\ N : X --> A ) /\ x e. X ) -> ( N ` x ) = ( x ( N o. ( -g ` G ) ) ( 0g ` G ) ) )
24 23 mpteq2dva 
 |-  ( ( G e. Grp /\ N : X --> A ) -> ( x e. X |-> ( N ` x ) ) = ( x e. X |-> ( x ( N o. ( -g ` G ) ) ( 0g ` G ) ) ) )
25 2 fvexi 
 |-  X e. _V
26 fex2 
 |-  ( ( N : X --> A /\ X e. _V /\ A e. _V ) -> N e. _V )
27 25 3 26 mp3an23 
 |-  ( N : X --> A -> N e. _V )
28 27 adantl 
 |-  ( ( G e. Grp /\ N : X --> A ) -> N e. _V )
29 1 2 tngbas 
 |-  ( N e. _V -> X = ( Base ` T ) )
30 28 29 syl 
 |-  ( ( G e. Grp /\ N : X --> A ) -> X = ( Base ` T ) )
31 1 6 tngds 
 |-  ( N e. _V -> ( N o. ( -g ` G ) ) = ( dist ` T ) )
32 28 31 syl 
 |-  ( ( G e. Grp /\ N : X --> A ) -> ( N o. ( -g ` G ) ) = ( dist ` T ) )
33 eqidd 
 |-  ( ( G e. Grp /\ N : X --> A ) -> x = x )
34 1 10 tng0 
 |-  ( N e. _V -> ( 0g ` G ) = ( 0g ` T ) )
35 28 34 syl 
 |-  ( ( G e. Grp /\ N : X --> A ) -> ( 0g ` G ) = ( 0g ` T ) )
36 32 33 35 oveq123d 
 |-  ( ( G e. Grp /\ N : X --> A ) -> ( x ( N o. ( -g ` G ) ) ( 0g ` G ) ) = ( x ( dist ` T ) ( 0g ` T ) ) )
37 30 36 mpteq12dv 
 |-  ( ( G e. Grp /\ N : X --> A ) -> ( x e. X |-> ( x ( N o. ( -g ` G ) ) ( 0g ` G ) ) ) = ( x e. ( Base ` T ) |-> ( x ( dist ` T ) ( 0g ` T ) ) ) )
38 eqid 
 |-  ( norm ` T ) = ( norm ` T )
39 eqid 
 |-  ( Base ` T ) = ( Base ` T )
40 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
41 eqid 
 |-  ( dist ` T ) = ( dist ` T )
42 38 39 40 41 nmfval 
 |-  ( norm ` T ) = ( x e. ( Base ` T ) |-> ( x ( dist ` T ) ( 0g ` T ) ) )
43 37 42 eqtr4di 
 |-  ( ( G e. Grp /\ N : X --> A ) -> ( x e. X |-> ( x ( N o. ( -g ` G ) ) ( 0g ` G ) ) ) = ( norm ` T ) )
44 5 24 43 3eqtrd 
 |-  ( ( G e. Grp /\ N : X --> A ) -> N = ( norm ` T ) )