Theorem srgdilem

Description: Lemma for srgdi and srgdir . (Contributed by NM, 26-Aug-2011) (Revised by Mario Carneiro, 6-Jan-2015) (Revised by Thierry Arnoux, 1-Apr-2018)

	Ref	Expression
Hypotheses	srgdilem.b	$$⊢B={\mathrm{Base}}_R$$
	srgdilem.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	srgdilem.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	srgdilem	$$⊢\left(R\in \mathrm{SRing}\wedge \left(X\in B\wedge Y\in B\wedge Z\in B\right)\right)\to \left(X\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}Z\right)=\left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{·}Z\right)\wedge \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}Z=\left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{·}Z\right)\right)$$

Proof

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