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

Metamath Proof Explorer

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 )