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	|- B = ( Base ` R )
	ringdi.p	|- .+ = ( +g ` R )
	ringdi.t	|- .x. = ( .r ` R )
Assertion	ringdir	|- ( ( R e. Ring /\ ( 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		ringdi.b	|- B = ( Base ` R )
2		ringdi.p	|- .+ = ( +g ` R )
3		ringdi.t	|- .x. = ( .r ` R )
4	1 2 3	ringi	|- ( ( R e. Ring /\ ( 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. Ring /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .+ Y ) .x. Z ) = ( ( X .x. Z ) .+ ( Y .x. Z ) ) )