Step |
Hyp |
Ref |
Expression |
0 |
|
cpsgn |
|- pmSgn |
1 |
|
vd |
|- d |
2 |
|
cvv |
|- _V |
3 |
|
vx |
|- x |
4 |
|
vp |
|- p |
5 |
|
cbs |
|- Base |
6 |
|
csymg |
|- SymGrp |
7 |
1
|
cv |
|- d |
8 |
7 6
|
cfv |
|- ( SymGrp ` d ) |
9 |
8 5
|
cfv |
|- ( Base ` ( SymGrp ` d ) ) |
10 |
4
|
cv |
|- p |
11 |
|
cid |
|- _I |
12 |
10 11
|
cdif |
|- ( p \ _I ) |
13 |
12
|
cdm |
|- dom ( p \ _I ) |
14 |
|
cfn |
|- Fin |
15 |
13 14
|
wcel |
|- dom ( p \ _I ) e. Fin |
16 |
15 4 9
|
crab |
|- { p e. ( Base ` ( SymGrp ` d ) ) | dom ( p \ _I ) e. Fin } |
17 |
|
vs |
|- s |
18 |
|
vw |
|- w |
19 |
|
cpmtr |
|- pmTrsp |
20 |
7 19
|
cfv |
|- ( pmTrsp ` d ) |
21 |
20
|
crn |
|- ran ( pmTrsp ` d ) |
22 |
21
|
cword |
|- Word ran ( pmTrsp ` d ) |
23 |
3
|
cv |
|- x |
24 |
|
cgsu |
|- gsum |
25 |
18
|
cv |
|- w |
26 |
8 25 24
|
co |
|- ( ( SymGrp ` d ) gsum w ) |
27 |
23 26
|
wceq |
|- x = ( ( SymGrp ` d ) gsum w ) |
28 |
17
|
cv |
|- s |
29 |
|
c1 |
|- 1 |
30 |
29
|
cneg |
|- -u 1 |
31 |
|
cexp |
|- ^ |
32 |
|
chash |
|- # |
33 |
25 32
|
cfv |
|- ( # ` w ) |
34 |
30 33 31
|
co |
|- ( -u 1 ^ ( # ` w ) ) |
35 |
28 34
|
wceq |
|- s = ( -u 1 ^ ( # ` w ) ) |
36 |
27 35
|
wa |
|- ( x = ( ( SymGrp ` d ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) |
37 |
36 18 22
|
wrex |
|- E. w e. Word ran ( pmTrsp ` d ) ( x = ( ( SymGrp ` d ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) |
38 |
37 17
|
cio |
|- ( iota s E. w e. Word ran ( pmTrsp ` d ) ( x = ( ( SymGrp ` d ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) |
39 |
3 16 38
|
cmpt |
|- ( x e. { p e. ( Base ` ( SymGrp ` d ) ) | dom ( p \ _I ) e. Fin } |-> ( iota s E. w e. Word ran ( pmTrsp ` d ) ( x = ( ( SymGrp ` d ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) ) |
40 |
1 2 39
|
cmpt |
|- ( d e. _V |-> ( x e. { p e. ( Base ` ( SymGrp ` d ) ) | dom ( p \ _I ) e. Fin } |-> ( iota s E. w e. Word ran ( pmTrsp ` d ) ( x = ( ( SymGrp ` d ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) ) ) |
41 |
0 40
|
wceq |
|- pmSgn = ( d e. _V |-> ( x e. { p e. ( Base ` ( SymGrp ` d ) ) | dom ( p \ _I ) e. Fin } |-> ( iota s E. w e. Word ran ( pmTrsp ` d ) ( x = ( ( SymGrp ` d ) gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) ) ) |