| Step |
Hyp |
Ref |
Expression |
| 1 |
|
psgninv.s |
|- S = ( SymGrp ` D ) |
| 2 |
|
psgninv.n |
|- N = ( pmSgn ` D ) |
| 3 |
|
psgninv.p |
|- P = ( Base ` S ) |
| 4 |
|
eqid |
|- ( +g ` S ) = ( +g ` S ) |
| 5 |
1 3 4
|
symgov |
|- ( ( F e. P /\ G e. P ) -> ( F ( +g ` S ) G ) = ( F o. G ) ) |
| 6 |
5
|
3adant1 |
|- ( ( D e. Fin /\ F e. P /\ G e. P ) -> ( F ( +g ` S ) G ) = ( F o. G ) ) |
| 7 |
6
|
fveq2d |
|- ( ( D e. Fin /\ F e. P /\ G e. P ) -> ( N ` ( F ( +g ` S ) G ) ) = ( N ` ( F o. G ) ) ) |
| 8 |
|
eqid |
|- ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) |
| 9 |
1 2 8
|
psgnghm2 |
|- ( D e. Fin -> N e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) ) |
| 10 |
|
prex |
|- { 1 , -u 1 } e. _V |
| 11 |
|
eqid |
|- ( mulGrp ` CCfld ) = ( mulGrp ` CCfld ) |
| 12 |
|
cnfldmul |
|- x. = ( .r ` CCfld ) |
| 13 |
11 12
|
mgpplusg |
|- x. = ( +g ` ( mulGrp ` CCfld ) ) |
| 14 |
8 13
|
ressplusg |
|- ( { 1 , -u 1 } e. _V -> x. = ( +g ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) ) |
| 15 |
10 14
|
ax-mp |
|- x. = ( +g ` ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) |
| 16 |
3 4 15
|
ghmlin |
|- ( ( N e. ( S GrpHom ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } ) ) /\ F e. P /\ G e. P ) -> ( N ` ( F ( +g ` S ) G ) ) = ( ( N ` F ) x. ( N ` G ) ) ) |
| 17 |
9 16
|
syl3an1 |
|- ( ( D e. Fin /\ F e. P /\ G e. P ) -> ( N ` ( F ( +g ` S ) G ) ) = ( ( N ` F ) x. ( N ` G ) ) ) |
| 18 |
7 17
|
eqtr3d |
|- ( ( D e. Fin /\ F e. P /\ G e. P ) -> ( N ` ( F o. G ) ) = ( ( N ` F ) x. ( N ` G ) ) ) |