This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem crng32d

Description: Commutative/associative law that swaps the last two factors in a triple product in a commutative ring. See also mul32d . (Contributed by Thierry Arnoux, 4-May-2025)

		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$
	Assertion	crng32d	$⊢ φ \to (X \underset{˙}{\cdot} Y) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} Y$

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	1 2 3 5 6	crngcomd	$⊢ φ \to Y \underset{˙}{\cdot} Z = Z \underset{˙}{\cdot} Y$
8	7	oveq2d	$⊢ φ \to X \underset{˙}{\cdot} (Y \underset{˙}{\cdot} Z) = X \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)$
9	3	crngringd	$⊢ φ \to R \in Ring$
10	1 2 9 4 5 6	ringassd	$⊢ φ \to (X \underset{˙}{\cdot} Y) \underset{˙}{\cdot} Z = X \underset{˙}{\cdot} (Y \underset{˙}{\cdot} Z)$
11	1 2 9 4 6 5	ringassd	$⊢ φ \to (X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} Y = X \underset{˙}{\cdot} (Z \underset{˙}{\cdot} Y)$
12	8 10 11	3eqtr4d	$⊢ φ \to (X \underset{˙}{\cdot} Y) \underset{˙}{\cdot} Z = (X \underset{˙}{\cdot} Z) \underset{˙}{\cdot} Y$