Theorem ringdi22

Description: Expand the product of two sums in a ring. (Contributed by Thierry Arnoux, 3-Jun-2025)

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

Proof

Step	Hyp	Ref	Expression
1		ringdid.b	$$⊢B={\mathrm{Base}}_R$$
2		ringdid.p	$$⊢\underset{\dot{}}{+}={+}_R$$
3		ringdid.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		ringdid.r	$$⊢\phi \to R\in \mathrm{Ring}$$
5		ringdid.x	$$⊢\phi \to X\in B$$
6		ringdid.y	$$⊢\phi \to Y\in B$$
7		ringdid.z	$$⊢\phi \to Z\in B$$
8		ringdi22.t	$$⊢\phi \to T\in B$$
9	4	ringgrpd	$$⊢\phi \to R\in \mathrm{Grp}$$
10	1 2 9 5 6	grpcld	$$⊢\phi \to X\underset{\dot{}}{+}Y\in B$$
11	1 2 3 4 10 7 8	ringdid	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{+}T\right)=\left(\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}Z\right)\underset{\dot{}}{+}\left(\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}T\right)$$
12	1 2 3 4 5 6 7	ringdird	$$⊢\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)$$
13	1 2 3 4 5 6 8	ringdird	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}T=\left(X\underset{\dot{}}{·}T\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{·}T\right)$$
14	12 13	oveq12d	$$⊢\phi \to \left(\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}Z\right)\underset{\dot{}}{+}\left(\left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}T\right)=\left(\left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{·}Z\right)\right)\underset{\dot{}}{+}\left(\left(X\underset{\dot{}}{·}T\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{·}T\right)\right)$$
15	11 14	eqtrd	$$⊢\phi \to \left(X\underset{\dot{}}{+}Y\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{+}T\right)=\left(\left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{·}Z\right)\right)\underset{\dot{}}{+}\left(\left(X\underset{\dot{}}{·}T\right)\underset{\dot{}}{+}\left(Y\underset{\dot{}}{·}T\right)\right)$$