Proof of Theorem splval2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | splval2.s | . . . 4
⊢ (𝜑 → 𝑆 = ((𝐴 ++ 𝐵) ++ 𝐶)) | 
| 2 |  | splval2.a | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ Word 𝑋) | 
| 3 |  | splval2.b | . . . . . 6
⊢ (𝜑 → 𝐵 ∈ Word 𝑋) | 
| 4 |  | ccatcl 14613 | . . . . . 6
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) → (𝐴 ++ 𝐵) ∈ Word 𝑋) | 
| 5 | 2, 3, 4 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝐴 ++ 𝐵) ∈ Word 𝑋) | 
| 6 |  | splval2.c | . . . . 5
⊢ (𝜑 → 𝐶 ∈ Word 𝑋) | 
| 7 |  | ccatcl 14613 | . . . . 5
⊢ (((𝐴 ++ 𝐵) ∈ Word 𝑋 ∧ 𝐶 ∈ Word 𝑋) → ((𝐴 ++ 𝐵) ++ 𝐶) ∈ Word 𝑋) | 
| 8 | 5, 6, 7 | syl2anc 584 | . . . 4
⊢ (𝜑 → ((𝐴 ++ 𝐵) ++ 𝐶) ∈ Word 𝑋) | 
| 9 | 1, 8 | eqeltrd 2840 | . . 3
⊢ (𝜑 → 𝑆 ∈ Word 𝑋) | 
| 10 |  | splval2.f | . . . 4
⊢ (𝜑 → 𝐹 = (♯‘𝐴)) | 
| 11 |  | lencl 14572 | . . . . 5
⊢ (𝐴 ∈ Word 𝑋 → (♯‘𝐴) ∈
ℕ0) | 
| 12 | 2, 11 | syl 17 | . . . 4
⊢ (𝜑 → (♯‘𝐴) ∈
ℕ0) | 
| 13 | 10, 12 | eqeltrd 2840 | . . 3
⊢ (𝜑 → 𝐹 ∈
ℕ0) | 
| 14 |  | splval2.t | . . . 4
⊢ (𝜑 → 𝑇 = (𝐹 + (♯‘𝐵))) | 
| 15 |  | lencl 14572 | . . . . . 6
⊢ (𝐵 ∈ Word 𝑋 → (♯‘𝐵) ∈
ℕ0) | 
| 16 | 3, 15 | syl 17 | . . . . 5
⊢ (𝜑 → (♯‘𝐵) ∈
ℕ0) | 
| 17 | 13, 16 | nn0addcld 12593 | . . . 4
⊢ (𝜑 → (𝐹 + (♯‘𝐵)) ∈
ℕ0) | 
| 18 | 14, 17 | eqeltrd 2840 | . . 3
⊢ (𝜑 → 𝑇 ∈
ℕ0) | 
| 19 |  | splval2.r | . . 3
⊢ (𝜑 → 𝑅 ∈ Word 𝑋) | 
| 20 |  | splval 14790 | . . 3
⊢ ((𝑆 ∈ Word 𝑋 ∧ (𝐹 ∈ ℕ0 ∧ 𝑇 ∈ ℕ0
∧ 𝑅 ∈ Word 𝑋)) → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))) | 
| 21 | 9, 13, 18, 19, 20 | syl13anc 1373 | . 2
⊢ (𝜑 → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉))) | 
| 22 |  | nn0uz 12921 | . . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) | 
| 23 | 13, 22 | eleqtrdi 2850 | . . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈
(ℤ≥‘0)) | 
| 24 | 13 | nn0zd 12641 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈ ℤ) | 
| 25 | 24 | uzidd 12895 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (ℤ≥‘𝐹)) | 
| 26 |  | uzaddcl 12947 | . . . . . . . . . . 11
⊢ ((𝐹 ∈
(ℤ≥‘𝐹) ∧ (♯‘𝐵) ∈ ℕ0) → (𝐹 + (♯‘𝐵)) ∈
(ℤ≥‘𝐹)) | 
| 27 | 25, 16, 26 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (𝐹 + (♯‘𝐵)) ∈
(ℤ≥‘𝐹)) | 
| 28 | 14, 27 | eqeltrd 2840 | . . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ (ℤ≥‘𝐹)) | 
| 29 |  | elfzuzb 13559 | . . . . . . . . 9
⊢ (𝐹 ∈ (0...𝑇) ↔ (𝐹 ∈ (ℤ≥‘0)
∧ 𝑇 ∈
(ℤ≥‘𝐹))) | 
| 30 | 23, 28, 29 | sylanbrc 583 | . . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (0...𝑇)) | 
| 31 | 18, 22 | eleqtrdi 2850 | . . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈
(ℤ≥‘0)) | 
| 32 |  | ccatlen 14614 | . . . . . . . . . . . 12
⊢ (((𝐴 ++ 𝐵) ∈ Word 𝑋 ∧ 𝐶 ∈ Word 𝑋) → (♯‘((𝐴 ++ 𝐵) ++ 𝐶)) = ((♯‘(𝐴 ++ 𝐵)) + (♯‘𝐶))) | 
| 33 | 5, 6, 32 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (♯‘((𝐴 ++ 𝐵) ++ 𝐶)) = ((♯‘(𝐴 ++ 𝐵)) + (♯‘𝐶))) | 
| 34 | 1 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝑆) = (♯‘((𝐴 ++ 𝐵) ++ 𝐶))) | 
| 35 | 10 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 + (♯‘𝐵)) = ((♯‘𝐴) + (♯‘𝐵))) | 
| 36 |  | ccatlen 14614 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) → (♯‘(𝐴 ++ 𝐵)) = ((♯‘𝐴) + (♯‘𝐵))) | 
| 37 | 2, 3, 36 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘(𝐴 ++ 𝐵)) = ((♯‘𝐴) + (♯‘𝐵))) | 
| 38 | 35, 14, 37 | 3eqtr4d 2786 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 = (♯‘(𝐴 ++ 𝐵))) | 
| 39 | 38 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑇 + (♯‘𝐶)) = ((♯‘(𝐴 ++ 𝐵)) + (♯‘𝐶))) | 
| 40 | 33, 34, 39 | 3eqtr4d 2786 | . . . . . . . . . 10
⊢ (𝜑 → (♯‘𝑆) = (𝑇 + (♯‘𝐶))) | 
| 41 | 18 | nn0zd 12641 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ ℤ) | 
| 42 | 41 | uzidd 12895 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ (ℤ≥‘𝑇)) | 
| 43 |  | lencl 14572 | . . . . . . . . . . . 12
⊢ (𝐶 ∈ Word 𝑋 → (♯‘𝐶) ∈
ℕ0) | 
| 44 | 6, 43 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝐶) ∈
ℕ0) | 
| 45 |  | uzaddcl 12947 | . . . . . . . . . . 11
⊢ ((𝑇 ∈
(ℤ≥‘𝑇) ∧ (♯‘𝐶) ∈ ℕ0) → (𝑇 + (♯‘𝐶)) ∈
(ℤ≥‘𝑇)) | 
| 46 | 42, 44, 45 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (𝑇 + (♯‘𝐶)) ∈
(ℤ≥‘𝑇)) | 
| 47 | 40, 46 | eqeltrd 2840 | . . . . . . . . 9
⊢ (𝜑 → (♯‘𝑆) ∈
(ℤ≥‘𝑇)) | 
| 48 |  | elfzuzb 13559 | . . . . . . . . 9
⊢ (𝑇 ∈
(0...(♯‘𝑆))
↔ (𝑇 ∈
(ℤ≥‘0) ∧ (♯‘𝑆) ∈ (ℤ≥‘𝑇))) | 
| 49 | 31, 47, 48 | sylanbrc 583 | . . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ (0...(♯‘𝑆))) | 
| 50 |  | ccatpfx 14740 | . . . . . . . 8
⊢ ((𝑆 ∈ Word 𝑋 ∧ 𝐹 ∈ (0...𝑇) ∧ 𝑇 ∈ (0...(♯‘𝑆))) → ((𝑆 prefix 𝐹) ++ (𝑆 substr 〈𝐹, 𝑇〉)) = (𝑆 prefix 𝑇)) | 
| 51 | 9, 30, 49, 50 | syl3anc 1372 | . . . . . . 7
⊢ (𝜑 → ((𝑆 prefix 𝐹) ++ (𝑆 substr 〈𝐹, 𝑇〉)) = (𝑆 prefix 𝑇)) | 
| 52 |  | lencl 14572 | . . . . . . . . . . . . . 14
⊢ (𝑆 ∈ Word 𝑋 → (♯‘𝑆) ∈
ℕ0) | 
| 53 | 9, 52 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘𝑆) ∈
ℕ0) | 
| 54 | 53, 22 | eleqtrdi 2850 | . . . . . . . . . . . 12
⊢ (𝜑 → (♯‘𝑆) ∈
(ℤ≥‘0)) | 
| 55 |  | eluzfz2 13573 | . . . . . . . . . . . 12
⊢
((♯‘𝑆)
∈ (ℤ≥‘0) → (♯‘𝑆) ∈ (0...(♯‘𝑆))) | 
| 56 | 54, 55 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝑆) ∈
(0...(♯‘𝑆))) | 
| 57 |  | ccatpfx 14740 | . . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝑋 ∧ 𝑇 ∈ (0...(♯‘𝑆)) ∧ (♯‘𝑆) ∈
(0...(♯‘𝑆)))
→ ((𝑆 prefix 𝑇) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉)) = (𝑆 prefix (♯‘𝑆))) | 
| 58 | 9, 49, 56, 57 | syl3anc 1372 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑆 prefix 𝑇) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉)) = (𝑆 prefix (♯‘𝑆))) | 
| 59 |  | pfxid 14723 | . . . . . . . . . . 11
⊢ (𝑆 ∈ Word 𝑋 → (𝑆 prefix (♯‘𝑆)) = 𝑆) | 
| 60 | 9, 59 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑆 prefix (♯‘𝑆)) = 𝑆) | 
| 61 | 58, 60, 1 | 3eqtrd 2780 | . . . . . . . . 9
⊢ (𝜑 → ((𝑆 prefix 𝑇) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉)) = ((𝐴 ++ 𝐵) ++ 𝐶)) | 
| 62 |  | pfxcl 14716 | . . . . . . . . . . 11
⊢ (𝑆 ∈ Word 𝑋 → (𝑆 prefix 𝑇) ∈ Word 𝑋) | 
| 63 | 9, 62 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑆 prefix 𝑇) ∈ Word 𝑋) | 
| 64 |  | swrdcl 14684 | . . . . . . . . . . 11
⊢ (𝑆 ∈ Word 𝑋 → (𝑆 substr 〈𝑇, (♯‘𝑆)〉) ∈ Word 𝑋) | 
| 65 | 9, 64 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑆 substr 〈𝑇, (♯‘𝑆)〉) ∈ Word 𝑋) | 
| 66 |  | pfxlen 14722 | . . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝑋 ∧ 𝑇 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 prefix 𝑇)) = 𝑇) | 
| 67 | 9, 49, 66 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (♯‘(𝑆 prefix 𝑇)) = 𝑇) | 
| 68 | 67, 38 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝜑 → (♯‘(𝑆 prefix 𝑇)) = (♯‘(𝐴 ++ 𝐵))) | 
| 69 |  | ccatopth 14755 | . . . . . . . . . 10
⊢ ((((𝑆 prefix 𝑇) ∈ Word 𝑋 ∧ (𝑆 substr 〈𝑇, (♯‘𝑆)〉) ∈ Word 𝑋) ∧ ((𝐴 ++ 𝐵) ∈ Word 𝑋 ∧ 𝐶 ∈ Word 𝑋) ∧ (♯‘(𝑆 prefix 𝑇)) = (♯‘(𝐴 ++ 𝐵))) → (((𝑆 prefix 𝑇) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉)) = ((𝐴 ++ 𝐵) ++ 𝐶) ↔ ((𝑆 prefix 𝑇) = (𝐴 ++ 𝐵) ∧ (𝑆 substr 〈𝑇, (♯‘𝑆)〉) = 𝐶))) | 
| 70 | 63, 65, 5, 6, 68, 69 | syl221anc 1382 | . . . . . . . . 9
⊢ (𝜑 → (((𝑆 prefix 𝑇) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉)) = ((𝐴 ++ 𝐵) ++ 𝐶) ↔ ((𝑆 prefix 𝑇) = (𝐴 ++ 𝐵) ∧ (𝑆 substr 〈𝑇, (♯‘𝑆)〉) = 𝐶))) | 
| 71 | 61, 70 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → ((𝑆 prefix 𝑇) = (𝐴 ++ 𝐵) ∧ (𝑆 substr 〈𝑇, (♯‘𝑆)〉) = 𝐶)) | 
| 72 | 71 | simpld 494 | . . . . . . 7
⊢ (𝜑 → (𝑆 prefix 𝑇) = (𝐴 ++ 𝐵)) | 
| 73 | 51, 72 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → ((𝑆 prefix 𝐹) ++ (𝑆 substr 〈𝐹, 𝑇〉)) = (𝐴 ++ 𝐵)) | 
| 74 |  | pfxcl 14716 | . . . . . . . 8
⊢ (𝑆 ∈ Word 𝑋 → (𝑆 prefix 𝐹) ∈ Word 𝑋) | 
| 75 | 9, 74 | syl 17 | . . . . . . 7
⊢ (𝜑 → (𝑆 prefix 𝐹) ∈ Word 𝑋) | 
| 76 |  | swrdcl 14684 | . . . . . . . 8
⊢ (𝑆 ∈ Word 𝑋 → (𝑆 substr 〈𝐹, 𝑇〉) ∈ Word 𝑋) | 
| 77 | 9, 76 | syl 17 | . . . . . . 7
⊢ (𝜑 → (𝑆 substr 〈𝐹, 𝑇〉) ∈ Word 𝑋) | 
| 78 |  | uztrn 12897 | . . . . . . . . . . 11
⊢
(((♯‘𝑆)
∈ (ℤ≥‘𝑇) ∧ 𝑇 ∈ (ℤ≥‘𝐹)) → (♯‘𝑆) ∈
(ℤ≥‘𝐹)) | 
| 79 | 47, 28, 78 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (♯‘𝑆) ∈
(ℤ≥‘𝐹)) | 
| 80 |  | elfzuzb 13559 | . . . . . . . . . 10
⊢ (𝐹 ∈
(0...(♯‘𝑆))
↔ (𝐹 ∈
(ℤ≥‘0) ∧ (♯‘𝑆) ∈ (ℤ≥‘𝐹))) | 
| 81 | 23, 79, 80 | sylanbrc 583 | . . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (0...(♯‘𝑆))) | 
| 82 |  | pfxlen 14722 | . . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝑋 ∧ 𝐹 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 prefix 𝐹)) = 𝐹) | 
| 83 | 9, 81, 82 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (♯‘(𝑆 prefix 𝐹)) = 𝐹) | 
| 84 | 83, 10 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → (♯‘(𝑆 prefix 𝐹)) = (♯‘𝐴)) | 
| 85 |  | ccatopth 14755 | . . . . . . 7
⊢ ((((𝑆 prefix 𝐹) ∈ Word 𝑋 ∧ (𝑆 substr 〈𝐹, 𝑇〉) ∈ Word 𝑋) ∧ (𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (♯‘(𝑆 prefix 𝐹)) = (♯‘𝐴)) → (((𝑆 prefix 𝐹) ++ (𝑆 substr 〈𝐹, 𝑇〉)) = (𝐴 ++ 𝐵) ↔ ((𝑆 prefix 𝐹) = 𝐴 ∧ (𝑆 substr 〈𝐹, 𝑇〉) = 𝐵))) | 
| 86 | 75, 77, 2, 3, 84, 85 | syl221anc 1382 | . . . . . 6
⊢ (𝜑 → (((𝑆 prefix 𝐹) ++ (𝑆 substr 〈𝐹, 𝑇〉)) = (𝐴 ++ 𝐵) ↔ ((𝑆 prefix 𝐹) = 𝐴 ∧ (𝑆 substr 〈𝐹, 𝑇〉) = 𝐵))) | 
| 87 | 73, 86 | mpbid 232 | . . . . 5
⊢ (𝜑 → ((𝑆 prefix 𝐹) = 𝐴 ∧ (𝑆 substr 〈𝐹, 𝑇〉) = 𝐵)) | 
| 88 | 87 | simpld 494 | . . . 4
⊢ (𝜑 → (𝑆 prefix 𝐹) = 𝐴) | 
| 89 | 88 | oveq1d 7447 | . . 3
⊢ (𝜑 → ((𝑆 prefix 𝐹) ++ 𝑅) = (𝐴 ++ 𝑅)) | 
| 90 | 71 | simprd 495 | . . 3
⊢ (𝜑 → (𝑆 substr 〈𝑇, (♯‘𝑆)〉) = 𝐶) | 
| 91 | 89, 90 | oveq12d 7450 | . 2
⊢ (𝜑 → (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr 〈𝑇, (♯‘𝑆)〉)) = ((𝐴 ++ 𝑅) ++ 𝐶)) | 
| 92 | 21, 91 | eqtrd 2776 | 1
⊢ (𝜑 → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = ((𝐴 ++ 𝑅) ++ 𝐶)) |