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 13502 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(#‘𝑆)) ∧ 𝑅 ∈ Word 𝐴)) → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉))) |
6 | 1, 2, 3, 4, 5 | syl13anc 1328 |
. . 3
⊢ (𝜑 → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉))) |
7 | | elfznn0 12433 |
. . . . . . 7
⊢ (𝐹 ∈ (0...𝑇) → 𝐹 ∈
ℕ0) |
8 | 2, 7 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈
ℕ0) |
9 | 8 | nn0cnd 11353 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ ℂ) |
10 | | splfv2a.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (0..^(#‘𝑅))) |
11 | | elfzoelz 12470 |
. . . . . . 7
⊢ (𝑋 ∈ (0..^(#‘𝑅)) → 𝑋 ∈ ℤ) |
12 | 10, 11 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ ℤ) |
13 | 12 | zcnd 11483 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ ℂ) |
14 | 9, 13 | addcomd 10238 |
. . . 4
⊢ (𝜑 → (𝐹 + 𝑋) = (𝑋 + 𝐹)) |
15 | | nn0uz 11722 |
. . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) |
16 | 8, 15 | syl6eleq 2711 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈
(ℤ≥‘0)) |
17 | | eluzfz1 12348 |
. . . . . . . 8
⊢ (𝐹 ∈
(ℤ≥‘0) → 0 ∈ (0...𝐹)) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 0 ∈ (0...𝐹)) |
19 | | elfzuz3 12339 |
. . . . . . . . . 10
⊢ (𝑇 ∈ (0...(#‘𝑆)) → (#‘𝑆) ∈
(ℤ≥‘𝑇)) |
20 | 3, 19 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝑆) ∈ (ℤ≥‘𝑇)) |
21 | | elfzuz3 12339 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (0...𝑇) → 𝑇 ∈ (ℤ≥‘𝐹)) |
22 | 2, 21 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ (ℤ≥‘𝐹)) |
23 | | uztrn 11704 |
. . . . . . . . 9
⊢
(((#‘𝑆) ∈
(ℤ≥‘𝑇) ∧ 𝑇 ∈ (ℤ≥‘𝐹)) → (#‘𝑆) ∈
(ℤ≥‘𝐹)) |
24 | 20, 22, 23 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (#‘𝑆) ∈ (ℤ≥‘𝐹)) |
25 | | elfzuzb 12336 |
. . . . . . . 8
⊢ (𝐹 ∈ (0...(#‘𝑆)) ↔ (𝐹 ∈ (ℤ≥‘0)
∧ (#‘𝑆) ∈
(ℤ≥‘𝐹))) |
26 | 16, 24, 25 | sylanbrc 698 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (0...(#‘𝑆))) |
27 | | swrdlen 13423 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 0 ∈ (0...𝐹) ∧ 𝐹 ∈ (0...(#‘𝑆))) → (#‘(𝑆 substr 〈0, 𝐹〉)) = (𝐹 − 0)) |
28 | 1, 18, 26, 27 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → (#‘(𝑆 substr 〈0, 𝐹〉)) = (𝐹 − 0)) |
29 | 9 | subid1d 10381 |
. . . . . 6
⊢ (𝜑 → (𝐹 − 0) = 𝐹) |
30 | 28, 29 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → (#‘(𝑆 substr 〈0, 𝐹〉)) = 𝐹) |
31 | 30 | oveq2d 6666 |
. . . 4
⊢ (𝜑 → (𝑋 + (#‘(𝑆 substr 〈0, 𝐹〉))) = (𝑋 + 𝐹)) |
32 | 14, 31 | eqtr4d 2659 |
. . 3
⊢ (𝜑 → (𝐹 + 𝑋) = (𝑋 + (#‘(𝑆 substr 〈0, 𝐹〉)))) |
33 | 6, 32 | fveq12d 6197 |
. 2
⊢ (𝜑 → ((𝑆 splice 〈𝐹, 𝑇, 𝑅〉)‘(𝐹 + 𝑋)) = ((((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉))‘(𝑋 + (#‘(𝑆 substr 〈0, 𝐹〉))))) |
34 | | swrdcl 13419 |
. . . . 5
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈0, 𝐹〉) ∈ Word 𝐴) |
35 | 1, 34 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑆 substr 〈0, 𝐹〉) ∈ Word 𝐴) |
36 | | ccatcl 13359 |
. . . 4
⊢ (((𝑆 substr 〈0, 𝐹〉) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → ((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ∈ Word 𝐴) |
37 | 35, 4, 36 | syl2anc 693 |
. . 3
⊢ (𝜑 → ((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ∈ Word 𝐴) |
38 | | swrdcl 13419 |
. . . 4
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑇, (#‘𝑆)〉) ∈ Word 𝐴) |
39 | 1, 38 | syl 17 |
. . 3
⊢ (𝜑 → (𝑆 substr 〈𝑇, (#‘𝑆)〉) ∈ Word 𝐴) |
40 | | 0nn0 11307 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
41 | | nn0addcl 11328 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ 𝐹 ∈ ℕ0) → (0 +
𝐹) ∈
ℕ0) |
42 | 40, 8, 41 | sylancr 695 |
. . . . . . 7
⊢ (𝜑 → (0 + 𝐹) ∈
ℕ0) |
43 | | fzoss1 12495 |
. . . . . . . 8
⊢ ((0 +
𝐹) ∈
(ℤ≥‘0) → ((0 + 𝐹)..^((#‘𝑅) + 𝐹)) ⊆ (0..^((#‘𝑅) + 𝐹))) |
44 | 43, 15 | eleq2s 2719 |
. . . . . . 7
⊢ ((0 +
𝐹) ∈
ℕ0 → ((0 + 𝐹)..^((#‘𝑅) + 𝐹)) ⊆ (0..^((#‘𝑅) + 𝐹))) |
45 | 42, 44 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((0 + 𝐹)..^((#‘𝑅) + 𝐹)) ⊆ (0..^((#‘𝑅) + 𝐹))) |
46 | | ccatlen 13360 |
. . . . . . . . 9
⊢ (((𝑆 substr 〈0, 𝐹〉) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)) = ((#‘(𝑆 substr 〈0, 𝐹〉)) + (#‘𝑅))) |
47 | 35, 4, 46 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)) = ((#‘(𝑆 substr 〈0, 𝐹〉)) + (#‘𝑅))) |
48 | 30 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝜑 → ((#‘(𝑆 substr 〈0, 𝐹〉)) + (#‘𝑅)) = (𝐹 + (#‘𝑅))) |
49 | | wrdfin 13323 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Word 𝐴 → 𝑅 ∈ Fin) |
50 | 4, 49 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ Fin) |
51 | | hashcl 13147 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Fin →
(#‘𝑅) ∈
ℕ0) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘𝑅) ∈
ℕ0) |
53 | 52 | nn0cnd 11353 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝑅) ∈ ℂ) |
54 | 9, 53 | addcomd 10238 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 + (#‘𝑅)) = ((#‘𝑅) + 𝐹)) |
55 | 47, 48, 54 | 3eqtrd 2660 |
. . . . . . 7
⊢ (𝜑 → (#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)) = ((#‘𝑅) + 𝐹)) |
56 | 55 | oveq2d 6666 |
. . . . . 6
⊢ (𝜑 → (0..^(#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅))) = (0..^((#‘𝑅) + 𝐹))) |
57 | 45, 56 | sseqtr4d 3642 |
. . . . 5
⊢ (𝜑 → ((0 + 𝐹)..^((#‘𝑅) + 𝐹)) ⊆ (0..^(#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)))) |
58 | 8 | nn0zd 11480 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ ℤ) |
59 | | fzoaddel 12520 |
. . . . . 6
⊢ ((𝑋 ∈ (0..^(#‘𝑅)) ∧ 𝐹 ∈ ℤ) → (𝑋 + 𝐹) ∈ ((0 + 𝐹)..^((#‘𝑅) + 𝐹))) |
60 | 10, 58, 59 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (𝑋 + 𝐹) ∈ ((0 + 𝐹)..^((#‘𝑅) + 𝐹))) |
61 | 57, 60 | sseldd 3604 |
. . . 4
⊢ (𝜑 → (𝑋 + 𝐹) ∈ (0..^(#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)))) |
62 | 31, 61 | eqeltrd 2701 |
. . 3
⊢ (𝜑 → (𝑋 + (#‘(𝑆 substr 〈0, 𝐹〉))) ∈ (0..^(#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)))) |
63 | | ccatval1 13361 |
. . 3
⊢ ((((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑇, (#‘𝑆)〉) ∈ Word 𝐴 ∧ (𝑋 + (#‘(𝑆 substr 〈0, 𝐹〉))) ∈ (0..^(#‘((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)))) → ((((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉))‘(𝑋 + (#‘(𝑆 substr 〈0, 𝐹〉)))) = (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)‘(𝑋 + (#‘(𝑆 substr 〈0, 𝐹〉))))) |
64 | 37, 39, 62, 63 | syl3anc 1326 |
. 2
⊢ (𝜑 → ((((𝑆 substr 〈0, 𝐹〉) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (#‘𝑆)〉))‘(𝑋 + (#‘(𝑆 substr 〈0, 𝐹〉)))) = (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)‘(𝑋 + (#‘(𝑆 substr 〈0, 𝐹〉))))) |
65 | | ccatval3 13363 |
. . 3
⊢ (((𝑆 substr 〈0, 𝐹〉) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ∧ 𝑋 ∈ (0..^(#‘𝑅))) → (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)‘(𝑋 + (#‘(𝑆 substr 〈0, 𝐹〉)))) = (𝑅‘𝑋)) |
66 | 35, 4, 10, 65 | syl3anc 1326 |
. 2
⊢ (𝜑 → (((𝑆 substr 〈0, 𝐹〉) ++ 𝑅)‘(𝑋 + (#‘(𝑆 substr 〈0, 𝐹〉)))) = (𝑅‘𝑋)) |
67 | 33, 64, 66 | 3eqtrd 2660 |
1
⊢ (𝜑 → ((𝑆 splice 〈𝐹, 𝑇, 𝑅〉)‘(𝐹 + 𝑋)) = (𝑅‘𝑋)) |