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