Step | Hyp | Ref
| Expression |
1 | | efgredlemd.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ dom 𝑆) |
2 | | efgval.w |
. . . . . . . . 9
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2𝑜)) |
3 | | efgval.r |
. . . . . . . . 9
⊢ ∼ = (
~FG ‘𝐼) |
4 | | efgval2.m |
. . . . . . . . 9
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) |
5 | | efgval2.t |
. . . . . . . . 9
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) |
6 | | efgred.d |
. . . . . . . . 9
⊢ 𝐷 = (𝑊 ∖ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) |
7 | | efgred.s |
. . . . . . . . 9
⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) |
8 | 2, 3, 4, 5, 6, 7 | efgsf 18142 |
. . . . . . . 8
⊢ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊 |
9 | 8 | fdmi 6052 |
. . . . . . . . 9
⊢ dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} |
10 | 9 | feq2i 6037 |
. . . . . . . 8
⊢ (𝑆:dom 𝑆⟶𝑊 ↔ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊) |
11 | 8, 10 | mpbir 221 |
. . . . . . 7
⊢ 𝑆:dom 𝑆⟶𝑊 |
12 | 11 | ffvelrni 6358 |
. . . . . 6
⊢ (𝐶 ∈ dom 𝑆 → (𝑆‘𝐶) ∈ 𝑊) |
13 | 1, 12 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑆‘𝐶) ∈ 𝑊) |
14 | | efgredlemb.q |
. . . . . . 7
⊢ (𝜑 → 𝑄 ∈ (0...(#‘(𝐵‘𝐿)))) |
15 | | elfzuz 12338 |
. . . . . . 7
⊢ (𝑄 ∈ (0...(#‘(𝐵‘𝐿))) → 𝑄 ∈
(ℤ≥‘0)) |
16 | 14, 15 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈
(ℤ≥‘0)) |
17 | | efgredlemd.sc |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉))) |
18 | 17 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝜑 → (#‘(𝑆‘𝐶)) = (#‘(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)))) |
19 | | fviss 6256 |
. . . . . . . . . . . . 13
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ⊆ Word (𝐼 ×
2𝑜) |
20 | 2, 19 | eqsstri 3635 |
. . . . . . . . . . . 12
⊢ 𝑊 ⊆ Word (𝐼 ×
2𝑜) |
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 18154 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴‘𝐾) ∈ 𝑊 ∧ (𝐵‘𝐿) ∈ 𝑊)) |
29 | 28 | simprd 479 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵‘𝐿) ∈ 𝑊) |
30 | 20, 29 | sseldi 3601 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵‘𝐿) ∈ Word (𝐼 ×
2𝑜)) |
31 | | swrdcl 13419 |
. . . . . . . . . . 11
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) →
((𝐵‘𝐿) substr 〈0, 𝑄〉) ∈ Word (𝐼 ×
2𝑜)) |
32 | 30, 31 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈0, 𝑄〉) ∈ Word (𝐼 ×
2𝑜)) |
33 | 28 | simpld 475 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴‘𝐾) ∈ 𝑊) |
34 | 20, 33 | sseldi 3601 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴‘𝐾) ∈ Word (𝐼 ×
2𝑜)) |
35 | | swrdcl 13419 |
. . . . . . . . . . 11
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) →
((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉) ∈ Word (𝐼 ×
2𝑜)) |
36 | 34, 35 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉) ∈ Word (𝐼 ×
2𝑜)) |
37 | | ccatlen 13360 |
. . . . . . . . . 10
⊢ ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ∈ Word (𝐼 × 2𝑜) ∧
((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2𝑜)) →
(#‘(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉))) = ((#‘((𝐵‘𝐿) substr 〈0, 𝑄〉)) + (#‘((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)))) |
38 | 32, 36, 37 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (#‘(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉))) = ((#‘((𝐵‘𝐿) substr 〈0, 𝑄〉)) + (#‘((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)))) |
39 | | swrd0len 13422 |
. . . . . . . . . . . 12
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(#‘(𝐵‘𝐿)))) → (#‘((𝐵‘𝐿) substr 〈0, 𝑄〉)) = 𝑄) |
40 | 30, 14, 39 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘((𝐵‘𝐿) substr 〈0, 𝑄〉)) = 𝑄) |
41 | | 2nn0 11309 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ0 |
42 | | uzaddcl 11744 |
. . . . . . . . . . . . . 14
⊢ ((𝑄 ∈
(ℤ≥‘0) ∧ 2 ∈ ℕ0) →
(𝑄 + 2) ∈
(ℤ≥‘0)) |
43 | 16, 41, 42 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄 + 2) ∈
(ℤ≥‘0)) |
44 | | efgredlemb.p |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ (0...(#‘(𝐴‘𝐾)))) |
45 | | elfzuz3 12339 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ (0...(#‘(𝐴‘𝐾))) → (#‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑃)) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (#‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑃)) |
47 | | efgredlemd.9 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) |
48 | | uztrn 11704 |
. . . . . . . . . . . . . 14
⊢
(((#‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑃) ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) → (#‘(𝐴‘𝐾)) ∈
(ℤ≥‘(𝑄 + 2))) |
49 | 46, 47, 48 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (#‘(𝐴‘𝐾)) ∈
(ℤ≥‘(𝑄 + 2))) |
50 | | elfzuzb 12336 |
. . . . . . . . . . . . 13
⊢ ((𝑄 + 2) ∈
(0...(#‘(𝐴‘𝐾))) ↔ ((𝑄 + 2) ∈
(ℤ≥‘0) ∧ (#‘(𝐴‘𝐾)) ∈
(ℤ≥‘(𝑄 + 2)))) |
51 | 43, 49, 50 | sylanbrc 698 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 + 2) ∈ (0...(#‘(𝐴‘𝐾)))) |
52 | | lencl 13324 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) →
(#‘(𝐴‘𝐾)) ∈
ℕ0) |
53 | 34, 52 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (#‘(𝐴‘𝐾)) ∈
ℕ0) |
54 | | nn0uz 11722 |
. . . . . . . . . . . . . 14
⊢
ℕ0 = (ℤ≥‘0) |
55 | 53, 54 | syl6eleq 2711 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (#‘(𝐴‘𝐾)) ∈
(ℤ≥‘0)) |
56 | | eluzfz2 12349 |
. . . . . . . . . . . . 13
⊢
((#‘(𝐴‘𝐾)) ∈ (ℤ≥‘0)
→ (#‘(𝐴‘𝐾)) ∈ (0...(#‘(𝐴‘𝐾)))) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (#‘(𝐴‘𝐾)) ∈ (0...(#‘(𝐴‘𝐾)))) |
58 | | swrdlen 13423 |
. . . . . . . . . . . 12
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 + 2) ∈
(0...(#‘(𝐴‘𝐾))) ∧ (#‘(𝐴‘𝐾)) ∈ (0...(#‘(𝐴‘𝐾)))) → (#‘((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = ((#‘(𝐴‘𝐾)) − (𝑄 + 2))) |
59 | 34, 51, 57, 58 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = ((#‘(𝐴‘𝐾)) − (𝑄 + 2))) |
60 | 40, 59 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝜑 → ((#‘((𝐵‘𝐿) substr 〈0, 𝑄〉)) + (#‘((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉))) = (𝑄 + ((#‘(𝐴‘𝐾)) − (𝑄 + 2)))) |
61 | | elfzelz 12342 |
. . . . . . . . . . . . 13
⊢ (𝑄 ∈ (0...(#‘(𝐵‘𝐿))) → 𝑄 ∈ ℤ) |
62 | 14, 61 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∈ ℤ) |
63 | 62 | zcnd 11483 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ ℂ) |
64 | 53 | nn0cnd 11353 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘(𝐴‘𝐾)) ∈ ℂ) |
65 | | 2z 11409 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℤ |
66 | | zaddcl 11417 |
. . . . . . . . . . . . 13
⊢ ((𝑄 ∈ ℤ ∧ 2 ∈
ℤ) → (𝑄 + 2)
∈ ℤ) |
67 | 62, 65, 66 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 + 2) ∈ ℤ) |
68 | 67 | zcnd 11483 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑄 + 2) ∈ ℂ) |
69 | 63, 64, 68 | addsubassd 10412 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑄 + (#‘(𝐴‘𝐾))) − (𝑄 + 2)) = (𝑄 + ((#‘(𝐴‘𝐾)) − (𝑄 + 2)))) |
70 | | 2cn 11091 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
71 | 70 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℂ) |
72 | 63, 64, 71 | pnpcand 10429 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑄 + (#‘(𝐴‘𝐾))) − (𝑄 + 2)) = ((#‘(𝐴‘𝐾)) − 2)) |
73 | 60, 69, 72 | 3eqtr2d 2662 |
. . . . . . . . 9
⊢ (𝜑 → ((#‘((𝐵‘𝐿) substr 〈0, 𝑄〉)) + (#‘((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉))) = ((#‘(𝐴‘𝐾)) − 2)) |
74 | 18, 38, 73 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (𝜑 → (#‘(𝑆‘𝐶)) = ((#‘(𝐴‘𝐾)) − 2)) |
75 | | elfzelz 12342 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ (0...(#‘(𝐴‘𝐾))) → 𝑃 ∈ ℤ) |
76 | 44, 75 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℤ) |
77 | | zsubcl 11419 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℤ ∧ 2 ∈
ℤ) → (𝑃 −
2) ∈ ℤ) |
78 | 76, 65, 77 | sylancl 694 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 − 2) ∈ ℤ) |
79 | 65 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℤ) |
80 | 76 | zcnd 11483 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℂ) |
81 | | npcan 10290 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℂ ∧ 2 ∈
ℂ) → ((𝑃 −
2) + 2) = 𝑃) |
82 | 80, 70, 81 | sylancl 694 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑃 − 2) + 2) = 𝑃) |
83 | 82 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝜑 →
(ℤ≥‘((𝑃 − 2) + 2)) =
(ℤ≥‘𝑃)) |
84 | 46, 83 | eleqtrrd 2704 |
. . . . . . . . 9
⊢ (𝜑 → (#‘(𝐴‘𝐾)) ∈
(ℤ≥‘((𝑃 − 2) + 2))) |
85 | | eluzsub 11717 |
. . . . . . . . 9
⊢ (((𝑃 − 2) ∈ ℤ ∧
2 ∈ ℤ ∧ (#‘(𝐴‘𝐾)) ∈
(ℤ≥‘((𝑃 − 2) + 2))) → ((#‘(𝐴‘𝐾)) − 2) ∈
(ℤ≥‘(𝑃 − 2))) |
86 | 78, 79, 84, 85 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → ((#‘(𝐴‘𝐾)) − 2) ∈
(ℤ≥‘(𝑃 − 2))) |
87 | 74, 86 | eqeltrd 2701 |
. . . . . . 7
⊢ (𝜑 → (#‘(𝑆‘𝐶)) ∈
(ℤ≥‘(𝑃 − 2))) |
88 | | eluzsub 11717 |
. . . . . . . 8
⊢ ((𝑄 ∈ ℤ ∧ 2 ∈
ℤ ∧ 𝑃 ∈
(ℤ≥‘(𝑄 + 2))) → (𝑃 − 2) ∈
(ℤ≥‘𝑄)) |
89 | 62, 79, 47, 88 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → (𝑃 − 2) ∈
(ℤ≥‘𝑄)) |
90 | | uztrn 11704 |
. . . . . . 7
⊢
(((#‘(𝑆‘𝐶)) ∈
(ℤ≥‘(𝑃 − 2)) ∧ (𝑃 − 2) ∈
(ℤ≥‘𝑄)) → (#‘(𝑆‘𝐶)) ∈
(ℤ≥‘𝑄)) |
91 | 87, 89, 90 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (#‘(𝑆‘𝐶)) ∈
(ℤ≥‘𝑄)) |
92 | | elfzuzb 12336 |
. . . . . 6
⊢ (𝑄 ∈ (0...(#‘(𝑆‘𝐶))) ↔ (𝑄 ∈ (ℤ≥‘0)
∧ (#‘(𝑆‘𝐶)) ∈
(ℤ≥‘𝑄))) |
93 | 16, 91, 92 | sylanbrc 698 |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ (0...(#‘(𝑆‘𝐶)))) |
94 | | efgredlemb.v |
. . . . 5
⊢ (𝜑 → 𝑉 ∈ (𝐼 ×
2𝑜)) |
95 | 2, 3, 4, 5 | efgtval 18136 |
. . . . 5
⊢ (((𝑆‘𝐶) ∈ 𝑊 ∧ 𝑄 ∈ (0...(#‘(𝑆‘𝐶))) ∧ 𝑉 ∈ (𝐼 × 2𝑜)) →
(𝑄(𝑇‘(𝑆‘𝐶))𝑉) = ((𝑆‘𝐶) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉)) |
96 | 13, 93, 94, 95 | syl3anc 1326 |
. . . 4
⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = ((𝑆‘𝐶) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉)) |
97 | | swrdcl 13419 |
. . . . . 6
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) →
((𝐴‘𝐾) substr 〈0, 𝑄〉) ∈ Word (𝐼 ×
2𝑜)) |
98 | 34, 97 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈0, 𝑄〉) ∈ Word (𝐼 ×
2𝑜)) |
99 | | wrd0 13330 |
. . . . . 6
⊢ ∅
∈ Word (𝐼 ×
2𝑜) |
100 | 99 | a1i 11 |
. . . . 5
⊢ (𝜑 → ∅ ∈ Word (𝐼 ×
2𝑜)) |
101 | 4 | efgmf 18126 |
. . . . . . . 8
⊢ 𝑀:(𝐼 ×
2𝑜)⟶(𝐼 ×
2𝑜) |
102 | 101 | ffvelrni 6358 |
. . . . . . 7
⊢ (𝑉 ∈ (𝐼 × 2𝑜) →
(𝑀‘𝑉) ∈ (𝐼 ×
2𝑜)) |
103 | 94, 102 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑀‘𝑉) ∈ (𝐼 ×
2𝑜)) |
104 | 94, 103 | s2cld 13616 |
. . . . 5
⊢ (𝜑 → 〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 ×
2𝑜)) |
105 | | eluzfz1 12348 |
. . . . . . . . . . . . . 14
⊢ (𝑄 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑄)) |
106 | 16, 105 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈ (0...𝑄)) |
107 | 62 | zred 11482 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑄 ∈ ℝ) |
108 | | nn0addge1 11339 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑄 ∈ ℝ ∧ 2 ∈
ℕ0) → 𝑄 ≤ (𝑄 + 2)) |
109 | 107, 41, 108 | sylancl 694 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑄 ≤ (𝑄 + 2)) |
110 | | eluz2 11693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑄 + 2) ∈
(ℤ≥‘𝑄) ↔ (𝑄 ∈ ℤ ∧ (𝑄 + 2) ∈ ℤ ∧ 𝑄 ≤ (𝑄 + 2))) |
111 | 62, 67, 109, 110 | syl3anbrc 1246 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑄 + 2) ∈
(ℤ≥‘𝑄)) |
112 | | uztrn 11704 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈
(ℤ≥‘(𝑄 + 2)) ∧ (𝑄 + 2) ∈
(ℤ≥‘𝑄)) → 𝑃 ∈ (ℤ≥‘𝑄)) |
113 | 47, 111, 112 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘𝑄)) |
114 | | elfzuzb 12336 |
. . . . . . . . . . . . . 14
⊢ (𝑄 ∈ (0...𝑃) ↔ (𝑄 ∈ (ℤ≥‘0)
∧ 𝑃 ∈
(ℤ≥‘𝑄))) |
115 | 16, 113, 114 | sylanbrc 698 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∈ (0...𝑃)) |
116 | | ccatswrd 13456 |
. . . . . . . . . . . . 13
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (0
∈ (0...𝑄) ∧ 𝑄 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) = ((𝐴‘𝐾) substr 〈0, 𝑃〉)) |
117 | 34, 106, 115, 44, 116 | syl13anc 1328 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) = ((𝐴‘𝐾) substr 〈0, 𝑃〉)) |
118 | 117 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)))) |
119 | | swrdcl 13419 |
. . . . . . . . . . . . 13
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) →
((𝐴‘𝐾) substr 〈0, 𝑃〉) ∈ Word (𝐼 ×
2𝑜)) |
120 | 34, 119 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈0, 𝑃〉) ∈ Word (𝐼 ×
2𝑜)) |
121 | | efgredlemb.u |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈ (𝐼 ×
2𝑜)) |
122 | 101 | ffvelrni 6358 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ (𝐼 × 2𝑜) →
(𝑀‘𝑈) ∈ (𝐼 ×
2𝑜)) |
123 | 121, 122 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀‘𝑈) ∈ (𝐼 ×
2𝑜)) |
124 | 121, 123 | s2cld 13616 |
. . . . . . . . . . . 12
⊢ (𝜑 → 〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 ×
2𝑜)) |
125 | | swrdcl 13419 |
. . . . . . . . . . . . 13
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) →
((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) ∈ Word (𝐼 ×
2𝑜)) |
126 | 34, 125 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) ∈ Word (𝐼 ×
2𝑜)) |
127 | | ccatass 13371 |
. . . . . . . . . . . 12
⊢ ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ∈ Word (𝐼 × 2𝑜) ∧
〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 × 2𝑜)
∧ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2𝑜)) →
((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)))) |
128 | 120, 124,
126, 127 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)))) |
129 | | efgredlemb.6 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈)) |
130 | 2, 3, 4, 5 | efgtval 18136 |
. . . . . . . . . . . . . 14
⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ 𝑃 ∈ (0...(#‘(𝐴‘𝐾))) ∧ 𝑈 ∈ (𝐼 × 2𝑜)) →
(𝑃(𝑇‘(𝐴‘𝐾))𝑈) = ((𝐴‘𝐾) splice 〈𝑃, 𝑃, 〈“𝑈(𝑀‘𝑈)”〉〉)) |
131 | 33, 44, 121, 130 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃(𝑇‘(𝐴‘𝐾))𝑈) = ((𝐴‘𝐾) splice 〈𝑃, 𝑃, 〈“𝑈(𝑀‘𝑈)”〉〉)) |
132 | | splval 13502 |
. . . . . . . . . . . . . 14
⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ (𝑃 ∈ (0...(#‘(𝐴‘𝐾))) ∧ 𝑃 ∈ (0...(#‘(𝐴‘𝐾))) ∧ 〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 ×
2𝑜))) → ((𝐴‘𝐾) splice 〈𝑃, 𝑃, 〈“𝑈(𝑀‘𝑈)”〉〉) = ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) |
133 | 33, 44, 44, 124, 132 | syl13anc 1328 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴‘𝐾) splice 〈𝑃, 𝑃, 〈“𝑈(𝑀‘𝑈)”〉〉) = ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) |
134 | 129, 131,
133 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆‘𝐴) = ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) |
135 | | efgredlemb.7 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉)) |
136 | 2, 3, 4, 5 | efgtval 18136 |
. . . . . . . . . . . . . 14
⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ 𝑄 ∈ (0...(#‘(𝐵‘𝐿))) ∧ 𝑉 ∈ (𝐼 × 2𝑜)) →
(𝑄(𝑇‘(𝐵‘𝐿))𝑉) = ((𝐵‘𝐿) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉)) |
137 | 29, 14, 94, 136 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄(𝑇‘(𝐵‘𝐿))𝑉) = ((𝐵‘𝐿) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉)) |
138 | | splval 13502 |
. . . . . . . . . . . . . 14
⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ (𝑄 ∈ (0...(#‘(𝐵‘𝐿))) ∧ 𝑄 ∈ (0...(#‘(𝐵‘𝐿))) ∧ 〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 ×
2𝑜))) → ((𝐵‘𝐿) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
139 | 29, 14, 14, 104, 138 | syl13anc 1328 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵‘𝐿) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
140 | 135, 137,
139 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆‘𝐵) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
141 | 24, 134, 140 | 3eqtr3d 2664 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
142 | 118, 128,
141 | 3eqtr2d 2662 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
143 | | swrdcl 13419 |
. . . . . . . . . . . 12
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) →
((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ∈ Word (𝐼 ×
2𝑜)) |
144 | 34, 143 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ∈ Word (𝐼 ×
2𝑜)) |
145 | | ccatcl 13359 |
. . . . . . . . . . . 12
⊢
((〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 × 2𝑜)
∧ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2𝑜)) →
(〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 ×
2𝑜)) |
146 | 124, 126,
145 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 ×
2𝑜)) |
147 | | ccatass 13371 |
. . . . . . . . . . 11
⊢ ((((𝐴‘𝐾) substr 〈0, 𝑄〉) ∈ Word (𝐼 × 2𝑜) ∧
((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ∈ Word (𝐼 × 2𝑜) ∧
(〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 × 2𝑜)) →
((((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = (((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))))) |
148 | 98, 144, 146, 147 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = (((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))))) |
149 | | swrdcl 13419 |
. . . . . . . . . . . 12
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) →
((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉) ∈ Word (𝐼 ×
2𝑜)) |
150 | 30, 149 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉) ∈ Word (𝐼 ×
2𝑜)) |
151 | | ccatass 13371 |
. . . . . . . . . . 11
⊢ ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ∈ Word (𝐼 × 2𝑜) ∧
〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 × 2𝑜)
∧ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2𝑜)) →
((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)))) |
152 | 32, 104, 150, 151 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)))) |
153 | 142, 148,
152 | 3eqtr3d 2664 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)))) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)))) |
154 | | ccatcl 13359 |
. . . . . . . . . . 11
⊢ ((((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ∈ Word (𝐼 × 2𝑜) ∧
(〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 × 2𝑜)) →
(((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) ∈ Word (𝐼 ×
2𝑜)) |
155 | 144, 146,
154 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) ∈ Word (𝐼 ×
2𝑜)) |
156 | | ccatcl 13359 |
. . . . . . . . . . 11
⊢
((〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 × 2𝑜)
∧ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2𝑜)) →
(〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) ∈ Word (𝐼 ×
2𝑜)) |
157 | 104, 150,
156 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) ∈ Word (𝐼 ×
2𝑜)) |
158 | | uztrn 11704 |
. . . . . . . . . . . . . 14
⊢
(((#‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑃) ∧ 𝑃 ∈ (ℤ≥‘𝑄)) → (#‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑄)) |
159 | 46, 113, 158 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (#‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑄)) |
160 | | elfzuzb 12336 |
. . . . . . . . . . . . 13
⊢ (𝑄 ∈ (0...(#‘(𝐴‘𝐾))) ↔ (𝑄 ∈ (ℤ≥‘0)
∧ (#‘(𝐴‘𝐾)) ∈
(ℤ≥‘𝑄))) |
161 | 16, 159, 160 | sylanbrc 698 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∈ (0...(#‘(𝐴‘𝐾)))) |
162 | | swrd0len 13422 |
. . . . . . . . . . . 12
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(#‘(𝐴‘𝐾)))) → (#‘((𝐴‘𝐾) substr 〈0, 𝑄〉)) = 𝑄) |
163 | 34, 161, 162 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘((𝐴‘𝐾) substr 〈0, 𝑄〉)) = 𝑄) |
164 | 163, 40 | eqtr4d 2659 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘((𝐴‘𝐾) substr 〈0, 𝑄〉)) = (#‘((𝐵‘𝐿) substr 〈0, 𝑄〉))) |
165 | | ccatopth 13470 |
. . . . . . . . . 10
⊢
(((((𝐴‘𝐾) substr 〈0, 𝑄〉) ∈ Word (𝐼 × 2𝑜)
∧ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) ∈ Word (𝐼 × 2𝑜)) ∧
(((𝐵‘𝐿) substr 〈0, 𝑄〉) ∈ Word (𝐼 × 2𝑜)
∧ (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) ∈ Word (𝐼 × 2𝑜)) ∧
(#‘((𝐴‘𝐾) substr 〈0, 𝑄〉)) = (#‘((𝐵‘𝐿) substr 〈0, 𝑄〉))) → ((((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)))) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) ↔ (((𝐴‘𝐾) substr 〈0, 𝑄〉) = ((𝐵‘𝐿) substr 〈0, 𝑄〉) ∧ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))))) |
166 | 98, 155, 32, 157, 164, 165 | syl221anc 1337 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)))) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) ↔ (((𝐴‘𝐾) substr 〈0, 𝑄〉) = ((𝐵‘𝐿) substr 〈0, 𝑄〉) ∧ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))))) |
167 | 153, 166 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈0, 𝑄〉) = ((𝐵‘𝐿) substr 〈0, 𝑄〉) ∧ (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)))) |
168 | 167 | simpld 475 |
. . . . . . 7
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈0, 𝑄〉) = ((𝐵‘𝐿) substr 〈0, 𝑄〉)) |
169 | 168 | oveq1d 6665 |
. . . . . 6
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉))) |
170 | | ccatrid 13370 |
. . . . . . . 8
⊢ (((𝐴‘𝐾) substr 〈0, 𝑄〉) ∈ Word (𝐼 × 2𝑜) →
(((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ ∅) = ((𝐴‘𝐾) substr 〈0, 𝑄〉)) |
171 | 98, 170 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ ∅) = ((𝐴‘𝐾) substr 〈0, 𝑄〉)) |
172 | 171 | oveq1d 6665 |
. . . . . 6
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ ∅) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉))) |
173 | 169, 172,
17 | 3eqtr4rd 2667 |
. . . . 5
⊢ (𝜑 → (𝑆‘𝐶) = ((((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ ∅) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉))) |
174 | 163 | eqcomd 2628 |
. . . . 5
⊢ (𝜑 → 𝑄 = (#‘((𝐴‘𝐾) substr 〈0, 𝑄〉))) |
175 | | hash0 13158 |
. . . . . . 7
⊢
(#‘∅) = 0 |
176 | 175 | oveq2i 6661 |
. . . . . 6
⊢ (𝑄 + (#‘∅)) = (𝑄 + 0) |
177 | 63 | addid1d 10236 |
. . . . . 6
⊢ (𝜑 → (𝑄 + 0) = 𝑄) |
178 | 176, 177 | syl5req 2669 |
. . . . 5
⊢ (𝜑 → 𝑄 = (𝑄 + (#‘∅))) |
179 | 98, 100, 36, 104, 173, 174, 178 | splval2 13508 |
. . . 4
⊢ (𝜑 → ((𝑆‘𝐶) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉) = ((((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉))) |
180 | | elfzuzb 12336 |
. . . . . . . . . . . . . 14
⊢ (𝑄 ∈ (0...(𝑄 + 2)) ↔ (𝑄 ∈ (ℤ≥‘0)
∧ (𝑄 + 2) ∈
(ℤ≥‘𝑄))) |
181 | 16, 111, 180 | sylanbrc 698 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∈ (0...(𝑄 + 2))) |
182 | | elfzuzb 12336 |
. . . . . . . . . . . . . 14
⊢ ((𝑄 + 2) ∈ (0...𝑃) ↔ ((𝑄 + 2) ∈
(ℤ≥‘0) ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2)))) |
183 | 43, 47, 182 | sylanbrc 698 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄 + 2) ∈ (0...𝑃)) |
184 | | ccatswrd 13456 |
. . . . . . . . . . . . 13
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) = ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) |
185 | 34, 181, 183, 44, 184 | syl13anc 1328 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) = ((𝐴‘𝐾) substr 〈𝑄, 𝑃〉)) |
186 | 185 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)))) |
187 | | swrdcl 13419 |
. . . . . . . . . . . . 13
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) →
((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ∈ Word (𝐼 ×
2𝑜)) |
188 | 34, 187 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ∈ Word (𝐼 ×
2𝑜)) |
189 | | swrdcl 13419 |
. . . . . . . . . . . . 13
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) →
((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ∈ Word (𝐼 ×
2𝑜)) |
190 | 34, 189 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ∈ Word (𝐼 ×
2𝑜)) |
191 | | ccatass 13371 |
. . . . . . . . . . . 12
⊢ ((((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ∈ Word (𝐼 × 2𝑜) ∧
((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ∈ Word (𝐼 × 2𝑜) ∧
(〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 × 2𝑜)) →
((((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))))) |
192 | 188, 190,
146, 191 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))))) |
193 | 167 | simprd 479 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈𝑄, 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
194 | 186, 192,
193 | 3eqtr3d 2664 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)))) = (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
195 | | ccatcl 13359 |
. . . . . . . . . . . 12
⊢ ((((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ∈ Word (𝐼 × 2𝑜) ∧
(〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 × 2𝑜)) →
(((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) ∈ Word (𝐼 ×
2𝑜)) |
196 | 190, 146,
195 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) ∈ Word (𝐼 ×
2𝑜)) |
197 | | swrdlen 13423 |
. . . . . . . . . . . . . 14
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(#‘(𝐴‘𝐾)))) → (#‘((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = ((𝑄 + 2) − 𝑄)) |
198 | 34, 181, 51, 197 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (#‘((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = ((𝑄 + 2) − 𝑄)) |
199 | | pncan2 10288 |
. . . . . . . . . . . . . 14
⊢ ((𝑄 ∈ ℂ ∧ 2 ∈
ℂ) → ((𝑄 + 2)
− 𝑄) =
2) |
200 | 63, 70, 199 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄 + 2) − 𝑄) = 2) |
201 | 198, 200 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ (𝜑 → (#‘((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = 2) |
202 | | s2len 13634 |
. . . . . . . . . . . 12
⊢
(#‘〈“𝑉(𝑀‘𝑉)”〉) = 2 |
203 | 201, 202 | syl6eqr 2674 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = (#‘〈“𝑉(𝑀‘𝑉)”〉)) |
204 | | ccatopth 13470 |
. . . . . . . . . . 11
⊢
(((((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ∈ Word (𝐼 × 2𝑜) ∧
(((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) ∈ Word (𝐼 × 2𝑜)) ∧
(〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 × 2𝑜)
∧ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2𝑜)) ∧
(#‘((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = (#‘〈“𝑉(𝑀‘𝑉)”〉)) → ((((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)))) = (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) ↔ (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) = 〈“𝑉(𝑀‘𝑉)”〉 ∧ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)))) |
205 | 188, 196,
104, 150, 203, 204 | syl221anc 1337 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) ++ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)))) = (〈“𝑉(𝑀‘𝑉)”〉 ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) ↔ (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) = 〈“𝑉(𝑀‘𝑉)”〉 ∧ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)))) |
206 | 194, 205 | mpbid 222 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) = 〈“𝑉(𝑀‘𝑉)”〉 ∧ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
207 | 206 | simpld 475 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉) = 〈“𝑉(𝑀‘𝑉)”〉) |
208 | 207 | oveq2d 6666 |
. . . . . . 7
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = (((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉)) |
209 | | ccatswrd 13456 |
. . . . . . . 8
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (0
∈ (0...𝑄) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(#‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = ((𝐴‘𝐾) substr 〈0, (𝑄 + 2)〉)) |
210 | 34, 106, 181, 51, 209 | syl13anc 1328 |
. . . . . . 7
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈𝑄, (𝑄 + 2)〉)) = ((𝐴‘𝐾) substr 〈0, (𝑄 + 2)〉)) |
211 | 208, 210 | eqtr3d 2658 |
. . . . . 6
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) = ((𝐴‘𝐾) substr 〈0, (𝑄 + 2)〉)) |
212 | 211 | oveq1d 6665 |
. . . . 5
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (((𝐴‘𝐾) substr 〈0, (𝑄 + 2)〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉))) |
213 | | eluzfz1 12348 |
. . . . . . 7
⊢ ((𝑄 + 2) ∈
(ℤ≥‘0) → 0 ∈ (0...(𝑄 + 2))) |
214 | 43, 213 | syl 17 |
. . . . . 6
⊢ (𝜑 → 0 ∈ (0...(𝑄 + 2))) |
215 | | ccatswrd 13456 |
. . . . . 6
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (0
∈ (0...(𝑄 + 2)) ∧
(𝑄 + 2) ∈
(0...(#‘(𝐴‘𝐾))) ∧ (#‘(𝐴‘𝐾)) ∈ (0...(#‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr 〈0, (𝑄 + 2)〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = ((𝐴‘𝐾) substr 〈0, (#‘(𝐴‘𝐾))〉)) |
216 | 34, 214, 51, 57, 215 | syl13anc 1328 |
. . . . 5
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈0, (𝑄 + 2)〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = ((𝐴‘𝐾) substr 〈0, (#‘(𝐴‘𝐾))〉)) |
217 | | swrdid 13428 |
. . . . . 6
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) →
((𝐴‘𝐾) substr 〈0, (#‘(𝐴‘𝐾))〉) = (𝐴‘𝐾)) |
218 | 34, 217 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈0, (#‘(𝐴‘𝐾))〉) = (𝐴‘𝐾)) |
219 | 212, 216,
218 | 3eqtrd 2660 |
. . . 4
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝐴‘𝐾)) |
220 | 96, 179, 219 | 3eqtrd 2660 |
. . 3
⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) = (𝐴‘𝐾)) |
221 | 2, 3, 4, 5 | efgtf 18135 |
. . . . . . 7
⊢ ((𝑆‘𝐶) ∈ 𝑊 → ((𝑇‘(𝑆‘𝐶)) = (𝑎 ∈ (0...(#‘(𝑆‘𝐶))), 𝑖 ∈ (𝐼 × 2𝑜) ↦
((𝑆‘𝐶) splice 〈𝑎, 𝑎, 〈“𝑖(𝑀‘𝑖)”〉〉)) ∧ (𝑇‘(𝑆‘𝐶)):((0...(#‘(𝑆‘𝐶))) × (𝐼 ×
2𝑜))⟶𝑊)) |
222 | 13, 221 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑇‘(𝑆‘𝐶)) = (𝑎 ∈ (0...(#‘(𝑆‘𝐶))), 𝑖 ∈ (𝐼 × 2𝑜) ↦
((𝑆‘𝐶) splice 〈𝑎, 𝑎, 〈“𝑖(𝑀‘𝑖)”〉〉)) ∧ (𝑇‘(𝑆‘𝐶)):((0...(#‘(𝑆‘𝐶))) × (𝐼 ×
2𝑜))⟶𝑊)) |
223 | 222 | simprd 479 |
. . . . 5
⊢ (𝜑 → (𝑇‘(𝑆‘𝐶)):((0...(#‘(𝑆‘𝐶))) × (𝐼 ×
2𝑜))⟶𝑊) |
224 | | ffn 6045 |
. . . . 5
⊢ ((𝑇‘(𝑆‘𝐶)):((0...(#‘(𝑆‘𝐶))) × (𝐼 ×
2𝑜))⟶𝑊 → (𝑇‘(𝑆‘𝐶)) Fn ((0...(#‘(𝑆‘𝐶))) × (𝐼 ×
2𝑜))) |
225 | 223, 224 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑇‘(𝑆‘𝐶)) Fn ((0...(#‘(𝑆‘𝐶))) × (𝐼 ×
2𝑜))) |
226 | | fnovrn 6809 |
. . . 4
⊢ (((𝑇‘(𝑆‘𝐶)) Fn ((0...(#‘(𝑆‘𝐶))) × (𝐼 × 2𝑜)) ∧ 𝑄 ∈ (0...(#‘(𝑆‘𝐶))) ∧ 𝑉 ∈ (𝐼 × 2𝑜)) →
(𝑄(𝑇‘(𝑆‘𝐶))𝑉) ∈ ran (𝑇‘(𝑆‘𝐶))) |
227 | 225, 93, 94, 226 | syl3anc 1326 |
. . 3
⊢ (𝜑 → (𝑄(𝑇‘(𝑆‘𝐶))𝑉) ∈ ran (𝑇‘(𝑆‘𝐶))) |
228 | 220, 227 | eqeltrrd 2702 |
. 2
⊢ (𝜑 → (𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶))) |
229 | | uztrn 11704 |
. . . . . . 7
⊢ (((𝑃 − 2) ∈
(ℤ≥‘𝑄) ∧ 𝑄 ∈ (ℤ≥‘0))
→ (𝑃 − 2) ∈
(ℤ≥‘0)) |
230 | 89, 16, 229 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (𝑃 − 2) ∈
(ℤ≥‘0)) |
231 | | elfzuzb 12336 |
. . . . . 6
⊢ ((𝑃 − 2) ∈
(0...(#‘(𝑆‘𝐶))) ↔ ((𝑃 − 2) ∈
(ℤ≥‘0) ∧ (#‘(𝑆‘𝐶)) ∈
(ℤ≥‘(𝑃 − 2)))) |
232 | 230, 87, 231 | sylanbrc 698 |
. . . . 5
⊢ (𝜑 → (𝑃 − 2) ∈ (0...(#‘(𝑆‘𝐶)))) |
233 | 2, 3, 4, 5 | efgtval 18136 |
. . . . 5
⊢ (((𝑆‘𝐶) ∈ 𝑊 ∧ (𝑃 − 2) ∈ (0...(#‘(𝑆‘𝐶))) ∧ 𝑈 ∈ (𝐼 × 2𝑜)) →
((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = ((𝑆‘𝐶) splice 〈(𝑃 − 2), (𝑃 − 2), 〈“𝑈(𝑀‘𝑈)”〉〉)) |
234 | 13, 232, 121, 233 | syl3anc 1326 |
. . . 4
⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = ((𝑆‘𝐶) splice 〈(𝑃 − 2), (𝑃 − 2), 〈“𝑈(𝑀‘𝑈)”〉〉)) |
235 | | swrdcl 13419 |
. . . . . 6
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) →
((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉) ∈ Word (𝐼 ×
2𝑜)) |
236 | 30, 235 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉) ∈ Word (𝐼 ×
2𝑜)) |
237 | | swrdcl 13419 |
. . . . . 6
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) →
((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉) ∈ Word (𝐼 ×
2𝑜)) |
238 | 30, 237 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉) ∈ Word (𝐼 ×
2𝑜)) |
239 | | ccatswrd 13456 |
. . . . . . . . . . 11
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) ∧
((𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐴‘𝐾))) ∧ (#‘(𝐴‘𝐾)) ∈ (0...(#‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) |
240 | 34, 183, 44, 57, 239 | syl13anc 1328 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) |
241 | 206 | simprd 479 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) |
242 | | elfzuzb 12336 |
. . . . . . . . . . . . . . . 16
⊢ (𝑄 ∈ (0...(𝑃 − 2)) ↔ (𝑄 ∈ (ℤ≥‘0)
∧ (𝑃 − 2) ∈
(ℤ≥‘𝑄))) |
243 | 16, 89, 242 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑄 ∈ (0...(𝑃 − 2))) |
244 | 2, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27, 44, 14, 121, 94, 129, 135 | efgredlemg 18155 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (#‘(𝐴‘𝐾)) = (#‘(𝐵‘𝐿))) |
245 | 244, 46 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (#‘(𝐵‘𝐿)) ∈
(ℤ≥‘𝑃)) |
246 | | 0le2 11111 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ≤
2 |
247 | 246 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ≤ 2) |
248 | 76 | zred 11482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑃 ∈ ℝ) |
249 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ |
250 | | subge02 10544 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℝ ∧ 2 ∈
ℝ) → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃)) |
251 | 248, 249,
250 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃)) |
252 | 247, 251 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑃 − 2) ≤ 𝑃) |
253 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈
(ℤ≥‘(𝑃 − 2)) ↔ ((𝑃 − 2) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑃 − 2) ≤ 𝑃)) |
254 | 78, 76, 252, 253 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑃 − 2))) |
255 | | uztrn 11704 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘(𝐵‘𝐿)) ∈
(ℤ≥‘𝑃) ∧ 𝑃 ∈ (ℤ≥‘(𝑃 − 2))) →
(#‘(𝐵‘𝐿)) ∈
(ℤ≥‘(𝑃 − 2))) |
256 | 245, 254,
255 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (#‘(𝐵‘𝐿)) ∈
(ℤ≥‘(𝑃 − 2))) |
257 | | elfzuzb 12336 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 − 2) ∈
(0...(#‘(𝐵‘𝐿))) ↔ ((𝑃 − 2) ∈
(ℤ≥‘0) ∧ (#‘(𝐵‘𝐿)) ∈
(ℤ≥‘(𝑃 − 2)))) |
258 | 230, 256,
257 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑃 − 2) ∈ (0...(#‘(𝐵‘𝐿)))) |
259 | | lencl 13324 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) →
(#‘(𝐵‘𝐿)) ∈
ℕ0) |
260 | 30, 259 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (#‘(𝐵‘𝐿)) ∈
ℕ0) |
261 | 260, 54 | syl6eleq 2711 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (#‘(𝐵‘𝐿)) ∈
(ℤ≥‘0)) |
262 | | eluzfz2 12349 |
. . . . . . . . . . . . . . . 16
⊢
((#‘(𝐵‘𝐿)) ∈ (ℤ≥‘0)
→ (#‘(𝐵‘𝐿)) ∈ (0...(#‘(𝐵‘𝐿)))) |
263 | 261, 262 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (#‘(𝐵‘𝐿)) ∈ (0...(#‘(𝐵‘𝐿)))) |
264 | | ccatswrd 13456 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(#‘(𝐵‘𝐿))) ∧ (#‘(𝐵‘𝐿)) ∈ (0...(#‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), (#‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) |
265 | 30, 243, 258, 263, 264 | syl13anc 1328 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), (#‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) |
266 | 241, 265 | eqtr4d 2659 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), (#‘(𝐵‘𝐿))〉))) |
267 | | swrdcl 13419 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) →
((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ∈ Word (𝐼 ×
2𝑜)) |
268 | 30, 267 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ∈ Word (𝐼 ×
2𝑜)) |
269 | | swrdcl 13419 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) →
((𝐵‘𝐿) substr 〈(𝑃 − 2), (#‘(𝐵‘𝐿))〉) ∈ Word (𝐼 ×
2𝑜)) |
270 | 30, 269 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈(𝑃 − 2), (#‘(𝐵‘𝐿))〉) ∈ Word (𝐼 ×
2𝑜)) |
271 | | swrdlen 13423 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐴‘𝐾)))) → (#‘((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) = (𝑃 − (𝑄 + 2))) |
272 | 34, 183, 44, 271 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (#‘((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) = (𝑃 − (𝑄 + 2))) |
273 | | swrdlen 13423 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(#‘(𝐵‘𝐿)))) → (#‘((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) = ((𝑃 − 2) − 𝑄)) |
274 | 30, 243, 258, 273 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (#‘((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) = ((𝑃 − 2) − 𝑄)) |
275 | 80, 63, 71 | sub32d 10424 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑃 − 𝑄) − 2) = ((𝑃 − 2) − 𝑄)) |
276 | 80, 63, 71 | subsub4d 10423 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑃 − 𝑄) − 2) = (𝑃 − (𝑄 + 2))) |
277 | 274, 275,
276 | 3eqtr2d 2662 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (#‘((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) = (𝑃 − (𝑄 + 2))) |
278 | 272, 277 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (#‘((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) = (#‘((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉))) |
279 | | ccatopth 13470 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ∈ Word (𝐼 × 2𝑜) ∧
(〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 × 2𝑜)) ∧
(((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ∈ Word (𝐼 × 2𝑜)
∧ ((𝐵‘𝐿) substr 〈(𝑃 − 2), (#‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2𝑜)) ∧
(#‘((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉)) = (#‘((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉))) → ((((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), (#‘(𝐵‘𝐿))〉)) ↔ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) = ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ∧ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((𝐵‘𝐿) substr 〈(𝑃 − 2), (#‘(𝐵‘𝐿))〉)))) |
280 | 190, 146,
268, 270, 278, 279 | syl221anc 1337 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), (#‘(𝐵‘𝐿))〉)) ↔ (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) = ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ∧ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((𝐵‘𝐿) substr 〈(𝑃 − 2), (#‘(𝐵‘𝐿))〉)))) |
281 | 266, 280 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) = ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ∧ (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((𝐵‘𝐿) substr 〈(𝑃 − 2), (#‘(𝐵‘𝐿))〉))) |
282 | 281 | simpld 475 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) = ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) |
283 | 281 | simprd 479 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((𝐵‘𝐿) substr 〈(𝑃 − 2), (#‘(𝐵‘𝐿))〉)) |
284 | | elfzuzb 12336 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 − 2) ∈ (0...𝑃) ↔ ((𝑃 − 2) ∈
(ℤ≥‘0) ∧ 𝑃 ∈ (ℤ≥‘(𝑃 − 2)))) |
285 | 230, 254,
284 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑃 − 2) ∈ (0...𝑃)) |
286 | | elfzuz 12338 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ (0...(#‘(𝐴‘𝐾))) → 𝑃 ∈
(ℤ≥‘0)) |
287 | 44, 286 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈
(ℤ≥‘0)) |
288 | | elfzuzb 12336 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ (0...(#‘(𝐵‘𝐿))) ↔ (𝑃 ∈ (ℤ≥‘0)
∧ (#‘(𝐵‘𝐿)) ∈
(ℤ≥‘𝑃))) |
289 | 287, 245,
288 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ (0...(#‘(𝐵‘𝐿)))) |
290 | | ccatswrd 13456 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) ∧
((𝑃 − 2) ∈
(0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐵‘𝐿))) ∧ (#‘(𝐵‘𝐿)) ∈ (0...(#‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) substr 〈(𝑃 − 2), (#‘(𝐵‘𝐿))〉)) |
291 | 30, 285, 289, 263, 290 | syl13anc 1328 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) substr 〈(𝑃 − 2), (#‘(𝐵‘𝐿))〉)) |
292 | 283, 291 | eqtr4d 2659 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉))) |
293 | | swrdcl 13419 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) →
((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ∈ Word (𝐼 ×
2𝑜)) |
294 | 30, 293 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ∈ Word (𝐼 ×
2𝑜)) |
295 | | s2len 13634 |
. . . . . . . . . . . . . . 15
⊢
(#‘〈“𝑈(𝑀‘𝑈)”〉) = 2 |
296 | | swrdlen 13423 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐵‘𝐿)))) → (#‘((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉)) = (𝑃 − (𝑃 − 2))) |
297 | 30, 285, 289, 296 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (#‘((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉)) = (𝑃 − (𝑃 − 2))) |
298 | | nncan 10310 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℂ ∧ 2 ∈
ℂ) → (𝑃 −
(𝑃 − 2)) =
2) |
299 | 80, 70, 298 | sylancl 694 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃 − (𝑃 − 2)) = 2) |
300 | 297, 299 | eqtr2d 2657 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 = (#‘((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉))) |
301 | 295, 300 | syl5eq 2668 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(#‘〈“𝑈(𝑀‘𝑈)”〉) = (#‘((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉))) |
302 | | ccatopth 13470 |
. . . . . . . . . . . . . 14
⊢
(((〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 × 2𝑜)
∧ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2𝑜)) ∧
(((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ∈ Word (𝐼 × 2𝑜) ∧
((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2𝑜)) ∧
(#‘〈“𝑈(𝑀‘𝑈)”〉) = (#‘((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉))) → ((〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉)) ↔ (〈“𝑈(𝑀‘𝑈)”〉 = ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ∧ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) = ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉)))) |
303 | 124, 126,
294, 238, 301, 302 | syl221anc 1337 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((〈“𝑈(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉)) ↔ (〈“𝑈(𝑀‘𝑈)”〉 = ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ∧ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) = ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉)))) |
304 | 292, 303 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (𝜑 → (〈“𝑈(𝑀‘𝑈)”〉 = ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉) ∧ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) = ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉))) |
305 | 304 | simprd 479 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) = ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉)) |
306 | 282, 305 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈(𝑄 + 2), 𝑃〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉))) |
307 | 240, 306 | eqtr3d 2658 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉) = (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉))) |
308 | 307 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝜑 → (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉)))) |
309 | | ccatass 13371 |
. . . . . . . . 9
⊢ ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ∈ Word (𝐼 × 2𝑜) ∧
((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ∈ Word (𝐼 × 2𝑜)
∧ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2𝑜)) →
((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉)))) |
310 | 32, 268, 238, 309 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ (((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉)))) |
311 | 308, 310 | eqtr4d 2659 |
. . . . . . 7
⊢ (𝜑 → (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉))) |
312 | | ccatswrd 13456 |
. . . . . . . . 9
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (0
∈ (0...𝑄) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(#‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) = ((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉)) |
313 | 30, 106, 243, 258, 312 | syl13anc 1328 |
. . . . . . . 8
⊢ (𝜑 → (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) = ((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉)) |
314 | 313 | oveq1d 6665 |
. . . . . . 7
⊢ (𝜑 → ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (𝑃 − 2)〉)) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉))) |
315 | 17, 311, 314 | 3eqtrd 2660 |
. . . . . 6
⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉))) |
316 | | ccatrid 13370 |
. . . . . . . 8
⊢ (((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉) ∈ Word (𝐼 × 2𝑜)
→ (((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉) ++ ∅) =
((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉)) |
317 | 236, 316 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉) ++ ∅) = ((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉)) |
318 | 317 | oveq1d 6665 |
. . . . . 6
⊢ (𝜑 → ((((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉) ++ ∅) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉))) |
319 | 315, 318 | eqtr4d 2659 |
. . . . 5
⊢ (𝜑 → (𝑆‘𝐶) = ((((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉) ++ ∅) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉))) |
320 | | swrd0len 13422 |
. . . . . . 7
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (𝑃 − 2) ∈
(0...(#‘(𝐵‘𝐿)))) → (#‘((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉)) = (𝑃 − 2)) |
321 | 30, 258, 320 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (#‘((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉)) = (𝑃 − 2)) |
322 | 321 | eqcomd 2628 |
. . . . 5
⊢ (𝜑 → (𝑃 − 2) = (#‘((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉))) |
323 | 175 | oveq2i 6661 |
. . . . . 6
⊢ ((𝑃 − 2) + (#‘∅))
= ((𝑃 − 2) +
0) |
324 | 78 | zcnd 11483 |
. . . . . . 7
⊢ (𝜑 → (𝑃 − 2) ∈ ℂ) |
325 | 324 | addid1d 10236 |
. . . . . 6
⊢ (𝜑 → ((𝑃 − 2) + 0) = (𝑃 − 2)) |
326 | 323, 325 | syl5req 2669 |
. . . . 5
⊢ (𝜑 → (𝑃 − 2) = ((𝑃 − 2) +
(#‘∅))) |
327 | 236, 100,
238, 124, 319, 322, 326 | splval2 13508 |
. . . 4
⊢ (𝜑 → ((𝑆‘𝐶) splice 〈(𝑃 − 2), (𝑃 − 2), 〈“𝑈(𝑀‘𝑈)”〉〉) = ((((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉))) |
328 | 304 | simpld 475 |
. . . . . . . 8
⊢ (𝜑 → 〈“𝑈(𝑀‘𝑈)”〉 = ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉)) |
329 | 328 | oveq2d 6666 |
. . . . . . 7
⊢ (𝜑 → (((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) = (((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉))) |
330 | | eluzfz1 12348 |
. . . . . . . . 9
⊢ ((𝑃 − 2) ∈
(ℤ≥‘0) → 0 ∈ (0...(𝑃 − 2))) |
331 | 230, 330 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ (0...(𝑃 − 2))) |
332 | | ccatswrd 13456 |
. . . . . . . 8
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (0
∈ (0...(𝑃 − 2))
∧ (𝑃 − 2) ∈
(0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉)) = ((𝐵‘𝐿) substr 〈0, 𝑃〉)) |
333 | 30, 331, 285, 289, 332 | syl13anc 1328 |
. . . . . . 7
⊢ (𝜑 → (((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉) ++ ((𝐵‘𝐿) substr 〈(𝑃 − 2), 𝑃〉)) = ((𝐵‘𝐿) substr 〈0, 𝑃〉)) |
334 | 329, 333 | eqtrd 2656 |
. . . . . 6
⊢ (𝜑 → (((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) = ((𝐵‘𝐿) substr 〈0, 𝑃〉)) |
335 | 334 | oveq1d 6665 |
. . . . 5
⊢ (𝜑 → ((((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉)) = (((𝐵‘𝐿) substr 〈0, 𝑃〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉))) |
336 | | eluzfz1 12348 |
. . . . . . 7
⊢ (𝑃 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑃)) |
337 | 287, 336 | syl 17 |
. . . . . 6
⊢ (𝜑 → 0 ∈ (0...𝑃)) |
338 | | ccatswrd 13456 |
. . . . . 6
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (0
∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐵‘𝐿))) ∧ (#‘(𝐵‘𝐿)) ∈ (0...(#‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr 〈0, 𝑃〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) substr 〈0, (#‘(𝐵‘𝐿))〉)) |
339 | 30, 337, 289, 263, 338 | syl13anc 1328 |
. . . . 5
⊢ (𝜑 → (((𝐵‘𝐿) substr 〈0, 𝑃〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) substr 〈0, (#‘(𝐵‘𝐿))〉)) |
340 | | swrdid 13428 |
. . . . . 6
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) →
((𝐵‘𝐿) substr 〈0, (#‘(𝐵‘𝐿))〉) = (𝐵‘𝐿)) |
341 | 30, 340 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈0, (#‘(𝐵‘𝐿))〉) = (𝐵‘𝐿)) |
342 | 335, 339,
341 | 3eqtrd 2660 |
. . . 4
⊢ (𝜑 → ((((𝐵‘𝐿) substr 〈0, (𝑃 − 2)〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐵‘𝐿) substr 〈𝑃, (#‘(𝐵‘𝐿))〉)) = (𝐵‘𝐿)) |
343 | 234, 327,
342 | 3eqtrd 2660 |
. . 3
⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) = (𝐵‘𝐿)) |
344 | | fnovrn 6809 |
. . . 4
⊢ (((𝑇‘(𝑆‘𝐶)) Fn ((0...(#‘(𝑆‘𝐶))) × (𝐼 × 2𝑜)) ∧
(𝑃 − 2) ∈
(0...(#‘(𝑆‘𝐶))) ∧ 𝑈 ∈ (𝐼 × 2𝑜)) →
((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) ∈ ran (𝑇‘(𝑆‘𝐶))) |
345 | 225, 232,
121, 344 | syl3anc 1326 |
. . 3
⊢ (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆‘𝐶))𝑈) ∈ ran (𝑇‘(𝑆‘𝐶))) |
346 | 343, 345 | eqeltrrd 2702 |
. 2
⊢ (𝜑 → (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶))) |
347 | 228, 346 | jca 554 |
1
⊢ (𝜑 → ((𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶)) ∧ (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶)))) |