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 14646 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(♯‘𝑆)) ∧ 𝑅 ∈ Word 𝐴)) → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩))) |
6 | 1, 2, 3, 4, 5 | syl13anc 1373 |
. . 3
⊢ (𝜑 → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩))) |
7 | 6 | fveq2d 6851 |
. 2
⊢ (𝜑 → (♯‘(𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩)) = (♯‘(((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)))) |
8 | | pfxcl 14572 |
. . . . 5
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix 𝐹) ∈ Word 𝐴) |
9 | 1, 8 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑆 prefix 𝐹) ∈ Word 𝐴) |
10 | | ccatcl 14469 |
. . . 4
⊢ (((𝑆 prefix 𝐹) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → ((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴) |
11 | 9, 4, 10 | syl2anc 585 |
. . 3
⊢ (𝜑 → ((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴) |
12 | | swrdcl 14540 |
. . . 4
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩) ∈ Word 𝐴) |
13 | 1, 12 | syl 17 |
. . 3
⊢ (𝜑 → (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩) ∈ Word 𝐴) |
14 | | ccatlen 14470 |
. . 3
⊢ ((((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴 ∧ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩) ∈ Word 𝐴) → (♯‘(((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩))) = ((♯‘((𝑆 prefix 𝐹) ++ 𝑅)) + (♯‘(𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)))) |
15 | 11, 13, 14 | syl2anc 585 |
. 2
⊢ (𝜑 → (♯‘(((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩))) = ((♯‘((𝑆 prefix 𝐹) ++ 𝑅)) + (♯‘(𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)))) |
16 | | lencl 14428 |
. . . . . . 7
⊢ (𝑅 ∈ Word 𝐴 → (♯‘𝑅) ∈
ℕ0) |
17 | 16 | nn0cnd 12482 |
. . . . . 6
⊢ (𝑅 ∈ Word 𝐴 → (♯‘𝑅) ∈ ℂ) |
18 | 4, 17 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘𝑅) ∈
ℂ) |
19 | | elfzelz 13448 |
. . . . . . 7
⊢ (𝐹 ∈ (0...𝑇) → 𝐹 ∈ ℤ) |
20 | 19 | zcnd 12615 |
. . . . . 6
⊢ (𝐹 ∈ (0...𝑇) → 𝐹 ∈ ℂ) |
21 | 2, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ ℂ) |
22 | 18, 21 | addcld 11181 |
. . . 4
⊢ (𝜑 → ((♯‘𝑅) + 𝐹) ∈ ℂ) |
23 | | elfzel2 13446 |
. . . . . 6
⊢ (𝑇 ∈
(0...(♯‘𝑆))
→ (♯‘𝑆)
∈ ℤ) |
24 | 23 | zcnd 12615 |
. . . . 5
⊢ (𝑇 ∈
(0...(♯‘𝑆))
→ (♯‘𝑆)
∈ ℂ) |
25 | 3, 24 | syl 17 |
. . . 4
⊢ (𝜑 → (♯‘𝑆) ∈
ℂ) |
26 | | elfzelz 13448 |
. . . . . 6
⊢ (𝑇 ∈
(0...(♯‘𝑆))
→ 𝑇 ∈
ℤ) |
27 | 26 | zcnd 12615 |
. . . . 5
⊢ (𝑇 ∈
(0...(♯‘𝑆))
→ 𝑇 ∈
ℂ) |
28 | 3, 27 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ ℂ) |
29 | 22, 25, 28 | addsub12d 11542 |
. . 3
⊢ (𝜑 → (((♯‘𝑅) + 𝐹) + ((♯‘𝑆) − 𝑇)) = ((♯‘𝑆) + (((♯‘𝑅) + 𝐹) − 𝑇))) |
30 | | ccatlen 14470 |
. . . . . 6
⊢ (((𝑆 prefix 𝐹) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅))) |
31 | 9, 4, 30 | syl2anc 585 |
. . . . 5
⊢ (𝜑 → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅))) |
32 | | elfzuz 13444 |
. . . . . . . . 9
⊢ (𝐹 ∈ (0...𝑇) → 𝐹 ∈
(ℤ≥‘0)) |
33 | 2, 32 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈
(ℤ≥‘0)) |
34 | | elfzuz3 13445 |
. . . . . . . . . 10
⊢ (𝑇 ∈
(0...(♯‘𝑆))
→ (♯‘𝑆)
∈ (ℤ≥‘𝑇)) |
35 | 3, 34 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘𝑆) ∈
(ℤ≥‘𝑇)) |
36 | | elfzuz3 13445 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (0...𝑇) → 𝑇 ∈ (ℤ≥‘𝐹)) |
37 | 2, 36 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ (ℤ≥‘𝐹)) |
38 | | uztrn 12788 |
. . . . . . . . 9
⊢
(((♯‘𝑆)
∈ (ℤ≥‘𝑇) ∧ 𝑇 ∈ (ℤ≥‘𝐹)) → (♯‘𝑆) ∈
(ℤ≥‘𝐹)) |
39 | 35, 37, 38 | syl2anc 585 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝑆) ∈
(ℤ≥‘𝐹)) |
40 | | elfzuzb 13442 |
. . . . . . . 8
⊢ (𝐹 ∈
(0...(♯‘𝑆))
↔ (𝐹 ∈
(ℤ≥‘0) ∧ (♯‘𝑆) ∈ (ℤ≥‘𝐹))) |
41 | 33, 39, 40 | sylanbrc 584 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (0...(♯‘𝑆))) |
42 | | pfxlen 14578 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 prefix 𝐹)) = 𝐹) |
43 | 1, 41, 42 | syl2anc 585 |
. . . . . 6
⊢ (𝜑 → (♯‘(𝑆 prefix 𝐹)) = 𝐹) |
44 | 43 | oveq1d 7377 |
. . . . 5
⊢ (𝜑 → ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅)) = (𝐹 + (♯‘𝑅))) |
45 | 21, 18 | addcomd 11364 |
. . . . 5
⊢ (𝜑 → (𝐹 + (♯‘𝑅)) = ((♯‘𝑅) + 𝐹)) |
46 | 31, 44, 45 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = ((♯‘𝑅) + 𝐹)) |
47 | | elfzuz2 13453 |
. . . . . 6
⊢ (𝑇 ∈
(0...(♯‘𝑆))
→ (♯‘𝑆)
∈ (ℤ≥‘0)) |
48 | | eluzfz2 13456 |
. . . . . 6
⊢
((♯‘𝑆)
∈ (ℤ≥‘0) → (♯‘𝑆) ∈ (0...(♯‘𝑆))) |
49 | 3, 47, 48 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (♯‘𝑆) ∈
(0...(♯‘𝑆))) |
50 | | swrdlen 14542 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ (0...(♯‘𝑆)) ∧ (♯‘𝑆) ∈
(0...(♯‘𝑆)))
→ (♯‘(𝑆
substr ⟨𝑇,
(♯‘𝑆)⟩)) =
((♯‘𝑆) −
𝑇)) |
51 | 1, 3, 49, 50 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → (♯‘(𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)) = ((♯‘𝑆) − 𝑇)) |
52 | 46, 51 | oveq12d 7380 |
. . 3
⊢ (𝜑 → ((♯‘((𝑆 prefix 𝐹) ++ 𝑅)) + (♯‘(𝑆 substr ⟨𝑇, (♯‘𝑆)⟩))) = (((♯‘𝑅) + 𝐹) + ((♯‘𝑆) − 𝑇))) |
53 | 18, 28, 21 | subsub3d 11549 |
. . . 4
⊢ (𝜑 → ((♯‘𝑅) − (𝑇 − 𝐹)) = (((♯‘𝑅) + 𝐹) − 𝑇)) |
54 | 53 | oveq2d 7378 |
. . 3
⊢ (𝜑 → ((♯‘𝑆) + ((♯‘𝑅) − (𝑇 − 𝐹))) = ((♯‘𝑆) + (((♯‘𝑅) + 𝐹) − 𝑇))) |
55 | 29, 52, 54 | 3eqtr4d 2787 |
. 2
⊢ (𝜑 → ((♯‘((𝑆 prefix 𝐹) ++ 𝑅)) + (♯‘(𝑆 substr ⟨𝑇, (♯‘𝑆)⟩))) = ((♯‘𝑆) + ((♯‘𝑅) − (𝑇 − 𝐹)))) |
56 | 7, 15, 55 | 3eqtrd 2781 |
1
⊢ (𝜑 → (♯‘(𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩)) = ((♯‘𝑆) + ((♯‘𝑅) − (𝑇 − 𝐹)))) |