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 𝑁 = ( norm ‘ 𝑊 )
nmfval.x 𝑋 = ( Base ‘ 𝑊 )
nmfval.z 0 = ( 0g𝑊 )
nmfval.d 𝐷 = ( dist ‘ 𝑊 )
Assertion nmval ( 𝐴𝑋 → ( 𝑁𝐴 ) = ( 𝐴 𝐷 0 ) )

Proof

Step Hyp Ref Expression
1 nmfval.n 𝑁 = ( norm ‘ 𝑊 )
2 nmfval.x 𝑋 = ( Base ‘ 𝑊 )
3 nmfval.z 0 = ( 0g𝑊 )
4 nmfval.d 𝐷 = ( dist ‘ 𝑊 )
5 oveq1 ( 𝑥 = 𝐴 → ( 𝑥 𝐷 0 ) = ( 𝐴 𝐷 0 ) )
6 1 2 3 4 nmfval 𝑁 = ( 𝑥𝑋 ↦ ( 𝑥 𝐷 0 ) )
7 ovex ( 𝐴 𝐷 0 ) ∈ V
8 5 6 7 fvmpt ( 𝐴𝑋 → ( 𝑁𝐴 ) = ( 𝐴 𝐷 0 ) )