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=SymGrpD
psgnuni.t T=ranpmTrspD
psgnuni.d φDV
psgnuni.w φWWordT
psgnuni.x φXWordT
psgnuni.e φGW=GX
Assertion psgnuni φ1W=1X

Proof

Step Hyp Ref Expression
1 psgnuni.g G=SymGrpD
2 psgnuni.t T=ranpmTrspD
3 psgnuni.d φDV
4 psgnuni.w φWWordT
5 psgnuni.x φXWordT
6 psgnuni.e φGW=GX
7 lencl WWordTW0
8 4 7 syl φW0
9 8 nn0zd φW
10 m1expcl W1W
11 9 10 syl φ1W
12 11 zcnd φ1W
13 lencl XWordTX0
14 5 13 syl φX0
15 14 nn0zd φX
16 m1expcl X1X
17 15 16 syl φ1X
18 17 zcnd φ1X
19 neg1cn 1
20 neg1ne0 10
21 expne0i 110X1X0
22 19 20 15 21 mp3an12i φ1X0
23 m1expaddsub WX1WX=1W+X
24 9 15 23 syl2anc φ1WX=1W+X
25 expsub 110WX1WX=1W1X
26 19 20 25 mpanl12 WX1WX=1W1X
27 9 15 26 syl2anc φ1WX=1W1X
28 revcl XWordTreverseXWordT
29 5 28 syl φreverseXWordT
30 ccatlen WWordTreverseXWordTW++reverseX=W+reverseX
31 4 29 30 syl2anc φW++reverseX=W+reverseX
32 revlen XWordTreverseX=X
33 5 32 syl φreverseX=X
34 33 oveq2d φW+reverseX=W+X
35 31 34 eqtr2d φW+X=W++reverseX
36 35 oveq2d φ1W+X=1W++reverseX
37 ccatcl WWordTreverseXWordTW++reverseXWordT
38 4 29 37 syl2anc φW++reverseXWordT
39 6 fveq2d φinvgGGW=invgGGX
40 eqid invgG=invgG
41 2 1 40 symgtrinv DVXWordTinvgGGX=GreverseX
42 3 5 41 syl2anc φinvgGGX=GreverseX
43 39 42 eqtr2d φGreverseX=invgGGW
44 43 oveq2d φGW+GGreverseX=GW+GinvgGGW
45 1 symggrp DVGGrp
46 3 45 syl φGGrp
47 grpmnd GGrpGMnd
48 3 45 47 3syl φGMnd
49 eqid BaseG=BaseG
50 2 1 49 symgtrf TBaseG
51 sswrd TBaseGWordTWordBaseG
52 50 51 ax-mp WordTWordBaseG
53 52 4 sselid φWWordBaseG
54 49 gsumwcl GMndWWordBaseGGWBaseG
55 48 53 54 syl2anc φGWBaseG
56 eqid +G=+G
57 eqid 0G=0G
58 49 56 57 40 grprinv GGrpGWBaseGGW+GinvgGGW=0G
59 46 55 58 syl2anc φGW+GinvgGGW=0G
60 44 59 eqtrd φGW+GGreverseX=0G
61 52 29 sselid φreverseXWordBaseG
62 49 56 gsumccat GMndWWordBaseGreverseXWordBaseGGW++reverseX=GW+GGreverseX
63 48 53 61 62 syl3anc φGW++reverseX=GW+GGreverseX
64 1 symgid DVID=0G
65 3 64 syl φID=0G
66 60 63 65 3eqtr4d φGW++reverseX=ID
67 1 2 3 38 66 psgnunilem4 φ1W++reverseX=1
68 36 67 eqtrd φ1W+X=1
69 24 27 68 3eqtr3d φ1W1X=1
70 12 18 22 69 diveq1d φ1W=1X