MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  psgnuni Structured version   Visualization version   GIF version

Theorem psgnuni 18303
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.)
Hypotheses
Ref Expression
psgnuni.g 𝐺 = (SymGrp‘𝐷)
psgnuni.t 𝑇 = ran (pmTrsp‘𝐷)
psgnuni.d (𝜑𝐷𝑉)
psgnuni.w (𝜑𝑊 ∈ Word 𝑇)
psgnuni.x (𝜑𝑋 ∈ Word 𝑇)
psgnuni.e (𝜑 → (𝐺 Σg 𝑊) = (𝐺 Σg 𝑋))
Assertion
Ref Expression
psgnuni (𝜑 → (-1↑(♯‘𝑊)) = (-1↑(♯‘𝑋)))

Proof of Theorem psgnuni
StepHypRef Expression
1 psgnuni.w . . . . . 6 (𝜑𝑊 ∈ Word 𝑇)
2 lencl 13621 . . . . . 6 (𝑊 ∈ Word 𝑇 → (♯‘𝑊) ∈ ℕ0)
31, 2syl 17 . . . . 5 (𝜑 → (♯‘𝑊) ∈ ℕ0)
43nn0zd 11832 . . . 4 (𝜑 → (♯‘𝑊) ∈ ℤ)
5 m1expcl 13201 . . . 4 ((♯‘𝑊) ∈ ℤ → (-1↑(♯‘𝑊)) ∈ ℤ)
64, 5syl 17 . . 3 (𝜑 → (-1↑(♯‘𝑊)) ∈ ℤ)
76zcnd 11835 . 2 (𝜑 → (-1↑(♯‘𝑊)) ∈ ℂ)
8 psgnuni.x . . . . . 6 (𝜑𝑋 ∈ Word 𝑇)
9 lencl 13621 . . . . . 6 (𝑋 ∈ Word 𝑇 → (♯‘𝑋) ∈ ℕ0)
108, 9syl 17 . . . . 5 (𝜑 → (♯‘𝑋) ∈ ℕ0)
1110nn0zd 11832 . . . 4 (𝜑 → (♯‘𝑋) ∈ ℤ)
12 m1expcl 13201 . . . 4 ((♯‘𝑋) ∈ ℤ → (-1↑(♯‘𝑋)) ∈ ℤ)
1311, 12syl 17 . . 3 (𝜑 → (-1↑(♯‘𝑋)) ∈ ℤ)
1413zcnd 11835 . 2 (𝜑 → (-1↑(♯‘𝑋)) ∈ ℂ)
15 neg1cn 11496 . . . 4 -1 ∈ ℂ
16 neg1ne0 11498 . . . 4 -1 ≠ 0
17 expne0i 13210 . . . 4 ((-1 ∈ ℂ ∧ -1 ≠ 0 ∧ (♯‘𝑋) ∈ ℤ) → (-1↑(♯‘𝑋)) ≠ 0)
1815, 16, 17mp3an12 1524 . . 3 ((♯‘𝑋) ∈ ℤ → (-1↑(♯‘𝑋)) ≠ 0)
1911, 18syl 17 . 2 (𝜑 → (-1↑(♯‘𝑋)) ≠ 0)
20 m1expaddsub 18302 . . . . 5 (((♯‘𝑊) ∈ ℤ ∧ (♯‘𝑋) ∈ ℤ) → (-1↑((♯‘𝑊) − (♯‘𝑋))) = (-1↑((♯‘𝑊) + (♯‘𝑋))))
214, 11, 20syl2anc 579 . . . 4 (𝜑 → (-1↑((♯‘𝑊) − (♯‘𝑋))) = (-1↑((♯‘𝑊) + (♯‘𝑋))))
22 expsub 13226 . . . . . 6 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ ((♯‘𝑊) ∈ ℤ ∧ (♯‘𝑋) ∈ ℤ)) → (-1↑((♯‘𝑊) − (♯‘𝑋))) = ((-1↑(♯‘𝑊)) / (-1↑(♯‘𝑋))))
2315, 16, 22mpanl12 692 . . . . 5 (((♯‘𝑊) ∈ ℤ ∧ (♯‘𝑋) ∈ ℤ) → (-1↑((♯‘𝑊) − (♯‘𝑋))) = ((-1↑(♯‘𝑊)) / (-1↑(♯‘𝑋))))
244, 11, 23syl2anc 579 . . . 4 (𝜑 → (-1↑((♯‘𝑊) − (♯‘𝑋))) = ((-1↑(♯‘𝑊)) / (-1↑(♯‘𝑋))))
2521, 24eqtr3d 2815 . . 3 (𝜑 → (-1↑((♯‘𝑊) + (♯‘𝑋))) = ((-1↑(♯‘𝑊)) / (-1↑(♯‘𝑋))))
26 revcl 13907 . . . . . . . 8 (𝑋 ∈ Word 𝑇 → (reverse‘𝑋) ∈ Word 𝑇)
278, 26syl 17 . . . . . . 7 (𝜑 → (reverse‘𝑋) ∈ Word 𝑇)
28 ccatlen 13665 . . . . . . 7 ((𝑊 ∈ Word 𝑇 ∧ (reverse‘𝑋) ∈ Word 𝑇) → (♯‘(𝑊 ++ (reverse‘𝑋))) = ((♯‘𝑊) + (♯‘(reverse‘𝑋))))
291, 27, 28syl2anc 579 . . . . . 6 (𝜑 → (♯‘(𝑊 ++ (reverse‘𝑋))) = ((♯‘𝑊) + (♯‘(reverse‘𝑋))))
30 revlen 13908 . . . . . . . 8 (𝑋 ∈ Word 𝑇 → (♯‘(reverse‘𝑋)) = (♯‘𝑋))
318, 30syl 17 . . . . . . 7 (𝜑 → (♯‘(reverse‘𝑋)) = (♯‘𝑋))
3231oveq2d 6938 . . . . . 6 (𝜑 → ((♯‘𝑊) + (♯‘(reverse‘𝑋))) = ((♯‘𝑊) + (♯‘𝑋)))
3329, 32eqtrd 2813 . . . . 5 (𝜑 → (♯‘(𝑊 ++ (reverse‘𝑋))) = ((♯‘𝑊) + (♯‘𝑋)))
3433oveq2d 6938 . . . 4 (𝜑 → (-1↑(♯‘(𝑊 ++ (reverse‘𝑋)))) = (-1↑((♯‘𝑊) + (♯‘𝑋))))
35 psgnuni.g . . . . 5 𝐺 = (SymGrp‘𝐷)
36 psgnuni.t . . . . 5 𝑇 = ran (pmTrsp‘𝐷)
37 psgnuni.d . . . . 5 (𝜑𝐷𝑉)
38 ccatcl 13664 . . . . . 6 ((𝑊 ∈ Word 𝑇 ∧ (reverse‘𝑋) ∈ Word 𝑇) → (𝑊 ++ (reverse‘𝑋)) ∈ Word 𝑇)
391, 27, 38syl2anc 579 . . . . 5 (𝜑 → (𝑊 ++ (reverse‘𝑋)) ∈ Word 𝑇)
40 psgnuni.e . . . . . . . . . 10 (𝜑 → (𝐺 Σg 𝑊) = (𝐺 Σg 𝑋))
4140fveq2d 6450 . . . . . . . . 9 (𝜑 → ((invg𝐺)‘(𝐺 Σg 𝑊)) = ((invg𝐺)‘(𝐺 Σg 𝑋)))
42 eqid 2777 . . . . . . . . . . 11 (invg𝐺) = (invg𝐺)
4336, 35, 42symgtrinv 18275 . . . . . . . . . 10 ((𝐷𝑉𝑋 ∈ Word 𝑇) → ((invg𝐺)‘(𝐺 Σg 𝑋)) = (𝐺 Σg (reverse‘𝑋)))
4437, 8, 43syl2anc 579 . . . . . . . . 9 (𝜑 → ((invg𝐺)‘(𝐺 Σg 𝑋)) = (𝐺 Σg (reverse‘𝑋)))
4541, 44eqtr2d 2814 . . . . . . . 8 (𝜑 → (𝐺 Σg (reverse‘𝑋)) = ((invg𝐺)‘(𝐺 Σg 𝑊)))
4645oveq2d 6938 . . . . . . 7 (𝜑 → ((𝐺 Σg 𝑊)(+g𝐺)(𝐺 Σg (reverse‘𝑋))) = ((𝐺 Σg 𝑊)(+g𝐺)((invg𝐺)‘(𝐺 Σg 𝑊))))
4735symggrp 18203 . . . . . . . . 9 (𝐷𝑉𝐺 ∈ Grp)
4837, 47syl 17 . . . . . . . 8 (𝜑𝐺 ∈ Grp)
49 grpmnd 17816 . . . . . . . . . 10 (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
5048, 49syl 17 . . . . . . . . 9 (𝜑𝐺 ∈ Mnd)
51 eqid 2777 . . . . . . . . . . . 12 (Base‘𝐺) = (Base‘𝐺)
5236, 35, 51symgtrf 18272 . . . . . . . . . . 11 𝑇 ⊆ (Base‘𝐺)
53 sswrd 13607 . . . . . . . . . . 11 (𝑇 ⊆ (Base‘𝐺) → Word 𝑇 ⊆ Word (Base‘𝐺))
5452, 53ax-mp 5 . . . . . . . . . 10 Word 𝑇 ⊆ Word (Base‘𝐺)
5554, 1sseldi 3818 . . . . . . . . 9 (𝜑𝑊 ∈ Word (Base‘𝐺))
5651gsumwcl 17763 . . . . . . . . 9 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word (Base‘𝐺)) → (𝐺 Σg 𝑊) ∈ (Base‘𝐺))
5750, 55, 56syl2anc 579 . . . . . . . 8 (𝜑 → (𝐺 Σg 𝑊) ∈ (Base‘𝐺))
58 eqid 2777 . . . . . . . . 9 (+g𝐺) = (+g𝐺)
59 eqid 2777 . . . . . . . . 9 (0g𝐺) = (0g𝐺)
6051, 58, 59, 42grprinv 17856 . . . . . . . 8 ((𝐺 ∈ Grp ∧ (𝐺 Σg 𝑊) ∈ (Base‘𝐺)) → ((𝐺 Σg 𝑊)(+g𝐺)((invg𝐺)‘(𝐺 Σg 𝑊))) = (0g𝐺))
6148, 57, 60syl2anc 579 . . . . . . 7 (𝜑 → ((𝐺 Σg 𝑊)(+g𝐺)((invg𝐺)‘(𝐺 Σg 𝑊))) = (0g𝐺))
6246, 61eqtrd 2813 . . . . . 6 (𝜑 → ((𝐺 Σg 𝑊)(+g𝐺)(𝐺 Σg (reverse‘𝑋))) = (0g𝐺))
6354, 27sseldi 3818 . . . . . . 7 (𝜑 → (reverse‘𝑋) ∈ Word (Base‘𝐺))
6451, 58gsumccat 17764 . . . . . . 7 ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word (Base‘𝐺) ∧ (reverse‘𝑋) ∈ Word (Base‘𝐺)) → (𝐺 Σg (𝑊 ++ (reverse‘𝑋))) = ((𝐺 Σg 𝑊)(+g𝐺)(𝐺 Σg (reverse‘𝑋))))
6550, 55, 63, 64syl3anc 1439 . . . . . 6 (𝜑 → (𝐺 Σg (𝑊 ++ (reverse‘𝑋))) = ((𝐺 Σg 𝑊)(+g𝐺)(𝐺 Σg (reverse‘𝑋))))
6635symgid 18204 . . . . . . 7 (𝐷𝑉 → ( I ↾ 𝐷) = (0g𝐺))
6737, 66syl 17 . . . . . 6 (𝜑 → ( I ↾ 𝐷) = (0g𝐺))
6862, 65, 673eqtr4d 2823 . . . . 5 (𝜑 → (𝐺 Σg (𝑊 ++ (reverse‘𝑋))) = ( I ↾ 𝐷))
6935, 36, 37, 39, 68psgnunilem4 18301 . . . 4 (𝜑 → (-1↑(♯‘(𝑊 ++ (reverse‘𝑋)))) = 1)
7034, 69eqtr3d 2815 . . 3 (𝜑 → (-1↑((♯‘𝑊) + (♯‘𝑋))) = 1)
7125, 70eqtr3d 2815 . 2 (𝜑 → ((-1↑(♯‘𝑊)) / (-1↑(♯‘𝑋))) = 1)
727, 14, 19, 71diveq1d 11159 1 (𝜑 → (-1↑(♯‘𝑊)) = (-1↑(♯‘𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1601  wcel 2106  wne 2968  wss 3791   I cid 5260  ran crn 5356  cres 5357  cfv 6135  (class class class)co 6922  cc 10270  0cc0 10272  1c1 10273   + caddc 10275  cmin 10606  -cneg 10607   / cdiv 11032  0cn0 11642  cz 11728  cexp 13178  chash 13435  Word cword 13599   ++ cconcat 13660  reversecreverse 13904  Basecbs 16255  +gcplusg 16338  0gc0g 16486   Σg cgsu 16487  Mndcmnd 17680  Grpcgrp 17809  invgcminusg 17810  SymGrpcsymg 18180  pmTrspcpmtr 18244
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-xor 1583  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-ot 4406  df-uni 4672  df-int 4711  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-tpos 7634  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-2o 7844  df-oadd 7847  df-er 8026  df-map 8142  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-card 9098  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-4 11440  df-5 11441  df-6 11442  df-7 11443  df-8 11444  df-9 11445  df-n0 11643  df-xnn0 11715  df-z 11729  df-uz 11993  df-rp 12138  df-fz 12644  df-fzo 12785  df-seq 13120  df-exp 13179  df-hash 13436  df-word 13600  df-lsw 13653  df-concat 13661  df-s1 13686  df-substr 13731  df-pfx 13780  df-splice 13887  df-reverse 13905  df-s2 13999  df-struct 16257  df-ndx 16258  df-slot 16259  df-base 16261  df-sets 16262  df-ress 16263  df-plusg 16351  df-tset 16357  df-0g 16488  df-gsum 16489  df-mgm 17628  df-sgrp 17670  df-mnd 17681  df-mhm 17721  df-submnd 17722  df-grp 17812  df-minusg 17813  df-subg 17975  df-ghm 18042  df-gim 18085  df-oppg 18159  df-symg 18181  df-pmtr 18245
This theorem is referenced by:  psgneu  18310  psgndiflemA  20343
  Copyright terms: Public domain W3C validator