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