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

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 ⊢ 𝑍 = ( 0vec ‘ 𝑈 )
nvz0.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
Assertion nvz0 ( 𝑈 ∈ NrmCVec → ( 𝑁 ‘ 𝑍 ) = 0 )

Proof

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