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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑋 · ( 𝑌 · 𝑍 ) ) = ( 𝑌 · ( 𝑋 · 𝑍 ) ) )