# 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 )`
` |-  ( ( 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 ) ) )`