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