| Step |
Hyp |
Ref |
Expression |
| 1 |
|
evpmss.s |
|- S = ( SymGrp ` D ) |
| 2 |
|
evpmss.p |
|- P = ( Base ` S ) |
| 3 |
|
psgnevpmb.n |
|- N = ( pmSgn ` D ) |
| 4 |
|
elex |
|- ( D e. Fin -> D e. _V ) |
| 5 |
|
fveq2 |
|- ( d = D -> ( pmSgn ` d ) = ( pmSgn ` D ) ) |
| 6 |
5 3
|
eqtr4di |
|- ( d = D -> ( pmSgn ` d ) = N ) |
| 7 |
6
|
cnveqd |
|- ( d = D -> `' ( pmSgn ` d ) = `' N ) |
| 8 |
7
|
imaeq1d |
|- ( d = D -> ( `' ( pmSgn ` d ) " { 1 } ) = ( `' N " { 1 } ) ) |
| 9 |
|
df-evpm |
|- pmEven = ( d e. _V |-> ( `' ( pmSgn ` d ) " { 1 } ) ) |
| 10 |
3
|
fvexi |
|- N e. _V |
| 11 |
10
|
cnvex |
|- `' N e. _V |
| 12 |
11
|
imaex |
|- ( `' N " { 1 } ) e. _V |
| 13 |
8 9 12
|
fvmpt |
|- ( D e. _V -> ( pmEven ` D ) = ( `' N " { 1 } ) ) |
| 14 |
4 13
|
syl |
|- ( D e. Fin -> ( pmEven ` D ) = ( `' N " { 1 } ) ) |
| 15 |
14
|
eleq2d |
|- ( D e. Fin -> ( F e. ( pmEven ` D ) <-> F e. ( `' N " { 1 } ) ) ) |
| 16 |
|
eqid |
|- ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) |
| 17 |
1 3 16
|
psgnghm2 |
|- ( D e. Fin -> N e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) ) |
| 18 |
|
eqid |
|- ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) = ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) |
| 19 |
2 18
|
ghmf |
|- ( N e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) -> N : P --> ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) ) |
| 20 |
|
ffn |
|- ( N : P --> ( Base ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) -> N Fn P ) |
| 21 |
|
fniniseg |
|- ( N Fn P -> ( F e. ( `' N " { 1 } ) <-> ( F e. P /\ ( N ` F ) = 1 ) ) ) |
| 22 |
17 19 20 21
|
4syl |
|- ( D e. Fin -> ( F e. ( `' N " { 1 } ) <-> ( F e. P /\ ( N ` F ) = 1 ) ) ) |
| 23 |
15 22
|
bitrd |
|- ( D e. Fin -> ( F e. ( pmEven ` D ) <-> ( F e. P /\ ( N ` F ) = 1 ) ) ) |