Theorem pfxccatin12 14792

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 14789	. . . 4 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))))
3		swrdvalfn 14710	. . . 4 ⊢ (((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) Fn (0..^(𝑁 − 𝑀)))
4	2, 3	syl 18	. . 3 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) Fn (0..^(𝑁 − 𝑀)))
5		swrdcl 14703	. . . . . 6 ⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉)
6		pfxcl 14737	. . . . . 6 ⊢ (𝐵 ∈ Word 𝑉 → (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉)
7		ccatvalfn 14636	. . . . . 6 ⊢ (((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))) Fn (0..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿))))))
8	5, 6, 7	syl2an 608	. . . . 5 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))) Fn (0..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿))))))
9	8	adantr 486	. . . 4 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))) Fn (0..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿))))))
10		simpll 779	. . . . . . . . 9 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → 𝐴 ∈ Word 𝑉)
11		simprl 783	. . . . . . . . 9 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → 𝑀 ∈ (0...𝐿))
12		lencl 14588	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℕ0)
13		nn0fz0 13670	. . . . . . . . . . . 12 ⊢ ((♯‘𝐴) ∈ ℕ0 ↔ (♯‘𝐴) ∈ (0...(♯‘𝐴)))
14	12, 13	sylib 221	. . . . . . . . . . 11 ⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ (0...(♯‘𝐴)))
15	1, 14	eqeltrid 2869	. . . . . . . . . 10 ⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ (0...(♯‘𝐴)))
16	15	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → 𝐿 ∈ (0...(♯‘𝐴)))
17		swrdlen 14705	. . . . . . . . 9 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝐴))) → (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) = (𝐿 − 𝑀))
18	10, 11, 16, 17	syl3anc 1398	. . . . . . . 8 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) = (𝐿 − 𝑀))
19		lencl 14588	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈ ℕ0)
20	19	nn0zd 12631	. . . . . . . . . . 11 ⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈ ℤ)
21		elfzmlbp 13684	. . . . . . . . . . 11 ⊢ (((♯‘𝐵) ∈ ℤ ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → (𝑁 − 𝐿) ∈ (0...(♯‘𝐵)))
22	20, 21	sylan 592	. . . . . . . . . 10 ⊢ ((𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → (𝑁 − 𝐿) ∈ (0...(♯‘𝐵)))
23		pfxlen 14743	. . . . . . . . . 10 ⊢ ((𝐵 ∈ Word 𝑉 ∧ (𝑁 − 𝐿) ∈ (0...(♯‘𝐵))) → (♯‘(𝐵 prefix (𝑁 − 𝐿))) = (𝑁 − 𝐿))
24	22, 23	syldan 603	. . . . . . . . 9 ⊢ ((𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → (♯‘(𝐵 prefix (𝑁 − 𝐿))) = (𝑁 − 𝐿))
25	24	ad2ant2l 759	. . . . . . . 8 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (♯‘(𝐵 prefix (𝑁 − 𝐿))) = (𝑁 − 𝐿))
26	18, 25	oveq12d 7437	. . . . . . 7 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿)))) = ((𝐿 − 𝑀) + (𝑁 − 𝐿)))
27		elfz2nn0 13663	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (0...𝐿) ↔ (𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿))
28		nn0cn 12529	. . . . . . . . . . . . . . . 16 ⊢ (𝐿 ∈ ℕ0 → 𝐿 ∈ ℂ)
29	28	ad2antll 742	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ (𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)) → 𝐿 ∈ ℂ)
30		nn0cn 12529	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℂ)
31	30	ad2antrl 741	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ (𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)) → 𝑀 ∈ ℂ)
32		zcn 12611	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
33	32	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ (𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)) → 𝑁 ∈ ℂ)
34	29, 31, 33	3jca 1146	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ (𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)) → (𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ))
35	34	ex 418	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℤ → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0) → (𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ)))
36		elfzelz 13568	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → 𝑁 ∈ ℤ)
37	35, 36	syl11 34	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0) → (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → (𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ)))
38	37	3adant3 1150	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿) → (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → (𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ)))
39	27, 38	sylbi 220	. . . . . . . . . 10 ⊢ (𝑀 ∈ (0...𝐿) → (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → (𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ)))
40	39	imp 412	. . . . . . . . 9 ⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → (𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ))
41		npncan3 11511	. . . . . . . . 9 ⊢ ((𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝐿 − 𝑀) + (𝑁 − 𝐿)) = (𝑁 − 𝑀))
42	40, 41	syl 18	. . . . . . . 8 ⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐿 − 𝑀) + (𝑁 − 𝐿)) = (𝑁 − 𝑀))
43	42	adantl 487	. . . . . . 7 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐿 − 𝑀) + (𝑁 − 𝐿)) = (𝑁 − 𝑀))
44	26, 43	eqtr2d 2801	. . . . . 6 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (𝑁 − 𝑀) = ((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿)))))
45	44	oveq2d 7435	. . . . 5 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (0..^(𝑁 − 𝑀)) = (0..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿))))))
46	45	fneq2d 6633	. . . 4 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))) Fn (0..^(𝑁 − 𝑀)) ↔ ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))) Fn (0..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿)))))))
47	9, 46	mpbird 260	. . 3 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))) Fn (0..^(𝑁 − 𝑀)))
48		simprl 783	. . . . . 6 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))))
49		simpr 490	. . . . . . . 8 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → 𝑘 ∈ (0..^(𝑁 − 𝑀)))
50	49	anim2i 629	. . . . . . 7 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))))
51	50	ancomd 467	. . . . . 6 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (𝑘 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝑘 ∈ (0..^(𝐿 − 𝑀))))
52	1	pfxccatin12lem3 14791	. . . . . 6 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝑘 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝑘 ∈ (0..^(𝐿 − 𝑀))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝑘) = ((𝐴 substr ⟨𝑀, 𝐿⟩)‘𝑘)))
53	48, 51, 52	sylc 66	. . . . 5 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝑘) = ((𝐴 substr ⟨𝑀, 𝐿⟩)‘𝑘))
54	5, 6	anim12i 625	. . . . . . . . 9 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉))
55	54	adantr 486	. . . . . . . 8 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉))
56	55	ad2antrl 741	. . . . . . 7 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉))
57		simpl 488	. . . . . . . 8 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → 𝑘 ∈ (0..^(𝐿 − 𝑀)))
58	18	oveq2d 7435	. . . . . . . . 9 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (0..^(♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))) = (0..^(𝐿 − 𝑀)))
59	58	ad2antrl 741	. . . . . . . 8 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (0..^(♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))) = (0..^(𝐿 − 𝑀)))
60	57, 59	eleqtrrd 2868	. . . . . . 7 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → 𝑘 ∈ (0..^(♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))))
61		df-3an 1105	. . . . . . 7 ⊢ (((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉 ∧ 𝑘 ∈ (0..^(♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)))) ↔ (((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉) ∧ 𝑘 ∈ (0..^(♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)))))
62	56, 60, 61	sylanbrc 595	. . . . . 6 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉 ∧ 𝑘 ∈ (0..^(♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)))))
63		ccatval1 14632	. . . . . 6 ⊢ (((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉 ∧ 𝑘 ∈ (0..^(♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)))) → (((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))‘𝑘) = ((𝐴 substr ⟨𝑀, 𝐿⟩)‘𝑘))
64	62, 63	syl 18	. . . . 5 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))‘𝑘) = ((𝐴 substr ⟨𝑀, 𝐿⟩)‘𝑘))
65	53, 64	eqtr4d 2803	. . . 4 ⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝑘) = (((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))‘𝑘))
66		simprl 783	. . . . . 6 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))))
67	49	anim2i 629	. . . . . . 7 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))))
68	67	ancomd 467	. . . . . 6 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (𝑘 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝑘 ∈ (0..^(𝐿 − 𝑀))))
69	1	pfxccatin12lem2 14790	. . . . . 6 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝑘 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝑘 ∈ (0..^(𝐿 − 𝑀))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝑘) = ((𝐵 prefix (𝑁 − 𝐿))‘(𝑘 − (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))))))
70	66, 68, 69	sylc 66	. . . . 5 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝑘) = ((𝐵 prefix (𝑁 − 𝐿))‘(𝑘 − (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)))))
71	55	ad2antrl 741	. . . . . . 7 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉))
72		elfzuz 13564	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → 𝑁 ∈ (ℤ≥‘𝐿))
73		eluzelz 12888	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ≥‘𝐿) → 𝑁 ∈ ℤ)
74		id 23	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ) → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ))
75	74	3expia 1139	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → (𝑁 ∈ ℤ → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ)))
76	75	ancoms 464	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0) → (𝑁 ∈ ℤ → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ)))
77	76	3adant3 1150	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿) → (𝑁 ∈ ℤ → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ)))
78	27, 77	sylbi 220	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (0...𝐿) → (𝑁 ∈ ℤ → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ)))
79	73, 78	syl5com 32	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ≥‘𝐿) → (𝑀 ∈ (0...𝐿) → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ)))
80	72, 79	syl 18	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → (𝑀 ∈ (0...𝐿) → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ)))
81	80	impcom 413	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ))
82	81	adantl 487	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ))
83	82	ad2antrl 741	. . . . . . . . 9 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ))
84		pfxccatin12lem4 14785	. . . . . . . . 9 ⊢ ((𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ) → ((𝑘 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝑘 ∈ (0..^(𝐿 − 𝑀))) → 𝑘 ∈ ((𝐿 − 𝑀)..^((𝐿 − 𝑀) + (𝑁 − 𝐿)))))
85	83, 68, 84	sylc 66	. . . . . . . 8 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → 𝑘 ∈ ((𝐿 − 𝑀)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))))
86	18, 26	oveq12d 7437	. . . . . . . . 9 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿))))) = ((𝐿 − 𝑀)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))))
87	86	ad2antrl 741	. . . . . . . 8 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → ((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿))))) = ((𝐿 − 𝑀)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))))
88	85, 87	eleqtrrd 2868	. . . . . . 7 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → 𝑘 ∈ ((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿))))))
89		df-3an 1105	. . . . . . 7 ⊢ (((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉 ∧ 𝑘 ∈ ((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿)))))) ↔ (((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉) ∧ 𝑘 ∈ ((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿)))))))
90	71, 88, 89	sylanbrc 595	. . . . . 6 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉 ∧ 𝑘 ∈ ((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿)))))))
91		ccatval2 14633	. . . . . 6 ⊢ (((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉 ∧ 𝑘 ∈ ((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))..^((♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) + (♯‘(𝐵 prefix (𝑁 − 𝐿)))))) → (((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))‘𝑘) = ((𝐵 prefix (𝑁 − 𝐿))‘(𝑘 − (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)))))
92	90, 91	syl 18	. . . . 5 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))‘𝑘) = ((𝐵 prefix (𝑁 − 𝐿))‘(𝑘 − (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)))))
93	70, 92	eqtr4d 2803	. . . 4 ⊢ ((¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝑘) = (((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))‘𝑘))
94	65, 93	pm2.61ian 824	. . 3 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝑘) = (((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))‘𝑘))
95	4, 47, 94	eqfnfvd 7032	. 2 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))))
96	95	ex 418	1 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿)))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ⟨cop 4597   class class class wbr 5111   Fn wfn 6535  ‘cfv 6540  (class class class)co 7419  ℂcc 11113  0cc0 11115   + caddc 11118   ≤ cle 11259   − cmin 11456  ℕ₀cn0 12519  ℤcz 12606  ℤ_≥cuz 12878  ...cfz 13551  ..^cfzo 13699  ♯chash 14384  Word cword 14568   ++ cconcat 14625   substr csubstr 14698   prefix cpfx 14730

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-cnex 11171  ax-resscn 11172  ax-1cn 11173  ax-icn 11174  ax-addcl 11175  ax-addrcl 11176  ax-mulcl 11177  ax-mulrcl 11178  ax-mulcom 11179  ax-addass 11180  ax-mulass 11181  ax-distr 11182  ax-i2m1 11183  ax-1ne0 11184  ax-1rid 11185  ax-rnegex 11186  ax-rrecex 11187  ax-cnre 11188  ax-pre-lttri 11189  ax-pre-lttrn 11190  ax-pre-ltadd 11191  ax-pre-mulgt0 11192

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-1st 7992  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-fin 8953  df-card 9941  df-pnf 11260  df-mnf 11261  df-xr 11262  df-ltxr 11263  df-le 11264  df-sub 11458  df-neg 11459  df-nn 12249  df-n0 12520  df-z 12607  df-uz 12879  df-fz 13552  df-fzo 13700  df-hash 14385  df-word 14569  df-concat 14626  df-substr 14699  df-pfx 14731

This theorem is used by:  pfxccat3  14793  pfxccatpfx2  14796  pfxccatin12d  14804