Metamath Proof Explorer

Theorem clmvsdir

Description: Distributive law for scalar product (right-distributivity). ( lmodvsdir analog.) (Contributed by Mario Carneiro, 16-Oct-2015)

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 clmvsdir 
|- ( ( W e. CMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( ( Q + R ) .x. X ) = ( ( Q .x. X ) .+ ( R .x. X ) ) )

Proof

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 2 clmadd 
 |-  ( W e. CMod -> + = ( +g ` F ) )
7 6 oveqd 
 |-  ( W e. CMod -> ( Q + R ) = ( Q ( +g ` F ) R ) )
8 7 oveq1d 
 |-  ( W e. CMod -> ( ( Q + R ) .x. X ) = ( ( Q ( +g ` F ) R ) .x. X ) )
9 8 adantr 
 |-  ( ( W e. CMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( ( Q + R ) .x. X ) = ( ( Q ( +g ` F ) R ) .x. X ) )
10 clmlmod 
 |-  ( W e. CMod -> W e. LMod )
11 eqid 
 |-  ( +g ` F ) = ( +g ` F )
12 1 5 2 3 4 11 lmodvsdir 
 |-  ( ( W e. LMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( ( Q ( +g ` F ) R ) .x. X ) = ( ( Q .x. X ) .+ ( R .x. X ) ) )
13 10 12 sylan 
 |-  ( ( W e. CMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( ( Q ( +g ` F ) R ) .x. X ) = ( ( Q .x. X ) .+ ( R .x. X ) ) )
14 9 13 eqtrd 
 |-  ( ( W e. CMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( ( Q + R ) .x. X ) = ( ( Q .x. X ) .+ ( R .x. X ) ) )