Metamath Proof Explorer

Theorem tngval

Description: Value of the function which augments a given structure G with a norm N . (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses tngval.t 
|- T = ( G toNrmGrp N )
tngval.m 
|- .- = ( -g ` G )
tngval.d 
|- D = ( N o. .- )
tngval.j 
|- J = ( MetOpen ` D )
Assertion tngval 
|- ( ( G e. V /\ N e. W ) -> T = ( ( G sSet <. ( dist ` ndx ) , D >. ) sSet <. ( TopSet ` ndx ) , J >. ) )

Proof

Step Hyp Ref Expression
1 tngval.t 
 |-  T = ( G toNrmGrp N )
2 tngval.m 
 |-  .- = ( -g ` G )
3 tngval.d 
 |-  D = ( N o. .- )
4 tngval.j 
 |-  J = ( MetOpen ` D )
5 elex 
 |-  ( G e. V -> G e. _V )
6 elex 
 |-  ( N e. W -> N e. _V )
7 simpl 
 |-  ( ( g = G /\ f = N ) -> g = G )
8 simpr 
 |-  ( ( g = G /\ f = N ) -> f = N )
9 7 fveq2d 
 |-  ( ( g = G /\ f = N ) -> ( -g ` g ) = ( -g ` G ) )
10 9 2 eqtr4di 
 |-  ( ( g = G /\ f = N ) -> ( -g ` g ) = .- )
11 8 10 coeq12d 
 |-  ( ( g = G /\ f = N ) -> ( f o. ( -g ` g ) ) = ( N o. .- ) )
12 11 3 eqtr4di 
 |-  ( ( g = G /\ f = N ) -> ( f o. ( -g ` g ) ) = D )
13 12 opeq2d 
 |-  ( ( g = G /\ f = N ) -> <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. = <. ( dist ` ndx ) , D >. )
14 7 13 oveq12d 
 |-  ( ( g = G /\ f = N ) -> ( g sSet <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. ) = ( G sSet <. ( dist ` ndx ) , D >. ) )
15 12 fveq2d 
 |-  ( ( g = G /\ f = N ) -> ( MetOpen ` ( f o. ( -g ` g ) ) ) = ( MetOpen ` D ) )
16 15 4 eqtr4di 
 |-  ( ( g = G /\ f = N ) -> ( MetOpen ` ( f o. ( -g ` g ) ) ) = J )
17 16 opeq2d 
 |-  ( ( g = G /\ f = N ) -> <. ( TopSet ` ndx ) , ( MetOpen ` ( f o. ( -g ` g ) ) ) >. = <. ( TopSet ` ndx ) , J >. )
18 14 17 oveq12d 
 |-  ( ( g = G /\ f = N ) -> ( ( g sSet <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( f o. ( -g ` g ) ) ) >. ) = ( ( G sSet <. ( dist ` ndx ) , D >. ) sSet <. ( TopSet ` ndx ) , J >. ) )
19 df-tng 
 |-  toNrmGrp = ( g e. _V , f e. _V |-> ( ( g sSet <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. ) sSet <. ( TopSet ` ndx ) , ( MetOpen ` ( f o. ( -g ` g ) ) ) >. ) )
20 ovex 
 |-  ( ( G sSet <. ( dist ` ndx ) , D >. ) sSet <. ( TopSet ` ndx ) , J >. ) e. _V
21 18 19 20 ovmpoa 
 |-  ( ( G e. _V /\ N e. _V ) -> ( G toNrmGrp N ) = ( ( G sSet <. ( dist ` ndx ) , D >. ) sSet <. ( TopSet ` ndx ) , J >. ) )
22 5 6 21 syl2an 
 |-  ( ( G e. V /\ N e. W ) -> ( G toNrmGrp N ) = ( ( G sSet <. ( dist ` ndx ) , D >. ) sSet <. ( TopSet ` ndx ) , J >. ) )
23 1 22 syl5eq 
 |-  ( ( G e. V /\ N e. W ) -> T = ( ( G sSet <. ( dist ` ndx ) , D >. ) sSet <. ( TopSet ` ndx ) , J >. ) )