Metamath Proof Explorer

Theorem nvz0

Description: The norm of a zero vector is zero. (Contributed by NM, 24-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nvz0.5 ⊢Z=0vec⁡U
nvz0.6 ⊢N=normCV⁡U
Assertion nvz0 ⊢U∈NrmCVec→N⁡Z=0

Proof

Step Hyp Ref Expression
1 nvz0.5 ⊢Z=0vec⁡U
2 nvz0.6 ⊢N=normCV⁡U
3 eqid ⊢BaseSet⁡U=BaseSet⁡U
4 3 1 nvzcl ⊢U∈NrmCVec→Z∈BaseSet⁡U
5 0re ⊢0∈ℝ
6 0le0 ⊢0≤0
7 5 6 pm3.2i ⊢0∈ℝ∧0≤0
8 eqid ⊢⋅𝑠OLD⁡U=⋅𝑠OLD⁡U
9 3 8 2 nvsge0 ⊢U∈NrmCVec∧0∈ℝ∧0≤0∧Z∈BaseSet⁡U→N⁡0⋅𝑠OLD⁡UZ=0⋅N⁡Z
10 7 9 mp3an2 ⊢U∈NrmCVec∧Z∈BaseSet⁡U→N⁡0⋅𝑠OLD⁡UZ=0⋅N⁡Z
11 4 10 mpdan ⊢U∈NrmCVec→N⁡0⋅𝑠OLD⁡UZ=0⋅N⁡Z
12 3 8 1 nv0 ⊢U∈NrmCVec∧Z∈BaseSet⁡U→0⋅𝑠OLD⁡UZ=Z
13 4 12 mpdan ⊢U∈NrmCVec→0⋅𝑠OLD⁡UZ=Z
14 13 fveq2d ⊢U∈NrmCVec→N⁡0⋅𝑠OLD⁡UZ=N⁡Z
15 3 2 nvcl ⊢U∈NrmCVec∧Z∈BaseSet⁡U→N⁡Z∈ℝ
16 15 recnd ⊢U∈NrmCVec∧Z∈BaseSet⁡U→N⁡Z∈ℂ
17 4 16 mpdan ⊢U∈NrmCVec→N⁡Z∈ℂ
18 17 mul02d ⊢U∈NrmCVec→0⋅N⁡Z=0
19 11 14 18 3eqtr3d ⊢U∈NrmCVec→N⁡Z=0