Theorem nvgt0

Description: A nonzero norm is positive. (Contributed by NM, 20-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvgt0.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	nvgt0.5	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
	nvgt0.6	⊢ 𝑁 = ( normCV ‘ 𝑈 )
Assertion	nvgt0	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ≠ 𝑍 ↔ 0 < ( 𝑁 ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nvgt0.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nvgt0.5	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
3		nvgt0.6	⊢ 𝑁 = ( normCV ‘ 𝑈 )
4	1 2 3	nvz	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) = 0 ↔ 𝐴 = 𝑍 ) )
5	4	necon3bid	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ 𝑍 ) )
6	1 3	nvcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
7	1 3	nvge0	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ 𝐴 ) )
8		ne0gt0	⊢ ( ( ( 𝑁 ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 𝑁 ‘ 𝐴 ) ) → ( ( 𝑁 ‘ 𝐴 ) ≠ 0 ↔ 0 < ( 𝑁 ‘ 𝐴 ) ) )
9	6 7 8	syl2anc	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) ≠ 0 ↔ 0 < ( 𝑁 ‘ 𝐴 ) ) )
10	5 9	bitr3d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ≠ 𝑍 ↔ 0 < ( 𝑁 ‘ 𝐴 ) ) )