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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	crng12d.t	⊢ · = ( .r ‘ 𝑅 )
	crng12d.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	crng12d.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	crng12d.2	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	crng12d.3	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion	crng12d	⊢ ( 𝜑 → ( 𝑋 · ( 𝑌 · 𝑍 ) ) = ( 𝑌 · ( 𝑋 · 𝑍 ) ) )

Proof

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