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 = 0 vec ⁡ U
nvz0.6 ⊢ N = norm CV ⁡ U
Assertion nvz0 ⊢ U ∈ NrmCVec → N ⁡ Z = 0

Proof

Step Hyp Ref Expression
1 nvz0.5 ⊢ Z = 0 vec ⁡ U
2 nvz0.6 ⊢ N = norm CV ⁡ 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 ⁡ U Z = 0 ⋅ N ⁡ Z
10 7 9 mp3an2 ⊢ U ∈ NrmCVec ∧ Z ∈ BaseSet ⁡ U → N ⁡ 0 ⋅ 𝑠OLD ⁡ U Z = 0 ⋅ N ⁡ Z
11 4 10 mpdan ⊢ U ∈ NrmCVec → N ⁡ 0 ⋅ 𝑠OLD ⁡ U Z = 0 ⋅ N ⁡ Z
12 3 8 1 nv0 ⊢ U ∈ NrmCVec ∧ Z ∈ BaseSet ⁡ U → 0 ⋅ 𝑠OLD ⁡ U Z = Z
13 4 12 mpdan ⊢ U ∈ NrmCVec → 0 ⋅ 𝑠OLD ⁡ U Z = Z
14 13 fveq2d ⊢ U ∈ NrmCVec → N ⁡ 0 ⋅ 𝑠OLD ⁡ U Z = 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