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 e. dom N -> E! s E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 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 e. dom N <-> ( P e. ( Base ` G ) /\ dom ( P \ _I ) e. Fin ) )
6 5 simplbi 
 |-  ( P e. dom N -> P e. ( Base ` G ) )
7 1 4 elbasfv 
 |-  ( P e. ( Base ` G ) -> D e. _V )
8 6 7 syl 
 |-  ( P e. dom N -> D e. _V )
9 1 2 3 psgneldm2 
 |-  ( D e. _V -> ( P e. dom N <-> E. w e. Word T P = ( G gsum w ) ) )
10 8 9 syl 
 |-  ( P e. dom N -> ( P e. dom N <-> E. w e. Word T P = ( G gsum w ) ) )
11 10 ibi 
 |-  ( P e. dom N -> E. w e. Word T P = ( G gsum w ) )
12 simpr 
 |-  ( ( ( P e. dom N /\ w e. Word T ) /\ P = ( G gsum w ) ) -> P = ( G gsum w ) )
13 eqid 
 |-  ( -u 1 ^ ( # ` w ) ) = ( -u 1 ^ ( # ` w ) )
14 ovex 
 |-  ( -u 1 ^ ( # ` w ) ) e. _V
15 eqeq1 
 |-  ( s = ( -u 1 ^ ( # ` w ) ) -> ( s = ( -u 1 ^ ( # ` w ) ) <-> ( -u 1 ^ ( # ` w ) ) = ( -u 1 ^ ( # ` w ) ) ) )
16 15 anbi2d 
 |-  ( s = ( -u 1 ^ ( # ` w ) ) -> ( ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) <-> ( P = ( G gsum w ) /\ ( -u 1 ^ ( # ` w ) ) = ( -u 1 ^ ( # ` w ) ) ) ) )
17 14 16 spcev 
 |-  ( ( P = ( G gsum w ) /\ ( -u 1 ^ ( # ` w ) ) = ( -u 1 ^ ( # ` w ) ) ) -> E. s ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) )
18 12 13 17 sylancl 
 |-  ( ( ( P e. dom N /\ w e. Word T ) /\ P = ( G gsum w ) ) -> E. s ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) )
19 18 ex 
 |-  ( ( P e. dom N /\ w e. Word T ) -> ( P = ( G gsum w ) -> E. s ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
20 19 reximdva 
 |-  ( P e. dom N -> ( E. w e. Word T P = ( G gsum w ) -> E. w e. Word T E. s ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) ) )
21 11 20 mpd 
 |-  ( P e. dom N -> E. w e. Word T E. s ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) )
22 rexcom4 
 |-  ( E. w e. Word T E. s ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) <-> E. s E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) )
23 21 22 sylib 
 |-  ( P e. dom N -> E. s E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) )
24 reeanv 
 |-  ( E. w e. Word T E. x e. Word T ( ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) /\ ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) ) <-> ( E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) /\ E. x e. Word T ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) ) )
25 8 ad2antrr 
 |-  ( ( ( P e. dom N /\ ( w e. Word T /\ x e. Word T ) ) /\ ( ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) /\ ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) ) ) -> D e. _V )
26 simplrl 
 |-  ( ( ( P e. dom N /\ ( w e. Word T /\ x e. Word T ) ) /\ ( ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) /\ ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) ) ) -> w e. Word T )
27 simplrr 
 |-  ( ( ( P e. dom N /\ ( w e. Word T /\ x e. Word T ) ) /\ ( ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) /\ ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) ) ) -> x e. Word T )
28 simprll 
 |-  ( ( ( P e. dom N /\ ( w e. Word T /\ x e. Word T ) ) /\ ( ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) /\ ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) ) ) -> P = ( G gsum w ) )
29 simprrl 
 |-  ( ( ( P e. dom N /\ ( w e. Word T /\ x e. Word T ) ) /\ ( ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) /\ ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) ) ) -> P = ( G gsum x ) )
