Metamath Proof Explorer

Theorem lmodvsinv

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

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

Proof

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