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