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