Step | Hyp | Ref
| Expression |
1 | | swrdccatin2.l |
. . . . 5
⊢ 𝐿 = (♯‘𝐴) |
2 | 1 | pfxccatin12lem2c 14371 |
. . . 4
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵))))) |
3 | | swrdvalfn 14292 |
. . . 4
⊢ (((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
4 | 2, 3 | syl 17 |
. . 3
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
5 | | swrdcl 14286 |
. . . . . 6
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr 〈𝑀, 𝐿〉) ∈ Word 𝑉) |
6 | | pfxcl 14318 |
. . . . . 6
⊢ (𝐵 ∈ Word 𝑉 → (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉) |
7 | | ccatvalfn 14214 |
. . . . . 6
⊢ (((𝐴 substr 〈𝑀, 𝐿〉) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉) → ((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿))) Fn (0..^((♯‘(𝐴 substr 〈𝑀, 𝐿〉)) + (♯‘(𝐵 prefix (𝑁 − 𝐿)))))) |
8 | 5, 6, 7 | syl2an 595 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿))) Fn (0..^((♯‘(𝐴 substr 〈𝑀, 𝐿〉)) + (♯‘(𝐵 prefix (𝑁 − 𝐿)))))) |
9 | 8 | adantr 480 |
. . . 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 14164 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈
ℕ0) |
13 | | nn0fz0 13283 |
. . . . . . . . . . . 12
⊢
((♯‘𝐴)
∈ ℕ0 ↔ (♯‘𝐴) ∈ (0...(♯‘𝐴))) |
14 | 12, 13 | sylib 217 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ (0...(♯‘𝐴))) |
15 | 1, 14 | eqeltrid 2843 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ (0...(♯‘𝐴))) |
16 | 15 | ad2antrr 722 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → 𝐿 ∈ (0...(♯‘𝐴))) |
17 | | swrdlen 14288 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝐴))) → (♯‘(𝐴 substr 〈𝑀, 𝐿〉)) = (𝐿 − 𝑀)) |
18 | 10, 11, 16, 17 | syl3anc 1369 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (♯‘(𝐴 substr 〈𝑀, 𝐿〉)) = (𝐿 − 𝑀)) |
19 | | lencl 14164 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈
ℕ0) |
20 | 19 | nn0zd 12353 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈ ℤ) |
21 | | elfzmlbp 13296 |
. . . . . . . . . . 11
⊢
(((♯‘𝐵)
∈ ℤ ∧ 𝑁
∈ (𝐿...(𝐿 + (♯‘𝐵)))) → (𝑁 − 𝐿) ∈ (0...(♯‘𝐵))) |
22 | 20, 21 | sylan 579 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → (𝑁 − 𝐿) ∈ (0...(♯‘𝐵))) |
23 | | pfxlen 14324 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ Word 𝑉 ∧ (𝑁 − 𝐿) ∈ (0...(♯‘𝐵))) → (♯‘(𝐵 prefix (𝑁 − 𝐿))) = (𝑁 − 𝐿)) |
24 | 22, 23 | syldan 590 |
. . . . . . . . 9
⊢ ((𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → (♯‘(𝐵 prefix (𝑁 − 𝐿))) = (𝑁 − 𝐿)) |
25 | 24 | ad2ant2l 742 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (♯‘(𝐵 prefix (𝑁 − 𝐿))) = (𝑁 − 𝐿)) |
26 | 18, 25 | oveq12d 7273 |
. . . . . . 7
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((♯‘(𝐴 substr 〈𝑀, 𝐿〉)) + (♯‘(𝐵 prefix (𝑁 − 𝐿)))) = ((𝐿 − 𝑀) + (𝑁 − 𝐿))) |
27 | | elfz2nn0 13276 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ (0...𝐿) ↔ (𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑀 ≤ 𝐿)) |
28 | | nn0cn 12173 |
. . . . . . . . . . . . . . . 16
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℂ) |
29 | 28 | ad2antll 725 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0)) → 𝐿 ∈ ℂ) |
30 | | nn0cn 12173 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℂ) |
31 | 30 | ad2antrl 724 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0)) → 𝑀 ∈ ℂ) |
32 | | zcn 12254 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
33 | 32 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0)) → 𝑁 ∈ ℂ) |
34 | 29, 31, 33 | 3jca 1126 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0)) → (𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ)) |
35 | 34 | ex 412 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ))) |
36 | | elfzelz 13185 |
. . . . . . . . . . . . 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 406 |
. . . . . . . . 9
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → (𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ)) |
41 | | npncan3 11189 |
. . . . . . . . 9
⊢ ((𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝐿 − 𝑀) + (𝑁 − 𝐿)) = (𝑁 − 𝑀)) |
42 | 40, 41 | syl 17 |
. . . . . . . 8
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐿 − 𝑀) + (𝑁 − 𝐿)) = (𝑁 − 𝑀)) |
43 | 42 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐿 − 𝑀) + (𝑁 − 𝐿)) = (𝑁 − 𝑀)) |
44 | 26, 43 | eqtr2d 2779 |
. . . . . 6
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (𝑁 − 𝑀) = ((♯‘(𝐴 substr 〈𝑀, 𝐿〉)) + (♯‘(𝐵 prefix (𝑁 − 𝐿))))) |
45 | 44 | oveq2d 7271 |
. . . . 5
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (0..^(𝑁 − 𝑀)) = (0..^((♯‘(𝐴 substr 〈𝑀, 𝐿〉)) + (♯‘(𝐵 prefix (𝑁 − 𝐿)))))) |
46 | 45 | fneq2d 6511 |
. . . 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 484 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → 𝑘 ∈ (0..^(𝑁 − 𝑀))) |
50 | 49 | anim2i 616 |
. . . . . . 7
⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) |
51 | 50 | ancomd 461 |
. . . . . 6
⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (𝑘 ∈ (0..^(𝑁 − 𝑀)) ∧ 𝑘 ∈ (0..^(𝐿 − 𝑀)))) |
52 | 1 | pfxccatin12lem3 14373 |
. . . . . 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 612 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐴 substr 〈𝑀, 𝐿〉) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉)) |
55 | 54 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 substr 〈𝑀, 𝐿〉) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉)) |
56 | 55 | ad2antrl 724 |
. . . . . . 7
⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → ((𝐴 substr 〈𝑀, 𝐿〉) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉)) |
57 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → 𝑘 ∈ (0..^(𝐿 − 𝑀))) |
58 | 18 | oveq2d 7271 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (0..^(♯‘(𝐴 substr 〈𝑀, 𝐿〉))) = (0..^(𝐿 − 𝑀))) |
59 | 58 | ad2antrl 724 |
. . . . . . . 8
⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (0..^(♯‘(𝐴 substr 〈𝑀, 𝐿〉))) = (0..^(𝐿 − 𝑀))) |
60 | 57, 59 | eleqtrrd 2842 |
. . . . . . 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 582 |
. . . . . 6
⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → ((𝐴 substr 〈𝑀, 𝐿〉) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉 ∧ 𝑘 ∈ (0..^(♯‘(𝐴 substr 〈𝑀, 𝐿〉))))) |
63 | | ccatval1 14209 |
. . . . . 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 2781 |
. . . 4
⊢ ((𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝑘) = (((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿)))‘𝑘)) |
66 | | simprl 767 |
. . . . . 6
⊢ ((¬
𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))))) |
67 | 49 | anim2i 616 |
. . . . . . 7
⊢ ((¬
𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) |
68 | 67 | ancomd 461 |
. . . . . 6
⊢ ((¬
𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (𝑘 ∈ (0..^(𝑁 − 𝑀)) ∧ ¬ 𝑘 ∈ (0..^(𝐿 − 𝑀)))) |
69 | 1 | pfxccatin12lem2 14372 |
. . . . . 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 13181 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → 𝑁 ∈ (ℤ≥‘𝐿)) |
73 | | eluzelz 12521 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘𝐿) → 𝑁 ∈ ℤ) |
74 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐿 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℤ) → (𝐿
∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈
ℤ)) |
75 | 74 | 3expia 1119 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐿 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑁 ∈ ℤ → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℤ))) |
76 | 75 | ancoms 458 |
. . . . . . . . . . . . . . . 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 407 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℤ)) |
82 | 81 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℤ)) |
83 | 82 | ad2antrl 724 |
. . . . . . . . 9
⊢ ((¬
𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → (𝐿 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℤ)) |
84 | | pfxccatin12lem4 14367 |
. . . . . . . . 9
⊢ ((𝐿 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑁
∈ ℤ) → ((𝑘
∈ (0..^(𝑁 −
𝑀)) ∧ ¬ 𝑘 ∈ (0..^(𝐿 − 𝑀))) → 𝑘 ∈ ((𝐿 − 𝑀)..^((𝐿 − 𝑀) + (𝑁 − 𝐿))))) |
85 | 83, 68, 84 | sylc 65 |
. . . . . . . 8
⊢ ((¬
𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → 𝑘 ∈ ((𝐿 − 𝑀)..^((𝐿 − 𝑀) + (𝑁 − 𝐿)))) |
86 | 18, 26 | oveq12d 7273 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((♯‘(𝐴 substr 〈𝑀, 𝐿〉))..^((♯‘(𝐴 substr 〈𝑀, 𝐿〉)) + (♯‘(𝐵 prefix (𝑁 − 𝐿))))) = ((𝐿 − 𝑀)..^((𝐿 − 𝑀) + (𝑁 − 𝐿)))) |
87 | 86 | ad2antrl 724 |
. . . . . . . 8
⊢ ((¬
𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → ((♯‘(𝐴 substr 〈𝑀, 𝐿〉))..^((♯‘(𝐴 substr 〈𝑀, 𝐿〉)) + (♯‘(𝐵 prefix (𝑁 − 𝐿))))) = ((𝐿 − 𝑀)..^((𝐿 − 𝑀) + (𝑁 − 𝐿)))) |
88 | 85, 87 | eleqtrrd 2842 |
. . . . . . 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 582 |
. . . . . 6
⊢ ((¬
𝑘 ∈ (0..^(𝐿 − 𝑀)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀)))) → ((𝐴 substr 〈𝑀, 𝐿〉) ∈ Word 𝑉 ∧ (𝐵 prefix (𝑁 − 𝐿)) ∈ Word 𝑉 ∧ 𝑘 ∈ ((♯‘(𝐴 substr 〈𝑀, 𝐿〉))..^((♯‘(𝐴 substr 〈𝑀, 𝐿〉)) + (♯‘(𝐵 prefix (𝑁 − 𝐿))))))) |
91 | | ccatval2 14211 |
. . . . . 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 2781 |
. . . 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 6894 |
. 2
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = ((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿)))) |
96 | 95 | ex 412 |
1
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = ((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿))))) |