Description: Functionality and domain of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | psgnfn.g | ⊢ 𝐺 = ( SymGrp ‘ 𝐷 ) | |
psgnfn.b | ⊢ 𝐵 = ( Base ‘ 𝐺 ) | ||
psgnfn.f | ⊢ 𝐹 = { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } | ||
psgnfn.n | ⊢ 𝑁 = ( pmSgn ‘ 𝐷 ) | ||
Assertion | psgnfn | ⊢ 𝑁 Fn 𝐹 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | psgnfn.g | ⊢ 𝐺 = ( SymGrp ‘ 𝐷 ) | |
2 | psgnfn.b | ⊢ 𝐵 = ( Base ‘ 𝐺 ) | |
3 | psgnfn.f | ⊢ 𝐹 = { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } | |
4 | psgnfn.n | ⊢ 𝑁 = ( pmSgn ‘ 𝐷 ) | |
5 | iotaex | ⊢ ( ℩ 𝑠 ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ∈ V | |
6 | eqid | ⊢ ran ( pmTrsp ‘ 𝐷 ) = ran ( pmTrsp ‘ 𝐷 ) | |
7 | 1 2 3 6 4 | psgnfval | ⊢ 𝑁 = ( 𝑥 ∈ 𝐹 ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ) |
8 | 5 7 | fnmpti | ⊢ 𝑁 Fn 𝐹 |