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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	cringmul32d.t	⊢ · = ( .r ‘ 𝑅 )
	cringmul32d.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	cringmul32d.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	cringmul32d.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	cringmul32d.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion	cringmul32d	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) · 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		cringmul32d.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		cringmul32d.t	⊢ · = ( .r ‘ 𝑅 )
3		cringmul32d.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
4		cringmul32d.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		cringmul32d.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		cringmul32d.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
7	1 2 3 5 6	crngcomd	⊢ ( 𝜑 → ( 𝑌 · 𝑍 ) = ( 𝑍 · 𝑌 ) )
8	7	oveq2d	⊢ ( 𝜑 → ( 𝑋 · ( 𝑌 · 𝑍 ) ) = ( 𝑋 · ( 𝑍 · 𝑌 ) ) )
9	3	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
10	1 2 9 4 5 6	ringassd	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) · 𝑍 ) = ( 𝑋 · ( 𝑌 · 𝑍 ) ) )
11	1 2 9 4 6 5	ringassd	⊢ ( 𝜑 → ( ( 𝑋 · 𝑍 ) · 𝑌 ) = ( 𝑋 · ( 𝑍 · 𝑌 ) ) )
12	8 10 11	3eqtr4d	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) · 𝑌 ) )