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 ) ) )