Metamath Proof Explorer


Theorem srgdir

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
|- B = ( Base ` R )
srgdi.p
|- .+ = ( +g ` R )
srgdi.t
|- .x. = ( .r ` R )
Assertion srgdir
|- ( ( R e. SRing /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) )

Proof

Step Hyp Ref Expression
1 srgdi.b
 |-  B = ( Base ` R )
2 srgdi.p
 |-  .+ = ( +g ` R )
3 srgdi.t
 |-  .x. = ( .r ` R )
4 1 2 3 srgi
 |-  ( ( R e. SRing /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .x. ( Y .+ Z ) ) = ( ( X .x. Y ) .+ ( X .x. Z ) ) /\ ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) ) )
5 4 simprd
 |-  ( ( R e. SRing /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) )