Metamath Proof Explorer


Theorem vcm

Description: Minus 1 times a vector is the underlying group's inverse element. Equation 2 of Kreyszig p. 51. (Contributed by NM, 25-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses vcm.1
|- G = ( 1st ` W )
vcm.2
|- S = ( 2nd ` W )
vcm.3
|- X = ran G
vcm.4
|- M = ( inv ` G )
Assertion vcm
|- ( ( W e. CVecOLD /\ A e. X ) -> ( -u 1 S A ) = ( M ` A ) )

Proof

Step Hyp Ref Expression
1 vcm.1
 |-  G = ( 1st ` W )
2 vcm.2
 |-  S = ( 2nd ` W )
3 vcm.3
 |-  X = ran G
4 vcm.4
 |-  M = ( inv ` G )
5 1 vcgrp
 |-  ( W e. CVecOLD -> G e. GrpOp )
6 5 adantr
 |-  ( ( W e. CVecOLD /\ A e. X ) -> G e. GrpOp )
7 neg1cn
 |-  -u 1 e. CC
8 1 2 3 vccl
 |-  ( ( W e. CVecOLD /\ -u 1 e. CC /\ A e. X ) -> ( -u 1 S A ) e. X )
9 7 8 mp3an2
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( -u 1 S A ) e. X )
10 eqid
 |-  ( GId ` G ) = ( GId ` G )
11 3 10 grporid
 |-  ( ( G e. GrpOp /\ ( -u 1 S A ) e. X ) -> ( ( -u 1 S A ) G ( GId ` G ) ) = ( -u 1 S A ) )
12 6 9 11 syl2anc
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( ( -u 1 S A ) G ( GId ` G ) ) = ( -u 1 S A ) )
13 simpr
 |-  ( ( W e. CVecOLD /\ A e. X ) -> A e. X )
14 3 4 grpoinvcl
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( M ` A ) e. X )
15 5 14 sylan
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( M ` A ) e. X )
16 3 grpoass
 |-  ( ( G e. GrpOp /\ ( ( -u 1 S A ) e. X /\ A e. X /\ ( M ` A ) e. X ) ) -> ( ( ( -u 1 S A ) G A ) G ( M ` A ) ) = ( ( -u 1 S A ) G ( A G ( M ` A ) ) ) )
17 6 9 13 15 16 syl13anc
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( ( ( -u 1 S A ) G A ) G ( M ` A ) ) = ( ( -u 1 S A ) G ( A G ( M ` A ) ) ) )
18 1 2 3 vcidOLD
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( 1 S A ) = A )
19 18 oveq2d
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( ( -u 1 S A ) G ( 1 S A ) ) = ( ( -u 1 S A ) G A ) )
20 ax-1cn
 |-  1 e. CC
21 1pneg1e0
 |-  ( 1 + -u 1 ) = 0
22 20 7 21 addcomli
 |-  ( -u 1 + 1 ) = 0
23 22 oveq1i
 |-  ( ( -u 1 + 1 ) S A ) = ( 0 S A )
24 1 2 3 vcdir
 |-  ( ( W e. CVecOLD /\ ( -u 1 e. CC /\ 1 e. CC /\ A e. X ) ) -> ( ( -u 1 + 1 ) S A ) = ( ( -u 1 S A ) G ( 1 S A ) ) )
25 7 24 mp3anr1
 |-  ( ( W e. CVecOLD /\ ( 1 e. CC /\ A e. X ) ) -> ( ( -u 1 + 1 ) S A ) = ( ( -u 1 S A ) G ( 1 S A ) ) )
26 20 25 mpanr1
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( ( -u 1 + 1 ) S A ) = ( ( -u 1 S A ) G ( 1 S A ) ) )
27 1 2 3 10 vc0
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( 0 S A ) = ( GId ` G ) )
28 23 26 27 3eqtr3a
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( ( -u 1 S A ) G ( 1 S A ) ) = ( GId ` G ) )
29 19 28 eqtr3d
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( ( -u 1 S A ) G A ) = ( GId ` G ) )
30 29 oveq1d
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( ( ( -u 1 S A ) G A ) G ( M ` A ) ) = ( ( GId ` G ) G ( M ` A ) ) )
31 17 30 eqtr3d
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( ( -u 1 S A ) G ( A G ( M ` A ) ) ) = ( ( GId ` G ) G ( M ` A ) ) )
32 3 10 4 grporinv
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( A G ( M ` A ) ) = ( GId ` G ) )
33 5 32 sylan
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( A G ( M ` A ) ) = ( GId ` G ) )
34 33 oveq2d
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( ( -u 1 S A ) G ( A G ( M ` A ) ) ) = ( ( -u 1 S A ) G ( GId ` G ) ) )
35 31 34 eqtr3d
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( ( GId ` G ) G ( M ` A ) ) = ( ( -u 1 S A ) G ( GId ` G ) ) )
36 3 10 grpolid
 |-  ( ( G e. GrpOp /\ ( M ` A ) e. X ) -> ( ( GId ` G ) G ( M ` A ) ) = ( M ` A ) )
37 6 15 36 syl2anc
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( ( GId ` G ) G ( M ` A ) ) = ( M ` A ) )
38 35 37 eqtr3d
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( ( -u 1 S A ) G ( GId ` G ) ) = ( M ` A ) )
39 12 38 eqtr3d
 |-  ( ( W e. CVecOLD /\ A e. X ) -> ( -u 1 S A ) = ( M ` A ) )