| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | efgredlemd.c | . . . . . 6
⊢ (𝜑 → 𝐶 ∈ dom 𝑆) | 
| 2 |  | efgval.w | . . . . . . . . 9
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2o)) | 
| 3 |  | efgval.r | . . . . . . . . 9
⊢  ∼ = (
~FG ‘𝐼) | 
| 4 |  | efgval2.m | . . . . . . . . 9
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) | 
| 5 |  | efgval2.t | . . . . . . . . 9
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) | 
| 6 |  | efgred.d | . . . . . . . . 9
⊢ 𝐷 = (𝑊 ∖ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) | 
| 7 |  | efgred.s | . . . . . . . . 9
⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈
(1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1))) | 
| 8 | 2, 3, 4, 5, 6, 7 | efgsf 19748 | . . . . . . . 8
⊢ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈
(1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊 | 
| 9 | 8 | fdmi 6746 | . . . . . . . . 9
⊢ dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈
(1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} | 
| 10 | 9 | feq2i 6727 | . . . . . . . 8
⊢ (𝑆:dom 𝑆⟶𝑊 ↔ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈
(1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊) | 
| 11 | 8, 10 | mpbir 231 | . . . . . . 7
⊢ 𝑆:dom 𝑆⟶𝑊 | 
| 12 | 11 | ffvelcdmi 7102 | . . . . . 6
⊢ (𝐶 ∈ dom 𝑆 → (𝑆‘𝐶) ∈ 𝑊) | 
| 13 | 1, 12 | syl 17 | . . . . 5
⊢ (𝜑 → (𝑆‘𝐶) ∈ 𝑊) | 
| 14 |  | efgredlemb.q | . . . . . . 7
⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐵‘𝐿)))) | 
| 15 |  | elfzuz 13561 | . . . . . . 7
⊢ (𝑄 ∈
(0...(♯‘(𝐵‘𝐿))) → 𝑄 ∈
(ℤ≥‘0)) | 
| 16 | 14, 15 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑄 ∈
(ℤ≥‘0)) | 
| 17 |  | efgredlemd.sc | . . . . . . . . . 10
⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) | 
| 18 | 17 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝜑 → (♯‘(𝑆‘𝐶)) = (♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)))) | 
| 19 |  | fviss 6985 | . . . . . . . . . . . . 13
⊢ ( I
‘Word (𝐼 ×
2o)) ⊆ Word (𝐼 × 2o) | 
| 20 | 2, 19 | eqsstri 4029 | . . . . . . . . . . . 12
⊢ 𝑊 ⊆ Word (𝐼 × 2o) | 
| 21 |  | efgredlem.1 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) | 
| 22 |  | efgredlem.2 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ dom 𝑆) | 
| 23 |  | efgredlem.3 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ dom 𝑆) | 
| 24 |  | efgredlem.4 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵)) | 
| 25 |  | efgredlem.5 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0)) | 
| 26 |  | efgredlemb.k | . . . . . . . . . . . . . 14
⊢ 𝐾 = (((♯‘𝐴) − 1) −
1) | 
| 27 |  | efgredlemb.l | . . . . . . . . . . . . . 14
⊢ 𝐿 = (((♯‘𝐵) − 1) −
1) | 
| 28 | 2, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27 | efgredlemf 19760 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴‘𝐾) ∈ 𝑊 ∧ (𝐵‘𝐿) ∈ 𝑊)) | 
| 29 | 28 | simprd 495 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐵‘𝐿) ∈ 𝑊) | 
| 30 | 20, 29 | sselid 3980 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐵‘𝐿) ∈ Word (𝐼 × 2o)) | 
| 31 |  | pfxcl 14716 | . . . . . . . . . . 11
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o)) | 
| 32 | 30, 31 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o)) | 
| 33 | 28 | simpld 494 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴‘𝐾) ∈ 𝑊) | 
| 34 | 20, 33 | sselid 3980 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴‘𝐾) ∈ Word (𝐼 × 2o)) | 
| 35 |  | swrdcl 14684 | . . . . . . . . . . 11
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2o)) | 
| 36 | 34, 35 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2o)) | 
| 37 |  | ccatlen 14614 | . . . . . . . . . 10
⊢ ((((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2o)) →
(♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) = ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)))) | 
| 38 | 32, 36, 37 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) = ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)))) | 
| 39 |  | pfxlen 14722 | . . . . . . . . . . . 12
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈
(0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) prefix 𝑄)) = 𝑄) | 
| 40 | 30, 14, 39 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (♯‘((𝐵‘𝐿) prefix 𝑄)) = 𝑄) | 
| 41 |  | 2nn0 12545 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ0 | 
| 42 |  | uzaddcl 12947 | . . . . . . . . . . . . . 14
⊢ ((𝑄 ∈
(ℤ≥‘0) ∧ 2 ∈ ℕ0) →
(𝑄 + 2) ∈
(ℤ≥‘0)) | 
| 43 | 16, 41, 42 | sylancl 586 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄 + 2) ∈
(ℤ≥‘0)) | 
| 44 |  | efgredlemb.p | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐴‘𝐾)))) | 
| 45 |  | elfzuz3 13562 | . . . . . . . . . . . . . . 15
⊢ (𝑃 ∈
(0...(♯‘(𝐴‘𝐾))) → (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑃)) | 
| 46 | 44, 45 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑃)) | 
| 47 |  | efgredlemd.9 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) | 
| 48 |  | uztrn 12897 | . . . . . . . . . . . . . 14
⊢
(((♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑃) ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) →
(♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘(𝑄 + 2))) | 
| 49 | 46, 47, 48 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘(𝑄 + 2))) | 
| 50 |  | elfzuzb 13559 | . . . . . . . . . . . . 13
⊢ ((𝑄 + 2) ∈
(0...(♯‘(𝐴‘𝐾))) ↔ ((𝑄 + 2) ∈
(ℤ≥‘0) ∧ (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘(𝑄 + 2)))) | 
| 51 | 43, 49, 50 | sylanbrc 583 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾)))) | 
| 52 |  | lencl 14572 | . . . . . . . . . . . . . . 15
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) →
(♯‘(𝐴‘𝐾)) ∈
ℕ0) | 
| 53 | 34, 52 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈
ℕ0) | 
| 54 |  | nn0uz 12921 | . . . . . . . . . . . . . 14
⊢
ℕ0 = (ℤ≥‘0) | 
| 55 | 53, 54 | eleqtrdi 2850 | . . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘0)) | 
| 56 |  | eluzfz2 13573 | . . . . . . . . . . . . 13
⊢
((♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘0)
→ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾)))) | 
| 57 | 55, 56 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾)))) | 
| 58 |  | swrdlen 14686 | . . . . . . . . . . . 12
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈
(0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = ((♯‘(𝐴‘𝐾)) − (𝑄 + 2))) | 
| 59 | 34, 51, 57, 58 | syl3anc 1372 | . . . . . . . . . . 11
⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = ((♯‘(𝐴‘𝐾)) − (𝑄 + 2))) | 
| 60 | 40, 59 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝜑 → ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) = (𝑄 + ((♯‘(𝐴‘𝐾)) − (𝑄 + 2)))) | 
| 61 | 14 | elfzelzd 13566 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∈ ℤ) | 
| 62 | 61 | zcnd 12725 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ ℂ) | 
| 63 | 53 | nn0cnd 12591 | . . . . . . . . . . 11
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ ℂ) | 
| 64 |  | 2z 12651 | . . . . . . . . . . . . 13
⊢ 2 ∈
ℤ | 
| 65 |  | zaddcl 12659 | . . . . . . . . . . . . 13
⊢ ((𝑄 ∈ ℤ ∧ 2 ∈
ℤ) → (𝑄 + 2)
∈ ℤ) | 
| 66 | 61, 64, 65 | sylancl 586 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 + 2) ∈ ℤ) | 
| 67 | 66 | zcnd 12725 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑄 + 2) ∈ ℂ) | 
| 68 | 62, 63, 67 | addsubassd 11641 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑄 + (♯‘(𝐴‘𝐾))) − (𝑄 + 2)) = (𝑄 + ((♯‘(𝐴‘𝐾)) − (𝑄 + 2)))) | 
| 69 |  | 2cn 12342 | . . . . . . . . . . . 12
⊢ 2 ∈
ℂ | 
| 70 | 69 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℂ) | 
| 71 | 62, 63, 70 | pnpcand 11658 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑄 + (♯‘(𝐴‘𝐾))) − (𝑄 + 2)) = ((♯‘(𝐴‘𝐾)) − 2)) | 
| 72 | 60, 68, 71 | 3eqtr2d 2782 | . . . . . . . . 9
⊢ (𝜑 → ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) = ((♯‘(𝐴‘𝐾)) − 2)) | 
| 73 | 18, 38, 72 | 3eqtrd 2780 | . . . . . . . 8
⊢ (𝜑 → (♯‘(𝑆‘𝐶)) = ((♯‘(𝐴‘𝐾)) − 2)) | 
| 74 | 44 | elfzelzd 13566 | . . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℤ) | 
| 75 |  | zsubcl 12661 | . . . . . . . . . 10
⊢ ((𝑃 ∈ ℤ ∧ 2 ∈
ℤ) → (𝑃 −
2) ∈ ℤ) | 
| 76 | 74, 64, 75 | sylancl 586 | . . . . . . . . 9
⊢ (𝜑 → (𝑃 − 2) ∈ ℤ) | 
| 77 | 64 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℤ) | 
| 78 | 74 | zcnd 12725 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℂ) | 
| 79 |  | npcan 11518 | . . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℂ ∧ 2 ∈
ℂ) → ((𝑃 −
2) + 2) = 𝑃) | 
| 80 | 78, 69, 79 | sylancl 586 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑃 − 2) + 2) = 𝑃) | 
| 81 | 80 | fveq2d 6909 | . . . . . . . . . 10
⊢ (𝜑 →
(ℤ≥‘((𝑃 − 2) + 2)) =
(ℤ≥‘𝑃)) | 
| 82 | 46, 81 | eleqtrrd 2843 | . . . . . . . . 9
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘((𝑃 − 2) + 2))) | 
| 83 |  | eluzsub 12909 | . . . . . . . . 9
⊢ (((𝑃 − 2) ∈ ℤ ∧
2 ∈ ℤ ∧ (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘((𝑃 − 2) + 2))) →
((♯‘(𝐴‘𝐾)) − 2) ∈
(ℤ≥‘(𝑃 − 2))) | 
| 84 | 76, 77, 82, 83 | syl3anc 1372 | . . . . . . . 8
⊢ (𝜑 → ((♯‘(𝐴‘𝐾)) − 2) ∈
(ℤ≥‘(𝑃 − 2))) | 
| 85 | 73, 84 | eqeltrd 2840 | . . . . . . 7
⊢ (𝜑 → (♯‘(𝑆‘𝐶)) ∈
(ℤ≥‘(𝑃 − 2))) | 
| 86 |  | eluzsub 12909 | . . . . . . . 8
⊢ ((𝑄 ∈ ℤ ∧ 2 ∈
ℤ ∧ 𝑃 ∈
(ℤ≥‘(𝑄 + 2))) → (𝑃 − 2) ∈
(ℤ≥‘𝑄)) | 
| 87 | 61, 77, 47, 86 | syl3anc 1372 | . . . . . . 7
⊢ (𝜑 → (𝑃 − 2) ∈
(ℤ≥‘𝑄)) | 
| 88 |  | uztrn 12897 | . . . . . . 7
⊢
(((♯‘(𝑆‘𝐶)) ∈
(ℤ≥‘(𝑃 − 2)) ∧ (𝑃 − 2) ∈
(ℤ≥‘𝑄)) → (♯‘(𝑆‘𝐶)) ∈
(ℤ≥‘𝑄)) | 
| 89 | 85, 87, 88 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (♯‘(𝑆‘𝐶)) ∈
(ℤ≥‘𝑄)) | 
| 90 |  | elfzuzb 13559 | . . . . . 6
⊢ (𝑄 ∈
(0...(♯‘(𝑆‘𝐶))) ↔ (𝑄 ∈ (ℤ≥‘0)
∧ (♯‘(𝑆‘𝐶)) ∈
(ℤ≥‘𝑄))) | 
| 91 | 16, 89, 90 | sylanbrc 583 | . . . . 5
⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝑆‘𝐶)))) | 
| 92 |  | efgredlemb.v | . . . . 5
⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2o)) | 
| 93 | 2, 3, 4, 5 | efgtval 19742 | . . . . 5
⊢ (((𝑆‘𝐶) ∈ 𝑊 ∧ 𝑄 ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = ((𝑆‘𝐶) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉)) | 
| 94 | 13, 91, 92, 93 | syl3anc 1372 | . . . 4
⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = ((𝑆‘𝐶) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉)) | 
| 95 |  | pfxcl 14716 | . . . . . 6
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o)) | 
| 96 | 34, 95 | syl 17 | . . . . 5
⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o)) | 
| 97 |  | wrd0 14578 | . . . . . 6
⊢ ∅
∈ Word (𝐼 ×
2o) | 
| 98 | 97 | a1i 11 | . . . . 5
⊢ (𝜑 → ∅ ∈ Word (𝐼 ×
2o)) | 
| 99 | 4 | efgmf 19732 | . . . . . . . 8
⊢ 𝑀:(𝐼 × 2o)⟶(𝐼 ×
2o) | 
| 100 | 99 | ffvelcdmi 7102 | . . . . . . 7
⊢ (𝑉 ∈ (𝐼 × 2o) → (𝑀‘𝑉) ∈ (𝐼 × 2o)) | 
| 101 | 92, 100 | syl 17 | . . . . . 6
⊢ (𝜑 → (𝑀‘𝑉) ∈ (𝐼 × 2o)) | 
| 102 | 92, 101 | s2cld 14911 | . . . . 5
⊢ (𝜑 → 〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 ×
2o)) | 
| 103 | 61 | zred 12724 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑄 ∈ ℝ) | 
| 104 |  | nn0addge1 12574 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑄 ∈ ℝ ∧ 2 ∈
ℕ0) → 𝑄 ≤ (𝑄 + 2)) | 
| 105 | 103, 41, 104 | sylancl 586 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑄 ≤ (𝑄 + 2)) | 
| 106 |  | eluz2 12885 | . . . . . . . . . . . . . . . 16
⊢ ((𝑄 + 2) ∈
(ℤ≥‘𝑄) ↔ (𝑄 ∈ ℤ ∧ (𝑄 + 2) ∈ ℤ ∧ 𝑄 ≤ (𝑄 + 2))) | 
| 107 | 61, 66, 105, 106 | syl3anbrc 1343 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑄 + 2) ∈
(ℤ≥‘𝑄)) | 
| 108 |  | uztrn 12897 | . . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈
(ℤ≥‘(𝑄 + 2)) ∧ (𝑄 + 2) ∈
(ℤ≥‘𝑄)) → 𝑃 ∈ (ℤ≥‘𝑄)) | 
| 109 | 47, 107, 108 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘𝑄)) | 
| 110 |  | elfzuzb 13559 | . . . . . . . . . . . . . 14
⊢ (𝑄 ∈ (0...𝑃) ↔ (𝑄 ∈ (ℤ≥‘0)
∧ 𝑃 ∈
(ℤ≥‘𝑄))) | 
| 111 | 16, 109, 110 | sylanbrc 583 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∈ (0...𝑃)) | 
| 112 |  | ccatpfx 14740 | . . . . . . . . . . . . 13
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) = ((𝐴‘𝐾) prefix 𝑃)) | 
| 113 | 34, 111, 44, 112 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) = ((𝐴‘𝐾) prefix 𝑃)) | 
| 114 | 113 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (((𝐴‘𝐾) prefix 𝑃) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)))) | 
| 115 |  | pfxcl 14716 | . . . . . . . . . . . . 13
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o)) | 
| 116 | 34, 115 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o)) | 
| 117 |  | efgredlemb.u | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2o)) | 
| 118 | 99 | ffvelcdmi 7102 | . . . . . . . . . . . . . 14
⊢ (𝑈 ∈ (𝐼 × 2o) → (𝑀‘𝑈) ∈ (𝐼 × 2o)) | 
| 119 | 117, 118 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀‘𝑈) ∈ (𝐼 × 2o)) | 
| 120 | 117, 119 | s2cld 14911 | . . . . . . . . . . . 12
⊢ (𝜑 → 〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 ×
2o)) | 
| 121 |  | swrdcl 14684 | . . . . . . . . . . . . 13
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2o)) | 
| 122 | 34, 121 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2o)) | 
| 123 |  | ccatass 14627 | . . . . . . . . . . . 12
⊢ ((((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o) ∧
〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 × 2o) ∧
((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2o)) → ((((𝐴‘𝐾) prefix 𝑃) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = (((𝐴‘𝐾) prefix 𝑃) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)))) | 
| 124 | 116, 120,
122, 123 | syl3anc 1372 | . . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑃) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = (((𝐴‘𝐾) prefix 𝑃) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)))) | 
| 125 |  | efgredlemb.6 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈)) | 
| 126 | 2, 3, 4, 5 | efgtval 19742 | . . . . . . . . . . . . . 14
⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ 𝑈 ∈ (𝐼 × 2o)) → (𝑃(𝑇‘(𝐴‘𝐾))𝑈) = ((𝐴‘𝐾) splice 〈𝑃, 𝑃, 〈“𝑈(𝑀‘𝑈)”〉〉)) | 
| 127 | 33, 44, 117, 126 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃(𝑇‘(𝐴‘𝐾))𝑈) = ((𝐴‘𝐾) splice 〈𝑃, 𝑃, 〈“𝑈(𝑀‘𝑈)”〉〉)) | 
| 128 |  | splval 14790 | . . . . . . . . . . . . . 14
⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ (𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ 〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 × 2o))) →
((𝐴‘𝐾) splice 〈𝑃, 𝑃, 〈“𝑈(𝑀‘𝑈)”〉〉) = ((((𝐴‘𝐾) prefix 𝑃) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) | 
| 129 | 33, 44, 44, 120, 128 | syl13anc 1373 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴‘𝐾) splice 〈𝑃, 𝑃, 〈“𝑈(𝑀‘𝑈)”〉〉) = ((((𝐴‘𝐾) prefix 𝑃) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) | 
| 130 | 125, 127,
129 | 3eqtrd 2780 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑆‘𝐴) = ((((𝐴‘𝐾) prefix 𝑃) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) | 
| 131 |  | efgredlemb.7 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉)) | 
| 132 | 2, 3, 4, 5 | efgtval 19742 | . . . . . . . . . . . . . 14
⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝐵‘𝐿))𝑉) = ((𝐵‘𝐿) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉)) | 
| 133 | 29, 14, 92, 132 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄(𝑇‘(𝐵‘𝐿))𝑉) = ((𝐵‘𝐿) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉)) | 
| 134 |  | splval 14790 | . . . . . . . . . . . . . 14
⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ (𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ 〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 × 2o))) →
((𝐵‘𝐿) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉) = ((((𝐵‘𝐿) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))) | 
| 135 | 29, 14, 14, 102, 134 | syl13anc 1373 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵‘𝐿) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉) = ((((𝐵‘𝐿) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))) | 
| 136 | 131, 133,
135 | 3eqtrd 2780 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑆‘𝐵) = ((((𝐵‘𝐿) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))) | 
| 137 | 24, 130, 136 | 3eqtr3d 2784 | . . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑃) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = ((((𝐵‘𝐿) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))) | 
| 138 | 114, 124,
137 | 3eqtr2d 2782 | . . . . . . . . . 10
⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = ((((𝐵‘𝐿) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))) | 
| 139 |  | swrdcl 14684 | . . . . . . . . . . . 12
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ∈ Word (𝐼 × 2o)) | 
| 140 | 34, 139 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ∈ Word (𝐼 × 2o)) | 
| 141 |  | ccatcl 14613 | . . . . . . . . . . . 12
⊢
((〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 × 2o) ∧
((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2o)) →
(〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 × 2o)) | 
| 142 | 120, 122,
141 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 × 2o)) | 
| 143 |  | ccatass 14627 | . . . . . . . . . . 11
⊢ ((((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ∈ Word (𝐼 × 2o) ∧
(〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 × 2o)) → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))))) | 
| 144 | 96, 140, 142, 143 | syl3anc 1372 | . . . . . . . . . 10
⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))))) | 
| 145 |  | swrdcl 14684 | . . . . . . . . . . . 12
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) | 
| 146 | 30, 145 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) | 
| 147 |  | ccatass 14627 | . . . . . . . . . . 11
⊢ ((((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧
〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 × 2o) ∧
((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) → ((((𝐵‘𝐿) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) prefix 𝑄) ++ (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)))) | 
| 148 | 32, 102, 146, 147 | syl3anc 1372 | . . . . . . . . . 10
⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) prefix 𝑄) ++ (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)))) | 
| 149 | 138, 144,
148 | 3eqtr3d 2784 | . . . . . . . . 9
⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)))) = (((𝐵‘𝐿) prefix 𝑄) ++ (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)))) | 
| 150 |  | ccatcl 14613 | . . . . . . . . . . 11
⊢ ((((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ∈ Word (𝐼 × 2o) ∧
(〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 × 2o)) → (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) ∈ Word (𝐼 × 2o)) | 
| 151 | 140, 142,
150 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) ∈ Word (𝐼 × 2o)) | 
| 152 |  | ccatcl 14613 | . . . . . . . . . . 11
⊢
((〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 × 2o) ∧
((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) →
(〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)) ∈ Word (𝐼 × 2o)) | 
| 153 | 102, 146,
152 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)) ∈ Word (𝐼 × 2o)) | 
| 154 |  | uztrn 12897 | . . . . . . . . . . . . . 14
⊢
(((♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑃) ∧ 𝑃 ∈ (ℤ≥‘𝑄)) → (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑄)) | 
| 155 | 46, 109, 154 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑄)) | 
| 156 |  | elfzuzb 13559 | . . . . . . . . . . . . 13
⊢ (𝑄 ∈
(0...(♯‘(𝐴‘𝐾))) ↔ (𝑄 ∈ (ℤ≥‘0)
∧ (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑄))) | 
| 157 | 16, 155, 156 | sylanbrc 583 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐴‘𝐾)))) | 
| 158 |  | pfxlen 14722 | . . . . . . . . . . . 12
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈
(0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) prefix 𝑄)) = 𝑄) | 
| 159 | 34, 157, 158 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (♯‘((𝐴‘𝐾) prefix 𝑄)) = 𝑄) | 
| 160 | 159, 40 | eqtr4d 2779 | . . . . . . . . . 10
⊢ (𝜑 → (♯‘((𝐴‘𝐾) prefix 𝑄)) = (♯‘((𝐵‘𝐿) prefix 𝑄))) | 
| 161 |  | ccatopth 14755 | . . . . . . . . . 10
⊢
(((((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) ∈ Word (𝐼 × 2o)) ∧ (((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧
(〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)) ∈ Word (𝐼 × 2o)) ∧
(♯‘((𝐴‘𝐾) prefix 𝑄)) = (♯‘((𝐵‘𝐿) prefix 𝑄))) → ((((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)))) = (((𝐵‘𝐿) prefix 𝑄) ++ (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))) ↔ (((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄) ∧ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))))) | 
| 162 | 96, 151, 32, 153, 160, 161 | syl221anc 1382 | . . . . . . . . 9
⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)))) = (((𝐵‘𝐿) prefix 𝑄) ++ (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))) ↔ (((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄) ∧ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))))) | 
| 163 | 149, 162 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄) ∧ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)))) | 
| 164 | 163 | simpld 494 | . . . . . . 7
⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄)) | 
| 165 | 164 | oveq1d 7447 | . . . . . 6
⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) | 
| 166 |  | ccatrid 14626 | . . . . . . . 8
⊢ (((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o) → (((𝐴‘𝐾) prefix 𝑄) ++ ∅) = ((𝐴‘𝐾) prefix 𝑄)) | 
| 167 | 96, 166 | syl 17 | . . . . . . 7
⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ∅) = ((𝐴‘𝐾) prefix 𝑄)) | 
| 168 | 167 | oveq1d 7447 | . . . . . 6
⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ∅) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) | 
| 169 | 165, 168,
17 | 3eqtr4rd 2787 | . . . . 5
⊢ (𝜑 → (𝑆‘𝐶) = ((((𝐴‘𝐾) prefix 𝑄) ++ ∅) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) | 
| 170 | 159 | eqcomd 2742 | . . . . 5
⊢ (𝜑 → 𝑄 = (♯‘((𝐴‘𝐾) prefix 𝑄))) | 
| 171 |  | hash0 14407 | . . . . . . 7
⊢
(♯‘∅) = 0 | 
| 172 | 171 | oveq2i 7443 | . . . . . 6
⊢ (𝑄 + (♯‘∅)) =
(𝑄 + 0) | 
| 173 | 62 | addridd 11462 | . . . . . 6
⊢ (𝜑 → (𝑄 + 0) = 𝑄) | 
| 174 | 172, 173 | eqtr2id 2789 | . . . . 5
⊢ (𝜑 → 𝑄 = (𝑄 +
(♯‘∅))) | 
| 175 | 96, 98, 36, 102, 169, 170, 174 | splval2 14796 | . . . 4
⊢ (𝜑 → ((𝑆‘𝐶) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉) = ((((𝐴‘𝐾) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) | 
| 176 |  | elfzuzb 13559 | . . . . . . . . . . . . . 14
⊢ (𝑄 ∈ (0...(𝑄 + 2)) ↔ (𝑄 ∈ (ℤ≥‘0)
∧ (𝑄 + 2) ∈
(ℤ≥‘𝑄))) | 
| 177 | 16, 107, 176 | sylanbrc 583 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∈ (0...(𝑄 + 2))) | 
| 178 |  | elfzuzb 13559 | . . . . . . . . . . . . . 14
⊢ ((𝑄 + 2) ∈ (0...𝑃) ↔ ((𝑄 + 2) ∈
(ℤ≥‘0) ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2)))) | 
| 179 | 43, 47, 178 | sylanbrc 583 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄 + 2) ∈ (0...𝑃)) | 
| 180 |  | ccatswrd 14707 | . . . . . . . . . . . . 13
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) = ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) | 
| 181 | 34, 177, 179, 44, 180 | syl13anc 1373 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) = ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) | 
| 182 | 181 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)))) | 
| 183 |  | swrdcl 14684 | . . . . . . . . . . . . 13
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ∈ Word (𝐼 × 2o)) | 
| 184 | 34, 183 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ∈ Word (𝐼 × 2o)) | 
| 185 |  | swrdcl 14684 | . . . . . . . . . . . . 13
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ∈ Word (𝐼 × 2o)) | 
| 186 | 34, 185 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ∈ Word (𝐼 × 2o)) | 
| 187 |  | ccatass 14627 | . . . . . . . . . . . 12
⊢ ((((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ∈ Word (𝐼 × 2o) ∧ ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ∈ Word (𝐼 × 2o) ∧
(〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 × 2o)) → ((((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))))) | 
| 188 | 184, 186,
142, 187 | syl3anc 1372 | . . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))))) | 
| 189 | 163 | simprd 495 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))) | 
| 190 | 182, 188,
189 | 3eqtr3d 2784 | . . . . . . . . . 10
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)))) = (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))) | 
| 191 |  | ccatcl 14613 | . . . . . . . . . . . 12
⊢ ((((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ∈ Word (𝐼 × 2o) ∧
(〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 × 2o)) → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) ∈ Word (𝐼 × 2o)) | 
| 192 | 186, 142,
191 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) ∈ Word (𝐼 × 2o)) | 
| 193 |  | swrdlen 14686 | . . . . . . . . . . . . . 14
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = ((𝑄 + 2) − 𝑄)) | 
| 194 | 34, 177, 51, 193 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = ((𝑄 + 2) − 𝑄)) | 
| 195 |  | pncan2 11516 | . . . . . . . . . . . . . 14
⊢ ((𝑄 ∈ ℂ ∧ 2 ∈
ℂ) → ((𝑄 + 2)
− 𝑄) =
2) | 
| 196 | 62, 69, 195 | sylancl 586 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄 + 2) − 𝑄) = 2) | 
| 197 | 194, 196 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = 2) | 
| 198 |  | s2len 14929 | . . . . . . . . . . . 12
⊢
(♯‘〈“𝑉(𝑀‘𝑉)”〉) = 2 | 
| 199 | 197, 198 | eqtr4di 2794 | . . . . . . . . . . 11
⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) =
(♯‘〈“𝑉(𝑀‘𝑉)”〉)) | 
| 200 |  | ccatopth 14755 | . . . . . . . . . . 11
⊢
(((((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ∈ Word (𝐼 × 2o) ∧ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) ∈ Word (𝐼 × 2o)) ∧
(〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 × 2o) ∧
((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) ∧
(♯‘((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) =
(♯‘〈“𝑉(𝑀‘𝑉)”〉)) → ((((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)))) = (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)) ↔ (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) = 〈“𝑉(𝑀‘𝑉)”〉 ∧ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)))) | 
| 201 | 184, 192,
102, 146, 199, 200 | syl221anc 1382 | . . . . . . . . . 10
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)))) = (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)) ↔ (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) = 〈“𝑉(𝑀‘𝑉)”〉 ∧ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)))) | 
| 202 | 190, 201 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) = 〈“𝑉(𝑀‘𝑉)”〉 ∧ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))) | 
| 203 | 202 | simpld 494 | . . . . . . . 8
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) = 〈“𝑉(𝑀‘𝑉)”〉) | 
| 204 | 203 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = (((𝐴‘𝐾) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉)) | 
| 205 |  | ccatpfx 14740 | . . . . . . . 8
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = ((𝐴‘𝐾) prefix (𝑄 + 2))) | 
| 206 | 34, 177, 51, 205 | syl3anc 1372 | . . . . . . 7
⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = ((𝐴‘𝐾) prefix (𝑄 + 2))) | 
| 207 | 204, 206 | eqtr3d 2778 | . . . . . 6
⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) = ((𝐴‘𝐾) prefix (𝑄 + 2))) | 
| 208 | 207 | oveq1d 7447 | . . . . 5
⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) | 
| 209 |  | ccatpfx 14740 | . . . . . 6
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈
(0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾)))) | 
| 210 | 34, 51, 57, 209 | syl3anc 1372 | . . . . 5
⊢ (𝜑 → (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾)))) | 
| 211 |  | pfxid 14723 | . . . . . 6
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))) = (𝐴‘𝐾)) | 
| 212 | 34, 211 | syl 17 | . . . . 5
⊢ (𝜑 → ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))) = (𝐴‘𝐾)) | 
| 213 | 208, 210,
212 | 3eqtrd 2780 | . . . 4
⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = (𝐴‘𝐾)) | 
| 214 | 94, 175, 213 | 3eqtrd 2780 | . . 3
⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = (𝐴‘𝐾)) | 
| 215 | 2, 3, 4, 5 | efgtf 19741 | . . . . . . 7
⊢ ((𝑆‘𝐶) ∈ 𝑊 → ((𝑇‘(𝑆‘𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆‘𝐶))), 𝑖 ∈ (𝐼 × 2o) ↦ ((𝑆‘𝐶) splice 〈𝑎, 𝑎, 〈“𝑖(𝑀‘𝑖)”〉〉)) ∧ (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o))⟶𝑊)) | 
| 216 | 13, 215 | syl 17 | . . . . . 6
⊢ (𝜑 → ((𝑇‘(𝑆‘𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆‘𝐶))), 𝑖 ∈ (𝐼 × 2o) ↦ ((𝑆‘𝐶) splice 〈𝑎, 𝑎, 〈“𝑖(𝑀‘𝑖)”〉〉)) ∧ (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o))⟶𝑊)) | 
| 217 | 216 | simprd 495 | . . . . 5
⊢ (𝜑 → (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o))⟶𝑊) | 
| 218 | 217 | ffnd 6736 | . . . 4
⊢ (𝜑 → (𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o))) | 
| 219 |  | fnovrn 7609 | . . . 4
⊢ (((𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o)) ∧ 𝑄 ∈
(0...(♯‘(𝑆‘𝐶))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) ∈ ran (𝑇‘(𝑆‘𝐶))) | 
| 220 | 218, 91, 92, 219 | syl3anc 1372 | . . 3
⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) ∈ ran (𝑇‘(𝑆‘𝐶))) | 
| 221 | 214, 220 | eqeltrrd 2841 | . 2
⊢ (𝜑 → (𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶))) | 
| 222 |  | uztrn 12897 | . . . . . . 7
⊢ (((𝑃 − 2) ∈
(ℤ≥‘𝑄) ∧ 𝑄 ∈ (ℤ≥‘0))
→ (𝑃 − 2) ∈
(ℤ≥‘0)) | 
| 223 | 87, 16, 222 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝑃 − 2) ∈
(ℤ≥‘0)) | 
| 224 |  | elfzuzb 13559 | . . . . . 6
⊢ ((𝑃 − 2) ∈
(0...(♯‘(𝑆‘𝐶))) ↔ ((𝑃 − 2) ∈
(ℤ≥‘0) ∧ (♯‘(𝑆‘𝐶)) ∈
(ℤ≥‘(𝑃 − 2)))) | 
| 225 | 223, 85, 224 | sylanbrc 583 | . . . . 5
⊢ (𝜑 → (𝑃 − 2) ∈
(0...(♯‘(𝑆‘𝐶)))) | 
| 226 | 2, 3, 4, 5 | efgtval 19742 | . . . . 5
⊢ (((𝑆‘𝐶) ∈ 𝑊 ∧ (𝑃 − 2) ∈
(0...(♯‘(𝑆‘𝐶))) ∧ 𝑈 ∈ (𝐼 × 2o)) → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = ((𝑆‘𝐶) splice 〈(𝑃 − 2), (𝑃 − 2), 〈“𝑈(𝑀‘𝑈)”〉〉)) | 
| 227 | 13, 225, 117, 226 | syl3anc 1372 | . . . 4
⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = ((𝑆‘𝐶) splice 〈(𝑃 − 2), (𝑃 − 2), 〈“𝑈(𝑀‘𝑈)”〉〉)) | 
| 228 |  | pfxcl 14716 | . . . . . 6
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o)) | 
| 229 | 30, 228 | syl 17 | . . . . 5
⊢ (𝜑 → ((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o)) | 
| 230 |  | swrdcl 14684 | . . . . . 6
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) | 
| 231 | 30, 230 | syl 17 | . . . . 5
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) | 
| 232 |  | ccatswrd 14707 | . . . . . . . . . . 11
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ ((𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) | 
| 233 | 34, 179, 44, 57, 232 | syl13anc 1373 | . . . . . . . . . 10
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) | 
| 234 | 202 | simprd 495 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)) | 
| 235 |  | elfzuzb 13559 | . . . . . . . . . . . . . . . 16
⊢ (𝑄 ∈ (0...(𝑃 − 2)) ↔ (𝑄 ∈ (ℤ≥‘0)
∧ (𝑃 − 2) ∈
(ℤ≥‘𝑄))) | 
| 236 | 16, 87, 235 | sylanbrc 583 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑄 ∈ (0...(𝑃 − 2))) | 
| 237 | 2, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27, 44, 14, 117, 92, 125, 131 | efgredlemg 19761 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) = (♯‘(𝐵‘𝐿))) | 
| 238 | 237, 46 | eqeltrrd 2841 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈
(ℤ≥‘𝑃)) | 
| 239 |  | 0le2 12369 | . . . . . . . . . . . . . . . . . . . 20
⊢ 0 ≤
2 | 
| 240 | 239 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ≤ 2) | 
| 241 | 74 | zred 12724 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑃 ∈ ℝ) | 
| 242 |  | 2re 12341 | . . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ | 
| 243 |  | subge02 11780 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℝ ∧ 2 ∈
ℝ) → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃)) | 
| 244 | 241, 242,
243 | sylancl 586 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃)) | 
| 245 | 240, 244 | mpbid 232 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑃 − 2) ≤ 𝑃) | 
| 246 |  | eluz2 12885 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈
(ℤ≥‘(𝑃 − 2)) ↔ ((𝑃 − 2) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑃 − 2) ≤ 𝑃)) | 
| 247 | 76, 74, 245, 246 | syl3anbrc 1343 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑃 − 2))) | 
| 248 |  | uztrn 12897 | . . . . . . . . . . . . . . . . 17
⊢
(((♯‘(𝐵‘𝐿)) ∈
(ℤ≥‘𝑃) ∧ 𝑃 ∈ (ℤ≥‘(𝑃 − 2))) →
(♯‘(𝐵‘𝐿)) ∈
(ℤ≥‘(𝑃 − 2))) | 
| 249 | 238, 247,
248 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈
(ℤ≥‘(𝑃 − 2))) | 
| 250 |  | elfzuzb 13559 | . . . . . . . . . . . . . . . 16
⊢ ((𝑃 − 2) ∈
(0...(♯‘(𝐵‘𝐿))) ↔ ((𝑃 − 2) ∈
(ℤ≥‘0) ∧ (♯‘(𝐵‘𝐿)) ∈
(ℤ≥‘(𝑃 − 2)))) | 
| 251 | 223, 249,
250 | sylanbrc 583 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑃 − 2) ∈
(0...(♯‘(𝐵‘𝐿)))) | 
| 252 |  | lencl 14572 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) →
(♯‘(𝐵‘𝐿)) ∈
ℕ0) | 
| 253 | 30, 252 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈
ℕ0) | 
| 254 | 253, 54 | eleqtrdi 2850 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈
(ℤ≥‘0)) | 
| 255 |  | eluzfz2 13573 | . . . . . . . . . . . . . . . 16
⊢
((♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘0)
→ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿)))) | 
| 256 | 254, 255 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿)))) | 
| 257 |  | ccatswrd 14707 | . . . . . . . . . . . . . . 15
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈
(0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)) | 
| 258 | 30, 236, 251, 256, 257 | syl13anc 1373 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)) | 
| 259 | 234, 258 | eqtr4d 2779 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉))) | 
| 260 |  | swrdcl 14684 | . . . . . . . . . . . . . . 15
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ∈ Word (𝐼 ×
2o)) | 
| 261 | 30, 260 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ∈ Word (𝐼 ×
2o)) | 
| 262 |  | swrdcl 14684 | . . . . . . . . . . . . . . 15
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) | 
| 263 | 30, 262 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) | 
| 264 |  | swrdlen 14686 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) = (𝑃 − (𝑄 + 2))) | 
| 265 | 34, 179, 44, 264 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) = (𝑃 − (𝑄 + 2))) | 
| 266 |  | swrdlen 14686 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈
(0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) = ((𝑃 − 2) − 𝑄)) | 
| 267 | 30, 236, 251, 266 | syl3anc 1372 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) = ((𝑃 − 2) − 𝑄)) | 
| 268 | 78, 62, 70 | sub32d 11653 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑃 − 𝑄) − 2) = ((𝑃 − 2) − 𝑄)) | 
| 269 | 78, 62, 70 | subsub4d 11652 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑃 − 𝑄) − 2) = (𝑃 − (𝑄 + 2))) | 
| 270 | 267, 268,
269 | 3eqtr2d 2782 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) = (𝑃 − (𝑄 + 2))) | 
| 271 | 265, 270 | eqtr4d 2779 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) = (♯‘((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉))) | 
| 272 |  | ccatopth 14755 | . . . . . . . . . . . . . 14
⊢
(((((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ∈ Word (𝐼 × 2o) ∧
(〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 × 2o)) ∧ (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ∈ Word (𝐼 × 2o) ∧
((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) ∧
(♯‘((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) = (♯‘((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉))) → ((((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉)) ↔ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) = ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ∧ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉)))) | 
| 273 | 186, 142,
261, 263, 271, 272 | syl221anc 1382 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉)) ↔ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) = ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ∧ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉)))) | 
| 274 | 259, 273 | mpbid 232 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) = ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ∧ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉))) | 
| 275 | 274 | simpld 494 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) = ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) | 
| 276 | 274 | simprd 495 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉)) | 
| 277 |  | elfzuzb 13559 | . . . . . . . . . . . . . . . 16
⊢ ((𝑃 − 2) ∈ (0...𝑃) ↔ ((𝑃 − 2) ∈
(ℤ≥‘0) ∧ 𝑃 ∈ (ℤ≥‘(𝑃 − 2)))) | 
| 278 | 223, 247,
277 | sylanbrc 583 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑃 − 2) ∈ (0...𝑃)) | 
| 279 |  | elfzuz 13561 | . . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈
(0...(♯‘(𝐴‘𝐾))) → 𝑃 ∈
(ℤ≥‘0)) | 
| 280 | 44, 279 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈
(ℤ≥‘0)) | 
| 281 |  | elfzuzb 13559 | . . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈
(0...(♯‘(𝐵‘𝐿))) ↔ (𝑃 ∈ (ℤ≥‘0)
∧ (♯‘(𝐵‘𝐿)) ∈
(ℤ≥‘𝑃))) | 
| 282 | 280, 238,
281 | sylanbrc 583 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐵‘𝐿)))) | 
| 283 |  | ccatswrd 14707 | . . . . . . . . . . . . . . 15
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ ((𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉)) | 
| 284 | 30, 278, 282, 256, 283 | syl13anc 1373 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉)) | 
| 285 | 276, 284 | eqtr4d 2779 | . . . . . . . . . . . . 13
⊢ (𝜑 → (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) | 
| 286 |  | swrdcl 14684 | . . . . . . . . . . . . . . 15
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ∈ Word (𝐼 × 2o)) | 
| 287 | 30, 286 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ∈ Word (𝐼 × 2o)) | 
| 288 |  | s2len 14929 | . . . . . . . . . . . . . . 15
⊢
(♯‘〈“𝑈(𝑀‘𝑈)”〉) = 2 | 
| 289 |  | swrdlen 14686 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉)) = (𝑃 − (𝑃 − 2))) | 
| 290 | 30, 278, 282, 289 | syl3anc 1372 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉)) = (𝑃 − (𝑃 − 2))) | 
| 291 |  | nncan 11539 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℂ ∧ 2 ∈
ℂ) → (𝑃 −
(𝑃 − 2)) =
2) | 
| 292 | 78, 69, 291 | sylancl 586 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃 − (𝑃 − 2)) = 2) | 
| 293 | 290, 292 | eqtr2d 2777 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 = (♯‘((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉))) | 
| 294 | 288, 293 | eqtrid 2788 | . . . . . . . . . . . . . 14
⊢ (𝜑 →
(♯‘〈“𝑈(𝑀‘𝑈)”〉) = (♯‘((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉))) | 
| 295 |  | ccatopth 14755 | . . . . . . . . . . . . . 14
⊢
(((〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 × 2o) ∧
((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2o)) ∧ (((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ∈ Word (𝐼 × 2o) ∧ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) ∧
(♯‘〈“𝑈(𝑀‘𝑈)”〉) = (♯‘((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉))) → ((〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) ↔ (〈“𝑈(𝑀‘𝑈)”〉 = ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ∧ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉) = ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)))) | 
| 296 | 120, 122,
287, 231, 294, 295 | syl221anc 1382 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) ↔ (〈“𝑈(𝑀‘𝑈)”〉 = ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ∧ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉) = ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)))) | 
| 297 | 285, 296 | mpbid 232 | . . . . . . . . . . . 12
⊢ (𝜑 → (〈“𝑈(𝑀‘𝑈)”〉 = ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ∧ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉) = ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) | 
| 298 | 297 | simprd 495 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉) = ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) | 
| 299 | 275, 298 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) | 
| 300 | 233, 299 | eqtr3d 2778 | . . . . . . . . 9
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉) = (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) | 
| 301 | 300 | oveq2d 7448 | . . . . . . . 8
⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) prefix 𝑄) ++ (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)))) | 
| 302 |  | ccatass 14627 | . . . . . . . . 9
⊢ ((((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ∈ Word (𝐼 × 2o) ∧
((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) → ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) prefix 𝑄) ++ (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)))) | 
| 303 | 32, 261, 231, 302 | syl3anc 1372 | . . . . . . . 8
⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) prefix 𝑄) ++ (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)))) | 
| 304 | 301, 303 | eqtr4d 2779 | . . . . . . 7
⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) | 
| 305 |  | ccatpfx 14740 | . . . . . . . . 9
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈
(0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) = ((𝐵‘𝐿) prefix (𝑃 − 2))) | 
| 306 | 30, 236, 251, 305 | syl3anc 1372 | . . . . . . . 8
⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) = ((𝐵‘𝐿) prefix (𝑃 − 2))) | 
| 307 | 306 | oveq1d 7447 | . . . . . . 7
⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) | 
| 308 | 17, 304, 307 | 3eqtrd 2780 | . . . . . 6
⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) | 
| 309 |  | ccatrid 14626 | . . . . . . . 8
⊢ (((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o) → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) = ((𝐵‘𝐿) prefix (𝑃 − 2))) | 
| 310 | 229, 309 | syl 17 | . . . . . . 7
⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) = ((𝐵‘𝐿) prefix (𝑃 − 2))) | 
| 311 | 310 | oveq1d 7447 | . . . . . 6
⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) | 
| 312 | 308, 311 | eqtr4d 2779 | . . . . 5
⊢ (𝜑 → (𝑆‘𝐶) = ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) | 
| 313 |  | pfxlen 14722 | . . . . . . 7
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈
(0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) prefix (𝑃 − 2))) = (𝑃 − 2)) | 
| 314 | 30, 251, 313 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (♯‘((𝐵‘𝐿) prefix (𝑃 − 2))) = (𝑃 − 2)) | 
| 315 | 314 | eqcomd 2742 | . . . . 5
⊢ (𝜑 → (𝑃 − 2) = (♯‘((𝐵‘𝐿) prefix (𝑃 − 2)))) | 
| 316 | 171 | oveq2i 7443 | . . . . . 6
⊢ ((𝑃 − 2) +
(♯‘∅)) = ((𝑃 − 2) + 0) | 
| 317 | 76 | zcnd 12725 | . . . . . . 7
⊢ (𝜑 → (𝑃 − 2) ∈ ℂ) | 
| 318 | 317 | addridd 11462 | . . . . . 6
⊢ (𝜑 → ((𝑃 − 2) + 0) = (𝑃 − 2)) | 
| 319 | 316, 318 | eqtr2id 2789 | . . . . 5
⊢ (𝜑 → (𝑃 − 2) = ((𝑃 − 2) +
(♯‘∅))) | 
| 320 | 229, 98, 231, 120, 312, 315, 319 | splval2 14796 | . . . 4
⊢ (𝜑 → ((𝑆‘𝐶) splice 〈(𝑃 − 2), (𝑃 − 2), 〈“𝑈(𝑀‘𝑈)”〉〉) = ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) | 
| 321 | 297 | simpld 494 | . . . . . . . 8
⊢ (𝜑 → 〈“𝑈(𝑀‘𝑈)”〉 = ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉)) | 
| 322 | 321 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ 〈“𝑈(𝑀‘𝑈)”〉) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉))) | 
| 323 |  | ccatpfx 14740 | . . . . . . . 8
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉)) = ((𝐵‘𝐿) prefix 𝑃)) | 
| 324 | 30, 278, 282, 323 | syl3anc 1372 | . . . . . . 7
⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉)) = ((𝐵‘𝐿) prefix 𝑃)) | 
| 325 | 322, 324 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ 〈“𝑈(𝑀‘𝑈)”〉) = ((𝐵‘𝐿) prefix 𝑃)) | 
| 326 | 325 | oveq1d 7447 | . . . . 5
⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) | 
| 327 |  | ccatpfx 14740 | . . . . . 6
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑃 ∈
(0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿)))) | 
| 328 | 30, 282, 256, 327 | syl3anc 1372 | . . . . 5
⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿)))) | 
| 329 |  | pfxid 14723 | . . . . . 6
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))) = (𝐵‘𝐿)) | 
| 330 | 30, 329 | syl 17 | . . . . 5
⊢ (𝜑 → ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))) = (𝐵‘𝐿)) | 
| 331 | 326, 328,
330 | 3eqtrd 2780 | . . . 4
⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) = (𝐵‘𝐿)) | 
| 332 | 227, 320,
331 | 3eqtrd 2780 | . . 3
⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = (𝐵‘𝐿)) | 
| 333 |  | fnovrn 7609 | . . . 4
⊢ (((𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o)) ∧ (𝑃 − 2) ∈
(0...(♯‘(𝑆‘𝐶))) ∧ 𝑈 ∈ (𝐼 × 2o)) → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) ∈ ran (𝑇‘(𝑆‘𝐶))) | 
| 334 | 218, 225,
117, 333 | syl3anc 1372 | . . 3
⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) ∈ ran (𝑇‘(𝑆‘𝐶))) | 
| 335 | 332, 334 | eqeltrrd 2841 | . 2
⊢ (𝜑 → (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶))) | 
| 336 | 221, 335 | jca 511 | 1
⊢ (𝜑 → ((𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶)) ∧ (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶)))) |