Step |
Hyp |
Ref |
Expression |
1 |
|
psgnval.g |
⊢ 𝐺 = ( SymGrp ‘ 𝐷 ) |
2 |
|
psgnval.t |
⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 ) |
3 |
|
psgnval.n |
⊢ 𝑁 = ( pmSgn ‘ 𝐷 ) |
4 |
|
eqeq1 |
⊢ ( 𝑡 = 𝑃 → ( 𝑡 = ( 𝐺 Σg 𝑤 ) ↔ 𝑃 = ( 𝐺 Σg 𝑤 ) ) ) |
5 |
4
|
anbi1d |
⊢ ( 𝑡 = 𝑃 → ( ( 𝑡 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) |
6 |
5
|
rexbidv |
⊢ ( 𝑡 = 𝑃 → ( ∃ 𝑤 ∈ Word 𝑇 ( 𝑡 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) |
7 |
6
|
iotabidv |
⊢ ( 𝑡 = 𝑃 → ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑡 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) |
8 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
9 |
|
eqid |
⊢ { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin } = { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin } |
10 |
1 8 9 3
|
psgnfn |
⊢ 𝑁 Fn { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin } |
11 |
10
|
fndmi |
⊢ dom 𝑁 = { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ dom ( 𝑥 ∖ I ) ∈ Fin } |
12 |
1 8 11 2 3
|
psgnfval |
⊢ 𝑁 = ( 𝑡 ∈ dom 𝑁 ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑡 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) |
13 |
|
iotaex |
⊢ ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ∈ V |
14 |
7 12 13
|
fvmpt |
⊢ ( 𝑃 ∈ dom 𝑁 → ( 𝑁 ‘ 𝑃 ) = ( ℩ 𝑠 ∃ 𝑤 ∈ Word 𝑇 ( 𝑃 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) |