Step | Hyp | Ref
| Expression |
1 | | oveq2 7239 |
. . . . . 6
⊢
((♯‘𝐴) =
0 → (0...(♯‘𝐴)) = (0...0)) |
2 | 1 | eleq2d 2824 |
. . . . 5
⊢
((♯‘𝐴) =
0 → (𝑁 ∈
(0...(♯‘𝐴))
↔ 𝑁 ∈
(0...0))) |
3 | | elfz1eq 13147 |
. . . . . 6
⊢ (𝑁 ∈ (0...0) → 𝑁 = 0) |
4 | | elfz1eq 13147 |
. . . . . . . 8
⊢ (𝑀 ∈ (0...0) → 𝑀 = 0) |
5 | | swrd00 14233 |
. . . . . . . . . 10
⊢ ((𝐴 ++ 𝐵) substr 〈0, 0〉) =
∅ |
6 | | swrd00 14233 |
. . . . . . . . . 10
⊢ (𝐴 substr 〈0, 0〉) =
∅ |
7 | 5, 6 | eqtr4i 2769 |
. . . . . . . . 9
⊢ ((𝐴 ++ 𝐵) substr 〈0, 0〉) = (𝐴 substr 〈0,
0〉) |
8 | | opeq1 4798 |
. . . . . . . . . 10
⊢ (𝑀 = 0 → 〈𝑀, 0〉 = 〈0,
0〉) |
9 | 8 | oveq2d 7247 |
. . . . . . . . 9
⊢ (𝑀 = 0 → ((𝐴 ++ 𝐵) substr 〈𝑀, 0〉) = ((𝐴 ++ 𝐵) substr 〈0, 0〉)) |
10 | 8 | oveq2d 7247 |
. . . . . . . . 9
⊢ (𝑀 = 0 → (𝐴 substr 〈𝑀, 0〉) = (𝐴 substr 〈0, 0〉)) |
11 | 7, 9, 10 | 3eqtr4a 2805 |
. . . . . . . 8
⊢ (𝑀 = 0 → ((𝐴 ++ 𝐵) substr 〈𝑀, 0〉) = (𝐴 substr 〈𝑀, 0〉)) |
12 | 4, 11 | syl 17 |
. . . . . . 7
⊢ (𝑀 ∈ (0...0) → ((𝐴 ++ 𝐵) substr 〈𝑀, 0〉) = (𝐴 substr 〈𝑀, 0〉)) |
13 | | oveq2 7239 |
. . . . . . . . 9
⊢ (𝑁 = 0 → (0...𝑁) = (0...0)) |
14 | 13 | eleq2d 2824 |
. . . . . . . 8
⊢ (𝑁 = 0 → (𝑀 ∈ (0...𝑁) ↔ 𝑀 ∈ (0...0))) |
15 | | opeq2 4799 |
. . . . . . . . . 10
⊢ (𝑁 = 0 → 〈𝑀, 𝑁〉 = 〈𝑀, 0〉) |
16 | 15 | oveq2d 7247 |
. . . . . . . . 9
⊢ (𝑁 = 0 → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = ((𝐴 ++ 𝐵) substr 〈𝑀, 0〉)) |
17 | 15 | oveq2d 7247 |
. . . . . . . . 9
⊢ (𝑁 = 0 → (𝐴 substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 0〉)) |
18 | 16, 17 | eqeq12d 2754 |
. . . . . . . 8
⊢ (𝑁 = 0 → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉) ↔ ((𝐴 ++ 𝐵) substr 〈𝑀, 0〉) = (𝐴 substr 〈𝑀, 0〉))) |
19 | 14, 18 | imbi12d 348 |
. . . . . . 7
⊢ (𝑁 = 0 → ((𝑀 ∈ (0...𝑁) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉)) ↔ (𝑀 ∈ (0...0) → ((𝐴 ++ 𝐵) substr 〈𝑀, 0〉) = (𝐴 substr 〈𝑀, 0〉)))) |
20 | 12, 19 | mpbiri 261 |
. . . . . 6
⊢ (𝑁 = 0 → (𝑀 ∈ (0...𝑁) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉))) |
21 | 3, 20 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ (0...0) → (𝑀 ∈ (0...𝑁) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉))) |
22 | 2, 21 | syl6bi 256 |
. . . 4
⊢
((♯‘𝐴) =
0 → (𝑁 ∈
(0...(♯‘𝐴))
→ (𝑀 ∈ (0...𝑁) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉)))) |
23 | 22 | impcomd 415 |
. . 3
⊢
((♯‘𝐴) =
0 → ((𝑀 ∈
(0...𝑁) ∧ 𝑁 ∈
(0...(♯‘𝐴)))
→ ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉))) |
24 | 23 | adantl 485 |
. 2
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) = 0) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉))) |
25 | | ccatcl 14153 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
26 | 25 | ad2antrr 726 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
27 | | simprl 771 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → 𝑀 ∈ (0...𝑁)) |
28 | | elfzelfzccat 14161 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ (0...(♯‘𝐴)) → 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵))))) |
29 | 28 | imp 410 |
. . . . . 6
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(♯‘𝐴))) → 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))) |
30 | 29 | ad2ant2rl 749 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))) |
31 | | swrdvalfn 14240 |
. . . . 5
⊢ (((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
32 | 26, 27, 30, 31 | syl3anc 1373 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
33 | | 3anass 1097 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))) ↔ (𝐴 ∈ Word 𝑉 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))))) |
34 | 33 | simplbi2 504 |
. . . . . . 7
⊢ (𝐴 ∈ Word 𝑉 → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))) → (𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))))) |
35 | 34 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))) → (𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))))) |
36 | 35 | imp 410 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → (𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) |
37 | | swrdvalfn 14240 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))) → (𝐴 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
38 | 36, 37 | syl 17 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → (𝐴 substr 〈𝑀, 𝑁〉) Fn (0..^(𝑁 − 𝑀))) |
39 | | simp-4l 783 |
. . . . . 6
⊢
(((((𝐴 ∈ Word
𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → 𝐴 ∈ Word 𝑉) |
40 | | simp-4r 784 |
. . . . . 6
⊢
(((((𝐴 ∈ Word
𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → 𝐵 ∈ Word 𝑉) |
41 | | elfznn0 13229 |
. . . . . . . . . 10
⊢ (𝑀 ∈ (0...𝑁) → 𝑀 ∈
ℕ0) |
42 | | nn0addcl 12149 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑘 + 𝑀) ∈
ℕ0) |
43 | 42 | expcom 417 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ (𝑘 ∈
ℕ0 → (𝑘 + 𝑀) ∈
ℕ0)) |
44 | 41, 43 | syl 17 |
. . . . . . . . 9
⊢ (𝑀 ∈ (0...𝑁) → (𝑘 ∈ ℕ0 → (𝑘 + 𝑀) ∈
ℕ0)) |
45 | 44 | ad2antrl 728 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → (𝑘 ∈ ℕ0 → (𝑘 + 𝑀) ∈
ℕ0)) |
46 | | elfzonn0 13311 |
. . . . . . . 8
⊢ (𝑘 ∈ (0..^(𝑁 − 𝑀)) → 𝑘 ∈ ℕ0) |
47 | 45, 46 | impel 509 |
. . . . . . 7
⊢
(((((𝐴 ∈ Word
𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (𝑘 + 𝑀) ∈
ℕ0) |
48 | | lencl 14112 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈
ℕ0) |
49 | | elnnne0 12128 |
. . . . . . . . . . . 12
⊢
((♯‘𝐴)
∈ ℕ ↔ ((♯‘𝐴) ∈ ℕ0 ∧
(♯‘𝐴) ≠
0)) |
50 | 49 | simplbi2 504 |
. . . . . . . . . . 11
⊢
((♯‘𝐴)
∈ ℕ0 → ((♯‘𝐴) ≠ 0 → (♯‘𝐴) ∈
ℕ)) |
51 | 48, 50 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Word 𝑉 → ((♯‘𝐴) ≠ 0 → (♯‘𝐴) ∈
ℕ)) |
52 | 51 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((♯‘𝐴) ≠ 0 → (♯‘𝐴) ∈
ℕ)) |
53 | 52 | imp 410 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) → (♯‘𝐴) ∈
ℕ) |
54 | 53 | ad2antrr 726 |
. . . . . . 7
⊢
(((((𝐴 ∈ Word
𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (♯‘𝐴) ∈ ℕ) |
55 | | elfzo0 13307 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0..^(𝑁 − 𝑀)) ↔ (𝑘 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀))) |
56 | | elfz2nn0 13227 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(0...(♯‘𝐴))
↔ (𝑁 ∈
ℕ0 ∧ (♯‘𝐴) ∈ ℕ0 ∧ 𝑁 ≤ (♯‘𝐴))) |
57 | | nn0re 12123 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
58 | 57 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ 𝑘 ∈
ℝ) |
59 | | nn0re 12123 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
60 | 59 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ 𝑀 ∈
ℝ) |
61 | | nn0re 12123 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
62 | 61 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ 𝑁 ∈
ℝ) |
63 | 58, 60, 62 | ltaddsubd 11456 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ ((𝑘 + 𝑀) < 𝑁 ↔ 𝑘 < (𝑁 − 𝑀))) |
64 | | nn0readdcl 12180 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑘 + 𝑀) ∈ ℝ) |
65 | 64 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ (𝑘 + 𝑀) ∈
ℝ) |
66 | | nn0re 12123 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((♯‘𝐴)
∈ ℕ0 → (♯‘𝐴) ∈ ℝ) |
67 | 66 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ (♯‘𝐴)
∈ ℝ) |
68 | | ltletr 10948 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑘 + 𝑀) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (♯‘𝐴) ∈ ℝ) →
(((𝑘 + 𝑀) < 𝑁 ∧ 𝑁 ≤ (♯‘𝐴)) → (𝑘 + 𝑀) < (♯‘𝐴))) |
69 | 65, 62, 67, 68 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ (((𝑘 + 𝑀) < 𝑁 ∧ 𝑁 ≤ (♯‘𝐴)) → (𝑘 + 𝑀) < (♯‘𝐴))) |
70 | 69 | expd 419 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ ((𝑘 + 𝑀) < 𝑁 → (𝑁 ≤ (♯‘𝐴) → (𝑘 + 𝑀) < (♯‘𝐴)))) |
71 | 63, 70 | sylbird 263 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) ∧ (𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0))
→ (𝑘 < (𝑁 − 𝑀) → (𝑁 ≤ (♯‘𝐴) → (𝑘 + 𝑀) < (♯‘𝐴)))) |
72 | 71 | ex 416 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) → ((𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝑘 < (𝑁 − 𝑀) → (𝑁 ≤ (♯‘𝐴) → (𝑘 + 𝑀) < (♯‘𝐴))))) |
73 | 72 | com24 95 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0) → (𝑁 ≤ (♯‘𝐴) → (𝑘 < (𝑁 − 𝑀) → ((𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝑘 + 𝑀) < (♯‘𝐴))))) |
74 | 73 | 3impia 1119 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0 ∧ 𝑁 ≤ (♯‘𝐴)) → (𝑘 < (𝑁 − 𝑀) → ((𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝑘 + 𝑀) < (♯‘𝐴)))) |
75 | 74 | com13 88 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑘 < (𝑁 − 𝑀) → ((𝑁 ∈ ℕ0 ∧
(♯‘𝐴) ∈
ℕ0 ∧ 𝑁
≤ (♯‘𝐴))
→ (𝑘 + 𝑀) < (♯‘𝐴)))) |
76 | 75 | impancom 455 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ0
∧ 𝑘 < (𝑁 − 𝑀)) → (𝑀 ∈ ℕ0 → ((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0 ∧ 𝑁 ≤ (♯‘𝐴)) → (𝑘 + 𝑀) < (♯‘𝐴)))) |
77 | 76 | 3adant2 1133 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℕ0
∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑀 ∈ ℕ0 → ((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0 ∧ 𝑁 ≤ (♯‘𝐴)) → (𝑘 + 𝑀) < (♯‘𝐴)))) |
78 | 77 | com13 88 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (♯‘𝐴)
∈ ℕ0 ∧ 𝑁 ≤ (♯‘𝐴)) → (𝑀 ∈ ℕ0 → ((𝑘 ∈ ℕ0
∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑘 + 𝑀) < (♯‘𝐴)))) |
79 | 56, 78 | sylbi 220 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(0...(♯‘𝐴))
→ (𝑀 ∈
ℕ0 → ((𝑘 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑘 + 𝑀) < (♯‘𝐴)))) |
80 | 41, 79 | mpan9 510 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))) → ((𝑘 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑘 + 𝑀) < (♯‘𝐴))) |
81 | 80 | adantl 485 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → ((𝑘 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 𝑘 < (𝑁 − 𝑀)) → (𝑘 + 𝑀) < (♯‘𝐴))) |
82 | 55, 81 | syl5bi 245 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → (𝑘 ∈ (0..^(𝑁 − 𝑀)) → (𝑘 + 𝑀) < (♯‘𝐴))) |
83 | 82 | imp 410 |
. . . . . . 7
⊢
(((((𝐴 ∈ Word
𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (𝑘 + 𝑀) < (♯‘𝐴)) |
84 | | elfzo0 13307 |
. . . . . . 7
⊢ ((𝑘 + 𝑀) ∈ (0..^(♯‘𝐴)) ↔ ((𝑘 + 𝑀) ∈ ℕ0 ∧
(♯‘𝐴) ∈
ℕ ∧ (𝑘 + 𝑀) < (♯‘𝐴))) |
85 | 47, 54, 83, 84 | syl3anbrc 1345 |
. . . . . 6
⊢
(((((𝐴 ∈ Word
𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (𝑘 + 𝑀) ∈ (0..^(♯‘𝐴))) |
86 | | ccatval1 14157 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ (𝑘 + 𝑀) ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘(𝑘 + 𝑀)) = (𝐴‘(𝑘 + 𝑀))) |
87 | 39, 40, 85, 86 | syl3anc 1373 |
. . . . 5
⊢
(((((𝐴 ∈ Word
𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → ((𝐴 ++ 𝐵)‘(𝑘 + 𝑀)) = (𝐴‘(𝑘 + 𝑀))) |
88 | 25 | ad5ant12 756 |
. . . . . 6
⊢
(((((𝐴 ∈ Word
𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
89 | | simplrl 777 |
. . . . . 6
⊢
(((((𝐴 ∈ Word
𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → 𝑀 ∈ (0...𝑁)) |
90 | 30 | adantr 484 |
. . . . . 6
⊢
(((((𝐴 ∈ Word
𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))) |
91 | | simpr 488 |
. . . . . 6
⊢
(((((𝐴 ∈ Word
𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → 𝑘 ∈ (0..^(𝑁 − 𝑀))) |
92 | | swrdfv 14237 |
. . . . . 6
⊢ ((((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝑘) = ((𝐴 ++ 𝐵)‘(𝑘 + 𝑀))) |
93 | 88, 89, 90, 91, 92 | syl31anc 1375 |
. . . . 5
⊢
(((((𝐴 ∈ Word
𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝑘) = ((𝐴 ++ 𝐵)‘(𝑘 + 𝑀))) |
94 | | swrdfv 14237 |
. . . . . 6
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → ((𝐴 substr 〈𝑀, 𝑁〉)‘𝑘) = (𝐴‘(𝑘 + 𝑀))) |
95 | 36, 94 | sylan 583 |
. . . . 5
⊢
(((((𝐴 ∈ Word
𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → ((𝐴 substr 〈𝑀, 𝑁〉)‘𝑘) = (𝐴‘(𝑘 + 𝑀))) |
96 | 87, 93, 95 | 3eqtr4d 2788 |
. . . 4
⊢
(((((𝐴 ∈ Word
𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) ∧ 𝑘 ∈ (0..^(𝑁 − 𝑀))) → (((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉)‘𝑘) = ((𝐴 substr 〈𝑀, 𝑁〉)‘𝑘)) |
97 | 32, 38, 96 | eqfnfvd 6873 |
. . 3
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉)) |
98 | 97 | ex 416 |
. 2
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐴) ≠ 0) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉))) |
99 | 24, 98 | pm2.61dane 3030 |
1
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝐴))) → ((𝐴 ++ 𝐵) substr 〈𝑀, 𝑁〉) = (𝐴 substr 〈𝑀, 𝑁〉))) |