Metamath Proof Explorer


Theorem psgneu

Description: A finitary permutation has exactly one parity. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypotheses psgnval.g G = SymGrp D
psgnval.t T = ran pmTrsp D
psgnval.n N = pmSgn D
Assertion psgneu P dom N ∃! s w Word T P = G w s = 1 w

Proof

Step Hyp Ref Expression
1 psgnval.g G = SymGrp D
2 psgnval.t T = ran pmTrsp D
3 psgnval.n N = pmSgn D
4 eqid Base G = Base G
5 1 3 4 psgneldm P dom N P Base G dom P I Fin
6 5 simplbi P dom N P Base G
7 1 4 elbasfv P Base G D V
8 6 7 syl P dom N D V
9 1 2 3 psgneldm2 D V P dom N w Word T P = G w
10 8 9 syl P dom N P dom N w Word T P = G w
11 10 ibi P dom N w Word T P = G w
12 simpr P dom N w Word T P = G w P = G w
13 eqid 1 w = 1 w
14 ovex 1 w V
15 eqeq1 s = 1 w s = 1 w 1 w = 1 w
16 15 anbi2d s = 1 w P = G w s = 1 w P = G w 1 w = 1 w
17 14 16 spcev P = G w 1 w = 1 w s P = G w s = 1 w
18 12 13 17 sylancl P dom N w Word T P = G w s P = G w s = 1 w
19 18 ex P dom N w Word T P = G w s P = G w s = 1 w
20 19 reximdva P dom N w Word T P = G w w Word T s P = G w s = 1 w
21 11 20 mpd P dom N w Word T s P = G w s = 1 w
22 rexcom4 w Word T s P = G w s = 1 w s w Word T P = G w s = 1 w
23 21 22 sylib P dom N s w Word T P = G w s = 1 w
24 reeanv w Word T x Word T P = G w s = 1 w P = G x t = 1 x w Word T P = G w s = 1 w x Word T P = G x t = 1 x
25 8 ad2antrr P dom N w Word T x Word T P = G w s = 1 w P = G x t = 1 x D V
26 simplrl P dom N w Word T x Word T P = G w s = 1 w P = G x t = 1 x w Word T
27 simplrr P dom N w Word T x Word T P = G w s = 1 w P = G x t = 1 x x Word T
28 simprll P dom N w Word T x Word T P = G w s = 1 w P = G x t = 1 x P = G w
29 simprrl P dom N w Word T x Word T P = G w s = 1 w P = G x t = 1 x P = G x
30 28 29 eqtr3d P dom N w Word T x Word T P = G w s = 1 w P = G x t = 1 x G w = G x
31 1 2 25 26 27 30 psgnuni P dom N w Word T x Word T P = G w s = 1 w P = G x t = 1 x 1 w = 1 x
32 simprlr P dom N w Word T x Word T P = G w s = 1 w P = G x t = 1 x s = 1 w
33 simprrr P dom N w Word T x Word T P = G w s = 1 w P = G x t = 1 x t = 1 x
34 31 32 33 3eqtr4d P dom N w Word T x Word T P = G w s = 1 w P = G x t = 1 x s = t
35 34 ex P dom N w Word T x Word T P = G w s = 1 w P = G x t = 1 x s = t
36 35 rexlimdvva P dom N w Word T x Word T P = G w s = 1 w P = G x t = 1 x s = t
37 24 36 syl5bir P dom N w Word T P = G w s = 1 w x Word T P = G x t = 1 x s = t
38 37 alrimivv P dom N s t w Word T P = G w s = 1 w x Word T P = G x t = 1 x s = t
39 eqeq1 s = t s = 1 w t = 1 w
40 39 anbi2d s = t P = G w s = 1 w P = G w t = 1 w
41 40 rexbidv s = t w Word T P = G w s = 1 w w Word T P = G w t = 1 w
42 oveq2 w = x G w = G x
43 42 eqeq2d w = x P = G w P = G x
44 fveq2 w = x w = x
45 44 oveq2d w = x 1 w = 1 x
46 45 eqeq2d w = x t = 1 w t = 1 x
47 43 46 anbi12d w = x P = G w t = 1 w P = G x t = 1 x
48 47 cbvrexvw w Word T P = G w t = 1 w x Word T P = G x t = 1 x
49 41 48 bitrdi s = t w Word T P = G w s = 1 w x Word T P = G x t = 1 x
50 49 eu4 ∃! s w Word T P = G w s = 1 w s w Word T P = G w s = 1 w s t w Word T P = G w s = 1 w x Word T P = G x t = 1 x s = t
51 23 38 50 sylanbrc P dom N ∃! s w Word T P = G w s = 1 w