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