swrdccat - Metamath Proof Explorer

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

Theorem swrdccat 12668

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

**Proof of Theorem swrdccat**
Step	Hyp	Ref	Expression
1		swrdccatin12.l	. . . . 5
2	1	swrdccat3 12667	. . . 4 Word $/\$ Word $/\$ concat substr substr substr substr concat substr
3	2	imp 429	. . 3 Word $/\$ Word $/\$ $/\$ concat substr substr substr substr concat substr
4		lencl 12515	. . . . . 6 Word
5	4	adantr 465	. . . . 5 Word $/\$ Word
6	1	eqcomi 2473	. . . . . . 7
7	6	eleq1i 2537	. . . . . 6
8		elfz2nn0 11757	. . . . . . . . 9 $/\$ $/\$
9		iftrue 3938	. . . . . . . . . . . . . . . . . . 19
10	9	adantl 466	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
11	10	opeq2d 4213	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
12	11	oveq2d 6291	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr substr
13		iftrue 3938	. . . . . . . . . . . . . . . . . . . . 21
14	13	opeq1d 4212	. . . . . . . . . . . . . . . . . . . 20
15	14	oveq2d 6291	. . . . . . . . . . . . . . . . . . 19 substr substr
16	15	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr substr
17		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word Word
18		nn0z 10876	. . . . . . . . . . . . . . . . . . . . . . 23
19		nn0z 10876	. . . . . . . . . . . . . . . . . . . . . . . . . 26
20	19	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
21		zsubcl 10894	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
22	20, 21	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
23		nn0z 10876	. . . . . . . . . . . . . . . . . . . . . . . . . 26
24	23	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
25		zsubcl 10894	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
26	24, 25	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
27	22, 26	jca 532	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
28	18, 27	sylan2 474	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
29	17, 28	anim12i 566	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
30		3anass 972	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ $/\$ Word $/\$ $/\$
31	29, 30	sylibr 212	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
32	31	ad2antrl 727	. . . . . . . . . . . . . . . . . . 19 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word $/\$ $/\$
33		nn0re 10793	. . . . . . . . . . . . . . . . . . . . . . . . 25
34		nn0re 10793	. . . . . . . . . . . . . . . . . . . . . . . . 25
35	33, 34	anim12i 566	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
36		nn0re 10793	. . . . . . . . . . . . . . . . . . . . . . . 24
37		subge0 10054	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
38	37	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
39		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
40	39	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
41		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
42		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
43	42	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
44	40, 41, 43	3jca 1171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
45		letr 9667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
46	44, 45	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
47	46	expd 436	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
48	47	com23 78	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
49	38, 48	sylbid 215	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
50	49	com23 78	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
51	35, 36, 50	syl2an 477	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
52	51	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$
53	52	imp 429	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
54	53	impcom 430	. . . . . . . . . . . . . . . . . . . 20 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
55	34	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
56	55	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
57	33	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
58	57	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
59	36	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
60	56, 58, 59	3jca 1171	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
61	60	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
62	61	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . 21 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		lesub1 10035	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
64	62, 63	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
65	54, 64	mpbid 210	. . . . . . . . . . . . . . . . . . 19 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
66		swrdlend 12606	. . . . . . . . . . . . . . . . . . 19 Word $/\$ $/\$ substr
67	32, 65, 66	sylc 60	. . . . . . . . . . . . . . . . . 18 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
68	16, 67	eqtrd 2501	. . . . . . . . . . . . . . . . 17 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
69		iffalse 3941	. . . . . . . . . . . . . . . . . . . 20
70	69	opeq1d 4212	. . . . . . . . . . . . . . . . . . 19
71	70	oveq2d 6291	. . . . . . . . . . . . . . . . . 18 substr substr
72	17	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ Word
73	72	adantr 465	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word
74		0zd 10865	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
75	24, 18, 25	syl2an 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
76	75	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$
77	76	adantr 465	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
78	73, 74, 77	3jca 1171	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word $/\$ $/\$
79	55, 36	anim12i 566	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
80	79	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
81		suble0 10055	. . . . . . . . . . . . . . . . . . . . 21 $/\$
82	80, 81	syl 16	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$
83	82	biimpar 485	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
84		swrdlend 12606	. . . . . . . . . . . . . . . . . . 19 Word $/\$ $/\$ substr
85	78, 83, 84	sylc 60	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
86	71, 85	sylan9eq 2521	. . . . . . . . . . . . . . . . 17 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
87	68, 86	pm2.61ian 788	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
88	12, 87	oveq12d 6293	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr concat substr substr concat
89		swrdcl 12596	. . . . . . . . . . . . . . . . . . 19 Word substr Word
90		ccatrid 12556	. . . . . . . . . . . . . . . . . . 19 substr Word substr concat substr
91	89, 90	syl 16	. . . . . . . . . . . . . . . . . 18 Word substr concat substr
92	91	adantr 465	. . . . . . . . . . . . . . . . 17 Word $/\$ Word substr concat substr
93	92	adantr 465	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ substr concat substr
94	93	adantr 465	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr concat substr
95	88, 94	eqtrd 2501	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr concat substr substr
96		iffalse 3941	. . . . . . . . . . . . . . . . . . . 20
97	96	3ad2ant2 1013	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
98	97	opeq2d 4213	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
99	98	oveq2d 6291	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
100		simpl 457	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word Word
101	100, 20, 18	3anim123i 1176	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
102	101	3expb 1192	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
103		swrdlend 12606	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ $/\$ substr
104	102, 103	syl 16	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ substr
105	104	imp 429	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
106	105	3adant2 1010	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr
107	99, 106	eqtrd 2501	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr
108	57, 36, 37	syl2an 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
109	108	biimprd 223	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
110	109	adantl 466	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$
111	110	imp 429	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
112	111	3adant2 1010	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
113	112, 14	syl 16	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
114	113	oveq2d 6291	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
115	107, 114	oveq12d 6293	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr concat substr concat substr
116		swrdcl 12596	. . . . . . . . . . . . . . . . . . 19 Word substr Word
117	116	adantl 466	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word substr Word
118		ccatlid 12555	. . . . . . . . . . . . . . . . . 18 substr Word concat substr substr
119	117, 118	syl 16	. . . . . . . . . . . . . . . . 17 Word $/\$ Word concat substr substr
120	119	adantr 465	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ concat substr substr
121	120	3ad2ant1 1012	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ concat substr substr
122	115, 121	eqtrd 2501	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr concat substr substr
123	96	3ad2ant2 1013	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
124	123	opeq2d 4213	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
125	124	oveq2d 6291	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
126	33, 36, 37	syl2an 477	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
127	126	adantlr 714	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
128	127	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$
129	128	biimpd 207	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$
130	129	con3dimp 441	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
131	130	3adant2 1010	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
132	131, 69	syl 16	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
133	132	opeq1d 4212	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
134	133	oveq2d 6291	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
135	125, 134	oveq12d 6293	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr concat substr substr concat substr
136	95, 122, 135	2if2 3980	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ substr concat substr substr substr substr concat substr
137	136	ex 434	. . . . . . . . . . . 12 Word $/\$ Word $/\$ $/\$ substr concat substr substr substr substr concat substr
138	137	expd 436	. . . . . . . . . . 11 Word $/\$ Word $/\$ substr concat substr substr substr substr concat substr
139	138	com12 31	. . . . . . . . . 10 $/\$ Word $/\$ Word substr concat substr substr substr substr concat substr
140	139	3adant3 1011	. . . . . . . . 9 $/\$ $/\$ Word $/\$ Word substr concat substr substr substr substr concat substr
141	8, 140	sylbi 195	. . . . . . . 8 Word $/\$ Word substr concat substr substr substr substr concat substr
142	141	adantr 465	. . . . . . 7 $/\$ Word $/\$ Word substr concat substr substr substr substr concat substr
143	142	com13 80	. . . . . 6 Word $/\$ Word $/\$ substr concat substr substr substr substr concat substr
144	7, 143	sylbi 195	. . . . 5 Word $/\$ Word $/\$ substr concat substr substr substr substr concat substr
145	5, 144	mpcom 36	. . . 4 Word $/\$ Word $/\$ substr concat substr substr substr substr concat substr
146	145	imp 429	. . 3 Word $/\$ Word $/\$ $/\$ substr concat substr substr substr substr concat substr
147	3, 146	eqtr4d 2504	. 2 Word $/\$ Word $/\$ $/\$ concat substr substr concat substr
148	147	ex 434	1 Word $/\$ Word $/\$ concat substr substr concat substr

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 968

