Metamath Proof Explorer

Theorem psgnuni

Description: If the same permutation can be written in more than one way as a product of transpositions, the parity of those products must agree; otherwise the product of one with the inverse of the other would be an odd representation of the identity. (Contributed by Stefan O'Rear, 27-Aug-2015)

Ref Expression
Hypotheses psgnuni.g 
|- G = ( SymGrp ` D )
psgnuni.t 
|- T = ran ( pmTrsp ` D )
psgnuni.d 
|- ( ph -> D e. V )
psgnuni.w 
|- ( ph -> W e. Word T )
psgnuni.x 
|- ( ph -> X e. Word T )
psgnuni.e 
|- ( ph -> ( G gsum W ) = ( G gsum X ) )
Assertion psgnuni 
|- ( ph -> ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` X ) ) )

Proof

Step Hyp Ref Expression
1 psgnuni.g 
 |-  G = ( SymGrp ` D )
2 psgnuni.t 
 |-  T = ran ( pmTrsp ` D )
3 psgnuni.d 
 |-  ( ph -> D e. V )
4 psgnuni.w 
 |-  ( ph -> W e. Word T )
5 psgnuni.x 
 |-  ( ph -> X e. Word T )
6 psgnuni.e 
 |-  ( ph -> ( G gsum W ) = ( G gsum X ) )
7 lencl 
 |-  ( W e. Word T -> ( # ` W ) e. NN0 )
