srgcom4lem

Description: Lemma for srgcom4 . This (formerly) part of the proof for ringcom is applicable for semirings (without using the commutativity of the addition given per definition of a semiring). (Contributed by Gérard Lang, 4-Dec-2014) (Revised by AV, 1-Feb-2025) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	srgcom4.b	$⊢ B = {Base}_{R}$
	srgcom4.p	$⊢ \underset{˙}{+} = +_{R}$
Assertion	srgcom4lem	$⊢ (R \in SRing \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		srgcom4.b	$⊢ B = {Base}_{R}$
2		srgcom4.p	$⊢ \underset{˙}{+} = +_{R}$
3		eqid	$⊢ \cdot_{R} = \cdot_{R}$
4	1 2 3	srgdir	$⊢ (R \in SRing \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 SRing \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 SRing \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	srgidcl	$⊢ R \in SRing \to 1_{R} \in B$
9	8	3ad2ant1	$⊢ (R \in SRing \land X \in B \land Y \in B) \to 1_{R} \in B$
10	1 3 7	srglidm	$⊢ (R \in SRing \land x \in B) \to 1_{R} \cdot_{R} x = x$
11	10	ralrimiva	$⊢ R \in SRing \to \forall x \in B 1_{R} \cdot_{R} x = x$
12	11	3ad2ant1	$⊢ (R \in SRing \land X \in B \land Y \in B) \to \forall x \in B 1_{R} \cdot_{R} x = x$
13		simp2	$⊢ (R \in SRing \land X \in B \land Y \in B) \to X \in B$
14	1 2	srgacl	$⊢ (R \in SRing \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
15	14	3expb	$⊢ (R \in SRing \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
16	15	ralrimivva	$⊢ R \in SRing \to \forall x \in B \forall y \in B x \underset{˙}{+} y \in B$
17	16	3ad2ant1	$⊢ (R \in SRing \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	srgdi	$⊢ (R \in SRing \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 SRing \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 SRing \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 SRing \land X \in B \land Y \in B) \to Y \in B$
22	6 9 12 13 17 20 21	rglcom4d	$⊢ (R \in SRing \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 srgcom4lem

Proof