Description: Distributive law for scalar product (left-distributivity). ( lmodvsdi analog.) (Contributed by NM, 3-Nov-2006) (Revised by AV, 28-Sep-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | clmvscl.v | |- V = ( Base ` W ) |
|
| clmvscl.f | |- F = ( Scalar ` W ) |
||
| clmvscl.s | |- .x. = ( .s ` W ) |
||
| clmvscl.k | |- K = ( Base ` F ) |
||
| clmvsdir.a | |- .+ = ( +g ` W ) |
||
| Assertion | clmvsdi | |- ( ( W e. CMod /\ ( A e. K /\ X e. V /\ Y e. V ) ) -> ( A .x. ( X .+ Y ) ) = ( ( A .x. X ) .+ ( A .x. Y ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | clmvscl.v | |- V = ( Base ` W ) |
|
| 2 | clmvscl.f | |- F = ( Scalar ` W ) |
|
| 3 | clmvscl.s | |- .x. = ( .s ` W ) |
|
| 4 | clmvscl.k | |- K = ( Base ` F ) |
|
| 5 | clmvsdir.a | |- .+ = ( +g ` W ) |
|
| 6 | clmlmod | |- ( W e. CMod -> W e. LMod ) |
|
| 7 | 1 5 2 3 4 | lmodvsdi | |- ( ( W e. LMod /\ ( A e. K /\ X e. V /\ Y e. V ) ) -> ( A .x. ( X .+ Y ) ) = ( ( A .x. X ) .+ ( A .x. Y ) ) ) |
| 8 | 6 7 | sylan | |- ( ( W e. CMod /\ ( A e. K /\ X e. V /\ Y e. V ) ) -> ( A .x. ( X .+ Y ) ) = ( ( A .x. X ) .+ ( A .x. Y ) ) ) |