swrdccat - Metamath Proof Explorer

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

Theorem swrdccat 12774

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	Word $/\$ Word $/\$ ++ substr substr ++ substr

**Proof of Theorem swrdccat**
Step	Hyp	Ref	Expression
1		swrdccatin12.l	. . . . 5
2	1	swrdccat3 12773	. . . 4 Word $/\$ Word $/\$ ++ substr substr substr substr ++ substr
3	2	imp 427	. . 3 Word $/\$ Word $/\$ $/\$ ++ substr substr substr substr ++ substr
4		lencl 12614	. . . . . 6 Word
5	4	adantr 463	. . . . 5 Word $/\$ Word
6	1	eqcomi 2415	. . . . . . 7
7	6	eleq1i 2479	. . . . . 6
8		elfz2nn0 11824	. . . . . . . . 9 $/\$ $/\$
9		iftrue 3891	. . . . . . . . . . . . . . . . . 18
10	9	adantl 464	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
11	10	opeq2d 4166	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
12	11	oveq2d 6294	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr substr
13		iftrue 3891	. . . . . . . . . . . . . . . . . . . 20
14	13	opeq1d 4165	. . . . . . . . . . . . . . . . . . 19
15	14	oveq2d 6294	. . . . . . . . . . . . . . . . . 18 substr substr
16	15	adantr 463	. . . . . . . . . . . . . . . . 17 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr substr
17		simpr 459	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word Word
18		nn0z 10928	. . . . . . . . . . . . . . . . . . . . . 22
19		nn0z 10928	. . . . . . . . . . . . . . . . . . . . . . . . 25
20	19	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
21		zsubcl 10947	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
22	20, 21	sylan 469	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
23		nn0z 10928	. . . . . . . . . . . . . . . . . . . . . . . . 25
24	23	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
25		zsubcl 10947	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
26	24, 25	sylan 469	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
27	22, 26	jca 530	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
28	18, 27	sylan2 472	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
29	17, 28	anim12i 564	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
30		3anass 978	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ $/\$ Word $/\$ $/\$
31	29, 30	sylibr 212	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
32	31	ad2antrl 726	. . . . . . . . . . . . . . . . . 18 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word $/\$ $/\$
33		nn0re 10845	. . . . . . . . . . . . . . . . . . . . . . . 24
34		nn0re 10845	. . . . . . . . . . . . . . . . . . . . . . . 24
35	33, 34	anim12i 564	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
36		nn0re 10845	. . . . . . . . . . . . . . . . . . . . . . 23
37		subge0 10106	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
38	37	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
39		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
40	39	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
41		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
42		simpl 455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
43	42	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
44	40, 41, 43	3jca 1177	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
45		letr 9709	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
46	44, 45	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
47	46	expcomd 436	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
48	38, 47	sylbid 215	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
49	48	com23 78	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
50	35, 36, 49	syl2an 475	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
51	50	adantl 464	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$
52	51	imp 427	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
53	52	impcom 428	. . . . . . . . . . . . . . . . . . 19 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
54	34	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
55	54	adantr 463	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
56	33	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
57	56	adantr 463	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
58	36	adantl 464	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
59	55, 57, 58	3jca 1177	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
60	59	adantl 464	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
61	60	ad2antrl 726	. . . . . . . . . . . . . . . . . . . 20 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62		lesub1 10087	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
63	61, 62	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
64	53, 63	mpbid 210	. . . . . . . . . . . . . . . . . 18 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
65		swrdlend 12712	. . . . . . . . . . . . . . . . . 18 Word $/\$ $/\$ substr
66	32, 64, 65	sylc 59	. . . . . . . . . . . . . . . . 17 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
67	16, 66	eqtrd 2443	. . . . . . . . . . . . . . . 16 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
68		iffalse 3894	. . . . . . . . . . . . . . . . . . 19
69	68	opeq1d 4165	. . . . . . . . . . . . . . . . . 18
70	69	oveq2d 6294	. . . . . . . . . . . . . . . . 17 substr substr
71	17	adantr 463	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ Word
72	71	adantr 463	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word
73		0zd 10917	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
74	24, 18, 25	syl2an 475	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
75	74	adantl 464	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$
76	75	adantr 463	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
77	72, 73, 76	3jca 1177	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word $/\$ $/\$
78	54, 36	anim12i 564	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
79	78	adantl 464	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
80		suble0 10107	. . . . . . . . . . . . . . . . . . . 20 $/\$
81	79, 80	syl 17	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$
82	81	biimpar 483	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
83		swrdlend 12712	. . . . . . . . . . . . . . . . . 18 Word $/\$ $/\$ substr
84	77, 82, 83	sylc 59	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
85	70, 84	sylan9eq 2463	. . . . . . . . . . . . . . . 16 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
86	67, 85	pm2.61ian 791	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
87	12, 86	oveq12d 6296	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr ++ substr substr ++
88		swrdcl 12700	. . . . . . . . . . . . . . . . . 18 Word substr Word
89		ccatrid 12658	. . . . . . . . . . . . . . . . . 18 substr Word substr ++ substr
90	88, 89	syl 17	. . . . . . . . . . . . . . . . 17 Word substr ++ substr
91	90	adantr 463	. . . . . . . . . . . . . . . 16 Word $/\$ Word substr ++ substr
92	91	adantr 463	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ substr ++ substr
93	92	adantr 463	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr ++ substr
94	87, 93	eqtrd 2443	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr ++ substr substr
95		iffalse 3894	. . . . . . . . . . . . . . . . . . 19
96	95	3ad2ant2 1019	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
97	96	opeq2d 4166	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
98	97	oveq2d 6294	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
99		simpl 455	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word Word
100	99, 20, 18	3anim123i 1182	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
101	100	3expb 1198	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
102		swrdlend 12712	. . . . . . . . . . . . . . . . . . 19 Word $/\$ $/\$ substr
103	101, 102	syl 17	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ substr
104	103	imp 427	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
105	104	3adant2 1016	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr
106	98, 105	eqtrd 2443	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr
107	56, 36, 37	syl2an 475	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
108	107	biimprd 223	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
109	108	adantl 464	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$
110	109	imp 427	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
111	110	3adant2 1016	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
112	111, 14	syl 17	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
113	112	oveq2d 6294	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
114	106, 113	oveq12d 6296	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr ++ substr
115		swrdcl 12700	. . . . . . . . . . . . . . . . . 18 Word substr Word
116	115	adantl 464	. . . . . . . . . . . . . . . . 17 Word $/\$ Word substr Word
117		ccatlid 12657	. . . . . . . . . . . . . . . . 17 substr Word ++ substr substr
118	116, 117	syl 17	. . . . . . . . . . . . . . . 16 Word $/\$ Word ++ substr substr
119	118	adantr 463	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ ++ substr substr
120	119	3ad2ant1 1018	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ++ substr substr
121	114, 120	eqtrd 2443	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr substr
122	95	3ad2ant2 1019	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
123	122	opeq2d 4166	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
124	123	oveq2d 6294	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
125	33, 36, 37	syl2an 475	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
126	125	adantlr 713	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
127	126	adantl 464	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$
128	127	biimpd 207	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$
129	128	con3dimp 439	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
130	129	3adant2 1016	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
131	130, 68	syl 17	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
132	131	opeq1d 4165	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
133	132	oveq2d 6294	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
134	124, 133	oveq12d 6296	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr substr ++ substr
135	94, 121, 134	2if2 3933	. . . . . . . . . . . 12 Word $/\$ Word $/\$ $/\$ $/\$ substr ++ substr substr substr substr ++ substr
136	135	exp32 603	. . . . . . . . . . 11 Word $/\$ Word $/\$ substr ++ substr substr substr substr ++ substr
137	136	com12 29	. . . . . . . . . 10 $/\$ Word $/\$ Word substr ++ substr substr substr substr ++ substr
138	137	3adant3 1017	. . . . . . . . 9 $/\$ $/\$ Word $/\$ Word substr ++ substr substr substr substr ++ substr
139	8, 138	sylbi 195	. . . . . . . 8 Word $/\$ Word substr ++ substr substr substr substr ++ substr
140	139	adantr 463	. . . . . . 7 $/\$ Word $/\$ Word substr ++ substr substr substr substr ++ substr
141	140	com13 80	. . . . . 6 Word $/\$ Word $/\$ substr ++ substr substr substr substr ++ substr
142	7, 141	sylbi 195	. . . . 5 Word $/\$ Word $/\$ substr ++ substr substr substr substr ++ substr
143	5, 142	mpcom 34	. . . 4 Word $/\$ Word $/\$ substr ++ substr substr substr substr ++ substr
144	143	imp 427	. . 3 Word $/\$ Word $/\$ $/\$ substr ++ substr substr substr substr ++ substr
145	3, 144	eqtr4d 2446	. 2 Word $/\$ Word $/\$ $/\$ ++ substr substr ++ substr
146	145	ex 432	1 Word $/\$ Word $/\$ ++ 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

