This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efgredleme

Description: Lemma for efgred . (Contributed by Mario Carneiro, 1-Oct-2015) (Proof shortened by AV, 15-Oct-2022)

Ref Expression
Hypotheses efgval.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
efgval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
efgval2.m ⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
efgval2.t ⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
efgred.d ⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
efgred.s ⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
efgredlem.1 ⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
efgredlem.2 ⊢ ( 𝜑 → 𝐴 ∈ dom 𝑆 )
efgredlem.3 ⊢ ( 𝜑 → 𝐵 ∈ dom 𝑆 )
efgredlem.4 ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐵 ) )
efgredlem.5 ⊢ ( 𝜑 → ¬ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )
efgredlemb.k ⊢ 𝐾 = ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 )
efgredlemb.l ⊢ 𝐿 = ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 )
efgredlemb.p ⊢ ( 𝜑 → 𝑃 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ) )
efgredlemb.q ⊢ ( 𝜑 → 𝑄 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ) )
efgredlemb.u ⊢ ( 𝜑 → 𝑈 ∈ ( 𝐼 × 2o ) )
efgredlemb.v ⊢ ( 𝜑 → 𝑉 ∈ ( 𝐼 × 2o ) )
efgredlemb.6 ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) = ( 𝑃 ( 𝑇 ‘ ( 𝐴 ‘ 𝐾 ) ) 𝑈 ) )
efgredlemb.7 ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐵 ) = ( 𝑄 ( 𝑇 ‘ ( 𝐵 ‘ 𝐿 ) ) 𝑉 ) )
efgredlemb.8 ⊢ ( 𝜑 → ¬ ( 𝐴 ‘ 𝐾 ) = ( 𝐵 ‘ 𝐿 ) )
efgredlemd.9 ⊢ ( 𝜑 → 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) )
efgredlemd.c ⊢ ( 𝜑 → 𝐶 ∈ dom 𝑆 )
efgredlemd.sc ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐶 ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) )
Assertion efgredleme ( 𝜑 → ( ( 𝐴 ‘ 𝐾 ) ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐶 ) ) ∧ ( 𝐵 ‘ 𝐿 ) ∈ ran ( 𝑇 ‘ ( 𝑆 ‘ 𝐶 ) ) ) )

Proof

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