Theorem srgdir

Description: Distributive law for the multiplication operation of a semiring. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Thierry Arnoux, 1-Apr-2018)

	Ref	Expression
Hypotheses	srgdi.b	$$⊢B={\mathrm{Base}}_R$$
	srgdi.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	srgdi.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	srgdir	$$⊢\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)$$

Proof

Step	Hyp	Ref	Expression
1		srgdi.b	$$⊢B={\mathrm{Base}}_R$$
2		srgdi.p	$$⊢\underset{\dot{}}{+}={+}_R$$
3		srgdi.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4	1 2 3	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)$$
5	4	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)$$