c0 3738

cif 3885

cop 3978 class class class wbr 4395

cfv 5569 (class class class)co 6278

cr 9521

cc0 9522

caddc 9525

cle 9659

cmin 9841

cn0 10836

cz 10905

cfz 11726

chash 12452 Word cword 12583 ++ cconcat 12585 substr csubstr 12587

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 4507 ax-sep 4517 ax-nul 4525 ax-pow 4572 ax-pr 4630 ax-un 6574 ax-cnex 9578 ax-resscn 9579 ax-1cn 9580 ax-icn 9581 ax-addcl 9582 ax-addrcl 9583 ax-mulcl 9584 ax-mulrcl 9585 ax-mulcom 9586 ax-addass 9587 ax-mulass 9588 ax-distr 9589 ax-i2m1 9590 ax-1ne0 9591 ax-1rid 9592 ax-rnegex 9593 ax-rrecex 9594 ax-cnre 9595 ax-pre-lttri 9596 ax-pre-lttrn 9597 ax-pre-ltadd 9598 ax-pre-mulgt0 9599

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 2759 df-rex 2760 df-reu 2761 df-rmo 2762 df-rab 2763 df-v 3061 df-sbc 3278 df-csb 3374 df-dif 3417 df-un 3419 df-in 3421 df-ss 3428 df-pss 3430 df-nul 3739 df-if 3886 df-pw 3957 df-sn 3973 df-pr 3975 df-tp 3977 df-op 3979 df-uni 4192 df-int 4228 df-iun 4273 df-br 4396 df-opab 4454 df-mpt 4455 df-tr 4490 df-eprel 4734 df-id 4738 df-po 4744 df-so 4745 df-fr 4782 df-we 4784 df-xp 4829 df-rel 4830 df-cnv 4831 df-co 4832 df-dm 4833 df-rn 4834 df-res 4835 df-ima 4836 df-pred 5367 df-ord 5413 df-on 5414 df-lim 5415 df-suc 5416 df-iota 5533 df-fun 5571 df-fn 5572 df-f 5573 df-f1 5574 df-fo 5575 df-f1o 5576 df-fv 5577 df-riota 6240 df-ov 6281 df-oprab 6282 df-mpt2 6283 df-om 6684 df-1st 6784 df-2nd 6785 df-wrecs 7013 df-recs 7075 df-rdg 7113 df-1o 7167 df-oadd 7171 df-er 7348 df-en 7555 df-dom 7556 df-sdom 7557 df-fin 7558 df-card 8352 df-cda 8580 df-pnf 9660 df-mnf 9661 df-xr 9662 df-ltxr 9663 df-le 9664 df-sub 9843 df-neg 9844 df-nn 10577 df-2 10635 df-n0 10837 df-z 10906 df-uz 11128 df-fz 11727 df-fzo 11855 df-hash 12453 df-word 12591 df-concat 12593 df-substr 12595

This theorem is referenced by: (None)

W3C validator