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