30 28 29 eqtr3d 
 |-  ( ( ( P e. dom N /\ ( w e. Word T /\ x e. Word T ) ) /\ ( ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) /\ ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) ) ) -> ( G gsum w ) = ( G gsum x ) )
31 1 2 25 26 27 30 psgnuni 
 |-  ( ( ( P e. dom N /\ ( w e. Word T /\ x e. Word T ) ) /\ ( ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) /\ ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) ) ) -> ( -u 1 ^ ( # ` w ) ) = ( -u 1 ^ ( # ` x ) ) )
32 simprlr 
 |-  ( ( ( P e. dom N /\ ( w e. Word T /\ x e. Word T ) ) /\ ( ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) /\ ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) ) ) -> s = ( -u 1 ^ ( # ` w ) ) )
33 simprrr 
 |-  ( ( ( P e. dom N /\ ( w e. Word T /\ x e. Word T ) ) /\ ( ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) /\ ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) ) ) -> t = ( -u 1 ^ ( # ` x ) ) )
34 31 32 33 3eqtr4d 
 |-  ( ( ( P e. dom N /\ ( w e. Word T /\ x e. Word T ) ) /\ ( ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) /\ ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) ) ) -> s = t )
35 34 ex 
 |-  ( ( P e. dom N /\ ( w e. Word T /\ x e. Word T ) ) -> ( ( ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) /\ ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) ) -> s = t ) )
36 35 rexlimdvva 
 |-  ( P e. dom N -> ( E. w e. Word T E. x e. Word T ( ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) /\ ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) ) -> s = t ) )
37 24 36 syl5bir 
 |-  ( P e. dom N -> ( ( E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) /\ E. x e. Word T ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) ) -> s = t ) )
38 37 alrimivv 
 |-  ( P e. dom N -> A. s A. t ( ( E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) /\ E. x e. Word T ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) ) -> s = t ) )
39 eqeq1 
 |-  ( s = t -> ( s = ( -u 1 ^ ( # ` w ) ) <-> t = ( -u 1 ^ ( # ` w ) ) ) )
40 39 anbi2d 
 |-  ( s = t -> ( ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) <-> ( P = ( G gsum w ) /\ t = ( -u 1 ^ ( # ` w ) ) ) ) )
41 40 rexbidv 
 |-  ( s = t -> ( E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) <-> E. w e. Word T ( P = ( G gsum w ) /\ t = ( -u 1 ^ ( # ` w ) ) ) ) )
42 oveq2 
 |-  ( w = x -> ( G gsum w ) = ( G gsum x ) )
43 42 eqeq2d 
 |-  ( w = x -> ( P = ( G gsum w ) <-> P = ( G gsum x ) ) )
44 fveq2 
 |-  ( w = x -> ( # ` w ) = ( # ` x ) )
45 44 oveq2d 
 |-  ( w = x -> ( -u 1 ^ ( # ` w ) ) = ( -u 1 ^ ( # ` x ) ) )
46 45 eqeq2d 
 |-  ( w = x -> ( t = ( -u 1 ^ ( # ` w ) ) <-> t = ( -u 1 ^ ( # ` x ) ) ) )
47 43 46 anbi12d 
 |-  ( w = x -> ( ( P = ( G gsum w ) /\ t = ( -u 1 ^ ( # ` w ) ) ) <-> ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) ) )
48 47 cbvrexvw 
 |-  ( E. w e. Word T ( P = ( G gsum w ) /\ t = ( -u 1 ^ ( # ` w ) ) ) <-> E. x e. Word T ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) )
49 41 48 bitrdi 
 |-  ( s = t -> ( E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) <-> E. x e. Word T ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) ) )
50 49 eu4 
 |-  ( E! s E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) <-> ( E. s E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) /\ A. s A. t ( ( E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) /\ E. x e. Word T ( P = ( G gsum x ) /\ t = ( -u 1 ^ ( # ` x ) ) ) ) -> s = t ) ) )
51 23 38 50 sylanbrc 
 |-  ( P e. dom N -> E! s E. w e. Word T ( P = ( G gsum w ) /\ s = ( -u 1 ^ ( # ` w ) ) ) )