Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  psgnunilem4 Structured version   Unicode version

Theorem psgnunilem4 17135
 Description: Lemma for psgnuni 17137. An odd-length representation of the identity is impossible, as it could be repeatedly shortened to a length of 1, but a length 1 permutation must be a transposition. (Contributed by Stefan O'Rear, 25-Aug-2015.)
Hypotheses
Ref Expression
psgnunilem4.g
psgnunilem4.t pmTrsp
psgnunilem4.d
psgnunilem4.w1 Word
psgnunilem4.w2 g
Assertion
Ref Expression
psgnunilem4

Proof of Theorem psgnunilem4
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 psgnunilem4.w1 . 2 Word
2 psgnunilem4.w2 . 2 g
3 wrdfin 12688 . . . . 5 Word
4 hashcl 12543 . . . . 5
51, 3, 43syl 18 . . . 4
6 nn0uz 11199 . . . 4
75, 6syl6eleq 2521 . . 3
8 fveq2 5880 . . . . . . . . 9
9 hash0 12553 . . . . . . . . 9
108, 9syl6eq 2480 . . . . . . . 8
1110oveq2d 6320 . . . . . . 7
12 neg1cn 10719 . . . . . . . 8
13 exp0 12281 . . . . . . . 8
1412, 13ax-mp 5 . . . . . . 7
1511, 14syl6eq 2480 . . . . . 6
16152a1d 28 . . . . 5 ..^ Word g Word g
17 psgnunilem4.g . . . . . . . . . . . . 13
18 psgnunilem4.t . . . . . . . . . . . . 13 pmTrsp
19 simpl1 1009 . . . . . . . . . . . . . 14 Word g Word g
20 psgnunilem4.d . . . . . . . . . . . . . 14
2119, 20syl 17 . . . . . . . . . . . . 13 Word g Word g
22 simpl3l 1061 . . . . . . . . . . . . 13 Word g Word g Word
23 eqidd 2424 . . . . . . . . . . . . 13 Word g Word g
24 wrdfin 12688 . . . . . . . . . . . . . . 15 Word
2522, 24syl 17 . . . . . . . . . . . . . 14 Word g Word g
26 simpl2 1010 . . . . . . . . . . . . . 14 Word g Word g
27 hashnncl 12552 . . . . . . . . . . . . . . 15
2827biimpar 488 . . . . . . . . . . . . . 14
2925, 26, 28syl2anc 666 . . . . . . . . . . . . 13 Word g Word g
30 simpl3r 1062 . . . . . . . . . . . . 13 Word g Word g g
31 fveq2 5880 . . . . . . . . . . . . . . . . . . 19
3231eqeq1d 2425 . . . . . . . . . . . . . . . . . 18
33 oveq2 6312 . . . . . . . . . . . . . . . . . . 19 g g
3433eqeq1d 2425 . . . . . . . . . . . . . . . . . 18 g g
3532, 34anbi12d 716 . . . . . . . . . . . . . . . . 17 g g
3635cbvrexv 3057 . . . . . . . . . . . . . . . 16 Word g Word g
3736notbii 298 . . . . . . . . . . . . . . 15 Word g Word g
3837biimpi 198 . . . . . . . . . . . . . 14 Word g Word g
3938adantl 468 . . . . . . . . . . . . 13 Word g Word g Word g
4017, 18, 21, 22, 23, 29, 30, 39psgnunilem3 17134 . . . . . . . . . . . 12 Word g Word g
41 iman 426 . . . . . . . . . . . 12 Word g Word g Word g Word g
4240, 41mpbir 213 . . . . . . . . . . 11 Word g Word g
43 df-rex 2782 . . . . . . . . . . 11 Word g Word g
4442, 43sylib 200 . . . . . . . . . 10 Word g Word g
45 simprl 763 . . . . . . . . . . . . . . . . 17 Word g Word g Word
46 simprrr 774 . . . . . . . . . . . . . . . . 17 Word g Word g g
4745, 46jca 535 . . . . . . . . . . . . . . . 16 Word g Word g Word g
48 wrdfin 12688 . . . . . . . . . . . . . . . . . 18 Word
49 hashcl 12543 . . . . . . . . . . . . . . . . . 18
5045, 48, 493syl 18 . . . . . . . . . . . . . . . . 17 Word g Word g
51 simp3l 1034 . . . . . . . . . . . . . . . . . . . 20 Word g Word
5251, 24syl 17 . . . . . . . . . . . . . . . . . . 19 Word g
53 simp2 1007 . . . . . . . . . . . . . . . . . . 19 Word g
5452, 53, 28syl2anc 666 . . . . . . . . . . . . . . . . . 18 Word g
5554adantr 467 . . . . . . . . . . . . . . . . 17 Word g Word g
56 simprrl 773 . . . . . . . . . . . . . . . . . 18 Word g Word g
5755nnred 10630 . . . . . . . . . . . . . . . . . . 19 Word g Word g
58 2rp 11313 . . . . . . . . . . . . . . . . . . 19
59 ltsubrp 11341 . . . . . . . . . . . . . . . . . . 19
6057, 58, 59sylancl 667 . . . . . . . . . . . . . . . . . 18 Word g Word g
6156, 60eqbrtrd 4443 . . . . . . . . . . . . . . . . 17 Word g Word g
62 elfzo0 11962 . . . . . . . . . . . . . . . . 17 ..^
6350, 55, 61, 62syl3anbrc 1190 . . . . . . . . . . . . . . . 16 Word g Word g ..^
64 id 23 . . . . . . . . . . . . . . . . 17 ..^ Word g ..^ Word g
6564com13 84 . . . . . . . . . . . . . . . 16 Word g ..^ ..^ Word g
6647, 63, 65sylc 63 . . . . . . . . . . . . . . 15 Word g Word g ..^ Word g
6756oveq2d 6320 . . . . . . . . . . . . . . . . 17 Word g Word g
6812a1i 11 . . . . . . . . . . . . . . . . . 18 Word g Word g
69 neg1ne0 10721 . . . . . . . . . . . . . . . . . . 19
7069a1i 11 . . . . . . . . . . . . . . . . . 18 Word g Word g
71 2z 10975 . . . . . . . . . . . . . . . . . . 19
7271a1i 11 . . . . . . . . . . . . . . . . . 18 Word g Word g
7355nnzd 11045 . . . . . . . . . . . . . . . . . 18 Word g Word g
7468, 70, 72, 73expsubd 12432 . . . . . . . . . . . . . . . . 17 Word g Word g
75 neg1sqe1 12375 . . . . . . . . . . . . . . . . . . 19
7675oveq2i 6315 . . . . . . . . . . . . . . . . . 18
77 m1expcl 12300 . . . . . . . . . . . . . . . . . . . . 21
7877zcnd 11047 . . . . . . . . . . . . . . . . . . . 20
7973, 78syl 17 . . . . . . . . . . . . . . . . . . 19 Word g Word g
8079div1d 10381 . . . . . . . . . . . . . . . . . 18 Word g Word g
8176, 80syl5eq 2476 . . . . . . . . . . . . . . . . 17 Word g Word g
8267, 74, 813eqtrd 2468 . . . . . . . . . . . . . . . 16 Word g Word g
8382eqeq1d 2425 . . . . . . . . . . . . . . 15 Word g Word g
8466, 83sylibd 218 . . . . . . . . . . . . . 14 Word g Word g ..^ Word g
8584ex 436 . . . . . . . . . . . . 13 Word g Word g ..^ Word g
8685com23 82 . . . . . . . . . . . 12 Word g ..^ Word g Word g
8786alimdv 1754 . . . . . . . . . . 11 Word g ..^ Word g Word g
88 19.23v 1808 . . . . . . . . . . 11 Word g Word g
8987, 88syl6ib 230 . . . . . . . . . 10 Word g ..^ Word g Word g
9044, 89mpid 43 . . . . . . . . 9 Word g ..^ Word g
91903exp 1205 . . . . . . . 8 Word g ..^ Word g
9291com34 87 . . . . . . 7 ..^ Word g Word g
9392com12 33 . . . . . 6 ..^ Word g Word g
9493impd 433 . . . . 5 ..^ Word g Word g
9516, 94pm2.61ine 2738 . . . 4 ..^ Word g Word g
96953adant2 1025 . . 3 ..^ Word g Word g
97 eleq1 2495 . . . . 5 Word Word
98 oveq2 6312 . . . . . 6 g g
9998eqeq1d 2425 . . . . 5 g g
10097, 99anbi12d 716 . . . 4 Word g Word g
101 fveq2 5880 . . . . . 6
102101oveq2d 6320 . . . . 5
103102eqeq1d 2425 . . . 4
104100, 103imbi12d 322 . . 3 Word g Word g
105 eleq1 2495 . . . . 5 Word Word
106 oveq2 6312 . . . . . 6 g g
107106eqeq1d 2425 . . . . 5 g g
108105, 107anbi12d 716 . . . 4 Word g Word g
109 fveq2 5880 . . . . . 6
110109oveq2d 6320 . . . . 5
111110eqeq1d 2425 . . . 4
112108, 111imbi12d 322 . . 3 Word g Word g
1131, 7, 96, 104, 112, 101, 109uzindi 12199 . 2 Word g
1141, 2, 113mp2and 684 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 371   w3a 983  wal 1436   wceq 1438  wex 1660   wcel 1869   wne 2619  wrex 2777  c0 3763   class class class wbr 4422   cid 4762   crn 4853   cres 4854  cfv 5600  (class class class)co 6304  cfn 7579  cc 9543  cr 9544  cc0 9545  c1 9546   clt 9681   cmin 9866  cneg 9867   cdiv 10275  cn 10615  c2 10665  cn0 10875  cz 10943  cuz 11165  crp 11308  cfz 11790  ..^cfzo 11921  cexp 12277  chash 12520  Word cword 12658   g cgsu 15336  csymg 17015  pmTrspcpmtr 17079 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4535  ax-sep 4545  ax-nul 4554  ax-pow 4601  ax-pr 4659  ax-un 6596  ax-cnex 9601  ax-resscn 9602  ax-1cn 9603  ax-icn 9604  ax-addcl 9605  ax-addrcl 9606  ax-mulcl 9607  ax-mulrcl 9608  ax-mulcom 9609  ax-addass 9610  ax-mulass 9611  ax-distr 9612  ax-i2m1 9613  ax-1ne0 9614  ax-1rid 9615  ax-rnegex 9616  ax-rrecex 9617  ax-cnre 9618  ax-pre-lttri 9619  ax-pre-lttrn 9620  ax-pre-ltadd 9621  ax-pre-mulgt0 9622 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-xor 1402  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3302  df-csb 3398  df-dif 3441  df-un 3443  df-in 3445  df-ss 3452  df-pss 3454  df-nul 3764  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-ot 4007  df-uni 4219  df-int 4255  df-iun 4300  df-br 4423  df-opab 4482  df-mpt 4483  df-tr 4518  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-se 4812  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-isom 5609  df-riota 6266  df-ov 6307  df-oprab 6308  df-mpt2 6309  df-om 6706  df-1st 6806  df-2nd 6807  df-wrecs 7038  df-recs 7100  df-rdg 7138  df-1o 7192  df-2o 7193  df-oadd 7196  df-er 7373  df-map 7484  df-en 7580  df-dom 7581  df-sdom 7582  df-fin 7583  df-card 8380  df-cda 8604  df-pnf 9683  df-mnf 9684  df-xr 9685  df-ltxr 9686  df-le 9687  df-sub 9868  df-neg 9869  df-div 10276  df-nn 10616  df-2 10674  df-3 10675  df-4 10676  df-5 10677  df-6 10678  df-7 10679  df-8 10680  df-9 10681  df-n0 10876  df-z 10944  df-uz 11166  df-rp 11309  df-fz 11791  df-fzo 11922  df-seq 12219  df-exp 12278  df-hash 12521  df-word 12666  df-lsw 12667  df-concat 12668  df-s1 12669  df-substr 12670  df-splice 12671  df-s2 12944  df-struct 15120  df-ndx 15121  df-slot 15122  df-base 15123  df-sets 15124  df-ress 15125  df-plusg 15200  df-tset 15206  df-0g 15337  df-gsum 15338  df-mgm 16485  df-sgrp 16524  df-mnd 16534  df-submnd 16580  df-grp 16670  df-minusg 16671  df-subg 16811  df-symg 17016  df-pmtr 17080 This theorem is referenced by:  psgnuni  17137
 Copyright terms: Public domain W3C validator