MPE Home 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