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

Theorem efgredleme 18072
Description: Lemma for efgred 18077. (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 18058 . . . . . . . 8 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
98fdmi 6011 . . . . . . . . 9 dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
109feq2i 5996 . . . . . . . 8 (𝑆:dom 𝑆𝑊𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊)
118, 10mpbir 221 . . . . . . 7 𝑆:dom 𝑆𝑊
1211ffvelrni 6315 . . . . . 6 (𝐶 ∈ dom 𝑆 → (𝑆𝐶) ∈ 𝑊)
131, 12syl 17 . . . . 5 (𝜑 → (𝑆𝐶) ∈ 𝑊)
14 efgredlemb.q . . . . . . 7 (𝜑𝑄 ∈ (0...(#‘(𝐵𝐿))))
15 elfzuz 12277 . . . . . . 7 (𝑄 ∈ (0...(#‘(𝐵𝐿))) → 𝑄 ∈ (ℤ‘0))
1614, 15syl 17 . . . . . 6 (𝜑𝑄 ∈ (ℤ‘0))
17 efgredlemd.sc . . . . . . . . . 10 (𝜑 → (𝑆𝐶) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)))
1817fveq2d 6154 . . . . . . . . 9 (𝜑 → (#‘(𝑆𝐶)) = (#‘(((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩))))
19 fviss 6214 . . . . . . . . . . . . 13 ( I ‘Word (𝐼 × 2𝑜)) ⊆ Word (𝐼 × 2𝑜)
202, 19eqsstri 3619 . . . . . . . . . . . 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 18070 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐾) ∈ 𝑊 ∧ (𝐵𝐿) ∈ 𝑊))
2928simprd 479 . . . . . . . . . . . 12 (𝜑 → (𝐵𝐿) ∈ 𝑊)
3020, 29sseldi 3586 . . . . . . . . . . 11 (𝜑 → (𝐵𝐿) ∈ Word (𝐼 × 2𝑜))
31 swrdcl 13352 . . . . . . . . . . 11 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜))
3230, 31syl 17 . . . . . . . . . 10 (𝜑 → ((𝐵𝐿) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜))
3328simpld 475 . . . . . . . . . . . 12 (𝜑 → (𝐴𝐾) ∈ 𝑊)
3420, 33sseldi 3586 . . . . . . . . . . 11 (𝜑 → (𝐴𝐾) ∈ Word (𝐼 × 2𝑜))
35 swrdcl 13352 . . . . . . . . . . 11 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜))
3634, 35syl 17 . . . . . . . . . 10 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜))
37 ccatlen 13294 . . . . . . . . . 10 ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) ∧ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜)) → (#‘(((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩))) = ((#‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) + (#‘((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩))))
3832, 36, 37syl2anc 692 . . . . . . . . 9 (𝜑 → (#‘(((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩))) = ((#‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) + (#‘((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩))))
39 swrd0len 13355 . . . . . . . . . . . 12 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(#‘(𝐵𝐿)))) → (#‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) = 𝑄)
4030, 14, 39syl2anc 692 . . . . . . . . . . 11 (𝜑 → (#‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) = 𝑄)
41 2nn0 11254 . . . . . . . . . . . . . 14 2 ∈ ℕ0
42 uzaddcl 11688 . . . . . . . . . . . . . 14 ((𝑄 ∈ (ℤ‘0) ∧ 2 ∈ ℕ0) → (𝑄 + 2) ∈ (ℤ‘0))
4316, 41, 42sylancl 693 . . . . . . . . . . . . 13 (𝜑 → (𝑄 + 2) ∈ (ℤ‘0))
44 efgredlemb.p . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ (0...(#‘(𝐴𝐾))))
45 elfzuz3 12278 . . . . . . . . . . . . . . 15 (𝑃 ∈ (0...(#‘(𝐴𝐾))) → (#‘(𝐴𝐾)) ∈ (ℤ𝑃))
4644, 45syl 17 . . . . . . . . . . . . . 14 (𝜑 → (#‘(𝐴𝐾)) ∈ (ℤ𝑃))
47 efgredlemd.9 . . . . . . . . . . . . . 14 (𝜑𝑃 ∈ (ℤ‘(𝑄 + 2)))
48 uztrn 11648 . . . . . . . . . . . . . 14 (((#‘(𝐴𝐾)) ∈ (ℤ𝑃) ∧ 𝑃 ∈ (ℤ‘(𝑄 + 2))) → (#‘(𝐴𝐾)) ∈ (ℤ‘(𝑄 + 2)))
4946, 47, 48syl2anc 692 . . . . . . . . . . . . 13 (𝜑 → (#‘(𝐴𝐾)) ∈ (ℤ‘(𝑄 + 2)))
50 elfzuzb 12275 . . . . . . . . . . . . 13 ((𝑄 + 2) ∈ (0...(#‘(𝐴𝐾))) ↔ ((𝑄 + 2) ∈ (ℤ‘0) ∧ (#‘(𝐴𝐾)) ∈ (ℤ‘(𝑄 + 2))))
5143, 49, 50sylanbrc 697 . . . . . . . . . . . 12 (𝜑 → (𝑄 + 2) ∈ (0...(#‘(𝐴𝐾))))
52 lencl 13258 . . . . . . . . . . . . . . 15 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → (#‘(𝐴𝐾)) ∈ ℕ0)
5334, 52syl 17 . . . . . . . . . . . . . 14 (𝜑 → (#‘(𝐴𝐾)) ∈ ℕ0)
54 nn0uz 11666 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
5553, 54syl6eleq 2714 . . . . . . . . . . . . 13 (𝜑 → (#‘(𝐴𝐾)) ∈ (ℤ‘0))
56 eluzfz2 12288 . . . . . . . . . . . . 13 ((#‘(𝐴𝐾)) ∈ (ℤ‘0) → (#‘(𝐴𝐾)) ∈ (0...(#‘(𝐴𝐾))))
5755, 56syl 17 . . . . . . . . . . . 12 (𝜑 → (#‘(𝐴𝐾)) ∈ (0...(#‘(𝐴𝐾))))
58 swrdlen 13356 . . . . . . . . . . . 12 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 + 2) ∈ (0...(#‘(𝐴𝐾))) ∧ (#‘(𝐴𝐾)) ∈ (0...(#‘(𝐴𝐾)))) → (#‘((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = ((#‘(𝐴𝐾)) − (𝑄 + 2)))
5934, 51, 57, 58syl3anc 1323 . . . . . . . . . . 11 (𝜑 → (#‘((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = ((#‘(𝐴𝐾)) − (𝑄 + 2)))
6040, 59oveq12d 6623 . . . . . . . . . 10 (𝜑 → ((#‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) + (#‘((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩))) = (𝑄 + ((#‘(𝐴𝐾)) − (𝑄 + 2))))
61 elfzelz 12281 . . . . . . . . . . . . 13 (𝑄 ∈ (0...(#‘(𝐵𝐿))) → 𝑄 ∈ ℤ)
6214, 61syl 17 . . . . . . . . . . . 12 (𝜑𝑄 ∈ ℤ)
6362zcnd 11427 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℂ)
6453nn0cnd 11298 . . . . . . . . . . 11 (𝜑 → (#‘(𝐴𝐾)) ∈ ℂ)
65 2z 11354 . . . . . . . . . . . . 13 2 ∈ ℤ
66 zaddcl 11362 . . . . . . . . . . . . 13 ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑄 + 2) ∈ ℤ)
6762, 65, 66sylancl 693 . . . . . . . . . . . 12 (𝜑 → (𝑄 + 2) ∈ ℤ)
6867zcnd 11427 . . . . . . . . . . 11 (𝜑 → (𝑄 + 2) ∈ ℂ)
6963, 64, 68addsubassd 10357 . . . . . . . . . 10 (𝜑 → ((𝑄 + (#‘(𝐴𝐾))) − (𝑄 + 2)) = (𝑄 + ((#‘(𝐴𝐾)) − (𝑄 + 2))))
70 2cn 11036 . . . . . . . . . . . 12 2 ∈ ℂ
7170a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℂ)
7263, 64, 71pnpcand 10374 . . . . . . . . . 10 (𝜑 → ((𝑄 + (#‘(𝐴𝐾))) − (𝑄 + 2)) = ((#‘(𝐴𝐾)) − 2))
7360, 69, 723eqtr2d 2666 . . . . . . . . 9 (𝜑 → ((#‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) + (#‘((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩))) = ((#‘(𝐴𝐾)) − 2))
7418, 38, 733eqtrd 2664 . . . . . . . 8 (𝜑 → (#‘(𝑆𝐶)) = ((#‘(𝐴𝐾)) − 2))
75 elfzelz 12281 . . . . . . . . . . 11 (𝑃 ∈ (0...(#‘(𝐴𝐾))) → 𝑃 ∈ ℤ)
7644, 75syl 17 . . . . . . . . . 10 (𝜑𝑃 ∈ ℤ)
77 zsubcl 11364 . . . . . . . . . 10 ((𝑃 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑃 − 2) ∈ ℤ)
7876, 65, 77sylancl 693 . . . . . . . . 9 (𝜑 → (𝑃 − 2) ∈ ℤ)
7965a1i 11 . . . . . . . . 9 (𝜑 → 2 ∈ ℤ)
8076zcnd 11427 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℂ)
81 npcan 10235 . . . . . . . . . . . 12 ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑃 − 2) + 2) = 𝑃)
8280, 70, 81sylancl 693 . . . . . . . . . . 11 (𝜑 → ((𝑃 − 2) + 2) = 𝑃)
8382fveq2d 6154 . . . . . . . . . 10 (𝜑 → (ℤ‘((𝑃 − 2) + 2)) = (ℤ𝑃))
8446, 83eleqtrrd 2707 . . . . . . . . 9 (𝜑 → (#‘(𝐴𝐾)) ∈ (ℤ‘((𝑃 − 2) + 2)))
85 eluzsub 11661 . . . . . . . . 9 (((𝑃 − 2) ∈ ℤ ∧ 2 ∈ ℤ ∧ (#‘(𝐴𝐾)) ∈ (ℤ‘((𝑃 − 2) + 2))) → ((#‘(𝐴𝐾)) − 2) ∈ (ℤ‘(𝑃 − 2)))
8678, 79, 84, 85syl3anc 1323 . . . . . . . 8 (𝜑 → ((#‘(𝐴𝐾)) − 2) ∈ (ℤ‘(𝑃 − 2)))
8774, 86eqeltrd 2704 . . . . . . 7 (𝜑 → (#‘(𝑆𝐶)) ∈ (ℤ‘(𝑃 − 2)))
88 eluzsub 11661 . . . . . . . 8 ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ ∧ 𝑃 ∈ (ℤ‘(𝑄 + 2))) → (𝑃 − 2) ∈ (ℤ𝑄))
8962, 79, 47, 88syl3anc 1323 . . . . . . 7 (𝜑 → (𝑃 − 2) ∈ (ℤ𝑄))
90 uztrn 11648 . . . . . . 7 (((#‘(𝑆𝐶)) ∈ (ℤ‘(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (ℤ𝑄)) → (#‘(𝑆𝐶)) ∈ (ℤ𝑄))
9187, 89, 90syl2anc 692 . . . . . 6 (𝜑 → (#‘(𝑆𝐶)) ∈ (ℤ𝑄))
92 elfzuzb 12275 . . . . . 6 (𝑄 ∈ (0...(#‘(𝑆𝐶))) ↔ (𝑄 ∈ (ℤ‘0) ∧ (#‘(𝑆𝐶)) ∈ (ℤ𝑄)))
9316, 91, 92sylanbrc 697 . . . . 5 (𝜑𝑄 ∈ (0...(#‘(𝑆𝐶))))
94 efgredlemb.v . . . . 5 (𝜑𝑉 ∈ (𝐼 × 2𝑜))
952, 3, 4, 5efgtval 18052 . . . . 5 (((𝑆𝐶) ∈ 𝑊𝑄 ∈ (0...(#‘(𝑆𝐶))) ∧ 𝑉 ∈ (𝐼 × 2𝑜)) → (𝑄(𝑇‘(𝑆𝐶))𝑉) = ((𝑆𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
9613, 93, 94, 95syl3anc 1323 . . . 4 (𝜑 → (𝑄(𝑇‘(𝑆𝐶))𝑉) = ((𝑆𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
97 swrdcl 13352 . . . . . 6 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜))
9834, 97syl 17 . . . . 5 (𝜑 → ((𝐴𝐾) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜))
99 wrd0 13264 . . . . . 6 ∅ ∈ Word (𝐼 × 2𝑜)
10099a1i 11 . . . . 5 (𝜑 → ∅ ∈ Word (𝐼 × 2𝑜))
1014efgmf 18042 . . . . . . . 8 𝑀:(𝐼 × 2𝑜)⟶(𝐼 × 2𝑜)
102101ffvelrni 6315 . . . . . . 7 (𝑉 ∈ (𝐼 × 2𝑜) → (𝑀𝑉) ∈ (𝐼 × 2𝑜))
10394, 102syl 17 . . . . . 6 (𝜑 → (𝑀𝑉) ∈ (𝐼 × 2𝑜))
10494, 103s2cld 13547 . . . . 5 (𝜑 → ⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2𝑜))
105 eluzfz1 12287 . . . . . . . . . . . . . 14 (𝑄 ∈ (ℤ‘0) → 0 ∈ (0...𝑄))
10616, 105syl 17 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ (0...𝑄))
10762zred 11426 . . . . . . . . . . . . . . . . 17 (𝜑𝑄 ∈ ℝ)
108 nn0addge1 11284 . . . . . . . . . . . . . . . . 17 ((𝑄 ∈ ℝ ∧ 2 ∈ ℕ0) → 𝑄 ≤ (𝑄 + 2))
109107, 41, 108sylancl 693 . . . . . . . . . . . . . . . 16 (𝜑𝑄 ≤ (𝑄 + 2))
110 eluz2 11637 . . . . . . . . . . . . . . . 16 ((𝑄 + 2) ∈ (ℤ𝑄) ↔ (𝑄 ∈ ℤ ∧ (𝑄 + 2) ∈ ℤ ∧ 𝑄 ≤ (𝑄 + 2)))
11162, 67, 109, 110syl3anbrc 1244 . . . . . . . . . . . . . . 15 (𝜑 → (𝑄 + 2) ∈ (ℤ𝑄))
112 uztrn 11648 . . . . . . . . . . . . . . 15 ((𝑃 ∈ (ℤ‘(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (ℤ𝑄)) → 𝑃 ∈ (ℤ𝑄))
11347, 111, 112syl2anc 692 . . . . . . . . . . . . . 14 (𝜑𝑃 ∈ (ℤ𝑄))
114 elfzuzb 12275 . . . . . . . . . . . . . 14 (𝑄 ∈ (0...𝑃) ↔ (𝑄 ∈ (ℤ‘0) ∧ 𝑃 ∈ (ℤ𝑄)))
11516, 113, 114sylanbrc 697 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ (0...𝑃))
116 ccatswrd 13389 . . . . . . . . . . . . 13 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...𝑄) ∧ 𝑄 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴𝐾) substr ⟨0, 𝑃⟩))
11734, 106, 115, 44, 116syl13anc 1325 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴𝐾) substr ⟨0, 𝑃⟩))
118117oveq1d 6620 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))))
119 swrdcl 13352 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨0, 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
12034, 119syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨0, 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
121 efgredlemb.u . . . . . . . . . . . . 13 (𝜑𝑈 ∈ (𝐼 × 2𝑜))
122101ffvelrni 6315 . . . . . . . . . . . . . 14 (𝑈 ∈ (𝐼 × 2𝑜) → (𝑀𝑈) ∈ (𝐼 × 2𝑜))
123121, 122syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑀𝑈) ∈ (𝐼 × 2𝑜))
124121, 123s2cld 13547 . . . . . . . . . . . 12 (𝜑 → ⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2𝑜))
125 swrdcl 13352 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜))
12634, 125syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜))
127 ccatass 13305 . . . . . . . . . . . 12 ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ ⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2𝑜) ∧ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜)) → ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = (((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))))
128120, 124, 126, 127syl3anc 1323 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = (((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))))
129 efgredlemb.6 . . . . . . . . . . . . 13 (𝜑 → (𝑆𝐴) = (𝑃(𝑇‘(𝐴𝐾))𝑈))
1302, 3, 4, 5efgtval 18052 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ 𝑊𝑃 ∈ (0...(#‘(𝐴𝐾))) ∧ 𝑈 ∈ (𝐼 × 2𝑜)) → (𝑃(𝑇‘(𝐴𝐾))𝑈) = ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩))
13133, 44, 121, 130syl3anc 1323 . . . . . . . . . . . . 13 (𝜑 → (𝑃(𝑇‘(𝐴𝐾))𝑈) = ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩))
132 splval 13434 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ 𝑊 ∧ (𝑃 ∈ (0...(#‘(𝐴𝐾))) ∧ 𝑃 ∈ (0...(#‘(𝐴𝐾))) ∧ ⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2𝑜))) → ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩) = ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))
13333, 44, 44, 124, 132syl13anc 1325 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩) = ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))
134129, 131, 1333eqtrd 2664 . . . . . . . . . . . 12 (𝜑 → (𝑆𝐴) = ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))
135 efgredlemb.7 . . . . . . . . . . . . 13 (𝜑 → (𝑆𝐵) = (𝑄(𝑇‘(𝐵𝐿))𝑉))
1362, 3, 4, 5efgtval 18052 . . . . . . . . . . . . . 14 (((𝐵𝐿) ∈ 𝑊𝑄 ∈ (0...(#‘(𝐵𝐿))) ∧ 𝑉 ∈ (𝐼 × 2𝑜)) → (𝑄(𝑇‘(𝐵𝐿))𝑉) = ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
13729, 14, 94, 136syl3anc 1323 . . . . . . . . . . . . 13 (𝜑 → (𝑄(𝑇‘(𝐵𝐿))𝑉) = ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
138 splval 13434 . . . . . . . . . . . . . 14 (((𝐵𝐿) ∈ 𝑊 ∧ (𝑄 ∈ (0...(#‘(𝐵𝐿))) ∧ 𝑄 ∈ (0...(#‘(𝐵𝐿))) ∧ ⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2𝑜))) → ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)))
13929, 14, 14, 104, 138syl13anc 1325 . . . . . . . . . . . . 13 (𝜑 → ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)))
140135, 137, 1393eqtrd 2664 . . . . . . . . . . . 12 (𝜑 → (𝑆𝐵) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)))
14124, 134, 1403eqtr3d 2668 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)))
142118, 128, 1413eqtr2d 2666 . . . . . . . . . 10 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)))
143 swrdcl 13352 . . . . . . . . . . . 12 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
14434, 143syl 17 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
145 ccatcl 13293 . . . . . . . . . . . 12 ((⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2𝑜) ∧ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜)) → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜))
146124, 126, 145syl2anc 692 . . . . . . . . . . 11 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜))
147 ccatass 13305 . . . . . . . . . . 11 ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) ∧ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜)) → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))))
14898, 144, 146, 147syl3anc 1323 . . . . . . . . . 10 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))))
149 swrdcl 13352 . . . . . . . . . . . 12 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
15030, 149syl 17 . . . . . . . . . . 11 (𝜑 → ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
151 ccatass 13305 . . . . . . . . . . 11 ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) ∧ ⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2𝑜) ∧ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜)) → ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))))
15232, 104, 150, 151syl3anc 1323 . . . . . . . . . 10 (𝜑 → ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))))
153142, 148, 1523eqtr3d 2668 . . . . . . . . 9 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))))
154 ccatcl 13293 . . . . . . . . . . 11 ((((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜)) → (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2𝑜))
155144, 146, 154syl2anc 692 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2𝑜))
156 ccatcl 13293 . . . . . . . . . . 11 ((⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2𝑜) ∧ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜)) → (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)) ∈ Word (𝐼 × 2𝑜))
157104, 150, 156syl2anc 692 . . . . . . . . . 10 (𝜑 → (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)) ∈ Word (𝐼 × 2𝑜))
158 uztrn 11648 . . . . . . . . . . . . . 14 (((#‘(𝐴𝐾)) ∈ (ℤ𝑃) ∧ 𝑃 ∈ (ℤ𝑄)) → (#‘(𝐴𝐾)) ∈ (ℤ𝑄))
15946, 113, 158syl2anc 692 . . . . . . . . . . . . 13 (𝜑 → (#‘(𝐴𝐾)) ∈ (ℤ𝑄))
160 elfzuzb 12275 . . . . . . . . . . . . 13 (𝑄 ∈ (0...(#‘(𝐴𝐾))) ↔ (𝑄 ∈ (ℤ‘0) ∧ (#‘(𝐴𝐾)) ∈ (ℤ𝑄)))
16116, 159, 160sylanbrc 697 . . . . . . . . . . . 12 (𝜑𝑄 ∈ (0...(#‘(𝐴𝐾))))
162 swrd0len 13355 . . . . . . . . . . . 12 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(#‘(𝐴𝐾)))) → (#‘((𝐴𝐾) substr ⟨0, 𝑄⟩)) = 𝑄)
16334, 161, 162syl2anc 692 . . . . . . . . . . 11 (𝜑 → (#‘((𝐴𝐾) substr ⟨0, 𝑄⟩)) = 𝑄)
164163, 40eqtr4d 2663 . . . . . . . . . 10 (𝜑 → (#‘((𝐴𝐾) substr ⟨0, 𝑄⟩)) = (#‘((𝐵𝐿) substr ⟨0, 𝑄⟩)))
165 ccatopth 13403 . . . . . . . . . 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 1334 . . . . . . . . 9 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))) ↔ (((𝐴𝐾) substr ⟨0, 𝑄⟩) = ((𝐵𝐿) substr ⟨0, 𝑄⟩) ∧ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)))))
167153, 166mpbid 222 . . . . . . . 8 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) = ((𝐵𝐿) substr ⟨0, 𝑄⟩) ∧ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))))
168167simpld 475 . . . . . . 7 (𝜑 → ((𝐴𝐾) substr ⟨0, 𝑄⟩) = ((𝐵𝐿) substr ⟨0, 𝑄⟩))
169168oveq1d 6620 . . . . . 6 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)))
170 ccatrid 13304 . . . . . . . 8 (((𝐴𝐾) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ∅) = ((𝐴𝐾) substr ⟨0, 𝑄⟩))
17198, 170syl 17 . . . . . . 7 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ∅) = ((𝐴𝐾) substr ⟨0, 𝑄⟩))
172171oveq1d 6620 . . . . . 6 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ∅) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)))
173169, 172, 173eqtr4rd 2671 . . . . 5 (𝜑 → (𝑆𝐶) = ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ∅) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)))
174163eqcomd 2632 . . . . 5 (𝜑𝑄 = (#‘((𝐴𝐾) substr ⟨0, 𝑄⟩)))
175 hash0 13095 . . . . . . 7 (#‘∅) = 0
176175oveq2i 6616 . . . . . 6 (𝑄 + (#‘∅)) = (𝑄 + 0)
17763addid1d 10181 . . . . . 6 (𝜑 → (𝑄 + 0) = 𝑄)
178176, 177syl5req 2673 . . . . 5 (𝜑𝑄 = (𝑄 + (#‘∅)))
17998, 100, 36, 104, 173, 174, 178splval2 13440 . . . 4 (𝜑 → ((𝑆𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩) = ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)))
180 elfzuzb 12275 . . . . . . . . . . . . . 14 (𝑄 ∈ (0...(𝑄 + 2)) ↔ (𝑄 ∈ (ℤ‘0) ∧ (𝑄 + 2) ∈ (ℤ𝑄)))
18116, 111, 180sylanbrc 697 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ (0...(𝑄 + 2)))
182 elfzuzb 12275 . . . . . . . . . . . . . 14 ((𝑄 + 2) ∈ (0...𝑃) ↔ ((𝑄 + 2) ∈ (ℤ‘0) ∧ 𝑃 ∈ (ℤ‘(𝑄 + 2))))
18343, 47, 182sylanbrc 697 . . . . . . . . . . . . 13 (𝜑 → (𝑄 + 2) ∈ (0...𝑃))
184 ccatswrd 13389 . . . . . . . . . . . . 13 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩))
18534, 181, 183, 44, 184syl13anc 1325 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩))
186185oveq1d 6620 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))))
187 swrdcl 13352 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2𝑜))
18834, 187syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2𝑜))
189 swrdcl 13352 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
19034, 189syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
191 ccatass 13305 . . . . . . . . . . . 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 1323 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))))
193167simprd 479 . . . . . . . . . . 11 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)))
194186, 192, 1933eqtr3d 2668 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)))
195 ccatcl 13293 . . . . . . . . . . . 12 ((((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜)) → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2𝑜))
196190, 146, 195syl2anc 692 . . . . . . . . . . 11 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2𝑜))
197 swrdlen 13356 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(#‘(𝐴𝐾)))) → (#‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
19834, 181, 51, 197syl3anc 1323 . . . . . . . . . . . . 13 (𝜑 → (#‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
199 pncan2 10233 . . . . . . . . . . . . . 14 ((𝑄 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑄 + 2) − 𝑄) = 2)
20063, 70, 199sylancl 693 . . . . . . . . . . . . 13 (𝜑 → ((𝑄 + 2) − 𝑄) = 2)
201198, 200eqtrd 2660 . . . . . . . . . . . 12 (𝜑 → (#‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = 2)
202 s2len 13565 . . . . . . . . . . . 12 (#‘⟨“𝑉(𝑀𝑉)”⟩) = 2
203201, 202syl6eqr 2678 . . . . . . . . . . 11 (𝜑 → (#‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (#‘⟨“𝑉(𝑀𝑉)”⟩))
204 ccatopth 13403 . . . . . . . . . . 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 1334 . . . . . . . . . 10 (𝜑 → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)) ↔ (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩ ∧ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))))
206194, 205mpbid 222 . . . . . . . . 9 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩ ∧ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩)))
207206simpld 475 . . . . . . . 8 (𝜑 → ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩)
208207oveq2d 6621 . . . . . . 7 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩))
209 ccatswrd 13389 . . . . . . . 8 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...𝑄) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(#‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩))
21034, 106, 181, 51, 209syl13anc 1325 . . . . . . 7 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩))
211208, 210eqtr3d 2662 . . . . . 6 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) = ((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩))
212211oveq1d 6620 . . . . 5 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = (((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)))
213 eluzfz1 12287 . . . . . . 7 ((𝑄 + 2) ∈ (ℤ‘0) → 0 ∈ (0...(𝑄 + 2)))
21443, 213syl 17 . . . . . 6 (𝜑 → 0 ∈ (0...(𝑄 + 2)))
215 ccatswrd 13389 . . . . . 6 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(#‘(𝐴𝐾))) ∧ (#‘(𝐴𝐾)) ∈ (0...(#‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨0, (#‘(𝐴𝐾))⟩))
21634, 214, 51, 57, 215syl13anc 1325 . . . . 5 (𝜑 → (((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨0, (#‘(𝐴𝐾))⟩))
217 swrdid 13361 . . . . . 6 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨0, (#‘(𝐴𝐾))⟩) = (𝐴𝐾))
21834, 217syl 17 . . . . 5 (𝜑 → ((𝐴𝐾) substr ⟨0, (#‘(𝐴𝐾))⟩) = (𝐴𝐾))
219212, 216, 2183eqtrd 2664 . . . 4 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = (𝐴𝐾))
22096, 179, 2193eqtrd 2664 . . 3 (𝜑 → (𝑄(𝑇‘(𝑆𝐶))𝑉) = (𝐴𝐾))
2212, 3, 4, 5efgtf 18051 . . . . . . 7 ((𝑆𝐶) ∈ 𝑊 → ((𝑇‘(𝑆𝐶)) = (𝑎 ∈ (0...(#‘(𝑆𝐶))), 𝑖 ∈ (𝐼 × 2𝑜) ↦ ((𝑆𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐶)):((0...(#‘(𝑆𝐶))) × (𝐼 × 2𝑜))⟶𝑊))
22213, 221syl 17 . . . . . 6 (𝜑 → ((𝑇‘(𝑆𝐶)) = (𝑎 ∈ (0...(#‘(𝑆𝐶))), 𝑖 ∈ (𝐼 × 2𝑜) ↦ ((𝑆𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐶)):((0...(#‘(𝑆𝐶))) × (𝐼 × 2𝑜))⟶𝑊))
223222simprd 479 . . . . 5 (𝜑 → (𝑇‘(𝑆𝐶)):((0...(#‘(𝑆𝐶))) × (𝐼 × 2𝑜))⟶𝑊)
224 ffn 6004 . . . . 5 ((𝑇‘(𝑆𝐶)):((0...(#‘(𝑆𝐶))) × (𝐼 × 2𝑜))⟶𝑊 → (𝑇‘(𝑆𝐶)) Fn ((0...(#‘(𝑆𝐶))) × (𝐼 × 2𝑜)))
225223, 224syl 17 . . . 4 (𝜑 → (𝑇‘(𝑆𝐶)) Fn ((0...(#‘(𝑆𝐶))) × (𝐼 × 2𝑜)))
226 fnovrn 6763 . . . 4 (((𝑇‘(𝑆𝐶)) Fn ((0...(#‘(𝑆𝐶))) × (𝐼 × 2𝑜)) ∧ 𝑄 ∈ (0...(#‘(𝑆𝐶))) ∧ 𝑉 ∈ (𝐼 × 2𝑜)) → (𝑄(𝑇‘(𝑆𝐶))𝑉) ∈ ran (𝑇‘(𝑆𝐶)))
227225, 93, 94, 226syl3anc 1323 . . 3 (𝜑 → (𝑄(𝑇‘(𝑆𝐶))𝑉) ∈ ran (𝑇‘(𝑆𝐶)))
228220, 227eqeltrrd 2705 . 2 (𝜑 → (𝐴𝐾) ∈ ran (𝑇‘(𝑆𝐶)))
229 uztrn 11648 . . . . . . 7 (((𝑃 − 2) ∈ (ℤ𝑄) ∧ 𝑄 ∈ (ℤ‘0)) → (𝑃 − 2) ∈ (ℤ‘0))
23089, 16, 229syl2anc 692 . . . . . 6 (𝜑 → (𝑃 − 2) ∈ (ℤ‘0))
231 elfzuzb 12275 . . . . . 6 ((𝑃 − 2) ∈ (0...(#‘(𝑆𝐶))) ↔ ((𝑃 − 2) ∈ (ℤ‘0) ∧ (#‘(𝑆𝐶)) ∈ (ℤ‘(𝑃 − 2))))
232230, 87, 231sylanbrc 697 . . . . 5 (𝜑 → (𝑃 − 2) ∈ (0...(#‘(𝑆𝐶))))
2332, 3, 4, 5efgtval 18052 . . . . 5 (((𝑆𝐶) ∈ 𝑊 ∧ (𝑃 − 2) ∈ (0...(#‘(𝑆𝐶))) ∧ 𝑈 ∈ (𝐼 × 2𝑜)) → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) = ((𝑆𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀𝑈)”⟩⟩))
23413, 232, 121, 233syl3anc 1323 . . . 4 (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) = ((𝑆𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀𝑈)”⟩⟩))
235 swrdcl 13352 . . . . . 6 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜))
23630, 235syl 17 . . . . 5 (𝜑 → ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜))
237 swrdcl 13352 . . . . . 6 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
23830, 237syl 17 . . . . 5 (𝜑 → ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
239 ccatswrd 13389 . . . . . . . . . . 11 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ ((𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐴𝐾))) ∧ (#‘(𝐴𝐾)) ∈ (0...(#‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩))
24034, 183, 44, 57, 239syl13anc 1325 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩))
241206simprd 479 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))
242 elfzuzb 12275 . . . . . . . . . . . . . . . 16 (𝑄 ∈ (0...(𝑃 − 2)) ↔ (𝑄 ∈ (ℤ‘0) ∧ (𝑃 − 2) ∈ (ℤ𝑄)))
24316, 89, 242sylanbrc 697 . . . . . . . . . . . . . . 15 (𝜑𝑄 ∈ (0...(𝑃 − 2)))
2442, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27, 44, 14, 121, 94, 129, 135efgredlemg 18071 . . . . . . . . . . . . . . . . . 18 (𝜑 → (#‘(𝐴𝐾)) = (#‘(𝐵𝐿)))
245244, 46eqeltrrd 2705 . . . . . . . . . . . . . . . . 17 (𝜑 → (#‘(𝐵𝐿)) ∈ (ℤ𝑃))
246 0le2 11056 . . . . . . . . . . . . . . . . . . . 20 0 ≤ 2
247246a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ≤ 2)
24876zred 11426 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑃 ∈ ℝ)
249 2re 11035 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
250 subge02 10489 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℝ ∧ 2 ∈ ℝ) → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
251248, 249, 250sylancl 693 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
252247, 251mpbid 222 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑃 − 2) ≤ 𝑃)
253 eluz2 11637 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ (ℤ‘(𝑃 − 2)) ↔ ((𝑃 − 2) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑃 − 2) ≤ 𝑃))
25478, 76, 252, 253syl3anbrc 1244 . . . . . . . . . . . . . . . . 17 (𝜑𝑃 ∈ (ℤ‘(𝑃 − 2)))
255 uztrn 11648 . . . . . . . . . . . . . . . . 17 (((#‘(𝐵𝐿)) ∈ (ℤ𝑃) ∧ 𝑃 ∈ (ℤ‘(𝑃 − 2))) → (#‘(𝐵𝐿)) ∈ (ℤ‘(𝑃 − 2)))
256245, 254, 255syl2anc 692 . . . . . . . . . . . . . . . 16 (𝜑 → (#‘(𝐵𝐿)) ∈ (ℤ‘(𝑃 − 2)))
257 elfzuzb 12275 . . . . . . . . . . . . . . . 16 ((𝑃 − 2) ∈ (0...(#‘(𝐵𝐿))) ↔ ((𝑃 − 2) ∈ (ℤ‘0) ∧ (#‘(𝐵𝐿)) ∈ (ℤ‘(𝑃 − 2))))
258230, 256, 257sylanbrc 697 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 − 2) ∈ (0...(#‘(𝐵𝐿))))
259 lencl 13258 . . . . . . . . . . . . . . . . . 18 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → (#‘(𝐵𝐿)) ∈ ℕ0)
26030, 259syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (#‘(𝐵𝐿)) ∈ ℕ0)
261260, 54syl6eleq 2714 . . . . . . . . . . . . . . . 16 (𝜑 → (#‘(𝐵𝐿)) ∈ (ℤ‘0))
262 eluzfz2 12288 . . . . . . . . . . . . . . . 16 ((#‘(𝐵𝐿)) ∈ (ℤ‘0) → (#‘(𝐵𝐿)) ∈ (0...(#‘(𝐵𝐿))))
263261, 262syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (#‘(𝐵𝐿)) ∈ (0...(#‘(𝐵𝐿))))
264 ccatswrd 13389 . . . . . . . . . . . . . . 15 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(#‘(𝐵𝐿))) ∧ (#‘(𝐵𝐿)) ∈ (0...(#‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))
26530, 243, 258, 263, 264syl13anc 1325 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨𝑄, (#‘(𝐵𝐿))⟩))
266241, 265eqtr4d 2663 . . . . . . . . . . . . 13 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩)))
267 swrdcl 13352 . . . . . . . . . . . . . . 15 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜))
26830, 267syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜))
269 swrdcl 13352 . . . . . . . . . . . . . . 15 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
27030, 269syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
271 swrdlen 13356 . . . . . . . . . . . . . . . 16 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐴𝐾)))) → (#‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
27234, 183, 44, 271syl3anc 1323 . . . . . . . . . . . . . . 15 (𝜑 → (#‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
273 swrdlen 13356 . . . . . . . . . . . . . . . . 17 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(#‘(𝐵𝐿)))) → (#‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
27430, 243, 258, 273syl3anc 1323 . . . . . . . . . . . . . . . 16 (𝜑 → (#‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
27580, 63, 71sub32d 10369 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑃𝑄) − 2) = ((𝑃 − 2) − 𝑄))
27680, 63, 71subsub4d 10368 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑃𝑄) − 2) = (𝑃 − (𝑄 + 2)))
277274, 275, 2763eqtr2d 2666 . . . . . . . . . . . . . . 15 (𝜑 → (#‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = (𝑃 − (𝑄 + 2)))
278272, 277eqtr4d 2663 . . . . . . . . . . . . . 14 (𝜑 → (#‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (#‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)))
279 ccatopth 13403 . . . . . . . . . . . . . 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 1334 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩))) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩)) ↔ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩))))
281266, 280mpbid 222 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩)))
282281simpld 475 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩))
283281simprd 479 . . . . . . . . . . . . . 14 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩))
284 elfzuzb 12275 . . . . . . . . . . . . . . . 16 ((𝑃 − 2) ∈ (0...𝑃) ↔ ((𝑃 − 2) ∈ (ℤ‘0) ∧ 𝑃 ∈ (ℤ‘(𝑃 − 2))))
285230, 254, 284sylanbrc 697 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 − 2) ∈ (0...𝑃))
286 elfzuz 12277 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ (0...(#‘(𝐴𝐾))) → 𝑃 ∈ (ℤ‘0))
28744, 286syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑃 ∈ (ℤ‘0))
288 elfzuzb 12275 . . . . . . . . . . . . . . . 16 (𝑃 ∈ (0...(#‘(𝐵𝐿))) ↔ (𝑃 ∈ (ℤ‘0) ∧ (#‘(𝐵𝐿)) ∈ (ℤ𝑃)))
289287, 245, 288sylanbrc 697 . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ (0...(#‘(𝐵𝐿))))
290 ccatswrd 13389 . . . . . . . . . . . . . . 15 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ ((𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐵𝐿))) ∧ (#‘(𝐵𝐿)) ∈ (0...(#‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩))
29130, 285, 289, 263, 290syl13anc 1325 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (#‘(𝐵𝐿))⟩))
292283, 291eqtr4d 2663 . . . . . . . . . . . . 13 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
293 swrdcl 13352 . . . . . . . . . . . . . . 15 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
29430, 293syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
295 s2len 13565 . . . . . . . . . . . . . . 15 (#‘⟨“𝑈(𝑀𝑈)”⟩) = 2
296 swrdlen 13356 . . . . . . . . . . . . . . . . 17 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐵𝐿)))) → (#‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
29730, 285, 289, 296syl3anc 1323 . . . . . . . . . . . . . . . 16 (𝜑 → (#‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
298 nncan 10255 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑃 − (𝑃 − 2)) = 2)
29980, 70, 298sylancl 693 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃 − (𝑃 − 2)) = 2)
300297, 299eqtr2d 2661 . . . . . . . . . . . . . . 15 (𝜑 → 2 = (#‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
301295, 300syl5eq 2672 . . . . . . . . . . . . . 14 (𝜑 → (#‘⟨“𝑈(𝑀𝑈)”⟩) = (#‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
302 ccatopth 13403 . . . . . . . . . . . . . 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 1334 . . . . . . . . . . . . 13 (𝜑 → ((⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) ↔ (⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩))))
304292, 303mpbid 222 . . . . . . . . . . . 12 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
305304simprd 479 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩))
306282, 305oveq12d 6623 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (#‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
307240, 306eqtr3d 2662 . . . . . . . . 9 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
308307oveq2d 6621 . . . . . . . 8 (𝜑 → (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩))))
309 ccatass 13305 . . . . . . . . 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 1323 . . . . . . . 8 (𝜑 → ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩))))
311308, 310eqtr4d 2663 . . . . . . 7 (𝜑 → (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (#‘(𝐴𝐾))⟩)) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
312 ccatswrd 13389 . . . . . . . . 9 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...𝑄) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(#‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩))
31330, 106, 243, 258, 312syl13anc 1325 . . . . . . . 8 (𝜑 → (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩))
314313oveq1d 6620 . . . . . . 7 (𝜑 → ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
31517, 311, 3143eqtrd 2664 . . . . . 6 (𝜑 → (𝑆𝐶) = (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
316 ccatrid 13304 . . . . . . . 8 (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜) → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ∅) = ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩))
317236, 316syl 17 . . . . . . 7 (𝜑 → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ∅) = ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩))
318317oveq1d 6620 . . . . . 6 (𝜑 → ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ∅) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
319315, 318eqtr4d 2663 . . . . 5 (𝜑 → (𝑆𝐶) = ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ∅) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
320 swrd0len 13355 . . . . . . 7 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (𝑃 − 2) ∈ (0...(#‘(𝐵𝐿)))) → (#‘((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩)) = (𝑃 − 2))
32130, 258, 320syl2anc 692 . . . . . 6 (𝜑 → (#‘((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩)) = (𝑃 − 2))
322321eqcomd 2632 . . . . 5 (𝜑 → (𝑃 − 2) = (#‘((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩)))
323175oveq2i 6616 . . . . . 6 ((𝑃 − 2) + (#‘∅)) = ((𝑃 − 2) + 0)
32478zcnd 11427 . . . . . . 7 (𝜑 → (𝑃 − 2) ∈ ℂ)
325324addid1d 10181 . . . . . 6 (𝜑 → ((𝑃 − 2) + 0) = (𝑃 − 2))
326323, 325syl5req 2673 . . . . 5 (𝜑 → (𝑃 − 2) = ((𝑃 − 2) + (#‘∅)))
327236, 100, 238, 124, 319, 322, 326splval2 13440 . . . 4 (𝜑 → ((𝑆𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀𝑈)”⟩⟩) = ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
328304simpld 475 . . . . . . . 8 (𝜑 → ⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩))
329328oveq2d 6621 . . . . . . 7 (𝜑 → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) = (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
330 eluzfz1 12287 . . . . . . . . 9 ((𝑃 − 2) ∈ (ℤ‘0) → 0 ∈ (0...(𝑃 − 2)))
331230, 330syl 17 . . . . . . . 8 (𝜑 → 0 ∈ (0...(𝑃 − 2)))
332 ccatswrd 13389 . . . . . . . 8 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵𝐿) substr ⟨0, 𝑃⟩))
33330, 331, 285, 289, 332syl13anc 1325 . . . . . . 7 (𝜑 → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵𝐿) substr ⟨0, 𝑃⟩))
334329, 333eqtrd 2660 . . . . . 6 (𝜑 → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) = ((𝐵𝐿) substr ⟨0, 𝑃⟩))
335334oveq1d 6620 . . . . 5 (𝜑 → ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)))
336 eluzfz1 12287 . . . . . . 7 (𝑃 ∈ (ℤ‘0) → 0 ∈ (0...𝑃))
337287, 336syl 17 . . . . . 6 (𝜑 → 0 ∈ (0...𝑃))
338 ccatswrd 13389 . . . . . 6 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐵𝐿))) ∧ (#‘(𝐵𝐿)) ∈ (0...(#‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨0, 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨0, (#‘(𝐵𝐿))⟩))
33930, 337, 289, 263, 338syl13anc 1325 . . . . 5 (𝜑 → (((𝐵𝐿) substr ⟨0, 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨0, (#‘(𝐵𝐿))⟩))
340 swrdid 13361 . . . . . 6 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨0, (#‘(𝐵𝐿))⟩) = (𝐵𝐿))
34130, 340syl 17 . . . . 5 (𝜑 → ((𝐵𝐿) substr ⟨0, (#‘(𝐵𝐿))⟩) = (𝐵𝐿))
342335, 339, 3413eqtrd 2664 . . . 4 (𝜑 → ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (#‘(𝐵𝐿))⟩)) = (𝐵𝐿))
343234, 327, 3423eqtrd 2664 . . 3 (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) = (𝐵𝐿))
344 fnovrn 6763 . . . 4 (((𝑇‘(𝑆𝐶)) Fn ((0...(#‘(𝑆𝐶))) × (𝐼 × 2𝑜)) ∧ (𝑃 − 2) ∈ (0...(#‘(𝑆𝐶))) ∧ 𝑈 ∈ (𝐼 × 2𝑜)) → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) ∈ ran (𝑇‘(𝑆𝐶)))
345225, 232, 121, 344syl3anc 1323 . . 3 (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) ∈ ran (𝑇‘(𝑆𝐶)))
346343, 345eqeltrrd 2705 . 2 (𝜑 → (𝐵𝐿) ∈ ran (𝑇‘(𝑆𝐶)))
347228, 346jca 554 1 (𝜑 → ((𝐴𝐾) ∈ ran (𝑇‘(𝑆𝐶)) ∧ (𝐵𝐿) ∈ ran (𝑇‘(𝑆𝐶))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wcel 1992  wral 2912  {crab 2916  cdif 3557  c0 3896  {csn 4153  cop 4159  cotp 4161   ciun 4490   class class class wbr 4618  cmpt 4678   I cid 4989   × cxp 5077  dom cdm 5079  ran crn 5080   Fn wfn 5845  wf 5846  cfv 5850  (class class class)co 6605  cmpt2 6607  1𝑜c1o 7499  2𝑜c2o 7500  cc 9879  cr 9880  0cc0 9881  1c1 9882   + caddc 9884   < clt 10019  cle 10020  cmin 10211  2c2 11015  0cn0 11237  cz 11322  cuz 11631  ...cfz 12265  ..^cfzo 12403  #chash 13054  Word cword 13225   ++ cconcat 13227   substr csubstr 13229   splice csplice 13230  ⟨“cs2 13518   ~FG cefg 18035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-cnex 9937  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-mulcom 9945  ax-addass 9946  ax-mulass 9947  ax-distr 9948  ax-i2m1 9949  ax-1ne0 9950  ax-1rid 9951  ax-rnegex 9952  ax-rrecex 9953  ax-cnre 9954  ax-pre-lttri 9955  ax-pre-lttrn 9956  ax-pre-ltadd 9957  ax-pre-mulgt0 9958
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-ot 4162  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-riota 6566  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-om 7014  df-1st 7116  df-2nd 7117  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-1o 7506  df-2o 7507  df-oadd 7510  df-er 7688  df-map 7805  df-pm 7806  df-en 7901  df-dom 7902  df-sdom 7903  df-fin 7904  df-card 8710  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025  df-sub 10213  df-neg 10214  df-nn 10966  df-2 11024  df-n0 11238  df-z 11323  df-uz 11632  df-fz 12266  df-fzo 12404  df-hash 13055  df-word 13233  df-concat 13235  df-s1 13236  df-substr 13237  df-splice 13238  df-s2 13525
This theorem is referenced by:  efgredlemd  18073
  Copyright terms: Public domain W3C validator