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

Theorem efgredleme 18354
Description: Lemma for efgred 18359. (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 18340 . . . . . . . 8 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
98fdmi 6211 . . . . . . . . 9 dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
109feq2i 6196 . . . . . . . 8 (𝑆:dom 𝑆𝑊𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊)
118, 10mpbir 221 . . . . . . 7 𝑆:dom 𝑆𝑊
1211ffvelrni 6519 . . . . . 6 (𝐶 ∈ dom 𝑆 → (𝑆𝐶) ∈ 𝑊)
131, 12syl 17 . . . . 5 (𝜑 → (𝑆𝐶) ∈ 𝑊)
14 efgredlemb.q . . . . . . 7 (𝜑𝑄 ∈ (0...(♯‘(𝐵𝐿))))
15 elfzuz 12529 . . . . . . 7 (𝑄 ∈ (0...(♯‘(𝐵𝐿))) → 𝑄 ∈ (ℤ‘0))
1614, 15syl 17 . . . . . 6 (𝜑𝑄 ∈ (ℤ‘0))
17 efgredlemd.sc . . . . . . . . . 10 (𝜑 → (𝑆𝐶) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
1817fveq2d 6354 . . . . . . . . 9 (𝜑 → (♯‘(𝑆𝐶)) = (♯‘(((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))))
19 fviss 6416 . . . . . . . . . . . . 13 ( I ‘Word (𝐼 × 2𝑜)) ⊆ Word (𝐼 × 2𝑜)
202, 19eqsstri 3774 . . . . . . . . . . . 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 18352 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐾) ∈ 𝑊 ∧ (𝐵𝐿) ∈ 𝑊))
2928simprd 482 . . . . . . . . . . . 12 (𝜑 → (𝐵𝐿) ∈ 𝑊)
3020, 29sseldi 3740 . . . . . . . . . . 11 (𝜑 → (𝐵𝐿) ∈ Word (𝐼 × 2𝑜))
31 swrdcl 13616 . . . . . . . . . . 11 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜))
3230, 31syl 17 . . . . . . . . . 10 (𝜑 → ((𝐵𝐿) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜))
3328simpld 477 . . . . . . . . . . . 12 (𝜑 → (𝐴𝐾) ∈ 𝑊)
3420, 33sseldi 3740 . . . . . . . . . . 11 (𝜑 → (𝐴𝐾) ∈ Word (𝐼 × 2𝑜))
35 swrdcl 13616 . . . . . . . . . . 11 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜))
3634, 35syl 17 . . . . . . . . . 10 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜))
37 ccatlen 13545 . . . . . . . . . 10 ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) ∧ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜)) → (♯‘(((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))) = ((♯‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) + (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))))
3832, 36, 37syl2anc 696 . . . . . . . . 9 (𝜑 → (♯‘(((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))) = ((♯‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) + (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))))
39 swrd0len 13619 . . . . . . . . . . . 12 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(♯‘(𝐵𝐿)))) → (♯‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) = 𝑄)
4030, 14, 39syl2anc 696 . . . . . . . . . . 11 (𝜑 → (♯‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) = 𝑄)
41 2nn0 11499 . . . . . . . . . . . . . 14 2 ∈ ℕ0
42 uzaddcl 11935 . . . . . . . . . . . . . 14 ((𝑄 ∈ (ℤ‘0) ∧ 2 ∈ ℕ0) → (𝑄 + 2) ∈ (ℤ‘0))
4316, 41, 42sylancl 697 . . . . . . . . . . . . 13 (𝜑 → (𝑄 + 2) ∈ (ℤ‘0))
44 efgredlemb.p . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ (0...(♯‘(𝐴𝐾))))
45 elfzuz3 12530 . . . . . . . . . . . . . . 15 (𝑃 ∈ (0...(♯‘(𝐴𝐾))) → (♯‘(𝐴𝐾)) ∈ (ℤ𝑃))
4644, 45syl 17 . . . . . . . . . . . . . 14 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ𝑃))
47 efgredlemd.9 . . . . . . . . . . . . . 14 (𝜑𝑃 ∈ (ℤ‘(𝑄 + 2)))
48 uztrn 11894 . . . . . . . . . . . . . 14 (((♯‘(𝐴𝐾)) ∈ (ℤ𝑃) ∧ 𝑃 ∈ (ℤ‘(𝑄 + 2))) → (♯‘(𝐴𝐾)) ∈ (ℤ‘(𝑄 + 2)))
4946, 47, 48syl2anc 696 . . . . . . . . . . . . 13 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ‘(𝑄 + 2)))
50 elfzuzb 12527 . . . . . . . . . . . . 13 ((𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾))) ↔ ((𝑄 + 2) ∈ (ℤ‘0) ∧ (♯‘(𝐴𝐾)) ∈ (ℤ‘(𝑄 + 2))))
5143, 49, 50sylanbrc 701 . . . . . . . . . . . 12 (𝜑 → (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾))))
52 lencl 13508 . . . . . . . . . . . . . . 15 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → (♯‘(𝐴𝐾)) ∈ ℕ0)
5334, 52syl 17 . . . . . . . . . . . . . 14 (𝜑 → (♯‘(𝐴𝐾)) ∈ ℕ0)
54 nn0uz 11913 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
5553, 54syl6eleq 2847 . . . . . . . . . . . . 13 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ‘0))
56 eluzfz2 12540 . . . . . . . . . . . . 13 ((♯‘(𝐴𝐾)) ∈ (ℤ‘0) → (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾))))
5755, 56syl 17 . . . . . . . . . . . 12 (𝜑 → (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾))))
58 swrdlen 13620 . . . . . . . . . . . 12 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾))) ∧ (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾)))) → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((♯‘(𝐴𝐾)) − (𝑄 + 2)))
5934, 51, 57, 58syl3anc 1477 . . . . . . . . . . 11 (𝜑 → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((♯‘(𝐴𝐾)) − (𝑄 + 2)))
6040, 59oveq12d 6829 . . . . . . . . . 10 (𝜑 → ((♯‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) + (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))) = (𝑄 + ((♯‘(𝐴𝐾)) − (𝑄 + 2))))
61 elfzelz 12533 . . . . . . . . . . . . 13 (𝑄 ∈ (0...(♯‘(𝐵𝐿))) → 𝑄 ∈ ℤ)
6214, 61syl 17 . . . . . . . . . . . 12 (𝜑𝑄 ∈ ℤ)
6362zcnd 11673 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℂ)
6453nn0cnd 11543 . . . . . . . . . . 11 (𝜑 → (♯‘(𝐴𝐾)) ∈ ℂ)
65 2z 11599 . . . . . . . . . . . . 13 2 ∈ ℤ
66 zaddcl 11607 . . . . . . . . . . . . 13 ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑄 + 2) ∈ ℤ)
6762, 65, 66sylancl 697 . . . . . . . . . . . 12 (𝜑 → (𝑄 + 2) ∈ ℤ)
6867zcnd 11673 . . . . . . . . . . 11 (𝜑 → (𝑄 + 2) ∈ ℂ)
6963, 64, 68addsubassd 10602 . . . . . . . . . 10 (𝜑 → ((𝑄 + (♯‘(𝐴𝐾))) − (𝑄 + 2)) = (𝑄 + ((♯‘(𝐴𝐾)) − (𝑄 + 2))))
70 2cn 11281 . . . . . . . . . . . 12 2 ∈ ℂ
7170a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℂ)
7263, 64, 71pnpcand 10619 . . . . . . . . . 10 (𝜑 → ((𝑄 + (♯‘(𝐴𝐾))) − (𝑄 + 2)) = ((♯‘(𝐴𝐾)) − 2))
7360, 69, 723eqtr2d 2798 . . . . . . . . 9 (𝜑 → ((♯‘((𝐵𝐿) substr ⟨0, 𝑄⟩)) + (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))) = ((♯‘(𝐴𝐾)) − 2))
7418, 38, 733eqtrd 2796 . . . . . . . 8 (𝜑 → (♯‘(𝑆𝐶)) = ((♯‘(𝐴𝐾)) − 2))
75 elfzelz 12533 . . . . . . . . . . 11 (𝑃 ∈ (0...(♯‘(𝐴𝐾))) → 𝑃 ∈ ℤ)
7644, 75syl 17 . . . . . . . . . 10 (𝜑𝑃 ∈ ℤ)
77 zsubcl 11609 . . . . . . . . . 10 ((𝑃 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑃 − 2) ∈ ℤ)
7876, 65, 77sylancl 697 . . . . . . . . 9 (𝜑 → (𝑃 − 2) ∈ ℤ)
7965a1i 11 . . . . . . . . 9 (𝜑 → 2 ∈ ℤ)
8076zcnd 11673 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℂ)
81 npcan 10480 . . . . . . . . . . . 12 ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑃 − 2) + 2) = 𝑃)
8280, 70, 81sylancl 697 . . . . . . . . . . 11 (𝜑 → ((𝑃 − 2) + 2) = 𝑃)
8382fveq2d 6354 . . . . . . . . . 10 (𝜑 → (ℤ‘((𝑃 − 2) + 2)) = (ℤ𝑃))
8446, 83eleqtrrd 2840 . . . . . . . . 9 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ‘((𝑃 − 2) + 2)))
85 eluzsub 11907 . . . . . . . . 9 (((𝑃 − 2) ∈ ℤ ∧ 2 ∈ ℤ ∧ (♯‘(𝐴𝐾)) ∈ (ℤ‘((𝑃 − 2) + 2))) → ((♯‘(𝐴𝐾)) − 2) ∈ (ℤ‘(𝑃 − 2)))
8678, 79, 84, 85syl3anc 1477 . . . . . . . 8 (𝜑 → ((♯‘(𝐴𝐾)) − 2) ∈ (ℤ‘(𝑃 − 2)))
8774, 86eqeltrd 2837 . . . . . . 7 (𝜑 → (♯‘(𝑆𝐶)) ∈ (ℤ‘(𝑃 − 2)))
88 eluzsub 11907 . . . . . . . 8 ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ ∧ 𝑃 ∈ (ℤ‘(𝑄 + 2))) → (𝑃 − 2) ∈ (ℤ𝑄))
8962, 79, 47, 88syl3anc 1477 . . . . . . 7 (𝜑 → (𝑃 − 2) ∈ (ℤ𝑄))
90 uztrn 11894 . . . . . . 7 (((♯‘(𝑆𝐶)) ∈ (ℤ‘(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (ℤ𝑄)) → (♯‘(𝑆𝐶)) ∈ (ℤ𝑄))
9187, 89, 90syl2anc 696 . . . . . 6 (𝜑 → (♯‘(𝑆𝐶)) ∈ (ℤ𝑄))
92 elfzuzb 12527 . . . . . 6 (𝑄 ∈ (0...(♯‘(𝑆𝐶))) ↔ (𝑄 ∈ (ℤ‘0) ∧ (♯‘(𝑆𝐶)) ∈ (ℤ𝑄)))
9316, 91, 92sylanbrc 701 . . . . 5 (𝜑𝑄 ∈ (0...(♯‘(𝑆𝐶))))
94 efgredlemb.v . . . . 5 (𝜑𝑉 ∈ (𝐼 × 2𝑜))
952, 3, 4, 5efgtval 18334 . . . . 5 (((𝑆𝐶) ∈ 𝑊𝑄 ∈ (0...(♯‘(𝑆𝐶))) ∧ 𝑉 ∈ (𝐼 × 2𝑜)) → (𝑄(𝑇‘(𝑆𝐶))𝑉) = ((𝑆𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
9613, 93, 94, 95syl3anc 1477 . . . 4 (𝜑 → (𝑄(𝑇‘(𝑆𝐶))𝑉) = ((𝑆𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
97 swrdcl 13616 . . . . . 6 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜))
9834, 97syl 17 . . . . 5 (𝜑 → ((𝐴𝐾) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜))
99 wrd0 13514 . . . . . 6 ∅ ∈ Word (𝐼 × 2𝑜)
10099a1i 11 . . . . 5 (𝜑 → ∅ ∈ Word (𝐼 × 2𝑜))
1014efgmf 18324 . . . . . . . 8 𝑀:(𝐼 × 2𝑜)⟶(𝐼 × 2𝑜)
102101ffvelrni 6519 . . . . . . 7 (𝑉 ∈ (𝐼 × 2𝑜) → (𝑀𝑉) ∈ (𝐼 × 2𝑜))
10394, 102syl 17 . . . . . 6 (𝜑 → (𝑀𝑉) ∈ (𝐼 × 2𝑜))
10494, 103s2cld 13814 . . . . 5 (𝜑 → ⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2𝑜))
105 eluzfz1 12539 . . . . . . . . . . . . . 14 (𝑄 ∈ (ℤ‘0) → 0 ∈ (0...𝑄))
10616, 105syl 17 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ (0...𝑄))
10762zred 11672 . . . . . . . . . . . . . . . . 17 (𝜑𝑄 ∈ ℝ)
108 nn0addge1 11529 . . . . . . . . . . . . . . . . 17 ((𝑄 ∈ ℝ ∧ 2 ∈ ℕ0) → 𝑄 ≤ (𝑄 + 2))
109107, 41, 108sylancl 697 . . . . . . . . . . . . . . . 16 (𝜑𝑄 ≤ (𝑄 + 2))
110 eluz2 11883 . . . . . . . . . . . . . . . 16 ((𝑄 + 2) ∈ (ℤ𝑄) ↔ (𝑄 ∈ ℤ ∧ (𝑄 + 2) ∈ ℤ ∧ 𝑄 ≤ (𝑄 + 2)))
11162, 67, 109, 110syl3anbrc 1429 . . . . . . . . . . . . . . 15 (𝜑 → (𝑄 + 2) ∈ (ℤ𝑄))
112 uztrn 11894 . . . . . . . . . . . . . . 15 ((𝑃 ∈ (ℤ‘(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (ℤ𝑄)) → 𝑃 ∈ (ℤ𝑄))
11347, 111, 112syl2anc 696 . . . . . . . . . . . . . 14 (𝜑𝑃 ∈ (ℤ𝑄))
114 elfzuzb 12527 . . . . . . . . . . . . . 14 (𝑄 ∈ (0...𝑃) ↔ (𝑄 ∈ (ℤ‘0) ∧ 𝑃 ∈ (ℤ𝑄)))
11516, 113, 114sylanbrc 701 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ (0...𝑃))
116 ccatswrd 13654 . . . . . . . . . . . . 13 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...𝑄) ∧ 𝑄 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴𝐾) substr ⟨0, 𝑃⟩))
11734, 106, 115, 44, 116syl13anc 1479 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴𝐾) substr ⟨0, 𝑃⟩))
118117oveq1d 6826 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))))
119 swrdcl 13616 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨0, 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
12034, 119syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨0, 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
121 efgredlemb.u . . . . . . . . . . . . 13 (𝜑𝑈 ∈ (𝐼 × 2𝑜))
122101ffvelrni 6519 . . . . . . . . . . . . . 14 (𝑈 ∈ (𝐼 × 2𝑜) → (𝑀𝑈) ∈ (𝐼 × 2𝑜))
123121, 122syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑀𝑈) ∈ (𝐼 × 2𝑜))
124121, 123s2cld 13814 . . . . . . . . . . . 12 (𝜑 → ⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2𝑜))
125 swrdcl 13616 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜))
12634, 125syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜))
127 ccatass 13558 . . . . . . . . . . . 12 ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ ⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2𝑜) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜)) → ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))))
128120, 124, 126, 127syl3anc 1477 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))))
129 efgredlemb.6 . . . . . . . . . . . . 13 (𝜑 → (𝑆𝐴) = (𝑃(𝑇‘(𝐴𝐾))𝑈))
1302, 3, 4, 5efgtval 18334 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ 𝑊𝑃 ∈ (0...(♯‘(𝐴𝐾))) ∧ 𝑈 ∈ (𝐼 × 2𝑜)) → (𝑃(𝑇‘(𝐴𝐾))𝑈) = ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩))
13133, 44, 121, 130syl3anc 1477 . . . . . . . . . . . . 13 (𝜑 → (𝑃(𝑇‘(𝐴𝐾))𝑈) = ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩))
132 splval 13700 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ 𝑊 ∧ (𝑃 ∈ (0...(♯‘(𝐴𝐾))) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾))) ∧ ⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2𝑜))) → ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩) = ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))
13333, 44, 44, 124, 132syl13anc 1479 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩) = ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))
134129, 131, 1333eqtrd 2796 . . . . . . . . . . . 12 (𝜑 → (𝑆𝐴) = ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))
135 efgredlemb.7 . . . . . . . . . . . . 13 (𝜑 → (𝑆𝐵) = (𝑄(𝑇‘(𝐵𝐿))𝑉))
1362, 3, 4, 5efgtval 18334 . . . . . . . . . . . . . 14 (((𝐵𝐿) ∈ 𝑊𝑄 ∈ (0...(♯‘(𝐵𝐿))) ∧ 𝑉 ∈ (𝐼 × 2𝑜)) → (𝑄(𝑇‘(𝐵𝐿))𝑉) = ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
13729, 14, 94, 136syl3anc 1477 . . . . . . . . . . . . 13 (𝜑 → (𝑄(𝑇‘(𝐵𝐿))𝑉) = ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
138 splval 13700 . . . . . . . . . . . . . 14 (((𝐵𝐿) ∈ 𝑊 ∧ (𝑄 ∈ (0...(♯‘(𝐵𝐿))) ∧ 𝑄 ∈ (0...(♯‘(𝐵𝐿))) ∧ ⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2𝑜))) → ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
13929, 14, 14, 104, 138syl13anc 1479 . . . . . . . . . . . . 13 (𝜑 → ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
140135, 137, 1393eqtrd 2796 . . . . . . . . . . . 12 (𝜑 → (𝑆𝐵) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
14124, 134, 1403eqtr3d 2800 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑃⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
142118, 128, 1413eqtr2d 2798 . . . . . . . . . 10 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
143 swrdcl 13616 . . . . . . . . . . . 12 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
14434, 143syl 17 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
145 ccatcl 13544 . . . . . . . . . . . 12 ((⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2𝑜) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2𝑜)) → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜))
146124, 126, 145syl2anc 696 . . . . . . . . . . 11 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜))
147 ccatass 13558 . . . . . . . . . . 11 ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) ∧ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜)) → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))))
14898, 144, 146, 147syl3anc 1477 . . . . . . . . . 10 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))))
149 swrdcl 13616 . . . . . . . . . . . 12 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
15030, 149syl 17 . . . . . . . . . . 11 (𝜑 → ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
151 ccatass 13558 . . . . . . . . . . 11 ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) ∧ ⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2𝑜) ∧ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜)) → ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
15232, 104, 150, 151syl3anc 1477 . . . . . . . . . 10 (𝜑 → ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
153142, 148, 1523eqtr3d 2800 . . . . . . . . 9 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
154 ccatcl 13544 . . . . . . . . . . 11 ((((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜)) → (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2𝑜))
155144, 146, 154syl2anc 696 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2𝑜))
156 ccatcl 13544 . . . . . . . . . . 11 ((⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2𝑜) ∧ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜)) → (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) ∈ Word (𝐼 × 2𝑜))
157104, 150, 156syl2anc 696 . . . . . . . . . 10 (𝜑 → (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) ∈ Word (𝐼 × 2𝑜))
158 uztrn 11894 . . . . . . . . . . . . . 14 (((♯‘(𝐴𝐾)) ∈ (ℤ𝑃) ∧ 𝑃 ∈ (ℤ𝑄)) → (♯‘(𝐴𝐾)) ∈ (ℤ𝑄))
15946, 113, 158syl2anc 696 . . . . . . . . . . . . 13 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ𝑄))
160 elfzuzb 12527 . . . . . . . . . . . . 13 (𝑄 ∈ (0...(♯‘(𝐴𝐾))) ↔ (𝑄 ∈ (ℤ‘0) ∧ (♯‘(𝐴𝐾)) ∈ (ℤ𝑄)))
16116, 159, 160sylanbrc 701 . . . . . . . . . . . 12 (𝜑𝑄 ∈ (0...(♯‘(𝐴𝐾))))
162 swrd0len 13619 . . . . . . . . . . . 12 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(♯‘(𝐴𝐾)))) → (♯‘((𝐴𝐾) substr ⟨0, 𝑄⟩)) = 𝑄)
16334, 161, 162syl2anc 696 . . . . . . . . . . 11 (𝜑 → (♯‘((𝐴𝐾) substr ⟨0, 𝑄⟩)) = 𝑄)
164163, 40eqtr4d 2795 . . . . . . . . . 10 (𝜑 → (♯‘((𝐴𝐾) substr ⟨0, 𝑄⟩)) = (♯‘((𝐵𝐿) substr ⟨0, 𝑄⟩)))
165 ccatopth 13668 . . . . . . . . . 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 1488 . . . . . . . . 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 477 . . . . . . 7 (𝜑 → ((𝐴𝐾) substr ⟨0, 𝑄⟩) = ((𝐵𝐿) substr ⟨0, 𝑄⟩))
169168oveq1d 6826 . . . . . 6 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
170 ccatrid 13557 . . . . . . . 8 (((𝐴𝐾) substr ⟨0, 𝑄⟩) ∈ Word (𝐼 × 2𝑜) → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ∅) = ((𝐴𝐾) substr ⟨0, 𝑄⟩))
17198, 170syl 17 . . . . . . 7 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ∅) = ((𝐴𝐾) substr ⟨0, 𝑄⟩))
172171oveq1d 6826 . . . . . 6 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ∅) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
173169, 172, 173eqtr4rd 2803 . . . . 5 (𝜑 → (𝑆𝐶) = ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ∅) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
174163eqcomd 2764 . . . . 5 (𝜑𝑄 = (♯‘((𝐴𝐾) substr ⟨0, 𝑄⟩)))
175 hash0 13348 . . . . . . 7 (♯‘∅) = 0
176175oveq2i 6822 . . . . . 6 (𝑄 + (♯‘∅)) = (𝑄 + 0)
17763addid1d 10426 . . . . . 6 (𝜑 → (𝑄 + 0) = 𝑄)
178176, 177syl5req 2805 . . . . 5 (𝜑𝑄 = (𝑄 + (♯‘∅)))
17998, 100, 36, 104, 173, 174, 178splval2 13706 . . . 4 (𝜑 → ((𝑆𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩) = ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
180 elfzuzb 12527 . . . . . . . . . . . . . 14 (𝑄 ∈ (0...(𝑄 + 2)) ↔ (𝑄 ∈ (ℤ‘0) ∧ (𝑄 + 2) ∈ (ℤ𝑄)))
18116, 111, 180sylanbrc 701 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ (0...(𝑄 + 2)))
182 elfzuzb 12527 . . . . . . . . . . . . . 14 ((𝑄 + 2) ∈ (0...𝑃) ↔ ((𝑄 + 2) ∈ (ℤ‘0) ∧ 𝑃 ∈ (ℤ‘(𝑄 + 2))))
18343, 47, 182sylanbrc 701 . . . . . . . . . . . . 13 (𝜑 → (𝑄 + 2) ∈ (0...𝑃))
184 ccatswrd 13654 . . . . . . . . . . . . 13 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩))
18534, 181, 183, 44, 184syl13anc 1479 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩))
186185oveq1d 6826 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))))
187 swrdcl 13616 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2𝑜))
18834, 187syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2𝑜))
189 swrdcl 13616 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
19034, 189syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
191 ccatass 13558 . . . . . . . . . . . 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 1477 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))))
193167simprd 482 . . . . . . . . . . 11 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
194186, 192, 1933eqtr3d 2800 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
195 ccatcl 13544 . . . . . . . . . . . 12 ((((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2𝑜)) → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2𝑜))
196190, 146, 195syl2anc 696 . . . . . . . . . . 11 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2𝑜))
197 swrdlen 13620 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾)))) → (♯‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
19834, 181, 51, 197syl3anc 1477 . . . . . . . . . . . . 13 (𝜑 → (♯‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
199 pncan2 10478 . . . . . . . . . . . . . 14 ((𝑄 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑄 + 2) − 𝑄) = 2)
20063, 70, 199sylancl 697 . . . . . . . . . . . . 13 (𝜑 → ((𝑄 + 2) − 𝑄) = 2)
201198, 200eqtrd 2792 . . . . . . . . . . . 12 (𝜑 → (♯‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = 2)
202 s2len 13832 . . . . . . . . . . . 12 (♯‘⟨“𝑉(𝑀𝑉)”⟩) = 2
203201, 202syl6eqr 2810 . . . . . . . . . . 11 (𝜑 → (♯‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (♯‘⟨“𝑉(𝑀𝑉)”⟩))
204 ccatopth 13668 . . . . . . . . . . 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 1488 . . . . . . . . . 10 (𝜑 → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) ↔ (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩ ∧ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
206194, 205mpbid 222 . . . . . . . . 9 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩ ∧ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
207206simpld 477 . . . . . . . 8 (𝜑 → ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩)
208207oveq2d 6827 . . . . . . 7 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩))
209 ccatswrd 13654 . . . . . . . 8 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...𝑄) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩))
21034, 106, 181, 51, 209syl13anc 1479 . . . . . . 7 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩))
211208, 210eqtr3d 2794 . . . . . 6 (𝜑 → (((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) = ((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩))
212211oveq1d 6826 . . . . 5 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
213 eluzfz1 12539 . . . . . . 7 ((𝑄 + 2) ∈ (ℤ‘0) → 0 ∈ (0...(𝑄 + 2)))
21443, 213syl 17 . . . . . 6 (𝜑 → 0 ∈ (0...(𝑄 + 2)))
215 ccatswrd 13654 . . . . . 6 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾))) ∧ (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨0, (♯‘(𝐴𝐾))⟩))
21634, 214, 51, 57, 215syl13anc 1479 . . . . 5 (𝜑 → (((𝐴𝐾) substr ⟨0, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨0, (♯‘(𝐴𝐾))⟩))
217 swrdid 13626 . . . . . 6 ((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) → ((𝐴𝐾) substr ⟨0, (♯‘(𝐴𝐾))⟩) = (𝐴𝐾))
21834, 217syl 17 . . . . 5 (𝜑 → ((𝐴𝐾) substr ⟨0, (♯‘(𝐴𝐾))⟩) = (𝐴𝐾))
219212, 216, 2183eqtrd 2796 . . . 4 (𝜑 → ((((𝐴𝐾) substr ⟨0, 𝑄⟩) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (𝐴𝐾))
22096, 179, 2193eqtrd 2796 . . 3 (𝜑 → (𝑄(𝑇‘(𝑆𝐶))𝑉) = (𝐴𝐾))
2212, 3, 4, 5efgtf 18333 . . . . . . 7 ((𝑆𝐶) ∈ 𝑊 → ((𝑇‘(𝑆𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆𝐶))), 𝑖 ∈ (𝐼 × 2𝑜) ↦ ((𝑆𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐶)):((0...(♯‘(𝑆𝐶))) × (𝐼 × 2𝑜))⟶𝑊))
22213, 221syl 17 . . . . . 6 (𝜑 → ((𝑇‘(𝑆𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆𝐶))), 𝑖 ∈ (𝐼 × 2𝑜) ↦ ((𝑆𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐶)):((0...(♯‘(𝑆𝐶))) × (𝐼 × 2𝑜))⟶𝑊))
223222simprd 482 . . . . 5 (𝜑 → (𝑇‘(𝑆𝐶)):((0...(♯‘(𝑆𝐶))) × (𝐼 × 2𝑜))⟶𝑊)
224 ffn 6204 . . . . 5 ((𝑇‘(𝑆𝐶)):((0...(♯‘(𝑆𝐶))) × (𝐼 × 2𝑜))⟶𝑊 → (𝑇‘(𝑆𝐶)) Fn ((0...(♯‘(𝑆𝐶))) × (𝐼 × 2𝑜)))
225223, 224syl 17 . . . 4 (𝜑 → (𝑇‘(𝑆𝐶)) Fn ((0...(♯‘(𝑆𝐶))) × (𝐼 × 2𝑜)))
226 fnovrn 6972 . . . 4 (((𝑇‘(𝑆𝐶)) Fn ((0...(♯‘(𝑆𝐶))) × (𝐼 × 2𝑜)) ∧ 𝑄 ∈ (0...(♯‘(𝑆𝐶))) ∧ 𝑉 ∈ (𝐼 × 2𝑜)) → (𝑄(𝑇‘(𝑆𝐶))𝑉) ∈ ran (𝑇‘(𝑆𝐶)))
227225, 93, 94, 226syl3anc 1477 . . 3 (𝜑 → (𝑄(𝑇‘(𝑆𝐶))𝑉) ∈ ran (𝑇‘(𝑆𝐶)))
228220, 227eqeltrrd 2838 . 2 (𝜑 → (𝐴𝐾) ∈ ran (𝑇‘(𝑆𝐶)))
229 uztrn 11894 . . . . . . 7 (((𝑃 − 2) ∈ (ℤ𝑄) ∧ 𝑄 ∈ (ℤ‘0)) → (𝑃 − 2) ∈ (ℤ‘0))
23089, 16, 229syl2anc 696 . . . . . 6 (𝜑 → (𝑃 − 2) ∈ (ℤ‘0))
231 elfzuzb 12527 . . . . . 6 ((𝑃 − 2) ∈ (0...(♯‘(𝑆𝐶))) ↔ ((𝑃 − 2) ∈ (ℤ‘0) ∧ (♯‘(𝑆𝐶)) ∈ (ℤ‘(𝑃 − 2))))
232230, 87, 231sylanbrc 701 . . . . 5 (𝜑 → (𝑃 − 2) ∈ (0...(♯‘(𝑆𝐶))))
2332, 3, 4, 5efgtval 18334 . . . . 5 (((𝑆𝐶) ∈ 𝑊 ∧ (𝑃 − 2) ∈ (0...(♯‘(𝑆𝐶))) ∧ 𝑈 ∈ (𝐼 × 2𝑜)) → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) = ((𝑆𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀𝑈)”⟩⟩))
23413, 232, 121, 233syl3anc 1477 . . . 4 (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) = ((𝑆𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀𝑈)”⟩⟩))
235 swrdcl 13616 . . . . . 6 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜))
23630, 235syl 17 . . . . 5 (𝜑 → ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜))
237 swrdcl 13616 . . . . . 6 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
23830, 237syl 17 . . . . 5 (𝜑 → ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
239 ccatswrd 13654 . . . . . . . . . . 11 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ ((𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾))) ∧ (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))
24034, 183, 44, 57, 239syl13anc 1479 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))
241206simprd 482 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))
242 elfzuzb 12527 . . . . . . . . . . . . . . . 16 (𝑄 ∈ (0...(𝑃 − 2)) ↔ (𝑄 ∈ (ℤ‘0) ∧ (𝑃 − 2) ∈ (ℤ𝑄)))
24316, 89, 242sylanbrc 701 . . . . . . . . . . . . . . 15 (𝜑𝑄 ∈ (0...(𝑃 − 2)))
2442, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27, 44, 14, 121, 94, 129, 135efgredlemg 18353 . . . . . . . . . . . . . . . . . 18 (𝜑 → (♯‘(𝐴𝐾)) = (♯‘(𝐵𝐿)))
245244, 46eqeltrrd 2838 . . . . . . . . . . . . . . . . 17 (𝜑 → (♯‘(𝐵𝐿)) ∈ (ℤ𝑃))
246 0le2 11301 . . . . . . . . . . . . . . . . . . . 20 0 ≤ 2
247246a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ≤ 2)
24876zred 11672 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑃 ∈ ℝ)
249 2re 11280 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
250 subge02 10734 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℝ ∧ 2 ∈ ℝ) → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
251248, 249, 250sylancl 697 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
252247, 251mpbid 222 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑃 − 2) ≤ 𝑃)
253 eluz2 11883 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ (ℤ‘(𝑃 − 2)) ↔ ((𝑃 − 2) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑃 − 2) ≤ 𝑃))
25478, 76, 252, 253syl3anbrc 1429 . . . . . . . . . . . . . . . . 17 (𝜑𝑃 ∈ (ℤ‘(𝑃 − 2)))
255 uztrn 11894 . . . . . . . . . . . . . . . . 17 (((♯‘(𝐵𝐿)) ∈ (ℤ𝑃) ∧ 𝑃 ∈ (ℤ‘(𝑃 − 2))) → (♯‘(𝐵𝐿)) ∈ (ℤ‘(𝑃 − 2)))
256245, 254, 255syl2anc 696 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘(𝐵𝐿)) ∈ (ℤ‘(𝑃 − 2)))
257 elfzuzb 12527 . . . . . . . . . . . . . . . 16 ((𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿))) ↔ ((𝑃 − 2) ∈ (ℤ‘0) ∧ (♯‘(𝐵𝐿)) ∈ (ℤ‘(𝑃 − 2))))
258230, 256, 257sylanbrc 701 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿))))
259 lencl 13508 . . . . . . . . . . . . . . . . . 18 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → (♯‘(𝐵𝐿)) ∈ ℕ0)
26030, 259syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (♯‘(𝐵𝐿)) ∈ ℕ0)
261260, 54syl6eleq 2847 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘(𝐵𝐿)) ∈ (ℤ‘0))
262 eluzfz2 12540 . . . . . . . . . . . . . . . 16 ((♯‘(𝐵𝐿)) ∈ (ℤ‘0) → (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿))))
263261, 262syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿))))
264 ccatswrd 13654 . . . . . . . . . . . . . . 15 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿))) ∧ (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))
26530, 243, 258, 263, 264syl13anc 1479 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))
266241, 265eqtr4d 2795 . . . . . . . . . . . . 13 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩)))
267 swrdcl 13616 . . . . . . . . . . . . . . 15 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜))
26830, 267syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜))
269 swrdcl 13616 . . . . . . . . . . . . . . 15 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
27030, 269syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2𝑜))
271 swrdlen 13620 . . . . . . . . . . . . . . . 16 (((𝐴𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾)))) → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
27234, 183, 44, 271syl3anc 1477 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
273 swrdlen 13620 . . . . . . . . . . . . . . . . 17 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿)))) → (♯‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
27430, 243, 258, 273syl3anc 1477 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
27580, 63, 71sub32d 10614 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑃𝑄) − 2) = ((𝑃 − 2) − 𝑄))
27680, 63, 71subsub4d 10613 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑃𝑄) − 2) = (𝑃 − (𝑄 + 2)))
277274, 275, 2763eqtr2d 2798 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = (𝑃 − (𝑄 + 2)))
278272, 277eqtr4d 2795 . . . . . . . . . . . . . 14 (𝜑 → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (♯‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)))
279 ccatopth 13668 . . . . . . . . . . . . . 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 1488 . . . . . . . . . . . . 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 477 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩))
283281simprd 482 . . . . . . . . . . . . . 14 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩))
284 elfzuzb 12527 . . . . . . . . . . . . . . . 16 ((𝑃 − 2) ∈ (0...𝑃) ↔ ((𝑃 − 2) ∈ (ℤ‘0) ∧ 𝑃 ∈ (ℤ‘(𝑃 − 2))))
285230, 254, 284sylanbrc 701 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 − 2) ∈ (0...𝑃))
286 elfzuz 12529 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ (0...(♯‘(𝐴𝐾))) → 𝑃 ∈ (ℤ‘0))
28744, 286syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑃 ∈ (ℤ‘0))
288 elfzuzb 12527 . . . . . . . . . . . . . . . 16 (𝑃 ∈ (0...(♯‘(𝐵𝐿))) ↔ (𝑃 ∈ (ℤ‘0) ∧ (♯‘(𝐵𝐿)) ∈ (ℤ𝑃)))
289287, 245, 288sylanbrc 701 . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ (0...(♯‘(𝐵𝐿))))
290 ccatswrd 13654 . . . . . . . . . . . . . . 15 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ ((𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵𝐿))) ∧ (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩))
29130, 285, 289, 263, 290syl13anc 1479 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩))
292283, 291eqtr4d 2795 . . . . . . . . . . . . 13 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
293 swrdcl 13616 . . . . . . . . . . . . . . 15 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
29430, 293syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2𝑜))
295 s2len 13832 . . . . . . . . . . . . . . 15 (♯‘⟨“𝑈(𝑀𝑈)”⟩) = 2
296 swrdlen 13620 . . . . . . . . . . . . . . . . 17 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵𝐿)))) → (♯‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
29730, 285, 289, 296syl3anc 1477 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
298 nncan 10500 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑃 − (𝑃 − 2)) = 2)
29980, 70, 298sylancl 697 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃 − (𝑃 − 2)) = 2)
300297, 299eqtr2d 2793 . . . . . . . . . . . . . . 15 (𝜑 → 2 = (♯‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
301295, 300syl5eq 2804 . . . . . . . . . . . . . 14 (𝜑 → (♯‘⟨“𝑈(𝑀𝑈)”⟩) = (♯‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
302 ccatopth 13668 . . . . . . . . . . . . . 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 1488 . . . . . . . . . . . . 13 (𝜑 → ((⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) ↔ (⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))))
304292, 303mpbid 222 . . . . . . . . . . . 12 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
305304simprd 482 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))
306282, 305oveq12d 6829 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
307240, 306eqtr3d 2794 . . . . . . . . 9 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
308307oveq2d 6827 . . . . . . . 8 (𝜑 → (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))))
309 ccatass 13558 . . . . . . . . 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 1477 . . . . . . . 8 (𝜑 → ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))))
311308, 310eqtr4d 2795 . . . . . . 7 (𝜑 → (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
312 ccatswrd 13654 . . . . . . . . 9 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...𝑄) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩))
31330, 106, 243, 258, 312syl13anc 1479 . . . . . . . 8 (𝜑 → (((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩))
314313oveq1d 6826 . . . . . . 7 (𝜑 → ((((𝐵𝐿) substr ⟨0, 𝑄⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
31517, 311, 3143eqtrd 2796 . . . . . 6 (𝜑 → (𝑆𝐶) = (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
316 ccatrid 13557 . . . . . . . 8 (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2𝑜) → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ∅) = ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩))
317236, 316syl 17 . . . . . . 7 (𝜑 → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ∅) = ((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩))
318317oveq1d 6826 . . . . . 6 (𝜑 → ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ∅) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
319315, 318eqtr4d 2795 . . . . 5 (𝜑 → (𝑆𝐶) = ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ∅) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
320 swrd0len 13619 . . . . . . 7 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿)))) → (♯‘((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩)) = (𝑃 − 2))
32130, 258, 320syl2anc 696 . . . . . 6 (𝜑 → (♯‘((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩)) = (𝑃 − 2))
322321eqcomd 2764 . . . . 5 (𝜑 → (𝑃 − 2) = (♯‘((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩)))
323175oveq2i 6822 . . . . . 6 ((𝑃 − 2) + (♯‘∅)) = ((𝑃 − 2) + 0)
32478zcnd 11673 . . . . . . 7 (𝜑 → (𝑃 − 2) ∈ ℂ)
325324addid1d 10426 . . . . . 6 (𝜑 → ((𝑃 − 2) + 0) = (𝑃 − 2))
326323, 325syl5req 2805 . . . . 5 (𝜑 → (𝑃 − 2) = ((𝑃 − 2) + (♯‘∅)))
327236, 100, 238, 124, 319, 322, 326splval2 13706 . . . 4 (𝜑 → ((𝑆𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀𝑈)”⟩⟩) = ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
328304simpld 477 . . . . . . . 8 (𝜑 → ⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩))
329328oveq2d 6827 . . . . . . 7 (𝜑 → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) = (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
330 eluzfz1 12539 . . . . . . . . 9 ((𝑃 − 2) ∈ (ℤ‘0) → 0 ∈ (0...(𝑃 − 2)))
331230, 330syl 17 . . . . . . . 8 (𝜑 → 0 ∈ (0...(𝑃 − 2)))
332 ccatswrd 13654 . . . . . . . 8 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵𝐿) substr ⟨0, 𝑃⟩))
33330, 331, 285, 289, 332syl13anc 1479 . . . . . . 7 (𝜑 → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵𝐿) substr ⟨0, 𝑃⟩))
334329, 333eqtrd 2792 . . . . . 6 (𝜑 → (((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) = ((𝐵𝐿) substr ⟨0, 𝑃⟩))
335334oveq1d 6826 . . . . 5 (𝜑 → ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) substr ⟨0, 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
336 eluzfz1 12539 . . . . . . 7 (𝑃 ∈ (ℤ‘0) → 0 ∈ (0...𝑃))
337287, 336syl 17 . . . . . 6 (𝜑 → 0 ∈ (0...𝑃))
338 ccatswrd 13654 . . . . . 6 (((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (0 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵𝐿))) ∧ (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨0, 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨0, (♯‘(𝐵𝐿))⟩))
33930, 337, 289, 263, 338syl13anc 1479 . . . . 5 (𝜑 → (((𝐵𝐿) substr ⟨0, 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨0, (♯‘(𝐵𝐿))⟩))
340 swrdid 13626 . . . . . 6 ((𝐵𝐿) ∈ Word (𝐼 × 2𝑜) → ((𝐵𝐿) substr ⟨0, (♯‘(𝐵𝐿))⟩) = (𝐵𝐿))
34130, 340syl 17 . . . . 5 (𝜑 → ((𝐵𝐿) substr ⟨0, (♯‘(𝐵𝐿))⟩) = (𝐵𝐿))
342335, 339, 3413eqtrd 2796 . . . 4 (𝜑 → ((((𝐵𝐿) substr ⟨0, (𝑃 − 2)⟩) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (𝐵𝐿))
343234, 327, 3423eqtrd 2796 . . 3 (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) = (𝐵𝐿))
344 fnovrn 6972 . . . 4 (((𝑇‘(𝑆𝐶)) Fn ((0...(♯‘(𝑆𝐶))) × (𝐼 × 2𝑜)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝑆𝐶))) ∧ 𝑈 ∈ (𝐼 × 2𝑜)) → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) ∈ ran (𝑇‘(𝑆𝐶)))
345225, 232, 121, 344syl3anc 1477 . . 3 (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) ∈ ran (𝑇‘(𝑆𝐶)))
346343, 345eqeltrrd 2838 . 2 (𝜑 → (𝐵𝐿) ∈ ran (𝑇‘(𝑆𝐶)))
347228, 346jca 555 1 (𝜑 → ((𝐴𝐾) ∈ ran (𝑇‘(𝑆𝐶)) ∧ (𝐵𝐿) ∈ ran (𝑇‘(𝑆𝐶))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1630  wcel 2137  wral 3048  {crab 3052  cdif 3710  c0 4056  {csn 4319  cop 4325  cotp 4327   ciun 4670   class class class wbr 4802  cmpt 4879   I cid 5171   × cxp 5262  dom cdm 5264  ran crn 5265   Fn wfn 6042  wf 6043  cfv 6047  (class class class)co 6811  cmpt2 6813  1𝑜c1o 7720  2𝑜c2o 7721  cc 10124  cr 10125  0cc0 10126  1c1 10127   + caddc 10129   < clt 10264  cle 10265  cmin 10456  2c2 11260  0cn0 11482  cz 11567  cuz 11877  ...cfz 12517  ..^cfzo 12657  chash 13309  Word cword 13475   ++ cconcat 13477   substr csubstr 13479   splice csplice 13480  ⟨“cs2 13784   ~FG cefg 18317
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-rep 4921  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-cnex 10182  ax-resscn 10183  ax-1cn 10184  ax-icn 10185  ax-addcl 10186  ax-addrcl 10187  ax-mulcl 10188  ax-mulrcl 10189  ax-mulcom 10190  ax-addass 10191  ax-mulass 10192  ax-distr 10193  ax-i2m1 10194  ax-1ne0 10195  ax-1rid 10196  ax-rnegex 10197  ax-rrecex 10198  ax-cnre 10199  ax-pre-lttri 10200  ax-pre-lttrn 10201  ax-pre-ltadd 10202  ax-pre-mulgt0 10203
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-reu 3055  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-pss 3729  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-tp 4324  df-op 4326  df-ot 4328  df-uni 4587  df-int 4626  df-iun 4672  df-br 4803  df-opab 4863  df-mpt 4880  df-tr 4903  df-id 5172  df-eprel 5177  df-po 5185  df-so 5186  df-fr 5223  df-we 5225  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-pred 5839  df-ord 5885  df-on 5886  df-lim 5887  df-suc 5888  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-riota 6772  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-om 7229  df-1st 7331  df-2nd 7332  df-wrecs 7574  df-recs 7635  df-rdg 7673  df-1o 7727  df-2o 7728  df-oadd 7731  df-er 7909  df-map 8023  df-pm 8024  df-en 8120  df-dom 8121  df-sdom 8122  df-fin 8123  df-card 8953  df-pnf 10266  df-mnf 10267  df-xr 10268  df-ltxr 10269  df-le 10270  df-sub 10458  df-neg 10459  df-nn 11211  df-2 11269  df-n0 11483  df-z 11568  df-uz 11878  df-fz 12518  df-fzo 12658  df-hash 13310  df-word 13483  df-concat 13485  df-s1 13486  df-substr 13487  df-splice 13488  df-s2 13791
This theorem is referenced by:  efgredlemd  18355
  Copyright terms: Public domain W3C validator