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	⊢ 𝐸 = ( 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 ∈ 𝐸 )