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 sselid
 |-  ( 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 sselid
 |-  ( 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 ) ) )