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

Metamath Proof Explorer

Theorem clmvsneg

Description: Multiplication of a vector by a negated scalar. ( lmodvsneg analog.) (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses clmvsneg.b 
|- B = ( Base ` W )
clmvsneg.f 
|- F = ( Scalar ` W )
clmvsneg.s 
|- .x. = ( .s ` W )
clmvsneg.n 
|- N = ( invg ` W )
clmvsneg.k 
|- K = ( Base ` F )
clmvsneg.w 
|- ( ph -> W e. CMod )
clmvsneg.x 
|- ( ph -> X e. B )
clmvsneg.r 
|- ( ph -> R e. K )
Assertion clmvsneg 
|- ( ph -> ( N ` ( R .x. X ) ) = ( -u R .x. X ) )

Proof

Step Hyp Ref Expression
1 clmvsneg.b 
 |-  B = ( Base ` W )
2 clmvsneg.f 
 |-  F = ( Scalar ` W )
3 clmvsneg.s 
 |-  .x. = ( .s ` W )
4 clmvsneg.n 
 |-  N = ( invg ` W )
5 clmvsneg.k 
 |-  K = ( Base ` F )
6 clmvsneg.w 
 |-  ( ph -> W e. CMod )
7 clmvsneg.x 
 |-  ( ph -> X e. B )
8 clmvsneg.r 
 |-  ( ph -> R e. K )
9 eqid 
 |-  ( invg ` F ) = ( invg ` F )
10 clmlmod 
 |-  ( W e. CMod -> W e. LMod )
11 6 10 syl 
 |-  ( ph -> W e. LMod )
12 1 2 3 4 5 9 11 7 8 lmodvsneg 
 |-  ( ph -> ( N ` ( R .x. X ) ) = ( ( ( invg ` F ) ` R ) .x. X ) )
13 2 5 clmneg 
 |-  ( ( W e. CMod /\ R e. K ) -> -u R = ( ( invg ` F ) ` R ) )
14 6 8 13 syl2anc 
 |-  ( ph -> -u R = ( ( invg ` F ) ` R ) )
15 14 oveq1d 
 |-  ( ph -> ( -u R .x. X ) = ( ( ( invg ` F ) ` R ) .x. X ) )
16 12 15 eqtr4d 
 |-  ( ph -> ( N ` ( R .x. X ) ) = ( -u R .x. X ) )