This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ G = SymGrp ⁡ D
psgnfn.b ⊢ B = Base G
psgnfn.f ⊢ F = p ∈ B | dom ⁡ p ∖ I ∈ Fin
psgnfn.n ⊢ N = pmSgn ⁡ D
Assertion psgnfn ⊢ N Fn F

Proof

Step Hyp Ref Expression
1 psgnfn.g ⊢ G = SymGrp ⁡ D
2 psgnfn.b ⊢ B = Base G
3 psgnfn.f ⊢ F = p ∈ B | dom ⁡ p ∖ I ∈ Fin
4 psgnfn.n ⊢ N = pmSgn ⁡ D
5 iotaex ⊢ ι s | ∃ w ∈ Word ran ⁡ pmTrsp ⁡ D x = ∑ G w ∧ s = − 1 w ∈ V
6 eqid ⊢ ran ⁡ pmTrsp ⁡ D = ran ⁡ pmTrsp ⁡ D
7 1 2 3 6 4 psgnfval ⊢ N = x ∈ F ⟼ ι s | ∃ w ∈ Word ran ⁡ pmTrsp ⁡ D x = ∑ G w ∧ s = − 1 w
8 5 7 fnmpti ⊢ N Fn F