This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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