Step |
Hyp |
Ref |
Expression |
0 |
|
cpsgn |
⊢ pmSgn |
1 |
|
vd |
⊢ 𝑑 |
2 |
|
cvv |
⊢ V |
3 |
|
vx |
⊢ 𝑥 |
4 |
|
vp |
⊢ 𝑝 |
5 |
|
cbs |
⊢ Base |
6 |
|
csymg |
⊢ SymGrp |
7 |
1
|
cv |
⊢ 𝑑 |
8 |
7 6
|
cfv |
⊢ ( SymGrp ‘ 𝑑 ) |
9 |
8 5
|
cfv |
⊢ ( Base ‘ ( SymGrp ‘ 𝑑 ) ) |
10 |
4
|
cv |
⊢ 𝑝 |
11 |
|
cid |
⊢ I |
12 |
10 11
|
cdif |
⊢ ( 𝑝 ∖ I ) |
13 |
12
|
cdm |
⊢ dom ( 𝑝 ∖ I ) |
14 |
|
cfn |
⊢ Fin |
15 |
13 14
|
wcel |
⊢ dom ( 𝑝 ∖ I ) ∈ Fin |
16 |
15 4 9
|
crab |
⊢ { 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑑 ) ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } |
17 |
|
vs |
⊢ 𝑠 |
18 |
|
vw |
⊢ 𝑤 |
19 |
|
cpmtr |
⊢ pmTrsp |
20 |
7 19
|
cfv |
⊢ ( pmTrsp ‘ 𝑑 ) |
21 |
20
|
crn |
⊢ ran ( pmTrsp ‘ 𝑑 ) |
22 |
21
|
cword |
⊢ Word ran ( pmTrsp ‘ 𝑑 ) |
23 |
3
|
cv |
⊢ 𝑥 |
24 |
|
cgsu |
⊢ Σg |
25 |
18
|
cv |
⊢ 𝑤 |
26 |
8 25 24
|
co |
⊢ ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) |
27 |
23 26
|
wceq |
⊢ 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) |
28 |
17
|
cv |
⊢ 𝑠 |
29 |
|
c1 |
⊢ 1 |
30 |
29
|
cneg |
⊢ - 1 |
31 |
|
cexp |
⊢ ↑ |
32 |
|
chash |
⊢ ♯ |
33 |
25 32
|
cfv |
⊢ ( ♯ ‘ 𝑤 ) |
34 |
30 33 31
|
co |
⊢ ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) |
35 |
28 34
|
wceq |
⊢ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) |
36 |
27 35
|
wa |
⊢ ( 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) |
37 |
36 18 22
|
wrex |
⊢ ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑑 ) ( 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) |
38 |
37 17
|
cio |
⊢ ( ℩ 𝑠 ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑑 ) ( 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) |
39 |
3 16 38
|
cmpt |
⊢ ( 𝑥 ∈ { 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑑 ) ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑑 ) ( 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) |
40 |
1 2 39
|
cmpt |
⊢ ( 𝑑 ∈ V ↦ ( 𝑥 ∈ { 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑑 ) ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑑 ) ( 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) ) |
41 |
0 40
|
wceq |
⊢ pmSgn = ( 𝑑 ∈ V ↦ ( 𝑥 ∈ { 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑑 ) ) ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝑑 ) ( 𝑥 = ( ( SymGrp ‘ 𝑑 ) Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) ) |