Metamath Proof Explorer

Theorem lmodvneg1

Description: Minus 1 times a vector is the negative of the vector. Equation 2 of Kreyszig p. 51. (Contributed by NM, 18-Apr-2014) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lmodvneg1.v 
|- V = ( Base ` W )
lmodvneg1.n 
|- N = ( invg ` W )
lmodvneg1.f 
|- F = ( Scalar ` W )
lmodvneg1.s 
|- .x. = ( .s ` W )
lmodvneg1.u 
|- .1. = ( 1r ` F )
lmodvneg1.m 
|- M = ( invg ` F )
Assertion lmodvneg1 
|- ( ( W e. LMod /\ X e. V ) -> ( ( M ` .1. ) .x. X ) = ( N ` X ) )

Proof

Step Hyp Ref Expression
1 lmodvneg1.v 
 |-  V = ( Base ` W )
2 lmodvneg1.n 
 |-  N = ( invg ` W )
3 lmodvneg1.f 
 |-  F = ( Scalar ` W )
4 lmodvneg1.s 
 |-  .x. = ( .s ` W )
5 lmodvneg1.u 
 |-  .1. = ( 1r ` F )
6 lmodvneg1.m 
 |-  M = ( invg ` F )
7 simpl 
 |-  ( ( W e. LMod /\ X e. V ) -> W e. LMod )
8 3 lmodfgrp 
 |-  ( W e. LMod -> F e. Grp )
9 eqid 
 |-  ( Base ` F ) = ( Base ` F )
10 3 9 5 lmod1cl 
 |-  ( W e. LMod -> .1. e. ( Base ` F ) )
11 10 adantr 
 |-  ( ( W e. LMod /\ X e. V ) -> .1. e. ( Base ` F ) )
12 9 6 grpinvcl 
 |-  ( ( F e. Grp /\ .1. e. ( Base ` F ) ) -> ( M ` .1. ) e. ( Base ` F ) )
13 8 11 12 syl2an2r 
 |-  ( ( W e. LMod /\ X e. V ) -> ( M ` .1. ) e. ( Base ` F ) )
14 simpr 
 |-  ( ( W e. LMod /\ X e. V ) -> X e. V )
15 1 3 4 9 lmodvscl 
 |-  ( ( W e. LMod /\ ( M ` .1. ) e. ( Base ` F ) /\ X e. V ) -> ( ( M ` .1. ) .x. X ) e. V )
16 7 13 14 15 syl3anc 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( M ` .1. ) .x. X ) e. V )
17 eqid 
 |-  ( +g ` W ) = ( +g ` W )
18 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
19 1 17 18 lmod0vrid 
 |-  ( ( W e. LMod /\ ( ( M ` .1. ) .x. X ) e. V ) -> ( ( ( M ` .1. ) .x. X ) ( +g ` W ) ( 0g ` W ) ) = ( ( M ` .1. ) .x. X ) )
20 16 19 syldan 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( ( M ` .1. ) .x. X ) ( +g ` W ) ( 0g ` W ) ) = ( ( M ` .1. ) .x. X ) )
21 1 2 lmodvnegcl 
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` X ) e. V )
22 1 17 lmodass 
 |-  ( ( W e. LMod /\ ( ( ( M ` .1. ) .x. X ) e. V /\ X e. V /\ ( N ` X ) e. V ) ) -> ( ( ( ( M ` .1. ) .x. X ) ( +g ` W ) X ) ( +g ` W ) ( N ` X ) ) = ( ( ( M ` .1. ) .x. X ) ( +g ` W ) ( X ( +g ` W ) ( N ` X ) ) ) )
23 7 16 14 21 22 syl13anc 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( ( ( M ` .1. ) .x. X ) ( +g ` W ) X ) ( +g ` W ) ( N ` X ) ) = ( ( ( M ` .1. ) .x. X ) ( +g ` W ) ( X ( +g ` W ) ( N ` X ) ) ) )
24 1 3 4 5 lmodvs1 
 |-  ( ( W e. LMod /\ X e. V ) -> ( .1. .x. X ) = X )
25 24 oveq2d 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( ( M ` .1. ) .x. X ) ( +g ` W ) ( .1. .x. X ) ) = ( ( ( M ` .1. ) .x. X ) ( +g ` W ) X ) )
26 eqid 
 |-  ( +g ` F ) = ( +g ` F )
27 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
28 9 26 27 6 grplinv 
 |-  ( ( F e. Grp /\ .1. e. ( Base ` F ) ) -> ( ( M ` .1. ) ( +g ` F ) .1. ) = ( 0g ` F ) )
29 8 11 28 syl2an2r 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( M ` .1. ) ( +g ` F ) .1. ) = ( 0g ` F ) )
30 29 oveq1d 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( ( M ` .1. ) ( +g ` F ) .1. ) .x. X ) = ( ( 0g ` F ) .x. X ) )
31 1 17 3 4 9 26 lmodvsdir 
 |-  ( ( W e. LMod /\ ( ( M ` .1. ) e. ( Base ` F ) /\ .1. e. ( Base ` F ) /\ X e. V ) ) -> ( ( ( M ` .1. ) ( +g ` F ) .1. ) .x. X ) = ( ( ( M ` .1. ) .x. X ) ( +g ` W ) ( .1. .x. X ) ) )
32 7 13 11 14 31 syl13anc 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( ( M ` .1. ) ( +g ` F ) .1. ) .x. X ) = ( ( ( M ` .1. ) .x. X ) ( +g ` W ) ( .1. .x. X ) ) )
33 1 3 4 27 18 lmod0vs 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( 0g ` F ) .x. X ) = ( 0g ` W ) )
34 30 32 33 3eqtr3d 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( ( M ` .1. ) .x. X ) ( +g ` W ) ( .1. .x. X ) ) = ( 0g ` W ) )
35 25 34 eqtr3d 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( ( M ` .1. ) .x. X ) ( +g ` W ) X ) = ( 0g ` W ) )
36 35 oveq1d 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( ( ( M ` .1. ) .x. X ) ( +g ` W ) X ) ( +g ` W ) ( N ` X ) ) = ( ( 0g ` W ) ( +g ` W ) ( N ` X ) ) )
37 23 36 eqtr3d 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( ( M ` .1. ) .x. X ) ( +g ` W ) ( X ( +g ` W ) ( N ` X ) ) ) = ( ( 0g ` W ) ( +g ` W ) ( N ` X ) ) )
38 1 17 18 2 lmodvnegid 
 |-  ( ( W e. LMod /\ X e. V ) -> ( X ( +g ` W ) ( N ` X ) ) = ( 0g ` W ) )
39 38 oveq2d 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( ( M ` .1. ) .x. X ) ( +g ` W ) ( X ( +g ` W ) ( N ` X ) ) ) = ( ( ( M ` .1. ) .x. X ) ( +g ` W ) ( 0g ` W ) ) )
40 1 17 18 lmod0vlid 
 |-  ( ( W e. LMod /\ ( N ` X ) e. V ) -> ( ( 0g ` W ) ( +g ` W ) ( N ` X ) ) = ( N ` X ) )
41 21 40 syldan 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( 0g ` W ) ( +g ` W ) ( N ` X ) ) = ( N ` X ) )
42 37 39 41 3eqtr3d 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( ( M ` .1. ) .x. X ) ( +g ` W ) ( 0g ` W ) ) = ( N ` X ) )
43 20 42 eqtr3d 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( M ` .1. ) .x. X ) = ( N ` X ) )