Metamath Proof Explorer

Theorem lmodvsneg

Description: Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 lmodvsneg.b 
 |-  B = ( Base ` W )
2 lmodvsneg.f 
 |-  F = ( Scalar ` W )
3 lmodvsneg.s 
 |-  .x. = ( .s ` W )
4 lmodvsneg.n 
 |-  N = ( invg ` W )
5 lmodvsneg.k 
 |-  K = ( Base ` F )
6 lmodvsneg.m 
 |-  M = ( invg ` F )
7 lmodvsneg.w 
 |-  ( ph -> W e. LMod )
8 lmodvsneg.x 
 |-  ( ph -> X e. B )
9 lmodvsneg.r 
 |-  ( ph -> R e. K )
10 2 lmodring 
 |-  ( W e. LMod -> F e. Ring )
11 7 10 syl 
 |-  ( ph -> F e. Ring )
12 ringgrp 
 |-  ( F e. Ring -> F e. Grp )
13 11 12 syl 
 |-  ( ph -> F e. Grp )
14 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
15 5 14 ringidcl 
 |-  ( F e. Ring -> ( 1r ` F ) e. K )
16 11 15 syl 
 |-  ( ph -> ( 1r ` F ) e. K )
17 5 6 grpinvcl 
 |-  ( ( F e. Grp /\ ( 1r ` F ) e. K ) -> ( M ` ( 1r ` F ) ) e. K )
18 13 16 17 syl2anc 
 |-  ( ph -> ( M ` ( 1r ` F ) ) e. K )
19 eqid 
 |-  ( .r ` F ) = ( .r ` F )
20 1 2 3 5 19 lmodvsass 
 |-  ( ( W e. LMod /\ ( ( M ` ( 1r ` F ) ) e. K /\ R e. K /\ X e. B ) ) -> ( ( ( M ` ( 1r ` F ) ) ( .r ` F ) R ) .x. X ) = ( ( M ` ( 1r ` F ) ) .x. ( R .x. X ) ) )
21 7 18 9 8 20 syl13anc 
 |-  ( ph -> ( ( ( M ` ( 1r ` F ) ) ( .r ` F ) R ) .x. X ) = ( ( M ` ( 1r ` F ) ) .x. ( R .x. X ) ) )
22 5 19 14 6 11 9 ringnegl 
 |-  ( ph -> ( ( M ` ( 1r ` F ) ) ( .r ` F ) R ) = ( M ` R ) )
23 22 oveq1d 
 |-  ( ph -> ( ( ( M ` ( 1r ` F ) ) ( .r ` F ) R ) .x. X ) = ( ( M ` R ) .x. X ) )
24 1 2 3 5 lmodvscl 
 |-  ( ( W e. LMod /\ R e. K /\ X e. B ) -> ( R .x. X ) e. B )
25 7 9 8 24 syl3anc 
 |-  ( ph -> ( R .x. X ) e. B )
26 1 4 2 3 14 6 lmodvneg1 
 |-  ( ( W e. LMod /\ ( R .x. X ) e. B ) -> ( ( M ` ( 1r ` F ) ) .x. ( R .x. X ) ) = ( N ` ( R .x. X ) ) )
27 7 25 26 syl2anc 
 |-  ( ph -> ( ( M ` ( 1r ` F ) ) .x. ( R .x. X ) ) = ( N ` ( R .x. X ) ) )
28 21 23 27 3eqtr3rd 
 |-  ( ph -> ( N ` ( R .x. X ) ) = ( ( M ` R ) .x. X ) )