Metamath Proof Explorer

Theorem crng4

Description: Commutative/associative law for commutative rings. See also mul4d . (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by AV, 20-Jul-2026)

		Ref	Expression
	Hypotheses	crng32d.b	$⊢ B = {Base}_{R}$
		crng32d.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		crng32d.r	$⊢ φ \to R \in CRing$
		crng32d.x	$⊢ φ \to X \in B$
		crng32d.y	$⊢ φ \to Y \in B$
		crng32d.z	$⊢ φ \to Z \in B$
		crng4.u	$⊢ φ \to U \in B$
	Assertion	crng4	$⊢ φ \to (X \underset{˙}{\cdot} Y) \underset{˙}{\cdot} (Z \underset{˙}{\cdot} U) = (X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} (Y \underset{˙}{\cdot} U)$

Proof

Step	Hyp	Ref	Expression
1		crng32d.b	$⊢ B = {Base}_{R}$
2		crng32d.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		crng32d.r	$⊢ φ \to R \in CRing$
4		crng32d.x	$⊢ φ \to X \in B$
5		crng32d.y	$⊢ φ \to Y \in B$
6		crng32d.z	$⊢ φ \to Z \in B$
7		crng4.u	$⊢ φ \to U \in B$
8	1 2 3 4 5 6	crng32d	$⊢ φ \to (X \underset{˙}{\cdot} Y) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} Y$
9	8	oveq1d	$⊢ φ \to ((X \underset{˙}{\cdot} Y) \underset{˙}{\cdot} Z) \underset{˙}{\cdot} U = ((X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} Y) \underset{˙}{\cdot} U$
10	3	crngringd	$⊢ φ \to R \in Ring$
11	1 2 10 4 5	ringcld	$⊢ φ \to X \underset{˙}{\cdot} Y \in B$
12	1 2 10 11 6 7	ringassd	$⊢ φ \to ((X \underset{˙}{\cdot} Y) \underset{˙}{\cdot} Z) \underset{˙}{\cdot} U = (X \underset{˙}{\cdot} Y) \underset{˙}{\cdot} (Z \underset{˙}{\cdot} U)$
13	1 2 10 4 6	ringcld	$⊢ φ \to X \underset{˙}{\cdot} Z \in B$
14	1 2 10 13 5 7	ringassd	$⊢ φ \to ((X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} Y) \underset{˙}{\cdot} U = (X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} (Y \underset{˙}{\cdot} U)$
15	9 12 14	3eqtr3d	$⊢ φ \to (X \underset{˙}{\cdot} Y) \underset{˙}{\cdot} (Z \underset{˙}{\cdot} U) = (X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} (Y \underset{˙}{\cdot} U)$