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

Metamath Proof Explorer

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	$⊢ \underset{˙}{0} = 0_{R}$
	Assertion	rrgnz	$⊢ R \in NzRing \to \neg \underset{˙}{0} \in E$

Proof

Step	Hyp	Ref	Expression
1		rrgnz.t	$⊢ E = RLReg (R)$
2		rrgnz.z	$⊢ \underset{˙}{0} = 0_{R}$
3		eqid	$⊢ 1_{R} = 1_{R}$
4	3 2	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq \underset{˙}{0}$
5	4	neneqd	$⊢ R \in NzRing \to \neg 1_{R} = \underset{˙}{0}$
6		nzrring	$⊢ R \in NzRing \to R \in Ring$
7	6	adantr	$⊢ (R \in NzRing \land \underset{˙}{0} \in E) \to R \in Ring$
8		simpr	$⊢ (R \in NzRing \land \underset{˙}{0} \in E) \to \underset{˙}{0} \in E$
9		eqid	$⊢ {Base}_{R} = {Base}_{R}$
10	9 3	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
11	7 10	syl	$⊢ (R \in NzRing \land \underset{˙}{0} \in E) \to 1_{R} \in {Base}_{R}$
12		eqid	$⊢ \cdot_{R} = \cdot_{R}$
13	9 12 2 7 11	ringlzd	$⊢ (R \in NzRing \land \underset{˙}{0} \in E) \to \underset{˙}{0} \cdot_{R} 1_{R} = \underset{˙}{0}$
14	1 9 12 2	rrgeq0	$⊢ (R \in Ring \land \underset{˙}{0} \in E \land 1_{R} \in {Base}_{R}) \to (\underset{˙}{0} \cdot_{R} 1_{R} = \underset{˙}{0} \leftrightarrow 1_{R} = \underset{˙}{0})$
15	14	biimpa	$⊢ ((R \in Ring \land \underset{˙}{0} \in E \land 1_{R} \in {Base}_{R}) \land \underset{˙}{0} \cdot_{R} 1_{R} = \underset{˙}{0}) \to 1_{R} = \underset{˙}{0}$
16	7 8 11 13 15	syl31anc	$⊢ (R \in NzRing \land \underset{˙}{0} \in E) \to 1_{R} = \underset{˙}{0}$
17	5 16	mtand	$⊢ R \in NzRing \to \neg \underset{˙}{0} \in E$