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={\mathrm{Base}}_R$$
	crng12d.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	crng12d.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	crng12d.1	$$⊢\phi \to X\in B$$
	crng12d.2	$$⊢\phi \to Y\in B$$
	crng12d.3	$$⊢\phi \to Z\in B$$
Assertion	crng12d	$$⊢\phi \to X\underset{\dot{}}{·}\left(Y\underset{\dot{}}{·}Z\right)=Y\underset{\dot{}}{·}\left(X\underset{\dot{}}{·}Z\right)$$

Proof

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