This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clmsubdir

Description: Scalar multiplication distributive law for subtraction. ( lmodsubdir analog.) (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses clmsubdir.v 
|- V = ( Base ` W )
clmsubdir.t 
|- .x. = ( .s ` W )
clmsubdir.f 
|- F = ( Scalar ` W )
clmsubdir.k 
|- K = ( Base ` F )
clmsubdir.m 
|- .- = ( -g ` W )
clmsubdir.w 
|- ( ph -> W e. CMod )
clmsubdir.a 
|- ( ph -> A e. K )
clmsubdir.b 
|- ( ph -> B e. K )
clmsubdir.x 
|- ( ph -> X e. V )
Assertion clmsubdir 
|- ( ph -> ( ( A - B ) .x. X ) = ( ( A .x. X ) .- ( B .x. X ) ) )

Proof

Step Hyp Ref Expression
1 clmsubdir.v 
 |-  V = ( Base ` W )
2 clmsubdir.t 
 |-  .x. = ( .s ` W )
3 clmsubdir.f 
 |-  F = ( Scalar ` W )
4 clmsubdir.k 
 |-  K = ( Base ` F )
5 clmsubdir.m 
 |-  .- = ( -g ` W )
6 clmsubdir.w 
 |-  ( ph -> W e. CMod )
7 clmsubdir.a 
 |-  ( ph -> A e. K )
8 clmsubdir.b 
 |-  ( ph -> B e. K )
9 clmsubdir.x 
 |-  ( ph -> X e. V )
10 3 4 clmsub 
 |-  ( ( W e. CMod /\ A e. K /\ B e. K ) -> ( A - B ) = ( A ( -g ` F ) B ) )
11 6 7 8 10 syl3anc 
 |-  ( ph -> ( A - B ) = ( A ( -g ` F ) B ) )
12 11 oveq1d 
 |-  ( ph -> ( ( A - B ) .x. X ) = ( ( A ( -g ` F ) B ) .x. X ) )
13 eqid 
 |-  ( -g ` F ) = ( -g ` F )
14 clmlmod 
 |-  ( W e. CMod -> W e. LMod )
15 6 14 syl 
 |-  ( ph -> W e. LMod )
16 1 2 3 4 5 13 15 7 8 9 lmodsubdir 
 |-  ( ph -> ( ( A ( -g ` F ) B ) .x. X ) = ( ( A .x. X ) .- ( B .x. X ) ) )
17 12 16 eqtrd 
 |-  ( ph -> ( ( A - B ) .x. X ) = ( ( A .x. X ) .- ( B .x. X ) ) )