ringdi22

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

	Ref	Expression
Hypotheses	ringdi22.1	$⊢ B = {Base}_{R}$
	ringdi22.2	$⊢ \underset{˙}{+} = +_{R}$
	ringdi22.3	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	ringdi22.4	$⊢ φ \to R \in Ring$
	ringdi22.5	$⊢ φ \to X \in B$
	ringdi22.6	$⊢ φ \to Y \in B$
	ringdi22.7	$⊢ φ \to Z \in B$
	ringdi22.8	$⊢ φ \to T \in B$
Assertion	ringdi22	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{\cdot} (Z \underset{˙}{+} T) = ((X \underset{˙}{\cdot} Z) \underset{˙}{+} (Y \underset{˙}{\cdot} Z)) \underset{˙}{+} ((X \underset{˙}{\cdot} T) \underset{˙}{+} (Y \underset{˙}{\cdot} T))$

Step	Hyp	Ref	Expression
1		ringdi22.1	$⊢ B = {Base}_{R}$
2		ringdi22.2	$⊢ \underset{˙}{+} = +_{R}$
3		ringdi22.3	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		ringdi22.4	$⊢ φ \to R \in Ring$
5		ringdi22.5	$⊢ φ \to X \in B$
6		ringdi22.6	$⊢ φ \to Y \in B$
7		ringdi22.7	$⊢ φ \to Z \in B$
8		ringdi22.8	$⊢ φ \to T \in B$
9	4	ringgrpd	$⊢ φ \to R \in Grp$
10	1 2 9 5 6	grpcld	$⊢ φ \to X \underset{˙}{+} Y \in B$
11	1 2 3 4 10 7 8	ringdid	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{\cdot} (Z \underset{˙}{+} T) = ((X \underset{˙}{+} Y) \underset{˙}{\cdot} Z) \underset{˙}{+} ((X \underset{˙}{+} Y) \underset{˙}{\cdot} T)$
12	1 2 3 4 5 6 7	ringdird	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) \underset{˙}{+} (Y \underset{˙}{\cdot} Z)$
13	1 2 3 4 5 6 8	ringdird	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{\cdot} T = (X \underset{˙}{\cdot} T) \underset{˙}{+} (Y \underset{˙}{\cdot} T)$
14	12 13	oveq12d	$⊢ φ \to ((X \underset{˙}{+} Y) \underset{˙}{\cdot} Z) \underset{˙}{+} ((X \underset{˙}{+} Y) \underset{˙}{\cdot} T) = ((X \underset{˙}{\cdot} Z) \underset{˙}{+} (Y \underset{˙}{\cdot} Z)) \underset{˙}{+} ((X \underset{˙}{\cdot} T) \underset{˙}{+} (Y \underset{˙}{\cdot} T))$
15	11 14	eqtrd	$⊢ φ \to (X \underset{˙}{+} Y) \underset{˙}{\cdot} (Z \underset{˙}{+} T) = ((X \underset{˙}{\cdot} Z) \underset{˙}{+} (Y \underset{˙}{\cdot} Z)) \underset{˙}{+} ((X \underset{˙}{\cdot} T) \underset{˙}{+} (Y \underset{˙}{\cdot} T))$

Metamath Proof Explorer