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

Metamath Proof Explorer

Theorem crng12d

Description: Commutative/associative law that swaps the first two factors in a triple product in a commutative ring. See also mul12d . (Contributed by SN, 8-Mar-2025)

		Ref	Expression
	Hypotheses	crng12d.b	$⊢ B = {Base}_{R}$
		crng12d.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
		crng12d.r	$⊢ φ \to R \in CRing$
		crng12d.1	$⊢ φ \to X \in B$
		crng12d.2	$⊢ φ \to Y \in B$
		crng12d.3	$⊢ φ \to Z \in B$
	Assertion	crng12d	$⊢ φ \to X \underset{˙}{\cdot} (Y \underset{˙}{\cdot} Z) = Y \underset{˙}{\cdot} (X \underset{˙}{\cdot} Z)$

Proof

Step	Hyp	Ref	Expression
1		crng12d.b	$⊢ B = {Base}_{R}$
2		crng12d.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		crng12d.r	$⊢ φ \to R \in CRing$
4		crng12d.1	$⊢ φ \to X \in B$
5		crng12d.2	$⊢ φ \to Y \in B$
6		crng12d.3	$⊢ φ \to Z \in B$
7	1 2 3 4 5	crngcomd	$⊢ φ \to X \underset{˙}{\cdot} Y = Y \underset{˙}{\cdot} X$
8	7	oveq1d	$⊢ φ \to (X \underset{˙}{\cdot} Y) \underset{˙}{\cdot} Z = (Y \underset{˙}{\cdot} X) \underset{˙}{\cdot} Z$
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 5 4 6	ringassd	$⊢ φ \to (Y \underset{˙}{\cdot} X) \underset{˙}{\cdot} Z = Y \underset{˙}{\cdot} (X \underset{˙}{\cdot} Z)$
12	8 10 11	3eqtr3d	$⊢ φ \to X \underset{˙}{\cdot} (Y \underset{˙}{\cdot} Z) = Y \underset{˙}{\cdot} (X \underset{˙}{\cdot} Z)$