Proof of Theorem splfv2a
Step | Hyp | Ref
| Expression |
1 | | spllen.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ Word 𝐴) |
2 | | spllen.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (0...𝑇)) |
3 | | spllen.t |
. . . 4
⊢ (𝜑 → 𝑇 ∈ (0...(♯‘𝑆))) |
4 | | spllen.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Word 𝐴) |
5 | | splval 14316 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(♯‘𝑆)) ∧ 𝑅 ∈ Word 𝐴)) → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))) |
6 | 1, 2, 3, 4, 5 | syl13anc 1374 |
. . 3
⊢ (𝜑 → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))) |
7 | | elfznn0 13205 |
. . . . . . 7
⊢ (𝐹 ∈ (0...𝑇) → 𝐹 ∈
ℕ0) |
8 | 2, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈
ℕ0) |
9 | 8 | nn0cnd 12152 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ ℂ) |
10 | | splfv2a.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (0..^(♯‘𝑅))) |
11 | | elfzonn0 13287 |
. . . . . . 7
⊢ (𝑋 ∈
(0..^(♯‘𝑅))
→ 𝑋 ∈
ℕ0) |
12 | 10, 11 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈
ℕ0) |
13 | 12 | nn0cnd 12152 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ ℂ) |
14 | 9, 13 | addcomd 11034 |
. . . 4
⊢ (𝜑 → (𝐹 + 𝑋) = (𝑋 + 𝐹)) |
15 | | nn0uz 12476 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) |
16 | 8, 15 | eleqtrdi 2848 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈
(ℤ≥‘0)) |
17 | | elfzuz3 13109 |
. . . . . . . . 9
⊢ (𝑇 ∈
(0...(♯‘𝑆))
→ (♯‘𝑆)
∈ (ℤ≥‘𝑇)) |
18 | 3, 17 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝑆) ∈
(ℤ≥‘𝑇)) |
19 | | elfzuz3 13109 |
. . . . . . . . 9
⊢ (𝐹 ∈ (0...𝑇) → 𝑇 ∈ (ℤ≥‘𝐹)) |
20 | 2, 19 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ (ℤ≥‘𝐹)) |
21 | | uztrn 12456 |
. . . . . . . 8
⊢
(((♯‘𝑆)
∈ (ℤ≥‘𝑇) ∧ 𝑇 ∈ (ℤ≥‘𝐹)) → (♯‘𝑆) ∈
(ℤ≥‘𝐹)) |
22 | 18, 20, 21 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝑆) ∈
(ℤ≥‘𝐹)) |
23 | | elfzuzb 13106 |
. . . . . . 7
⊢ (𝐹 ∈
(0...(♯‘𝑆))
↔ (𝐹 ∈
(ℤ≥‘0) ∧ (♯‘𝑆) ∈ (ℤ≥‘𝐹))) |
24 | 16, 22, 23 | sylanbrc 586 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (0...(♯‘𝑆))) |
25 | | pfxlen 14248 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 prefix 𝐹)) = 𝐹) |
26 | 1, 24, 25 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (♯‘(𝑆 prefix 𝐹)) = 𝐹) |
27 | 26 | oveq2d 7229 |
. . . 4
⊢ (𝜑 → (𝑋 + (♯‘(𝑆 prefix 𝐹))) = (𝑋 + 𝐹)) |
28 | 14, 27 | eqtr4d 2780 |
. . 3
⊢ (𝜑 → (𝐹 + 𝑋) = (𝑋 + (♯‘(𝑆 prefix 𝐹)))) |
29 | 6, 28 | fveq12d 6724 |
. 2
⊢ (𝜑 → ((𝑆 splice 〈𝐹, 𝑇, 𝑅〉)‘(𝐹 + 𝑋)) = ((((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))‘(𝑋 + (♯‘(𝑆 prefix 𝐹))))) |
30 | | pfxcl 14242 |
. . . . 5
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix 𝐹) ∈ Word 𝐴) |
31 | 1, 30 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑆 prefix 𝐹) ∈ Word 𝐴) |
32 | | ccatcl 14129 |
. . . 4
⊢ (((𝑆 prefix 𝐹) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → ((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴) |
33 | 31, 4, 32 | syl2anc 587 |
. . 3
⊢ (𝜑 → ((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴) |
34 | | swrdcl 14210 |
. . . 4
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑇, (♯‘𝑆)〉) ∈ Word 𝐴) |
35 | 1, 34 | syl 17 |
. . 3
⊢ (𝜑 → (𝑆 substr 〈𝑇, (♯‘𝑆)〉) ∈ Word 𝐴) |
36 | | 0nn0 12105 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
37 | | nn0addcl 12125 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ 𝐹 ∈ ℕ0) → (0 +
𝐹) ∈
ℕ0) |
38 | 36, 8, 37 | sylancr 590 |
. . . . . . 7
⊢ (𝜑 → (0 + 𝐹) ∈
ℕ0) |
39 | | fzoss1 13269 |
. . . . . . . 8
⊢ ((0 +
𝐹) ∈
(ℤ≥‘0) → ((0 + 𝐹)..^((♯‘𝑅) + 𝐹)) ⊆ (0..^((♯‘𝑅) + 𝐹))) |
40 | 39, 15 | eleq2s 2856 |
. . . . . . 7
⊢ ((0 +
𝐹) ∈
ℕ0 → ((0 + 𝐹)..^((♯‘𝑅) + 𝐹)) ⊆ (0..^((♯‘𝑅) + 𝐹))) |
41 | 38, 40 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((0 + 𝐹)..^((♯‘𝑅) + 𝐹)) ⊆ (0..^((♯‘𝑅) + 𝐹))) |
42 | | ccatlen 14130 |
. . . . . . . . 9
⊢ (((𝑆 prefix 𝐹) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅))) |
43 | 31, 4, 42 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅))) |
44 | 26 | oveq1d 7228 |
. . . . . . . 8
⊢ (𝜑 → ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅)) = (𝐹 + (♯‘𝑅))) |
45 | | lencl 14088 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Word 𝐴 → (♯‘𝑅) ∈
ℕ0) |
46 | 4, 45 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝑅) ∈
ℕ0) |
47 | 46 | nn0cnd 12152 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘𝑅) ∈
ℂ) |
48 | 9, 47 | addcomd 11034 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 + (♯‘𝑅)) = ((♯‘𝑅) + 𝐹)) |
49 | 43, 44, 48 | 3eqtrd 2781 |
. . . . . . 7
⊢ (𝜑 → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = ((♯‘𝑅) + 𝐹)) |
50 | 49 | oveq2d 7229 |
. . . . . 6
⊢ (𝜑 →
(0..^(♯‘((𝑆
prefix 𝐹) ++ 𝑅))) = (0..^((♯‘𝑅) + 𝐹))) |
51 | 41, 50 | sseqtrrd 3942 |
. . . . 5
⊢ (𝜑 → ((0 + 𝐹)..^((♯‘𝑅) + 𝐹)) ⊆ (0..^(♯‘((𝑆 prefix 𝐹) ++ 𝑅)))) |
52 | 8 | nn0zd 12280 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ ℤ) |
53 | | fzoaddel 13295 |
. . . . . 6
⊢ ((𝑋 ∈
(0..^(♯‘𝑅))
∧ 𝐹 ∈ ℤ)
→ (𝑋 + 𝐹) ∈ ((0 + 𝐹)..^((♯‘𝑅) + 𝐹))) |
54 | 10, 52, 53 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝑋 + 𝐹) ∈ ((0 + 𝐹)..^((♯‘𝑅) + 𝐹))) |
55 | 51, 54 | sseldd 3902 |
. . . 4
⊢ (𝜑 → (𝑋 + 𝐹) ∈ (0..^(♯‘((𝑆 prefix 𝐹) ++ 𝑅)))) |
56 | 27, 55 | eqeltrd 2838 |
. . 3
⊢ (𝜑 → (𝑋 + (♯‘(𝑆 prefix 𝐹))) ∈ (0..^(♯‘((𝑆 prefix 𝐹) ++ 𝑅)))) |
57 | | ccatval1 14133 |
. . 3
⊢ ((((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑇, (♯‘𝑆)〉) ∈ Word 𝐴 ∧ (𝑋 + (♯‘(𝑆 prefix 𝐹))) ∈ (0..^(♯‘((𝑆 prefix 𝐹) ++ 𝑅)))) → ((((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))‘(𝑋 + (♯‘(𝑆 prefix 𝐹)))) = (((𝑆 prefix 𝐹) ++ 𝑅)‘(𝑋 + (♯‘(𝑆 prefix 𝐹))))) |
58 | 33, 35, 56, 57 | syl3anc 1373 |
. 2
⊢ (𝜑 → ((((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))‘(𝑋 + (♯‘(𝑆 prefix 𝐹)))) = (((𝑆 prefix 𝐹) ++ 𝑅)‘(𝑋 + (♯‘(𝑆 prefix 𝐹))))) |
59 | | ccatval3 14136 |
. . 3
⊢ (((𝑆 prefix 𝐹) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ∧ 𝑋 ∈ (0..^(♯‘𝑅))) → (((𝑆 prefix 𝐹) ++ 𝑅)‘(𝑋 + (♯‘(𝑆 prefix 𝐹)))) = (𝑅‘𝑋)) |
60 | 31, 4, 10, 59 | syl3anc 1373 |
. 2
⊢ (𝜑 → (((𝑆 prefix 𝐹) ++ 𝑅)‘(𝑋 + (♯‘(𝑆 prefix 𝐹)))) = (𝑅‘𝑋)) |
61 | 29, 58, 60 | 3eqtrd 2781 |
1
⊢ (𝜑 → ((𝑆 splice 〈𝐹, 𝑇, 𝑅〉)‘(𝐹 + 𝑋)) = (𝑅‘𝑋)) |