Metamath Proof Explorer


Theorem rrgnz

Description: In a non-zero ring, the zero is not a nonzero-divisors. (Contributed by Thierry Arnoux, 6-May-2025)

Ref Expression
Hypotheses rrgnz.t 𝐸 = ( RLReg ‘ 𝑅 )
rrgnz.z 0 = ( 0g𝑅 )
Assertion rrgnz ( 𝑅 ∈ NzRing → ¬ 0𝐸 )

Proof

Step Hyp Ref Expression
1 rrgnz.t 𝐸 = ( RLReg ‘ 𝑅 )
2 rrgnz.z 0 = ( 0g𝑅 )
3 eqid ( 1r𝑅 ) = ( 1r𝑅 )
4 3 2 nzrnz ( 𝑅 ∈ NzRing → ( 1r𝑅 ) ≠ 0 )
5 4 neneqd ( 𝑅 ∈ NzRing → ¬ ( 1r𝑅 ) = 0 )
6 nzrring ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
7 6 adantr ( ( 𝑅 ∈ NzRing ∧ 0𝐸 ) → 𝑅 ∈ Ring )
8 simpr ( ( 𝑅 ∈ NzRing ∧ 0𝐸 ) → 0𝐸 )
9 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 9 3 ringidcl ( 𝑅 ∈ Ring → ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) )
11 7 10 syl ( ( 𝑅 ∈ NzRing ∧ 0𝐸 ) → ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) )
12 eqid ( .r𝑅 ) = ( .r𝑅 )
13 9 12 2 7 11 ringlzd ( ( 𝑅 ∈ NzRing ∧ 0𝐸 ) → ( 0 ( .r𝑅 ) ( 1r𝑅 ) ) = 0 )
14 1 9 12 2 rrgeq0 ( ( 𝑅 ∈ Ring ∧ 0𝐸 ∧ ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 0 ( .r𝑅 ) ( 1r𝑅 ) ) = 0 ↔ ( 1r𝑅 ) = 0 ) )
15 14 biimpa ( ( ( 𝑅 ∈ Ring ∧ 0𝐸 ∧ ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) ) ∧ ( 0 ( .r𝑅 ) ( 1r𝑅 ) ) = 0 ) → ( 1r𝑅 ) = 0 )
16 7 8 11 13 15 syl31anc ( ( 𝑅 ∈ NzRing ∧ 0𝐸 ) → ( 1r𝑅 ) = 0 )
17 5 16 mtand ( 𝑅 ∈ NzRing → ¬ 0𝐸 )