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