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

Theorem swrdccat 12718
Description: The subword of a concatenation of two words as concatenation of subwords of the two concatenated words. (Contributed by Alexander van der Vekens, 29-May-2018.)
Hypothesis
Ref Expression
swrdccatin12.l
Assertion
Ref Expression
swrdccat

Proof of Theorem swrdccat
StepHypRef Expression
1 swrdccatin12.l . . . . 5
21swrdccat3 12717 . . . 4
32imp 429 . . 3
4 lencl 12562 . . . . . 6
54adantr 465 . . . . 5
61eqcomi 2470 . . . . . . 7
76eleq1i 2534 . . . . . 6
8 elfz2nn0 11798 . . . . . . . . 9
9 iftrue 3947 . . . . . . . . . . . . . . . . . 18
109adantl 466 . . . . . . . . . . . . . . . . 17
1110opeq2d 4224 . . . . . . . . . . . . . . . 16
1211oveq2d 6312 . . . . . . . . . . . . . . 15
13 iftrue 3947 . . . . . . . . . . . . . . . . . . . 20
1413opeq1d 4223 . . . . . . . . . . . . . . . . . . 19
1514oveq2d 6312 . . . . . . . . . . . . . . . . . 18
1615adantr 465 . . . . . . . . . . . . . . . . 17
17 simpr 461 . . . . . . . . . . . . . . . . . . . . 21
18 nn0z 10912 . . . . . . . . . . . . . . . . . . . . . 22
19 nn0z 10912 . . . . . . . . . . . . . . . . . . . . . . . . 25
2019adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
21 zsubcl 10931 . . . . . . . . . . . . . . . . . . . . . . . 24
2220, 21sylan 471 . . . . . . . . . . . . . . . . . . . . . . 23
23 nn0z 10912 . . . . . . . . . . . . . . . . . . . . . . . . 25
2423adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24
25 zsubcl 10931 . . . . . . . . . . . . . . . . . . . . . . . 24
2624, 25sylan 471 . . . . . . . . . . . . . . . . . . . . . . 23
2722, 26jca 532 . . . . . . . . . . . . . . . . . . . . . 22
2818, 27sylan2 474 . . . . . . . . . . . . . . . . . . . . 21
2917, 28anim12i 566 . . . . . . . . . . . . . . . . . . . 20
30 3anass 977 . . . . . . . . . . . . . . . . . . . 20
3129, 30sylibr 212 . . . . . . . . . . . . . . . . . . 19
3231ad2antrl 727 . . . . . . . . . . . . . . . . . 18
33 nn0re 10829 . . . . . . . . . . . . . . . . . . . . . . . 24
34 nn0re 10829 . . . . . . . . . . . . . . . . . . . . . . . 24
3533, 34anim12i 566 . . . . . . . . . . . . . . . . . . . . . . 23
36 nn0re 10829 . . . . . . . . . . . . . . . . . . . . . . 23
37 subge0 10090 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3837adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25
39 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
4039adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
41 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
42 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
4342adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
4440, 41, 433jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
45 letr 9699 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4644, 45syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4746expcomd 438 . . . . . . . . . . . . . . . . . . . . . . . . 25
4838, 47sylbid 215 . . . . . . . . . . . . . . . . . . . . . . . 24
4948com23 78 . . . . . . . . . . . . . . . . . . . . . . 23
5035, 36, 49syl2an 477 . . . . . . . . . . . . . . . . . . . . . 22
5150adantl 466 . . . . . . . . . . . . . . . . . . . . 21
5251imp 429 . . . . . . . . . . . . . . . . . . . 20
5352impcom 430 . . . . . . . . . . . . . . . . . . 19
5434adantl 466 . . . . . . . . . . . . . . . . . . . . . . . 24
5554adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23
5633adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
5756adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23
5836adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23
5955, 57, 583jca 1176 . . . . . . . . . . . . . . . . . . . . . 22
6059adantl 466 . . . . . . . . . . . . . . . . . . . . 21
6160ad2antrl 727 . . . . . . . . . . . . . . . . . . . 20
62 lesub1 10071 . . . . . . . . . . . . . . . . . . . 20
6361, 62syl 16 . . . . . . . . . . . . . . . . . . 19
6453, 63mpbid 210 . . . . . . . . . . . . . . . . . 18
65 swrdlend 12656 . . . . . . . . . . . . . . . . . 18
6632, 64, 65sylc 60 . . . . . . . . . . . . . . . . 17
6716, 66eqtrd 2498 . . . . . . . . . . . . . . . 16
68 iffalse 3950 . . . . . . . . . . . . . . . . . . 19
6968opeq1d 4223 . . . . . . . . . . . . . . . . . 18
7069oveq2d 6312 . . . . . . . . . . . . . . . . 17
7117adantr 465 . . . . . . . . . . . . . . . . . . . 20
7271adantr 465 . . . . . . . . . . . . . . . . . . 19
73 0zd 10901 . . . . . . . . . . . . . . . . . . 19
7424, 18, 25syl2an 477 . . . . . . . . . . . . . . . . . . . . 21
7574adantl 466 . . . . . . . . . . . . . . . . . . . 20
7675adantr 465 . . . . . . . . . . . . . . . . . . 19
7772, 73, 763jca 1176 . . . . . . . . . . . . . . . . . 18
7854, 36anim12i 566 . . . . . . . . . . . . . . . . . . . . 21
7978adantl 466 . . . . . . . . . . . . . . . . . . . 20
80 suble0 10091 . . . . . . . . . . . . . . . . . . . 20
8179, 80syl 16 . . . . . . . . . . . . . . . . . . 19
8281biimpar 485 . . . . . . . . . . . . . . . . . 18
83 swrdlend 12656 . . . . . . . . . . . . . . . . . 18
8477, 82, 83sylc 60 . . . . . . . . . . . . . . . . 17
8570, 84sylan9eq 2518 . . . . . . . . . . . . . . . 16
8667, 85pm2.61ian 790 . . . . . . . . . . . . . . 15
8712, 86oveq12d 6314 . . . . . . . . . . . . . 14
88 swrdcl 12646 . . . . . . . . . . . . . . . . . 18
89 ccatrid 12604 . . . . . . . . . . . . . . . . . 18
9088, 89syl 16 . . . . . . . . . . . . . . . . 17
9190adantr 465 . . . . . . . . . . . . . . . 16
9291adantr 465 . . . . . . . . . . . . . . 15
9392adantr 465 . . . . . . . . . . . . . 14
9487, 93eqtrd 2498 . . . . . . . . . . . . 13
95 iffalse 3950 . . . . . . . . . . . . . . . . . . 19
96953ad2ant2 1018 . . . . . . . . . . . . . . . . . 18
9796opeq2d 4224 . . . . . . . . . . . . . . . . 17
9897oveq2d 6312 . . . . . . . . . . . . . . . 16
99 simpl 457 . . . . . . . . . . . . . . . . . . . . 21
10099, 20, 183anim123i 1181 . . . . . . . . . . . . . . . . . . . 20
1011003expb 1197 . . . . . . . . . . . . . . . . . . 19
102 swrdlend 12656 . . . . . . . . . . . . . . . . . . 19
103101, 102syl 16 . . . . . . . . . . . . . . . . . 18
104103imp 429 . . . . . . . . . . . . . . . . 17
1051043adant2 1015 . . . . . . . . . . . . . . . 16
10698, 105eqtrd 2498 . . . . . . . . . . . . . . 15
10756, 36, 37syl2an 477 . . . . . . . . . . . . . . . . . . . . 21
108107biimprd 223 . . . . . . . . . . . . . . . . . . . 20
109108adantl 466 . . . . . . . . . . . . . . . . . . 19
110109imp 429 . . . . . . . . . . . . . . . . . 18
1111103adant2 1015 . . . . . . . . . . . . . . . . 17
112111, 14syl 16 . . . . . . . . . . . . . . . 16
113112oveq2d 6312 . . . . . . . . . . . . . . 15
114106, 113oveq12d 6314 . . . . . . . . . . . . . 14
115 swrdcl 12646 . . . . . . . . . . . . . . . . . 18
116115adantl 466 . . . . . . . . . . . . . . . . 17
117 ccatlid 12603 . . . . . . . . . . . . . . . . 17
118116, 117syl 16 . . . . . . . . . . . . . . . 16
119118adantr 465 . . . . . . . . . . . . . . 15
1201193ad2ant1 1017 . . . . . . . . . . . . . 14
121114, 120eqtrd 2498 . . . . . . . . . . . . 13
122953ad2ant2 1018 . . . . . . . . . . . . . . . 16
123122opeq2d 4224 . . . . . . . . . . . . . . 15
124123oveq2d 6312 . . . . . . . . . . . . . 14
12533, 36, 37syl2an 477 . . . . . . . . . . . . . . . . . . . . . 22
126125adantlr 714 . . . . . . . . . . . . . . . . . . . . 21
127126adantl 466 . . . . . . . . . . . . . . . . . . . 20
128127biimpd 207 . . . . . . . . . . . . . . . . . . 19
129128con3dimp 441 . . . . . . . . . . . . . . . . . 18
1301293adant2 1015 . . . . . . . . . . . . . . . . 17
131130, 68syl 16 . . . . . . . . . . . . . . . 16
132131opeq1d 4223 . . . . . . . . . . . . . . 15
133132oveq2d 6312 . . . . . . . . . . . . . 14
134124, 133oveq12d 6314 . . . . . . . . . . . . 13
13594, 121, 1342if2 3989 . . . . . . . . . . . 12
136135exp32 605 . . . . . . . . . . 11
137136com12 31 . . . . . . . . . 10
1381373adant3 1016 . . . . . . . . 9
1398, 138sylbi 195 . . . . . . . 8 </