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. ) ) |
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. ) ) |