Theorem rngdir

Description: Distributive law for the multiplication operation of a non-unital ring (right-distributivity). (Contributed by AV, 17-Apr-2020)

	Ref	Expression
Hypotheses	rngdi.b	$$⊢B={\mathrm{Base}}_R$$
	rngdi.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	rngdi.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	rngdir	$$⊢\left(R\in \mathrm{Rng}\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		rngdi.b	$$⊢B={\mathrm{Base}}_R$$
2		rngdi.p	$$⊢\underset{\dot{}}{+}={+}_R$$
3		rngdi.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
5	1 4 2 3	isrng	$$⊢R\in \mathrm{Rng}\leftrightarrow \left(R\in \mathrm{Abel}\wedge {\mathrm{mulGrp}}_R\in \mathrm{Smgrp}\wedge \forall a\in B\forall b\in B\forall c\in B\left(a\underset{\dot{}}{·}\left(b\underset{\dot{}}{+}c\right)=\left(a\underset{\dot{}}{·}b\right)\underset{\dot{}}{+}\left(a\underset{\dot{}}{·}c\right)\wedge \left(a\underset{\dot{}}{+}b\right)\underset{\dot{}}{·}c=\left(a\underset{\dot{}}{·}c\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}c\right)\right)\right)$$
6		oveq1	$$⊢a=X\to a\underset{\dot{}}{·}\left(b\underset{\dot{}}{+}c\right)=X\underset{\dot{}}{·}\left(b\underset{\dot{}}{+}c\right)$$
7		oveq1	$$⊢a=X\to a\underset{\dot{}}{·}b=X\underset{\dot{}}{·}b$$
8		oveq1	$$⊢a=X\to a\underset{\dot{}}{·}c=X\underset{\dot{}}{·}c$$
9	7 8	oveq12d	$$⊢a=X\to \left(a\underset{\dot{}}{·}b\right)\underset{\dot{}}{+}\left(a\underset{\dot{}}{·}c\right)=\left(X\underset{\dot{}}{·}b\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{·}c\right)$$
10	6 9	eqeq12d	$$⊢a=X\to \left(a\underset{\dot{}}{·}\left(b\underset{\dot{}}{+}c\right)=\left(a\underset{\dot{}}{·}b\right)\underset{\dot{}}{+}\left(a\underset{\dot{}}{·}c\right)\leftrightarrow X\underset{\dot{}}{·}\left(b\underset{\dot{}}{+}c\right)=\left(X\underset{\dot{}}{·}b\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{·}c\right)\right)$$
11		oveq1	$$⊢a=X\to a\underset{\dot{}}{+}b=X\underset{\dot{}}{+}b$$
12	11	oveq1d	$$⊢a=X\to \left(a\underset{\dot{}}{+}b\right)\underset{\dot{}}{·}c=\left(X\underset{\dot{}}{+}b\right)\underset{\dot{}}{·}c$$
13	8	oveq1d	$$⊢a=X\to \left(a\underset{\dot{}}{·}c\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}c\right)=\left(X\underset{\dot{}}{·}c\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}c\right)$$
14	12 13	eqeq12d	$$⊢a=X\to \left(\left(a\underset{\dot{}}{+}b\right)\underset{\dot{}}{·}c=\left(a\underset{\dot{}}{·}c\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}c\right)\leftrightarrow \left(X\underset{\dot{}}{+}b\right)\underset{\dot{}}{·}c=\left(X\underset{\dot{}}{·}c\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}c\right)\right)$$
15	10 14	anbi12d	$$⊢a=X\to \left(\left(a\underset{\dot{}}{·}\left(b\underset{\dot{}}{+}c\right)=\left(a\underset{\dot{}}{·}b\right)\underset{\dot{}}{+}\left(a\underset{\dot{}}{·}c\right)\wedge \left(a\underset{\dot{}}{+}b\right)\underset{\dot{}}{·}c=\left(a\underset{\dot{}}{·}c\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}c\right)\right)\leftrightarrow \left(X\underset{\dot{}}{·}\left(b\underset{\dot{}}{+}c\right)=\left(X\underset{\dot{}}{·}b\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{·}c\right)\wedge \left(X\underset{\dot{}}{+}b\right)\underset{\dot{}}{·}c=\left(X\underset{\dot{}}{·}c\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}c\right)\right)\right)$$
16		oveq1	$$⊢b=Y\to b\underset{\dot{}}{+}c=Y\underset{\dot{}}{+}c$$
17	16	oveq2d	$$⊢b=Y\to X\underset{\dot{}}{·}\left(b\underset{\dot{}}{+}c\right)=X\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}c\right)$$
18		oveq2	$$⊢b=Y\to X\underset{\dot{}}{·}b=X\underset{\dot{}}{·}Y$$
19	18	oveq1d	$$⊢b=Y\to \left(X\underset{\dot{}}{·}b\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{·}c\right)=\left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{·}c\right)$$
20	17 19	eqeq12d	$$⊢b=Y\to \left(X\underset{\dot{}}{·}\left(b\underset{\dot{}}{+}c\right)=\left(X\underset{\dot{}}{·}b\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{·}c\right)\leftrightarrow X\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}c\right)=\left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{·}c\right)\right)$$
21		oveq2	$$⊢b=Y\to X\underset{\dot{}}{+}b=X\underset{\dot{}}{+}Y$$
22	21	oveq1d	$$⊢b=Y\to \left(X\underset{\dot{}}{+}b\right)\underset{\dot{}}{·}c=\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}c$$
23		oveq1	$$⊢b=Y\to b\underset{\dot{}}{·}c=Y\underset{\dot{}}{·}c$$
24	23	oveq2d	$$⊢b=Y\to \left(X\underset{\dot{}}{·}c\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}c\right)=\left(X\underset{\dot{}}{·}c\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{·}c\right)$$
25	22 24	eqeq12d	$$⊢b=Y\to \left(\left(X\underset{\dot{}}{+}b\right)\underset{\dot{}}{·}c=\left(X\underset{\dot{}}{·}c\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}c\right)\leftrightarrow \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}c=\left(X\underset{\dot{}}{·}c\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{·}c\right)\right)$$
26	20 25	anbi12d	$$⊢b=Y\to \left(\left(X\underset{\dot{}}{·}\left(b\underset{\dot{}}{+}c\right)=\left(X\underset{\dot{}}{·}b\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{·}c\right)\wedge \left(X\underset{\dot{}}{+}b\right)\underset{\dot{}}{·}c=\left(X\underset{\dot{}}{·}c\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}c\right)\right)\leftrightarrow \left(X\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}c\right)=\left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{·}c\right)\wedge \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}c=\left(X\underset{\dot{}}{·}c\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{·}c\right)\right)\right)$$
27		oveq2	$$⊢c=Z\to Y\underset{\dot{}}{+}c=Y\underset{\dot{}}{+}Z$$
28	27	oveq2d	$$⊢c=Z\to X\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}c\right)=X\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}Z\right)$$
29		oveq2	$$⊢c=Z\to X\underset{\dot{}}{·}c=X\underset{\dot{}}{·}Z$$
30	29	oveq2d	$$⊢c=Z\to \left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{·}c\right)=\left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{·}Z\right)$$
31	28 30	eqeq12d	$$⊢c=Z\to \left(X\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}c\right)=\left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{·}c\right)\leftrightarrow X\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}Z\right)=\left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{·}Z\right)\right)$$
32		oveq2	$$⊢c=Z\to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}c=\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}Z$$
33		oveq2	$$⊢c=Z\to Y\underset{\dot{}}{·}c=Y\underset{\dot{}}{·}Z$$
34	29 33	oveq12d	$$⊢c=Z\to \left(X\underset{\dot{}}{·}c\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{·}c\right)=\left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{·}Z\right)$$
35	32 34	eqeq12d	$$⊢c=Z\to \left(\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}c=\left(X\underset{\dot{}}{·}c\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{·}c\right)\leftrightarrow \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}Z=\left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{·}Z\right)\right)$$
36	31 35	anbi12d	$$⊢c=Z\to \left(\left(X\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}c\right)=\left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(X\underset{\dot{}}{·}c\right)\wedge \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}c=\left(X\underset{\dot{}}{·}c\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{·}c\right)\right)\leftrightarrow \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)$$
37	15 26 36	rspc3v	$$⊢\left(X\in B\wedge Y\in B\wedge Z\in B\right)\to \left(\forall a\in B\forall b\in B\forall c\in B\left(a\underset{\dot{}}{·}\left(b\underset{\dot{}}{+}c\right)=\left(a\underset{\dot{}}{·}b\right)\underset{\dot{}}{+}\left(a\underset{\dot{}}{·}c\right)\wedge \left(a\underset{\dot{}}{+}b\right)\underset{\dot{}}{·}c=\left(a\underset{\dot{}}{·}c\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}c\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)\right)$$
38		simpr	$$⊢\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(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}Z=\left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{·}Z\right)$$
39	37 38	syl6com	$$⊢\forall a\in B\forall b\in B\forall c\in B\left(a\underset{\dot{}}{·}\left(b\underset{\dot{}}{+}c\right)=\left(a\underset{\dot{}}{·}b\right)\underset{\dot{}}{+}\left(a\underset{\dot{}}{·}c\right)\wedge \left(a\underset{\dot{}}{+}b\right)\underset{\dot{}}{·}c=\left(a\underset{\dot{}}{·}c\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}c\right)\right)\to \left(\left(X\in B\wedge Y\in B\wedge Z\in B\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)\right)$$
40	39	3ad2ant3	$$⊢\left(R\in \mathrm{Abel}\wedge {\mathrm{mulGrp}}_R\in \mathrm{Smgrp}\wedge \forall a\in B\forall b\in B\forall c\in B\left(a\underset{\dot{}}{·}\left(b\underset{\dot{}}{+}c\right)=\left(a\underset{\dot{}}{·}b\right)\underset{\dot{}}{+}\left(a\underset{\dot{}}{·}c\right)\wedge \left(a\underset{\dot{}}{+}b\right)\underset{\dot{}}{·}c=\left(a\underset{\dot{}}{·}c\right)\underset{\dot{}}{+}\left(b\underset{\dot{}}{·}c\right)\right)\right)\to \left(\left(X\in B\wedge Y\in B\wedge Z\in B\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)\right)$$
41	5 40	sylbi	$$⊢R\in \mathrm{Rng}\to \left(\left(X\in B\wedge Y\in B\wedge Z\in B\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)\right)$$
42	41	imp	$$⊢\left(R\in \mathrm{Rng}\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)$$