# Metamath Proof Explorer

## Theorem lmodvsinv2

Description: Multiplying a negated vector by a scalar. (Contributed by Stefan O'Rear, 5-Sep-2015)

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

### Proof

Step Hyp Ref Expression
1 lmodvsinv2.b
` |-  B = ( Base ` W )`
2 lmodvsinv2.f
` |-  F = ( Scalar ` W )`
3 lmodvsinv2.s
` |-  .x. = ( .s ` W )`
4 lmodvsinv2.n
` |-  N = ( invg ` W )`
5 lmodvsinv2.k
` |-  K = ( Base ` F )`
6 simp1
` |-  ( ( W e. LMod /\ R e. K /\ X e. B ) -> W e. LMod )`
7 lmodgrp
` |-  ( W e. LMod -> W e. Grp )`
8 6 7 syl
` |-  ( ( W e. LMod /\ R e. K /\ X e. B ) -> W e. Grp )`
9 simp3
` |-  ( ( W e. LMod /\ R e. K /\ X e. B ) -> X e. B )`
10 eqid
` |-  ( +g ` W ) = ( +g ` W )`
11 eqid
` |-  ( 0g ` W ) = ( 0g ` W )`
12 1 10 11 4 grprinv
` |-  ( ( W e. Grp /\ X e. B ) -> ( X ( +g ` W ) ( N ` X ) ) = ( 0g ` W ) )`
13 8 9 12 syl2anc
` |-  ( ( W e. LMod /\ R e. K /\ X e. B ) -> ( X ( +g ` W ) ( N ` X ) ) = ( 0g ` W ) )`
14 13 oveq2d
` |-  ( ( W e. LMod /\ R e. K /\ X e. B ) -> ( R .x. ( X ( +g ` W ) ( N ` X ) ) ) = ( R .x. ( 0g ` W ) ) )`
15 simp2
` |-  ( ( W e. LMod /\ R e. K /\ X e. B ) -> R e. K )`
16 1 4 grpinvcl
` |-  ( ( W e. Grp /\ X e. B ) -> ( N ` X ) e. B )`
17 8 9 16 syl2anc
` |-  ( ( W e. LMod /\ R e. K /\ X e. B ) -> ( N ` X ) e. B )`
18 1 10 2 3 5 lmodvsdi
` |-  ( ( W e. LMod /\ ( R e. K /\ X e. B /\ ( N ` X ) e. B ) ) -> ( R .x. ( X ( +g ` W ) ( N ` X ) ) ) = ( ( R .x. X ) ( +g ` W ) ( R .x. ( N ` X ) ) ) )`
19 6 15 9 17 18 syl13anc
` |-  ( ( W e. LMod /\ R e. K /\ X e. B ) -> ( R .x. ( X ( +g ` W ) ( N ` X ) ) ) = ( ( R .x. X ) ( +g ` W ) ( R .x. ( N ` X ) ) ) )`
20 2 3 5 11 lmodvs0
` |-  ( ( W e. LMod /\ R e. K ) -> ( R .x. ( 0g ` W ) ) = ( 0g ` W ) )`
21 6 15 20 syl2anc
` |-  ( ( W e. LMod /\ R e. K /\ X e. B ) -> ( R .x. ( 0g ` W ) ) = ( 0g ` W ) )`
22 14 19 21 3eqtr3d
` |-  ( ( W e. LMod /\ R e. K /\ X e. B ) -> ( ( R .x. X ) ( +g ` W ) ( R .x. ( N ` X ) ) ) = ( 0g ` W ) )`
23 1 2 3 5 lmodvscl
` |-  ( ( W e. LMod /\ R e. K /\ X e. B ) -> ( R .x. X ) e. B )`
24 1 2 3 5 lmodvscl
` |-  ( ( W e. LMod /\ R e. K /\ ( N ` X ) e. B ) -> ( R .x. ( N ` X ) ) e. B )`
25 6 15 17 24 syl3anc
` |-  ( ( W e. LMod /\ R e. K /\ X e. B ) -> ( R .x. ( N ` X ) ) e. B )`
26 1 10 11 4 grpinvid1
` |-  ( ( W e. Grp /\ ( R .x. X ) e. B /\ ( R .x. ( N ` X ) ) e. B ) -> ( ( N ` ( R .x. X ) ) = ( R .x. ( N ` X ) ) <-> ( ( R .x. X ) ( +g ` W ) ( R .x. ( N ` X ) ) ) = ( 0g ` W ) ) )`
27 8 23 25 26 syl3anc
` |-  ( ( W e. LMod /\ R e. K /\ X e. B ) -> ( ( N ` ( R .x. X ) ) = ( R .x. ( N ` X ) ) <-> ( ( R .x. X ) ( +g ` W ) ( R .x. ( N ` X ) ) ) = ( 0g ` W ) ) )`
28 22 27 mpbird
` |-  ( ( W e. LMod /\ R e. K /\ X e. B ) -> ( N ` ( R .x. X ) ) = ( R .x. ( N ` X ) ) )`
29 28 eqcomd
` |-  ( ( W e. LMod /\ R e. K /\ X e. B ) -> ( R .x. ( N ` X ) ) = ( N ` ( R .x. X ) ) )`