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 )