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

Metamath Proof Explorer

Theorem nmgt0

Description: The norm of a nonzero element is a positive real. (Contributed by NM, 20-Nov-2007) (Revised by AV, 8-Oct-2021)

Ref Expression
Hypotheses nmgt0.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
nmgt0.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
nmgt0.z ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion nmgt0 ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ≠ 0 ↔ 0 < ( 𝑁 ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 nmgt0.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 nmgt0.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
3 nmgt0.z ⊢ 0 = ( 0g ‘ 𝐺 )
4 1 2 3 nmeq0 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )
5 4 necon3bid ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ 0 ) )
6 1 2 nmcl ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
7 1 2 nmge0 ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ 𝐴 ) )
8 ne0gt0 ⊢ ( ( ( 𝑁 ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 𝑁 ‘ 𝐴 ) ) → ( ( 𝑁 ‘ 𝐴 ) ≠ 0 ↔ 0 < ( 𝑁 ‘ 𝐴 ) ) )
9 6 7 8 syl2anc ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) ≠ 0 ↔ 0 < ( 𝑁 ‘ 𝐴 ) ) )
10 5 9 bitr3d ⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ≠ 0 ↔ 0 < ( 𝑁 ‘ 𝐴 ) ) )