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 ) ) ) |
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 ) ) ) |