Theorem ringdir

Description: Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007)

	Ref	Expression
Hypotheses	ringdi.b	$$⊢B={\mathrm{Base}}_R$$
	ringdi.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	ringdi.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	ringdir	$$⊢\left(R\in \mathrm{Ring}\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		ringdi.b	$$⊢B={\mathrm{Base}}_R$$
2		ringdi.p	$$⊢\underset{\dot{}}{+}={+}_R$$
3		ringdi.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4	1 2 3	ringdilem	$$⊢\left(R\in \mathrm{Ring}\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{Ring}\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)$$