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

Metamath Proof Explorer

Theorem ringassd

Description: Associative law for multiplication in a ring. (Contributed by SN, 14-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 ringassd.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 ringassd.t ⊢ · = ( .r ‘ 𝑅 )
3 ringassd.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 ringassd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 ringassd.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 ringassd.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
7 1 2 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 · 𝑌 ) · 𝑍 ) = ( 𝑋 · ( 𝑌 · 𝑍 ) ) )
8 3 4 5 6 7 syl13anc ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) · 𝑍 ) = ( 𝑋 · ( 𝑌 · 𝑍 ) ) )