Metamath Proof Explorer


Theorem nmval

Description: The value of the norm as the distance to zero. Problem 1 of Kreyszig p. 63. (Contributed by NM, 4-Dec-2006) (Revised 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 nmval
|- ( A e. X -> ( N ` A ) = ( A 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 oveq1
 |-  ( x = A -> ( x D .0. ) = ( A D .0. ) )
6 1 2 3 4 nmfval
 |-  N = ( x e. X |-> ( x D .0. ) )
7 ovex
 |-  ( A D .0. ) e. _V
8 5 6 7 fvmpt
 |-  ( A e. X -> ( N ` A ) = ( A D .0. ) )