Metamath Proof Explorer


Theorem slmdvsdi

Description: Distributive law for scalar product. ( ax-hvdistr1 analog.) (Contributed by NM, 10-Jan-2014) (Revised by Mario Carneiro, 22-Sep-2015) (Revised by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Hypotheses slmdvsdi.v
|- V = ( Base ` W )
slmdvsdi.a
|- .+ = ( +g ` W )
slmdvsdi.f
|- F = ( Scalar ` W )
slmdvsdi.s
|- .x. = ( .s ` W )
slmdvsdi.k
|- K = ( Base ` F )
Assertion slmdvsdi
|- ( ( W e. SLMod /\ ( R e. K /\ X e. V /\ Y e. V ) ) -> ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) )

Proof

Step Hyp Ref Expression
1 slmdvsdi.v
 |-  V = ( Base ` W )
2 slmdvsdi.a
 |-  .+ = ( +g ` W )
3 slmdvsdi.f
 |-  F = ( Scalar ` W )
4 slmdvsdi.s
 |-  .x. = ( .s ` W )
5 slmdvsdi.k
 |-  K = ( Base ` F )
6 eqid
 |-  ( 0g ` W ) = ( 0g ` W )
7 eqid
 |-  ( +g ` F ) = ( +g ` F )
8 eqid
 |-  ( .r ` F ) = ( .r ` F )
9 eqid
 |-  ( 1r ` F ) = ( 1r ` F )
10 eqid
 |-  ( 0g ` F ) = ( 0g ` F )
11 1 2 4 6 3 5 7 8 9 10 slmdlema
 |-  ( ( W e. SLMod /\ ( R e. K /\ R e. K ) /\ ( Y e. V /\ X e. V ) ) -> ( ( ( R .x. X ) e. V /\ ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) /\ ( ( R ( +g ` F ) R ) .x. X ) = ( ( R .x. X ) .+ ( R .x. X ) ) ) /\ ( ( ( R ( .r ` F ) R ) .x. X ) = ( R .x. ( R .x. X ) ) /\ ( ( 1r ` F ) .x. X ) = X /\ ( ( 0g ` F ) .x. X ) = ( 0g ` W ) ) ) )
12 11 simpld
 |-  ( ( W e. SLMod /\ ( R e. K /\ R e. K ) /\ ( Y e. V /\ X e. V ) ) -> ( ( R .x. X ) e. V /\ ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) /\ ( ( R ( +g ` F ) R ) .x. X ) = ( ( R .x. X ) .+ ( R .x. X ) ) ) )
13 12 simp2d
 |-  ( ( W e. SLMod /\ ( R e. K /\ R e. K ) /\ ( Y e. V /\ X e. V ) ) -> ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) )
14 13 3expia
 |-  ( ( W e. SLMod /\ ( R e. K /\ R e. K ) ) -> ( ( Y e. V /\ X e. V ) -> ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) ) )
15 14 anabsan2
 |-  ( ( W e. SLMod /\ R e. K ) -> ( ( Y e. V /\ X e. V ) -> ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) ) )
16 15 exp4b
 |-  ( W e. SLMod -> ( R e. K -> ( Y e. V -> ( X e. V -> ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) ) ) ) )
17 16 com34
 |-  ( W e. SLMod -> ( R e. K -> ( X e. V -> ( Y e. V -> ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) ) ) ) )
18 17 3imp2
 |-  ( ( W e. SLMod /\ ( R e. K /\ X e. V /\ Y e. V ) ) -> ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) )