ringcomlem

Description: Lemma for ringcom . This (formerly) part of the proof for ringcom is also applicable for semirings (without using the commutativity of the addition given per definition of a semiring), see srgcom4lem . (Contributed by Gérard Lang, 4-Dec-2014) Variant of rglcom4d for rings. (Revised by AV, 5-Feb-2025)

	Ref	Expression
Hypotheses	ringacl.b	$⊢ B = {Base}_{R}$
	ringacl.p	$⊢ \underset{˙}{+} = +_{R}$
Assertion	ringcomlem	$⊢ (R \in Ring \land X \in B \land Y \in B) \to (X \underset{˙}{+} X) \underset{˙}{+} (Y \underset{˙}{+} Y) = (X \underset{˙}{+} Y) \underset{˙}{+} (X \underset{˙}{+} Y)$

Proof

Step	Hyp	Ref	Expression
1		ringacl.b	$⊢ B = {Base}_{R}$
2		ringacl.p	$⊢ \underset{˙}{+} = +_{R}$
3		eqid	$⊢ \cdot_{R} = \cdot_{R}$
4	1 2 3	ringdir	$⊢ (R \in Ring \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \cdot_{R} z = (x \cdot_{R} z) \underset{˙}{+} (y \cdot_{R} z)$
5	4	ralrimivvva	$⊢ R \in Ring \to \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{+} y) \cdot_{R} z = (x \cdot_{R} z) \underset{˙}{+} (y \cdot_{R} z)$
6	5	3ad2ant1	$⊢ (R \in Ring \land X \in B \land Y \in B) \to \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{+} y) \cdot_{R} z = (x \cdot_{R} z) \underset{˙}{+} (y \cdot_{R} z)$
7		eqid	$⊢ 1_{R} = 1_{R}$
8	1 7	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
9	8	3ad2ant1	$⊢ (R \in Ring \land X \in B \land Y \in B) \to 1_{R} \in B$
10	1 3 7	ringlidm	$⊢ (R \in Ring \land x \in B) \to 1_{R} \cdot_{R} x = x$
11	10	ralrimiva	$⊢ R \in Ring \to \forall x \in B 1_{R} \cdot_{R} x = x$
12	11	3ad2ant1	$⊢ (R \in Ring \land X \in B \land Y \in B) \to \forall x \in B 1_{R} \cdot_{R} x = x$
13		simp2	$⊢ (R \in Ring \land X \in B \land Y \in B) \to X \in B$
14	1 2	ringacl	$⊢ (R \in Ring \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
15	14	3expb	$⊢ (R \in Ring \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
16	15	ralrimivva	$⊢ R \in Ring \to \forall x \in B \forall y \in B x \underset{˙}{+} y \in B$
17	16	3ad2ant1	$⊢ (R \in Ring \land X \in B \land Y \in B) \to \forall x \in B \forall y \in B x \underset{˙}{+} y \in B$
18	1 2 3	ringdi	$⊢ (R \in Ring \land (x \in B \land y \in B \land z \in B)) \to x \cdot_{R} (y \underset{˙}{+} z) = (x \cdot_{R} y) \underset{˙}{+} (x \cdot_{R} z)$
19	18	ralrimivvva	$⊢ R \in Ring \to \forall x \in B \forall y \in B \forall z \in B x \cdot_{R} (y \underset{˙}{+} z) = (x \cdot_{R} y) \underset{˙}{+} (x \cdot_{R} z)$
20	19	3ad2ant1	$⊢ (R \in Ring \land X \in B \land Y \in B) \to \forall x \in B \forall y \in B \forall z \in B x \cdot_{R} (y \underset{˙}{+} z) = (x \cdot_{R} y) \underset{˙}{+} (x \cdot_{R} z)$
21		simp3	$⊢ (R \in Ring \land X \in B \land Y \in B) \to Y \in B$
22	6 9 12 13 17 20 21	rglcom4d	$⊢ (R \in Ring \land X \in B \land Y \in B) \to (X \underset{˙}{+} X) \underset{˙}{+} (Y \underset{˙}{+} Y) = (X \underset{˙}{+} Y) \underset{˙}{+} (X \underset{˙}{+} Y)$

Metamath Proof Explorer

Theorem ringcomlem

Proof