Theorem pfxccatin12 14687

Description: The subword of a concatenation of two words within both of the concatenated words. (Contributed by Alexander van der Vekens, 5-Apr-2018.) (Revised by AV, 9-May-2020.)

Hypothesis

Ref	Expression
swrdccatin2.l	⊢ 𝐿 = (♯‘𝐴)

Assertion

Ref	Expression
pfxccatin12	⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))))

Proof of Theorem pfxccatin12

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		swrdccatin2.l	. . . . 5 ⊢ 𝐿 = (♯‘𝐴)
2	1	pfxccatin12lem2c 14684	. . . 4 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))))
3		swrdvalfn 14605	. . . 4 ⊢ (((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) Fn (0..^(𝑁 − 𝑀)))
4	2, 3	syl 17	. . 3 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) Fn (0..^(𝑁 − 𝑀)))
5		swrdcl 14599	. . . . . 6 ⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉)
6		pfxcl 14631	. . . . . 6 ⊢ (𝐵 ∈ Word 𝑉 → (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉)
7		ccatvalfn 14535	. . . . . 6 ⊢ (((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))) Fn (0..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿))))))
8	5, 6, 7	syl2an 594	. . . . 5 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))) Fn (0..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿))))))
9	8	adantr 479	. . . 4 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))) Fn (0..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿))))))
10		simpll 763	. . . . . . . . 9 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → 𝐴 ∈ Word 𝑉)
11		simprl 767	. . . . . . . . 9 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → 𝑀 ∈ (0...𝐿))
12		lencl 14487	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℕ0)
13		nn0fz0 13603	. . . . . . . . . . . 12 ⊢ ((♯‘𝐴) ∈ ℕ0 ↔ (♯‘𝐴) ∈ (0...(♯‘𝐴)))
14	12, 13	sylib 217	. . . . . . . . . . 11 ⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ (0...(♯‘𝐴)))
15	1, 14	eqeltrid 2835	. . . . . . . . . 10 ⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ (0...(♯‘𝐴)))
16	15	ad2antrr 722	. . . . . . . . 9 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → 𝐿 ∈ (0...(♯‘𝐴)))
17		swrdlen 14601	. . . . . . . . 9 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝐴))) → (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) = (𝐿 − 𝑀))
18	10, 11, 16, 17	syl3anc 1369	. . . . . . . 8 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) = (𝐿 − 𝑀))
19		lencl 14487	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈ ℕ0)
20	19	nn0zd 12588	. . . . . . . . . . 11 ⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈ ℤ)
21		elfzmlbp 13616	. . . . . . . . . . 11 ⊢ (((♯‘𝐵) ∈ ℤ ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → (𝑁 − 𝐿) ∈ (0...(♯‘𝐵)))
22	20, 21	sylan 578	. . . . . . . . . 10 ⊢ ((𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → (𝑁 − 𝐿) ∈ (0...(♯‘𝐵)))
23		pfxlen 14637	. . . . . . . . . 10 ⊢ ((𝐵 ∈ Word 𝑉 ∧ (𝑁 − 𝐿) ∈ (0...(♯‘𝐵))) → (♯‘(𝐵 prefix (𝑁 − 𝐿))) = (𝑁 − 𝐿))
24	22, 23	syldan 589	. . . . . . . . 9 ⊢ ((𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → (♯‘(𝐵 prefix (𝑁 − 𝐿))) = (𝑁 − 𝐿))
25	24	ad2ant2l 742	. . . . . . . 8 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (♯‘(𝐵 prefix (𝑁 − 𝐿))) = (𝑁 − 𝐿))
26	18, 25	oveq12d 7429	. . . . . . 7 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿)))) = ((𝐿 − 𝑀) + (𝑁 − 𝐿)))
27		elfz2nn0 13596	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (0...𝐿) ↔ (𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿))
28		nn0cn 12486	. . . . . . . . . . . . . . . 16 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℂ)
29	28	ad2antll 725	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ (𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)) → 𝐿 ∈ ℂ)
30		nn0cn 12486	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℂ)
31	30	ad2antrl 724	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ (𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)) → 𝑀 ∈ ℂ)
32		zcn 12567	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
33	32	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ (𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)) → 𝑁 ∈ ℂ)
34	29, 31, 33	3jca 1126	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ (𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)) → (𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ))
35	34	ex 411	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℤ → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0) → (𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ)))
36		elfzelz 13505	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → 𝑁 ∈ ℤ)
37	35, 36	syl11 33	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0) → (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → (𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ)))
38	37	3adant3 1130	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿) → (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → (𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ)))
39	27, 38	sylbi 216	. . . . . . . . . 10 ⊢ (𝑀 ∈ (0...𝐿) → (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → (𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ)))
40	39	imp 405	. . . . . . . . 9 ⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → (𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ))
41		npncan3 11502	. . . . . . . . 9 ⊢ ((𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝐿 − 𝑀) + (𝑁 − 𝐿)) = (𝑁 − 𝑀))
42	40, 41	syl 17	. . . . . . . 8 ⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐿 − 𝑀) + (𝑁 − 𝐿)) = (𝑁 − 𝑀))
43	42	adantl 480	. . . . . . 7 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐿 − 𝑀) + (𝑁 − 𝐿)) = (𝑁 − 𝑀))
44	26, 43	eqtr2d 2771	. . . . . 6 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (𝑁 − 𝑀) = ((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿)))))
45	44	oveq2d 7427	. . . . 5 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (0..^(𝑁 − 𝑀)) = (0..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿))))))
46	45	fneq2d 6642	. . . 4 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))) Fn (0..^(𝑁 − 𝑀)) ↔ ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))) Fn (0..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿)))))))
47	9, 46	mpbird 256	. . 3 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))) Fn (0..^(𝑁 − 𝑀)))
48		simprl 767	. . . . . 6 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))))
49		simpr 483	. . . . . . . 8 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → 𝑘 ∈ (0..^(𝑁 − 𝑀)))
50	49	anim2i 615	. . . . . . 7 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))))
51	50	ancomd 460	. . . . . 6 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (𝑘 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝑘 ∈ (0..^(𝐿 − 𝑀))))
52	1	pfxccatin12lem3 14686	. . . . . 6 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝑘 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝑘 ∈ (0..^(𝐿 − 𝑀))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝑘) = ((𝐴 substr ⟨𝑀, 𝐿⟩)‘𝑘)))
53	48, 51, 52	sylc 65	. . . . 5 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝑘) = ((𝐴 substr ⟨𝑀, 𝐿⟩)‘𝑘))
54	5, 6	anim12i 611	. . . . . . . . 9 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉))
55	54	adantr 479	. . . . . . . 8 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉))
56	55	ad2antrl 724	. . . . . . 7 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉))
57		simpl 481	. . . . . . . 8 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → 𝑘 ∈ (0..^(𝐿 − 𝑀)))
58	18	oveq2d 7427	. . . . . . . . 9 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (0..^(♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))) = (0..^(𝐿 − 𝑀)))
59	58	ad2antrl 724	. . . . . . . 8 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (0..^(♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))) = (0..^(𝐿 − 𝑀)))
60	57, 59	eleqtrrd 2834	. . . . . . 7 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → 𝑘 ∈ (0..^(♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))))
61		df-3an 1087	. . . . . . 7 ⊢ (((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉 ∧ 𝑘 ∈ (0..^(♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)))) ↔ (((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉) ∧ 𝑘 ∈ (0..^(♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)))))
62	56, 60, 61	sylanbrc 581	. . . . . 6 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉 ∧ 𝑘 ∈ (0..^(♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)))))
63		ccatval1 14531	. . . . . 6 ⊢ (((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉 ∧ 𝑘 ∈ (0..^(♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)))) → (((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))‘𝑘) = ((𝐴 substr ⟨𝑀, 𝐿⟩)‘𝑘))
64	62, 63	syl 17	. . . . 5 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))‘𝑘) = ((𝐴 substr ⟨𝑀, 𝐿⟩)‘𝑘))
65	53, 64	eqtr4d 2773	. . . 4 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝑘) = (((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))‘𝑘))
66		simprl 767	. . . . . 6 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))))
67	49	anim2i 615	. . . . . . 7 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))))
68	67	ancomd 460	. . . . . 6 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (𝑘 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝑘 ∈ (0..^(𝐿 − 𝑀))))
69	1	pfxccatin12lem2 14685	. . . . . 6 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝑘 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝑘 ∈ (0..^(𝐿 − 𝑀))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝑘) = ((𝐵 prefix (𝑁 − 𝐿))‘(𝑘 − (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))))))
70	66, 68, 69	sylc 65	. . . . 5 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝑘) = ((𝐵 prefix (𝑁 − 𝐿))‘(𝑘 − (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)))))
71	55	ad2antrl 724	. . . . . . 7 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉))
72		elfzuz 13501	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → 𝑁 ∈ (ℤ≥‘𝐿))
73		eluzelz 12836	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ≥‘𝐿) → 𝑁 ∈ ℤ)
74		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ) → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ))
75	74	3expia 1119	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → (𝑁 ∈ ℤ → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ)))
76	75	ancoms 457	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0) → (𝑁 ∈ ℤ → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ)))
77	76	3adant3 1130	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿) → (𝑁 ∈ ℤ → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ)))
78	27, 77	sylbi 216	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (0...𝐿) → (𝑁 ∈ ℤ → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ)))
79	73, 78	syl5com 31	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ≥‘𝐿) → (𝑀 ∈ (0...𝐿) → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ)))
80	72, 79	syl 17	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → (𝑀 ∈ (0...𝐿) → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ)))
81	80	impcom 406	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ))
82	81	adantl 480	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ))
83	82	ad2antrl 724	. . . . . . . . 9 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ))
84		pfxccatin12lem4 14680	. . . . . . . . 9 ⊢ ((𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ) → ((𝑘 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝑘 ∈ (0..^(𝐿 − 𝑀))) → 𝑘 ∈ ((𝐿 − 𝑀)..^((𝐿 − 𝑀) + (𝑁 − 𝐿)))))
85	83, 68, 84	sylc 65	. . . . . . . 8 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → 𝑘 ∈ ((𝐿 − 𝑀)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))))
86	18, 26	oveq12d 7429	. . . . . . . . 9 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿))))) = ((𝐿 − 𝑀)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))))
87	86	ad2antrl 724	. . . . . . . 8 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → ((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿))))) = ((𝐿 − 𝑀)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))))
88	85, 87	eleqtrrd 2834	. . . . . . 7 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → 𝑘 ∈ ((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿))))))
89		df-3an 1087	. . . . . . 7 ⊢ (((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉 ∧ 𝑘 ∈ ((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿)))))) ↔ (((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉) ∧ 𝑘 ∈ ((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿)))))))
90	71, 88, 89	sylanbrc 581	. . . . . 6 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉 ∧ 𝑘 ∈ ((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿)))))))
91		ccatval2 14532	. . . . . 6 ⊢ (((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉 ∧ 𝑘 ∈ ((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿)))))) → (((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))‘𝑘) = ((𝐵 prefix (𝑁 − 𝐿))‘(𝑘 − (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)))))
92	90, 91	syl 17	. . . . 5 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))‘𝑘) = ((𝐵 prefix (𝑁 − 𝐿))‘(𝑘 − (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)))))
93	70, 92	eqtr4d 2773	. . . 4 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝑘) = (((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))‘𝑘))
94	65, 93	pm2.61ian 808	. . 3 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝑘) = (((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))‘𝑘))
95	4, 47, 94	eqfnfvd 7034	. 2 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))
96	95	ex 411	1 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104  ⟨cop 4633   class class class wbr 5147   Fn wfn 6537  ‘cfv 6542  (class class class)co 7411  ℂcc 11110  0cc0 11112   + caddc 11115   ≤ cle 11253   − cmin 11448  ℕ₀cn0 12476  ℤcz 12562  ℤ_≥cuz 12826  ...cfz 13488  ..^cfzo 13631  ♯chash 14294  Word cword 14468   ++ cconcat 14524   substr csubstr 14594   prefix cpfx 14624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-n0 12477  df-z 12563  df-uz 12827  df-fz 13489  df-fzo 13632  df-hash 14295  df-word 14469  df-concat 14525  df-substr 14595  df-pfx 14625

This theorem is referenced by:  pfxccat3  14688  pfxccatpfx2  14691  pfxccatin12d  14699