Theorem ringdi22

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

	Ref	Expression
Hypotheses	ringdi22.1	$$⊢B={\mathrm{Base}}_R$$
	ringdi22.2	$$⊢\underset{\dot{}}{+}={+}_R$$
	ringdi22.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	ringdi22.4	$$⊢\phi \to R\in \mathrm{Ring}$$
	ringdi22.5	$$⊢\phi \to X\in B$$
	ringdi22.6	$$⊢\phi \to Y\in B$$
	ringdi22.7	$$⊢\phi \to Z\in B$$
	ringdi22.8	$$⊢\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		ringdi22.1	$$⊢B={\mathrm{Base}}_R$$
2		ringdi22.2	$$⊢\underset{\dot{}}{+}={+}_R$$
3		ringdi22.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		ringdi22.4	$$⊢\phi \to R\in \mathrm{Ring}$$
5		ringdi22.5	$$⊢\phi \to X\in B$$
6		ringdi22.6	$$⊢\phi \to Y\in B$$
7		ringdi22.7	$$⊢\phi \to Z\in B$$
8		ringdi22.8	$$⊢\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)$$