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 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 ( 𝑇 ‘ ( 𝑆 ‘ 𝐶 ) ) ) )