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 Jeff Madsen, 19-Jun-2010) (Revised by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	crng32d.b	$$⊢B={\mathrm{Base}}_R$$
	crng32d.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	crng32d.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	crng32d.x	$$⊢\phi \to X\in B$$
	crng32d.y	$$⊢\phi \to Y\in B$$
	crng32d.z	$$⊢\phi \to Z\in B$$
Assertion	crng32d	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{·}Z=\left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}Y$$

Proof

Step	Hyp	Ref	Expression
1		crng32d.b	$$⊢B={\mathrm{Base}}_R$$
2		crng32d.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		crng32d.r	$$⊢\phi \to R\in \mathrm{CRing}$$
4		crng32d.x	$$⊢\phi \to X\in B$$
5		crng32d.y	$$⊢\phi \to Y\in B$$
6		crng32d.z	$$⊢\phi \to Z\in B$$
7	1 2 3 5 6	crngcomd	$$⊢\phi \to Y\underset{\dot{}}{·}Z=Z\underset{\dot{}}{·}Y$$
8	7	oveq2d	$$⊢\phi \to X\underset{\dot{}}{·}\left(Y\underset{\dot{}}{·}Z\right)=X\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}Y\right)$$
9	3	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
10	1 2 9 4 5 6	ringassd	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{·}Z=X\underset{\dot{}}{·}\left(Y\underset{\dot{}}{·}Z\right)$$
11	1 2 9 4 6 5	ringassd	$$⊢\phi \to \left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}Y\right)$$
12	8 10 11	3eqtr4d	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y\right)\underset{\dot{}}{·}Z=\left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}Y$$