Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rusgranumwlks Structured version   Unicode version

Theorem rusgranumwlks 30499
 Description: Induction step for rusgranumwlk 30500. (Contributed by Alexander van der Vekens, 24-Aug-2018.)
Hypotheses
Ref Expression
rusgranumwlk.w Walks
rusgranumwlk.l
Assertion
Ref Expression
rusgranumwlks RegUSGrph
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,,   ,   ,,,   ,,   ,,   ,
Allowed substitution hints:   ()   (,,)   (,,,)   ()

Proof of Theorem rusgranumwlks
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rusisusgra 30473 . . . 4 RegUSGrph USGrph
21adantr 462 . . 3 RegUSGrph USGrph
3 simpr2 990 . . 3 RegUSGrph
4 simp3 985 . . . 4
54adantl 463 . . 3 RegUSGrph
6 rusgranumwlk.w . . . . 5 Walks
7 rusgranumwlk.l . . . . 5
86, 7rusgranumwlklem4 30495 . . . 4 USGrph WWalksN
98eqeq1d 2449 . . 3 USGrph WWalksN
102, 3, 5, 9syl3anc 1213 . 2 RegUSGrph WWalksN
11 wwlknredwwlkn0 30284 . . . . . . . . . . . 12 WWalksN WWalksN substr lastS lastS
1211ex 434 . . . . . . . . . . 11 WWalksN WWalksN substr lastS lastS
13123ad2ant3 1006 . . . . . . . . . 10 WWalksN WWalksN substr lastS lastS
1413adantl 463 . . . . . . . . 9 RegUSGrph WWalksN WWalksN substr lastS lastS
1514imp 429 . . . . . . . 8 RegUSGrph WWalksN WWalksN substr lastS lastS
1615rabbidva 2961 . . . . . . 7 RegUSGrph WWalksN WWalksN WWalksN substr lastS lastS
1716adantr 462 . . . . . 6 RegUSGrph WWalksN WWalksN WWalksN WWalksN substr lastS lastS
1817fveq2d 5692 . . . . 5 RegUSGrph WWalksN WWalksN WWalksN WWalksN substr lastS lastS
19 simp2 984 . . . . . . . . . . . . 13 substr lastS lastS
2019pm4.71ri 628 . . . . . . . . . . . 12 substr lastS lastS substr lastS lastS
2120a1i 11 . . . . . . . . . . 11 RegUSGrph WWalksN WWalksN substr lastS lastS substr lastS lastS
2221rexbidva 2730 . . . . . . . . . 10 RegUSGrph WWalksN WWalksN substr lastS lastS WWalksN substr lastS lastS
23 fveq1 5687 . . . . . . . . . . . 12
2423eqeq1d 2449 . . . . . . . . . . 11
2524rexrab 3120 . . . . . . . . . 10 WWalksN substr lastS lastS WWalksN substr lastS lastS
2622, 25syl6bbr 263 . . . . . . . . 9 RegUSGrph WWalksN WWalksN substr lastS lastS WWalksN substr lastS lastS
2726rabbidva 2961 . . . . . . . 8 RegUSGrph WWalksN WWalksN substr lastS lastS WWalksN WWalksN substr lastS lastS
2827adantr 462 . . . . . . 7 RegUSGrph WWalksN WWalksN WWalksN substr lastS lastS WWalksN WWalksN substr lastS lastS
2928fveq2d 5692 . . . . . 6 RegUSGrph WWalksN WWalksN WWalksN substr lastS lastS WWalksN WWalksN substr lastS lastS
30 simplr1 1025 . . . . . . . 8 RegUSGrph WWalksN
31 eqid 2441 . . . . . . . . 9 WWalksN WWalksN
32 eqid 2441 . . . . . . . . 9 WWalksN WWalksN
3331, 32hashwwlkext 30490 . . . . . . . 8 WWalksN WWalksN substr lastS lastS WWalksN WWalksN substr lastS lastS
3430, 33syl 16 . . . . . . 7 RegUSGrph WWalksN WWalksN WWalksN substr lastS lastS WWalksN WWalksN substr lastS lastS
35 fveq1 5687 . . . . . . . . . . 11
3635eqeq1d 2449 . . . . . . . . . 10
3736cbvrabv 2969 . . . . . . . . 9 WWalksN WWalksN
3837sumeq1i 13171 . . . . . . . 8 WWalksN WWalksN substr lastS lastS WWalksN WWalksN substr lastS lastS
3938a1i 11 . . . . . . 7 RegUSGrph WWalksN WWalksN WWalksN substr lastS lastS WWalksN WWalksN substr lastS lastS
4034, 39eqtrd 2473 . . . . . 6 RegUSGrph WWalksN WWalksN WWalksN substr lastS lastS WWalksN WWalksN substr lastS lastS
4129, 40eqtrd 2473 . . . . 5 RegUSGrph WWalksN WWalksN WWalksN substr lastS lastS WWalksN WWalksN substr lastS lastS
42 rusgranumwlklem0 30491 . . . . . . . . . . . 12 WWalksN WWalksN substr lastS lastS WWalksN substr lastS lastS
4342eqcomd 2446 . . . . . . . . . . 11 WWalksN WWalksN substr lastS lastS WWalksN substr lastS lastS
4443fveq2d 5692 . . . . . . . . . 10 WWalksN WWalksN substr lastS lastS WWalksN substr lastS lastS
4544adantl 463 . . . . . . . . 9 RegUSGrph WWalksN WWalksN WWalksN substr lastS lastS WWalksN substr lastS lastS
46 fveq1 5687 . . . . . . . . . . . . . 14
4746eqeq1d 2449 . . . . . . . . . . . . 13
4847elrab 3114 . . . . . . . . . . . 12 WWalksN WWalksN
4948simplbi 457 . . . . . . . . . . 11 WWalksN WWalksN
5049adantl 463 . . . . . . . . . 10 RegUSGrph WWalksN WWalksN WWalksN
51 wwlkexthasheq 30291 . . . . . . . . . 10 WWalksN WWalksN substr lastS lastS lastS
5250, 51syl 16 . . . . . . . . 9 RegUSGrph WWalksN WWalksN WWalksN substr lastS lastS lastS
53 rusgraprop3 30480 . . . . . . . . . . 11 RegUSGrph USGrph
54 wwlknimp 30246 . . . . . . . . . . . . . . . . . . . . 21 WWalksN Word ..^
5554adantr 462 . . . . . . . . . . . . . . . . . . . 20 WWalksN Word ..^
56 simpll 748 . . . . . . . . . . . . . . . . . . . . . . 23 Word Word
57 nn0re 10584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
58 1re 9381 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
5958a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
60 nn0ge0 10601 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
61 0lt1 9858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6261a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6357, 59, 60, 62addgegt0d 9909 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
64633ad2ant3 1006 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6564adantl 463 . . . . . . . . . . . . . . . . . . . . . . . . 25 Word
66 breq2 4293 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6766ad2antlr 721 . . . . . . . . . . . . . . . . . . . . . . . . 25 Word
6865, 67mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . 24 Word
69 hashle00 12154 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word
70 lencl 12245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word
7170nn0red 10633 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word
72 0re 9382 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
73 lenlt 9449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7473bicomd 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7571, 72, 74sylancl 657 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word
76 nne 2610 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7776a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word
7869, 75, 773bitr4rd 286 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Word
7978ad2antrr 720 . . . . . . . . . . . . . . . . . . . . . . . . 25 Word
8079con4bid 293 . . . . . . . . . . . . . . . . . . . . . . . 24 Word
8168, 80mpbird 232 . . . . . . . . . . . . . . . . . . . . . . 23 Word
8256, 81jca 529 . . . . . . . . . . . . . . . . . . . . . 22 Word Word
8382ex 434 . . . . . . . . . . . . . . . . . . . . 21 Word Word
84833adant3 1003 . . . . . . . . . . . . . . . . . . . 20 Word ..^ Word
8555, 84syl 16 . . . . . . . . . . . . . . . . . . 19 WWalksN Word
8648, 85sylbi 195 . . . . . . . . . . . . . . . . . 18 WWalksN Word
8786imp 429 . . . . . . . . . . . . . . . . 17 WWalksN Word
88 lswcl 12266 . . . . . . . . . . . . . . . . 17 Word lastS
8987, 88syl 16 . . . . . . . . . . . . . . . 16 WWalksN lastS
9089ad2antrr 720 . . . . . . . . . . . . . . 15 WWalksN WWalksN lastS
91 preq1 3951 . . . . . . . . . . . . . . . . . . . 20 lastS lastS
9291eleq1d 2507 . . . . . . . . . . . . . . . . . . 19 lastS lastS
9392rabbidv 2962 . . . . . . . . . . . . . . . . . 18 lastS lastS
9493fveq2d 5692 . . . . . . . . . . . . . . . . 17 lastS lastS
9594eqeq1d 2449 . . . . . . . . . . . . . . . 16 lastS lastS
9695rspcva 3068 . . . . . . . . . . . . . . 15 lastS lastS
9790, 96sylancom 662 . . . . . . . . . . . . . 14 WWalksN WWalksN lastS
9897exp41 607 . . . . . . . . . . . . 13 WWalksN WWalksN lastS
9998com14 88 . . . . . . . . . . . 12 WWalksN WWalksN lastS
100993ad2ant3 1006 . . . . . . . . . . 11 USGrph WWalksN WWalksN lastS
10153, 100syl 16 . . . . . . . . . 10 RegUSGrph WWalksN WWalksN lastS
102101imp41 590 . . . . . . . . 9 RegUSGrph WWalksN WWalksN lastS
10345, 52, 1023eqtrd 2477 . . . . . . . 8 RegUSGrph WWalksN WWalksN WWalksN substr lastS lastS
104103ralrimiva 2797 . . . . . . 7 RegUSGrph WWalksN WWalksN WWalksN substr lastS lastS
105104sumeq2d 13175 . . . . . 6 RegUSGrph WWalksN WWalksN WWalksN substr lastS lastS WWalksN
106 oveq1 6097 . . . . . . . 8 WWalksN WWalksN
107106adantl 463 . . . . . . 7 RegUSGrph WWalksN WWalksN
108 wwlknfi 30295 . . . . . . . . . . 11 WWalksN
1091083ad2ant1 1004 . . . . . . . . . 10 WWalksN
110109ad2antlr 721 . . . . . . . . 9 RegUSGrph WWalksN WWalksN
111 rabfi 7533 . . . . . . . . 9 WWalksN WWalksN
112110, 111syl 16 . . . . . . . 8 RegUSGrph WWalksN WWalksN
113 rusgraprop 30471 . . . . . . . . . 10 RegUSGrph USGrph VDeg
114 nn0cn 10585 . . . . . . . . . . 11
1151143ad2ant2 1005 . . . . . . . . . 10 USGrph VDeg
116113, 115syl 16 . . . . . . . . 9 RegUSGrph
117116ad2antrr 720 . . . . . . . 8 RegUSGrph WWalksN
118 fsumconst 13253 . . . . . . . 8 WWalksN WWalksN WWalksN
119112, 117, 118syl2anc 656 . . . . . . 7 RegUSGrph WWalksN WWalksN WWalksN
120 expp1 11868 . . . . . . . . 9
121116, 4, 120syl2an 474 . . . . . . . 8 RegUSGrph
122121adantr 462 . . . . . . 7 RegUSGrph WWalksN
123107, 119, 1223eqtr4d 2483 . . . . . 6 RegUSGrph WWalksN WWalksN
124105, 123eqtrd 2473 . . . . 5 RegUSGrph WWalksN WWalksN WWalksN substr lastS lastS
12518, 41, 1243eqtrd 2477 . . . 4 RegUSGrph WWalksN WWalksN
126 peano2nn0 10616 . . . . . . . 8
1271263ad2ant3 1006 . . . . . . 7
128127adantl 463 . . . . . 6 RegUSGrph
1296, 7rusgranumwlklem4 30495 . . . . . . 7 USGrph WWalksN
130129eqeq1d 2449 . . . . . 6 USGrph WWalksN
1312, 3, 128, 130syl3anc 1213 . . . . 5 RegUSGrph WWalksN
132131adantr 462 . . . 4 RegUSGrph WWalksN WWalksN
133125, 132mpbird 232 . . 3 RegUSGrph WWalksN
134133ex 434 . 2 RegUSGrph WWalksN
13510, 134sylbid 215 1 RegUSGrph
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184   wa 369   w3a 960   wceq 1364   wcel 1761   wne 2604  wral 2713  wrex 2714  crab 2717  c0 3634  cpr 3876  cop 3880   class class class wbr 4289   cmpt 4347   crn 4837  cfv 5415  (class class class)co 6090   cmpt2 6092  c1st 6574  c2nd 6575  cfn 7306  cc 9276  cr 9277  cc0 9278  c1 9279   caddc 9281   cmul 9283   clt 9414   cle 9415  cn0 10575  ..^cfzo 11544  cexp 11861  chash 12099  Word cword 12217   lastS clsw 12218   substr csubstr 12221  csu 13159   USGrph cusg 23199   Walks cwalk 23340   VDeg cvdg 23498   WWalksN cwwlkn 30237   RegUSGrph crusgra 30465 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-inf2 7843  ax-cnex 9334  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346  ax-1ne0 9347  ax-1rid 9348  ax-rnegex 9349  ax-rrecex 9350  ax-cnre 9351  ax-pre-lttri 9352  ax-pre-lttrn 9353  ax-pre-ltadd 9354  ax-pre-mulgt0 9355  ax-pre-sup 9356 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-fal 1370  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-disj 4260  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-se 4676  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-isom 5424  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-om 6476  df-1st 6576  df-2nd 6577  df-recs 6828  df-rdg 6862  df-1o 6916  df-2o 6917  df-oadd 6920  df-er 7097  df-map 7212  df-pm 7213  df-en 7307  df-dom 7308  df-sdom 7309  df-fin 7310  df-sup 7687  df-oi 7720  df-card 8105  df-cda 8333  df-pnf 9416  df-mnf 9417  df-xr 9418  df-ltxr 9419  df-le 9420  df-sub 9593  df-neg 9594  df-div 9990  df-nn 10319  df-2 10376  df-3 10377  df-n0 10576  df-z 10643  df-uz 10858  df-rp 10988  df-xadd 11086  df-fz 11434  df-fzo 11545  df-seq 11803  df-exp 11862  df-hash 12100  df-word 12225  df-lsw 12226  df-concat 12227  df-s1 12228  df-substr 12229  df-cj 12584  df-re 12585  df-im 12586  df-sqr 12720  df-abs 12721  df-clim 12962  df-sum 13160  df-usgra 23201  df-nbgra 23267  df-wlk 23350  df-vdgr 23499  df-wwlk 30238  df-wwlkn 30239  df-rgra 30466  df-rusgra 30467 This theorem is referenced by:  rusgranumwlk  30500
 Copyright terms: Public domain W3C validator