Metamath Proof Explorer

Theorem psgnfvalfi

Description: Function definition of the permutation sign function for permutations of finite sets. (Contributed by AV, 13-Jan-2019)

Ref Expression
Hypotheses psgnfvalfi.g ⊢ G = SymGrp ⁡ D
psgnfvalfi.b ⊢ B = Base G
psgnfvalfi.t ⊢ T = ran ⁡ pmTrsp ⁡ D
psgnfvalfi.n ⊢ N = pmSgn ⁡ D
Assertion psgnfvalfi ⊢ D ∈ Fin → N = x ∈ B ⟼ ι s | ∃ w ∈ Word T x = ∑ G w ∧ s = − 1 w

Proof

Step Hyp Ref Expression
1 psgnfvalfi.g ⊢ G = SymGrp ⁡ D
2 psgnfvalfi.b ⊢ B = Base G
3 psgnfvalfi.t ⊢ T = ran ⁡ pmTrsp ⁡ D
4 psgnfvalfi.n ⊢ N = pmSgn ⁡ D
5 eqid ⊢ p ∈ B | dom ⁡ p ∖ I ∈ Fin = p ∈ B | dom ⁡ p ∖ I ∈ Fin
6 1 2 5 3 4 psgnfval ⊢ N = x ∈ p ∈ B | dom ⁡ p ∖ I ∈ Fin ⟼ ι s | ∃ w ∈ Word T x = ∑ G w ∧ s = − 1 w
7 1 2 sygbasnfpfi ⊢ D ∈ Fin ∧ p ∈ B → dom ⁡ p ∖ I ∈ Fin
8 7 ralrimiva ⊢ D ∈ Fin → ∀ p ∈ B dom ⁡ p ∖ I ∈ Fin
9 rabid2 ⊢ B = p ∈ B | dom ⁡ p ∖ I ∈ Fin ↔ ∀ p ∈ B dom ⁡ p ∖ I ∈ Fin
10 8 9 sylibr ⊢ D ∈ Fin → B = p ∈ B | dom ⁡ p ∖ I ∈ Fin
11 10 eqcomd ⊢ D ∈ Fin → p ∈ B | dom ⁡ p ∖ I ∈ Fin = B
12 11 mpteq1d ⊢ D ∈ Fin → x ∈ p ∈ B | dom ⁡ p ∖ I ∈ Fin ⟼ ι s | ∃ w ∈ Word T x = ∑ G w ∧ s = − 1 w = x ∈ B ⟼ ι s | ∃ w ∈ Word T x = ∑ G w ∧ s = − 1 w
13 6 12 syl5eq ⊢ D ∈ Fin → N = x ∈ B ⟼ ι s | ∃ w ∈ Word T x = ∑ G w ∧ s = − 1 w