Proof of Theorem spllen
| 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 14789 | . . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(♯‘𝑆)) ∧ 𝑅 ∈ Word 𝐴)) → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))) | 
| 6 | 1, 2, 3, 4, 5 | syl13anc 1374 | . . 3
⊢ (𝜑 → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))) | 
| 7 | 6 | fveq2d 6910 | . 2
⊢ (𝜑 → (♯‘(𝑆 splice 〈𝐹, 𝑇, 𝑅〉)) = (♯‘(((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉)))) | 
| 8 |  | pfxcl 14715 | . . . . 5
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix 𝐹) ∈ Word 𝐴) | 
| 9 | 1, 8 | syl 17 | . . . 4
⊢ (𝜑 → (𝑆 prefix 𝐹) ∈ Word 𝐴) | 
| 10 |  | ccatcl 14612 | . . . 4
⊢ (((𝑆 prefix 𝐹) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → ((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴) | 
| 11 | 9, 4, 10 | syl2anc 584 | . . 3
⊢ (𝜑 → ((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴) | 
| 12 |  | swrdcl 14683 | . . . 4
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑇, (♯‘𝑆)〉) ∈ Word 𝐴) | 
| 13 | 1, 12 | syl 17 | . . 3
⊢ (𝜑 → (𝑆 substr 〈𝑇, (♯‘𝑆)〉) ∈ Word 𝐴) | 
| 14 |  | ccatlen 14613 | . . 3
⊢ ((((𝑆 prefix 𝐹) ++ 𝑅) ∈ Word 𝐴 ∧ (𝑆 substr 〈𝑇, (♯‘𝑆)〉) ∈ Word 𝐴) → (♯‘(((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))) = ((♯‘((𝑆 prefix 𝐹) ++ 𝑅)) + (♯‘(𝑆 substr 〈𝑇, (♯‘𝑆)〉)))) | 
| 15 | 11, 13, 14 | syl2anc 584 | . 2
⊢ (𝜑 → (♯‘(((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))) = ((♯‘((𝑆 prefix 𝐹) ++ 𝑅)) + (♯‘(𝑆 substr 〈𝑇, (♯‘𝑆)〉)))) | 
| 16 |  | lencl 14571 | . . . . . . 7
⊢ (𝑅 ∈ Word 𝐴 → (♯‘𝑅) ∈
ℕ0) | 
| 17 | 16 | nn0cnd 12589 | . . . . . 6
⊢ (𝑅 ∈ Word 𝐴 → (♯‘𝑅) ∈ ℂ) | 
| 18 | 4, 17 | syl 17 | . . . . 5
⊢ (𝜑 → (♯‘𝑅) ∈
ℂ) | 
| 19 |  | elfzelz 13564 | . . . . . . 7
⊢ (𝐹 ∈ (0...𝑇) → 𝐹 ∈ ℤ) | 
| 20 | 19 | zcnd 12723 | . . . . . 6
⊢ (𝐹 ∈ (0...𝑇) → 𝐹 ∈ ℂ) | 
| 21 | 2, 20 | syl 17 | . . . . 5
⊢ (𝜑 → 𝐹 ∈ ℂ) | 
| 22 | 18, 21 | addcld 11280 | . . . 4
⊢ (𝜑 → ((♯‘𝑅) + 𝐹) ∈ ℂ) | 
| 23 |  | elfzel2 13562 | . . . . . 6
⊢ (𝑇 ∈
(0...(♯‘𝑆))
→ (♯‘𝑆)
∈ ℤ) | 
| 24 | 23 | zcnd 12723 | . . . . 5
⊢ (𝑇 ∈
(0...(♯‘𝑆))
→ (♯‘𝑆)
∈ ℂ) | 
| 25 | 3, 24 | syl 17 | . . . 4
⊢ (𝜑 → (♯‘𝑆) ∈
ℂ) | 
| 26 |  | elfzelz 13564 | . . . . . 6
⊢ (𝑇 ∈
(0...(♯‘𝑆))
→ 𝑇 ∈
ℤ) | 
| 27 | 26 | zcnd 12723 | . . . . 5
⊢ (𝑇 ∈
(0...(♯‘𝑆))
→ 𝑇 ∈
ℂ) | 
| 28 | 3, 27 | syl 17 | . . . 4
⊢ (𝜑 → 𝑇 ∈ ℂ) | 
| 29 | 22, 25, 28 | addsub12d 11643 | . . 3
⊢ (𝜑 → (((♯‘𝑅) + 𝐹) + ((♯‘𝑆) − 𝑇)) = ((♯‘𝑆) + (((♯‘𝑅) + 𝐹) − 𝑇))) | 
| 30 |  | ccatlen 14613 | . . . . . 6
⊢ (((𝑆 prefix 𝐹) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅))) | 
| 31 | 9, 4, 30 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅))) | 
| 32 |  | elfzuz 13560 | . . . . . . . . 9
⊢ (𝐹 ∈ (0...𝑇) → 𝐹 ∈
(ℤ≥‘0)) | 
| 33 | 2, 32 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝐹 ∈
(ℤ≥‘0)) | 
| 34 |  | elfzuz3 13561 | . . . . . . . . . 10
⊢ (𝑇 ∈
(0...(♯‘𝑆))
→ (♯‘𝑆)
∈ (ℤ≥‘𝑇)) | 
| 35 | 3, 34 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (♯‘𝑆) ∈
(ℤ≥‘𝑇)) | 
| 36 |  | elfzuz3 13561 | . . . . . . . . . 10
⊢ (𝐹 ∈ (0...𝑇) → 𝑇 ∈ (ℤ≥‘𝐹)) | 
| 37 | 2, 36 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ (ℤ≥‘𝐹)) | 
| 38 |  | uztrn 12896 | . . . . . . . . 9
⊢
(((♯‘𝑆)
∈ (ℤ≥‘𝑇) ∧ 𝑇 ∈ (ℤ≥‘𝐹)) → (♯‘𝑆) ∈
(ℤ≥‘𝐹)) | 
| 39 | 35, 37, 38 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (♯‘𝑆) ∈
(ℤ≥‘𝐹)) | 
| 40 |  | elfzuzb 13558 | . . . . . . . 8
⊢ (𝐹 ∈
(0...(♯‘𝑆))
↔ (𝐹 ∈
(ℤ≥‘0) ∧ (♯‘𝑆) ∈ (ℤ≥‘𝐹))) | 
| 41 | 33, 39, 40 | sylanbrc 583 | . . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (0...(♯‘𝑆))) | 
| 42 |  | pfxlen 14721 | . . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 prefix 𝐹)) = 𝐹) | 
| 43 | 1, 41, 42 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (♯‘(𝑆 prefix 𝐹)) = 𝐹) | 
| 44 | 43 | oveq1d 7446 | . . . . 5
⊢ (𝜑 → ((♯‘(𝑆 prefix 𝐹)) + (♯‘𝑅)) = (𝐹 + (♯‘𝑅))) | 
| 45 | 21, 18 | addcomd 11463 | . . . . 5
⊢ (𝜑 → (𝐹 + (♯‘𝑅)) = ((♯‘𝑅) + 𝐹)) | 
| 46 | 31, 44, 45 | 3eqtrd 2781 | . . . 4
⊢ (𝜑 → (♯‘((𝑆 prefix 𝐹) ++ 𝑅)) = ((♯‘𝑅) + 𝐹)) | 
| 47 |  | elfzuz2 13569 | . . . . . 6
⊢ (𝑇 ∈
(0...(♯‘𝑆))
→ (♯‘𝑆)
∈ (ℤ≥‘0)) | 
| 48 |  | eluzfz2 13572 | . . . . . 6
⊢
((♯‘𝑆)
∈ (ℤ≥‘0) → (♯‘𝑆) ∈ (0...(♯‘𝑆))) | 
| 49 | 3, 47, 48 | 3syl 18 | . . . . 5
⊢ (𝜑 → (♯‘𝑆) ∈
(0...(♯‘𝑆))) | 
| 50 |  | swrdlen 14685 | . . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ (0...(♯‘𝑆)) ∧ (♯‘𝑆) ∈
(0...(♯‘𝑆)))
→ (♯‘(𝑆
substr 〈𝑇,
(♯‘𝑆)〉)) =
((♯‘𝑆) −
𝑇)) | 
| 51 | 1, 3, 49, 50 | syl3anc 1373 | . . . 4
⊢ (𝜑 → (♯‘(𝑆 substr 〈𝑇, (♯‘𝑆)〉)) = ((♯‘𝑆) − 𝑇)) | 
| 52 | 46, 51 | oveq12d 7449 | . . 3
⊢ (𝜑 → ((♯‘((𝑆 prefix 𝐹) ++ 𝑅)) + (♯‘(𝑆 substr 〈𝑇, (♯‘𝑆)〉))) = (((♯‘𝑅) + 𝐹) + ((♯‘𝑆) − 𝑇))) | 
| 53 | 18, 28, 21 | subsub3d 11650 | . . . 4
⊢ (𝜑 → ((♯‘𝑅) − (𝑇 − 𝐹)) = (((♯‘𝑅) + 𝐹) − 𝑇)) | 
| 54 | 53 | oveq2d 7447 | . . 3
⊢ (𝜑 → ((♯‘𝑆) + ((♯‘𝑅) − (𝑇 − 𝐹))) = ((♯‘𝑆) + (((♯‘𝑅) + 𝐹) − 𝑇))) | 
| 55 | 29, 52, 54 | 3eqtr4d 2787 | . 2
⊢ (𝜑 → ((♯‘((𝑆 prefix 𝐹) ++ 𝑅)) + (♯‘(𝑆 substr 〈𝑇, (♯‘𝑆)〉))) = ((♯‘𝑆) + ((♯‘𝑅) − (𝑇 − 𝐹)))) | 
| 56 | 7, 15, 55 | 3eqtrd 2781 | 1
⊢ (𝜑 → (♯‘(𝑆 splice 〈𝐹, 𝑇, 𝑅〉)) = ((♯‘𝑆) + ((♯‘𝑅) − (𝑇 − 𝐹)))) |