Step | Hyp | Ref
| Expression |
1 | | simpll 790 |
. . . 4
pmEven
pmEven |
2 | | evpmodpmf1o.s |
. . . . . . 7
|
3 | 2 | symggrp 17820 |
. . . . . 6
|
4 | 3 | ad2antrr 762 |
. . . . 5
pmEven
pmEven |
5 | | eldifi 3732 |
. . . . . 6
pmEven
|
6 | 5 | ad2antlr 763 |
. . . . 5
pmEven
pmEven |
7 | | evpmodpmf1o.p |
. . . . . . . 8
|
8 | 2, 7 | evpmss 19932 |
. . . . . . 7
pmEven |
9 | 8 | sseli 3599 |
. . . . . 6
pmEven
|
10 | 9 | adantl 482 |
. . . . 5
pmEven
pmEven |
11 | | eqid 2622 |
. . . . . 6
|
12 | 7, 11 | grpcl 17430 |
. . . . 5
|
13 | 4, 6, 10, 12 | syl3anc 1326 |
. . . 4
pmEven
pmEven |
14 | | eqid 2622 |
. . . . . . . 8
pmSgn pmSgn |
15 | | eqid 2622 |
. . . . . . . 8
mulGrpℂfld ↾s mulGrpℂfld
↾s |
16 | 2, 14, 15 | psgnghm2 19927 |
. . . . . . 7
pmSgn mulGrpℂfld ↾s |
17 | 16 | ad2antrr 762 |
. . . . . 6
pmEven
pmEven pmSgn mulGrpℂfld ↾s |
18 | | prex 4909 |
. . . . . . . 8
|
19 | | eqid 2622 |
. . . . . . . . . 10
mulGrpℂfld mulGrpℂfld |
20 | | cnfldmul 19752 |
. . . . . . . . . 10
ℂfld |
21 | 19, 20 | mgpplusg 18493 |
. . . . . . . . 9
mulGrpℂfld |
22 | 15, 21 | ressplusg 15993 |
. . . . . . . 8
mulGrpℂfld
↾s |
23 | 18, 22 | ax-mp 5 |
. . . . . . 7
mulGrpℂfld ↾s |
24 | 7, 11, 23 | ghmlin 17665 |
. . . . . 6
pmSgn mulGrpℂfld ↾s
pmSgn pmSgn pmSgn |
25 | 17, 6, 10, 24 | syl3anc 1326 |
. . . . 5
pmEven
pmEven pmSgn pmSgn pmSgn |
26 | 2, 7, 14 | psgnodpm 19934 |
. . . . . . . 8
pmEven pmSgn |
27 | 26 | adantr 481 |
. . . . . . 7
pmEven
pmEven pmSgn |
28 | 2, 7, 14 | psgnevpm 19935 |
. . . . . . . 8
pmEven pmSgn |
29 | 28 | adantlr 751 |
. . . . . . 7
pmEven
pmEven pmSgn |
30 | 27, 29 | oveq12d 6668 |
. . . . . 6
pmEven
pmEven pmSgn pmSgn |
31 | | ax-1cn 9994 |
. . . . . . 7
|
32 | 31 | mulm1i 10475 |
. . . . . 6
|
33 | 30, 32 | syl6eq 2672 |
. . . . 5
pmEven
pmEven pmSgn pmSgn |
34 | 25, 33 | eqtrd 2656 |
. . . 4
pmEven
pmEven pmSgn |
35 | 2, 7, 14 | psgnodpmr 19936 |
. . . 4
pmSgn pmEven |
36 | 1, 13, 34, 35 | syl3anc 1326 |
. . 3
pmEven
pmEven pmEven |
37 | | eqid 2622 |
. . 3
pmEven pmEven |
38 | 36, 37 | fmptd 6385 |
. 2
pmEven pmEven pmEven pmEven |
39 | 3 | ad2antrr 762 |
. . . . 5
pmEven
pmEven |
40 | | eqid 2622 |
. . . . . . . 8
|
41 | 7, 40 | grpinvcl 17467 |
. . . . . . 7
|
42 | 3, 5, 41 | syl2an 494 |
. . . . . 6
pmEven |
43 | 42 | adantr 481 |
. . . . 5
pmEven
pmEven |
44 | | eldifi 3732 |
. . . . . 6
pmEven
|
45 | 44 | adantl 482 |
. . . . 5
pmEven
pmEven |
46 | 7, 11 | grpcl 17430 |
. . . . 5
|
47 | 39, 43, 45, 46 | syl3anc 1326 |
. . . 4
pmEven
pmEven |
48 | 16 | ad2antrr 762 |
. . . . . 6
pmEven
pmEven pmSgn mulGrpℂfld ↾s |
49 | 7, 11, 23 | ghmlin 17665 |
. . . . . 6
pmSgn mulGrpℂfld ↾s pmSgn pmSgn pmSgn |
50 | 48, 43, 45, 49 | syl3anc 1326 |
. . . . 5
pmEven
pmEven pmSgn pmSgn pmSgn |
51 | 2, 7, 40 | symginv 17822 |
. . . . . . . . 9
|
52 | 5, 51 | syl 17 |
. . . . . . . 8
pmEven
|
53 | 52 | ad2antlr 763 |
. . . . . . 7
pmEven
pmEven |
54 | 53 | fveq2d 6195 |
. . . . . 6
pmEven
pmEven pmSgn pmSgn |
55 | 2, 7, 14 | psgnodpm 19934 |
. . . . . . 7
pmEven pmSgn |
56 | 55 | adantlr 751 |
. . . . . 6
pmEven
pmEven pmSgn |
57 | 54, 56 | oveq12d 6668 |
. . . . 5
pmEven
pmEven pmSgn pmSgn pmSgn |
58 | | simpll 790 |
. . . . . . . . 9
pmEven
pmEven |
59 | 5 | ad2antlr 763 |
. . . . . . . . 9
pmEven
pmEven |
60 | 2, 14, 7 | psgninv 19928 |
. . . . . . . . 9
pmSgn pmSgn |
61 | 58, 59, 60 | syl2anc 693 |
. . . . . . . 8
pmEven
pmEven pmSgn pmSgn |
62 | 26 | adantr 481 |
. . . . . . . 8
pmEven
pmEven pmSgn |
63 | 61, 62 | eqtrd 2656 |
. . . . . . 7
pmEven
pmEven pmSgn |
64 | 63 | oveq1d 6665 |
. . . . . 6
pmEven
pmEven pmSgn |
65 | | neg1mulneg1e1 11245 |
. . . . . 6
|
66 | 64, 65 | syl6eq 2672 |
. . . . 5
pmEven
pmEven pmSgn |
67 | 50, 57, 66 | 3eqtrd 2660 |
. . . 4
pmEven
pmEven pmSgn |
68 | 2, 7, 14 | psgnevpmb 19933 |
. . . . 5
pmEven
pmSgn |
69 | 68 | ad2antrr 762 |
. . . 4
pmEven
pmEven pmEven
pmSgn |
70 | 47, 67, 69 | mpbir2and 957 |
. . 3
pmEven
pmEven pmEven |
71 | | eqid 2622 |
. . 3
pmEven
pmEven |
72 | 70, 71 | fmptd 6385 |
. 2
pmEven pmEven pmEvenpmEven |
73 | | eqidd 2623 |
. . . . 5
pmEven pmEven pmEven |
74 | | eqidd 2623 |
. . . . 5
pmEven pmEven pmEven |
75 | | oveq2 6658 |
. . . . 5
|
76 | 36, 73, 74, 75 | fmptco 6396 |
. . . 4
pmEven pmEven pmEven pmEven |
77 | | eqid 2622 |
. . . . . . . . 9
|
78 | 7, 11, 77, 40 | grplinv 17468 |
. . . . . . . 8
|
79 | 4, 6, 78 | syl2anc 693 |
. . . . . . 7
pmEven
pmEven |
80 | 79 | oveq1d 6665 |
. . . . . 6
pmEven
pmEven |
81 | 42 | adantr 481 |
. . . . . . 7
pmEven
pmEven |
82 | 7, 11 | grpass 17431 |
. . . . . . 7
|
83 | 4, 81, 6, 10, 82 | syl13anc 1328 |
. . . . . 6
pmEven
pmEven
|
84 | 7, 11, 77 | grplid 17452 |
. . . . . . 7
|
85 | 4, 10, 84 | syl2anc 693 |
. . . . . 6
pmEven
pmEven |
86 | 80, 83, 85 | 3eqtr3d 2664 |
. . . . 5
pmEven
pmEven |
87 | 86 | mpteq2dva 4744 |
. . . 4
pmEven pmEven pmEven |
88 | 76, 87 | eqtrd 2656 |
. . 3
pmEven pmEven pmEven pmEven |
89 | | mptresid 5456 |
. . 3
pmEven pmEven |
90 | 88, 89 | syl6eq 2672 |
. 2
pmEven pmEven pmEven
pmEven |
91 | | oveq2 6658 |
. . . . 5
|
92 | 70, 74, 73, 91 | fmptco 6396 |
. . . 4
pmEven pmEven pmEven pmEven |
93 | 7, 11, 77, 40 | grprinv 17469 |
. . . . . . . . 9
|
94 | 3, 5, 93 | syl2an 494 |
. . . . . . . 8
pmEven |
95 | 94 | oveq1d 6665 |
. . . . . . 7
pmEven |
96 | 95 | adantr 481 |
. . . . . 6
pmEven
pmEven |
97 | 7, 11 | grpass 17431 |
. . . . . . 7
|
98 | 39, 59, 43, 45, 97 | syl13anc 1328 |
. . . . . 6
pmEven
pmEven |
99 | 7, 11, 77 | grplid 17452 |
. . . . . . 7
|
100 | 39, 45, 99 | syl2anc 693 |
. . . . . 6
pmEven
pmEven |
101 | 96, 98, 100 | 3eqtr3d 2664 |
. . . . 5
pmEven
pmEven
|
102 | 101 | mpteq2dva 4744 |
. . . 4
pmEven pmEven
pmEven |
103 | 92, 102 | eqtrd 2656 |
. . 3
pmEven pmEven pmEven pmEven |
104 | | mptresid 5456 |
. . 3
pmEven pmEven |
105 | 103, 104 | syl6eq 2672 |
. 2
pmEven pmEven pmEven pmEven |
106 | 38, 72, 90, 105 | fcof1od 6549 |
1
pmEven pmEven pmEven
pmEven |