This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 Thierry Arnoux, 4-May-2025)

Ref Expression
Hypotheses crng32d.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
crng32d.t ⊢ · = ( .r ‘ 𝑅 )
crng32d.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
crng32d.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
crng32d.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
crng32d.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion crng32d ( 𝜑 → ( ( 𝑋 · 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) · 𝑌 ) )

Proof

Step Hyp Ref Expression
1 crng32d.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 crng32d.t ⊢ · = ( .r ‘ 𝑅 )
3 crng32d.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
4 crng32d.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 crng32d.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 crng32d.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 ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) · 𝑌 ) )