| Step |
Hyp |
Ref |
Expression |
| 1 |
|
psgneldm.g |
|- G = ( SymGrp ` D ) |
| 2 |
|
psgneldm.n |
|- N = ( pmSgn ` D ) |
| 3 |
|
psgneldm.b |
|- B = ( Base ` G ) |
| 4 |
|
difeq1 |
|- ( p = P -> ( p \ _I ) = ( P \ _I ) ) |
| 5 |
4
|
dmeqd |
|- ( p = P -> dom ( p \ _I ) = dom ( P \ _I ) ) |
| 6 |
5
|
eleq1d |
|- ( p = P -> ( dom ( p \ _I ) e. Fin <-> dom ( P \ _I ) e. Fin ) ) |
| 7 |
|
eqid |
|- { p e. B | dom ( p \ _I ) e. Fin } = { p e. B | dom ( p \ _I ) e. Fin } |
| 8 |
1 3 7 2
|
psgnfn |
|- N Fn { p e. B | dom ( p \ _I ) e. Fin } |
| 9 |
8
|
fndmi |
|- dom N = { p e. B | dom ( p \ _I ) e. Fin } |
| 10 |
6 9
|
elrab2 |
|- ( P e. dom N <-> ( P e. B /\ dom ( P \ _I ) e. Fin ) ) |