Metamath Proof Explorer


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