Metamath Proof Explorer


Theorem psgnprfval

Description: The permutation sign function for a pair. (Contributed by AV, 10-Dec-2018)

Ref Expression
Hypotheses psgnprfval.0 D = 1 2
psgnprfval.g G = SymGrp D
psgnprfval.b B = Base G
psgnprfval.t T = ran pmTrsp D
psgnprfval.n N = pmSgn D
Assertion psgnprfval X B N X = ι s | w Word T X = G w s = 1 w

Proof

Step Hyp Ref Expression
1 psgnprfval.0 D = 1 2
2 psgnprfval.g G = SymGrp D
3 psgnprfval.b B = Base G
4 psgnprfval.t T = ran pmTrsp D
5 psgnprfval.n N = pmSgn D
6 id X B X B
7 elpri X 1 1 2 2 1 2 2 1 X = 1 1 2 2 X = 1 2 2 1
8 prfi 1 1 2 2 Fin
9 eleq1 X = 1 1 2 2 X Fin 1 1 2 2 Fin
10 8 9 mpbiri X = 1 1 2 2 X Fin
11 prfi 1 2 2 1 Fin
12 eleq1 X = 1 2 2 1 X Fin 1 2 2 1 Fin
13 11 12 mpbiri X = 1 2 2 1 X Fin
14 10 13 jaoi X = 1 1 2 2 X = 1 2 2 1 X Fin
15 diffi X Fin X I Fin
16 14 15 syl X = 1 1 2 2 X = 1 2 2 1 X I Fin
17 dmfi X I Fin dom X I Fin
18 7 16 17 3syl X 1 1 2 2 1 2 2 1 dom X I Fin
19 1ex 1 V
20 2nn 2
21 2 3 1 symg2bas 1 V 2 B = 1 1 2 2 1 2 2 1
22 19 20 21 mp2an B = 1 1 2 2 1 2 2 1
23 18 22 eleq2s X B dom X I Fin
24 2 5 3 psgneldm X dom N X B dom X I Fin
25 6 23 24 sylanbrc X B X dom N
26 2 4 5 psgnval X dom N N X = ι s | w Word T X = G w s = 1 w
27 25 26 syl X B N X = ι s | w Word T X = G w s = 1 w
28 6 27 syl X B N X = ι s | w Word T X = G w s = 1 w