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 E = RLReg R
rrgnz.z 0 ˙ = 0 R
Assertion rrgnz R NzRing ¬ 0 ˙ E

Proof

Step Hyp Ref Expression
1 rrgnz.t E = RLReg R
2 rrgnz.z 0 ˙ = 0 R
3 eqid 1 R = 1 R
4 3 2 nzrnz R NzRing 1 R 0 ˙
5 4 neneqd R NzRing ¬ 1 R = 0 ˙
6 nzrring R NzRing R Ring
7 6 adantr R NzRing 0 ˙ E R Ring
8 simpr R NzRing 0 ˙ E 0 ˙ E
9 eqid Base R = Base R
10 9 3 ringidcl R Ring 1 R Base R
11 7 10 syl R NzRing 0 ˙ E 1 R Base R
12 eqid R = R
13 9 12 2 7 11 ringlzd R NzRing 0 ˙ E 0 ˙ R 1 R = 0 ˙
14 1 9 12 2 rrgeq0 R Ring 0 ˙ E 1 R Base R 0 ˙ R 1 R = 0 ˙ 1 R = 0 ˙
15 14 biimpa R Ring 0 ˙ E 1 R Base R 0 ˙ R 1 R = 0 ˙ 1 R = 0 ˙
16 7 8 11 13 15 syl31anc R NzRing 0 ˙ E 1 R = 0 ˙
17 5 16 mtand R NzRing ¬ 0 ˙ E