Theorem unitnmn0

Description: The norm of a unit is nonzero in a nonzero normed ring. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypotheses	nminvr.n	⊢ 𝑁 = ( norm ‘ 𝑅 )
	nminvr.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
Assertion	unitnmn0	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → ( 𝑁 ‘ 𝐴 ) ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		nminvr.n	⊢ 𝑁 = ( norm ‘ 𝑅 )
2		nminvr.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3		nrgngp	⊢ ( 𝑅 ∈ NrmRing → 𝑅 ∈ NrmGrp )
4	3	3ad2ant1	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → 𝑅 ∈ NrmGrp )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6	5 2	unitcl	⊢ ( 𝐴 ∈ 𝑈 → 𝐴 ∈ ( Base ‘ 𝑅 ) )
7	6	3ad2ant3	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
8		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
9	2 8	nzrunit	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → 𝐴 ≠ ( 0g ‘ 𝑅 ) )
10	9	3adant1	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → 𝐴 ≠ ( 0g ‘ 𝑅 ) )
11	5 1 8	nmne0	⊢ ( ( 𝑅 ∈ NrmGrp ∧ 𝐴 ∈ ( Base ‘ 𝑅 ) ∧ 𝐴 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑁 ‘ 𝐴 ) ≠ 0 )
12	4 7 10 11	syl3anc	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → ( 𝑁 ‘ 𝐴 ) ≠ 0 )