Metamath Proof Explorer


Theorem srgdi

Description: Distributive law for the multiplication operation of a semiring. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Thierry Arnoux, 1-Apr-2018)

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

Proof

Step Hyp Ref Expression
1 srgdi.b 𝐵 = ( Base ‘ 𝑅 )
2 srgdi.p + = ( +g𝑅 )
3 srgdi.t · = ( .r𝑅 )
4 1 2 3 srgi ( ( 𝑅 ∈ SRing ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( ( 𝑋 · ( 𝑌 + 𝑍 ) ) = ( ( 𝑋 · 𝑌 ) + ( 𝑋 · 𝑍 ) ) ∧ ( ( 𝑋 + 𝑌 ) · 𝑍 ) = ( ( 𝑋 · 𝑍 ) + ( 𝑌 · 𝑍 ) ) ) )
5 4 simpld ( ( 𝑅 ∈ SRing ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( 𝑋 · ( 𝑌 + 𝑍 ) ) = ( ( 𝑋 · 𝑌 ) + ( 𝑋 · 𝑍 ) ) )