Theorem nmrpcl

Description: The norm of a nonzero element is a positive real. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	nmf.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	nmf.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
	nmeq0.z	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	nmrpcl	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ+ )

Proof

Step	Hyp	Ref	Expression
1		nmf.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		nmf.n	⊢ 𝑁 = ( norm ‘ 𝐺 )
3		nmeq0.z	⊢ 0 = ( 0g ‘ 𝐺 )
4	1 2	nmcl	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
5	4	3adant3	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
6	1 2	nmge0	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ 𝐴 ) )
7	6	3adant3	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) → 0 ≤ ( 𝑁 ‘ 𝐴 ) )
8	1 2 3	nmne0	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) → ( 𝑁 ‘ 𝐴 ) ≠ 0 )
9	5 7 8	ne0gt0d	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) → 0 < ( 𝑁 ‘ 𝐴 ) )
10	5 9	elrpd	⊢ ( ( 𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 0 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ+ )