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

Theorem efgredleme 18357
Description: Lemma for efgred 18362. (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 18343 . . . . . . . 8 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
98fdmi 6266 . . . . . . . . 9 dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
109feq2i 6248 . . . . . . . 8 (𝑆:dom 𝑆𝑊𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊)
118, 10mpbir 222 . . . . . . 7 𝑆:dom 𝑆𝑊
1211ffvelrni 6580 . . . . . 6 (𝐶 ∈ dom 𝑆 → (𝑆𝐶) ∈ 𝑊)
131, 12syl 17 . . . . 5 (𝜑 → (𝑆𝐶) ∈ 𝑊)
14 efgredlemb.q . . . . . . 7 (𝜑𝑄 ∈ (0...(♯‘(𝐵𝐿))))
15 elfzuz 12561 . . . . . . 7 (𝑄 ∈ (0...(♯‘(𝐵𝐿))) → 𝑄 ∈ (ℤ‘0))
1614, 15syl 17 . . . . . 6 (𝜑𝑄 ∈ (ℤ‘0))
17 efgredlemd.sc . . . . . . . . . 10 (𝜑 → (𝑆𝐶) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
1817fveq2d 6412 . . . . . . . . 9 (𝜑 → (♯‘(𝑆𝐶)) = (♯‘(((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))))
19 fviss 6477 . . . . . . . . . . . . 13 ( I ‘Word (𝐼 × 2𝑜)) ⊆ Word (𝐼 × 2𝑜)
202, 19eqsstri 3832 . . . . . . . . . . . 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 18355 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐾) ∈ 𝑊 ∧ (𝐵𝐿) ∈ 𝑊))
2928simprd 485 . . . . . . . . . . . 12 (𝜑 → (𝐵𝐿) ∈ 𝑊)
3020, 29sseldi 3796 . . . . . . . . . . 11 (𝜑 → (𝐵𝐿) ∈ Word (𝐼 × 2𝑜))
31 swrdcl 13642 . . . . . . . . . . 11 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜))
3230, 31syl 17 . . . . . . . . . 10 (𝜑 → ((𝐵𝐿) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜))
3328simpld 484 . . . . . . . . . . . 12 (𝜑 → (𝐴𝐾) ∈ 𝑊)
3420, 33sseldi 3796 . . . . . . . . . . 11 (𝜑 → (𝐴𝐾) ∈ Word (𝐼 × 2𝑜))
35 swrdcl 13642 . . . . . . . . . . 11 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜))
3634, 35syl 17 . . . . . . . . . 10 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜))
37 ccatlen 13572 . . . . . . . . . 10 ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) ∧ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜)) → (♯‘(((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))) = ((♯‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) + (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))))
3832, 36, 37syl2anc 575 . . . . . . . . 9 (𝜑 → (♯‘(((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))) = ((♯‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) + (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))))
39 swrd0len 13645 . . . . . . . . . . . 12 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(♯‘(𝐵𝐿)))) → (♯‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) = 𝑄)
4030, 14, 39syl2anc 575 . . . . . . . . . . 11 (𝜑 → (♯‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) = 𝑄)
41 2nn0 11576 . . . . . . . . . . . . . 14 2 ∈ ℕ0
42 uzaddcl 11962 . . . . . . . . . . . . . 14 ((𝑄 ∈ (ℤ‘0) ∧ 2 ∈ ℕ0) → (𝑄 + 2) ∈ (ℤ‘0))
4316, 41, 42sylancl 576 . . . . . . . . . . . . 13 (𝜑 → (𝑄 + 2) ∈ (ℤ‘0))
44 efgredlemb.p . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ (0...(♯‘(𝐴𝐾))))
45 elfzuz3 12562 . . . . . . . . . . . . . . 15 (𝑃 ∈ (0...(♯‘(𝐴𝐾))) → (♯‘(𝐴𝐾)) ∈ (ℤ𝑃))
4644, 45syl 17 . . . . . . . . . . . . . 14 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ𝑃))
47 efgredlemd.9 . . . . . . . . . . . . . 14 (𝜑𝑃 ∈ (ℤ‘(𝑄 + 2)))
48 uztrn 11921 . . . . . . . . . . . . . 14 (((♯‘(𝐴𝐾)) ∈ (ℤ𝑃) ∧ 𝑃 ∈ (ℤ‘(𝑄 + 2))) → (♯‘(𝐴𝐾)) ∈ (ℤ‘(𝑄 + 2)))
4946, 47, 48syl2anc 575 . . . . . . . . . . . . 13 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ‘(𝑄 + 2)))
50 elfzuzb 12559 . . . . . . . . . . . . 13 ((𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾))) ↔ ((𝑄 + 2) ∈ (ℤ‘0) ∧ (♯‘(𝐴𝐾)) ∈ (ℤ‘(𝑄 + 2))))
5143, 49, 50sylanbrc 574 . . . . . . . . . . . 12 (𝜑 → (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾))))
52 lencl 13535 . . . . . . . . . . . . . . 15 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → (♯‘(𝐴𝐾)) ∈ ℕ0)
5334, 52syl 17 . . . . . . . . . . . . . 14 (𝜑 → (♯‘(𝐴𝐾)) ∈ ℕ0)
54 nn0uz 11940 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
5553, 54syl6eleq 2895 . . . . . . . . . . . . 13 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ‘0))
56 eluzfz2 12572 . . . . . . . . . . . . 13 ((♯‘(𝐴𝐾)) ∈ (ℤ‘0) → (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾))))
5755, 56syl 17 . . . . . . . . . . . 12 (𝜑 → (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾))))
58 swrdlen 13646 . . . . . . . . . . . 12 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾))) ∧ (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾)))) → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((♯‘(𝐴𝐾)) − (𝑄 + 2)))
5934, 51, 57, 58syl3anc 1483 . . . . . . . . . . 11 (𝜑 → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((♯‘(𝐴𝐾)) − (𝑄 + 2)))
6040, 59oveq12d 6892 . . . . . . . . . 10 (𝜑 → ((♯‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) + (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))) = (𝑄 + ((♯‘(𝐴𝐾)) − (𝑄 + 2))))
61 elfzelz 12565 . . . . . . . . . . . . 13 (𝑄 ∈ (0...(♯‘(𝐵𝐿))) → 𝑄 ∈ ℤ)
6214, 61syl 17 . . . . . . . . . . . 12 (𝜑𝑄 ∈ ℤ)
6362zcnd 11749 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℂ)
6453nn0cnd 11619 . . . . . . . . . . 11 (𝜑 → (♯‘(𝐴𝐾)) ∈ ℂ)
65 2z 11675 . . . . . . . . . . . . 13 2 ∈ ℤ
66 zaddcl 11683 . . . . . . . . . . . . 13 ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑄 + 2) ∈ ℤ)
6762, 65, 66sylancl 576 . . . . . . . . . . . 12 (𝜑 → (𝑄 + 2) ∈ ℤ)
6867zcnd 11749 . . . . . . . . . . 11 (𝜑 → (𝑄 + 2) ∈ ℂ)
6963, 64, 68addsubassd 10697 . . . . . . . . . 10 (𝜑 → ((𝑄 + (♯‘(𝐴𝐾))) − (𝑄 + 2)) = (𝑄 + ((♯‘(𝐴𝐾)) − (𝑄 + 2))))
70 2cn 11375 . . . . . . . . . . . 12 2 ∈ ℂ
7170a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℂ)
7263, 64, 71pnpcand 10714 . . . . . . . . . 10 (𝜑 → ((𝑄 + (♯‘(𝐴𝐾))) − (𝑄 + 2)) = ((♯‘(𝐴𝐾)) − 2))
7360, 69, 723eqtr2d 2846 . . . . . . . . 9 (𝜑 → ((♯‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) + (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))) = ((♯‘(𝐴𝐾)) − 2))
7418, 38, 733eqtrd 2844 . . . . . . . 8 (𝜑 → (♯‘(𝑆𝐶)) = ((♯‘(𝐴𝐾)) − 2))
75 elfzelz 12565 . . . . . . . . . . 11 (𝑃 ∈ (0...(♯‘(𝐴𝐾))) → 𝑃 ∈ ℤ)
7644, 75syl 17 . . . . . . . . . 10 (𝜑𝑃 ∈ ℤ)
77 zsubcl 11685 . . . . . . . . . 10 ((𝑃 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑃 − 2) ∈ ℤ)
7876, 65, 77sylancl 576 . . . . . . . . 9 (𝜑 → (𝑃 − 2) ∈ ℤ)
7965a1i 11 . . . . . . . . 9 (𝜑 → 2 ∈ ℤ)
8076zcnd 11749 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℂ)
81 npcan 10575 . . . . . . . . . . . 12 ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑃 − 2) + 2) = 𝑃)
8280, 70, 81sylancl 576 . . . . . . . . . . 11 (𝜑 → ((𝑃 − 2) + 2) = 𝑃)
8382fveq2d 6412 . . . . . . . . . 10 (𝜑 → (ℤ‘((𝑃 − 2) + 2)) = (ℤ𝑃))
8446, 83eleqtrrd 2888 . . . . . . . . 9 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ‘((𝑃 − 2) + 2)))
85 eluzsub 11934 . . . . . . . . 9 (((𝑃 − 2) ∈ ℤ ∧ 2 ∈ ℤ ∧ (♯‘(𝐴𝐾)) ∈ (ℤ‘((𝑃 − 2) + 2))) → ((♯‘(𝐴𝐾)) − 2) ∈ (ℤ‘(𝑃 − 2)))
8678, 79, 84, 85syl3anc 1483 . . . . . . . 8 (𝜑 → ((♯‘(𝐴𝐾)) − 2) ∈ (ℤ‘(𝑃 − 2)))
8774, 86eqeltrd 2885 . . . . . . 7 (𝜑 → (♯‘(𝑆𝐶)) ∈ (ℤ‘(𝑃 − 2)))
88 eluzsub 11934 . . . . . . . 8 ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ ∧ 𝑃 ∈ (ℤ‘(𝑄 + 2))) → (𝑃 − 2) ∈ (ℤ𝑄))
8962, 79, 47, 88syl3anc 1483 . . . . . . 7 (𝜑 → (𝑃 − 2) ∈ (ℤ𝑄))
90 uztrn 11921 . . . . . . 7 (((♯‘(𝑆𝐶)) ∈ (ℤ‘(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (ℤ𝑄)) → (♯‘(𝑆𝐶)) ∈ (ℤ𝑄))
9187, 89, 90syl2anc 575 . . . . . 6 (𝜑 → (♯‘(𝑆𝐶)) ∈ (ℤ𝑄))
92 elfzuzb 12559 . . . . . 6 (𝑄 ∈ (0...(♯‘(𝑆𝐶))) ↔ (𝑄 ∈ (ℤ‘0) ∧ (♯‘(𝑆𝐶)) ∈ (ℤ𝑄)))
9316, 91, 92sylanbrc 574 . . . . 5 (𝜑𝑄 ∈ (0...(♯‘(𝑆𝐶))))
94 efgredlemb.v . . . . 5 (𝜑𝑉 ∈ (𝐼 × 2𝑜))
952, 3, 4, 5efgtval 18337 . . . . 5 (((𝑆𝐶) ∈ 𝑊𝑄 ∈ (0...(♯‘(𝑆𝐶))) ∧ 𝑉 ∈ (𝐼 × 2𝑜)) → (𝑄(𝑇‘(𝑆𝐶))𝑉) = ((𝑆𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
9613, 93, 94, 95syl3anc 1483 . . . 4 (𝜑 → (𝑄(𝑇‘(𝑆𝐶))𝑉) = ((𝑆𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
97 swrdcl 13642 . . . . . 6 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜))
9834, 97syl 17 . . . . 5 (𝜑 → ((𝐴𝐾) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜))
99 wrd0 13541 . . . . . 6 ∅ ∈ Word (𝐼 × 2𝑜)
10099a1i 11 . . . . 5 (𝜑 → ∅ ∈ Word (𝐼 × 2𝑜))
1014efgmf 18327 . . . . . . . 8 𝑀:(𝐼 × 2𝑜)⟶(𝐼 × 2𝑜)
102101ffvelrni 6580 . . . . . . 7 (𝑉 ∈ (𝐼 × 2𝑜) → (𝑀𝑉) ∈ (𝐼 × 2𝑜))
10394, 102syl 17 . . . . . 6 (𝜑 → (𝑀𝑉) ∈ (𝐼 × 2𝑜))
10494, 103s2cld 13840 . . . . 5 (𝜑 → ⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2𝑜))
105 eluzfz1 12571 . . . . . . . . . . . . . 14 (𝑄 ∈ (ℤ‘0) → 0 ∈ (0...𝑄))
10616, 105syl 17 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ (0...𝑄))
10762zred 11748 . . . . . . . . . . . . . . . . 17 (𝜑𝑄 ∈ ℝ)
108 nn0addge1 11605 . . . . . . . . . . . . . . . . 17 ((𝑄 ∈ ℝ ∧ 2 ∈ ℕ0) → 𝑄 ≤ (𝑄 + 2))
109107, 41, 108sylancl 576 . . . . . . . . . . . . . . . 16 (𝜑𝑄 ≤ (𝑄 + 2))
110 eluz2 11910 . . . . . . . . . . . . . . . 16 ((𝑄 + 2) ∈ (ℤ𝑄) ↔ (𝑄 ∈ ℤ ∧ (𝑄 + 2) ∈ ℤ ∧ 𝑄 ≤ (𝑄 + 2)))
11162, 67, 109, 110syl3anbrc 1436 . . . . . . . . . . . . . . 15 (𝜑 → (𝑄 + 2) ∈ (ℤ𝑄))
112 uztrn 11921 . . . . . . . . . . . . . . 15 ((𝑃 ∈ (ℤ‘(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (ℤ𝑄)) → 𝑃 ∈ (ℤ𝑄))
11347, 111, 112syl2anc 575 . . . . . . . . . . . . . 14 (𝜑𝑃 ∈ (ℤ𝑄))
114 elfzuzb 12559 . . . . . . . . . . . . . 14 (𝑄 ∈ (0...𝑃) ↔ (𝑄 ∈ (ℤ‘0) ∧ 𝑃 ∈ (ℤ𝑄)))
11516, 113, 114sylanbrc 574 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ (0...𝑃))
116 ccatswrd 13680 . . . . . . . . . . . . 13 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...𝑄) ∧ 𝑄 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴𝐾) substr ⟨0, 𝑃⟩))
11734, 106, 115, 44, 116syl13anc 1484 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴𝐾) substr ⟨0, 𝑃⟩))
118117oveq1d 6889 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))))
119 swrdcl 13642 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨0, 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
12034, 119syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨0, 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
121 efgredlemb.u . . . . . . . . . . . . 13 (𝜑𝑈 ∈ (𝐼 × 2𝑜))
122101ffvelrni 6580 . . . . . . . . . . . . . 14 (𝑈 ∈ (𝐼 × 2𝑜) → (𝑀𝑈) ∈ (𝐼 × 2𝑜))
123121, 122syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑀𝑈) ∈ (𝐼 × 2𝑜))
124121, 123s2cld 13840 . . . . . . . . . . . 12 (𝜑 → ⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2𝑜))
125 swrdcl 13642 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜))
12634, 125syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜))
127 ccatass 13585 . . . . . . . . . . . 12 ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ ⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2𝑜) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜)) → ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))))
128120, 124, 126, 127syl3anc 1483 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))))
129 efgredlemb.6 . . . . . . . . . . . . 13 (𝜑 → (𝑆𝐴) = (𝑃(𝑇‘(𝐴𝐾))𝑈))
1302, 3, 4, 5efgtval 18337 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ 𝑊𝑃 ∈ (0...(♯‘(𝐴𝐾))) ∧ 𝑈 ∈ (𝐼 × 2𝑜)) → (𝑃(𝑇‘(𝐴𝐾))𝑈) = ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩))
13133, 44, 121, 130syl3anc 1483 . . . . . . . . . . . . 13 (𝜑 → (𝑃(𝑇‘(𝐴𝐾))𝑈) = ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩))
132 splval 13726 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ 𝑊 ∧ (𝑃 ∈ (0...(♯‘(𝐴𝐾))) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾))) ∧ ⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2𝑜))) → ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩) = ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))
13333, 44, 44, 124, 132syl13anc 1484 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩) = ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))
134129, 131, 1333eqtrd 2844 . . . . . . . . . . . 12 (𝜑 → (𝑆𝐴) = ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))
135 efgredlemb.7 . . . . . . . . . . . . 13 (𝜑 → (𝑆𝐵) = (𝑄(𝑇‘(𝐵𝐿))𝑉))
1362, 3, 4, 5efgtval 18337 . . . . . . . . . . . . . 14 (((𝐵𝐿) ∈ 𝑊𝑄 ∈ (0...(♯‘(𝐵𝐿))) ∧ 𝑉 ∈ (𝐼 × 2𝑜)) → (𝑄(𝑇‘(𝐵𝐿))𝑉) = ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
13729, 14, 94, 136syl3anc 1483 . . . . . . . . . . . . 13 (𝜑 → (𝑄(𝑇‘(𝐵𝐿))𝑉) = ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
138 splval 13726 . . . . . . . . . . . . . 14 (((𝐵𝐿) ∈ 𝑊 ∧ (𝑄 ∈ (0...(♯‘(𝐵𝐿))) ∧ 𝑄 ∈ (0...(♯‘(𝐵𝐿))) ∧ ⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2𝑜))) → ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
13929, 14, 14, 104, 138syl13anc 1484 . . . . . . . . . . . . 13 (𝜑 → ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
140135, 137, 1393eqtrd 2844 . . . . . . . . . . . 12 (𝜑 → (𝑆𝐵) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
14124, 134, 1403eqtr3d 2848 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
142118, 128, 1413eqtr2d 2846 . . . . . . . . . 10 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
143 swrdcl 13642 . . . . . . . . . . . 12 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
14434, 143syl 17 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
145 ccatcl 13571 . . . . . . . . . . . 12 ((⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2𝑜) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜)) → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜))
146124, 126, 145syl2anc 575 . . . . . . . . . . 11 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜))
147 ccatass 13585 . . . . . . . . . . 11 ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) ∧ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜)) → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))))
14898, 144, 146, 147syl3anc 1483 . . . . . . . . . 10 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))))
149 swrdcl 13642 . . . . . . . . . . . 12 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
15030, 149syl 17 . . . . . . . . . . 11 (𝜑 → ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
151 ccatass 13585 . . . . . . . . . . 11 ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) ∧ ⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2𝑜) ∧ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜)) → ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
15232, 104, 150, 151syl3anc 1483 . . . . . . . . . 10 (𝜑 → ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
153142, 148, 1523eqtr3d 2848 . . . . . . . . 9 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
154 ccatcl 13571 . . . . . . . . . . 11 ((((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜)) → (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2𝑜))
155144, 146, 154syl2anc 575 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2𝑜))
156 ccatcl 13571 . . . . . . . . . . 11 ((⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2𝑜) ∧ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜)) → (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) ∈ Word (𝐼 × 2𝑜))
157104, 150, 156syl2anc 575 . . . . . . . . . 10 (𝜑 → (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) ∈ Word (𝐼 × 2𝑜))
158 uztrn 11921 . . . . . . . . . . . . . 14 (((♯‘(𝐴𝐾)) ∈ (ℤ𝑃) ∧ 𝑃 ∈ (ℤ𝑄)) → (♯‘(𝐴𝐾)) ∈ (ℤ𝑄))
15946, 113, 158syl2anc 575 . . . . . . . . . . . . 13 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ𝑄))
160 elfzuzb 12559 . . . . . . . . . . . . 13 (𝑄 ∈ (0...(♯‘(𝐴𝐾))) ↔ (𝑄 ∈ (ℤ‘0) ∧ (♯‘(𝐴𝐾)) ∈ (ℤ𝑄)))
16116, 159, 160sylanbrc 574 . . . . . . . . . . . 12 (𝜑𝑄 ∈ (0...(♯‘(𝐴𝐾))))
162 swrd0len 13645 . . . . . . . . . . . 12 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(♯‘(𝐴𝐾)))) → (♯‘((𝐴𝐾) substr ⟨0, 𝑄⟩)) = 𝑄)
16334, 161, 162syl2anc 575 . . . . . . . . . . 11 (𝜑 → (♯‘((𝐴𝐾) substr ⟨0, 𝑄⟩)) = 𝑄)
164163, 40eqtr4d 2843 . . . . . . . . . 10 (𝜑 → (♯‘((𝐴𝐾) substr ⟨0, 𝑄⟩)) = (♯‘((𝐵𝐿) substr ⟨0, 𝑄⟩)))
165 ccatopth 13694 . . . . . . . . . 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 1493 . . . . . . . . 9 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))) ↔ (((𝐴𝐾) substr ⟨0, 𝑄⟩) = ((𝐵𝐿) substr ⟨0, 𝑄⟩) ∧ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))))
167153, 166mpbid 223 . . . . . . . 8 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) = ((𝐵𝐿) substr ⟨0, 𝑄⟩) ∧ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
168167simpld 484 . . . . . . 7 (𝜑 → ((𝐴𝐾) substr ⟨0, 𝑄⟩) = ((𝐵𝐿) substr ⟨0, 𝑄⟩))
169168oveq1d 6889 . . . . . 6 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
170 ccatrid 13584 . . . . . . . 8 (((𝐴𝐾) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ∅) = ((𝐴𝐾) substr ⟨0, 𝑄⟩))
17198, 170syl 17 . . . . . . 7 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ∅) = ((𝐴𝐾) substr ⟨0, 𝑄⟩))
172171oveq1d 6889 . . . . . 6 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ∅) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
173169, 172, 173eqtr4rd 2851 . . . . 5 (𝜑 → (𝑆𝐶) = ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ∅) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
174163eqcomd 2812 . . . . 5 (𝜑𝑄 = (♯‘((𝐴𝐾) substr ⟨0, 𝑄⟩)))
175 hash0 13376 . . . . . . 7 (♯‘∅) = 0
176175oveq2i 6885 . . . . . 6 (𝑄 + (♯‘∅)) = (𝑄 + 0)
17763addid1d 10521 . . . . . 6 (𝜑 → (𝑄 + 0) = 𝑄)
178176, 177syl5req 2853 . . . . 5 (𝜑𝑄 = (𝑄 + (♯‘∅)))
17998, 100, 36, 104, 173, 174, 178splval2 13732 . . . 4 (𝜑 → ((𝑆𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩) = ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
180 elfzuzb 12559 . . . . . . . . . . . . . 14 (𝑄 ∈ (0...(𝑄 + 2)) ↔ (𝑄 ∈ (ℤ‘0) ∧ (𝑄 + 2) ∈ (ℤ𝑄)))
18116, 111, 180sylanbrc 574 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ (0...(𝑄 + 2)))
182 elfzuzb 12559 . . . . . . . . . . . . . 14 ((𝑄 + 2) ∈ (0...𝑃) ↔ ((𝑄 + 2) ∈ (ℤ‘0) ∧ 𝑃 ∈ (ℤ‘(𝑄 + 2))))
18343, 47, 182sylanbrc 574 . . . . . . . . . . . . 13 (𝜑 → (𝑄 + 2) ∈ (0...𝑃))
184 ccatswrd 13680 . . . . . . . . . . . . 13 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩))
18534, 181, 183, 44, 184syl13anc 1484 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩))
186185oveq1d 6889 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))))
187 swrdcl 13642 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2𝑜))
18834, 187syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2𝑜))
189 swrdcl 13642 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
19034, 189syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
191 ccatass 13585 . . . . . . . . . . . 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 1483 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))))
193167simprd 485 . . . . . . . . . . 11 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
194186, 192, 1933eqtr3d 2848 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
195 ccatcl 13571 . . . . . . . . . . . 12 ((((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜)) → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2𝑜))
196190, 146, 195syl2anc 575 . . . . . . . . . . 11 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2𝑜))
197 swrdlen 13646 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾)))) → (♯‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
19834, 181, 51, 197syl3anc 1483 . . . . . . . . . . . . 13 (𝜑 → (♯‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
199 pncan2 10573 . . . . . . . . . . . . . 14 ((𝑄 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑄 + 2) − 𝑄) = 2)
20063, 70, 199sylancl 576 . . . . . . . . . . . . 13 (𝜑 → ((𝑄 + 2) − 𝑄) = 2)
201198, 200eqtrd 2840 . . . . . . . . . . . 12 (𝜑 → (♯‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = 2)
202 s2len 13858 . . . . . . . . . . . 12 (♯‘⟨“𝑉(𝑀𝑉)”⟩) = 2
203201, 202syl6eqr 2858 . . . . . . . . . . 11 (𝜑 → (♯‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (♯‘⟨“𝑉(𝑀𝑉)”⟩))
204 ccatopth 13694 . . . . . . . . . . 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 1493 . . . . . . . . . 10 (𝜑 → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) ↔ (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩ ∧ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
206194, 205mpbid 223 . . . . . . . . 9 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩ ∧ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
207206simpld 484 . . . . . . . 8 (𝜑 → ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩)
208207oveq2d 6890 . . . . . . 7 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩))
209 ccatswrd 13680 . . . . . . . 8 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...𝑄) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩))
21034, 106, 181, 51, 209syl13anc 1484 . . . . . . 7 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩))
211208, 210eqtr3d 2842 . . . . . 6 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) = ((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩))
212211oveq1d 6889 . . . . 5 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
213 eluzfz1 12571 . . . . . . 7 ((𝑄 + 2) ∈ (ℤ‘0) → 0 ∈ (0...(𝑄 + 2)))
21443, 213syl 17 . . . . . 6 (𝜑 → 0 ∈ (0...(𝑄 + 2)))
215 ccatswrd 13680 . . . . . 6 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾))) ∧ (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨0, (♯‘(𝐴𝐾))⟩))
21634, 214, 51, 57, 215syl13anc 1484 . . . . 5 (𝜑 → (((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨0, (♯‘(𝐴𝐾))⟩))
217 swrdid 13652 . . . . . 6 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨0, (♯‘(𝐴𝐾))⟩) = (𝐴𝐾))
21834, 217syl 17 . . . . 5 (𝜑 → ((𝐴𝐾) substr ⟨0, (♯‘(𝐴𝐾))⟩) = (𝐴𝐾))
219212, 216, 2183eqtrd 2844 . . . 4 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (𝐴𝐾))
22096, 179, 2193eqtrd 2844 . . 3 (𝜑 → (𝑄(𝑇‘(𝑆𝐶))𝑉) = (𝐴𝐾))
2212, 3, 4, 5efgtf 18336 . . . . . . 7 ((𝑆𝐶) ∈ 𝑊 → ((𝑇‘(𝑆𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆𝐶))), 𝑖 ∈ (𝐼 × 2𝑜) ↦ ((𝑆𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐶)):((0...(♯‘(𝑆𝐶))) × (𝐼 × 2𝑜))⟶𝑊))
22213, 221syl 17 . . . . . 6 (𝜑 → ((𝑇‘(𝑆𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆𝐶))), 𝑖 ∈ (𝐼 × 2𝑜) ↦ ((𝑆𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐶)):((0...(♯‘(𝑆𝐶))) × (𝐼 × 2𝑜))⟶𝑊))
223222simprd 485 . . . . 5 (𝜑 → (𝑇‘(𝑆𝐶)):((0...(♯‘(𝑆𝐶))) × (𝐼 × 2𝑜))⟶𝑊)
224223ffnd 6257 . . . 4 (𝜑 → (𝑇‘(𝑆𝐶)) Fn ((0...(♯‘(𝑆𝐶))) × (𝐼 × 2𝑜)))
225 fnovrn 7039 . . . 4 (((𝑇‘(𝑆𝐶)) Fn ((0...(♯‘(𝑆𝐶))) × (𝐼 × 2𝑜)) ∧ 𝑄 ∈ (0...(♯‘(𝑆𝐶))) ∧ 𝑉 ∈ (𝐼 × 2𝑜)) → (𝑄(𝑇‘(𝑆𝐶))𝑉) ∈ ran (𝑇‘(𝑆𝐶)))
226224, 93, 94, 225syl3anc 1483 . . 3 (𝜑 → (𝑄(𝑇‘(𝑆𝐶))𝑉) ∈ ran (𝑇‘(𝑆𝐶)))
227220, 226eqeltrrd 2886 . 2 (𝜑 → (𝐴𝐾) ∈ ran (𝑇‘(𝑆𝐶)))
228 uztrn 11921 . . . . . . 7 (((𝑃 − 2) ∈ (ℤ𝑄) ∧ 𝑄 ∈ (ℤ‘0)) → (𝑃 − 2) ∈ (ℤ‘0))
22989, 16, 228syl2anc 575 . . . . . 6 (𝜑 → (𝑃 − 2) ∈ (ℤ‘0))
230 elfzuzb 12559 . . . . . 6 ((𝑃 − 2) ∈ (0...(♯‘(𝑆𝐶))) ↔ ((𝑃 − 2) ∈ (ℤ‘0) ∧ (♯‘(𝑆𝐶)) ∈ (ℤ‘(𝑃 − 2))))
231229, 87, 230sylanbrc 574 . . . . 5 (𝜑 → (𝑃 − 2) ∈ (0...(♯‘(𝑆𝐶))))
2322, 3, 4, 5efgtval 18337 . . . . 5 (((𝑆𝐶) ∈ 𝑊 ∧ (𝑃 − 2) ∈ (0...(♯‘(𝑆𝐶))) ∧ 𝑈 ∈ (𝐼 × 2𝑜)) → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) = ((𝑆𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀𝑈)”⟩⟩))
23313, 231, 121, 232syl3anc 1483 . . . 4 (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) = ((𝑆𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀𝑈)”⟩⟩))
234 swrdcl 13642 . . . . . 6 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜))
23530, 234syl 17 . . . . 5 (𝜑 → ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜))
236 swrdcl 13642 . . . . . 6 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
23730, 236syl 17 . . . . 5 (𝜑 → ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
238 ccatswrd 13680 . . . . . . . . . . 11 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ ((𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾))) ∧ (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))
23934, 183, 44, 57, 238syl13anc 1484 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))
240206simprd 485 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))
241 elfzuzb 12559 . . . . . . . . . . . . . . . 16 (𝑄 ∈ (0...(𝑃 − 2)) ↔ (𝑄 ∈ (ℤ‘0) ∧ (𝑃 − 2) ∈ (ℤ𝑄)))
24216, 89, 241sylanbrc 574 . . . . . . . . . . . . . . 15 (𝜑𝑄 ∈ (0...(𝑃 − 2)))
2432, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27, 44, 14, 121, 94, 129, 135efgredlemg 18356 . . . . . . . . . . . . . . . . . 18 (𝜑 → (♯‘(𝐴𝐾)) = (♯‘(𝐵𝐿)))
244243, 46eqeltrrd 2886 . . . . . . . . . . . . . . . . 17 (𝜑 → (♯‘(𝐵𝐿)) ∈ (ℤ𝑃))
245 0le2 11394 . . . . . . . . . . . . . . . . . . . 20 0 ≤ 2
246245a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ≤ 2)
24776zred 11748 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑃 ∈ ℝ)
248 2re 11374 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
249 subge02 10829 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℝ ∧ 2 ∈ ℝ) → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
250247, 248, 249sylancl 576 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
251246, 250mpbid 223 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑃 − 2) ≤ 𝑃)
252 eluz2 11910 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ (ℤ‘(𝑃 − 2)) ↔ ((𝑃 − 2) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑃 − 2) ≤ 𝑃))
25378, 76, 251, 252syl3anbrc 1436 . . . . . . . . . . . . . . . . 17 (𝜑𝑃 ∈ (ℤ‘(𝑃 − 2)))
254 uztrn 11921 . . . . . . . . . . . . . . . . 17 (((♯‘(𝐵𝐿)) ∈ (ℤ𝑃) ∧ 𝑃 ∈ (ℤ‘(𝑃 − 2))) → (♯‘(𝐵𝐿)) ∈ (ℤ‘(𝑃 − 2)))
255244, 253, 254syl2anc 575 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘(𝐵𝐿)) ∈ (ℤ‘(𝑃 − 2)))
256 elfzuzb 12559 . . . . . . . . . . . . . . . 16 ((𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿))) ↔ ((𝑃 − 2) ∈ (ℤ‘0) ∧ (♯‘(𝐵𝐿)) ∈ (ℤ‘(𝑃 − 2))))
257229, 255, 256sylanbrc 574 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿))))
258 lencl 13535 . . . . . . . . . . . . . . . . . 18 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → (♯‘(𝐵𝐿)) ∈ ℕ0)
25930, 258syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (♯‘(𝐵𝐿)) ∈ ℕ0)
260259, 54syl6eleq 2895 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘(𝐵𝐿)) ∈ (ℤ‘0))
261 eluzfz2 12572 . . . . . . . . . . . . . . . 16 ((♯‘(𝐵𝐿)) ∈ (ℤ‘0) → (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿))))
262260, 261syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿))))
263 ccatswrd 13680 . . . . . . . . . . . . . . 15 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿))) ∧ (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))
26430, 242, 257, 262, 263syl13anc 1484 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))
265240, 264eqtr4d 2843 . . . . . . . . . . . . 13 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩)))
266 swrdcl 13642 . . . . . . . . . . . . . . 15 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜))
26730, 266syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜))
268 swrdcl 13642 . . . . . . . . . . . . . . 15 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
26930, 268syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
270 swrdlen 13646 . . . . . . . . . . . . . . . 16 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾)))) → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
27134, 183, 44, 270syl3anc 1483 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
272 swrdlen 13646 . . . . . . . . . . . . . . . . 17 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿)))) → (♯‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
27330, 242, 257, 272syl3anc 1483 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
27480, 63, 71sub32d 10709 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑃𝑄) − 2) = ((𝑃 − 2) − 𝑄))
27580, 63, 71subsub4d 10708 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑃𝑄) − 2) = (𝑃 − (𝑄 + 2)))
276273, 274, 2753eqtr2d 2846 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = (𝑃 − (𝑄 + 2)))
277271, 276eqtr4d 2843 . . . . . . . . . . . . . 14 (𝜑 → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (♯‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)))
278 ccatopth 13694 . . . . . . . . . . . . . 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), (♯‘(𝐵𝐿))⟩))))
279190, 146, 267, 269, 277, 278syl221anc 1493 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩)) ↔ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩))))
280265, 279mpbid 223 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩)))
281280simpld 484 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩))
282280simprd 485 . . . . . . . . . . . . . 14 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩))
283 elfzuzb 12559 . . . . . . . . . . . . . . . 16 ((𝑃 − 2) ∈ (0...𝑃) ↔ ((𝑃 − 2) ∈ (ℤ‘0) ∧ 𝑃 ∈ (ℤ‘(𝑃 − 2))))
284229, 253, 283sylanbrc 574 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 − 2) ∈ (0...𝑃))
285 elfzuz 12561 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ (0...(♯‘(𝐴𝐾))) → 𝑃 ∈ (ℤ‘0))
28644, 285syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑃 ∈ (ℤ‘0))
287 elfzuzb 12559 . . . . . . . . . . . . . . . 16 (𝑃 ∈ (0...(♯‘(𝐵𝐿))) ↔ (𝑃 ∈ (ℤ‘0) ∧ (♯‘(𝐵𝐿)) ∈ (ℤ𝑃)))
288286, 244, 287sylanbrc 574 . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ (0...(♯‘(𝐵𝐿))))
289 ccatswrd 13680 . . . . . . . . . . . . . . 15 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ ((𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵𝐿))) ∧ (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩))
29030, 284, 288, 262, 289syl13anc 1484 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩))
291282, 290eqtr4d 2843 . . . . . . . . . . . . 13 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
292 swrdcl 13642 . . . . . . . . . . . . . . 15 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
29330, 292syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
294 s2len 13858 . . . . . . . . . . . . . . 15 (♯‘⟨“𝑈(𝑀𝑈)”⟩) = 2
295 swrdlen 13646 . . . . . . . . . . . . . . . . 17 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵𝐿)))) → (♯‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
29630, 284, 288, 295syl3anc 1483 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
297 nncan 10595 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑃 − (𝑃 − 2)) = 2)
29880, 70, 297sylancl 576 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃 − (𝑃 − 2)) = 2)
299296, 298eqtr2d 2841 . . . . . . . . . . . . . . 15 (𝜑 → 2 = (♯‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
300294, 299syl5eq 2852 . . . . . . . . . . . . . 14 (𝜑 → (♯‘⟨“𝑈(𝑀𝑈)”⟩) = (♯‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
301 ccatopth 13694 . . . . . . . . . . . . . 14 (((⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2𝑜) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜)) ∧ (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜)) ∧ (♯‘⟨“𝑈(𝑀𝑈)”⟩) = (♯‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩))) → ((⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) ↔ (⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))))
302124, 126, 293, 237, 300, 301syl221anc 1493 . . . . . . . . . . . . 13 (𝜑 → ((⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) ↔ (⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))))
303291, 302mpbid 223 . . . . . . . . . . . 12 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
304303simprd 485 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))
305281, 304oveq12d 6892 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
306239, 305eqtr3d 2842 . . . . . . . . 9 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
307306oveq2d 6890 . . . . . . . 8 (𝜑 → (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))))
308 ccatass 13585 . . . . . . . . 9 ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) ∧ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜) ∧ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜)) → ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))))
30932, 267, 237, 308syl3anc 1483 . . . . . . . 8 (𝜑 → ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))))
310307, 309eqtr4d 2843 . . . . . . 7 (𝜑 → (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
311 ccatswrd 13680 . . . . . . . . 9 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...𝑄) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩))
31230, 106, 242, 257, 311syl13anc 1484 . . . . . . . 8 (𝜑 → (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩))
313312oveq1d 6889 . . . . . . 7 (𝜑 → ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
31417, 310, 3133eqtrd 2844 . . . . . 6 (𝜑 → (𝑆𝐶) = (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
315 ccatrid 13584 . . . . . . . 8 (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜) → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ∅) = ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩))
316235, 315syl 17 . . . . . . 7 (𝜑 → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ∅) = ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩))
317316oveq1d 6889 . . . . . 6 (𝜑 → ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ∅) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
318314, 317eqtr4d 2843 . . . . 5 (𝜑 → (𝑆𝐶) = ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ∅) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
319 swrd0len 13645 . . . . . . 7 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿)))) → (♯‘((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩)) = (𝑃 − 2))
32030, 257, 319syl2anc 575 . . . . . 6 (𝜑 → (♯‘((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩)) = (𝑃 − 2))
321320eqcomd 2812 . . . . 5 (𝜑 → (𝑃 − 2) = (♯‘((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩)))
322175oveq2i 6885 . . . . . 6 ((𝑃 − 2) + (♯‘∅)) = ((𝑃 − 2) + 0)
32378zcnd 11749 . . . . . . 7 (𝜑 → (𝑃 − 2) ∈ ℂ)
324323addid1d 10521 . . . . . 6 (𝜑 → ((𝑃 − 2) + 0) = (𝑃 − 2))
325322, 324syl5req 2853 . . . . 5 (𝜑 → (𝑃 − 2) = ((𝑃 − 2) + (♯‘∅)))
326235, 100, 237, 124, 318, 321, 325splval2 13732 . . . 4 (𝜑 → ((𝑆𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀𝑈)”⟩⟩) = ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
327303simpld 484 . . . . . . . 8 (𝜑 → ⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩))
328327oveq2d 6890 . . . . . . 7 (𝜑 → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) = (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
329 eluzfz1 12571 . . . . . . . . 9 ((𝑃 − 2) ∈ (ℤ‘0) → 0 ∈ (0...(𝑃 − 2)))
330229, 329syl 17 . . . . . . . 8 (𝜑 → 0 ∈ (0...(𝑃 − 2)))
331 ccatswrd 13680 . . . . . . . 8 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵𝐿) substr ⟨0, 𝑃⟩))
33230, 330, 284, 288, 331syl13anc 1484 . . . . . . 7 (𝜑 → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵𝐿) substr ⟨0, 𝑃⟩))
333328, 332eqtrd 2840 . . . . . 6 (𝜑 → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) = ((𝐵𝐿) substr ⟨0, 𝑃⟩))
334333oveq1d 6889 . . . . 5 (𝜑 → ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
335 eluzfz1 12571 . . . . . . 7 (𝑃 ∈ (ℤ‘0) → 0 ∈ (0...𝑃))
336286, 335syl 17 . . . . . 6 (𝜑 → 0 ∈ (0...𝑃))
337 ccatswrd 13680 . . . . . 6 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵𝐿))) ∧ (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨0, 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨0, (♯‘(𝐵𝐿))⟩))
33830, 336, 288, 262, 337syl13anc 1484 . . . . 5 (𝜑 → (((𝐵𝐿) substr ⟨0, 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨0, (♯‘(𝐵𝐿))⟩))
339 swrdid 13652 . . . . . 6 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨0, (♯‘(𝐵𝐿))⟩) = (𝐵𝐿))
34030, 339syl 17 . . . . 5 (𝜑 → ((𝐵𝐿) substr ⟨0, (♯‘(𝐵𝐿))⟩) = (𝐵𝐿))
341334, 338, 3403eqtrd 2844 . . . 4 (𝜑 → ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (𝐵𝐿))
342233, 326, 3413eqtrd 2844 . . 3 (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) = (𝐵𝐿))
343 fnovrn 7039 . . . 4 (((𝑇‘(𝑆𝐶)) Fn ((0...(♯‘(𝑆𝐶))) × (𝐼 × 2𝑜)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝑆𝐶))) ∧ 𝑈 ∈ (𝐼 × 2𝑜)) → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) ∈ ran (𝑇‘(𝑆𝐶)))
344224, 231, 121, 343syl3anc 1483 . . 3 (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) ∈ ran (𝑇‘(𝑆𝐶)))
345342, 344eqeltrrd 2886 . 2 (𝜑 → (𝐵𝐿) ∈ ran (𝑇‘(𝑆𝐶)))
346227, 345jca 503 1 (𝜑 → ((𝐴𝐾) ∈ ran (𝑇‘(𝑆𝐶)) ∧ (𝐵𝐿) ∈ ran (𝑇‘(𝑆𝐶))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1637  wcel 2156  wral 3096  {crab 3100  cdif 3766  c0 4116  {csn 4370  cop 4376  cotp 4378   ciun 4712   class class class wbr 4844  cmpt 4923   I cid 5218   × cxp 5309  dom cdm 5311  ran crn 5312   Fn wfn 6096  wf 6097  cfv 6101  (class class class)co 6874  cmpt2 6876  1𝑜c1o 7789  2𝑜c2o 7790  cc 10219  cr 10220  0cc0 10221  1c1 10222   + caddc 10224   < clt 10359  cle 10360  cmin 10551  2c2 11356  0cn0 11559  cz 11643  cuz 11904  ...cfz 12549  ..^cfzo 12689  chash 13337  Word cword 13502   ++ cconcat 13504   substr csubstr 13506   splice csplice 13507  ⟨“cs2 13810   ~FG cefg 18320
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-cnex 10277  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-ot 4379  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-om 7296  df-1st 7398  df-2nd 7399  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-1o 7796  df-2o 7797  df-oadd 7800  df-er 7979  df-map 8094  df-pm 8095  df-en 8193  df-dom 8194  df-sdom 8195  df-fin 8196  df-card 9048  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-nn 11306  df-2 11364  df-n0 11560  df-z 11644  df-uz 11905  df-fz 12550  df-fzo 12690  df-hash 13338  df-word 13510  df-concat 13512  df-s1 13513  df-substr 13514  df-splice 13515  df-s2 13817
This theorem is referenced by:  efgredlemd  18358
  Copyright terms: Public domain W3C validator