Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  efgredleme Structured version   Visualization version   GIF version

Theorem efgredleme 17979
 Description: Lemma for efgred 17984. (Contributed by Mario Carneiro, 1-Oct-2015.)
Hypotheses
Ref Expression
efgval.w 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
efgval.r = ( ~FG𝐼)
efgval2.m 𝑀 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)
efgval2.t 𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 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 (𝜑𝑈 ∈ (𝐼 × 2𝑜))
efgredlemb.v (𝜑𝑉 ∈ (𝐼 × 2𝑜))
efgredlemb.6 (𝜑 → (𝑆𝐴) = (𝑃(𝑇‘(𝐴𝐾))𝑈))
efgredlemb.7 (𝜑 → (𝑆𝐵) = (𝑄(𝑇‘(𝐵𝐿))𝑉))
efgredlemb.8 (𝜑 → ¬ (𝐴𝐾) = (𝐵𝐿))
efgredlemd.9 (𝜑𝑃 ∈ (ℤ‘(𝑄 + 2)))
efgredlemd.c (𝜑𝐶 ∈ dom 𝑆)
efgredlemd.sc (𝜑 → (𝑆𝐶) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)))
Assertion
Ref Expression
efgredleme (𝜑 → ((𝐴𝐾) ∈ ran (𝑇‘(𝑆𝐶)) ∧ (𝐵𝐿) ∈ ran (𝑇‘(𝑆𝐶))))
Distinct variable groups:   𝑎,𝑏,𝐴   𝑦,𝑎,𝑧,𝑏   𝐿,𝑎,𝑏   𝐾,𝑎,𝑏   𝑡,𝑛,𝑣,𝑤,𝑦,𝑧,𝑃   𝑚,𝑎,𝑛,𝑡,𝑣,𝑤,𝑥,𝑀,𝑏   𝑈,𝑛,𝑣,𝑤,𝑦,𝑧   𝑘,𝑎,𝑇,𝑏,𝑚,𝑡,𝑥   𝑛,𝑉,𝑣,𝑤,𝑦,𝑧   𝑄,𝑛,𝑡,𝑣,𝑤,𝑦,𝑧   𝑊,𝑎,𝑏   𝑘,𝑛,𝑣,𝑤,𝑦,𝑧,𝑊,𝑚,𝑡,𝑥   ,𝑎,𝑏,𝑚,𝑡,𝑥,𝑦,𝑧   𝐵,𝑎,𝑏   𝐶,𝑎,𝑏,𝑘,𝑚,𝑛,𝑡,𝑣,𝑤,𝑥,𝑦,𝑧   𝑆,𝑎,𝑏   𝐼,𝑎,𝑏,𝑚,𝑛,𝑡,𝑣,𝑤,𝑥,𝑦,𝑧   𝐷,𝑎,𝑏,𝑚,𝑡
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛,𝑎,𝑏)   𝐴(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐵(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐷(𝑥,𝑦,𝑧,𝑤,𝑣,𝑘,𝑛)   𝑃(𝑥,𝑘,𝑚,𝑎,𝑏)   𝑄(𝑥,𝑘,𝑚,𝑎,𝑏)   (𝑤,𝑣,𝑘,𝑛)   𝑆(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝑇(𝑦,𝑧,𝑤,𝑣,𝑛)   𝑈(𝑥,𝑡,𝑘,𝑚,𝑎,𝑏)   𝐼(𝑘)   𝐾(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐿(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝑀(𝑦,𝑧,𝑘)   𝑉(𝑥,𝑡,𝑘,𝑚,𝑎,𝑏)

Proof of Theorem efgredleme
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 efgredlemd.c . . . . . 6 (𝜑𝐶 ∈ dom 𝑆)
2 efgval.w . . . . . . . . 9 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
3 efgval.r . . . . . . . . 9 = ( ~FG𝐼)
4 efgval2.m . . . . . . . . 9 𝑀 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)
5 efgval2.t . . . . . . . . 9 𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀𝑤)”⟩⟩)))
6 efgred.d . . . . . . . . 9 𝐷 = (𝑊 𝑥𝑊 ran (𝑇𝑥))
7 efgred.s . . . . . . . . 9 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1)))
82, 3, 4, 5, 6, 7efgsf 17965 . . . . . . . 8 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
98fdmi 5965 . . . . . . . . 9 dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
109feq2i 5950 . . . . . . . 8 (𝑆:dom 𝑆𝑊𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊)
118, 10mpbir 220 . . . . . . 7 𝑆:dom 𝑆𝑊
1211ffvelrni 6266 . . . . . 6 (𝐶 ∈ dom 𝑆 → (𝑆𝐶) ∈ 𝑊)
131, 12syl 17 . . . . 5 (𝜑 → (𝑆𝐶) ∈ 𝑊)
14 efgredlemb.q . . . . . . 7 (𝜑𝑄 ∈ (0...(#‘(𝐵𝐿))))
15 elfzuz 12209 . . . . . . 7 (𝑄 ∈ (0...(#‘(𝐵𝐿))) → 𝑄 ∈ (ℤ‘0))
1614, 15syl 17 . . . . . 6 (𝜑𝑄 ∈ (ℤ‘0))
17 efgredlemd.sc . . . . . . . . . 10 (𝜑 → (𝑆𝐶) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)))
1817fveq2d 6107 . . . . . . . . 9 (𝜑 → (#‘(𝑆𝐶)) = (#‘(((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩))))
19 fviss 6166 . . . . . . . . . . . . 13 ( I ‘Word (𝐼 × 2𝑜)) ⊆ Word (𝐼 × 2𝑜)
202, 19eqsstri 3598 . . . . . . . . . . . 12 𝑊 ⊆ Word (𝐼 × 2𝑜)
21 efgredlem.1 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑎 ∈ dom 𝑆𝑏 ∈ dom 𝑆((#‘(𝑆𝑎)) < (#‘(𝑆𝐴)) → ((𝑆𝑎) = (𝑆𝑏) → (𝑎‘0) = (𝑏‘0))))
22 efgredlem.2 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ dom 𝑆)
23 efgredlem.3 . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ dom 𝑆)
24 efgredlem.4 . . . . . . . . . . . . . 14 (𝜑 → (𝑆𝐴) = (𝑆𝐵))
25 efgredlem.5 . . . . . . . . . . . . . 14 (𝜑 → ¬ (𝐴‘0) = (𝐵‘0))
26 efgredlemb.k . . . . . . . . . . . . . 14 𝐾 = (((#‘𝐴) − 1) − 1)
27 efgredlemb.l . . . . . . . . . . . . . 14 𝐿 = (((#‘𝐵) − 1) − 1)
282, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27efgredlemf 17977 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐾) ∈ 𝑊 ∧ (𝐵𝐿) ∈ 𝑊))
2928simprd 478 . . . . . . . . . . . 12 (𝜑 → (𝐵𝐿) ∈ 𝑊)
3020, 29sseldi 3566 . . . . . . . . . . 11 (𝜑 → (𝐵𝐿) ∈ Word (𝐼 × 2𝑜))
31 swrdcl 13271 . . . . . . . . . . 11 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜))
3230, 31syl 17 . . . . . . . . . 10 (𝜑 → ((𝐵𝐿) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜))
3328simpld 474 . . . . . . . . . . . 12 (𝜑 → (𝐴𝐾) ∈ 𝑊)
3420, 33sseldi 3566 . . . . . . . . . . 11 (𝜑 → (𝐴𝐾) ∈ Word (𝐼 × 2𝑜))
35 swrdcl 13271 . . . . . . . . . . 11 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜))
3634, 35syl 17 . . . . . . . . . 10 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜))
37 ccatlen 13213 . . . . . . . . . 10 ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) ∧ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜)) → (#‘(((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩))) = ((#‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) + (#‘((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩))))
3832, 36, 37syl2anc 691 . . . . . . . . 9 (𝜑 → (#‘(((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩))) = ((#‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) + (#‘((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩))))
39 swrd0len 13274 . . . . . . . . . . . 12 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(#‘(𝐵𝐿)))) → (#‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) = 𝑄)
4030, 14, 39syl2anc 691 . . . . . . . . . . 11 (𝜑 → (#‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) = 𝑄)
41 2nn0 11186 . . . . . . . . . . . . . 14 2 ∈ ℕ0
42 uzaddcl 11620 . . . . . . . . . . . . . 14 ((𝑄 ∈ (ℤ‘0) ∧ 2 ∈ ℕ0) → (𝑄 + 2) ∈ (ℤ‘0))
4316, 41, 42sylancl 693 . . . . . . . . . . . . 13 (𝜑 → (𝑄 + 2) ∈ (ℤ‘0))
44 efgredlemb.p . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ (0...(#‘(𝐴𝐾))))
45 elfzuz3 12210 . . . . . . . . . . . . . . 15 (𝑃 ∈ (0...(#‘(𝐴𝐾))) → (#‘(𝐴𝐾)) ∈ (ℤ𝑃))
4644, 45syl 17 . . . . . . . . . . . . . 14 (𝜑 → (#‘(𝐴𝐾)) ∈ (ℤ𝑃))
47 efgredlemd.9 . . . . . . . . . . . . . 14 (𝜑𝑃 ∈ (ℤ‘(𝑄 + 2)))
48 uztrn 11580 . . . . . . . . . . . . . 14 (((#‘(𝐴𝐾)) ∈ (ℤ𝑃) ∧ 𝑃 ∈ (ℤ‘(𝑄 + 2))) → (#‘(𝐴𝐾)) ∈ (ℤ‘(𝑄 + 2)))
4946, 47, 48syl2anc 691 . . . . . . . . . . . . 13 (𝜑 → (#‘(𝐴𝐾)) ∈ (ℤ‘(𝑄 + 2)))
50 elfzuzb 12207 . . . . . . . . . . . . 13 ((𝑄 + 2) ∈ (0...(#‘(𝐴𝐾))) ↔ ((𝑄 + 2) ∈ (ℤ‘0) ∧ (#‘(𝐴𝐾)) ∈ (ℤ‘(𝑄 + 2))))
5143, 49, 50sylanbrc 695 . . . . . . . . . . . 12 (𝜑 → (𝑄 + 2) ∈ (0...(#‘(𝐴𝐾))))
52 lencl 13179 . . . . . . . . . . . . . . 15 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → (#‘(𝐴𝐾)) ∈ ℕ0)
5334, 52syl 17 . . . . . . . . . . . . . 14 (𝜑 → (#‘(𝐴𝐾)) ∈ ℕ0)
54 nn0uz 11598 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
5553, 54syl6eleq 2698 . . . . . . . . . . . . 13 (𝜑 → (#‘(𝐴𝐾)) ∈ (ℤ‘0))
56 eluzfz2 12220 . . . . . . . . . . . . 13 ((#‘(𝐴𝐾)) ∈ (ℤ‘0) → (#‘(𝐴𝐾)) ∈ (0...(#‘(𝐴𝐾))))
5755, 56syl 17 . . . . . . . . . . . 12 (𝜑 → (#‘(𝐴𝐾)) ∈ (0...(#‘(𝐴𝐾))))
58 swrdlen 13275 . . . . . . . . . . . 12 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 + 2) ∈ (0...(#‘(𝐴𝐾))) ∧ (#‘(𝐴𝐾)) ∈ (0...(#‘(𝐴𝐾)))) → (#‘((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = ((#‘(𝐴𝐾)) − (𝑄 + 2)))
5934, 51, 57, 58syl3anc 1318 . . . . . . . . . . 11 (𝜑 → (#‘((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = ((#‘(𝐴𝐾)) − (𝑄 + 2)))
6040, 59oveq12d 6567 . . . . . . . . . 10 (𝜑 → ((#‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) + (#‘((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩))) = (𝑄 + ((#‘(𝐴𝐾)) − (𝑄 + 2))))
61 elfzelz 12213 . . . . . . . . . . . . 13 (𝑄 ∈ (0...(#‘(𝐵𝐿))) → 𝑄 ∈ ℤ)
6214, 61syl 17 . . . . . . . . . . . 12 (𝜑𝑄 ∈ ℤ)
6362zcnd 11359 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℂ)
6453nn0cnd 11230 . . . . . . . . . . 11 (𝜑 → (#‘(𝐴𝐾)) ∈ ℂ)
65 2z 11286 . . . . . . . . . . . . 13 2 ∈ ℤ
66 zaddcl 11294 . . . . . . . . . . . . 13 ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑄 + 2) ∈ ℤ)
6762, 65, 66sylancl 693 . . . . . . . . . . . 12 (𝜑 → (𝑄 + 2) ∈ ℤ)
6867zcnd 11359 . . . . . . . . . . 11 (𝜑 → (𝑄 + 2) ∈ ℂ)
6963, 64, 68addsubassd 10291 . . . . . . . . . 10 (𝜑 → ((𝑄 + (#‘(𝐴𝐾))) − (𝑄 + 2)) = (𝑄 + ((#‘(𝐴𝐾)) − (𝑄 + 2))))
70 2cn 10968 . . . . . . . . . . . 12 2 ∈ ℂ
7170a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℂ)
7263, 64, 71pnpcand 10308 . . . . . . . . . 10 (𝜑 → ((𝑄 + (#‘(𝐴𝐾))) − (𝑄 + 2)) = ((#‘(𝐴𝐾)) − 2))
7360, 69, 723eqtr2d 2650 . . . . . . . . 9 (𝜑 → ((#‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) + (#‘((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩))) = ((#‘(𝐴𝐾)) − 2))
7418, 38, 733eqtrd 2648 . . . . . . . 8 (𝜑 → (#‘(𝑆𝐶)) = ((#‘(𝐴𝐾)) − 2))
75 elfzelz 12213 . . . . . . . . . . 11 (𝑃 ∈ (0...(#‘(𝐴𝐾))) → 𝑃 ∈ ℤ)
7644, 75syl 17 . . . . . . . . . 10 (𝜑𝑃 ∈ ℤ)
77 zsubcl 11296 . . . . . . . . . 10 ((𝑃 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑃 − 2) ∈ ℤ)
7876, 65, 77sylancl 693 . . . . . . . . 9 (𝜑 → (𝑃 − 2) ∈ ℤ)
7965a1i 11 . . . . . . . . 9 (𝜑 → 2 ∈ ℤ)
8076zcnd 11359 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℂ)
81 npcan 10169 . . . . . . . . . . . 12 ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑃 − 2) + 2) = 𝑃)
8280, 70, 81sylancl 693 . . . . . . . . . . 11 (𝜑 → ((𝑃 − 2) + 2) = 𝑃)
8382fveq2d 6107 . . . . . . . . . 10 (𝜑 → (ℤ‘((𝑃 − 2) + 2)) = (ℤ𝑃))
8446, 83eleqtrrd 2691 . . . . . . . . 9 (𝜑 → (#‘(𝐴𝐾)) ∈ (ℤ‘((𝑃 − 2) + 2)))
85 eluzsub 11593 . . . . . . . . 9 (((𝑃 − 2) ∈ ℤ ∧ 2 ∈ ℤ ∧ (#‘(𝐴𝐾)) ∈ (ℤ‘((𝑃 − 2) + 2))) → ((#‘(𝐴𝐾)) − 2) ∈ (ℤ‘(𝑃 − 2)))
8678, 79, 84, 85syl3anc 1318 . . . . . . . 8 (𝜑 → ((#‘(𝐴𝐾)) − 2) ∈ (ℤ‘(𝑃 − 2)))
8774, 86eqeltrd 2688 . . . . . . 7 (𝜑 → (#‘(𝑆𝐶)) ∈ (ℤ‘(𝑃 − 2)))
88 eluzsub 11593 . . . . . . . 8 ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ ∧ 𝑃 ∈ (ℤ‘(𝑄 + 2))) → (𝑃 − 2) ∈ (ℤ𝑄))
8962, 79, 47, 88syl3anc 1318 . . . . . . 7 (𝜑 → (𝑃 − 2) ∈ (ℤ𝑄))
90 uztrn 11580 . . . . . . 7 (((#‘(𝑆𝐶)) ∈ (ℤ‘(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (ℤ𝑄)) → (#‘(𝑆𝐶)) ∈ (ℤ𝑄))
9187, 89, 90syl2anc 691 . . . . . 6 (𝜑 → (#‘(𝑆𝐶)) ∈ (ℤ𝑄))
92 elfzuzb 12207 . . . . . 6 (𝑄 ∈ (0...(#‘(𝑆𝐶))) ↔ (𝑄 ∈ (ℤ‘0) ∧ (#‘(𝑆𝐶)) ∈ (ℤ𝑄)))
9316, 91, 92sylanbrc 695 . . . . 5 (𝜑𝑄 ∈ (0...(#‘(𝑆𝐶))))
94 efgredlemb.v . . . . 5 (𝜑𝑉 ∈ (𝐼 × 2𝑜))
952, 3, 4, 5efgtval 17959 . . . . 5 (((𝑆𝐶) ∈ 𝑊𝑄 ∈ (0...(#‘(𝑆𝐶))) ∧ 𝑉 ∈ (𝐼 × 2𝑜)) → (𝑄(𝑇‘(𝑆𝐶))𝑉) = ((𝑆𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
9613, 93, 94, 95syl3anc 1318 . . . 4 (𝜑 → (𝑄(𝑇‘(𝑆𝐶))𝑉) = ((𝑆𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
97 swrdcl 13271 . . . . . 6 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜))
9834, 97syl 17 . . . . 5 (𝜑 → ((𝐴𝐾) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜))
99 wrd0 13185 . . . . . 6 ∅ ∈ Word (𝐼 × 2𝑜)
10099a1i 11 . . . . 5 (𝜑 → ∅ ∈ Word (𝐼 × 2𝑜))
1014efgmf 17949 . . . . . . . 8 𝑀:(𝐼 × 2𝑜)⟶(𝐼 × 2𝑜)
102101ffvelrni 6266 . . . . . . 7 (𝑉 ∈ (𝐼 × 2𝑜) → (𝑀𝑉) ∈ (𝐼 × 2𝑜))
10394, 102syl 17 . . . . . 6 (𝜑 → (𝑀𝑉) ∈ (𝐼 × 2𝑜))
10494, 103s2cld 13466 . . . . 5 (𝜑 → ⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2𝑜))
105 eluzfz1 12219 . . . . . . . . . . . . . 14 (𝑄 ∈ (ℤ‘0) → 0 ∈ (0...𝑄))
10616, 105syl 17 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ (0...𝑄))
10762zred 11358 . . . . . . . . . . . . . . . . 17 (𝜑𝑄 ∈ ℝ)
108 nn0addge1 11216 . . . . . . . . . . . . . . . . 17 ((𝑄 ∈ ℝ ∧ 2 ∈ ℕ0) → 𝑄 ≤ (𝑄 + 2))
109107, 41, 108sylancl 693 . . . . . . . . . . . . . . . 16 (𝜑𝑄 ≤ (𝑄 + 2))
110 eluz2 11569 . . . . . . . . . . . . . . . 16 ((𝑄 + 2) ∈ (ℤ𝑄) ↔ (𝑄 ∈ ℤ ∧ (𝑄 + 2) ∈ ℤ ∧ 𝑄 ≤ (𝑄 + 2)))
11162, 67, 109, 110syl3anbrc 1239 . . . . . . . . . . . . . . 15 (𝜑 → (𝑄 + 2) ∈ (ℤ𝑄))
112 uztrn 11580 . . . . . . . . . . . . . . 15 ((𝑃 ∈ (ℤ‘(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (ℤ𝑄)) → 𝑃 ∈ (ℤ𝑄))
11347, 111, 112syl2anc 691 . . . . . . . . . . . . . 14 (𝜑𝑃 ∈ (ℤ𝑄))
114 elfzuzb 12207 . . . . . . . . . . . . . 14 (𝑄 ∈ (0...𝑃) ↔ (𝑄 ∈ (ℤ‘0) ∧ 𝑃 ∈ (ℤ𝑄)))
11516, 113, 114sylanbrc 695 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ (0...𝑃))
116 ccatswrd 13308 . . . . . . . . . . . . 13 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...𝑄) ∧ 𝑄 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴𝐾) substr ⟨0, 𝑃⟩))
11734, 106, 115, 44, 116syl13anc 1320 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴𝐾) substr ⟨0, 𝑃⟩))
118117oveq1d 6564 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))))
119 swrdcl 13271 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨0, 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
12034, 119syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨0, 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
121 efgredlemb.u . . . . . . . . . . . . 13 (𝜑𝑈 ∈ (𝐼 × 2𝑜))
122101ffvelrni 6266 . . . . . . . . . . . . . 14 (𝑈 ∈ (𝐼 × 2𝑜) → (𝑀𝑈) ∈ (𝐼 × 2𝑜))
123121, 122syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑀𝑈) ∈ (𝐼 × 2𝑜))
124121, 123s2cld 13466 . . . . . . . . . . . 12 (𝜑 → ⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2𝑜))
125 swrdcl 13271 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜))
12634, 125syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜))
127 ccatass 13224 . . . . . . . . . . . 12 ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ ⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2𝑜) ∧ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜)) → ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = (((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))))
128120, 124, 126, 127syl3anc 1318 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = (((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))))
129 efgredlemb.6 . . . . . . . . . . . . 13 (𝜑 → (𝑆𝐴) = (𝑃(𝑇‘(𝐴𝐾))𝑈))
1302, 3, 4, 5efgtval 17959 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ 𝑊𝑃 ∈ (0...(#‘(𝐴𝐾))) ∧ 𝑈 ∈ (𝐼 × 2𝑜)) → (𝑃(𝑇‘(𝐴𝐾))𝑈) = ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩))
13133, 44, 121, 130syl3anc 1318 . . . . . . . . . . . . 13 (𝜑 → (𝑃(𝑇‘(𝐴𝐾))𝑈) = ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩))
132 splval 13353 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ 𝑊 ∧ (𝑃 ∈ (0...(#‘(𝐴𝐾))) ∧ 𝑃 ∈ (0...(#‘(𝐴𝐾))) ∧ ⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2𝑜))) → ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩) = ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))
13333, 44, 44, 124, 132syl13anc 1320 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩) = ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))
134129, 131, 1333eqtrd 2648 . . . . . . . . . . . 12 (𝜑 → (𝑆𝐴) = ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))
135 efgredlemb.7 . . . . . . . . . . . . 13 (𝜑 → (𝑆𝐵) = (𝑄(𝑇‘(𝐵𝐿))𝑉))
1362, 3, 4, 5efgtval 17959 . . . . . . . . . . . . . 14 (((𝐵𝐿) ∈ 𝑊𝑄 ∈ (0...(#‘(𝐵𝐿))) ∧ 𝑉 ∈ (𝐼 × 2𝑜)) → (𝑄(𝑇‘(𝐵𝐿))𝑉) = ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
13729, 14, 94, 136syl3anc 1318 . . . . . . . . . . . . 13 (𝜑 → (𝑄(𝑇‘(𝐵𝐿))𝑉) = ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
138 splval 13353 . . . . . . . . . . . . . 14 (((𝐵𝐿) ∈ 𝑊 ∧ (𝑄 ∈ (0...(#‘(𝐵𝐿))) ∧ 𝑄 ∈ (0...(#‘(𝐵𝐿))) ∧ ⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2𝑜))) → ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)))
13929, 14, 14, 104, 138syl13anc 1320 . . . . . . . . . . . . 13 (𝜑 → ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)))
140135, 137, 1393eqtrd 2648 . . . . . . . . . . . 12 (𝜑 → (𝑆𝐵) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)))
14124, 134, 1403eqtr3d 2652 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)))
142118, 128, 1413eqtr2d 2650 . . . . . . . . . 10 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)))
143 swrdcl 13271 . . . . . . . . . . . 12 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
14434, 143syl 17 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
145 ccatcl 13212 . . . . . . . . . . . 12 ((⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2𝑜) ∧ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜)) → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜))
146124, 126, 145syl2anc 691 . . . . . . . . . . 11 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜))
147 ccatass 13224 . . . . . . . . . . 11 ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) ∧ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜)) → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))))
14898, 144, 146, 147syl3anc 1318 . . . . . . . . . 10 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))))
149 swrdcl 13271 . . . . . . . . . . . 12 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
15030, 149syl 17 . . . . . . . . . . 11 (𝜑 → ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
151 ccatass 13224 . . . . . . . . . . 11 ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) ∧ ⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2𝑜) ∧ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜)) → ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))))
15232, 104, 150, 151syl3anc 1318 . . . . . . . . . 10 (𝜑 → ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))))
153142, 148, 1523eqtr3d 2652 . . . . . . . . 9 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))))
154 ccatcl 13212 . . . . . . . . . . 11 ((((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜)) → (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2𝑜))
155144, 146, 154syl2anc 691 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2𝑜))
156 ccatcl 13212 . . . . . . . . . . 11 ((⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2𝑜) ∧ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜)) → (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)) ∈ Word (𝐼 × 2𝑜))
157104, 150, 156syl2anc 691 . . . . . . . . . 10 (𝜑 → (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)) ∈ Word (𝐼 × 2𝑜))
158 uztrn 11580 . . . . . . . . . . . . . 14 (((#‘(𝐴𝐾)) ∈ (ℤ𝑃) ∧ 𝑃 ∈ (ℤ𝑄)) → (#‘(𝐴𝐾)) ∈ (ℤ𝑄))
15946, 113, 158syl2anc 691 . . . . . . . . . . . . 13 (𝜑 → (#‘(𝐴𝐾)) ∈ (ℤ𝑄))
160 elfzuzb 12207 . . . . . . . . . . . . 13 (𝑄 ∈ (0...(#‘(𝐴𝐾))) ↔ (𝑄 ∈ (ℤ‘0) ∧ (#‘(𝐴𝐾)) ∈ (ℤ𝑄)))
16116, 159, 160sylanbrc 695 . . . . . . . . . . . 12 (𝜑𝑄 ∈ (0...(#‘(𝐴𝐾))))
162 swrd0len 13274 . . . . . . . . . . . 12 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(#‘(𝐴𝐾)))) → (#‘((𝐴𝐾) substr ⟨0, 𝑄⟩)) = 𝑄)
16334, 161, 162syl2anc 691 . . . . . . . . . . 11 (𝜑 → (#‘((𝐴𝐾) substr ⟨0, 𝑄⟩)) = 𝑄)
164163, 40eqtr4d 2647 . . . . . . . . . 10 (𝜑 → (#‘((𝐴𝐾) substr ⟨0, 𝑄⟩)) = (#‘((𝐵𝐿) substr ⟨0, 𝑄⟩)))
165 ccatopth 13322 . . . . . . . . . 10 (((((𝐴𝐾) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) ∧ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2𝑜)) ∧ (((𝐵𝐿) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) ∧ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)) ∈ Word (𝐼 × 2𝑜)) ∧ (#‘((𝐴𝐾) substr ⟨0, 𝑄⟩)) = (#‘((𝐵𝐿) substr ⟨0, 𝑄⟩))) → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))) ↔ (((𝐴𝐾) substr ⟨0, 𝑄⟩) = ((𝐵𝐿) substr ⟨0, 𝑄⟩) ∧ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)))))
16698, 155, 32, 157, 164, 165syl221anc 1329 . . . . . . . . 9 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))) ↔ (((𝐴𝐾) substr ⟨0, 𝑄⟩) = ((𝐵𝐿) substr ⟨0, 𝑄⟩) ∧ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)))))
167153, 166mpbid 221 . . . . . . . 8 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) = ((𝐵𝐿) substr ⟨0, 𝑄⟩) ∧ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))))
168167simpld 474 . . . . . . 7 (𝜑 → ((𝐴𝐾) substr ⟨0, 𝑄⟩) = ((𝐵𝐿) substr ⟨0, 𝑄⟩))
169168oveq1d 6564 . . . . . 6 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)))
170 ccatrid 13223 . . . . . . . 8 (((𝐴𝐾) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ∅) = ((𝐴𝐾) substr ⟨0, 𝑄⟩))
17198, 170syl 17 . . . . . . 7 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ∅) = ((𝐴𝐾) substr ⟨0, 𝑄⟩))
172171oveq1d 6564 . . . . . 6 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ∅) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)))
173169, 172, 173eqtr4rd 2655 . . . . 5 (𝜑 → (𝑆𝐶) = ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ∅) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)))
174163eqcomd 2616 . . . . 5 (𝜑𝑄 = (#‘((𝐴𝐾) substr ⟨0, 𝑄⟩)))
175 hash0 13019 . . . . . . 7 (#‘∅) = 0
176175oveq2i 6560 . . . . . 6 (𝑄 + (#‘∅)) = (𝑄 + 0)
17763addid1d 10115 . . . . . 6 (𝜑 → (𝑄 + 0) = 𝑄)
178176, 177syl5req 2657 . . . . 5 (𝜑𝑄 = (𝑄 + (#‘∅)))
17998, 100, 36, 104, 173, 174, 178splval2 13359 . . . 4 (𝜑 → ((𝑆𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩) = ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)))
180 elfzuzb 12207 . . . . . . . . . . . . . 14 (𝑄 ∈ (0...(𝑄 + 2)) ↔ (𝑄 ∈ (ℤ‘0) ∧ (𝑄 + 2) ∈ (ℤ𝑄)))
18116, 111, 180sylanbrc 695 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ (0...(𝑄 + 2)))
182 elfzuzb 12207 . . . . . . . . . . . . . 14 ((𝑄 + 2) ∈ (0...𝑃) ↔ ((𝑄 + 2) ∈ (ℤ‘0) ∧ 𝑃 ∈ (ℤ‘(𝑄 + 2))))
18343, 47, 182sylanbrc 695 . . . . . . . . . . . . 13 (𝜑 → (𝑄 + 2) ∈ (0...𝑃))
184 ccatswrd 13308 . . . . . . . . . . . . 13 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩))
18534, 181, 183, 44, 184syl13anc 1320 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩))
186185oveq1d 6564 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))))
187 swrdcl 13271 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2𝑜))
18834, 187syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2𝑜))
189 swrdcl 13271 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
19034, 189syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
191 ccatass 13224 . . . . . . . . . . . 12 ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2𝑜) ∧ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜)) → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))))
192188, 190, 146, 191syl3anc 1318 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))))
193167simprd 478 . . . . . . . . . . 11 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)))
194186, 192, 1933eqtr3d 2652 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)))
195 ccatcl 13212 . . . . . . . . . . . 12 ((((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜)) → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2𝑜))
196190, 146, 195syl2anc 691 . . . . . . . . . . 11 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2𝑜))
197 swrdlen 13275 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(#‘(𝐴𝐾)))) → (#‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
19834, 181, 51, 197syl3anc 1318 . . . . . . . . . . . . 13 (𝜑 → (#‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
199 pncan2 10167 . . . . . . . . . . . . . 14 ((𝑄 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑄 + 2) − 𝑄) = 2)
20063, 70, 199sylancl 693 . . . . . . . . . . . . 13 (𝜑 → ((𝑄 + 2) − 𝑄) = 2)
201198, 200eqtrd 2644 . . . . . . . . . . . 12 (𝜑 → (#‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = 2)
202 s2len 13484 . . . . . . . . . . . 12 (#‘⟨“𝑉(𝑀𝑉)”⟩) = 2
203201, 202syl6eqr 2662 . . . . . . . . . . 11 (𝜑 → (#‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (#‘⟨“𝑉(𝑀𝑉)”⟩))
204 ccatopth 13322 . . . . . . . . . . 11 (((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2𝑜) ∧ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2𝑜)) ∧ (⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2𝑜) ∧ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜)) ∧ (#‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (#‘⟨“𝑉(𝑀𝑉)”⟩)) → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)) ↔ (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩ ∧ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))))
205188, 196, 104, 150, 203, 204syl221anc 1329 . . . . . . . . . 10 (𝜑 → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)) ↔ (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩ ∧ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))))
206194, 205mpbid 221 . . . . . . . . 9 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩ ∧ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)))
207206simpld 474 . . . . . . . 8 (𝜑 → ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩)
208207oveq2d 6565 . . . . . . 7 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩))
209 ccatswrd 13308 . . . . . . . 8 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...𝑄) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(#‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩))
21034, 106, 181, 51, 209syl13anc 1320 . . . . . . 7 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩))
211208, 210eqtr3d 2646 . . . . . 6 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) = ((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩))
212211oveq1d 6564 . . . . 5 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = (((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)))
213 eluzfz1 12219 . . . . . . 7 ((𝑄 + 2) ∈ (ℤ‘0) → 0 ∈ (0...(𝑄 + 2)))
21443, 213syl 17 . . . . . 6 (𝜑 → 0 ∈ (0...(𝑄 + 2)))
215 ccatswrd 13308 . . . . . 6 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(#‘(𝐴𝐾))) ∧ (#‘(𝐴𝐾)) ∈ (0...(#‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨0, (#‘(𝐴𝐾))⟩))
21634, 214, 51, 57, 215syl13anc 1320 . . . . 5 (𝜑 → (((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨0, (#‘(𝐴𝐾))⟩))
217 swrdid 13280 . . . . . 6 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨0, (#‘(𝐴𝐾))⟩) = (𝐴𝐾))
21834, 217syl 17 . . . . 5 (𝜑 → ((𝐴𝐾) substr ⟨0, (#‘(𝐴𝐾))⟩) = (𝐴𝐾))
219212, 216, 2183eqtrd 2648 . . . 4 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = (𝐴𝐾))
22096, 179, 2193eqtrd 2648 . . 3 (𝜑 → (𝑄(𝑇‘(𝑆𝐶))𝑉) = (𝐴𝐾))
2212, 3, 4, 5efgtf 17958 . . . . . . 7 ((𝑆𝐶) ∈ 𝑊 → ((𝑇‘(𝑆𝐶)) = (𝑎 ∈ (0...(#‘(𝑆𝐶))), 𝑖 ∈ (𝐼 × 2𝑜) ↦ ((𝑆𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐶)):((0...(#‘(𝑆𝐶))) × (𝐼 × 2𝑜))⟶𝑊))
22213, 221syl 17 . . . . . 6 (𝜑 → ((𝑇‘(𝑆𝐶)) = (𝑎 ∈ (0...(#‘(𝑆𝐶))), 𝑖 ∈ (𝐼 × 2𝑜) ↦ ((𝑆𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐶)):((0...(#‘(𝑆𝐶))) × (𝐼 × 2𝑜))⟶𝑊))
223222simprd 478 . . . . 5 (𝜑 → (𝑇‘(𝑆𝐶)):((0...(#‘(𝑆𝐶))) × (𝐼 × 2𝑜))⟶𝑊)
224 ffn 5958 . . . . 5 ((𝑇‘(𝑆𝐶)):((0...(#‘(𝑆𝐶))) × (𝐼 × 2𝑜))⟶𝑊 → (𝑇‘(𝑆𝐶)) Fn ((0...(#‘(𝑆𝐶))) × (𝐼 × 2𝑜)))
225223, 224syl 17 . . . 4 (𝜑 → (𝑇‘(𝑆𝐶)) Fn ((0...(#‘(𝑆𝐶))) × (𝐼 × 2𝑜)))
226 fnovrn 6707 . . . 4 (((𝑇‘(𝑆𝐶)) Fn ((0...(#‘(𝑆𝐶))) × (𝐼 × 2𝑜)) ∧ 𝑄 ∈ (0...(#‘(𝑆𝐶))) ∧ 𝑉 ∈ (𝐼 × 2𝑜)) → (𝑄(𝑇‘(𝑆𝐶))𝑉) ∈ ran (𝑇‘(𝑆𝐶)))
227225, 93, 94, 226syl3anc 1318 . . 3 (𝜑 → (𝑄(𝑇‘(𝑆𝐶))𝑉) ∈ ran (𝑇‘(𝑆𝐶)))
228220, 227eqeltrrd 2689 . 2 (𝜑 → (𝐴𝐾) ∈ ran (𝑇‘(𝑆𝐶)))
229 uztrn 11580 . . . . . . 7 (((𝑃 − 2) ∈ (ℤ𝑄) ∧ 𝑄 ∈ (ℤ‘0)) → (𝑃 − 2) ∈ (ℤ‘0))
23089, 16, 229syl2anc 691 . . . . . 6 (𝜑 → (𝑃 − 2) ∈ (ℤ‘0))
231 elfzuzb 12207 . . . . . 6 ((𝑃 − 2) ∈ (0...(#‘(𝑆𝐶))) ↔ ((𝑃 − 2) ∈ (ℤ‘0) ∧ (#‘(𝑆𝐶)) ∈ (ℤ‘(𝑃 − 2))))
232230, 87, 231sylanbrc 695 . . . . 5 (𝜑 → (𝑃 − 2) ∈ (0...(#‘(𝑆𝐶))))
2332, 3, 4, 5efgtval 17959 . . . . 5 (((𝑆𝐶) ∈ 𝑊 ∧ (𝑃 − 2) ∈ (0...(#‘(𝑆𝐶))) ∧ 𝑈 ∈ (𝐼 × 2𝑜)) → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) = ((𝑆𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀𝑈)”⟩⟩))
23413, 232, 121, 233syl3anc 1318 . . . 4 (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) = ((𝑆𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀𝑈)”⟩⟩))
235 swrdcl 13271 . . . . . 6 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜))
23630, 235syl 17 . . . . 5 (𝜑 → ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜))
237 swrdcl 13271 . . . . . 6 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
23830, 237syl 17 . . . . 5 (𝜑 → ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
239 ccatswrd 13308 . . . . . . . . . . 11 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ ((𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐴𝐾))) ∧ (#‘(𝐴𝐾)) ∈ (0...(#‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩))
24034, 183, 44, 57, 239syl13anc 1320 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩))
241206simprd 478 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))
242 elfzuzb 12207 . . . . . . . . . . . . . . . 16 (𝑄 ∈ (0...(𝑃 − 2)) ↔ (𝑄 ∈ (ℤ‘0) ∧ (𝑃 − 2) ∈ (ℤ𝑄)))
24316, 89, 242sylanbrc 695 . . . . . . . . . . . . . . 15 (𝜑𝑄 ∈ (0...(𝑃 − 2)))
2442, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27, 44, 14, 121, 94, 129, 135efgredlemg 17978 . . . . . . . . . . . . . . . . . 18 (𝜑 → (#‘(𝐴𝐾)) = (#‘(𝐵𝐿)))
245244, 46eqeltrrd 2689 . . . . . . . . . . . . . . . . 17 (𝜑 → (#‘(𝐵𝐿)) ∈ (ℤ𝑃))
246 0le2 10988 . . . . . . . . . . . . . . . . . . . 20 0 ≤ 2
247246a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ≤ 2)
24876zred 11358 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑃 ∈ ℝ)
249 2re 10967 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
250 subge02 10423 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℝ ∧ 2 ∈ ℝ) → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
251248, 249, 250sylancl 693 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
252247, 251mpbid 221 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑃 − 2) ≤ 𝑃)
253 eluz2 11569 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ (ℤ‘(𝑃 − 2)) ↔ ((𝑃 − 2) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑃 − 2) ≤ 𝑃))
25478, 76, 252, 253syl3anbrc 1239 . . . . . . . . . . . . . . . . 17 (𝜑𝑃 ∈ (ℤ‘(𝑃 − 2)))
255 uztrn 11580 . . . . . . . . . . . . . . . . 17 (((#‘(𝐵𝐿)) ∈ (ℤ𝑃) ∧ 𝑃 ∈ (ℤ‘(𝑃 − 2))) → (#‘(𝐵𝐿)) ∈ (ℤ‘(𝑃 − 2)))
256245, 254, 255syl2anc 691 . . . . . . . . . . . . . . . 16 (𝜑 → (#‘(𝐵𝐿)) ∈ (ℤ‘(𝑃 − 2)))
257 elfzuzb 12207 . . . . . . . . . . . . . . . 16 ((𝑃 − 2) ∈ (0...(#‘(𝐵𝐿))) ↔ ((𝑃 − 2) ∈ (ℤ‘0) ∧ (#‘(𝐵𝐿)) ∈ (ℤ‘(𝑃 − 2))))
258230, 256, 257sylanbrc 695 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 − 2) ∈ (0...(#‘(𝐵𝐿))))
259 lencl 13179 . . . . . . . . . . . . . . . . . 18 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → (#‘(𝐵𝐿)) ∈ ℕ0)
26030, 259syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (#‘(𝐵𝐿)) ∈ ℕ0)
261260, 54syl6eleq 2698 . . . . . . . . . . . . . . . 16 (𝜑 → (#‘(𝐵𝐿)) ∈ (ℤ‘0))
262 eluzfz2 12220 . . . . . . . . . . . . . . . 16 ((#‘(𝐵𝐿)) ∈ (ℤ‘0) → (#‘(𝐵𝐿)) ∈ (0...(#‘(𝐵𝐿))))
263261, 262syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (#‘(𝐵𝐿)) ∈ (0...(#‘(𝐵𝐿))))
264 ccatswrd 13308 . . . . . . . . . . . . . . 15 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(#‘(𝐵𝐿))) ∧ (#‘(𝐵𝐿)) ∈ (0...(#‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))
26530, 243, 258, 263, 264syl13anc 1320 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))
266241, 265eqtr4d 2647 . . . . . . . . . . . . 13 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩)))
267 swrdcl 13271 . . . . . . . . . . . . . . 15 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜))
26830, 267syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜))
269 swrdcl 13271 . . . . . . . . . . . . . . 15 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
27030, 269syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
271 swrdlen 13275 . . . . . . . . . . . . . . . 16 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐴𝐾)))) → (#‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
27234, 183, 44, 271syl3anc 1318 . . . . . . . . . . . . . . 15 (𝜑 → (#‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
273 swrdlen 13275 . . . . . . . . . . . . . . . . 17 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(#‘(𝐵𝐿)))) → (#‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
27430, 243, 258, 273syl3anc 1318 . . . . . . . . . . . . . . . 16 (𝜑 → (#‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
27580, 63, 71sub32d 10303 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑃𝑄) − 2) = ((𝑃 − 2) − 𝑄))
27680, 63, 71subsub4d 10302 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑃𝑄) − 2) = (𝑃 − (𝑄 + 2)))
277274, 275, 2763eqtr2d 2650 . . . . . . . . . . . . . . 15 (𝜑 → (#‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = (𝑃 − (𝑄 + 2)))
278272, 277eqtr4d 2647 . . . . . . . . . . . . . 14 (𝜑 → (#‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (#‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)))
279 ccatopth 13322 . . . . . . . . . . . . . 14 (((((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜)) ∧ (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜) ∧ ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜)) ∧ (#‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (#‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩))) → ((((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩)) ↔ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩))))
280190, 146, 268, 270, 278, 279syl221anc 1329 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩)) ↔ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩))))
281266, 280mpbid 221 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩)))
282281simpld 474 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩))
283281simprd 478 . . . . . . . . . . . . . 14 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩))
284 elfzuzb 12207 . . . . . . . . . . . . . . . 16 ((𝑃 − 2) ∈ (0...𝑃) ↔ ((𝑃 − 2) ∈ (ℤ‘0) ∧ 𝑃 ∈ (ℤ‘(𝑃 − 2))))
285230, 254, 284sylanbrc 695 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 − 2) ∈ (0...𝑃))
286 elfzuz 12209 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ (0...(#‘(𝐴𝐾))) → 𝑃 ∈ (ℤ‘0))
28744, 286syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑃 ∈ (ℤ‘0))
288 elfzuzb 12207 . . . . . . . . . . . . . . . 16 (𝑃 ∈ (0...(#‘(𝐵𝐿))) ↔ (𝑃 ∈ (ℤ‘0) ∧ (#‘(𝐵𝐿)) ∈ (ℤ𝑃)))
289287, 245, 288sylanbrc 695 . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ (0...(#‘(𝐵𝐿))))
290 ccatswrd 13308 . . . . . . . . . . . . . . 15 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ ((𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐵𝐿))) ∧ (#‘(𝐵𝐿)) ∈ (0...(#‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩))
29130, 285, 289, 263, 290syl13anc 1320 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩))
292283, 291eqtr4d 2647 . . . . . . . . . . . . 13 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
293 swrdcl 13271 . . . . . . . . . . . . . . 15 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
29430, 293syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
295 s2len 13484 . . . . . . . . . . . . . . 15 (#‘⟨“𝑈(𝑀𝑈)”⟩) = 2
296 swrdlen 13275 . . . . . . . . . . . . . . . . 17 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐵𝐿)))) → (#‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
29730, 285, 289, 296syl3anc 1318 . . . . . . . . . . . . . . . 16 (𝜑 → (#‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
298 nncan 10189 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑃 − (𝑃 − 2)) = 2)
29980, 70, 298sylancl 693 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃 − (𝑃 − 2)) = 2)
300297, 299eqtr2d 2645 . . . . . . . . . . . . . . 15 (𝜑 → 2 = (#‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
301295, 300syl5eq 2656 . . . . . . . . . . . . . 14 (𝜑 → (#‘⟨“𝑈(𝑀𝑈)”⟩) = (#‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
302 ccatopth 13322 . . . . . . . . . . . . . 14 (((⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2𝑜) ∧ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜)) ∧ (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜)) ∧ (#‘⟨“𝑈(𝑀𝑈)”⟩) = (#‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩))) → ((⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) ↔ (⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩))))
303124, 126, 294, 238, 301, 302syl221anc 1329 . . . . . . . . . . . . 13 (𝜑 → ((⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) ↔ (⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩))))
304292, 303mpbid 221 . . . . . . . . . . . 12 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
305304simprd 478 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩))
306282, 305oveq12d 6567 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
307240, 306eqtr3d 2646 . . . . . . . . 9 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
308307oveq2d 6565 . . . . . . . 8 (𝜑 → (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩))))
309 ccatass 13224 . . . . . . . . 9 ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) ∧ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜) ∧ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜)) → ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩))))
31032, 268, 238, 309syl3anc 1318 . . . . . . . 8 (𝜑 → ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩))))
311308, 310eqtr4d 2647 . . . . . . 7 (𝜑 → (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
312 ccatswrd 13308 . . . . . . . . 9 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...𝑄) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(#‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩))
31330, 106, 243, 258, 312syl13anc 1320 . . . . . . . 8 (𝜑 → (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩))
314313oveq1d 6564 . . . . . . 7 (𝜑 → ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
31517, 311, 3143eqtrd 2648 . . . . . 6 (𝜑 → (𝑆𝐶) = (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
316 ccatrid 13223 . . . . . . . 8 (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜) → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ∅) = ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩))
317236, 316syl 17 . . . . . . 7 (𝜑 → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ∅) = ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩))
318317oveq1d 6564 . . . . . 6 (𝜑 → ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ∅) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
319315, 318eqtr4d 2647 . . . . 5 (𝜑 → (𝑆𝐶) = ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ∅) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
320 swrd0len 13274 . . . . . . 7 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (𝑃 − 2) ∈ (0...(#‘(𝐵𝐿)))) → (#‘((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩)) = (𝑃 − 2))
32130, 258, 320syl2anc 691 . . . . . 6 (𝜑 → (#‘((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩)) = (𝑃 − 2))
322321eqcomd 2616 . . . . 5 (𝜑 → (𝑃 − 2) = (#‘((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩)))
323175oveq2i 6560 . . . . . 6 ((𝑃 − 2) + (#‘∅)) = ((𝑃 − 2) + 0)
32478zcnd 11359 . . . . . . 7 (𝜑 → (𝑃 − 2) ∈ ℂ)
325324addid1d 10115 . . . . . 6 (𝜑 → ((𝑃 − 2) + 0) = (𝑃 − 2))
326323, 325syl5req 2657 . . . . 5 (𝜑 → (𝑃 − 2) = ((𝑃 − 2) + (#‘∅)))
327236, 100, 238, 124, 319, 322, 326splval2 13359 . . . 4 (𝜑 → ((𝑆𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀𝑈)”⟩⟩) = ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
328304simpld 474 . . . . . . . 8 (𝜑 → ⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩))
329328oveq2d 6565 . . . . . . 7 (𝜑 → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) = (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
330 eluzfz1 12219 . . . . . . . . 9 ((𝑃 − 2) ∈ (ℤ‘0) → 0 ∈ (0...(𝑃 − 2)))
331230, 330syl 17 . . . . . . . 8 (𝜑 → 0 ∈ (0...(𝑃 − 2)))
332 ccatswrd 13308 . . . . . . . 8 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵𝐿) substr ⟨0, 𝑃⟩))
33330, 331, 285, 289, 332syl13anc 1320 . . . . . . 7 (𝜑 → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵𝐿) substr ⟨0, 𝑃⟩))
334329, 333eqtrd 2644 . . . . . 6 (𝜑 → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) = ((𝐵𝐿) substr ⟨0, 𝑃⟩))
335334oveq1d 6564 . . . . 5 (𝜑 → ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
336 eluzfz1 12219 . . . . . . 7 (𝑃 ∈ (ℤ‘0) → 0 ∈ (0...𝑃))
337287, 336syl 17 . . . . . 6 (𝜑 → 0 ∈ (0...𝑃))
338 ccatswrd 13308 . . . . . 6 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐵𝐿))) ∧ (#‘(𝐵𝐿)) ∈ (0...(#‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨0, 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨0, (#‘(𝐵𝐿))⟩))
33930, 337, 289, 263, 338syl13anc 1320 . . . . 5 (𝜑 → (((𝐵𝐿) substr ⟨0, 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨0, (#‘(𝐵𝐿))⟩))
340 swrdid 13280 . . . . . 6 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨0, (#‘(𝐵𝐿))⟩) = (𝐵𝐿))
34130, 340syl 17 . . . . 5 (𝜑 → ((𝐵𝐿) substr ⟨0, (#‘(𝐵𝐿))⟩) = (𝐵𝐿))
342335, 339, 3413eqtrd 2648 . . . 4 (𝜑 → ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) = (𝐵𝐿))
343234, 327, 3423eqtrd 2648 . . 3 (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) = (𝐵𝐿))
344 fnovrn 6707 . . . 4 (((𝑇‘(𝑆𝐶)) Fn ((0...(#‘(𝑆𝐶))) × (𝐼 × 2𝑜)) ∧ (𝑃 − 2) ∈ (0...(#‘(𝑆𝐶))) ∧ 𝑈 ∈ (𝐼 × 2𝑜)) → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) ∈ ran (𝑇‘(𝑆𝐶)))
345225, 232, 121, 344syl3anc 1318 . . 3 (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) ∈ ran (𝑇‘(𝑆𝐶)))
346343, 345eqeltrrd 2689 . 2 (𝜑 → (𝐵𝐿) ∈ ran (𝑇‘(𝑆𝐶)))
347228, 346jca 553 1 (𝜑 → ((𝐴𝐾) ∈ ran (𝑇‘(𝑆𝐶)) ∧ (𝐵𝐿) ∈ ran (𝑇‘(𝑆𝐶))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  {crab 2900   ∖ cdif 3537  ∅c0 3874  {csn 4125  ⟨cop 4131  ⟨cotp 4133  ∪ ciun 4455   class class class wbr 4583   ↦ cmpt 4643   I cid 4948   × cxp 5036  dom cdm 5038  ran crn 5039   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  1𝑜c1o 7440  2𝑜c2o 7441  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   < clt 9953   ≤ cle 9954   − cmin 10145  2c2 10947  ℕ0cn0 11169  ℤcz 11254  ℤ≥cuz 11563  ...cfz 12197  ..^cfzo 12334  #chash 12979  Word cword 13146   ++ cconcat 13148   substr csubstr 13150   splice csplice 13151  ⟨“cs2 13437   ~FG cefg 17942 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-ot 4134  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-hash 12980  df-word 13154  df-concat 13156  df-s1 13157  df-substr 13158  df-splice 13159  df-s2 13444 This theorem is referenced by:  efgredlemd  17980
 Copyright terms: Public domain W3C validator