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

Theorem swrdccat3 12771
 Description: The subword of a concatenation is either a subword of the first concatenated word or a subword of the second concatenated word or a concatenation of a suffix of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 28-May-2018.)
Hypothesis
Ref Expression
swrdccatin12.l
Assertion
Ref Expression
swrdccat3 Word Word ++ substr substr substr substr ++ substr

Proof of Theorem swrdccat3
StepHypRef Expression
1 simpll 752 . . . 4 Word Word Word Word
2 simplrl 762 . . . . 5 Word Word
3 lencl 12612 . . . . . . . . 9 Word
4 elfznn0 11824 . . . . . . . . . . . . . 14
54adantr 463 . . . . . . . . . . . . 13
65adantr 463 . . . . . . . . . . . 12
7 simplr 754 . . . . . . . . . . . 12
8 swrdccatin12.l . . . . . . . . . . . . . . 15
98breq2i 4402 . . . . . . . . . . . . . 14
109biimpi 194 . . . . . . . . . . . . 13
1110adantl 464 . . . . . . . . . . . 12
12 elfz2nn0 11822 . . . . . . . . . . . 12
136, 7, 11, 12syl3anbrc 1181 . . . . . . . . . . 11
1413exp31 602 . . . . . . . . . 10
1514adantl 464 . . . . . . . . 9
163, 15syl5com 28 . . . . . . . 8 Word
1716adantr 463 . . . . . . 7 Word Word
1817imp 427 . . . . . 6 Word Word
1918imp 427 . . . . 5 Word Word
202, 19jca 530 . . . 4 Word Word
21 swrdccatin1 12762 . . . 4 Word Word ++ substr substr
221, 20, 21sylc 59 . . 3 Word Word ++ substr substr
23 simp1l 1021 . . . 4 Word Word Word Word
248eleq1i 2479 . . . . . . . . . . 11
25 elfz2nn0 11822 . . . . . . . . . . . . . 14
26 nn0z 10927 . . . . . . . . . . . . . . . . . . 19
2726adantl 464 . . . . . . . . . . . . . . . . . 18
28 nn0z 10927 . . . . . . . . . . . . . . . . . . . 20
29283ad2ant2 1019 . . . . . . . . . . . . . . . . . . 19
3029adantr 463 . . . . . . . . . . . . . . . . . 18
31 nn0z 10927 . . . . . . . . . . . . . . . . . . . 20
32313ad2ant1 1018 . . . . . . . . . . . . . . . . . . 19
3332adantr 463 . . . . . . . . . . . . . . . . . 18
3427, 30, 333jca 1177 . . . . . . . . . . . . . . . . 17
3534adantr 463 . . . . . . . . . . . . . . . 16
36 simpl3 1002 . . . . . . . . . . . . . . . . . 18
3736anim1i 566 . . . . . . . . . . . . . . . . 17
3837ancomd 449 . . . . . . . . . . . . . . . 16
39 elfz2 11731 . . . . . . . . . . . . . . . 16
4035, 38, 39sylanbrc 662 . . . . . . . . . . . . . . 15
4140exp31 602 . . . . . . . . . . . . . 14
4225, 41sylbi 195 . . . . . . . . . . . . 13
4342adantr 463 . . . . . . . . . . . 12
4443com12 29 . . . . . . . . . . 11
4524, 44sylbir 213 . . . . . . . . . 10
463, 45syl 17 . . . . . . . . 9 Word
4746adantr 463 . . . . . . . 8 Word Word
4847imp 427 . . . . . . 7 Word Word
4948a1d 25 . . . . . 6 Word Word
50493imp 1191 . . . . 5 Word Word
51 elfz2nn0 11822 . . . . . . . . . . . 12
52 nn0z 10927 . . . . . . . . . . . . . . . . . 18
538, 52syl5eqel 2494 . . . . . . . . . . . . . . . . 17
5453adantr 463 . . . . . . . . . . . . . . . 16
5554adantl 464 . . . . . . . . . . . . . . 15
56 nn0z 10927 . . . . . . . . . . . . . . . . 17
57563ad2ant2 1019 . . . . . . . . . . . . . . . 16
5857adantr 463 . . . . . . . . . . . . . . 15
59283ad2ant1 1018 . . . . . . . . . . . . . . . 16
6059adantr 463 . . . . . . . . . . . . . . 15
6155, 58, 603jca 1177 . . . . . . . . . . . . . 14
628eqcomi 2415 . . . . . . . . . . . . . . . . . . 19
6362eleq1i 2479 . . . . . . . . . . . . . . . . . 18
64 nn0re 10844 . . . . . . . . . . . . . . . . . . . . . 22
65 nn0re 10844 . . . . . . . . . . . . . . . . . . . . . 22
66 ltnle 9694 . . . . . . . . . . . . . . . . . . . . . 22
6764, 65, 66syl2anr 476 . . . . . . . . . . . . . . . . . . . . 21
6867bicomd 201 . . . . . . . . . . . . . . . . . . . 20
69 ltle 9703 . . . . . . . . . . . . . . . . . . . . 21
7064, 65, 69syl2anr 476 . . . . . . . . . . . . . . . . . . . 20
7168, 70sylbid 215 . . . . . . . . . . . . . . . . . . 19
7271ex 432 . . . . . . . . . . . . . . . . . 18
7363, 72syl5bi 217 . . . . . . . . . . . . . . . . 17
74733ad2ant1 1018 . . . . . . . . . . . . . . . 16
7574imp32 431 . . . . . . . . . . . . . . 15
76 simpl3 1002 . . . . . . . . . . . . . . 15
7775, 76jca 530 . . . . . . . . . . . . . 14
78 elfz2 11731 . . . . . . . . . . . . . 14
7961, 77, 78sylanbrc 662 . . . . . . . . . . . . 13
8079exp32 603 . . . . . . . . . . . 12
8151, 80sylbi 195 . . . . . . . . . . 11
8281adantl 464 . . . . . . . . . 10
833, 82syl5com 28 . . . . . . . . 9 Word
8483adantr 463 . . . . . . . 8 Word Word
8584imp 427 . . . . . . 7 Word Word
8685a1dd 44 . . . . . 6 Word Word
87863imp 1191 . . . . 5 Word Word
8850, 87jca 530 . . . 4 Word Word
898swrdccatin2 12766 . . . 4 Word Word ++ substr substr
9023, 88, 89sylc 59 . . 3 Word Word ++ substr substr
91 simp1l 1021 . . . 4 Word Word Word Word
92 nn0re 10844 . . . . . . . . . . . . . . . . . . 19
9392adantr 463 . . . . . . . . . . . . . . . . . 18
94 ltnle 9694 . . . . . . . . . . . . . . . . . 18
9593, 64, 94syl2anr 476 . . . . . . . . . . . . . . . . 17
9695bicomd 201 . . . . . . . . . . . . . . . 16
97 simpll 752 . . . . . . . . . . . . . . . . . . . 20
98 simplr 754 . . . . . . . . . . . . . . . . . . . 20
99 ltle 9703 . . . . . . . . . . . . . . . . . . . . . 22
10092, 64, 99syl2an 475 . . . . . . . . . . . . . . . . . . . . 21
101100imp 427 . . . . . . . . . . . . . . . . . . . 20
102 elfz2nn0 11822 . . . . . . . . . . . . . . . . . . . 20
10397, 98, 101, 102syl3anbrc 1181 . . . . . . . . . . . . . . . . . . 19
104103exp31 602 . . . . . . . . . . . . . . . . . 18
105104adantr 463 . . . . . . . . . . . . . . . . 17
106105impcom 428 . . . . . . . . . . . . . . . 16
10796, 106sylbid 215 . . . . . . . . . . . . . . 15
108107expcom 433 . . . . . . . . . . . . . 14
1091083adant3 1017 . . . . . . . . . . . . 13
11025, 109sylbi 195 . . . . . . . . . . . 12
11163, 110syl5bi 217 . . . . . . . . . . 11
112111adantr 463 . . . . . . . . . 10
1133, 112syl5com 28 . . . . . . . . 9 Word
114113adantr 463 . . . . . . . 8 Word Word
115114imp 427 . . . . . . 7 Word Word
116115a1d 25 . . . . . 6 Word Word
1171163imp 1191 . . . . 5 Word Word
118653ad2ant1 1018 . . . . . . . . . . . . . . . . 17
11966bicomd 201 . . . . . . . . . . . . . . . . 17
12064, 118, 119syl2an 475 . . . . . . . . . . . . . . . 16
12126adantr 463 . . . . . . . . . . . . . . . . . . . 20
12257adantl 464 . . . . . . . . . . . . . . . . . . . 20
12359adantl 464 . . . . . . . . . . . . . . . . . . . 20
124121, 122, 1233jca 1177 . . . . . . . . . . . . . . . . . . 19
125124adantr 463 . . . . . . . . . . . . . . . . . 18
12664, 118, 69syl2an 475 . . . . . . . . . . . . . . . . . . . 20
127126imp 427 . . . . . . . . . . . . . . . . . . 19
128 simplr3 1041 . . . . . . . . . . . . . . . . . . 19
129127, 128jca 530 . . . . . . . . . . . . . . . . . 18
130125, 129, 78sylanbrc 662 . . . . . . . . . . . . . . . . 17
131130ex 432 . . . . . . . . . . . . . . . 16
132120, 131sylbid 215 . . . . . . . . . . . . . . 15
133132ex 432 . . . . . . . . . . . . . 14
13463, 133sylbi 195 . . . . . . . . . . . . 13
1353, 134syl 17 . . . . . . . . . . . 12 Word
136135adantr 463 . . . . . . . . . . 11 Word Word
137136com12 29 . . . . . . . . . 10 Word Word
13851, 137sylbi 195 . . . . . . . . 9 Word Word
139138adantl 464 . . . . . . . 8 Word Word
140139impcom 428 . . . . . . 7 Word Word
141140a1dd 44 . . . . . 6 Word Word
1421413imp 1191 . . . . 5 Word Word
143117, 142jca 530 . . . 4 Word Word
1448swrdccatin12 12770 . . . 4 Word Word ++ substr substr ++ substr
14591, 143, 144sylc 59 . . 3 Word Word ++ substr substr ++ substr
14622, 90, 1452if2 3932 . 2 Word Word ++ substr substr substr substr ++ substr
147146ex 432 1 Word Word ++ substr substr substr substr ++ substr
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184   wa 367   w3a 974   wceq 1405   wcel 1842  cif 3884  cop 3977   class class class wbr 4394  cfv 5568  (class class class)co 6277  cr 9520  cc0 9521   caddc 9524   clt 9657   cle 9658   cmin 9840  cn0 10835  cz 10904  cfz 11724  chash 12450  Word cword 12581   ++ cconcat 12583   substr csubstr 12585 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573  ax-cnex 9577  ax-resscn 9578  ax-1cn 9579  ax-icn 9580  ax-addcl 9581  ax-addrcl 9582  ax-mulcl 9583  ax-mulrcl 9584  ax-mulcom 9585  ax-addass 9586  ax-mulass 9587  ax-distr 9588  ax-i2m1 9589  ax-1ne0 9590  ax-1rid 9591  ax-rnegex 9592  ax-rrecex 9593  ax-cnre 9594  ax-pre-lttri 9595  ax-pre-lttrn 9596  ax-pre-ltadd 9597  ax-pre-mulgt0 9598 This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2758  df-rex 2759  df-reu 2760  df-rmo 2761  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-pss 3429  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-tp 3976  df-op 3978  df-uni 4191  df-int 4227  df-iun 4272  df-br 4395  df-opab 4453  df-mpt 4454  df-tr 4489  df-eprel 4733  df-id 4737  df-po 4743  df-so 4744  df-fr 4781  df-we 4783  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-pred 5366  df-ord 5412  df-on 5413  df-lim 5414  df-suc 5415  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576  df-riota 6239  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-om 6683  df-1st 6783  df-2nd 6784  df-wrecs 7012  df-recs 7074  df-rdg 7112  df-1o 7166  df-oadd 7170  df-er 7347  df-en 7554  df-dom 7555  df-sdom 7556  df-fin 7557  df-card 8351  df-cda 8579  df-pnf 9659  df-mnf 9660  df-xr 9661  df-ltxr 9662  df-le 9663  df-sub 9842  df-neg 9843  df-nn 10576  df-2 10634  df-n0 10836  df-z 10905  df-uz 11127  df-fz 11725  df-fzo 11853  df-hash 12451  df-word 12589  df-concat 12591  df-substr 12593 This theorem is referenced by:  swrdccat  12772  swrdccat3a  12773  swrdccat3b  12775
 Copyright terms: Public domain W3C validator