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 φ D V
psgnuni.w φ W Word T
psgnuni.x φ X Word T
psgnuni.e φ G W = G X
Assertion psgnuni φ 1 W = 1 X

Proof

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