srgi

Description: Properties of a semiring. (Contributed by NM, 26-Aug-2011) (Revised by Mario Carneiro, 6-Jan-2015) (Revised by Thierry Arnoux, 1-Apr-2018)

	Ref	Expression
Hypotheses	srgi.b	$⊢ B = {Base}_{R}$
	srgi.p	$⊢ \underset{˙}{+} = +_{R}$
	srgi.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	srgi	$⊢ (R \in SRing \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\cdot} (Y \underset{˙}{+} Z) = (X \underset{˙}{\cdot} Y) \underset{˙}{+} (X \underset{˙}{\cdot} Z) \land (X \underset{˙}{+} Y) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) \underset{˙}{+} (Y \underset{˙}{\cdot} Z))$

Proof

Step	Hyp	Ref	Expression
1		srgi.b	$⊢ B = {Base}_{R}$
2		srgi.p	$⊢ \underset{˙}{+} = +_{R}$
3		srgi.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
5		eqid	$⊢ 0_{R} = 0_{R}$
6	1 4 2 3 5	issrg	$⊢ R \in SRing \leftrightarrow (R \in CMnd \land {mulGrp}_{R} \in Mnd \land \forall x \in B (\forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land (0_{R} \underset{˙}{\cdot} x = 0_{R} \land x \underset{˙}{\cdot} 0_{R} = 0_{R})))$
7	6	simp3bi	$⊢ R \in SRing \to \forall x \in B (\forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land (0_{R} \underset{˙}{\cdot} x = 0_{R} \land x \underset{˙}{\cdot} 0_{R} = 0_{R}))$
8	7	r19.21bi	$⊢ (R \in SRing \land x \in B) \to (\forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \land (0_{R} \underset{˙}{\cdot} x = 0_{R} \land x \underset{˙}{\cdot} 0_{R} = 0_{R}))$
9	8	simpld	$⊢ (R \in SRing \land x \in B) \to \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))$
10	9	3ad2antr1	$⊢ (R \in SRing \land (x \in B \land y \in B \land z \in B)) \to \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))$
11		simpr2	$⊢ (R \in SRing \land (x \in B \land y \in B \land z \in B)) \to y \in B$
12		rsp	$⊢ \forall y \in B \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \to (y \in B \to \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
13	10 11 12	sylc	$⊢ (R \in SRing \land (x \in B \land y \in B \land z \in B)) \to \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))$
14		simpr3	$⊢ (R \in SRing \land (x \in B \land y \in B \land z \in B)) \to z \in B$
15		rsp	$⊢ \forall z \in B (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)) \to (z \in B \to (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)))$
16	13 14 15	sylc	$⊢ (R \in SRing \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) \land (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z))$
17	16	simpld	$⊢ (R \in SRing \land (x \in B \land y \in B \land z \in B)) \to x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z)$
18	17	caovdig	$⊢ (R \in SRing \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\cdot} (Y \underset{˙}{+} Z) = (X \underset{˙}{\cdot} Y) \underset{˙}{+} (X \underset{˙}{\cdot} Z)$
19	16	simprd	$⊢ (R \in SRing \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
20	19	caovdirg	$⊢ (R \in SRing \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{+} Y) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) \underset{˙}{+} (Y \underset{˙}{\cdot} Z)$
21	18 20	jca	$⊢ (R \in SRing \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\cdot} (Y \underset{˙}{+} Z) = (X \underset{˙}{\cdot} Y) \underset{˙}{+} (X \underset{˙}{\cdot} Z) \land (X \underset{˙}{+} Y) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) \underset{˙}{+} (Y \underset{˙}{\cdot} Z))$

Metamath Proof Explorer

Theorem srgi

Proof