Theorem rngsubdi

Description: Ring multiplication distributes over subtraction. ( subdi analog.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 2-Jul-2014) ringsubdi generalized for non-unital rings. (Revised by AV, 23-Feb-2025)

	Ref	Expression
Hypotheses	rngsubdi.b	$$⊢B={\mathrm{Base}}_R$$
	rngsubdi.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rngsubdi.m	$$⊢\underset{\dot{}}{-}={-}_R$$
	rngsubdi.r	$$⊢\phi \to R\in \mathrm{Rng}$$
	rngsubdi.x	$$⊢\phi \to X\in B$$
	rngsubdi.y	$$⊢\phi \to Y\in B$$
	rngsubdi.z	$$⊢\phi \to Z\in B$$
Assertion	rngsubdi	$$⊢\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		rngsubdi.b	$$⊢B={\mathrm{Base}}_R$$
2		rngsubdi.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		rngsubdi.m	$$⊢\underset{\dot{}}{-}={-}_R$$
4		rngsubdi.r	$$⊢\phi \to R\in \mathrm{Rng}$$
5		rngsubdi.x	$$⊢\phi \to X\in B$$
6		rngsubdi.y	$$⊢\phi \to Y\in B$$
7		rngsubdi.z	$$⊢\phi \to Z\in B$$
8		eqid	$$⊢{inv}_g\left(R\right)={inv}_g\left(R\right)$$
9		rnggrp	$$⊢R\in \mathrm{Rng}\to R\in \mathrm{Grp}$$
10	4 9	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
11	1 8 10 7	grpinvcld	$$⊢\phi \to {inv}_g\left(R\right)\left(Z\right)\in B$$
12		eqid	$$⊢{+}_R={+}_R$$
13	1 12 2	rngdi	$$⊢\left(R\in \mathrm{Rng}\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)$$
14	4 5 6 11 13	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)$$
15	1 2 8 4 5 7	rngmneg2	$$⊢\phi \to X\underset{\dot{}}{·}{inv}_g\left(R\right)\left(Z\right)={inv}_g\left(R\right)\left(X\underset{\dot{}}{·}Z\right)$$
16	15	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)$$
17	14 16	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)$$
18	1 12 8 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)$$
19	6 7 18	syl2anc	$$⊢\phi \to Y\underset{\dot{}}{-}Z=Y{+}_R{inv}_g\left(R\right)\left(Z\right)$$
20	19	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)$$
21	1 2	rngcl	$$⊢\left(R\in \mathrm{Rng}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{·}Y\in B$$
22	4 5 6 21	syl3anc	$$⊢\phi \to X\underset{\dot{}}{·}Y\in B$$
23	1 2	rngcl	$$⊢\left(R\in \mathrm{Rng}\wedge X\in B\wedge Z\in B\right)\to X\underset{\dot{}}{·}Z\in B$$
24	4 5 7 23	syl3anc	$$⊢\phi \to X\underset{\dot{}}{·}Z\in B$$
25	1 12 8 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)$$
26	22 24 25	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)$$
27	17 20 26	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)$$