wceq 1374

wcel 1762

c0 3778

cif 3932

cop 4026 class class class wbr 4440

cfv 5579 (class class class)co 6275

cr 9480

cc0 9481

caddc 9484

cle 9618

cmin 9794

cn0 10784

cz 10853

cfz 11661

chash 12360 Word cword 12487 concat cconcat 12489 substr csubstr 12491

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1961 ax-ext 2438 ax-rep 4551 ax-sep 4561 ax-nul 4569 ax-pow 4618 ax-pr 4679 ax-un 6567 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2272 df-mo 2273 df-clab 2446 df-cleq 2452 df-clel 2455 df-nfc 2610 df-ne 2657 df-nel 2658 df-ral 2812 df-rex 2813 df-reu 2814 df-rab 2816 df-v 3108 df-sbc 3325 df-csb 3429 df-dif 3472 df-un 3474 df-in 3476 df-ss 3483 df-pss 3485 df-nul 3779 df-if 3933 df-pw 4005 df-sn 4021 df-pr 4023 df-tp 4025 df-op 4027 df-uni 4239 df-int 4276 df-iun 4320 df-br 4441 df-opab 4499 df-mpt 4500 df-tr 4534 df-eprel 4784 df-id 4788 df-po 4793 df-so 4794 df-fr 4831 df-we 4833 df-ord 4874 df-on 4875 df-lim 4876 df-suc 4877 df-xp 4998 df-rel 4999 df-cnv 5000 df-co 5001 df-dm 5002 df-rn 5003 df-res 5004 df-ima 5005 df-iota 5542 df-fun 5581 df-fn 5582 df-f 5583 df-f1 5584 df-fo 5585 df-f1o 5586 df-fv 5587 df-riota 6236 df-ov 6278 df-oprab 6279 df-mpt2 6280 df-om 6672 df-1st 6774 df-2nd 6775 df-recs 7032 df-rdg 7066 df-1o 7120 df-oadd 7124 df-er 7301 df-en 7507 df-dom 7508 df-sdom 7509 df-fin 7510 df-card 8309 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9796 df-neg 9797 df-nn 10526 df-n0 10785 df-z 10854 df-uz 11072 df-fz 11662 df-fzo 11782 df-hash 12361 df-word 12495 df-concat 12497 df-substr 12499

This theorem is referenced by: (None)

W3C validator