rngrz

Description: The zero of a non-unital ring is a right-absorbing element. (Contributed by AV, 16-Feb-2025)

	Ref	Expression
Hypotheses	rngcl.b	$⊢ B = {Base}_{R}$
	rngcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rnglz.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	rngrz	$⊢ (R \in Rng \land X \in B) \to X \underset{˙}{\cdot} \underset{˙}{0} = \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		rnggrp	$⊢ R \in Rng \to R \in Grp$
5	1 3	grpidcl	$⊢ R \in Grp \to \underset{˙}{0} \in B$
6		eqid	$⊢ +_{R} = +_{R}$
7	1 6 3	grplid	$⊢ (R \in Grp \land \underset{˙}{0} \in B) \to \underset{˙}{0} +_{R} \underset{˙}{0} = \underset{˙}{0}$
8	4 5 7	syl2anc2	$⊢ R \in Rng \to \underset{˙}{0} +_{R} \underset{˙}{0} = \underset{˙}{0}$
9	8	adantr	$⊢ (R \in Rng \land X \in B) \to \underset{˙}{0} +_{R} \underset{˙}{0} = \underset{˙}{0}$
10	9	oveq2d	$⊢ (R \in Rng \land X \in B) \to X \underset{˙}{\cdot} (\underset{˙}{0} +_{R} \underset{˙}{0}) = X \underset{˙}{\cdot} \underset{˙}{0}$
11		simpr	$⊢ (R \in Rng \land X \in B) \to X \in B$
12	1 3	rng0cl	$⊢ R \in Rng \to \underset{˙}{0} \in B$
13	12	adantr	$⊢ (R \in Rng \land X \in B) \to \underset{˙}{0} \in B$
14	11 13 13	3jca	$⊢ (R \in Rng \land X \in B) \to (X \in B \land \underset{˙}{0} \in B \land \underset{˙}{0} \in B)$
15	1 6 2	rngdi	$⊢ (R \in Rng \land (X \in B \land \underset{˙}{0} \in B \land \underset{˙}{0} \in B)) \to X \underset{˙}{\cdot} (\underset{˙}{0} +_{R} \underset{˙}{0}) = (X \underset{˙}{\cdot} \underset{˙}{0}) +_{R} (X \underset{˙}{\cdot} \underset{˙}{0})$
16	14 15	syldan	$⊢ (R \in Rng \land X \in B) \to X \underset{˙}{\cdot} (\underset{˙}{0} +_{R} \underset{˙}{0}) = (X \underset{˙}{\cdot} \underset{˙}{0}) +_{R} (X \underset{˙}{\cdot} \underset{˙}{0})$
17	4	adantr	$⊢ (R \in Rng \land X \in B) \to R \in Grp$
18	1 2	rngcl	$⊢ (R \in Rng \land X \in B \land \underset{˙}{0} \in B) \to X \underset{˙}{\cdot} \underset{˙}{0} \in B$
19	13 18	mpd3an3	$⊢ (R \in Rng \land X \in B) \to X \underset{˙}{\cdot} \underset{˙}{0} \in B$
20	1 6 3	grplid	$⊢ (R \in Grp \land X \underset{˙}{\cdot} \underset{˙}{0} \in B) \to \underset{˙}{0} +_{R} (X \underset{˙}{\cdot} \underset{˙}{0}) = X \underset{˙}{\cdot} \underset{˙}{0}$
21	20	eqcomd	$⊢ (R \in Grp \land X \underset{˙}{\cdot} \underset{˙}{0} \in B) \to X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0} +_{R} (X \underset{˙}{\cdot} \underset{˙}{0})$
22	17 19 21	syl2anc	$⊢ (R \in Rng \land X \in B) \to X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0} +_{R} (X \underset{˙}{\cdot} \underset{˙}{0})$
23	10 16 22	3eqtr3d	$⊢ (R \in Rng \land X \in B) \to (X \underset{˙}{\cdot} \underset{˙}{0}) +_{R} (X \underset{˙}{\cdot} \underset{˙}{0}) = \underset{˙}{0} +_{R} (X \underset{˙}{\cdot} \underset{˙}{0})$
24	1 6	grprcan	$⊢ (R \in Grp \land (X \underset{˙}{\cdot} \underset{˙}{0} \in B \land \underset{˙}{0} \in B \land X \underset{˙}{\cdot} \underset{˙}{0} \in B)) \to ((X \underset{˙}{\cdot} \underset{˙}{0}) +_{R} (X \underset{˙}{\cdot} \underset{˙}{0}) = \underset{˙}{0} +_{R} (X \underset{˙}{\cdot} \underset{˙}{0}) \leftrightarrow X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0})$
25	17 19 13 19 24	syl13anc	$⊢ (R \in Rng \land X \in B) \to ((X \underset{˙}{\cdot} \underset{˙}{0}) +_{R} (X \underset{˙}{\cdot} \underset{˙}{0}) = \underset{˙}{0} +_{R} (X \underset{˙}{\cdot} \underset{˙}{0}) \leftrightarrow X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0})$
26	23 25	mpbid	$⊢ (R \in Rng \land X \in B) \to X \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$

Metamath Proof Explorer

Theorem rngrz

Proof