Metamath Proof Explorer

Theorem nmfval

Description: The value of the norm function as the distance to zero. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses nmfval.n 
|- N = ( norm ` W )
nmfval.x 
|- X = ( Base ` W )
nmfval.z 
|- .0. = ( 0g ` W )
nmfval.d 
|- D = ( dist ` W )
Assertion nmfval 
|- N = ( x e. X |-> ( x D .0. ) )

Proof

Step Hyp Ref Expression
1 nmfval.n 
 |-  N = ( norm ` W )
2 nmfval.x 
 |-  X = ( Base ` W )
3 nmfval.z 
 |-  .0. = ( 0g ` W )
4 nmfval.d 
 |-  D = ( dist ` W )
5 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
6 5 2 eqtr4di 
 |-  ( w = W -> ( Base ` w ) = X )
7 fveq2 
 |-  ( w = W -> ( dist ` w ) = ( dist ` W ) )
8 7 4 eqtr4di 
 |-  ( w = W -> ( dist ` w ) = D )
9 eqidd 
 |-  ( w = W -> x = x )
10 fveq2 
 |-  ( w = W -> ( 0g ` w ) = ( 0g ` W ) )
11 10 3 eqtr4di 
 |-  ( w = W -> ( 0g ` w ) = .0. )
12 8 9 11 oveq123d 
 |-  ( w = W -> ( x ( dist ` w ) ( 0g ` w ) ) = ( x D .0. ) )
13 6 12 mpteq12dv 
 |-  ( w = W -> ( x e. ( Base ` w ) |-> ( x ( dist ` w ) ( 0g ` w ) ) ) = ( x e. X |-> ( x D .0. ) ) )
14 df-nm 
 |-  norm = ( w e. _V |-> ( x e. ( Base ` w ) |-> ( x ( dist ` w ) ( 0g ` w ) ) ) )
15 eqid 
 |-  ( x e. X |-> ( x D .0. ) ) = ( x e. X |-> ( x D .0. ) )
16 df-ov 
 |-  ( x D .0. ) = ( D ` <. x , .0. >. )
17 fvrn0 
 |-  ( D ` <. x , .0. >. ) e. ( ran D u. { (/) } )
18 16 17 eqeltri 
 |-  ( x D .0. ) e. ( ran D u. { (/) } )
19 18 a1i 
 |-  ( x e. X -> ( x D .0. ) e. ( ran D u. { (/) } ) )
20 15 19 fmpti 
 |-  ( x e. X |-> ( x D .0. ) ) : X --> ( ran D u. { (/) } )
21 2 fvexi 
 |-  X e. _V
22 4 fvexi 
 |-  D e. _V
23 22 rnex 
 |-  ran D e. _V
24 p0ex 
 |-  { (/) } e. _V
25 23 24 unex 
 |-  ( ran D u. { (/) } ) e. _V
26 fex2 
 |-  ( ( ( x e. X |-> ( x D .0. ) ) : X --> ( ran D u. { (/) } ) /\ X e. _V /\ ( ran D u. { (/) } ) e. _V ) -> ( x e. X |-> ( x D .0. ) ) e. _V )
27 20 21 25 26 mp3an 
 |-  ( x e. X |-> ( x D .0. ) ) e. _V
28 13 14 27 fvmpt 
 |-  ( W e. _V -> ( norm ` W ) = ( x e. X |-> ( x D .0. ) ) )
29 fvprc 
 |-  ( -. W e. _V -> ( norm ` W ) = (/) )
30 mpt0 
 |-  ( x e. (/) |-> ( x D .0. ) ) = (/)
31 29 30 eqtr4di 
 |-  ( -. W e. _V -> ( norm ` W ) = ( x e. (/) |-> ( x D .0. ) ) )
32 fvprc 
 |-  ( -. W e. _V -> ( Base ` W ) = (/) )
33 2 32 syl5eq 
 |-  ( -. W e. _V -> X = (/) )
34 33 mpteq1d 
 |-  ( -. W e. _V -> ( x e. X |-> ( x D .0. ) ) = ( x e. (/) |-> ( x D .0. ) ) )
35 31 34 eqtr4d 
 |-  ( -. W e. _V -> ( norm ` W ) = ( x e. X |-> ( x D .0. ) ) )
36 28 35 pm2.61i 
 |-  ( norm ` W ) = ( x e. X |-> ( x D .0. ) )
37 1 36 eqtri 
 |-  N = ( x e. X |-> ( x D .0. ) )