| Step |
Hyp |
Ref |
Expression |
| 1 |
|
psgnval.g |
|- G = ( SymGrp ` D ) |
| 2 |
|
psgnval.t |
|- T = ran ( pmTrsp ` D ) |
| 3 |
|
psgnval.n |
|- N = ( pmSgn ` D ) |
| 4 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
| 5 |
|
eqid |
|- { p e. ( Base ` G ) | dom ( p \ _I ) e. Fin } = { p e. ( Base ` G ) | dom ( p \ _I ) e. Fin } |
| 6 |
1 4 5 3
|
psgnfn |
|- N Fn { p e. ( Base ` G ) | dom ( p \ _I ) e. Fin } |
| 7 |
6
|
fndmi |
|- dom N = { p e. ( Base ` G ) | dom ( p \ _I ) e. Fin } |
| 8 |
|
eqid |
|- ( mrCls ` ( SubMnd ` G ) ) = ( mrCls ` ( SubMnd ` G ) ) |
| 9 |
2 1 4 8
|
symggen |
|- ( D e. V -> ( ( mrCls ` ( SubMnd ` G ) ) ` T ) = { p e. ( Base ` G ) | dom ( p \ _I ) e. Fin } ) |
| 10 |
1
|
symggrp |
|- ( D e. V -> G e. Grp ) |
| 11 |
10
|
grpmndd |
|- ( D e. V -> G e. Mnd ) |
| 12 |
2 1 4
|
symgtrf |
|- T C_ ( Base ` G ) |
| 13 |
4 8
|
gsumwspan |
|- ( ( G e. Mnd /\ T C_ ( Base ` G ) ) -> ( ( mrCls ` ( SubMnd ` G ) ) ` T ) = ran ( w e. Word T |-> ( G gsum w ) ) ) |
| 14 |
11 12 13
|
sylancl |
|- ( D e. V -> ( ( mrCls ` ( SubMnd ` G ) ) ` T ) = ran ( w e. Word T |-> ( G gsum w ) ) ) |
| 15 |
9 14
|
eqtr3d |
|- ( D e. V -> { p e. ( Base ` G ) | dom ( p \ _I ) e. Fin } = ran ( w e. Word T |-> ( G gsum w ) ) ) |
| 16 |
7 15
|
eqtrid |
|- ( D e. V -> dom N = ran ( w e. Word T |-> ( G gsum w ) ) ) |
| 17 |
16
|
eleq2d |
|- ( D e. V -> ( P e. dom N <-> P e. ran ( w e. Word T |-> ( G gsum w ) ) ) ) |
| 18 |
|
eqid |
|- ( w e. Word T |-> ( G gsum w ) ) = ( w e. Word T |-> ( G gsum w ) ) |
| 19 |
|
ovex |
|- ( G gsum w ) e. _V |
| 20 |
18 19
|
elrnmpti |
|- ( P e. ran ( w e. Word T |-> ( G gsum w ) ) <-> E. w e. Word T P = ( G gsum w ) ) |
| 21 |
17 20
|
bitrdi |
|- ( D e. V -> ( P e. dom N <-> E. w e. Word T P = ( G gsum w ) ) ) |