Theorem rrgnz

Description: In a nonzero ring, the zero is a left zero divisor (that is, not a left-regular element). (Contributed by Thierry Arnoux, 6-May-2025)

	Ref	Expression
Hypotheses	rrgnz.t	|- E = ( RLReg ` R )
	rrgnz.z	|- .0. = ( 0g ` R )
Assertion	rrgnz	|- ( R e. NzRing -> -. .0. e. E )

Proof

Step	Hyp	Ref	Expression
1		rrgnz.t	|- E = ( RLReg ` R )
2		rrgnz.z	|- .0. = ( 0g ` R )
3		eqid	|- ( 1r ` R ) = ( 1r ` R )
4	3 2	nzrnz	|- ( R e. NzRing -> ( 1r ` R ) =/= .0. )
5	4	neneqd	|- ( R e. NzRing -> -. ( 1r ` R ) = .0. )
6		nzrring	|- ( R e. NzRing -> R e. Ring )
7	6	adantr	|- ( ( R e. NzRing /\ .0. e. E ) -> R e. Ring )
8		simpr	|- ( ( R e. NzRing /\ .0. e. E ) -> .0. e. E )
9		eqid	|- ( Base ` R ) = ( Base ` R )
10	9 3	ringidcl	|- ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
11	7 10	syl	|- ( ( R e. NzRing /\ .0. e. E ) -> ( 1r ` R ) e. ( Base ` R ) )
12		eqid	|- ( .r ` R ) = ( .r ` R )
13	9 12 2 7 11	ringlzd	|- ( ( R e. NzRing /\ .0. e. E ) -> ( .0. ( .r ` R ) ( 1r ` R ) ) = .0. )
14	1 9 12 2	rrgeq0	|- ( ( R e. Ring /\ .0. e. E /\ ( 1r ` R ) e. ( Base ` R ) ) -> ( ( .0. ( .r ` R ) ( 1r ` R ) ) = .0. <-> ( 1r ` R ) = .0. ) )
15	14	biimpa	|- ( ( ( R e. Ring /\ .0. e. E /\ ( 1r ` R ) e. ( Base ` R ) ) /\ ( .0. ( .r ` R ) ( 1r ` R ) ) = .0. ) -> ( 1r ` R ) = .0. )
16	7 8 11 13 15	syl31anc	|- ( ( R e. NzRing /\ .0. e. E ) -> ( 1r ` R ) = .0. )
17	5 16	mtand	|- ( R e. NzRing -> -. .0. e. E )