Theorem ringsubdi

Description: Ring multiplication distributes over subtraction. ( subdi analog.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 2-Jul-2014)

	Ref	Expression
Hypotheses	ringsubdi.b	$$⊢B={\mathrm{Base}}_R$$
	ringsubdi.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	ringsubdi.m	$$⊢\underset{\dot{}}{-}={-}_R$$
	ringsubdi.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	ringsubdi.x	$$⊢\phi \to X\in B$$
	ringsubdi.y	$$⊢\phi \to Y\in B$$
	ringsubdi.z	$$⊢\phi \to Z\in B$$
Assertion	ringsubdi	$$⊢\phi \to X\underset{\dot{}}{·}\left(Y\underset{\dot{}}{-}Z\right)=\left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{-}\left(X\underset{\dot{}}{·}Z\right)$$

Proof

Step	Hyp	Ref	Expression
1		ringsubdi.b	$$⊢B={\mathrm{Base}}_R$$
2		ringsubdi.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		ringsubdi.m	$$⊢\underset{\dot{}}{-}={-}_R$$
4		ringsubdi.r	$$⊢\phi \to R\in \mathrm{Ring}$$
5		ringsubdi.x	$$⊢\phi \to X\in B$$
6		ringsubdi.y	$$⊢\phi \to Y\in B$$
7		ringsubdi.z	$$⊢\phi \to Z\in B$$
8		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
9	4 8	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
10		eqid	$$⊢{inv}_g\left(R\right)={inv}_g\left(R\right)$$
11	1 10	grpinvcl	$$⊢\left(R\in \mathrm{Grp}\wedge Z\in B\right)\to {inv}_g\left(R\right)\left(Z\right)\in B$$
12	9 7 11	syl2anc	$$⊢\phi \to {inv}_g\left(R\right)\left(Z\right)\in B$$
13		eqid	$$⊢{+}_R={+}_R$$
14	1 13 2	ringdi	$$⊢\left(R\in \mathrm{Ring}\wedge \left(X\in B\wedge Y\in B\wedge {inv}_g\left(R\right)\left(Z\right)\in B\right)\right)\to X\underset{\dot{}}{·}\left(Y{+}_R{inv}_g\left(R\right)\left(Z\right)\right)=\left(X\underset{\dot{}}{·}Y\right){+}_R\left(X\underset{\dot{}}{·}{inv}_g\left(R\right)\left(Z\right)\right)$$
15	4 5 6 12 14	syl13anc	$$⊢\phi \to X\underset{\dot{}}{·}\left(Y{+}_R{inv}_g\left(R\right)\left(Z\right)\right)=\left(X\underset{\dot{}}{·}Y\right){+}_R\left(X\underset{\dot{}}{·}{inv}_g\left(R\right)\left(Z\right)\right)$$
16	1 2 10 4 5 7	ringmneg2	$$⊢\phi \to X\underset{\dot{}}{·}{inv}_g\left(R\right)\left(Z\right)={inv}_g\left(R\right)\left(X\underset{\dot{}}{·}Z\right)$$
17	16	oveq2d	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y\right){+}_R\left(X\underset{\dot{}}{·}{inv}_g\left(R\right)\left(Z\right)\right)=\left(X\underset{\dot{}}{·}Y\right){+}_R{inv}_g\left(R\right)\left(X\underset{\dot{}}{·}Z\right)$$
18	15 17	eqtrd	$$⊢\phi \to X\underset{\dot{}}{·}\left(Y{+}_R{inv}_g\left(R\right)\left(Z\right)\right)=\left(X\underset{\dot{}}{·}Y\right){+}_R{inv}_g\left(R\right)\left(X\underset{\dot{}}{·}Z\right)$$
19	1 13 10 3	grpsubval	$$⊢\left(Y\in B\wedge Z\in B\right)\to Y\underset{\dot{}}{-}Z=Y{+}_R{inv}_g\left(R\right)\left(Z\right)$$
20	6 7 19	syl2anc	$$⊢\phi \to Y\underset{\dot{}}{-}Z=Y{+}_R{inv}_g\left(R\right)\left(Z\right)$$
21	20	oveq2d	$$⊢\phi \to X\underset{\dot{}}{·}\left(Y\underset{\dot{}}{-}Z\right)=X\underset{\dot{}}{·}\left(Y{+}_R{inv}_g\left(R\right)\left(Z\right)\right)$$
22	1 2	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{·}Y\in B$$
23	4 5 6 22	syl3anc	$$⊢\phi \to X\underset{\dot{}}{·}Y\in B$$
24	1 2	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Z\in B\right)\to X\underset{\dot{}}{·}Z\in B$$
25	4 5 7 24	syl3anc	$$⊢\phi \to X\underset{\dot{}}{·}Z\in B$$
26	1 13 10 3	grpsubval	$$⊢\left(X\underset{\dot{}}{·}Y\in B\wedge X\underset{\dot{}}{·}Z\in B\right)\to \left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{-}\left(X\underset{\dot{}}{·}Z\right)=\left(X\underset{\dot{}}{·}Y\right){+}_R{inv}_g\left(R\right)\left(X\underset{\dot{}}{·}Z\right)$$
27	23 25 26	syl2anc	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{-}\left(X\underset{\dot{}}{·}Z\right)=\left(X\underset{\dot{}}{·}Y\right){+}_R{inv}_g\left(R\right)\left(X\underset{\dot{}}{·}Z\right)$$
28	18 21 27	3eqtr4d	$$⊢\phi \to X\underset{\dot{}}{·}\left(Y\underset{\dot{}}{-}Z\right)=\left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{-}\left(X\underset{\dot{}}{·}Z\right)$$