Theorem rngsubdir

Description: Ring multiplication distributes over subtraction. ( subdir analog.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 2-Jul-2014) Generalization of ringsubdir . (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	rngsubdir	$$⊢\phi \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		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 6	grpinvcld	$$⊢\phi \to {inv}_g\left(R\right)\left(Y\right)\in B$$
12		eqid	$$⊢{+}_R={+}_R$$
13	1 12 2	rngdir	$$⊢\left(R\in \mathrm{Rng}\wedge \left(X\in B\wedge {inv}_g\left(R\right)\left(Y\right)\in B\wedge Z\in B\right)\right)\to \left(X{+}_R{inv}_g\left(R\right)\left(Y\right)\right)\underset{\dot{}}{·}Z=\left(X\underset{\dot{}}{·}Z\right){+}_R\left({inv}_g\left(R\right)\left(Y\right)\underset{\dot{}}{·}Z\right)$$
14	4 5 11 7 13	syl13anc	$$⊢\phi \to \left(X{+}_R{inv}_g\left(R\right)\left(Y\right)\right)\underset{\dot{}}{·}Z=\left(X\underset{\dot{}}{·}Z\right){+}_R\left({inv}_g\left(R\right)\left(Y\right)\underset{\dot{}}{·}Z\right)$$
15	1 2 8 4 6 7	rngmneg1	$$⊢\phi \to {inv}_g\left(R\right)\left(Y\right)\underset{\dot{}}{·}Z={inv}_g\left(R\right)\left(Y\underset{\dot{}}{·}Z\right)$$
16	15	oveq2d	$$⊢\phi \to \left(X\underset{\dot{}}{·}Z\right){+}_R\left({inv}_g\left(R\right)\left(Y\right)\underset{\dot{}}{·}Z\right)=\left(X\underset{\dot{}}{·}Z\right){+}_R{inv}_g\left(R\right)\left(Y\underset{\dot{}}{·}Z\right)$$
17	14 16	eqtrd	$$⊢\phi \to \left(X{+}_R{inv}_g\left(R\right)\left(Y\right)\right)\underset{\dot{}}{·}Z=\left(X\underset{\dot{}}{·}Z\right){+}_R{inv}_g\left(R\right)\left(Y\underset{\dot{}}{·}Z\right)$$
18	1 12 8 3	grpsubval	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{-}Y=X{+}_R{inv}_g\left(R\right)\left(Y\right)$$
19	5 6 18	syl2anc	$$⊢\phi \to X\underset{\dot{}}{-}Y=X{+}_R{inv}_g\left(R\right)\left(Y\right)$$
20	19	oveq1d	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{·}Z=\left(X{+}_R{inv}_g\left(R\right)\left(Y\right)\right)\underset{\dot{}}{·}Z$$
21	1 2	rngcl	$$⊢\left(R\in \mathrm{Rng}\wedge X\in B\wedge Z\in B\right)\to X\underset{\dot{}}{·}Z\in B$$
22	4 5 7 21	syl3anc	$$⊢\phi \to X\underset{\dot{}}{·}Z\in B$$
23	1 2	rngcl	$$⊢\left(R\in \mathrm{Rng}\wedge Y\in B\wedge Z\in B\right)\to Y\underset{\dot{}}{·}Z\in B$$
24	4 6 7 23	syl3anc	$$⊢\phi \to Y\underset{\dot{}}{·}Z\in B$$
25	1 12 8 3	grpsubval	$$⊢\left(X\underset{\dot{}}{·}Z\in B\wedge Y\underset{\dot{}}{·}Z\in B\right)\to \left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{-}\left(Y\underset{\dot{}}{·}Z\right)=\left(X\underset{\dot{}}{·}Z\right){+}_R{inv}_g\left(R\right)\left(Y\underset{\dot{}}{·}Z\right)$$
26	22 24 25	syl2anc	$$⊢\phi \to \left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{-}\left(Y\underset{\dot{}}{·}Z\right)=\left(X\underset{\dot{}}{·}Z\right){+}_R{inv}_g\left(R\right)\left(Y\underset{\dot{}}{·}Z\right)$$
27	17 20 26	3eqtr4d	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y\right)\underset{\dot{}}{·}Z=\left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{-}\left(Y\underset{\dot{}}{·}Z\right)$$