rnglz

Description: The zero of a nonunital ring is a left-absorbing element. (Contributed by AV, 17-Apr-2020)

	Ref	Expression
Hypotheses	rngcl.b	$⊢ B = {Base}_{R}$
	rngcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rnglz.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	rnglz	$⊢ (R \in Rng \land X \in B) \to \underset{˙}{0} \underset{˙}{\cdot} X = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		rngcl.b	$⊢ B = {Base}_{R}$
2		rngcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		rnglz.z	$⊢ \underset{˙}{0} = 0_{R}$
4		rngabl	$⊢ R \in Rng \to R \in Abel$
5		ablgrp	$⊢ R \in Abel \to R \in Grp$
6	4 5	syl	$⊢ R \in Rng \to R \in Grp$
7	1 3	grpidcl	$⊢ R \in Grp \to \underset{˙}{0} \in B$
8		eqid	$⊢ +_{R} = +_{R}$
9	1 8 3	grplid	$⊢ (R \in Grp \land \underset{˙}{0} \in B) \to \underset{˙}{0} +_{R} \underset{˙}{0} = \underset{˙}{0}$
10	6 7 9	syl2anc2	$⊢ R \in Rng \to \underset{˙}{0} +_{R} \underset{˙}{0} = \underset{˙}{0}$
11	10	adantr	$⊢ (R \in Rng \land X \in B) \to \underset{˙}{0} +_{R} \underset{˙}{0} = \underset{˙}{0}$
12	11	oveq1d	$⊢ (R \in Rng \land X \in B) \to (\underset{˙}{0} +_{R} \underset{˙}{0}) \underset{˙}{\cdot} X = \underset{˙}{0} \underset{˙}{\cdot} X$
13		simpl	$⊢ (R \in Rng \land X \in B) \to R \in Rng$
14	6 7	syl	$⊢ R \in Rng \to \underset{˙}{0} \in B$
15	14 14	jca	$⊢ R \in Rng \to (\underset{˙}{0} \in B \land \underset{˙}{0} \in B)$
16	15	anim1i	$⊢ (R \in Rng \land X \in B) \to ((\underset{˙}{0} \in B \land \underset{˙}{0} \in B) \land X \in B)$
17		df-3an	$⊢ (\underset{˙}{0} \in B \land \underset{˙}{0} \in B \land X \in B) \leftrightarrow ((\underset{˙}{0} \in B \land \underset{˙}{0} \in B) \land X \in B)$
18	16 17	sylibr	$⊢ (R \in Rng \land X \in B) \to (\underset{˙}{0} \in B \land \underset{˙}{0} \in B \land X \in B)$
19	1 8 2	rngdir	$⊢ (R \in Rng \land (\underset{˙}{0} \in B \land \underset{˙}{0} \in B \land X \in B)) \to (\underset{˙}{0} +_{R} \underset{˙}{0}) \underset{˙}{\cdot} X = (\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} (\underset{˙}{0} \underset{˙}{\cdot} X)$
20	13 18 19	syl2anc	$⊢ (R \in Rng \land X \in B) \to (\underset{˙}{0} +_{R} \underset{˙}{0}) \underset{˙}{\cdot} X = (\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} (\underset{˙}{0} \underset{˙}{\cdot} X)$
21	6	adantr	$⊢ (R \in Rng \land X \in B) \to R \in Grp$
22	14	adantr	$⊢ (R \in Rng \land X \in B) \to \underset{˙}{0} \in B$
23		simpr	$⊢ (R \in Rng \land X \in B) \to X \in B$
24	1 2	rngcl	$⊢ (R \in Rng \land \underset{˙}{0} \in B \land X \in B) \to \underset{˙}{0} \underset{˙}{\cdot} X \in B$
25	13 22 23 24	syl3anc	$⊢ (R \in Rng \land X \in B) \to \underset{˙}{0} \underset{˙}{\cdot} X \in B$
26	1 8 3	grprid	$⊢ (R \in Grp \land \underset{˙}{0} \underset{˙}{\cdot} X \in B) \to (\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} \underset{˙}{0} = \underset{˙}{0} \underset{˙}{\cdot} X$
27	26	eqcomd	$⊢ (R \in Grp \land \underset{˙}{0} \underset{˙}{\cdot} X \in B) \to \underset{˙}{0} \underset{˙}{\cdot} X = (\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} \underset{˙}{0}$
28	21 25 27	syl2anc	$⊢ (R \in Rng \land X \in B) \to \underset{˙}{0} \underset{˙}{\cdot} X = (\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} \underset{˙}{0}$
29	12 20 28	3eqtr3d	$⊢ (R \in Rng \land X \in B) \to (\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} (\underset{˙}{0} \underset{˙}{\cdot} X) = (\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} \underset{˙}{0}$
30	1 8	grplcan	$⊢ (R \in Grp \land (\underset{˙}{0} \underset{˙}{\cdot} X \in B \land \underset{˙}{0} \in B \land \underset{˙}{0} \underset{˙}{\cdot} X \in B)) \to ((\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} (\underset{˙}{0} \underset{˙}{\cdot} X) = (\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} \underset{˙}{0} \leftrightarrow \underset{˙}{0} \underset{˙}{\cdot} X = \underset{˙}{0})$
31	21 25 22 25 30	syl13anc	$⊢ (R \in Rng \land X \in B) \to ((\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} (\underset{˙}{0} \underset{˙}{\cdot} X) = (\underset{˙}{0} \underset{˙}{\cdot} X) +_{R} \underset{˙}{0} \leftrightarrow \underset{˙}{0} \underset{˙}{\cdot} X = \underset{˙}{0})$
32	29 31	mpbid	$⊢ (R \in Rng \land X \in B) \to \underset{˙}{0} \underset{˙}{\cdot} X = \underset{˙}{0}$

Metamath Proof Explorer

Theorem rnglz

Proof