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 12844

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 12843	. . . 4 Word $/\$ Word $/\$ ++ substr substr substr substr ++ substr
3	2	imp 431	. . 3 Word $/\$ Word $/\$ $/\$ ++ substr substr substr substr ++ substr
4		lencl 12684	. . . . . 6 Word
5	4	adantr 467	. . . . 5 Word $/\$ Word
6	1	eqcomi 2459	. . . . . . 7
7	6	eleq1i 2519	. . . . . 6
8		elfz2nn0 11882	. . . . . . . . 9 $/\$ $/\$
9		iftrue 3886	. . . . . . . . . . . . . . . . . 18
10	9	adantl 468	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
11	10	opeq2d 4172	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
12	11	oveq2d 6304	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr substr
13		iftrue 3886	. . . . . . . . . . . . . . . . . . . 20
14	13	opeq1d 4171	. . . . . . . . . . . . . . . . . . 19
15	14	oveq2d 6304	. . . . . . . . . . . . . . . . . 18 substr substr
16	15	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr substr
17		simpr 463	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word Word
18		nn0z 10957	. . . . . . . . . . . . . . . . . . . . . 22
19		nn0z 10957	. . . . . . . . . . . . . . . . . . . . . . . . 25
20	19	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
21		zsubcl 10976	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
22	20, 21	sylan 474	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
23		nn0z 10957	. . . . . . . . . . . . . . . . . . . . . . . . 25
24	23	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
25		zsubcl 10976	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
26	24, 25	sylan 474	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
27	22, 26	jca 535	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
28	18, 27	sylan2 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
29	17, 28	anim12i 569	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
30		3anass 988	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ $/\$ Word $/\$ $/\$
31	29, 30	sylibr 216	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
32	31	ad2antrl 733	. . . . . . . . . . . . . . . . . 18 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word $/\$ $/\$
33		nn0re 10875	. . . . . . . . . . . . . . . . . . . . . . . 24
34		nn0re 10875	. . . . . . . . . . . . . . . . . . . . . . . 24
35	33, 34	anim12i 569	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
36		nn0re 10875	. . . . . . . . . . . . . . . . . . . . . . 23
37		subge0 10124	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
38	37	adantlr 720	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
39		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
40	39	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
41		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
42		simpl 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
43	42	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
44	40, 41, 43	3jca 1187	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
45		letr 9724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
46	44, 45	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
47	46	expcomd 440	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
48	38, 47	sylbid 219	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
49	48	com23 81	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
50	35, 36, 49	syl2an 480	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
51	50	adantl 468	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$
52	51	imp 431	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
53	52	impcom 432	. . . . . . . . . . . . . . . . . . 19 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
54	34	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
55	54	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
56	33	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
57	56	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
58	36	adantl 468	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
59	55, 57, 58	3jca 1187	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
60	59	adantl 468	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
61	60	ad2antrl 733	. . . . . . . . . . . . . . . . . . . 20 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62		lesub1 10105	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
63	61, 62	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
64	53, 63	mpbid 214	. . . . . . . . . . . . . . . . . 18 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
65		swrdlend 12782	. . . . . . . . . . . . . . . . . 18 Word $/\$ $/\$ substr
66	32, 64, 65	sylc 62	. . . . . . . . . . . . . . . . 17 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
67	16, 66	eqtrd 2484	. . . . . . . . . . . . . . . 16 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
68		iffalse 3889	. . . . . . . . . . . . . . . . . . 19
69	68	opeq1d 4171	. . . . . . . . . . . . . . . . . 18
70	69	oveq2d 6304	. . . . . . . . . . . . . . . . 17 substr substr
71	17	adantr 467	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ Word
72	71	adantr 467	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word
73		0zd 10946	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
74	24, 18, 25	syl2an 480	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
75	74	adantl 468	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$
76	75	adantr 467	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
77	72, 73, 76	3jca 1187	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ Word $/\$ $/\$
78	54, 36	anim12i 569	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
79	78	adantl 468	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
80		suble0 10125	. . . . . . . . . . . . . . . . . . . 20 $/\$
81	79, 80	syl 17	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$
82	81	biimpar 488	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
83		swrdlend 12782	. . . . . . . . . . . . . . . . . 18 Word $/\$ $/\$ substr
84	77, 82, 83	sylc 62	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
85	70, 84	sylan9eq 2504	. . . . . . . . . . . . . . . 16 $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
86	67, 85	pm2.61ian 798	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
87	12, 86	oveq12d 6306	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr ++ substr substr ++
88		swrdcl 12770	. . . . . . . . . . . . . . . . . 18 Word substr Word
89		ccatrid 12728	. . . . . . . . . . . . . . . . . 18 substr Word substr ++ substr
90	88, 89	syl 17	. . . . . . . . . . . . . . . . 17 Word substr ++ substr
91	90	adantr 467	. . . . . . . . . . . . . . . 16 Word $/\$ Word substr ++ substr
92	91	adantr 467	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ substr ++ substr
93	92	adantr 467	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr ++ substr
94	87, 93	eqtrd 2484	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr ++ substr substr
95		iffalse 3889	. . . . . . . . . . . . . . . . . . 19
96	95	3ad2ant2 1029	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
97	96	opeq2d 4172	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
98	97	oveq2d 6304	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
99		simpl 459	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word Word
100	99, 20, 18	3anim123i 1192	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
101	100	3expb 1208	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ Word $/\$ $/\$
102		swrdlend 12782	. . . . . . . . . . . . . . . . . . 19 Word $/\$ $/\$ substr
103	101, 102	syl 17	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ substr
104	103	imp 431	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
105	104	3adant2 1026	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr
106	98, 105	eqtrd 2484	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr
107	56, 36, 37	syl2an 480	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
108	107	biimprd 227	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
109	108	adantl 468	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$
110	109	imp 431	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
111	110	3adant2 1026	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
112	111, 14	syl 17	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
113	112	oveq2d 6304	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
114	106, 113	oveq12d 6306	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr ++ substr
115		swrdcl 12770	. . . . . . . . . . . . . . . . . 18 Word substr Word
116	115	adantl 468	. . . . . . . . . . . . . . . . 17 Word $/\$ Word substr Word
117		ccatlid 12727	. . . . . . . . . . . . . . . . 17 substr Word ++ substr substr
118	116, 117	syl 17	. . . . . . . . . . . . . . . 16 Word $/\$ Word ++ substr substr
119	118	adantr 467	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ ++ substr substr
120	119	3ad2ant1 1028	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ++ substr substr
121	114, 120	eqtrd 2484	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr substr
122	95	3ad2ant2 1029	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
123	122	opeq2d 4172	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
124	123	oveq2d 6304	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
125	33, 36, 37	syl2an 480	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
126	125	adantlr 720	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
127	126	adantl 468	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$
128	127	biimpd 211	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$
129	128	con3dimp 443	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
130	129	3adant2 1026	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
131	130, 68	syl 17	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
132	131	opeq1d 4171	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
133	132	oveq2d 6304	. . . . . . . . . . . . . 14 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr substr
134	124, 133	oveq12d 6306	. . . . . . . . . . . . 13 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ substr ++ substr substr ++ substr
135	94, 121, 134	2if2 3928	. . . . . . . . . . . 12 Word $/\$ Word $/\$ $/\$ $/\$ substr ++ substr substr substr substr ++ substr
136	135	exp32 609	. . . . . . . . . . 11 Word $/\$ Word $/\$ substr ++ substr substr substr substr ++ substr
137	136	com12 32	. . . . . . . . . 10 $/\$ Word $/\$ Word substr ++ substr substr substr substr ++ substr
138	137	3adant3 1027	. . . . . . . . 9 $/\$ $/\$ Word $/\$ Word substr ++ substr substr substr substr ++ substr
139	8, 138	sylbi 199	. . . . . . . 8 Word $/\$ Word substr ++ substr substr substr substr ++ substr
140	139	adantr 467	. . . . . . 7 $/\$ Word $/\$ Word substr ++ substr substr substr substr ++ substr
141	140	com13 83	. . . . . 6 Word $/\$ Word $/\$ substr ++ substr substr substr substr ++ substr
142	7, 141	sylbi 199	. . . . 5 Word $/\$ Word $/\$ substr ++ substr substr substr substr ++ substr
143	5, 142	mpcom 37	. . . 4 Word $/\$ Word $/\$ substr ++ substr substr substr substr ++ substr
144	143	imp 431	. . 3 Word $/\$ Word $/\$ $/\$ substr ++ substr substr substr substr ++ substr
145	3, 144	eqtr4d 2487	. 2 Word $/\$ Word $/\$ $/\$ ++ substr substr ++ substr
146	145	ex 436	1 Word $/\$ Word $/\$ ++ substr substr ++ substr

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 984

wceq 1443

wcel 1886

c0 3730

cif 3880

cop 3973 class class class wbr 4401

cfv 5581 (class class class)co 6288

cr 9535

cc0 9536

caddc 9539

cle 9673

cmin 9857

cn0 10866

cz 10934

cfz 11781

chash 12512 Word cword 12653 ++ cconcat 12655 substr csubstr 12657

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-rep 4514 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-int 4234 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-om 6690 df-1st 6790 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-1o 7179 df-oadd 7183 df-er 7360 df-en 7567 df-dom 7568 df-sdom 7569 df-fin 7570 df-card 8370 df-cda 8595 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-nn 10607 df-2 10665 df-n0 10867 df-z 10935 df-uz 11157 df-fz 11782 df-fzo 11913 df-hash 12513 df-word 12661 df-concat 12663 df-substr 12665

This theorem is referenced by: (None)

W3C validator