swrdccat - Metamath Proof Explorer

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

Theorem swrdccat 12903

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 12902	. . . 4 Word $/\$ Word $/\$ ++ substr substr substr substr ++ substr
3	2	imp 436	. . 3 Word $/\$ Word $/\$ $/\$ ++ substr substr substr substr ++ substr
4		lencl 12737	. . . . . 6 Word
5	4	adantr 472	. . . . 5 Word $/\$ Word
6	1	eqcomi 2480	. . . . . . 7
7	6	eleq1i 2540	. . . . . 6
8		elfz2nn0 11911	. . . . . . . . 9 $/\$ $/\$
9		iftrue 3878	. . . . . . . . . . . . . . . . . 18
10	9	adantl 473	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
11	10	opeq2d 4165	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
12	11	oveq2d 6324	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr substr
13		iftrue 3878	. . . . . . . . . . . . . . . . . . . 20
14	13	opeq1d 4164	. . . . . . . . . . . . . . . . . . 19
15	14	oveq2d 6324	. . . . . . . . . . . . . . . . . 18 substr substr
16	15	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr substr
17		simpr 468	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word Word
18		nn0z 10984	. . . . . . . . . . . . . . . . . . . . . 22
19		nn0z 10984	. . . . . . . . . . . . . . . . . . . . . . . . 25
20	19	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
21		zsubcl 11003	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
22	20, 21	sylan 479	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
23		nn0z 10984	. . . . . . . . . . . . . . . . . . . . . . . . 25
24	23	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
25		zsubcl 11003	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
26	24, 25	sylan 479	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
27	22, 26	jca 541	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
28	18, 27	sylan2 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
29	17, 28	anim12i 576	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
30		3anass 1011	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ $/\$ Word $/\$ $/\$
31	29, 30	sylibr 217	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
32	31	ad2antrl 742	. . . . . . . . . . . . . . . . . 18 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word $/\$ $/\$
33		nn0re 10902	. . . . . . . . . . . . . . . . . . . . . . . 24
34		nn0re 10902	. . . . . . . . . . . . . . . . . . . . . . . 24
35	33, 34	anim12i 576	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
36		nn0re 10902	. . . . . . . . . . . . . . . . . . . . . . 23
37		subge0 10148	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
38	37	adantlr 729	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
39		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
40	39	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
41		simpr 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
42		simpl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
43	42	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
44	40, 41, 43	3jca 1210	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
45		letr 9745	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
46	44, 45	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
47	46	expcomd 445	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
48	38, 47	sylbid 223	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
49	48	com23 80	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
50	35, 36, 49	syl2an 485	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
51	50	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$
52	51	imp 436	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
53	52	impcom 437	. . . . . . . . . . . . . . . . . . 19 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
54	34	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
55	54	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
56	33	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
57	56	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
58	36	adantl 473	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
59	55, 57, 58	3jca 1210	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
60	59	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
61	60	ad2antrl 742	. . . . . . . . . . . . . . . . . . . 20 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62		lesub1 10129	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
63	61, 62	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
64	53, 63	mpbid 215	. . . . . . . . . . . . . . . . . 18 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
65		swrdlend 12841	. . . . . . . . . . . . . . . . . 18 Word $/\$ $/\$ substr
66	32, 64, 65	sylc 61	. . . . . . . . . . . . . . . . 17 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
67	16, 66	eqtrd 2505	. . . . . . . . . . . . . . . 16 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
68		iffalse 3881	. . . . . . . . . . . . . . . . . . 19
69	68	opeq1d 4164	. . . . . . . . . . . . . . . . . 18
70	69	oveq2d 6324	. . . . . . . . . . . . . . . . 17 substr substr
71	17	adantr 472	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ Word
72	71	adantr 472	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word
73		0zd 10973	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
74	24, 18, 25	syl2an 485	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
75	74	adantl 473	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$
76	75	adantr 472	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
77	72, 73, 76	3jca 1210	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word $/\$ $/\$
78	54, 36	anim12i 576	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
79	78	adantl 473	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
80		suble0 10149	. . . . . . . . . . . . . . . . . . . 20 $/\$
81	79, 80	syl 17	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$
82	81	biimpar 493	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
83		swrdlend 12841	. . . . . . . . . . . . . . . . . 18 Word $/\$ $/\$ substr
84	77, 82, 83	sylc 61	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
85	70, 84	sylan9eq 2525	. . . . . . . . . . . . . . . 16 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
86	67, 85	pm2.61ian 807	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
87	12, 86	oveq12d 6326	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr ++ substr substr ++
88		swrdcl 12829	. . . . . . . . . . . . . . . . . 18 Word substr Word
89		ccatrid 12782	. . . . . . . . . . . . . . . . . 18 substr Word substr ++ substr
90	88, 89	syl 17	. . . . . . . . . . . . . . . . 17 Word substr ++ substr
91	90	adantr 472	. . . . . . . . . . . . . . . 16 Word $/\$ Word substr ++ substr
92	91	adantr 472	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ substr ++ substr
93	92	adantr 472	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr ++ substr
94	87, 93	eqtrd 2505	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr ++ substr substr
95		iffalse 3881	. . . . . . . . . . . . . . . . . . 19
96	95	3ad2ant2 1052	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
97	96	opeq2d 4165	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
98	97	oveq2d 6324	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
99		simpl 464	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word Word
100	99, 20, 18	3anim123i 1215	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
101	100	3expb 1232	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
102		swrdlend 12841	. . . . . . . . . . . . . . . . . . 19 Word $/\$ $/\$ substr
103	101, 102	syl 17	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ substr
104	103	imp 436	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
105	104	3adant2 1049	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr
106	98, 105	eqtrd 2505	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr
107	56, 36, 37	syl2an 485	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
108	107	biimprd 231	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
109	108	adantl 473	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$
110	109	imp 436	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
111	110	3adant2 1049	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
112	111, 14	syl 17	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
113	112	oveq2d 6324	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
114	106, 113	oveq12d 6326	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr ++ substr
115		swrdcl 12829	. . . . . . . . . . . . . . . . . 18 Word substr Word
116	115	adantl 473	. . . . . . . . . . . . . . . . 17 Word $/\$ Word substr Word
117		ccatlid 12781	. . . . . . . . . . . . . . . . 17 substr Word ++ substr substr
118	116, 117	syl 17	. . . . . . . . . . . . . . . 16 Word $/\$ Word ++ substr substr
119	118	adantr 472	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ ++ substr substr
120	119	3ad2ant1 1051	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ++ substr substr
121	114, 120	eqtrd 2505	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr substr
122	95	3ad2ant2 1052	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
123	122	opeq2d 4165	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
124	123	oveq2d 6324	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
125	33, 36, 37	syl2an 485	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
126	125	adantlr 729	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
127	126	adantl 473	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$
128	127	biimpd 212	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$
129	128	con3dimp 448	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
130	129	3adant2 1049	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
131	130, 68	syl 17	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
132	131	opeq1d 4164	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
133	132	oveq2d 6324	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
134	124, 133	oveq12d 6326	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr substr ++ substr
135	94, 121, 134	2if2 3920	. . . . . . . . . . . 12 Word $/\$ Word $/\$ $/\$ $/\$ substr ++ substr substr substr substr ++ substr
136	135	exp32 616	. . . . . . . . . . 11 Word $/\$ Word $/\$ substr ++ substr substr substr substr ++ substr
137	136	com12 31	. . . . . . . . . 10 $/\$ Word $/\$ Word substr ++ substr substr substr substr ++ substr
138	137	3adant3 1050	. . . . . . . . 9 $/\$ $/\$ Word $/\$ Word substr ++ substr substr substr substr ++ substr
139	8, 138	sylbi 200	. . . . . . . 8 Word $/\$ Word substr ++ substr substr substr substr ++ substr
140	139	adantr 472	. . . . . . 7 $/\$ Word $/\$ Word substr ++ substr substr substr substr ++ substr
141	140	com13 82	. . . . . 6 Word $/\$ Word $/\$ substr ++ substr substr substr substr ++ substr
142	7, 141	sylbi 200	. . . . 5 Word $/\$ Word $/\$ substr ++ substr substr substr substr ++ substr
143	5, 142	mpcom 36	. . . 4 Word $/\$ Word $/\$ substr ++ substr substr substr substr ++ substr
144	143	imp 436	. . 3 Word $/\$ Word $/\$ $/\$ substr ++ substr substr substr substr ++ substr
145	3, 144	eqtr4d 2508	. 2 Word $/\$ Word $/\$ $/\$ ++ substr substr ++ substr
146	145	ex 441	1 Word $/\$ Word $/\$ ++ substr substr ++ substr

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

c0 3722

cif 3872

cop 3965 class class class wbr 4395

cfv 5589 (class class class)co 6308

cr 9556

cc0 9557

caddc 9560

cle 9694

cmin 9880

cn0 10893

cz 10961

cfz 11810

chash 12553 Word cword 12703 ++ cconcat 12705 substr csubstr 12707

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-oadd 7204 df-er 7381 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-nn 10632 df-2 10690 df-n0 10894 df-z 10962 df-uz 11183 df-fz 11811 df-fzo 11943 df-hash 12554 df-word 12711 df-concat 12713 df-substr 12715

This theorem is referenced by: (None)

W3C validator