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