8 4 7 syl 
 |-  ( ph -> ( # ` W ) e. NN0 )
9 8 nn0zd 
 |-  ( ph -> ( # ` W ) e. ZZ )
10 m1expcl 
 |-  ( ( # ` W ) e. ZZ -> ( -u 1 ^ ( # ` W ) ) e. ZZ )
11 9 10 syl 
 |-  ( ph -> ( -u 1 ^ ( # ` W ) ) e. ZZ )
12 11 zcnd 
 |-  ( ph -> ( -u 1 ^ ( # ` W ) ) e. CC )
13 lencl 
 |-  ( X e. Word T -> ( # ` X ) e. NN0 )
14 5 13 syl 
 |-  ( ph -> ( # ` X ) e. NN0 )
15 14 nn0zd 
 |-  ( ph -> ( # ` X ) e. ZZ )
16 m1expcl 
 |-  ( ( # ` X ) e. ZZ -> ( -u 1 ^ ( # ` X ) ) e. ZZ )
17 15 16 syl 
 |-  ( ph -> ( -u 1 ^ ( # ` X ) ) e. ZZ )
18 17 zcnd 
 |-  ( ph -> ( -u 1 ^ ( # ` X ) ) e. CC )
19 neg1cn 
 |-  -u 1 e. CC
20 neg1ne0 
 |-  -u 1 =/= 0
21 expne0i 
 |-  ( ( -u 1 e. CC /\ -u 1 =/= 0 /\ ( # ` X ) e. ZZ ) -> ( -u 1 ^ ( # ` X ) ) =/= 0 )
22 19 20 15 21 mp3an12i 
 |-  ( ph -> ( -u 1 ^ ( # ` X ) ) =/= 0 )
23 m1expaddsub 
 |-  ( ( ( # ` W ) e. ZZ /\ ( # ` X ) e. ZZ ) -> ( -u 1 ^ ( ( # ` W ) - ( # ` X ) ) ) = ( -u 1 ^ ( ( # ` W ) + ( # ` X ) ) ) )
24 9 15 23 syl2anc 
 |-  ( ph -> ( -u 1 ^ ( ( # ` W ) - ( # ` X ) ) ) = ( -u 1 ^ ( ( # ` W ) + ( # ` X ) ) ) )
25 expsub 
 |-  ( ( ( -u 1 e. CC /\ -u 1 =/= 0 ) /\ ( ( # ` W ) e. ZZ /\ ( # ` X ) e. ZZ ) ) -> ( -u 1 ^ ( ( # ` W ) - ( # ` X ) ) ) = ( ( -u 1 ^ ( # ` W ) ) / ( -u 1 ^ ( # ` X ) ) ) )
26 19 20 25 mpanl12 
 |-  ( ( ( # ` W ) e. ZZ /\ ( # ` X ) e. ZZ ) -> ( -u 1 ^ ( ( # ` W ) - ( # ` X ) ) ) = ( ( -u 1 ^ ( # ` W ) ) / ( -u 1 ^ ( # ` X ) ) ) )
27 9 15 26 syl2anc 
 |-  ( ph -> ( -u 1 ^ ( ( # ` W ) - ( # ` X ) ) ) = ( ( -u 1 ^ ( # ` W ) ) / ( -u 1 ^ ( # ` X ) ) ) )
28 revcl 
 |-  ( X e. Word T -> ( reverse ` X ) e. Word T )
29 5 28 syl 
 |-  ( ph -> ( reverse ` X ) e. Word T )
30 ccatlen 
 |-  ( ( W e. Word T /\ ( reverse ` X ) e. Word T ) -> ( # ` ( W ++ ( reverse ` X ) ) ) = ( ( # ` W ) + ( # ` ( reverse ` X ) ) ) )
31 4 29 30 syl2anc 
 |-  ( ph -> ( # ` ( W ++ ( reverse ` X ) ) ) = ( ( # ` W ) + ( # ` ( reverse ` X ) ) ) )
32 revlen 
 |-  ( X e. Word T -> ( # ` ( reverse ` X ) ) = ( # ` X ) )
33 5 32 syl 
 |-  ( ph -> ( # ` ( reverse ` X ) ) = ( # ` X ) )
34 33 oveq2d 
 |-  ( ph -> ( ( # ` W ) + ( # ` ( reverse ` X ) ) ) = ( ( # ` W ) + ( # ` X ) ) )
35 31 34 eqtr2d 
 |-  ( ph -> ( ( # ` W ) + ( # ` X ) ) = ( # ` ( W ++ ( reverse ` X ) ) ) )
36 35 oveq2d 
 |-  ( ph -> ( -u 1 ^ ( ( # ` W ) + ( # ` X ) ) ) = ( -u 1 ^ ( # ` ( W ++ ( reverse ` X ) ) ) ) )
37 ccatcl 
 |-  ( ( W e. Word T /\ ( reverse ` X ) e. Word T ) -> ( W ++ ( reverse ` X ) ) e. Word T )
38 4 29 37 syl2anc 
 |-  ( ph -> ( W ++ ( reverse ` X ) ) e. Word T )
39 6 fveq2d 
 |-  ( ph -> ( ( invg ` G ) ` ( G gsum W ) ) = ( ( invg ` G ) ` ( G gsum X ) ) )
40 eqid 
 |-  ( invg ` G ) = ( invg ` G )
41 2 1 40 symgtrinv 
 |-  ( ( D e. V /\ X e. Word T ) -> ( ( invg ` G ) ` ( G gsum X ) ) = ( G gsum ( reverse ` X ) ) )
42 3 5 41 syl2anc 
 |-  ( ph -> ( ( invg ` G ) ` ( G gsum X ) ) = ( G gsum ( reverse ` X ) ) )
43 39 42 eqtr2d 
 |-  ( ph -> ( G gsum ( reverse ` X ) ) = ( ( invg ` G ) ` ( G gsum W ) ) )
44 43 oveq2d 
 |-  ( ph -> ( ( G gsum W ) ( +g ` G ) ( G gsum ( reverse ` X ) ) ) = ( ( G gsum W ) ( +g ` G ) ( ( invg ` G ) ` ( G gsum W ) ) ) )
45 1 symggrp 
 |-  ( D e. V -> G e. Grp )
46 3 45 syl 
 |-  ( ph -> G e. Grp )
47 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
48 3 45 47 3syl 
 |-  ( ph -> G e. Mnd )
49 eqid 
 |-  ( Base ` G ) = ( Base ` G )
50 2 1 49 symgtrf 
 |-  T C_ ( Base ` G )
51 sswrd 
 |-  ( T C_ ( Base ` G ) -> Word T C_ Word ( Base ` G ) )
52 50 51 ax-mp 
 |-  Word T C_ Word ( Base ` G )
53 52 4 sseldi 
 |-  ( ph -> W e. Word ( Base ` G ) )
54 49 gsumwcl 
 |-  ( ( G e. Mnd /\ W e. Word ( Base ` G ) ) -> ( G gsum W ) e. ( Base ` G ) )
55 48 53 54 syl2anc 
 |-  ( ph -> ( G gsum W ) e. ( Base ` G ) )
56 eqid 
 |-  ( +g ` G ) = ( +g ` G )
57 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
58 49 56 57 40 grprinv 
 |-  ( ( G e. Grp /\ ( G gsum W ) e. ( Base ` G ) ) -> ( ( G gsum W ) ( +g ` G ) ( ( invg ` G ) ` ( G gsum W ) ) ) = ( 0g ` G ) )
59 46 55 58 syl2anc 
 |-  ( ph -> ( ( G gsum W ) ( +g ` G ) ( ( invg ` G ) ` ( G gsum W ) ) ) = ( 0g ` G ) )
60 44 59 eqtrd 
 |-  ( ph -> ( ( G gsum W ) ( +g ` G ) ( G gsum ( reverse ` X ) ) ) = ( 0g ` G ) )
61 52 29 sseldi 
 |-  ( ph -> ( reverse ` X ) e. Word ( Base ` G ) )
62 49 56 gsumccat 
 |-  ( ( G e. Mnd /\ W e. Word ( Base ` G ) /\ ( reverse ` X ) e. Word ( Base ` G ) ) -> ( G gsum ( W ++ ( reverse ` X ) ) ) = ( ( G gsum W ) ( +g ` G ) ( G gsum ( reverse ` X ) ) ) )
63 48 53 61 62 syl3anc 
 |-  ( ph -> ( G gsum ( W ++ ( reverse ` X ) ) ) = ( ( G gsum W ) ( +g ` G ) ( G gsum ( reverse ` X ) ) ) )
64 1 symgid 
 |-  ( D e. V -> ( _I |` D ) = ( 0g ` G ) )
65 3 64 syl 
 |-  ( ph -> ( _I |` D ) = ( 0g ` G ) )
66 60 63 65 3eqtr4d 
 |-  ( ph -> ( G gsum ( W ++ ( reverse ` X ) ) ) = ( _I |` D ) )
67 1 2 3 38 66 psgnunilem4 
 |-  ( ph -> ( -u 1 ^ ( # ` ( W ++ ( reverse ` X ) ) ) ) = 1 )
68 36 67 eqtrd 
 |-  ( ph -> ( -u 1 ^ ( ( # ` W ) + ( # ` X ) ) ) = 1 )
69 24 27 68 3eqtr3d 
 |-  ( ph -> ( ( -u 1 ^ ( # ` W ) ) / ( -u 1 ^ ( # ` X ) ) ) = 1 )
70 12 18 22 69 diveq1d 
 |-  ( ph -> ( -u 1 ^ ( # ` W ) ) = ( -u 1 ^ ( # ` X ) ) )