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