Metamath Proof Explorer


Theorem ringdir

Description: Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007)

Ref Expression
Hypotheses ringdi.b 𝐵 = ( Base ‘ 𝑅 )
ringdi.p + = ( +g𝑅 )
ringdi.t · = ( .r𝑅 )
Assertion ringdir ( ( 𝑅 ∈ Ring ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( ( 𝑋 + 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) + ( 𝑌 · 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 ringdi.b 𝐵 = ( Base ‘ 𝑅 )
2 ringdi.p + = ( +g𝑅 )
3 ringdi.t · = ( .r𝑅 )
4 1 2 3 ringi ( ( 𝑅 ∈ Ring ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( ( 𝑋 · ( 𝑌 + 𝑍 ) ) = ( ( 𝑋 · 𝑌 ) + ( 𝑋 · 𝑍 ) ) ∧ ( ( 𝑋 + 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) + ( 𝑌 · 𝑍 ) ) ) )
5 4 simprd ( ( 𝑅 ∈ Ring ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( ( 𝑋 + 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) + ( 𝑌 · 𝑍 ) ) )