Metamath Proof Explorer

Theorem efgredlemc

Description: The reduced word that forms the base of the sequence in efgsval is uniquely determined, given the ending representation. (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 ⊢ ( 𝜑 → ¬ ( 𝐴 ‘ 𝐾 ) = ( 𝐵 ‘ 𝐿 ) )
Assertion efgredlemc ( 𝜑 → ( 𝑃 ∈ ( ℤ≥ ‘ 𝑄 ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) )

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 uzp1 ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 𝑄 ) → ( 𝑃 = 𝑄 ∨ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ) )
22 fviss ⊢ ( I ‘ Word ( 𝐼 × 2o ) ) ⊆ Word ( 𝐼 × 2o )
23 1 22 eqsstri ⊢ 𝑊 ⊆ Word ( 𝐼 × 2o )
24 1 2 3 4 5 6 efgsdm ⊢ ( 𝐴 ∈ dom 𝑆 ↔ ( 𝐴 ∈ ( Word 𝑊 ∖ { ∅ } ) ∧ ( 𝐴 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐴 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐴 ‘ ( 𝑖 − 1 ) ) ) ) )
25 24 simp1bi ⊢ ( 𝐴 ∈ dom 𝑆 → 𝐴 ∈ ( Word 𝑊 ∖ { ∅ } ) )
26 8 25 syl ⊢ ( 𝜑 → 𝐴 ∈ ( Word 𝑊 ∖ { ∅ } ) )
27 26 eldifad ⊢ ( 𝜑 → 𝐴 ∈ Word 𝑊 )
28 wrdf ⊢ ( 𝐴 ∈ Word 𝑊 → 𝐴 : ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ⟶ 𝑊 )
29 27 28 syl ⊢ ( 𝜑 → 𝐴 : ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ⟶ 𝑊 )
30 fzossfz ⊢ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ⊆ ( 0 ... ( ( ♯ ‘ 𝐴 ) − 1 ) )
31 1 2 3 4 5 6 7 8 9 10 11 efgredlema ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ ∧ ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ ) )
32 31 simpld ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ )
33 fzo0end ⊢ ( ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ → ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
34 32 33 syl ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
35 12 34 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
36 30 35 sselid ⊢ ( 𝜑 → 𝐾 ∈ ( 0 ... ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
37 lencl ⊢ ( 𝐴 ∈ Word 𝑊 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
38 27 37 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
39 38 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℤ )
40 fzoval ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℤ → ( 0 ..^ ( ♯ ‘ 𝐴 ) ) = ( 0 ... ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
41 39 40 syl ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐴 ) ) = ( 0 ... ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
42 36 41 eleqtrrd ⊢ ( 𝜑 → 𝐾 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
43 29 42 ffvelrnd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐾 ) ∈ 𝑊 )
44 23 43 sselid ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐾 ) ∈ Word ( 𝐼 × 2o ) )
45 lencl ⊢ ( ( 𝐴 ‘ 𝐾 ) ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ∈ ℕ0 )
46 44 45 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ∈ ℕ0 )
47 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
48 46 47 eleqtrdi ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ∈ ( ℤ≥ ‘ 0 ) )
49 eluzfz2 ⊢ ( ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ∈ ( ℤ≥ ‘ 0 ) → ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ) )
50 48 49 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ) )
51 ccatpfx ⊢ ( ( ( 𝐴 ‘ 𝐾 ) ∈ Word ( 𝐼 × 2o ) ∧ 𝑃 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ) ∧ ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ) ) → ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( 𝐴 ‘ 𝐾 ) prefix ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ) )
52 44 14 50 51 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( 𝐴 ‘ 𝐾 ) prefix ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ) )
53 pfxid ⊢ ( ( 𝐴 ‘ 𝐾 ) ∈ Word ( 𝐼 × 2o ) → ( ( 𝐴 ‘ 𝐾 ) prefix ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ) = ( 𝐴 ‘ 𝐾 ) )
54 44 53 syl ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐾 ) prefix ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ) = ( 𝐴 ‘ 𝐾 ) )
55 52 54 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝐴 ‘ 𝐾 ) )
56 1 2 3 4 5 6 efgsdm ⊢ ( 𝐵 ∈ dom 𝑆 ↔ ( 𝐵 ∈ ( Word 𝑊 ∖ { ∅ } ) ∧ ( 𝐵 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ..^ ( ♯ ‘ 𝐵 ) ) ( 𝐵 ‘ 𝑖 ) ∈ ran ( 𝑇 ‘ ( 𝐵 ‘ ( 𝑖 − 1 ) ) ) ) )
57 56 simp1bi ⊢ ( 𝐵 ∈ dom 𝑆 → 𝐵 ∈ ( Word 𝑊 ∖ { ∅ } ) )
58 9 57 syl ⊢ ( 𝜑 → 𝐵 ∈ ( Word 𝑊 ∖ { ∅ } ) )
59 58 eldifad ⊢ ( 𝜑 → 𝐵 ∈ Word 𝑊 )
60 wrdf ⊢ ( 𝐵 ∈ Word 𝑊 → 𝐵 : ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ⟶ 𝑊 )
61 59 60 syl ⊢ ( 𝜑 → 𝐵 : ( 0 ..^ ( ♯ ‘ 𝐵 ) ) ⟶ 𝑊 )
62 fzossfz ⊢ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) ⊆ ( 0 ... ( ( ♯ ‘ 𝐵 ) − 1 ) )
63 31 simprd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ )
64 fzo0end ⊢ ( ( ( ♯ ‘ 𝐵 ) − 1 ) ∈ ℕ → ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
65 63 64 syl ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
66 13 65 eqeltrid ⊢ ( 𝜑 → 𝐿 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
67 62 66 sselid ⊢ ( 𝜑 → 𝐿 ∈ ( 0 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
68 lencl ⊢ ( 𝐵 ∈ Word 𝑊 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
69 59 68 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
70 69 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℤ )
71 fzoval ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℤ → ( 0 ..^ ( ♯ ‘ 𝐵 ) ) = ( 0 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
72 70 71 syl ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐵 ) ) = ( 0 ... ( ( ♯ ‘ 𝐵 ) − 1 ) ) )
73 67 72 eleqtrrd ⊢ ( 𝜑 → 𝐿 ∈ ( 0 ..^ ( ♯ ‘ 𝐵 ) ) )
74 61 73 ffvelrnd ⊢ ( 𝜑 → ( 𝐵 ‘ 𝐿 ) ∈ 𝑊 )
75 23 74 sselid ⊢ ( 𝜑 → ( 𝐵 ‘ 𝐿 ) ∈ Word ( 𝐼 × 2o ) )
76 lencl ⊢ ( ( 𝐵 ‘ 𝐿 ) ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ∈ ℕ0 )
77 75 76 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ∈ ℕ0 )
78 77 47 eleqtrdi ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ∈ ( ℤ≥ ‘ 0 ) )
79 eluzfz2 ⊢ ( ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ∈ ( ℤ≥ ‘ 0 ) → ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ) )
80 78 79 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ) )
81 ccatpfx ⊢ ( ( ( 𝐵 ‘ 𝐿 ) ∈ Word ( 𝐼 × 2o ) ∧ 𝑄 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ) ∧ ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ) ) → ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) = ( ( 𝐵 ‘ 𝐿 ) prefix ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ) )
82 75 15 80 81 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) = ( ( 𝐵 ‘ 𝐿 ) prefix ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ) )
83 pfxid ⊢ ( ( 𝐵 ‘ 𝐿 ) ∈ Word ( 𝐼 × 2o ) → ( ( 𝐵 ‘ 𝐿 ) prefix ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ) = ( 𝐵 ‘ 𝐿 ) )
84 75 83 syl ⊢ ( 𝜑 → ( ( 𝐵 ‘ 𝐿 ) prefix ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ) = ( 𝐵 ‘ 𝐿 ) )
85 82 84 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) = ( 𝐵 ‘ 𝐿 ) )
86 55 85 eqeq12d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) ↔ ( 𝐴 ‘ 𝐾 ) = ( 𝐵 ‘ 𝐿 ) ) )
87 20 86 mtbird ⊢ ( 𝜑 → ¬ ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) )
88 1 2 3 4 efgtval ⊢ ( ( ( 𝐴 ‘ 𝐾 ) ∈ 𝑊 ∧ 𝑃 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ) ∧ 𝑈 ∈ ( 𝐼 × 2o ) ) → ( 𝑃 ( 𝑇 ‘ ( 𝐴 ‘ 𝐾 ) ) 𝑈 ) = ( ( 𝐴 ‘ 𝐾 ) splice ⟨ 𝑃 , 𝑃 , ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ⟩ ) )
89 43 14 16 88 syl3anc ⊢ ( 𝜑 → ( 𝑃 ( 𝑇 ‘ ( 𝐴 ‘ 𝐾 ) ) 𝑈 ) = ( ( 𝐴 ‘ 𝐾 ) splice ⟨ 𝑃 , 𝑃 , ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ⟩ ) )
90 3 efgmf ⊢ 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o )
91 90 ffvelrni ⊢ ( 𝑈 ∈ ( 𝐼 × 2o ) → ( 𝑀 ‘ 𝑈 ) ∈ ( 𝐼 × 2o ) )
92 16 91 syl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑈 ) ∈ ( 𝐼 × 2o ) )
93 16 92 s2cld ⊢ ( 𝜑 → ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ∈ Word ( 𝐼 × 2o ) )
94 splval ⊢ ( ( ( 𝐴 ‘ 𝐾 ) ∈ 𝑊 ∧ ( 𝑃 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ) ∧ 𝑃 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ) ∧ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ‘ 𝐾 ) splice ⟨ 𝑃 , 𝑃 , ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ⟩ ) = ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) )
95 43 14 14 93 94 syl13anc ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐾 ) splice ⟨ 𝑃 , 𝑃 , ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ⟩ ) = ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) )
96 18 89 95 3eqtrd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) = ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) )
97 1 2 3 4 efgtval ⊢ ( ( ( 𝐵 ‘ 𝐿 ) ∈ 𝑊 ∧ 𝑄 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ) ∧ 𝑉 ∈ ( 𝐼 × 2o ) ) → ( 𝑄 ( 𝑇 ‘ ( 𝐵 ‘ 𝐿 ) ) 𝑉 ) = ( ( 𝐵 ‘ 𝐿 ) splice ⟨ 𝑄 , 𝑄 , ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ⟩ ) )
98 74 15 17 97 syl3anc ⊢ ( 𝜑 → ( 𝑄 ( 𝑇 ‘ ( 𝐵 ‘ 𝐿 ) ) 𝑉 ) = ( ( 𝐵 ‘ 𝐿 ) splice ⟨ 𝑄 , 𝑄 , ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ⟩ ) )
99 90 ffvelrni ⊢ ( 𝑉 ∈ ( 𝐼 × 2o ) → ( 𝑀 ‘ 𝑉 ) ∈ ( 𝐼 × 2o ) )
100 17 99 syl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑉 ) ∈ ( 𝐼 × 2o ) )
101 17 100 s2cld ⊢ ( 𝜑 → ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ∈ Word ( 𝐼 × 2o ) )
102 splval ⊢ ( ( ( 𝐵 ‘ 𝐿 ) ∈ 𝑊 ∧ ( 𝑄 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ) ∧ 𝑄 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ) ∧ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ) ) → ( ( 𝐵 ‘ 𝐿 ) splice ⟨ 𝑄 , 𝑄 , ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ⟩ ) = ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) )
103 74 15 15 101 102 syl13anc ⊢ ( 𝜑 → ( ( 𝐵 ‘ 𝐿 ) splice ⟨ 𝑄 , 𝑄 , ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ⟩ ) = ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) )
104 19 98 103 3eqtrd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝐵 ) = ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) )
105 10 96 104 3eqtr3d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) )
106 105 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) )
107 pfxcl ⊢ ( ( 𝐴 ‘ 𝐾 ) ∈ Word ( 𝐼 × 2o ) → ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ∈ Word ( 𝐼 × 2o ) )
108 44 107 syl ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ∈ Word ( 𝐼 × 2o ) )
109 108 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ∈ Word ( 𝐼 × 2o ) )
110 93 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ∈ Word ( 𝐼 × 2o ) )
111 ccatcl ⊢ ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
112 109 110 111 syl2anc ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
113 swrdcl ⊢ ( ( 𝐴 ‘ 𝐾 ) ∈ Word ( 𝐼 × 2o ) → ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ∈ Word ( 𝐼 × 2o ) )
114 44 113 syl ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ∈ Word ( 𝐼 × 2o ) )
115 114 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ∈ Word ( 𝐼 × 2o ) )
116 pfxcl ⊢ ( ( 𝐵 ‘ 𝐿 ) ∈ Word ( 𝐼 × 2o ) → ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ∈ Word ( 𝐼 × 2o ) )
117 75 116 syl ⊢ ( 𝜑 → ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ∈ Word ( 𝐼 × 2o ) )
118 117 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ∈ Word ( 𝐼 × 2o ) )
119 101 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ∈ Word ( 𝐼 × 2o ) )
120 ccatcl ⊢ ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
121 118 119 120 syl2anc ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
122 swrdcl ⊢ ( ( 𝐵 ‘ 𝐿 ) ∈ Word ( 𝐼 × 2o ) → ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ∈ Word ( 𝐼 × 2o ) )
123 75 122 syl ⊢ ( 𝜑 → ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ∈ Word ( 𝐼 × 2o ) )
124 123 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ∈ Word ( 𝐼 × 2o ) )
125 pfxlen ⊢ ( ( ( 𝐴 ‘ 𝐾 ) ∈ Word ( 𝐼 × 2o ) ∧ 𝑃 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ) ) → ( ♯ ‘ ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ) = 𝑃 )
126 44 14 125 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ) = 𝑃 )
127 pfxlen ⊢ ( ( ( 𝐵 ‘ 𝐿 ) ∈ Word ( 𝐼 × 2o ) ∧ 𝑄 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ) ) → ( ♯ ‘ ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ) = 𝑄 )
128 75 15 127 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ) = 𝑄 )
129 126 128 eqeq12d ⊢ ( 𝜑 → ( ( ♯ ‘ ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ) = ( ♯ ‘ ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ) ↔ 𝑃 = 𝑄 ) )
130 129 biimpar ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ♯ ‘ ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ) = ( ♯ ‘ ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ) )
131 s2len ⊢ ( ♯ ‘ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) = 2
132 s2len ⊢ ( ♯ ‘ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) = 2
133 131 132 eqtr4i ⊢ ( ♯ ‘ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) = ( ♯ ‘ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ )
134 133 a1i ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ♯ ‘ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) = ( ♯ ‘ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) )
135 130 134 oveq12d ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ( ♯ ‘ ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ) + ( ♯ ‘ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) ) = ( ( ♯ ‘ ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ) + ( ♯ ‘ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) )
136 ccatlen ⊢ ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( ♯ ‘ ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) ) = ( ( ♯ ‘ ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ) + ( ♯ ‘ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) ) )
137 109 110 136 syl2anc ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ♯ ‘ ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) ) = ( ( ♯ ‘ ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ) + ( ♯ ‘ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) ) )
138 ccatlen ⊢ ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( ♯ ‘ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) = ( ( ♯ ‘ ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ) + ( ♯ ‘ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) )
139 118 119 138 syl2anc ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ♯ ‘ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) = ( ( ♯ ‘ ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ) + ( ♯ ‘ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) )
140 135 137 139 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ♯ ‘ ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) ) = ( ♯ ‘ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) )
141 ccatopth ⊢ ( ( ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) ∈ Word ( 𝐼 × 2o ) ∧ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ∈ Word ( 𝐼 × 2o ) ) ∧ ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ∈ Word ( 𝐼 × 2o ) ∧ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ∈ Word ( 𝐼 × 2o ) ) ∧ ( ♯ ‘ ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) ) = ( ♯ ‘ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) ) → ( ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) ↔ ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ∧ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) = ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) ) )
142 112 115 121 124 140 141 syl221anc ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) ↔ ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ∧ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) = ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) ) )
143 106 142 mpbid ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ∧ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) = ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) )
144 143 simpld ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) )
145 ccatopth ⊢ ( ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ) ∧ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ) ∧ ( ♯ ‘ ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ) = ( ♯ ‘ ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ) ) → ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ↔ ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) = ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ∧ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ = ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) )
146 109 110 118 119 130 145 syl221anc ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ↔ ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) = ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ∧ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ = ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) )
147 144 146 mpbid ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) = ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ∧ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ = ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) )
148 147 simpld ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) = ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) )
149 143 simprd ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) = ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) )
150 148 149 oveq12d ⊢ ( ( 𝜑 ∧ 𝑃 = 𝑄 ) → ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) )
151 87 150 mtand ⊢ ( 𝜑 → ¬ 𝑃 = 𝑄 )
152 151 pm2.21d ⊢ ( 𝜑 → ( 𝑃 = 𝑄 → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) )
153 uzp1 ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) → ( 𝑃 = ( 𝑄 + 1 ) ∨ 𝑃 ∈ ( ℤ≥ ‘ ( ( 𝑄 + 1 ) + 1 ) ) ) )
154 16 s1cld ⊢ ( 𝜑 → ⟨“ 𝑈 ”⟩ ∈ Word ( 𝐼 × 2o ) )
155 ccatcl ⊢ ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑈 ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
156 108 154 155 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
157 92 s1cld ⊢ ( 𝜑 → ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ∈ Word ( 𝐼 × 2o ) )
158 ccatass ⊢ ( ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ∧ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ∈ Word ( 𝐼 × 2o ) ) → ( ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ++ ( ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) ) )
159 156 157 114 158 syl3anc ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ++ ( ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) ) )
160 ccatass ⊢ ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑈 ”⟩ ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ) = ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ( ⟨“ 𝑈 ”⟩ ++ ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ) ) )
161 108 154 157 160 syl3anc ⊢ ( 𝜑 → ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ) = ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ( ⟨“ 𝑈 ”⟩ ++ ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ) ) )
162 df-s2 ⊢ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ = ( ⟨“ 𝑈 ”⟩ ++ ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ )
163 162 oveq2i ⊢ ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) = ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ( ⟨“ 𝑈 ”⟩ ++ ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ) )
164 161 163 eqtr4di ⊢ ( 𝜑 → ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ) = ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) )
165 164 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ( 𝑀 ‘ 𝑈 ) ”⟩ ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) )
166 17 s1cld ⊢ ( 𝜑 → ⟨“ 𝑉 ”⟩ ∈ Word ( 𝐼 × 2o ) )
167 100 s1cld ⊢ ( 𝜑 → ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ∈ Word ( 𝐼 × 2o ) )
168 ccatass ⊢ ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑉 ”⟩ ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ⟨“ 𝑉 ”⟩ ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) )
169 117 166 167 168 syl3anc ⊢ ( 𝜑 → ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ⟨“ 𝑉 ”⟩ ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) )
170 df-s2 ⊢ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ = ( ⟨“ 𝑉 ”⟩ ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ )
171 170 oveq2i ⊢ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ⟨“ 𝑉 ”⟩ ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) )
172 169 171 eqtr4di ⊢ ( 𝜑 → ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) )
173 172 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) = ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ( 𝑀 ‘ 𝑉 ) ”⟩ ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) )
174 105 165 173 3eqtr4d ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) )
175 159 174 eqtr3d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ++ ( ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) ) = ( ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) )
176 175 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ++ ( ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) ) = ( ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) )
177 156 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
178 157 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ∈ Word ( 𝐼 × 2o ) )
179 114 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ∈ Word ( 𝐼 × 2o ) )
180 ccatcl ⊢ ( ( ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ∧ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ∈ Word ( 𝐼 × 2o ) ) → ( ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) ∈ Word ( 𝐼 × 2o ) )
181 178 179 180 syl2anc ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) ∈ Word ( 𝐼 × 2o ) )
182 ccatcl ⊢ ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑉 ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
183 117 166 182 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
184 183 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
185 167 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ∈ Word ( 𝐼 × 2o ) )
186 ccatcl ⊢ ( ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
187 184 185 186 syl2anc ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ∈ Word ( 𝐼 × 2o ) )
188 123 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ∈ Word ( 𝐼 × 2o ) )
189 ccatlen ⊢ ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑉 ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( ♯ ‘ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ) = ( ( ♯ ‘ ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ) + ( ♯ ‘ ⟨“ 𝑉 ”⟩ ) ) )
190 117 166 189 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ) = ( ( ♯ ‘ ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ) + ( ♯ ‘ ⟨“ 𝑉 ”⟩ ) ) )
191 s1len ⊢ ( ♯ ‘ ⟨“ 𝑉 ”⟩ ) = 1
192 191 a1i ⊢ ( 𝜑 → ( ♯ ‘ ⟨“ 𝑉 ”⟩ ) = 1 )
193 128 192 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ) + ( ♯ ‘ ⟨“ 𝑉 ”⟩ ) ) = ( 𝑄 + 1 ) )
194 190 193 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ) = ( 𝑄 + 1 ) )
195 126 194 eqeq12d ⊢ ( 𝜑 → ( ( ♯ ‘ ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ) = ( ♯ ‘ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ) ↔ 𝑃 = ( 𝑄 + 1 ) ) )
196 195 biimpar ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ♯ ‘ ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ) = ( ♯ ‘ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ) )
197 s1len ⊢ ( ♯ ‘ ⟨“ 𝑈 ”⟩ ) = 1
198 s1len ⊢ ( ♯ ‘ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) = 1
199 197 198 eqtr4i ⊢ ( ♯ ‘ ⟨“ 𝑈 ”⟩ ) = ( ♯ ‘ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ )
200 199 a1i ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ♯ ‘ ⟨“ 𝑈 ”⟩ ) = ( ♯ ‘ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) )
201 196 200 oveq12d ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ( ♯ ‘ ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ) + ( ♯ ‘ ⟨“ 𝑈 ”⟩ ) ) = ( ( ♯ ‘ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ) + ( ♯ ‘ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) )
202 108 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ∈ Word ( 𝐼 × 2o ) )
203 154 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ⟨“ 𝑈 ”⟩ ∈ Word ( 𝐼 × 2o ) )
204 ccatlen ⊢ ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑈 ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( ♯ ‘ ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ) = ( ( ♯ ‘ ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ) + ( ♯ ‘ ⟨“ 𝑈 ”⟩ ) ) )
205 202 203 204 syl2anc ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ♯ ‘ ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ) = ( ( ♯ ‘ ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ) + ( ♯ ‘ ⟨“ 𝑈 ”⟩ ) ) )
206 ccatlen ⊢ ( ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( ♯ ‘ ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) = ( ( ♯ ‘ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ) + ( ♯ ‘ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) )
207 184 185 206 syl2anc ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ♯ ‘ ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) = ( ( ♯ ‘ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ) + ( ♯ ‘ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) )
208 201 205 207 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ♯ ‘ ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ) = ( ♯ ‘ ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) )
209 ccatopth ⊢ ( ( ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ∈ Word ( 𝐼 × 2o ) ∧ ( ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) ∈ Word ( 𝐼 × 2o ) ) ∧ ( ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ∈ Word ( 𝐼 × 2o ) ∧ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ∈ Word ( 𝐼 × 2o ) ) ∧ ( ♯ ‘ ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ) = ( ♯ ‘ ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) ) → ( ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ++ ( ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) ) = ( ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) ↔ ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) = ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ∧ ( ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) ) )
210 177 181 187 188 208 209 syl221anc ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) ++ ( ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) ) = ( ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) ↔ ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) = ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ∧ ( ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) ) )
211 176 210 mpbid ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) = ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ∧ ( ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) )
212 211 simpld ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) = ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) )
213 ccatopth ⊢ ( ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑈 ”⟩ ∈ Word ( 𝐼 × 2o ) ) ∧ ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ) ∧ ( ♯ ‘ ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ) = ( ♯ ‘ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ) ) → ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) = ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ↔ ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ∧ ⟨“ 𝑈 ”⟩ = ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) )
214 202 203 184 185 196 213 syl221anc ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ⟨“ 𝑈 ”⟩ ) = ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ↔ ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ∧ ⟨“ 𝑈 ”⟩ = ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) ) )
215 212 214 mpbid ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ∧ ⟨“ 𝑈 ”⟩ = ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ) )
216 215 simpld ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) )
217 216 oveq1d ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) )
218 117 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ∈ Word ( 𝐼 × 2o ) )
219 166 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ⟨“ 𝑉 ”⟩ ∈ Word ( 𝐼 × 2o ) )
220 ccatass ⊢ ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑉 ”⟩ ∈ Word ( 𝐼 × 2o ) ∧ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ∈ Word ( 𝐼 × 2o ) ) → ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ⟨“ 𝑉 ”⟩ ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) ) )
221 218 219 179 220 syl3anc ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ⟨“ 𝑉 ”⟩ ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ⟨“ 𝑉 ”⟩ ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) ) )
222 215 simprd ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ⟨“ 𝑈 ”⟩ = ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ )
223 s111 ⊢ ( ( 𝑈 ∈ ( 𝐼 × 2o ) ∧ ( 𝑀 ‘ 𝑉 ) ∈ ( 𝐼 × 2o ) ) → ( ⟨“ 𝑈 ”⟩ = ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ↔ 𝑈 = ( 𝑀 ‘ 𝑉 ) ) )
224 16 100 223 syl2anc ⊢ ( 𝜑 → ( ⟨“ 𝑈 ”⟩ = ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ↔ 𝑈 = ( 𝑀 ‘ 𝑉 ) ) )
225 224 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ⟨“ 𝑈 ”⟩ = ⟨“ ( 𝑀 ‘ 𝑉 ) ”⟩ ↔ 𝑈 = ( 𝑀 ‘ 𝑉 ) ) )
226 222 225 mpbid ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → 𝑈 = ( 𝑀 ‘ 𝑉 ) )
227 226 fveq2d ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( 𝑀 ‘ 𝑈 ) = ( 𝑀 ‘ ( 𝑀 ‘ 𝑉 ) ) )
228 3 efgmnvl ⊢ ( 𝑉 ∈ ( 𝐼 × 2o ) → ( 𝑀 ‘ ( 𝑀 ‘ 𝑉 ) ) = 𝑉 )
229 17 228 syl ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑀 ‘ 𝑉 ) ) = 𝑉 )
230 229 adantr ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( 𝑀 ‘ ( 𝑀 ‘ 𝑉 ) ) = 𝑉 )
231 227 230 eqtrd ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( 𝑀 ‘ 𝑈 ) = 𝑉 )
232 231 s1eqd ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ = ⟨“ 𝑉 ”⟩ )
233 232 oveq1d ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ⟨“ 𝑉 ”⟩ ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) )
234 211 simprd ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ⟨“ ( 𝑀 ‘ 𝑈 ) ”⟩ ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) )
235 233 234 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ⟨“ 𝑉 ”⟩ ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) )
236 235 oveq2d ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ⟨“ 𝑉 ”⟩ ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) )
237 217 221 236 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑃 = ( 𝑄 + 1 ) ) → ( ( ( 𝐴 ‘ 𝐾 ) prefix 𝑃 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ 𝑃 , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐵 ‘ 𝐿 ) substr ⟨ 𝑄 , ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ⟩ ) ) )
238 87 237 mtand ⊢ ( 𝜑 → ¬ 𝑃 = ( 𝑄 + 1 ) )
239 238 pm2.21d ⊢ ( 𝜑 → ( 𝑃 = ( 𝑄 + 1 ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) )
240 15 elfzelzd ⊢ ( 𝜑 → 𝑄 ∈ ℤ )
241 240 zcnd ⊢ ( 𝜑 → 𝑄 ∈ ℂ )
242 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
243 241 242 242 addassd ⊢ ( 𝜑 → ( ( 𝑄 + 1 ) + 1 ) = ( 𝑄 + ( 1 + 1 ) ) )
244 df-2 ⊢ 2 = ( 1 + 1 )
245 244 oveq2i ⊢ ( 𝑄 + 2 ) = ( 𝑄 + ( 1 + 1 ) )
246 243 245 eqtr4di ⊢ ( 𝜑 → ( ( 𝑄 + 1 ) + 1 ) = ( 𝑄 + 2 ) )
247 246 fveq2d ⊢ ( 𝜑 → ( ℤ≥ ‘ ( ( 𝑄 + 1 ) + 1 ) ) = ( ℤ≥ ‘ ( 𝑄 + 2 ) ) )
248 247 eleq2d ⊢ ( 𝜑 → ( 𝑃 ∈ ( ℤ≥ ‘ ( ( 𝑄 + 1 ) + 1 ) ) ↔ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) )
249 1 2 3 4 5 6 efgsfo ⊢ 𝑆 : dom 𝑆 –onto→ 𝑊
250 swrdcl ⊢ ( ( 𝐴 ‘ 𝐾 ) ∈ Word ( 𝐼 × 2o ) → ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ∈ Word ( 𝐼 × 2o ) )
251 44 250 syl ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ∈ Word ( 𝐼 × 2o ) )
252 ccatcl ⊢ ( ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ∈ Word ( 𝐼 × 2o ) ∧ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ∈ Word ( 𝐼 × 2o ) ) → ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) ∈ Word ( 𝐼 × 2o ) )
253 117 251 252 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) ∈ Word ( 𝐼 × 2o ) )
254 1 efgrcl ⊢ ( ( 𝐴 ‘ 𝐾 ) ∈ 𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )
255 43 254 syl ⊢ ( 𝜑 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )
256 255 simprd ⊢ ( 𝜑 → 𝑊 = Word ( 𝐼 × 2o ) )
257 253 256 eleqtrrd ⊢ ( 𝜑 → ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) ∈ 𝑊 )
258 foelrn ⊢ ( ( 𝑆 : dom 𝑆 –onto→ 𝑊 ∧ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) ∈ 𝑊 ) → ∃ 𝑐 ∈ dom 𝑆 ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) )
259 249 257 258 sylancr ⊢ ( 𝜑 → ∃ 𝑐 ∈ dom 𝑆 ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) )
260 259 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) → ∃ 𝑐 ∈ dom 𝑆 ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) )
261 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) ) ) → ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
262 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) ) ) → 𝐴 ∈ dom 𝑆 )
263 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) ) ) → 𝐵 ∈ dom 𝑆 )
264 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) ) ) → ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐵 ) )
265 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) ) ) → ¬ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )
266 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) ) ) → 𝑃 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ) )
267 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) ) ) → 𝑄 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ) )
268 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) ) ) → 𝑈 ∈ ( 𝐼 × 2o ) )
269 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) ) ) → 𝑉 ∈ ( 𝐼 × 2o ) )
270 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) ) ) → ( 𝑆 ‘ 𝐴 ) = ( 𝑃 ( 𝑇 ‘ ( 𝐴 ‘ 𝐾 ) ) 𝑈 ) )
271 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) ) ) → ( 𝑆 ‘ 𝐵 ) = ( 𝑄 ( 𝑇 ‘ ( 𝐵 ‘ 𝐿 ) ) 𝑉 ) )
272 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) ) ) → ¬ ( 𝐴 ‘ 𝐾 ) = ( 𝐵 ‘ 𝐿 ) )
273 simplr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) ) ) → 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) )
274 simprl ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) ) ) → 𝑐 ∈ dom 𝑆 )
275 simprr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) ) ) → ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) )
276 275 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) ) ) → ( 𝑆 ‘ 𝑐 ) = ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) )
277 1 2 3 4 5 6 261 262 263 264 265 12 13 266 267 268 269 270 271 272 273 274 276 efgredlemd ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ ( ( ( 𝐵 ‘ 𝐿 ) prefix 𝑄 ) ++ ( ( 𝐴 ‘ 𝐾 ) substr ⟨ ( 𝑄 + 2 ) , ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ⟩ ) ) = ( 𝑆 ‘ 𝑐 ) ) ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )
278 260 277 rexlimddv ⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )
279 278 ex ⊢ ( 𝜑 → ( 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 2 ) ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) )
280 248 279 sylbid ⊢ ( 𝜑 → ( 𝑃 ∈ ( ℤ≥ ‘ ( ( 𝑄 + 1 ) + 1 ) ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) )
281 239 280 jaod ⊢ ( 𝜑 → ( ( 𝑃 = ( 𝑄 + 1 ) ∨ 𝑃 ∈ ( ℤ≥ ‘ ( ( 𝑄 + 1 ) + 1 ) ) ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) )
282 153 281 syl5 ⊢ ( 𝜑 → ( 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) )
283 152 282 jaod ⊢ ( 𝜑 → ( ( 𝑃 = 𝑄 ∨ 𝑃 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) )
284 21 283 syl5 ⊢ ( 𝜑 → ( 𝑃 ∈ ( ℤ≥ ‘ 𝑄 ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) )