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

Theorem clwlkfclwwlk 30658
 Description: There is a function between the set of closed walks (defined as words) of length n and the set of closed walks of length n (in an undirected simple graph). (Contributed by Alexander van der Vekens, 25-Jun-2018.)
Hypotheses
Ref Expression
clwlkfclwwlk.1
clwlkfclwwlk.2
clwlkfclwwlk.c ClWalks
clwlkfclwwlk.f substr
Assertion
Ref Expression
clwlkfclwwlk USGrph ClWWalksN
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem clwlkfclwwlk
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 clwlkfclwwlk.c . . . . . 6 ClWalks
21rabeq2i 3068 . . . . 5 ClWalks
3 clwlkfclwwlk.1 . . . . . . . 8
4 clwlkfclwwlk.2 . . . . . . . 8
53, 4clwlkcompim 30568 . . . . . . 7 ClWalks Word ..^
6 lencl 12360 . . . . . . . . 9 Word
7 clwlkfclwwlk.f . . . . . . . . . . . . . . . . . 18 substr
83, 4, 1, 7clwlkfclwwlk2wrd 30654 . . . . . . . . . . . . . . . . 17 Word
98ad2antlr 726 . . . . . . . . . . . . . . . 16 Word ..^ USGrph Word
10 swrdcl 12426 . . . . . . . . . . . . . . . 16 Word substr Word
119, 10syl 16 . . . . . . . . . . . . . . 15 Word ..^ USGrph substr Word
12 simp-5r 768 . . . . . . . . . . . . . . . . . . 19 Word ..^ Word
13 simp1 988 . . . . . . . . . . . . . . . . . . 19 USGrph USGrph
1412, 13anim12ci 567 . . . . . . . . . . . . . . . . . 18 Word ..^ USGrph USGrph Word
15 simp-5r 768 . . . . . . . . . . . . . . . . . 18 Word ..^ USGrph
16 prmuz2 13892 . . . . . . . . . . . . . . . . . . . . 21
17 hashfzdm 12313 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1817adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25 Word
19 eluz2 10971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
20 2re 10495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
2120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
22 zre 10754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
23 peano2re 9646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
2422, 23syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
2521, 22, 243jca 1168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
2625adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
27 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2822lep1d 10368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
2928adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
30 letr 9572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3130imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3226, 27, 29, 31syl12anc 1217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
33323adant1 1006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3419, 33sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3534a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
36 eleq1 2523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3736eqcoms 2463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3837adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
39 breq2 4397 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
4039adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4135, 38, 403imtr4d 268 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4241ex 434 . . . . . . . . . . . . . . . . . . . . . . . . 25
4318, 42syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24 Word
4443adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23 Word ..^
4544imp 429 . . . . . . . . . . . . . . . . . . . . . 22 Word ..^
4645adantr 465 . . . . . . . . . . . . . . . . . . . . 21 Word ..^
4716, 46syl5com 30 . . . . . . . . . . . . . . . . . . . 20 Word ..^
48473ad2ant3 1011 . . . . . . . . . . . . . . . . . . 19 USGrph Word ..^
4948impcom 430 . . . . . . . . . . . . . . . . . 18 Word ..^ USGrph
50 simp-4r 766 . . . . . . . . . . . . . . . . . 18 Word ..^ USGrph ..^
51 clwlkisclwwlklem1 30590 . . . . . . . . . . . . . . . . . 18 USGrph Word ..^ lastS ..^
5214, 15, 49, 50, 51syl121anc 1224 . . . . . . . . . . . . . . . . 17 Word ..^ USGrph lastS ..^
533, 4, 1, 7clwlkfclwwlk1hash 30656 . . . . . . . . . . . . . . . . . . . . . . . 24
54 simp2 989 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word ..^ Word
55 simp1 988 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word ..^
56 elfzelz 11563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
57 peano2zm 10792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
58 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
5922lem1d 10370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
60 eluz2 10971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
6157, 58, 59, 60syl3anbrc 1172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
62 fzoss2 11687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ ..^
6356, 61, 623syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^ ..^
6463sselda 3457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ ..^
65643adant2 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word ..^ ..^
66 swrd0fv 12446 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word ..^ substr
6754, 55, 65, 66syl3anc 1219 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word ..^ substr
6867eqcomd 2459 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Word ..^ substr
69 elfzom1elp1fzo 30359 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ ..^
7056, 69sylan 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ ..^
71703adant2 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word ..^ ..^
72 swrd0fv 12446 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word ..^ substr
7372eqcomd 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word ..^ substr
7454, 55, 71, 73syl3anc 1219 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Word ..^ substr
7568, 74preq12d 4063 . . . . . . . . . . . . . . . . . . . . . . . . 25 Word ..^ substr substr
76753exp 1187 . . . . . . . . . . . . . . . . . . . . . . . 24 Word ..^ substr substr
7753, 8, 76sylc 60 . . . . . . . . . . . . . . . . . . . . . . 23 ..^ substr substr
7877imp 429 . . . . . . . . . . . . . . . . . . . . . 22 ..^ substr substr
7978eleq1d 2520 . . . . . . . . . . . . . . . . . . . . 21 ..^ substr substr
8079ralbidva 2839 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^ substr substr
8180ad2antlr 726 . . . . . . . . . . . . . . . . . . 19 Word ..^ USGrph ..^ ..^ substr substr
823, 4, 1, 7clwlkfclwwlk2sswd 30657 . . . . . . . . . . . . . . . . . . . . . . 23 substr
8382oveq1d 6208 . . . . . . . . . . . . . . . . . . . . . 22 substr
8483ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21 Word ..^ USGrph substr
8584oveq2d 6209 . . . . . . . . . . . . . . . . . . . 20 Word ..^ USGrph ..^ ..^ substr
8685raleqdv 3022 . . . . . . . . . . . . . . . . . . 19 Word ..^ USGrph ..^ substr substr ..^ substr substr substr
8781, 86bitrd 253 . . . . . . . . . . . . . . . . . 18 Word ..^ USGrph ..^ ..^ substr substr substr
88 eleq1 2523 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8988biimpd 207 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9089eqcoms 2463 . . . . . . . . . . . . . . . . . . . . . . . . . 26
91 prmnn 13877 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
92 elfz2nn0 11590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
93 1z 10780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
9493a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
95 nn0z 10773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
9695adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
97 nn0z 10773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
9897adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
9994, 96, 983jca 1168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
100993adant3 1008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
101100adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
102 simp3 990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
103 nnge1 10452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
104102, 103anim12ci 567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
105101, 104jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
10692, 105sylanb 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
107 elfz2 11554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
108106, 107sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
109 swrd0fvlsw 12450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Word lastS substr
110109eqcomd 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Word lastS substr
111 swrd0fv0 12447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Word substr
112111eqcomd 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Word substr
113110, 112preq12d 4063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Word lastS substr substr
114113expcom 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Word lastS substr substr
115108, 114syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Word lastS substr substr
116115ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word lastS substr substr
117116com23 78 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word lastS substr substr
11853, 8, 117sylc 60 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 lastS substr substr
11991, 118syl5com 30 . . . . . . . . . . . . . . . . . . . . . . . . . 26 lastS substr substr
12090, 119syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . 25 lastS substr substr
121120com23 78 . . . . . . . . . . . . . . . . . . . . . . . 24 lastS substr substr
122121adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23 Word ..^ lastS substr substr
123122imp 429 . . . . . . . . . . . . . . . . . . . . . 22 Word ..^ lastS substr substr
124123com12 31 . . . . . . . . . . . . . . . . . . . . 21 Word ..^ lastS substr substr
1251243ad2ant3 1011 . . . . . . . . . . . . . . . . . . . 20 USGrph Word ..^ lastS substr substr
126125impcom 430 . . . . . . . . . . . . . . . . . . 19 Word ..^ USGrph lastS substr substr
127126eleq1d 2520 . . . . . . . . . . . . . . . . . 18 Word ..^ USGrph lastS substr substr
12887, 1273anbi23d 1293 . . . . . . . . . . . . . . . . 17 Word ..^ USGrph lastS ..^ lastS ..^ substr substr substr lastS substr substr
12952, 128mpbid 210 . . . . . . . . . . . . . . . 16 Word ..^ USGrph lastS ..^ substr substr substr lastS substr substr
130 3simpc 987 . . . . . . . . . . . . . . . 16 lastS ..^ substr substr substr lastS substr substr ..^ substr substr substr lastS substr substr
131129, 130syl 16 . . . . . . . . . . . . . . 15 Word ..^ USGrph ..^ substr substr substr lastS substr substr
132 3anass 969 . . . . . . . . . . . . . . 15 substr Word ..^ substr substr substr lastS substr substr substr Word ..^ substr substr substr lastS substr substr
13311, 131, 132sylanbrc 664 . . . . . . . . . . . . . 14 Word ..^ USGrph substr Word ..^ substr substr substr lastS substr substr
134 usgrav 23415 . . . . . . . . . . . . . . . . 17 USGrph
1351343ad2ant1 1009 . . . . . . . . . . . . . . . 16 USGrph
136135adantl 466 . . . . . . . . . . . . . . 15 Word ..^ USGrph
137 isclwwlk 30572 . . . . . . . . . . . . . . 15 substr ClWWalks substr Word ..^ substr substr substr lastS substr substr
138136, 137syl 16 . . . . . . . . . . . . . 14 Word ..^ USGrph substr ClWWalks substr Word ..^ substr substr substr lastS substr substr
139133, 138mpbird 232 . . . . . . . . . . . . 13 Word ..^ USGrph substr ClWWalks
14082eqeq1d 2453 . . . . . . . . . . . . . . . . 17 substr
141140biimpcd 224 . . . . . . . . . . . . . . . 16 substr
142141adantl 466 . . . . . . . . . . . . . . 15 Word ..^ substr
143142imp 429 . . . . . . . . . . . . . 14 Word ..^ substr
144143adantr 465 . . . . . . . . . . . . 13 Word ..^ USGrph substr
145139, 144jca 532 . . . . . . . . . . . 12 Word ..^ USGrph substr ClWWalks substr
146134simpld 459 . . . . . . . . . . . . . . . . 17 USGrph
147146adantr 465 . . . . . . . . . . . . . . . 16 USGrph
148134simprd 463 . . . . . . . . . . . . . . . . 17 USGrph
149148adantr 465 . . . . . . . . . . . . . . . 16 USGrph
150 prmnn 13877 . . . . . . . . . . . . . . . . . 18
151150nnnn0d 10740 . . . . . . . . . . . . . . . . 17
152151adantl 466 . . . . . . . . . . . . . . . 16 USGrph
153147, 149, 1523jca 1168 . . . . . . . . . . . . . . 15 USGrph
1541533adant2 1007 . . . . . . . . . . . . . 14 USGrph
155154adantl 466 . . . . . . . . . . . . 13 Word ..^ USGrph
156 isclwwlkn 30573 . . . . . . . . . . . . 13 substr ClWWalksN substr ClWWalks substr
157155, 156syl 16 . . . . . . . . . . . 12 Word ..^ USGrph substr ClWWalksN substr ClWWalks substr
158145, 157mpbird 232 . . . . . . . . . . 11 Word ..^ USGrph substr ClWWalksN
159158exp31 604 . . . . . . . . . 10 Word ..^ USGrph substr ClWWalksN
160159exp41 610 . . . . . . . . 9 Word ..^ USGrph substr ClWWalksN
1616, 160mpancom 669 . . . . . . . 8 Word ..^ USGrph substr ClWWalksN
162161imp31 432 . . . . . . 7 Word ..^ USGrph substr ClWWalksN
1635, 162syl 16 . . . . . 6 ClWalks USGrph substr ClWWalksN
164163imp 429 . . . . 5 ClWalks USGrph substr ClWWalksN
1652, 164sylbi 195 . . . 4 USGrph substr ClWWalksN
166165pm2.43i 47 . . 3 USGrph substr ClWWalksN
167166impcom 430 . 2 USGrph substr ClWWalksN
168167, 7fmptd 5969 1 USGrph ClWWalksN
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   w3a 965   wceq 1370   wcel 1758  wral 2795  crab 2799  cvv 3071   wss 3429  cpr 3980  cop 3984   class class class wbr 4393   cmpt 4451   cdm 4941   crn 4942  wf 5515  cfv 5519  (class class class)co 6193  c1st 6678  c2nd 6679  cfn 7413  cr 9385  cc0 9386  c1 9387   caddc 9389   cle 9523   cmin 9699  cn 10426  c2 10475  cn0 10683  cz 10750  cuz 10965  cfz 11547  ..^cfzo 11658  chash 12213  Word cword 12332   lastS clsw 12333   substr csubstr 12336  cprime 13874   USGrph cusg 23409   ClWalks cclwlk 30553   ClWWalks cclwwlk 30554   ClWWalksN cclwwlkn 30555 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-rep 4504  ax-sep 4514  ax-nul 4522  ax-pow 4571  ax-pr 4632  ax-un 6475  ax-cnex 9442  ax-resscn 9443  ax-1cn 9444  ax-icn 9445  ax-addcl 9446  ax-addrcl 9447  ax-mulcl 9448  ax-mulrcl 9449  ax-mulcom 9450  ax-addass 9451  ax-mulass 9452  ax-distr 9453  ax-i2m1 9454  ax-1ne0 9455  ax-1rid 9456  ax-rnegex 9457  ax-rrecex 9458  ax-cnre 9459  ax-pre-lttri 9460  ax-pre-lttrn 9461  ax-pre-ltadd 9462  ax-pre-mulgt0 9463 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-reu 2802  df-rmo 2803  df-rab 2804  df-v 3073  df-sbc 3288  df-csb 3390  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-pss 3445  df-nul 3739  df-if 3893  df-pw 3963  df-sn 3979  df-pr 3981  df-tp 3983  df-op 3985  df-uni 4193  df-int 4230  df-iun 4274  df-br 4394  df-opab 4452  df-mpt 4453  df-tr 4487  df-eprel 4733  df-id 4737  df-po 4742  df-so 4743  df-fr 4780  df-we 4782  df-ord 4823  df-on 4824  df-lim 4825  df-suc 4826  df-xp 4947  df-rel 4948  df-cnv 4949  df-co 4950  df-dm 4951  df-rn 4952  df-res 4953  df-ima 4954  df-iota 5482  df-fun 5521  df-fn 5522  df-f 5523  df-f1 5524  df-fo 5525  df-f1o 5526  df-fv 5527  df-riota 6154  df-ov 6196  df-oprab 6197  df-mpt2 6198  df-om 6580  df-1st 6680  df-2nd 6681  df-recs 6935  df-rdg 6969  df-1o 7023  df-2o 7024  df-oadd 7027  df-er 7204  df-map 7319  df-pm 7320  df-en 7414  df-dom 7415  df-sdom 7416  df-fin 7417  df-card 8213  df-cda 8441  df-pnf 9524  df-mnf 9525  df-xr 9526  df-ltxr 9527  df-le 9528  df-sub 9701  df-neg 9702  df-nn 10427  df-2 10484  df-n0 10684  df-z 10751  df-uz 10966  df-fz 11548  df-fzo 11659  df-hash 12214  df-word 12340  df-lsw 12341  df-substr 12344  df-dvds 13647  df-prm 13875  df-usgra 23411  df-wlk 23560  df-clwlk 30556  df-clwwlk 30557  df-clwwlkn 30558 This theorem is referenced by:  clwlkfoclwwlk  30659  clwlkf1clwwlk  30664
 Copyright terms: Public domain W3C validator