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 19119 |
. . . . . . . 8
⊢ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈
(1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊 |
9 | 8 | fdmi 6557 |
. . . . . . . . 9
⊢ dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈
(1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} |
10 | 9 | feq2i 6537 |
. . . . . . . 8
⊢ (𝑆:dom 𝑆⟶𝑊 ↔ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈
(1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊) |
11 | 8, 10 | mpbir 234 |
. . . . . . 7
⊢ 𝑆:dom 𝑆⟶𝑊 |
12 | 11 | ffvelrni 6903 |
. . . . . 6
⊢ (𝐶 ∈ dom 𝑆 → (𝑆‘𝐶) ∈ 𝑊) |
13 | 1, 12 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑆‘𝐶) ∈ 𝑊) |
14 | | efgredlemb.q |
. . . . . . 7
⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐵‘𝐿)))) |
15 | | elfzuz 13108 |
. . . . . . 7
⊢ (𝑄 ∈
(0...(♯‘(𝐵‘𝐿))) → 𝑄 ∈
(ℤ≥‘0)) |
16 | 14, 15 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈
(ℤ≥‘0)) |
17 | | efgredlemd.sc |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) |
18 | 17 | fveq2d 6721 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘(𝑆‘𝐶)) = (♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)))) |
19 | | fviss 6788 |
. . . . . . . . . . . . 13
⊢ ( I
‘Word (𝐼 ×
2o)) ⊆ Word (𝐼 × 2o) |
20 | 2, 19 | eqsstri 3935 |
. . . . . . . . . . . 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 19131 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴‘𝐾) ∈ 𝑊 ∧ (𝐵‘𝐿) ∈ 𝑊)) |
29 | 28 | simprd 499 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵‘𝐿) ∈ 𝑊) |
30 | 20, 29 | sseldi 3899 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵‘𝐿) ∈ Word (𝐼 × 2o)) |
31 | | pfxcl 14242 |
. . . . . . . . . . 11
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o)) |
32 | 30, 31 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o)) |
33 | 28 | simpld 498 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴‘𝐾) ∈ 𝑊) |
34 | 20, 33 | sseldi 3899 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴‘𝐾) ∈ Word (𝐼 × 2o)) |
35 | | swrdcl 14210 |
. . . . . . . . . . 11
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2o)) |
36 | 34, 35 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2o)) |
37 | | ccatlen 14130 |
. . . . . . . . . 10
⊢ ((((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2o)) →
(♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) = ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)))) |
38 | 32, 36, 37 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘(((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) = ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)))) |
39 | | pfxlen 14248 |
. . . . . . . . . . . 12
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈
(0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) prefix 𝑄)) = 𝑄) |
40 | 30, 14, 39 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘((𝐵‘𝐿) prefix 𝑄)) = 𝑄) |
41 | | 2nn0 12107 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ0 |
42 | | uzaddcl 12500 |
. . . . . . . . . . . . . 14
⊢ ((𝑄 ∈
(ℤ≥‘0) ∧ 2 ∈ ℕ0) →
(𝑄 + 2) ∈
(ℤ≥‘0)) |
43 | 16, 41, 42 | sylancl 589 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄 + 2) ∈
(ℤ≥‘0)) |
44 | | efgredlemb.p |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐴‘𝐾)))) |
45 | | elfzuz3 13109 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈
(0...(♯‘(𝐴‘𝐾))) → (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑃)) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑃)) |
47 | | efgredlemd.9 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) |
48 | | uztrn 12456 |
. . . . . . . . . . . . . 14
⊢
(((♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑃) ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) →
(♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘(𝑄 + 2))) |
49 | 46, 47, 48 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘(𝑄 + 2))) |
50 | | elfzuzb 13106 |
. . . . . . . . . . . . 13
⊢ ((𝑄 + 2) ∈
(0...(♯‘(𝐴‘𝐾))) ↔ ((𝑄 + 2) ∈
(ℤ≥‘0) ∧ (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘(𝑄 + 2)))) |
51 | 43, 49, 50 | sylanbrc 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾)))) |
52 | | lencl 14088 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) →
(♯‘(𝐴‘𝐾)) ∈
ℕ0) |
53 | 34, 52 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈
ℕ0) |
54 | | nn0uz 12476 |
. . . . . . . . . . . . . 14
⊢
ℕ0 = (ℤ≥‘0) |
55 | 53, 54 | eleqtrdi 2848 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘0)) |
56 | | eluzfz2 13120 |
. . . . . . . . . . . . 13
⊢
((♯‘(𝐴‘𝐾)) ∈ (ℤ≥‘0)
→ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾)))) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾)))) |
58 | | swrdlen 14212 |
. . . . . . . . . . . 12
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈
(0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = ((♯‘(𝐴‘𝐾)) − (𝑄 + 2))) |
59 | 34, 51, 57, 58 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = ((♯‘(𝐴‘𝐾)) − (𝑄 + 2))) |
60 | 40, 59 | oveq12d 7231 |
. . . . . . . . . 10
⊢ (𝜑 → ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) = (𝑄 + ((♯‘(𝐴‘𝐾)) − (𝑄 + 2)))) |
61 | 14 | elfzelzd 13113 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∈ ℤ) |
62 | 61 | zcnd 12283 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ ℂ) |
63 | 53 | nn0cnd 12152 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ ℂ) |
64 | | 2z 12209 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℤ |
65 | | zaddcl 12217 |
. . . . . . . . . . . . 13
⊢ ((𝑄 ∈ ℤ ∧ 2 ∈
ℤ) → (𝑄 + 2)
∈ ℤ) |
66 | 61, 64, 65 | sylancl 589 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 + 2) ∈ ℤ) |
67 | 66 | zcnd 12283 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑄 + 2) ∈ ℂ) |
68 | 62, 63, 67 | addsubassd 11209 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑄 + (♯‘(𝐴‘𝐾))) − (𝑄 + 2)) = (𝑄 + ((♯‘(𝐴‘𝐾)) − (𝑄 + 2)))) |
69 | | 2cn 11905 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
70 | 69 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℂ) |
71 | 62, 63, 70 | pnpcand 11226 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑄 + (♯‘(𝐴‘𝐾))) − (𝑄 + 2)) = ((♯‘(𝐴‘𝐾)) − 2)) |
72 | 60, 68, 71 | 3eqtr2d 2783 |
. . . . . . . . 9
⊢ (𝜑 → ((♯‘((𝐵‘𝐿) prefix 𝑄)) + (♯‘((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) = ((♯‘(𝐴‘𝐾)) − 2)) |
73 | 18, 38, 72 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (𝜑 → (♯‘(𝑆‘𝐶)) = ((♯‘(𝐴‘𝐾)) − 2)) |
74 | 44 | elfzelzd 13113 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℤ) |
75 | | zsubcl 12219 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℤ ∧ 2 ∈
ℤ) → (𝑃 −
2) ∈ ℤ) |
76 | 74, 64, 75 | sylancl 589 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 − 2) ∈ ℤ) |
77 | 64 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℤ) |
78 | 74 | zcnd 12283 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℂ) |
79 | | npcan 11087 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℂ ∧ 2 ∈
ℂ) → ((𝑃 −
2) + 2) = 𝑃) |
80 | 78, 69, 79 | sylancl 589 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑃 − 2) + 2) = 𝑃) |
81 | 80 | fveq2d 6721 |
. . . . . . . . . 10
⊢ (𝜑 →
(ℤ≥‘((𝑃 − 2) + 2)) =
(ℤ≥‘𝑃)) |
82 | 46, 81 | eleqtrrd 2841 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘((𝑃 − 2) + 2))) |
83 | | eluzsub 12470 |
. . . . . . . . 9
⊢ (((𝑃 − 2) ∈ ℤ ∧
2 ∈ ℤ ∧ (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘((𝑃 − 2) + 2))) →
((♯‘(𝐴‘𝐾)) − 2) ∈
(ℤ≥‘(𝑃 − 2))) |
84 | 76, 77, 82, 83 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → ((♯‘(𝐴‘𝐾)) − 2) ∈
(ℤ≥‘(𝑃 − 2))) |
85 | 73, 84 | eqeltrd 2838 |
. . . . . . 7
⊢ (𝜑 → (♯‘(𝑆‘𝐶)) ∈
(ℤ≥‘(𝑃 − 2))) |
86 | | eluzsub 12470 |
. . . . . . . 8
⊢ ((𝑄 ∈ ℤ ∧ 2 ∈
ℤ ∧ 𝑃 ∈
(ℤ≥‘(𝑄 + 2))) → (𝑃 − 2) ∈
(ℤ≥‘𝑄)) |
87 | 61, 77, 47, 86 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (𝑃 − 2) ∈
(ℤ≥‘𝑄)) |
88 | | uztrn 12456 |
. . . . . . 7
⊢
(((♯‘(𝑆‘𝐶)) ∈
(ℤ≥‘(𝑃 − 2)) ∧ (𝑃 − 2) ∈
(ℤ≥‘𝑄)) → (♯‘(𝑆‘𝐶)) ∈
(ℤ≥‘𝑄)) |
89 | 85, 87, 88 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (♯‘(𝑆‘𝐶)) ∈
(ℤ≥‘𝑄)) |
90 | | elfzuzb 13106 |
. . . . . 6
⊢ (𝑄 ∈
(0...(♯‘(𝑆‘𝐶))) ↔ (𝑄 ∈ (ℤ≥‘0)
∧ (♯‘(𝑆‘𝐶)) ∈
(ℤ≥‘𝑄))) |
91 | 16, 89, 90 | sylanbrc 586 |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝑆‘𝐶)))) |
92 | | efgredlemb.v |
. . . . 5
⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2o)) |
93 | 2, 3, 4, 5 | efgtval 19113 |
. . . . 5
⊢ (((𝑆‘𝐶) ∈ 𝑊 ∧ 𝑄 ∈ (0...(♯‘(𝑆‘𝐶))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = ((𝑆‘𝐶) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉)) |
94 | 13, 91, 92, 93 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = ((𝑆‘𝐶) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉)) |
95 | | pfxcl 14242 |
. . . . . 6
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o)) |
96 | 34, 95 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o)) |
97 | | wrd0 14094 |
. . . . . 6
⊢ ∅
∈ Word (𝐼 ×
2o) |
98 | 97 | a1i 11 |
. . . . 5
⊢ (𝜑 → ∅ ∈ Word (𝐼 ×
2o)) |
99 | 4 | efgmf 19103 |
. . . . . . . 8
⊢ 𝑀:(𝐼 × 2o)⟶(𝐼 ×
2o) |
100 | 99 | ffvelrni 6903 |
. . . . . . 7
⊢ (𝑉 ∈ (𝐼 × 2o) → (𝑀‘𝑉) ∈ (𝐼 × 2o)) |
101 | 92, 100 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑀‘𝑉) ∈ (𝐼 × 2o)) |
102 | 92, 101 | s2cld 14436 |
. . . . 5
⊢ (𝜑 → 〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 ×
2o)) |
103 | 61 | zred 12282 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑄 ∈ ℝ) |
104 | | nn0addge1 12136 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑄 ∈ ℝ ∧ 2 ∈
ℕ0) → 𝑄 ≤ (𝑄 + 2)) |
105 | 103, 41, 104 | sylancl 589 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑄 ≤ (𝑄 + 2)) |
106 | | eluz2 12444 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑄 + 2) ∈
(ℤ≥‘𝑄) ↔ (𝑄 ∈ ℤ ∧ (𝑄 + 2) ∈ ℤ ∧ 𝑄 ≤ (𝑄 + 2))) |
107 | 61, 66, 105, 106 | syl3anbrc 1345 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑄 + 2) ∈
(ℤ≥‘𝑄)) |
108 | | uztrn 12456 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈
(ℤ≥‘(𝑄 + 2)) ∧ (𝑄 + 2) ∈
(ℤ≥‘𝑄)) → 𝑃 ∈ (ℤ≥‘𝑄)) |
109 | 47, 107, 108 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘𝑄)) |
110 | | elfzuzb 13106 |
. . . . . . . . . . . . . 14
⊢ (𝑄 ∈ (0...𝑃) ↔ (𝑄 ∈ (ℤ≥‘0)
∧ 𝑃 ∈
(ℤ≥‘𝑄))) |
111 | 16, 109, 110 | sylanbrc 586 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∈ (0...𝑃)) |
112 | | ccatpfx 14266 |
. . . . . . . . . . . . 13
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) = ((𝐴‘𝐾) prefix 𝑃)) |
113 | 34, 111, 44, 112 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) = ((𝐴‘𝐾) prefix 𝑃)) |
114 | 113 | oveq1d 7228 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (((𝐴‘𝐾) prefix 𝑃) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)))) |
115 | | pfxcl 14242 |
. . . . . . . . . . . . 13
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o)) |
116 | 34, 115 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o)) |
117 | | efgredlemb.u |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2o)) |
118 | 99 | ffvelrni 6903 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ (𝐼 × 2o) → (𝑀‘𝑈) ∈ (𝐼 × 2o)) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀‘𝑈) ∈ (𝐼 × 2o)) |
120 | 117, 119 | s2cld 14436 |
. . . . . . . . . . . 12
⊢ (𝜑 → 〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 ×
2o)) |
121 | | swrdcl 14210 |
. . . . . . . . . . . . 13
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2o)) |
122 | 34, 121 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2o)) |
123 | | ccatass 14145 |
. . . . . . . . . . . 12
⊢ ((((𝐴‘𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o) ∧
〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 × 2o) ∧
((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2o)) → ((((𝐴‘𝐾) prefix 𝑃) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = (((𝐴‘𝐾) prefix 𝑃) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)))) |
124 | 116, 120,
122, 123 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑃) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = (((𝐴‘𝐾) prefix 𝑃) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)))) |
125 | | efgredlemb.6 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈)) |
126 | 2, 3, 4, 5 | efgtval 19113 |
. . . . . . . . . . . . . 14
⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ 𝑈 ∈ (𝐼 × 2o)) → (𝑃(𝑇‘(𝐴‘𝐾))𝑈) = ((𝐴‘𝐾) splice 〈𝑃, 𝑃, 〈“𝑈(𝑀‘𝑈)”〉〉)) |
127 | 33, 44, 117, 126 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃(𝑇‘(𝐴‘𝐾))𝑈) = ((𝐴‘𝐾) splice 〈𝑃, 𝑃, 〈“𝑈(𝑀‘𝑈)”〉〉)) |
128 | | splval 14316 |
. . . . . . . . . . . . . 14
⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ (𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ 〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 × 2o))) →
((𝐴‘𝐾) splice 〈𝑃, 𝑃, 〈“𝑈(𝑀‘𝑈)”〉〉) = ((((𝐴‘𝐾) prefix 𝑃) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) |
129 | 33, 44, 44, 120, 128 | syl13anc 1374 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴‘𝐾) splice 〈𝑃, 𝑃, 〈“𝑈(𝑀‘𝑈)”〉〉) = ((((𝐴‘𝐾) prefix 𝑃) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) |
130 | 125, 127,
129 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆‘𝐴) = ((((𝐴‘𝐾) prefix 𝑃) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) |
131 | | efgredlemb.7 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉)) |
132 | 2, 3, 4, 5 | efgtval 19113 |
. . . . . . . . . . . . . 14
⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝐵‘𝐿))𝑉) = ((𝐵‘𝐿) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉)) |
133 | 29, 14, 92, 132 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄(𝑇‘(𝐵‘𝐿))𝑉) = ((𝐵‘𝐿) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉)) |
134 | | splval 14316 |
. . . . . . . . . . . . . 14
⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ (𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ 𝑄 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ 〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 × 2o))) →
((𝐵‘𝐿) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉) = ((((𝐵‘𝐿) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))) |
135 | 29, 14, 14, 102, 134 | syl13anc 1374 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵‘𝐿) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉) = ((((𝐵‘𝐿) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))) |
136 | 131, 133,
135 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆‘𝐵) = ((((𝐵‘𝐿) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))) |
137 | 24, 130, 136 | 3eqtr3d 2785 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑃) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = ((((𝐵‘𝐿) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))) |
138 | 114, 124,
137 | 3eqtr2d 2783 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = ((((𝐵‘𝐿) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))) |
139 | | swrdcl 14210 |
. . . . . . . . . . . 12
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ∈ Word (𝐼 × 2o)) |
140 | 34, 139 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ∈ Word (𝐼 × 2o)) |
141 | | ccatcl 14129 |
. . . . . . . . . . . 12
⊢
((〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 × 2o) ∧
((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2o)) →
(〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 × 2o)) |
142 | 120, 122,
141 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 × 2o)) |
143 | | ccatass 14145 |
. . . . . . . . . . 11
⊢ ((((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ∈ Word (𝐼 × 2o) ∧
(〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 × 2o)) → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))))) |
144 | 96, 140, 142, 143 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))))) |
145 | | swrdcl 14210 |
. . . . . . . . . . . 12
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) |
146 | 30, 145 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) |
147 | | ccatass 14145 |
. . . . . . . . . . 11
⊢ ((((𝐵‘𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧
〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 × 2o) ∧
((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) → ((((𝐵‘𝐿) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) prefix 𝑄) ++ (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)))) |
148 | 32, 102, 146, 147 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) prefix 𝑄) ++ (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)))) |
149 | 138, 144,
148 | 3eqtr3d 2785 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)))) = (((𝐵‘𝐿) prefix 𝑄) ++ (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)))) |
150 | | ccatcl 14129 |
. . . . . . . . . . 11
⊢ ((((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ∈ Word (𝐼 × 2o) ∧
(〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 × 2o)) → (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) ∈ Word (𝐼 × 2o)) |
151 | 140, 142,
150 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) ∈ Word (𝐼 × 2o)) |
152 | | ccatcl 14129 |
. . . . . . . . . . 11
⊢
((〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 × 2o) ∧
((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) →
(〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)) ∈ Word (𝐼 × 2o)) |
153 | 102, 146,
152 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)) ∈ Word (𝐼 × 2o)) |
154 | | uztrn 12456 |
. . . . . . . . . . . . . 14
⊢
(((♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑃) ∧ 𝑃 ∈ (ℤ≥‘𝑄)) → (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑄)) |
155 | 46, 109, 154 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑄)) |
156 | | elfzuzb 13106 |
. . . . . . . . . . . . 13
⊢ (𝑄 ∈
(0...(♯‘(𝐴‘𝐾))) ↔ (𝑄 ∈ (ℤ≥‘0)
∧ (♯‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑄))) |
157 | 16, 155, 156 | sylanbrc 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐴‘𝐾)))) |
158 | | pfxlen 14248 |
. . . . . . . . . . . 12
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈
(0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) prefix 𝑄)) = 𝑄) |
159 | 34, 157, 158 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘((𝐴‘𝐾) prefix 𝑄)) = 𝑄) |
160 | 159, 40 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘((𝐴‘𝐾) prefix 𝑄)) = (♯‘((𝐵‘𝐿) prefix 𝑄))) |
161 | | ccatopth 14281 |
. . . . . . . . . 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 1383 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)))) = (((𝐵‘𝐿) prefix 𝑄) ++ (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))) ↔ (((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄) ∧ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))))) |
163 | 149, 162 | mpbid 235 |
. . . . . . . 8
⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄) ∧ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)))) |
164 | 163 | simpld 498 |
. . . . . . 7
⊢ (𝜑 → ((𝐴‘𝐾) prefix 𝑄) = ((𝐵‘𝐿) prefix 𝑄)) |
165 | 164 | oveq1d 7228 |
. . . . . 6
⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) |
166 | | ccatrid 14144 |
. . . . . . . 8
⊢ (((𝐴‘𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o) → (((𝐴‘𝐾) prefix 𝑄) ++ ∅) = ((𝐴‘𝐾) prefix 𝑄)) |
167 | 96, 166 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ∅) = ((𝐴‘𝐾) prefix 𝑄)) |
168 | 167 | oveq1d 7228 |
. . . . . 6
⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ ∅) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) |
169 | 165, 168,
17 | 3eqtr4rd 2788 |
. . . . 5
⊢ (𝜑 → (𝑆‘𝐶) = ((((𝐴‘𝐾) prefix 𝑄) ++ ∅) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) |
170 | 159 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → 𝑄 = (♯‘((𝐴‘𝐾) prefix 𝑄))) |
171 | | hash0 13934 |
. . . . . . 7
⊢
(♯‘∅) = 0 |
172 | 171 | oveq2i 7224 |
. . . . . 6
⊢ (𝑄 + (♯‘∅)) =
(𝑄 + 0) |
173 | 62 | addid1d 11032 |
. . . . . 6
⊢ (𝜑 → (𝑄 + 0) = 𝑄) |
174 | 172, 173 | eqtr2id 2791 |
. . . . 5
⊢ (𝜑 → 𝑄 = (𝑄 +
(♯‘∅))) |
175 | 96, 98, 36, 102, 169, 170, 174 | splval2 14322 |
. . . 4
⊢ (𝜑 → ((𝑆‘𝐶) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉) = ((((𝐴‘𝐾) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) |
176 | | elfzuzb 13106 |
. . . . . . . . . . . . . 14
⊢ (𝑄 ∈ (0...(𝑄 + 2)) ↔ (𝑄 ∈ (ℤ≥‘0)
∧ (𝑄 + 2) ∈
(ℤ≥‘𝑄))) |
177 | 16, 107, 176 | sylanbrc 586 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∈ (0...(𝑄 + 2))) |
178 | | elfzuzb 13106 |
. . . . . . . . . . . . . 14
⊢ ((𝑄 + 2) ∈ (0...𝑃) ↔ ((𝑄 + 2) ∈
(ℤ≥‘0) ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2)))) |
179 | 43, 47, 178 | sylanbrc 586 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄 + 2) ∈ (0...𝑃)) |
180 | | ccatswrd 14233 |
. . . . . . . . . . . . 13
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) = ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) |
181 | 34, 177, 179, 44, 180 | syl13anc 1374 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) = ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) |
182 | 181 | oveq1d 7228 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)))) |
183 | | swrdcl 14210 |
. . . . . . . . . . . . 13
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ∈ Word (𝐼 × 2o)) |
184 | 34, 183 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ∈ Word (𝐼 × 2o)) |
185 | | swrdcl 14210 |
. . . . . . . . . . . . 13
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ∈ Word (𝐼 × 2o)) |
186 | 34, 185 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ∈ Word (𝐼 × 2o)) |
187 | | ccatass 14145 |
. . . . . . . . . . . 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 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))))) |
189 | 163 | simprd 499 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))) |
190 | 182, 188,
189 | 3eqtr3d 2785 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)))) = (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))) |
191 | | ccatcl 14129 |
. . . . . . . . . . . 12
⊢ ((((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ∈ Word (𝐼 × 2o) ∧
(〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 × 2o)) → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) ∈ Word (𝐼 × 2o)) |
192 | 186, 142,
191 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) ∈ Word (𝐼 × 2o)) |
193 | | swrdlen 14212 |
. . . . . . . . . . . . . 14
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = ((𝑄 + 2) − 𝑄)) |
194 | 34, 177, 51, 193 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = ((𝑄 + 2) − 𝑄)) |
195 | | pncan2 11085 |
. . . . . . . . . . . . . 14
⊢ ((𝑄 ∈ ℂ ∧ 2 ∈
ℂ) → ((𝑄 + 2)
− 𝑄) =
2) |
196 | 62, 69, 195 | sylancl 589 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄 + 2) − 𝑄) = 2) |
197 | 194, 196 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = 2) |
198 | | s2len 14454 |
. . . . . . . . . . . 12
⊢
(♯‘〈“𝑉(𝑀‘𝑉)”〉) = 2 |
199 | 197, 198 | eqtr4di 2796 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) =
(♯‘〈“𝑉(𝑀‘𝑉)”〉)) |
200 | | ccatopth 14281 |
. . . . . . . . . . 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 1383 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)))) = (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)) ↔ (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) = 〈“𝑉(𝑀‘𝑉)”〉 ∧ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)))) |
202 | 190, 201 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) = 〈“𝑉(𝑀‘𝑉)”〉 ∧ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉))) |
203 | 202 | simpld 498 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) = 〈“𝑉(𝑀‘𝑉)”〉) |
204 | 203 | oveq2d 7229 |
. . . . . . 7
⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = (((𝐴‘𝐾) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉)) |
205 | | ccatpfx 14266 |
. . . . . . . 8
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = ((𝐴‘𝐾) prefix (𝑄 + 2))) |
206 | 34, 177, 51, 205 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = ((𝐴‘𝐾) prefix (𝑄 + 2))) |
207 | 204, 206 | eqtr3d 2779 |
. . . . . 6
⊢ (𝜑 → (((𝐴‘𝐾) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) = ((𝐴‘𝐾) prefix (𝑄 + 2))) |
208 | 207 | oveq1d 7228 |
. . . . 5
⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) |
209 | | ccatpfx 14266 |
. . . . . 6
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈
(0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾)))) → (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾)))) |
210 | 34, 51, 57, 209 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (((𝐴‘𝐾) prefix (𝑄 + 2)) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾)))) |
211 | | pfxid 14249 |
. . . . . 6
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) → ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))) = (𝐴‘𝐾)) |
212 | 34, 211 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐴‘𝐾) prefix (♯‘(𝐴‘𝐾))) = (𝐴‘𝐾)) |
213 | 208, 210,
212 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → ((((𝐴‘𝐾) prefix 𝑄) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = (𝐴‘𝐾)) |
214 | 94, 175, 213 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = (𝐴‘𝐾)) |
215 | 2, 3, 4, 5 | efgtf 19112 |
. . . . . . 7
⊢ ((𝑆‘𝐶) ∈ 𝑊 → ((𝑇‘(𝑆‘𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆‘𝐶))), 𝑖 ∈ (𝐼 × 2o) ↦ ((𝑆‘𝐶) splice 〈𝑎, 𝑎, 〈“𝑖(𝑀‘𝑖)”〉〉)) ∧ (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o))⟶𝑊)) |
216 | 13, 215 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑇‘(𝑆‘𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆‘𝐶))), 𝑖 ∈ (𝐼 × 2o) ↦ ((𝑆‘𝐶) splice 〈𝑎, 𝑎, 〈“𝑖(𝑀‘𝑖)”〉〉)) ∧ (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o))⟶𝑊)) |
217 | 216 | simprd 499 |
. . . . 5
⊢ (𝜑 → (𝑇‘(𝑆‘𝐶)):((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o))⟶𝑊) |
218 | 217 | ffnd 6546 |
. . . 4
⊢ (𝜑 → (𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o))) |
219 | | fnovrn 7383 |
. . . 4
⊢ (((𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o)) ∧ 𝑄 ∈
(0...(♯‘(𝑆‘𝐶))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) ∈ ran (𝑇‘(𝑆‘𝐶))) |
220 | 218, 91, 92, 219 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) ∈ ran (𝑇‘(𝑆‘𝐶))) |
221 | 214, 220 | eqeltrrd 2839 |
. 2
⊢ (𝜑 → (𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶))) |
222 | | uztrn 12456 |
. . . . . . 7
⊢ (((𝑃 − 2) ∈
(ℤ≥‘𝑄) ∧ 𝑄 ∈ (ℤ≥‘0))
→ (𝑃 − 2) ∈
(ℤ≥‘0)) |
223 | 87, 16, 222 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝑃 − 2) ∈
(ℤ≥‘0)) |
224 | | elfzuzb 13106 |
. . . . . 6
⊢ ((𝑃 − 2) ∈
(0...(♯‘(𝑆‘𝐶))) ↔ ((𝑃 − 2) ∈
(ℤ≥‘0) ∧ (♯‘(𝑆‘𝐶)) ∈
(ℤ≥‘(𝑃 − 2)))) |
225 | 223, 85, 224 | sylanbrc 586 |
. . . . 5
⊢ (𝜑 → (𝑃 − 2) ∈
(0...(♯‘(𝑆‘𝐶)))) |
226 | 2, 3, 4, 5 | efgtval 19113 |
. . . . 5
⊢ (((𝑆‘𝐶) ∈ 𝑊 ∧ (𝑃 − 2) ∈
(0...(♯‘(𝑆‘𝐶))) ∧ 𝑈 ∈ (𝐼 × 2o)) → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = ((𝑆‘𝐶) splice 〈(𝑃 − 2), (𝑃 − 2), 〈“𝑈(𝑀‘𝑈)”〉〉)) |
227 | 13, 225, 117, 226 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = ((𝑆‘𝐶) splice 〈(𝑃 − 2), (𝑃 − 2), 〈“𝑈(𝑀‘𝑈)”〉〉)) |
228 | | pfxcl 14242 |
. . . . . 6
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o)) |
229 | 30, 228 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o)) |
230 | | swrdcl 14210 |
. . . . . 6
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) |
231 | 30, 230 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) |
232 | | ccatswrd 14233 |
. . . . . . . . . . 11
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ ((𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾))) ∧ (♯‘(𝐴‘𝐾)) ∈ (0...(♯‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) |
233 | 34, 179, 44, 57, 232 | syl13anc 1374 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) |
234 | 202 | simprd 499 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)) |
235 | | elfzuzb 13106 |
. . . . . . . . . . . . . . . 16
⊢ (𝑄 ∈ (0...(𝑃 − 2)) ↔ (𝑄 ∈ (ℤ≥‘0)
∧ (𝑃 − 2) ∈
(ℤ≥‘𝑄))) |
236 | 16, 87, 235 | sylanbrc 586 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑄 ∈ (0...(𝑃 − 2))) |
237 | 2, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27, 44, 14, 117, 92, 125, 131 | efgredlemg 19132 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) = (♯‘(𝐵‘𝐿))) |
238 | 237, 46 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈
(ℤ≥‘𝑃)) |
239 | | 0le2 11932 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ≤
2 |
240 | 239 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ≤ 2) |
241 | 74 | zred 12282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑃 ∈ ℝ) |
242 | | 2re 11904 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ |
243 | | subge02 11348 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℝ ∧ 2 ∈
ℝ) → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃)) |
244 | 241, 242,
243 | sylancl 589 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃)) |
245 | 240, 244 | mpbid 235 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑃 − 2) ≤ 𝑃) |
246 | | eluz2 12444 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈
(ℤ≥‘(𝑃 − 2)) ↔ ((𝑃 − 2) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑃 − 2) ≤ 𝑃)) |
247 | 76, 74, 245, 246 | syl3anbrc 1345 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑃 − 2))) |
248 | | uztrn 12456 |
. . . . . . . . . . . . . . . . 17
⊢
(((♯‘(𝐵‘𝐿)) ∈
(ℤ≥‘𝑃) ∧ 𝑃 ∈ (ℤ≥‘(𝑃 − 2))) →
(♯‘(𝐵‘𝐿)) ∈
(ℤ≥‘(𝑃 − 2))) |
249 | 238, 247,
248 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈
(ℤ≥‘(𝑃 − 2))) |
250 | | elfzuzb 13106 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 − 2) ∈
(0...(♯‘(𝐵‘𝐿))) ↔ ((𝑃 − 2) ∈
(ℤ≥‘0) ∧ (♯‘(𝐵‘𝐿)) ∈
(ℤ≥‘(𝑃 − 2)))) |
251 | 223, 249,
250 | sylanbrc 586 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑃 − 2) ∈
(0...(♯‘(𝐵‘𝐿)))) |
252 | | lencl 14088 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) →
(♯‘(𝐵‘𝐿)) ∈
ℕ0) |
253 | 30, 252 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈
ℕ0) |
254 | 253, 54 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈
(ℤ≥‘0)) |
255 | | eluzfz2 13120 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘(𝐵‘𝐿)) ∈ (ℤ≥‘0)
→ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿)))) |
256 | 254, 255 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿)))) |
257 | | ccatswrd 14233 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈
(0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)) |
258 | 30, 236, 251, 256, 257 | syl13anc 1374 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) substr 〈𝑄, (♯‘(𝐵‘𝐿))〉)) |
259 | 234, 258 | eqtr4d 2780 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉))) |
260 | | swrdcl 14210 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ∈ Word (𝐼 ×
2o)) |
261 | 30, 260 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ∈ Word (𝐼 ×
2o)) |
262 | | swrdcl 14210 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) |
263 | 30, 262 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2o)) |
264 | | swrdlen 14212 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴‘𝐾)))) → (♯‘((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) = (𝑃 − (𝑄 + 2))) |
265 | 34, 179, 44, 264 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) = (𝑃 − (𝑄 + 2))) |
266 | | swrdlen 14212 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈
(0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) = ((𝑃 − 2) − 𝑄)) |
267 | 30, 236, 251, 266 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) = ((𝑃 − 2) − 𝑄)) |
268 | 78, 62, 70 | sub32d 11221 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑃 − 𝑄) − 2) = ((𝑃 − 2) − 𝑄)) |
269 | 78, 62, 70 | subsub4d 11220 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑃 − 𝑄) − 2) = (𝑃 − (𝑄 + 2))) |
270 | 267, 268,
269 | 3eqtr2d 2783 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) = (𝑃 − (𝑄 + 2))) |
271 | 265, 270 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) = (♯‘((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉))) |
272 | | ccatopth 14281 |
. . . . . . . . . . . . . 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 1383 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉))) = (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉)) ↔ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) = ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ∧ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉)))) |
274 | 259, 273 | mpbid 235 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) = ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ∧ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉))) |
275 | 274 | simpld 498 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) = ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) |
276 | 274 | simprd 499 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉)) |
277 | | elfzuzb 13106 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 − 2) ∈ (0...𝑃) ↔ ((𝑃 − 2) ∈
(ℤ≥‘0) ∧ 𝑃 ∈ (ℤ≥‘(𝑃 − 2)))) |
278 | 223, 247,
277 | sylanbrc 586 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑃 − 2) ∈ (0...𝑃)) |
279 | | elfzuz 13108 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈
(0...(♯‘(𝐴‘𝐾))) → 𝑃 ∈
(ℤ≥‘0)) |
280 | 44, 279 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈
(ℤ≥‘0)) |
281 | | elfzuzb 13106 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈
(0...(♯‘(𝐵‘𝐿))) ↔ (𝑃 ∈ (ℤ≥‘0)
∧ (♯‘(𝐵‘𝐿)) ∈
(ℤ≥‘𝑃))) |
282 | 280, 238,
281 | sylanbrc 586 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐵‘𝐿)))) |
283 | | ccatswrd 14233 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ ((𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉)) |
284 | 30, 278, 282, 256, 283 | syl13anc 1374 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) substr 〈(𝑃 − 2), (♯‘(𝐵‘𝐿))〉)) |
285 | 276, 284 | eqtr4d 2780 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) |
286 | | swrdcl 14210 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ∈ Word (𝐼 × 2o)) |
287 | 30, 286 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ∈ Word (𝐼 × 2o)) |
288 | | s2len 14454 |
. . . . . . . . . . . . . . 15
⊢
(♯‘〈“𝑈(𝑀‘𝑈)”〉) = 2 |
289 | | swrdlen 14212 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉)) = (𝑃 − (𝑃 − 2))) |
290 | 30, 278, 282, 289 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (♯‘((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉)) = (𝑃 − (𝑃 − 2))) |
291 | | nncan 11107 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℂ ∧ 2 ∈
ℂ) → (𝑃 −
(𝑃 − 2)) =
2) |
292 | 78, 69, 291 | sylancl 589 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃 − (𝑃 − 2)) = 2) |
293 | 290, 292 | eqtr2d 2778 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 = (♯‘((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉))) |
294 | 288, 293 | syl5eq 2790 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(♯‘〈“𝑈(𝑀‘𝑈)”〉) = (♯‘((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉))) |
295 | | ccatopth 14281 |
. . . . . . . . . . . . . 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 1383 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) ↔ (〈“𝑈(𝑀‘𝑈)”〉 = ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ∧ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉) = ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)))) |
297 | 285, 296 | mpbid 235 |
. . . . . . . . . . . 12
⊢ (𝜑 → (〈“𝑈(𝑀‘𝑈)”〉 = ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ∧ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉) = ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) |
298 | 297 | simprd 499 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉) = ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) |
299 | 275, 298 | oveq12d 7231 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (♯‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) |
300 | 233, 299 | eqtr3d 2779 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉) = (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) |
301 | 300 | oveq2d 7229 |
. . . . . . . 8
⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) prefix 𝑄) ++ (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)))) |
302 | | ccatass 14145 |
. . . . . . . . 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 1373 |
. . . . . . . 8
⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) prefix 𝑄) ++ (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)))) |
304 | 301, 303 | eqtr4d 2780 |
. . . . . . 7
⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉)) = ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) |
305 | | ccatpfx 14266 |
. . . . . . . . 9
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈
(0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) = ((𝐵‘𝐿) prefix (𝑃 − 2))) |
306 | 30, 236, 251, 305 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) = ((𝐵‘𝐿) prefix (𝑃 − 2))) |
307 | 306 | oveq1d 7228 |
. . . . . . 7
⊢ (𝜑 → ((((𝐵‘𝐿) prefix 𝑄) ++ ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) |
308 | 17, 304, 307 | 3eqtrd 2781 |
. . . . . 6
⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) |
309 | | ccatrid 14144 |
. . . . . . . 8
⊢ (((𝐵‘𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o) → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) = ((𝐵‘𝐿) prefix (𝑃 − 2))) |
310 | 229, 309 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) = ((𝐵‘𝐿) prefix (𝑃 − 2))) |
311 | 310 | oveq1d 7228 |
. . . . . 6
⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) |
312 | 308, 311 | eqtr4d 2780 |
. . . . 5
⊢ (𝜑 → (𝑆‘𝐶) = ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ∅) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) |
313 | | pfxlen 14248 |
. . . . . . 7
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈
(0...(♯‘(𝐵‘𝐿)))) → (♯‘((𝐵‘𝐿) prefix (𝑃 − 2))) = (𝑃 − 2)) |
314 | 30, 251, 313 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (♯‘((𝐵‘𝐿) prefix (𝑃 − 2))) = (𝑃 − 2)) |
315 | 314 | eqcomd 2743 |
. . . . 5
⊢ (𝜑 → (𝑃 − 2) = (♯‘((𝐵‘𝐿) prefix (𝑃 − 2)))) |
316 | 171 | oveq2i 7224 |
. . . . . 6
⊢ ((𝑃 − 2) +
(♯‘∅)) = ((𝑃 − 2) + 0) |
317 | 76 | zcnd 12283 |
. . . . . . 7
⊢ (𝜑 → (𝑃 − 2) ∈ ℂ) |
318 | 317 | addid1d 11032 |
. . . . . 6
⊢ (𝜑 → ((𝑃 − 2) + 0) = (𝑃 − 2)) |
319 | 316, 318 | eqtr2id 2791 |
. . . . 5
⊢ (𝜑 → (𝑃 − 2) = ((𝑃 − 2) +
(♯‘∅))) |
320 | 229, 98, 231, 120, 312, 315, 319 | splval2 14322 |
. . . 4
⊢ (𝜑 → ((𝑆‘𝐶) splice 〈(𝑃 − 2), (𝑃 − 2), 〈“𝑈(𝑀‘𝑈)”〉〉) = ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) |
321 | 297 | simpld 498 |
. . . . . . . 8
⊢ (𝜑 → 〈“𝑈(𝑀‘𝑈)”〉 = ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉)) |
322 | 321 | oveq2d 7229 |
. . . . . . 7
⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ 〈“𝑈(𝑀‘𝑈)”〉) = (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉))) |
323 | | ccatpfx 14266 |
. . . . . . . 8
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉)) = ((𝐵‘𝐿) prefix 𝑃)) |
324 | 30, 278, 282, 323 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉)) = ((𝐵‘𝐿) prefix 𝑃)) |
325 | 322, 324 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → (((𝐵‘𝐿) prefix (𝑃 − 2)) ++ 〈“𝑈(𝑀‘𝑈)”〉) = ((𝐵‘𝐿) prefix 𝑃)) |
326 | 325 | oveq1d 7228 |
. . . . 5
⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉))) |
327 | | ccatpfx 14266 |
. . . . . 6
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑃 ∈
(0...(♯‘(𝐵‘𝐿))) ∧ (♯‘(𝐵‘𝐿)) ∈ (0...(♯‘(𝐵‘𝐿)))) → (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿)))) |
328 | 30, 282, 256, 327 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (((𝐵‘𝐿) prefix 𝑃) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿)))) |
329 | | pfxid 14249 |
. . . . . 6
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) → ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))) = (𝐵‘𝐿)) |
330 | 30, 329 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐵‘𝐿) prefix (♯‘(𝐵‘𝐿))) = (𝐵‘𝐿)) |
331 | 326, 328,
330 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → ((((𝐵‘𝐿) prefix (𝑃 − 2)) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (♯‘(𝐵‘𝐿))〉)) = (𝐵‘𝐿)) |
332 | 227, 320,
331 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = (𝐵‘𝐿)) |
333 | | fnovrn 7383 |
. . . 4
⊢ (((𝑇‘(𝑆‘𝐶)) Fn ((0...(♯‘(𝑆‘𝐶))) × (𝐼 × 2o)) ∧ (𝑃 − 2) ∈
(0...(♯‘(𝑆‘𝐶))) ∧ 𝑈 ∈ (𝐼 × 2o)) → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) ∈ ran (𝑇‘(𝑆‘𝐶))) |
334 | 218, 225,
117, 333 | syl3anc 1373 |
. . 3
⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) ∈ ran (𝑇‘(𝑆‘𝐶))) |
335 | 332, 334 | eqeltrrd 2839 |
. 2
⊢ (𝜑 → (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶))) |
336 | 221, 335 | jca 515 |
1
⊢ (𝜑 → ((𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶)) ∧ (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶)))) |