Metamath Proof Explorer


Theorem psgnfn

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 𝐹

Proof

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 𝐹