Step | Hyp | Ref
| Expression |
1 | | vcm.1 |
. . . . 5
β’ πΊ = (1st βπ) |
2 | 1 | vcgrp 29554 |
. . . 4
β’ (π β CVecOLD
β πΊ β
GrpOp) |
3 | 2 | adantr 482 |
. . 3
β’ ((π β CVecOLD β§
π΄ β π) β πΊ β GrpOp) |
4 | | neg1cn 12272 |
. . . 4
β’ -1 β
β |
5 | | vcm.2 |
. . . . 5
β’ π = (2nd βπ) |
6 | | vcm.3 |
. . . . 5
β’ π = ran πΊ |
7 | 1, 5, 6 | vccl 29547 |
. . . 4
β’ ((π β CVecOLD β§
-1 β β β§ π΄
β π) β (-1ππ΄) β π) |
8 | 4, 7 | mp3an2 1450 |
. . 3
β’ ((π β CVecOLD β§
π΄ β π) β (-1ππ΄) β π) |
9 | | eqid 2733 |
. . . 4
β’
(GIdβπΊ) =
(GIdβπΊ) |
10 | 6, 9 | grporid 29501 |
. . 3
β’ ((πΊ β GrpOp β§ (-1ππ΄) β π) β ((-1ππ΄)πΊ(GIdβπΊ)) = (-1ππ΄)) |
11 | 3, 8, 10 | syl2anc 585 |
. 2
β’ ((π β CVecOLD β§
π΄ β π) β ((-1ππ΄)πΊ(GIdβπΊ)) = (-1ππ΄)) |
12 | | simpr 486 |
. . . . . 6
β’ ((π β CVecOLD β§
π΄ β π) β π΄ β π) |
13 | | vcm.4 |
. . . . . . . 8
β’ π = (invβπΊ) |
14 | 6, 13 | grpoinvcl 29508 |
. . . . . . 7
β’ ((πΊ β GrpOp β§ π΄ β π) β (πβπ΄) β π) |
15 | 2, 14 | sylan 581 |
. . . . . 6
β’ ((π β CVecOLD β§
π΄ β π) β (πβπ΄) β π) |
16 | 6 | grpoass 29487 |
. . . . . 6
β’ ((πΊ β GrpOp β§ ((-1ππ΄) β π β§ π΄ β π β§ (πβπ΄) β π)) β (((-1ππ΄)πΊπ΄)πΊ(πβπ΄)) = ((-1ππ΄)πΊ(π΄πΊ(πβπ΄)))) |
17 | 3, 8, 12, 15, 16 | syl13anc 1373 |
. . . . 5
β’ ((π β CVecOLD β§
π΄ β π) β (((-1ππ΄)πΊπ΄)πΊ(πβπ΄)) = ((-1ππ΄)πΊ(π΄πΊ(πβπ΄)))) |
18 | 1, 5, 6 | vcidOLD 29548 |
. . . . . . . 8
β’ ((π β CVecOLD β§
π΄ β π) β (1ππ΄) = π΄) |
19 | 18 | oveq2d 7374 |
. . . . . . 7
β’ ((π β CVecOLD β§
π΄ β π) β ((-1ππ΄)πΊ(1ππ΄)) = ((-1ππ΄)πΊπ΄)) |
20 | | ax-1cn 11114 |
. . . . . . . . . 10
β’ 1 β
β |
21 | | 1pneg1e0 12277 |
. . . . . . . . . 10
β’ (1 + -1)
= 0 |
22 | 20, 4, 21 | addcomli 11352 |
. . . . . . . . 9
β’ (-1 + 1)
= 0 |
23 | 22 | oveq1i 7368 |
. . . . . . . 8
β’ ((-1 +
1)ππ΄) = (0ππ΄) |
24 | 1, 5, 6 | vcdir 29550 |
. . . . . . . . . 10
β’ ((π β CVecOLD β§
(-1 β β β§ 1 β β β§ π΄ β π)) β ((-1 + 1)ππ΄) = ((-1ππ΄)πΊ(1ππ΄))) |
25 | 4, 24 | mp3anr1 1459 |
. . . . . . . . 9
β’ ((π β CVecOLD β§
(1 β β β§ π΄
β π)) β ((-1 +
1)ππ΄) = ((-1ππ΄)πΊ(1ππ΄))) |
26 | 20, 25 | mpanr1 702 |
. . . . . . . 8
β’ ((π β CVecOLD β§
π΄ β π) β ((-1 + 1)ππ΄) = ((-1ππ΄)πΊ(1ππ΄))) |
27 | 1, 5, 6, 9 | vc0 29558 |
. . . . . . . 8
β’ ((π β CVecOLD β§
π΄ β π) β (0ππ΄) = (GIdβπΊ)) |
28 | 23, 26, 27 | 3eqtr3a 2797 |
. . . . . . 7
β’ ((π β CVecOLD β§
π΄ β π) β ((-1ππ΄)πΊ(1ππ΄)) = (GIdβπΊ)) |
29 | 19, 28 | eqtr3d 2775 |
. . . . . 6
β’ ((π β CVecOLD β§
π΄ β π) β ((-1ππ΄)πΊπ΄) = (GIdβπΊ)) |
30 | 29 | oveq1d 7373 |
. . . . 5
β’ ((π β CVecOLD β§
π΄ β π) β (((-1ππ΄)πΊπ΄)πΊ(πβπ΄)) = ((GIdβπΊ)πΊ(πβπ΄))) |
31 | 17, 30 | eqtr3d 2775 |
. . . 4
β’ ((π β CVecOLD β§
π΄ β π) β ((-1ππ΄)πΊ(π΄πΊ(πβπ΄))) = ((GIdβπΊ)πΊ(πβπ΄))) |
32 | 6, 9, 13 | grporinv 29511 |
. . . . . 6
β’ ((πΊ β GrpOp β§ π΄ β π) β (π΄πΊ(πβπ΄)) = (GIdβπΊ)) |
33 | 2, 32 | sylan 581 |
. . . . 5
β’ ((π β CVecOLD β§
π΄ β π) β (π΄πΊ(πβπ΄)) = (GIdβπΊ)) |
34 | 33 | oveq2d 7374 |
. . . 4
β’ ((π β CVecOLD β§
π΄ β π) β ((-1ππ΄)πΊ(π΄πΊ(πβπ΄))) = ((-1ππ΄)πΊ(GIdβπΊ))) |
35 | 31, 34 | eqtr3d 2775 |
. . 3
β’ ((π β CVecOLD β§
π΄ β π) β ((GIdβπΊ)πΊ(πβπ΄)) = ((-1ππ΄)πΊ(GIdβπΊ))) |
36 | 6, 9 | grpolid 29500 |
. . . 4
β’ ((πΊ β GrpOp β§ (πβπ΄) β π) β ((GIdβπΊ)πΊ(πβπ΄)) = (πβπ΄)) |
37 | 3, 15, 36 | syl2anc 585 |
. . 3
β’ ((π β CVecOLD β§
π΄ β π) β ((GIdβπΊ)πΊ(πβπ΄)) = (πβπ΄)) |
38 | 35, 37 | eqtr3d 2775 |
. 2
β’ ((π β CVecOLD β§
π΄ β π) β ((-1ππ΄)πΊ(GIdβπΊ)) = (πβπ΄)) |
39 | 11, 38 | eqtr3d 2775 |
1
β’ ((π β CVecOLD β§
π΄ β π) β (-1ππ΄) = (πβπ΄)) |