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

Metamath Proof Explorer

Theorem nzrunit

Description: A unit is nonzero in any nonzero ring. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses nzrunit.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
nzrunit.2 ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion nzrunit ( ( 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → 𝐴 ≠ 0 )

Proof

Step Hyp Ref Expression
1 nzrunit.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
2 nzrunit.2 ⊢ 0 = ( 0g ‘ 𝑅 )
3 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
4 3 2 nzrnz ⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ 0 )
5 nzrring ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
6 1 2 3 0unit ⊢ ( 𝑅 ∈ Ring → ( 0 ∈ 𝑈 ↔ ( 1r ‘ 𝑅 ) = 0 ) )
7 6 necon3bbid ⊢ ( 𝑅 ∈ Ring → ( ¬ 0 ∈ 𝑈 ↔ ( 1r ‘ 𝑅 ) ≠ 0 ) )
8 5 7 syl ⊢ ( 𝑅 ∈ NzRing → ( ¬ 0 ∈ 𝑈 ↔ ( 1r ‘ 𝑅 ) ≠ 0 ) )
9 4 8 mpbird ⊢ ( 𝑅 ∈ NzRing → ¬ 0 ∈ 𝑈 )
10 eleq1 ⊢ ( 𝐴 = 0 → ( 𝐴 ∈ 𝑈 ↔ 0 ∈ 𝑈 ) )
11 10 notbid ⊢ ( 𝐴 = 0 → ( ¬ 𝐴 ∈ 𝑈 ↔ ¬ 0 ∈ 𝑈 ) )
12 9 11 syl5ibrcom ⊢ ( 𝑅 ∈ NzRing → ( 𝐴 = 0 → ¬ 𝐴 ∈ 𝑈 ) )
13 12 necon2ad ⊢ ( 𝑅 ∈ NzRing → ( 𝐴 ∈ 𝑈 → 𝐴 ≠ 0 ) )
14 13 imp ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐴 ∈ 𝑈 ) → 𝐴 ≠ 0 )