Theorem cringmul32d

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

	Ref	Expression
Hypotheses	cringmul32d.b	$$⊢B={\mathrm{Base}}_R$$
	cringmul32d.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	cringmul32d.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	cringmul32d.x	$$⊢\phi \to X\in B$$
	cringmul32d.y	$$⊢\phi \to Y\in B$$
	cringmul32d.z	$$⊢\phi \to Z\in B$$
Assertion	cringmul32d	$$⊢\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		cringmul32d.b	$$⊢B={\mathrm{Base}}_R$$
2		cringmul32d.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		cringmul32d.r	$$⊢\phi \to R\in \mathrm{CRing}$$
4		cringmul32d.x	$$⊢\phi \to X\in B$$
5		cringmul32d.y	$$⊢\phi \to Y\in B$$
6		cringmul32d.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$$