Step |
Hyp |
Ref |
Expression |
1 |
|
psgnval.g |
⊢ 𝐺 = ( SymGrp ‘ 𝐷 ) |
2 |
|
psgnval.t |
⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 ) |
3 |
|
psgnval.n |
⊢ 𝑁 = ( pmSgn ‘ 𝐷 ) |
4 |
1 2 3
|
psgnval |
⊢ ( 𝑃 ∈ dom 𝑁 → ( 𝑁 ‘ 𝑃 ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) |
5 |
1 2 3
|
psgneu |
⊢ ( 𝑃 ∈ dom 𝑁 → ∃! 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) |
6 |
|
iotacl |
⊢ ( ∃! 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) → ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ∈ { 𝑠 ∣ ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) } ) |
7 |
5 6
|
syl |
⊢ ( 𝑃 ∈ dom 𝑁 → ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ∈ { 𝑠 ∣ ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) } ) |
8 |
4 7
|
eqeltrd |
⊢ ( 𝑃 ∈ dom 𝑁 → ( 𝑁 ‘ 𝑃 ) ∈ { 𝑠 ∣ ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) } ) |
9 |
|
fvex |
⊢ ( 𝑁 ‘ 𝑃 ) ∈ V |
10 |
|
eqeq1 |
⊢ ( 𝑠 = ( 𝑁 ‘ 𝑃 ) → ( 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ↔ ( 𝑁 ‘ 𝑃 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) |
11 |
10
|
anbi2d |
⊢ ( 𝑠 = ( 𝑁 ‘ 𝑃 ) → ( ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑃 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) |
12 |
11
|
rexbidv |
⊢ ( 𝑠 = ( 𝑁 ‘ 𝑃 ) → ( ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑃 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) |
13 |
9 12
|
elab |
⊢ ( ( 𝑁 ‘ 𝑃 ) ∈ { 𝑠 ∣ ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) } ↔ ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑃 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) |
14 |
8 13
|
sylib |
⊢ ( 𝑃 ∈ dom 𝑁 → ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ ( 𝑁 ‘ 𝑃 ) = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) |