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

Metamath Proof Explorer

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 < ( 𝑁 ‘ 𝐴 ) ) )