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

Theorem efgredleme 18864
 Description: Lemma for efgred 18869. (Contributed by Mario Carneiro, 1-Oct-2015.) (Proof shortened by AV, 15-Oct-2022.)
Hypotheses
Ref Expression
efgval.w 𝑊 = ( I ‘Word (𝐼 × 2o))
efgval.r = ( ~FG𝐼)
efgval2.m 𝑀 = (𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)
efgval2.t 𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 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 (𝜑𝑈 ∈ (𝐼 × 2o))
efgredlemb.v (𝜑𝑉 ∈ (𝐼 × 2o))
efgredlemb.6 (𝜑 → (𝑆𝐴) = (𝑃(𝑇‘(𝐴𝐾))𝑈))
efgredlemb.7 (𝜑 → (𝑆𝐵) = (𝑄(𝑇‘(𝐵𝐿))𝑉))
efgredlemb.8 (𝜑 → ¬ (𝐴𝐾) = (𝐵𝐿))
efgredlemd.9 (𝜑𝑃 ∈ (ℤ‘(𝑄 + 2)))
efgredlemd.c (𝜑𝐶 ∈ dom 𝑆)
efgredlemd.sc (𝜑 → (𝑆𝐶) = (((𝐵𝐿) prefix 𝑄) ++ ((𝐴𝐾) 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 (𝐼 × 2o))
3 efgval.r . . . . . . . . 9 = ( ~FG𝐼)
4 efgval2.m . . . . . . . . 9 𝑀 = (𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)
5 efgval2.t . . . . . . . . 9 𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀𝑤)”⟩⟩)))
6 efgred.d . . . . . . . . 9 𝐷 = (𝑊 𝑥𝑊 ran (𝑇𝑥))
7 efgred.s . . . . . . . . 9 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))
82, 3, 4, 5, 6, 7efgsf 18850 . . . . . . . 8 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
98fdmi 6498 . . . . . . . . 9 dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
109feq2i 6479 . . . . . . . 8 (𝑆:dom 𝑆𝑊𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊)
118, 10mpbir 234 . . . . . . 7 𝑆:dom 𝑆𝑊
1211ffvelrni 6827 . . . . . 6 (𝐶 ∈ dom 𝑆 → (𝑆𝐶) ∈ 𝑊)
131, 12syl 17 . . . . 5 (𝜑 → (𝑆𝐶) ∈ 𝑊)
14 efgredlemb.q . . . . . . 7 (𝜑𝑄 ∈ (0...(♯‘(𝐵𝐿))))
15 elfzuz 12900 . . . . . . 7 (𝑄 ∈ (0...(♯‘(𝐵𝐿))) → 𝑄 ∈ (ℤ‘0))
1614, 15syl 17 . . . . . 6 (𝜑𝑄 ∈ (ℤ‘0))
17 efgredlemd.sc . . . . . . . . . 10 (𝜑 → (𝑆𝐶) = (((𝐵𝐿) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
1817fveq2d 6649 . . . . . . . . 9 (𝜑 → (♯‘(𝑆𝐶)) = (♯‘(((𝐵𝐿) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))))
19 fviss 6716 . . . . . . . . . . . . 13 ( I ‘Word (𝐼 × 2o)) ⊆ Word (𝐼 × 2o)
202, 19eqsstri 3949 . . . . . . . . . . . 12 𝑊 ⊆ Word (𝐼 × 2o)
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 18862 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐾) ∈ 𝑊 ∧ (𝐵𝐿) ∈ 𝑊))
2928simprd 499 . . . . . . . . . . . 12 (𝜑 → (𝐵𝐿) ∈ 𝑊)
3020, 29sseldi 3913 . . . . . . . . . . 11 (𝜑 → (𝐵𝐿) ∈ Word (𝐼 × 2o))
31 pfxcl 14032 . . . . . . . . . . 11 ((𝐵𝐿) ∈ Word (𝐼 × 2o) → ((𝐵𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o))
3230, 31syl 17 . . . . . . . . . 10 (𝜑 → ((𝐵𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o))
3328simpld 498 . . . . . . . . . . . 12 (𝜑 → (𝐴𝐾) ∈ 𝑊)
3420, 33sseldi 3913 . . . . . . . . . . 11 (𝜑 → (𝐴𝐾) ∈ Word (𝐼 × 2o))
35 swrdcl 14000 . . . . . . . . . . 11 ((𝐴𝐾) ∈ Word (𝐼 × 2o) → ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2o))
3634, 35syl 17 . . . . . . . . . 10 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2o))
37 ccatlen 13920 . . . . . . . . . 10 ((((𝐵𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2o)) → (♯‘(((𝐵𝐿) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))) = ((♯‘((𝐵𝐿) prefix 𝑄)) + (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))))
3832, 36, 37syl2anc 587 . . . . . . . . 9 (𝜑 → (♯‘(((𝐵𝐿) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))) = ((♯‘((𝐵𝐿) prefix 𝑄)) + (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))))
39 pfxlen 14038 . . . . . . . . . . . 12 (((𝐵𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(♯‘(𝐵𝐿)))) → (♯‘((𝐵𝐿) prefix 𝑄)) = 𝑄)
4030, 14, 39syl2anc 587 . . . . . . . . . . 11 (𝜑 → (♯‘((𝐵𝐿) prefix 𝑄)) = 𝑄)
41 2nn0 11904 . . . . . . . . . . . . . 14 2 ∈ ℕ0
42 uzaddcl 12294 . . . . . . . . . . . . . 14 ((𝑄 ∈ (ℤ‘0) ∧ 2 ∈ ℕ0) → (𝑄 + 2) ∈ (ℤ‘0))
4316, 41, 42sylancl 589 . . . . . . . . . . . . 13 (𝜑 → (𝑄 + 2) ∈ (ℤ‘0))
44 efgredlemb.p . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ (0...(♯‘(𝐴𝐾))))
45 elfzuz3 12901 . . . . . . . . . . . . . . 15 (𝑃 ∈ (0...(♯‘(𝐴𝐾))) → (♯‘(𝐴𝐾)) ∈ (ℤ𝑃))
4644, 45syl 17 . . . . . . . . . . . . . 14 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ𝑃))
47 efgredlemd.9 . . . . . . . . . . . . . 14 (𝜑𝑃 ∈ (ℤ‘(𝑄 + 2)))
48 uztrn 12251 . . . . . . . . . . . . . 14 (((♯‘(𝐴𝐾)) ∈ (ℤ𝑃) ∧ 𝑃 ∈ (ℤ‘(𝑄 + 2))) → (♯‘(𝐴𝐾)) ∈ (ℤ‘(𝑄 + 2)))
4946, 47, 48syl2anc 587 . . . . . . . . . . . . 13 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ‘(𝑄 + 2)))
50 elfzuzb 12898 . . . . . . . . . . . . 13 ((𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾))) ↔ ((𝑄 + 2) ∈ (ℤ‘0) ∧ (♯‘(𝐴𝐾)) ∈ (ℤ‘(𝑄 + 2))))
5143, 49, 50sylanbrc 586 . . . . . . . . . . . 12 (𝜑 → (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾))))
52 lencl 13878 . . . . . . . . . . . . . . 15 ((𝐴𝐾) ∈ Word (𝐼 × 2o) → (♯‘(𝐴𝐾)) ∈ ℕ0)
5334, 52syl 17 . . . . . . . . . . . . . 14 (𝜑 → (♯‘(𝐴𝐾)) ∈ ℕ0)
54 nn0uz 12270 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
5553, 54eleqtrdi 2900 . . . . . . . . . . . . 13 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ‘0))
56 eluzfz2 12912 . . . . . . . . . . . . 13 ((♯‘(𝐴𝐾)) ∈ (ℤ‘0) → (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾))))
5755, 56syl 17 . . . . . . . . . . . 12 (𝜑 → (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾))))
58 swrdlen 14002 . . . . . . . . . . . 12 (((𝐴𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾))) ∧ (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾)))) → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((♯‘(𝐴𝐾)) − (𝑄 + 2)))
5934, 51, 57, 58syl3anc 1368 . . . . . . . . . . 11 (𝜑 → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((♯‘(𝐴𝐾)) − (𝑄 + 2)))
6040, 59oveq12d 7153 . . . . . . . . . 10 (𝜑 → ((♯‘((𝐵𝐿) prefix 𝑄)) + (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))) = (𝑄 + ((♯‘(𝐴𝐾)) − (𝑄 + 2))))
61 elfzelz 12904 . . . . . . . . . . . . 13 (𝑄 ∈ (0...(♯‘(𝐵𝐿))) → 𝑄 ∈ ℤ)
6214, 61syl 17 . . . . . . . . . . . 12 (𝜑𝑄 ∈ ℤ)
6362zcnd 12078 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℂ)
6453nn0cnd 11947 . . . . . . . . . . 11 (𝜑 → (♯‘(𝐴𝐾)) ∈ ℂ)
65 2z 12004 . . . . . . . . . . . . 13 2 ∈ ℤ
66 zaddcl 12012 . . . . . . . . . . . . 13 ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑄 + 2) ∈ ℤ)
6762, 65, 66sylancl 589 . . . . . . . . . . . 12 (𝜑 → (𝑄 + 2) ∈ ℤ)
6867zcnd 12078 . . . . . . . . . . 11 (𝜑 → (𝑄 + 2) ∈ ℂ)
6963, 64, 68addsubassd 11008 . . . . . . . . . 10 (𝜑 → ((𝑄 + (♯‘(𝐴𝐾))) − (𝑄 + 2)) = (𝑄 + ((♯‘(𝐴𝐾)) − (𝑄 + 2))))
70 2cn 11702 . . . . . . . . . . . 12 2 ∈ ℂ
7170a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℂ)
7263, 64, 71pnpcand 11025 . . . . . . . . . 10 (𝜑 → ((𝑄 + (♯‘(𝐴𝐾))) − (𝑄 + 2)) = ((♯‘(𝐴𝐾)) − 2))
7360, 69, 723eqtr2d 2839 . . . . . . . . 9 (𝜑 → ((♯‘((𝐵𝐿) prefix 𝑄)) + (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))) = ((♯‘(𝐴𝐾)) − 2))
7418, 38, 733eqtrd 2837 . . . . . . . 8 (𝜑 → (♯‘(𝑆𝐶)) = ((♯‘(𝐴𝐾)) − 2))
75 elfzelz 12904 . . . . . . . . . . 11 (𝑃 ∈ (0...(♯‘(𝐴𝐾))) → 𝑃 ∈ ℤ)
7644, 75syl 17 . . . . . . . . . 10 (𝜑𝑃 ∈ ℤ)
77 zsubcl 12014 . . . . . . . . . 10 ((𝑃 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑃 − 2) ∈ ℤ)
7876, 65, 77sylancl 589 . . . . . . . . 9 (𝜑 → (𝑃 − 2) ∈ ℤ)
7965a1i 11 . . . . . . . . 9 (𝜑 → 2 ∈ ℤ)
8076zcnd 12078 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℂ)
81 npcan 10886 . . . . . . . . . . . 12 ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑃 − 2) + 2) = 𝑃)
8280, 70, 81sylancl 589 . . . . . . . . . . 11 (𝜑 → ((𝑃 − 2) + 2) = 𝑃)
8382fveq2d 6649 . . . . . . . . . 10 (𝜑 → (ℤ‘((𝑃 − 2) + 2)) = (ℤ𝑃))
8446, 83eleqtrrd 2893 . . . . . . . . 9 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ‘((𝑃 − 2) + 2)))
85 eluzsub 12264 . . . . . . . . 9 (((𝑃 − 2) ∈ ℤ ∧ 2 ∈ ℤ ∧ (♯‘(𝐴𝐾)) ∈ (ℤ‘((𝑃 − 2) + 2))) → ((♯‘(𝐴𝐾)) − 2) ∈ (ℤ‘(𝑃 − 2)))
8678, 79, 84, 85syl3anc 1368 . . . . . . . 8 (𝜑 → ((♯‘(𝐴𝐾)) − 2) ∈ (ℤ‘(𝑃 − 2)))
8774, 86eqeltrd 2890 . . . . . . 7 (𝜑 → (♯‘(𝑆𝐶)) ∈ (ℤ‘(𝑃 − 2)))
88 eluzsub 12264 . . . . . . . 8 ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ ∧ 𝑃 ∈ (ℤ‘(𝑄 + 2))) → (𝑃 − 2) ∈ (ℤ𝑄))
8962, 79, 47, 88syl3anc 1368 . . . . . . 7 (𝜑 → (𝑃 − 2) ∈ (ℤ𝑄))
90 uztrn 12251 . . . . . . 7 (((♯‘(𝑆𝐶)) ∈ (ℤ‘(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (ℤ𝑄)) → (♯‘(𝑆𝐶)) ∈ (ℤ𝑄))
9187, 89, 90syl2anc 587 . . . . . 6 (𝜑 → (♯‘(𝑆𝐶)) ∈ (ℤ𝑄))
92 elfzuzb 12898 . . . . . 6 (𝑄 ∈ (0...(♯‘(𝑆𝐶))) ↔ (𝑄 ∈ (ℤ‘0) ∧ (♯‘(𝑆𝐶)) ∈ (ℤ𝑄)))
9316, 91, 92sylanbrc 586 . . . . 5 (𝜑𝑄 ∈ (0...(♯‘(𝑆𝐶))))
94 efgredlemb.v . . . . 5 (𝜑𝑉 ∈ (𝐼 × 2o))
952, 3, 4, 5efgtval 18844 . . . . 5 (((𝑆𝐶) ∈ 𝑊𝑄 ∈ (0...(♯‘(𝑆𝐶))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝑆𝐶))𝑉) = ((𝑆𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
9613, 93, 94, 95syl3anc 1368 . . . 4 (𝜑 → (𝑄(𝑇‘(𝑆𝐶))𝑉) = ((𝑆𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
97 pfxcl 14032 . . . . . 6 ((𝐴𝐾) ∈ Word (𝐼 × 2o) → ((𝐴𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o))
9834, 97syl 17 . . . . 5 (𝜑 → ((𝐴𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o))
99 wrd0 13884 . . . . . 6 ∅ ∈ Word (𝐼 × 2o)
10099a1i 11 . . . . 5 (𝜑 → ∅ ∈ Word (𝐼 × 2o))
1014efgmf 18834 . . . . . . . 8 𝑀:(𝐼 × 2o)⟶(𝐼 × 2o)
102101ffvelrni 6827 . . . . . . 7 (𝑉 ∈ (𝐼 × 2o) → (𝑀𝑉) ∈ (𝐼 × 2o))
10394, 102syl 17 . . . . . 6 (𝜑 → (𝑀𝑉) ∈ (𝐼 × 2o))
10494, 103s2cld 14226 . . . . 5 (𝜑 → ⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2o))
10562zred 12077 . . . . . . . . . . . . . . . . 17 (𝜑𝑄 ∈ ℝ)
106 nn0addge1 11933 . . . . . . . . . . . . . . . . 17 ((𝑄 ∈ ℝ ∧ 2 ∈ ℕ0) → 𝑄 ≤ (𝑄 + 2))
107105, 41, 106sylancl 589 . . . . . . . . . . . . . . . 16 (𝜑𝑄 ≤ (𝑄 + 2))
108 eluz2 12239 . . . . . . . . . . . . . . . 16 ((𝑄 + 2) ∈ (ℤ𝑄) ↔ (𝑄 ∈ ℤ ∧ (𝑄 + 2) ∈ ℤ ∧ 𝑄 ≤ (𝑄 + 2)))
10962, 67, 107, 108syl3anbrc 1340 . . . . . . . . . . . . . . 15 (𝜑 → (𝑄 + 2) ∈ (ℤ𝑄))
110 uztrn 12251 . . . . . . . . . . . . . . 15 ((𝑃 ∈ (ℤ‘(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (ℤ𝑄)) → 𝑃 ∈ (ℤ𝑄))
11147, 109, 110syl2anc 587 . . . . . . . . . . . . . 14 (𝜑𝑃 ∈ (ℤ𝑄))
112 elfzuzb 12898 . . . . . . . . . . . . . 14 (𝑄 ∈ (0...𝑃) ↔ (𝑄 ∈ (ℤ‘0) ∧ 𝑃 ∈ (ℤ𝑄)))
11316, 111, 112sylanbrc 586 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ (0...𝑃))
114 ccatpfx 14056 . . . . . . . . . . . . 13 (((𝐴𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾)))) → (((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴𝐾) prefix 𝑃))
11534, 113, 44, 114syl3anc 1368 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴𝐾) prefix 𝑃))
116115oveq1d 7150 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))))
117 pfxcl 14032 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2o) → ((𝐴𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o))
11834, 117syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o))
119 efgredlemb.u . . . . . . . . . . . . 13 (𝜑𝑈 ∈ (𝐼 × 2o))
120101ffvelrni 6827 . . . . . . . . . . . . . 14 (𝑈 ∈ (𝐼 × 2o) → (𝑀𝑈) ∈ (𝐼 × 2o))
121119, 120syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑀𝑈) ∈ (𝐼 × 2o))
122119, 121s2cld 14226 . . . . . . . . . . . 12 (𝜑 → ⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2o))
123 swrdcl 14000 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2o) → ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2o))
12434, 123syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2o))
125 ccatass 13935 . . . . . . . . . . . 12 ((((𝐴𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2o)) → ((((𝐴𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐴𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))))
126118, 122, 124, 125syl3anc 1368 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐴𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))))
127 efgredlemb.6 . . . . . . . . . . . . 13 (𝜑 → (𝑆𝐴) = (𝑃(𝑇‘(𝐴𝐾))𝑈))
1282, 3, 4, 5efgtval 18844 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ 𝑊𝑃 ∈ (0...(♯‘(𝐴𝐾))) ∧ 𝑈 ∈ (𝐼 × 2o)) → (𝑃(𝑇‘(𝐴𝐾))𝑈) = ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩))
12933, 44, 119, 128syl3anc 1368 . . . . . . . . . . . . 13 (𝜑 → (𝑃(𝑇‘(𝐴𝐾))𝑈) = ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩))
130 splval 14106 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ 𝑊 ∧ (𝑃 ∈ (0...(♯‘(𝐴𝐾))) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾))) ∧ ⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2o))) → ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩) = ((((𝐴𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))
13133, 44, 44, 122, 130syl13anc 1369 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩) = ((((𝐴𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))
132127, 129, 1313eqtrd 2837 . . . . . . . . . . . 12 (𝜑 → (𝑆𝐴) = ((((𝐴𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))
133 efgredlemb.7 . . . . . . . . . . . . 13 (𝜑 → (𝑆𝐵) = (𝑄(𝑇‘(𝐵𝐿))𝑉))
1342, 3, 4, 5efgtval 18844 . . . . . . . . . . . . . 14 (((𝐵𝐿) ∈ 𝑊𝑄 ∈ (0...(♯‘(𝐵𝐿))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝐵𝐿))𝑉) = ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
13529, 14, 94, 134syl3anc 1368 . . . . . . . . . . . . 13 (𝜑 → (𝑄(𝑇‘(𝐵𝐿))𝑉) = ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
136 splval 14106 . . . . . . . . . . . . . 14 (((𝐵𝐿) ∈ 𝑊 ∧ (𝑄 ∈ (0...(♯‘(𝐵𝐿))) ∧ 𝑄 ∈ (0...(♯‘(𝐵𝐿))) ∧ ⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2o))) → ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩) = ((((𝐵𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
13729, 14, 14, 104, 136syl13anc 1369 . . . . . . . . . . . . 13 (𝜑 → ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩) = ((((𝐵𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
138133, 135, 1373eqtrd 2837 . . . . . . . . . . . 12 (𝜑 → (𝑆𝐵) = ((((𝐵𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
13924, 132, 1383eqtr3d 2841 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((((𝐵𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
140116, 126, 1393eqtr2d 2839 . . . . . . . . . 10 (𝜑 → ((((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = ((((𝐵𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
141 swrdcl 14000 . . . . . . . . . . . 12 ((𝐴𝐾) ∈ Word (𝐼 × 2o) → ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o))
14234, 141syl 17 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o))
143 ccatcl 13919 . . . . . . . . . . . 12 ((⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2o)) → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2o))
144122, 124, 143syl2anc 587 . . . . . . . . . . 11 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2o))
145 ccatass 13935 . . . . . . . . . . 11 ((((𝐴𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2o)) → ((((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) prefix 𝑄) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))))
14698, 142, 144, 145syl3anc 1368 . . . . . . . . . 10 (𝜑 → ((((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) prefix 𝑄) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))))
147 swrdcl 14000 . . . . . . . . . . . 12 ((𝐵𝐿) ∈ Word (𝐼 × 2o) → ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o))
14830, 147syl 17 . . . . . . . . . . 11 (𝜑 → ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o))
149 ccatass 13935 . . . . . . . . . . 11 ((((𝐵𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o)) → ((((𝐵𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
15032, 104, 148, 149syl3anc 1368 . . . . . . . . . 10 (𝜑 → ((((𝐵𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
151140, 146, 1503eqtr3d 2841 . . . . . . . . 9 (𝜑 → (((𝐴𝐾) prefix 𝑄) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))) = (((𝐵𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
152 ccatcl 13919 . . . . . . . . . . 11 ((((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2o)) → (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2o))
153142, 144, 152syl2anc 587 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2o))
154 ccatcl 13919 . . . . . . . . . . 11 ((⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o)) → (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) ∈ Word (𝐼 × 2o))
155104, 148, 154syl2anc 587 . . . . . . . . . 10 (𝜑 → (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) ∈ Word (𝐼 × 2o))
156 uztrn 12251 . . . . . . . . . . . . . 14 (((♯‘(𝐴𝐾)) ∈ (ℤ𝑃) ∧ 𝑃 ∈ (ℤ𝑄)) → (♯‘(𝐴𝐾)) ∈ (ℤ𝑄))
15746, 111, 156syl2anc 587 . . . . . . . . . . . . 13 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ𝑄))
158 elfzuzb 12898 . . . . . . . . . . . . 13 (𝑄 ∈ (0...(♯‘(𝐴𝐾))) ↔ (𝑄 ∈ (ℤ‘0) ∧ (♯‘(𝐴𝐾)) ∈ (ℤ𝑄)))
15916, 157, 158sylanbrc 586 . . . . . . . . . . . 12 (𝜑𝑄 ∈ (0...(♯‘(𝐴𝐾))))
160 pfxlen 14038 . . . . . . . . . . . 12 (((𝐴𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(♯‘(𝐴𝐾)))) → (♯‘((𝐴𝐾) prefix 𝑄)) = 𝑄)
16134, 159, 160syl2anc 587 . . . . . . . . . . 11 (𝜑 → (♯‘((𝐴𝐾) prefix 𝑄)) = 𝑄)
162161, 40eqtr4d 2836 . . . . . . . . . 10 (𝜑 → (♯‘((𝐴𝐾) prefix 𝑄)) = (♯‘((𝐵𝐿) prefix 𝑄)))
163 ccatopth 14071 . . . . . . . . . 10 (((((𝐴𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2o)) ∧ (((𝐵𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) ∈ Word (𝐼 × 2o)) ∧ (♯‘((𝐴𝐾) prefix 𝑄)) = (♯‘((𝐵𝐿) prefix 𝑄))) → ((((𝐴𝐾) prefix 𝑄) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))) = (((𝐵𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))) ↔ (((𝐴𝐾) prefix 𝑄) = ((𝐵𝐿) prefix 𝑄) ∧ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))))
16498, 153, 32, 155, 162, 163syl221anc 1378 . . . . . . . . 9 (𝜑 → ((((𝐴𝐾) prefix 𝑄) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))) = (((𝐵𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))) ↔ (((𝐴𝐾) prefix 𝑄) = ((𝐵𝐿) prefix 𝑄) ∧ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))))
165151, 164mpbid 235 . . . . . . . 8 (𝜑 → (((𝐴𝐾) prefix 𝑄) = ((𝐵𝐿) prefix 𝑄) ∧ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
166165simpld 498 . . . . . . 7 (𝜑 → ((𝐴𝐾) prefix 𝑄) = ((𝐵𝐿) prefix 𝑄))
167166oveq1d 7150 . . . . . 6 (𝜑 → (((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
168 ccatrid 13934 . . . . . . . 8 (((𝐴𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o) → (((𝐴𝐾) prefix 𝑄) ++ ∅) = ((𝐴𝐾) prefix 𝑄))
16998, 168syl 17 . . . . . . 7 (𝜑 → (((𝐴𝐾) prefix 𝑄) ++ ∅) = ((𝐴𝐾) prefix 𝑄))
170169oveq1d 7150 . . . . . 6 (𝜑 → ((((𝐴𝐾) prefix 𝑄) ++ ∅) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
171167, 170, 173eqtr4rd 2844 . . . . 5 (𝜑 → (𝑆𝐶) = ((((𝐴𝐾) prefix 𝑄) ++ ∅) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
172161eqcomd 2804 . . . . 5 (𝜑𝑄 = (♯‘((𝐴𝐾) prefix 𝑄)))
173 hash0 13726 . . . . . . 7 (♯‘∅) = 0
174173oveq2i 7146 . . . . . 6 (𝑄 + (♯‘∅)) = (𝑄 + 0)
17563addid1d 10831 . . . . . 6 (𝜑 → (𝑄 + 0) = 𝑄)
176174, 175syl5req 2846 . . . . 5 (𝜑𝑄 = (𝑄 + (♯‘∅)))
17798, 100, 36, 104, 171, 172, 176splval2 14112 . . . 4 (𝜑 → ((𝑆𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩) = ((((𝐴𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
178 elfzuzb 12898 . . . . . . . . . . . . . 14 (𝑄 ∈ (0...(𝑄 + 2)) ↔ (𝑄 ∈ (ℤ‘0) ∧ (𝑄 + 2) ∈ (ℤ𝑄)))
17916, 109, 178sylanbrc 586 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ (0...(𝑄 + 2)))
180 elfzuzb 12898 . . . . . . . . . . . . . 14 ((𝑄 + 2) ∈ (0...𝑃) ↔ ((𝑄 + 2) ∈ (ℤ‘0) ∧ 𝑃 ∈ (ℤ‘(𝑄 + 2))))
18143, 47, 180sylanbrc 586 . . . . . . . . . . . . 13 (𝜑 → (𝑄 + 2) ∈ (0...𝑃))
182 ccatswrd 14023 . . . . . . . . . . . . 13 (((𝐴𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩))
18334, 179, 181, 44, 182syl13anc 1369 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩))
184183oveq1d 7150 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))))
185 swrdcl 14000 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2o) → ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2o))
18634, 185syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2o))
187 swrdcl 14000 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2o) → ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
18834, 187syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
189 ccatass 13935 . . . . . . . . . . . 12 ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2o) ∧ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2o)) → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))))
190186, 188, 144, 189syl3anc 1368 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))))
191165simprd 499 . . . . . . . . . . 11 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
192184, 190, 1913eqtr3d 2841 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
193 ccatcl 13919 . . . . . . . . . . . 12 ((((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2o)) → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2o))
194188, 144, 193syl2anc 587 . . . . . . . . . . 11 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2o))
195 swrdlen 14002 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾)))) → (♯‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
19634, 179, 51, 195syl3anc 1368 . . . . . . . . . . . . 13 (𝜑 → (♯‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
197 pncan2 10884 . . . . . . . . . . . . . 14 ((𝑄 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑄 + 2) − 𝑄) = 2)
19863, 70, 197sylancl 589 . . . . . . . . . . . . 13 (𝜑 → ((𝑄 + 2) − 𝑄) = 2)
199196, 198eqtrd 2833 . . . . . . . . . . . 12 (𝜑 → (♯‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = 2)
200 s2len 14244 . . . . . . . . . . . 12 (♯‘⟨“𝑉(𝑀𝑉)”⟩) = 2
201199, 200eqtr4di 2851 . . . . . . . . . . 11 (𝜑 → (♯‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (♯‘⟨“𝑉(𝑀𝑉)”⟩))
202 ccatopth 14071 . . . . . . . . . . 11 (((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2o) ∧ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2o)) ∧ (⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o)) ∧ (♯‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (♯‘⟨“𝑉(𝑀𝑉)”⟩)) → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) ↔ (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩ ∧ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
203186, 194, 104, 148, 201, 202syl221anc 1378 . . . . . . . . . 10 (𝜑 → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) ↔ (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩ ∧ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
204192, 203mpbid 235 . . . . . . . . 9 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩ ∧ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
205204simpld 498 . . . . . . . 8 (𝜑 → ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩)
206205oveq2d 7151 . . . . . . 7 (𝜑 → (((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (((𝐴𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩))
207 ccatpfx 14056 . . . . . . . 8 (((𝐴𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾)))) → (((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴𝐾) prefix (𝑄 + 2)))
20834, 179, 51, 207syl3anc 1368 . . . . . . 7 (𝜑 → (((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴𝐾) prefix (𝑄 + 2)))
209206, 208eqtr3d 2835 . . . . . 6 (𝜑 → (((𝐴𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) = ((𝐴𝐾) prefix (𝑄 + 2)))
210209oveq1d 7150 . . . . 5 (𝜑 → ((((𝐴𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (((𝐴𝐾) prefix (𝑄 + 2)) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
211 ccatpfx 14056 . . . . . 6 (((𝐴𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾))) ∧ (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾)))) → (((𝐴𝐾) prefix (𝑄 + 2)) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((𝐴𝐾) prefix (♯‘(𝐴𝐾))))
21234, 51, 57, 211syl3anc 1368 . . . . 5 (𝜑 → (((𝐴𝐾) prefix (𝑄 + 2)) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((𝐴𝐾) prefix (♯‘(𝐴𝐾))))
213 pfxid 14039 . . . . . 6 ((𝐴𝐾) ∈ Word (𝐼 × 2o) → ((𝐴𝐾) prefix (♯‘(𝐴𝐾))) = (𝐴𝐾))
21434, 213syl 17 . . . . 5 (𝜑 → ((𝐴𝐾) prefix (♯‘(𝐴𝐾))) = (𝐴𝐾))
215210, 212, 2143eqtrd 2837 . . . 4 (𝜑 → ((((𝐴𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (𝐴𝐾))
21696, 177, 2153eqtrd 2837 . . 3 (𝜑 → (𝑄(𝑇‘(𝑆𝐶))𝑉) = (𝐴𝐾))
2172, 3, 4, 5efgtf 18843 . . . . . . 7 ((𝑆𝐶) ∈ 𝑊 → ((𝑇‘(𝑆𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆𝐶))), 𝑖 ∈ (𝐼 × 2o) ↦ ((𝑆𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐶)):((0...(♯‘(𝑆𝐶))) × (𝐼 × 2o))⟶𝑊))
21813, 217syl 17 . . . . . 6 (𝜑 → ((𝑇‘(𝑆𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆𝐶))), 𝑖 ∈ (𝐼 × 2o) ↦ ((𝑆𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐶)):((0...(♯‘(𝑆𝐶))) × (𝐼 × 2o))⟶𝑊))
219218simprd 499 . . . . 5 (𝜑 → (𝑇‘(𝑆𝐶)):((0...(♯‘(𝑆𝐶))) × (𝐼 × 2o))⟶𝑊)
220219ffnd 6488 . . . 4 (𝜑 → (𝑇‘(𝑆𝐶)) Fn ((0...(♯‘(𝑆𝐶))) × (𝐼 × 2o)))
221 fnovrn 7304 . . . 4 (((𝑇‘(𝑆𝐶)) Fn ((0...(♯‘(𝑆𝐶))) × (𝐼 × 2o)) ∧ 𝑄 ∈ (0...(♯‘(𝑆𝐶))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝑆𝐶))𝑉) ∈ ran (𝑇‘(𝑆𝐶)))
222220, 93, 94, 221syl3anc 1368 . . 3 (𝜑 → (𝑄(𝑇‘(𝑆𝐶))𝑉) ∈ ran (𝑇‘(𝑆𝐶)))
223216, 222eqeltrrd 2891 . 2 (𝜑 → (𝐴𝐾) ∈ ran (𝑇‘(𝑆𝐶)))
224 uztrn 12251 . . . . . . 7 (((𝑃 − 2) ∈ (ℤ𝑄) ∧ 𝑄 ∈ (ℤ‘0)) → (𝑃 − 2) ∈ (ℤ‘0))
22589, 16, 224syl2anc 587 . . . . . 6 (𝜑 → (𝑃 − 2) ∈ (ℤ‘0))
226 elfzuzb 12898 . . . . . 6 ((𝑃 − 2) ∈ (0...(♯‘(𝑆𝐶))) ↔ ((𝑃 − 2) ∈ (ℤ‘0) ∧ (♯‘(𝑆𝐶)) ∈ (ℤ‘(𝑃 − 2))))
227225, 87, 226sylanbrc 586 . . . . 5 (𝜑 → (𝑃 − 2) ∈ (0...(♯‘(𝑆𝐶))))
2282, 3, 4, 5efgtval 18844 . . . . 5 (((𝑆𝐶) ∈ 𝑊 ∧ (𝑃 − 2) ∈ (0...(♯‘(𝑆𝐶))) ∧ 𝑈 ∈ (𝐼 × 2o)) → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) = ((𝑆𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀𝑈)”⟩⟩))
22913, 227, 119, 228syl3anc 1368 . . . 4 (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) = ((𝑆𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀𝑈)”⟩⟩))
230 pfxcl 14032 . . . . . 6 ((𝐵𝐿) ∈ Word (𝐼 × 2o) → ((𝐵𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o))
23130, 230syl 17 . . . . 5 (𝜑 → ((𝐵𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o))
232 swrdcl 14000 . . . . . 6 ((𝐵𝐿) ∈ Word (𝐼 × 2o) → ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o))
23330, 232syl 17 . . . . 5 (𝜑 → ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o))
234 ccatswrd 14023 . . . . . . . . . . 11 (((𝐴𝐾) ∈ Word (𝐼 × 2o) ∧ ((𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾))) ∧ (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))
23534, 181, 44, 57, 234syl13anc 1369 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))
236204simprd 499 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))
237 elfzuzb 12898 . . . . . . . . . . . . . . . 16 (𝑄 ∈ (0...(𝑃 − 2)) ↔ (𝑄 ∈ (ℤ‘0) ∧ (𝑃 − 2) ∈ (ℤ𝑄)))
23816, 89, 237sylanbrc 586 . . . . . . . . . . . . . . 15 (𝜑𝑄 ∈ (0...(𝑃 − 2)))
2392, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27, 44, 14, 119, 94, 127, 133efgredlemg 18863 . . . . . . . . . . . . . . . . . 18 (𝜑 → (♯‘(𝐴𝐾)) = (♯‘(𝐵𝐿)))
240239, 46eqeltrrd 2891 . . . . . . . . . . . . . . . . 17 (𝜑 → (♯‘(𝐵𝐿)) ∈ (ℤ𝑃))
241 0le2 11729 . . . . . . . . . . . . . . . . . . . 20 0 ≤ 2
242241a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ≤ 2)
24376zred 12077 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑃 ∈ ℝ)
244 2re 11701 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
245 subge02 11147 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℝ ∧ 2 ∈ ℝ) → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
246243, 244, 245sylancl 589 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
247242, 246mpbid 235 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑃 − 2) ≤ 𝑃)
248 eluz2 12239 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ (ℤ‘(𝑃 − 2)) ↔ ((𝑃 − 2) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑃 − 2) ≤ 𝑃))
24978, 76, 247, 248syl3anbrc 1340 . . . . . . . . . . . . . . . . 17 (𝜑𝑃 ∈ (ℤ‘(𝑃 − 2)))
250 uztrn 12251 . . . . . . . . . . . . . . . . 17 (((♯‘(𝐵𝐿)) ∈ (ℤ𝑃) ∧ 𝑃 ∈ (ℤ‘(𝑃 − 2))) → (♯‘(𝐵𝐿)) ∈ (ℤ‘(𝑃 − 2)))
251240, 249, 250syl2anc 587 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘(𝐵𝐿)) ∈ (ℤ‘(𝑃 − 2)))
252 elfzuzb 12898 . . . . . . . . . . . . . . . 16 ((𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿))) ↔ ((𝑃 − 2) ∈ (ℤ‘0) ∧ (♯‘(𝐵𝐿)) ∈ (ℤ‘(𝑃 − 2))))
253225, 251, 252sylanbrc 586 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿))))
254 lencl 13878 . . . . . . . . . . . . . . . . . 18 ((𝐵𝐿) ∈ Word (𝐼 × 2o) → (♯‘(𝐵𝐿)) ∈ ℕ0)
25530, 254syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (♯‘(𝐵𝐿)) ∈ ℕ0)
256255, 54eleqtrdi 2900 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘(𝐵𝐿)) ∈ (ℤ‘0))
257 eluzfz2 12912 . . . . . . . . . . . . . . . 16 ((♯‘(𝐵𝐿)) ∈ (ℤ‘0) → (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿))))
258256, 257syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿))))
259 ccatswrd 14023 . . . . . . . . . . . . . . 15 (((𝐵𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿))) ∧ (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))
26030, 238, 253, 258, 259syl13anc 1369 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))
261236, 260eqtr4d 2836 . . . . . . . . . . . . 13 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩)))
262 swrdcl 14000 . . . . . . . . . . . . . . 15 ((𝐵𝐿) ∈ Word (𝐼 × 2o) → ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2o))
26330, 262syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2o))
264 swrdcl 14000 . . . . . . . . . . . . . . 15 ((𝐵𝐿) ∈ Word (𝐼 × 2o) → ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o))
26530, 264syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o))
266 swrdlen 14002 . . . . . . . . . . . . . . . 16 (((𝐴𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾)))) → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
26734, 181, 44, 266syl3anc 1368 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
268 swrdlen 14002 . . . . . . . . . . . . . . . . 17 (((𝐵𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿)))) → (♯‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
26930, 238, 253, 268syl3anc 1368 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
27080, 63, 71sub32d 11020 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑃𝑄) − 2) = ((𝑃 − 2) − 𝑄))
27180, 63, 71subsub4d 11019 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑃𝑄) − 2) = (𝑃 − (𝑄 + 2)))
272269, 270, 2713eqtr2d 2839 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = (𝑃 − (𝑄 + 2)))
273267, 272eqtr4d 2836 . . . . . . . . . . . . . 14 (𝜑 → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (♯‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)))
274 ccatopth 14071 . . . . . . . . . . . . . 14 (((((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2o)) ∧ (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2o) ∧ ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o)) ∧ (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (♯‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩))) → ((((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩)) ↔ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩))))
275188, 144, 263, 265, 273, 274syl221anc 1378 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩)) ↔ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩))))
276261, 275mpbid 235 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩)))
277276simpld 498 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩))
278276simprd 499 . . . . . . . . . . . . . 14 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩))
279 elfzuzb 12898 . . . . . . . . . . . . . . . 16 ((𝑃 − 2) ∈ (0...𝑃) ↔ ((𝑃 − 2) ∈ (ℤ‘0) ∧ 𝑃 ∈ (ℤ‘(𝑃 − 2))))
280225, 249, 279sylanbrc 586 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 − 2) ∈ (0...𝑃))
281 elfzuz 12900 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ (0...(♯‘(𝐴𝐾))) → 𝑃 ∈ (ℤ‘0))
28244, 281syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑃 ∈ (ℤ‘0))
283 elfzuzb 12898 . . . . . . . . . . . . . . . 16 (𝑃 ∈ (0...(♯‘(𝐵𝐿))) ↔ (𝑃 ∈ (ℤ‘0) ∧ (♯‘(𝐵𝐿)) ∈ (ℤ𝑃)))
284282, 240, 283sylanbrc 586 . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ (0...(♯‘(𝐵𝐿))))
285 ccatswrd 14023 . . . . . . . . . . . . . . 15 (((𝐵𝐿) ∈ Word (𝐼 × 2o) ∧ ((𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵𝐿))) ∧ (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩))
28630, 280, 284, 258, 285syl13anc 1369 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩))
287278, 286eqtr4d 2836 . . . . . . . . . . . . 13 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
288 swrdcl 14000 . . . . . . . . . . . . . . 15 ((𝐵𝐿) ∈ Word (𝐼 × 2o) → ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
28930, 288syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
290 s2len 14244 . . . . . . . . . . . . . . 15 (♯‘⟨“𝑈(𝑀𝑈)”⟩) = 2
291 swrdlen 14002 . . . . . . . . . . . . . . . . 17 (((𝐵𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵𝐿)))) → (♯‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
29230, 280, 284, 291syl3anc 1368 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
293 nncan 10906 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑃 − (𝑃 − 2)) = 2)
29480, 70, 293sylancl 589 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃 − (𝑃 − 2)) = 2)
295292, 294eqtr2d 2834 . . . . . . . . . . . . . . 15 (𝜑 → 2 = (♯‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
296290, 295syl5eq 2845 . . . . . . . . . . . . . 14 (𝜑 → (♯‘⟨“𝑈(𝑀𝑈)”⟩) = (♯‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
297 ccatopth 14071 . . . . . . . . . . . . . 14 (((⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2o)) ∧ (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o)) ∧ (♯‘⟨“𝑈(𝑀𝑈)”⟩) = (♯‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩))) → ((⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) ↔ (⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))))
298122, 124, 289, 233, 296, 297syl221anc 1378 . . . . . . . . . . . . 13 (𝜑 → ((⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) ↔ (⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))))
299287, 298mpbid 235 . . . . . . . . . . . 12 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
300299simprd 499 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))
301277, 300oveq12d 7153 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
302235, 301eqtr3d 2835 . . . . . . . . 9 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
303302oveq2d 7151 . . . . . . . 8 (𝜑 → (((𝐵𝐿) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) prefix 𝑄) ++ (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))))
304 ccatass 13935 . . . . . . . . 9 ((((𝐵𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2o) ∧ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o)) → ((((𝐵𝐿) prefix 𝑄) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) prefix 𝑄) ++ (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))))
30532, 263, 233, 304syl3anc 1368 . . . . . . . 8 (𝜑 → ((((𝐵𝐿) prefix 𝑄) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) prefix 𝑄) ++ (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))))
306303, 305eqtr4d 2836 . . . . . . 7 (𝜑 → (((𝐵𝐿) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((((𝐵𝐿) prefix 𝑄) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
307 ccatpfx 14056 . . . . . . . . 9 (((𝐵𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿)))) → (((𝐵𝐿) prefix 𝑄) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵𝐿) prefix (𝑃 − 2)))
30830, 238, 253, 307syl3anc 1368 . . . . . . . 8 (𝜑 → (((𝐵𝐿) prefix 𝑄) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵𝐿) prefix (𝑃 − 2)))
309308oveq1d 7150 . . . . . . 7 (𝜑 → ((((𝐵𝐿) prefix 𝑄) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) prefix (𝑃 − 2)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
31017, 306, 3093eqtrd 2837 . . . . . 6 (𝜑 → (𝑆𝐶) = (((𝐵𝐿) prefix (𝑃 − 2)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
311 ccatrid 13934 . . . . . . . 8 (((𝐵𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o) → (((𝐵𝐿) prefix (𝑃 − 2)) ++ ∅) = ((𝐵𝐿) prefix (𝑃 − 2)))
312231, 311syl 17 . . . . . . 7 (𝜑 → (((𝐵𝐿) prefix (𝑃 − 2)) ++ ∅) = ((𝐵𝐿) prefix (𝑃 − 2)))
313312oveq1d 7150 . . . . . 6 (𝜑 → ((((𝐵𝐿) prefix (𝑃 − 2)) ++ ∅) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) prefix (𝑃 − 2)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
314310, 313eqtr4d 2836 . . . . 5 (𝜑 → (𝑆𝐶) = ((((𝐵𝐿) prefix (𝑃 − 2)) ++ ∅) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
315 pfxlen 14038 . . . . . . 7 (((𝐵𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿)))) → (♯‘((𝐵𝐿) prefix (𝑃 − 2))) = (𝑃 − 2))
31630, 253, 315syl2anc 587 . . . . . 6 (𝜑 → (♯‘((𝐵𝐿) prefix (𝑃 − 2))) = (𝑃 − 2))
317316eqcomd 2804 . . . . 5 (𝜑 → (𝑃 − 2) = (♯‘((𝐵𝐿) prefix (𝑃 − 2))))
318173oveq2i 7146 . . . . . 6 ((𝑃 − 2) + (♯‘∅)) = ((𝑃 − 2) + 0)
31978zcnd 12078 . . . . . . 7 (𝜑 → (𝑃 − 2) ∈ ℂ)
320319addid1d 10831 . . . . . 6 (𝜑 → ((𝑃 − 2) + 0) = (𝑃 − 2))
321318, 320syl5req 2846 . . . . 5 (𝜑 → (𝑃 − 2) = ((𝑃 − 2) + (♯‘∅)))
322231, 100, 233, 122, 314, 317, 321splval2 14112 . . . 4 (𝜑 → ((𝑆𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀𝑈)”⟩⟩) = ((((𝐵𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
323299simpld 498 . . . . . . . 8 (𝜑 → ⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩))
324323oveq2d 7151 . . . . . . 7 (𝜑 → (((𝐵𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀𝑈)”⟩) = (((𝐵𝐿) prefix (𝑃 − 2)) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
325 ccatpfx 14056 . . . . . . . 8 (((𝐵𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵𝐿)))) → (((𝐵𝐿) prefix (𝑃 − 2)) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵𝐿) prefix 𝑃))
32630, 280, 284, 325syl3anc 1368 . . . . . . 7 (𝜑 → (((𝐵𝐿) prefix (𝑃 − 2)) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵𝐿) prefix 𝑃))
327324, 326eqtrd 2833 . . . . . 6 (𝜑 → (((𝐵𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀𝑈)”⟩) = ((𝐵𝐿) prefix 𝑃))
328327oveq1d 7150 . . . . 5 (𝜑 → ((((𝐵𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) prefix 𝑃) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
329 ccatpfx 14056 . . . . . 6 (((𝐵𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑃 ∈ (0...(♯‘(𝐵𝐿))) ∧ (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿)))) → (((𝐵𝐿) prefix 𝑃) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) prefix (♯‘(𝐵𝐿))))
33030, 284, 258, 329syl3anc 1368 . . . . 5 (𝜑 → (((𝐵𝐿) prefix 𝑃) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) prefix (♯‘(𝐵𝐿))))
331 pfxid 14039 . . . . . 6 ((𝐵𝐿) ∈ Word (𝐼 × 2o) → ((𝐵𝐿) prefix (♯‘(𝐵𝐿))) = (𝐵𝐿))
33230, 331syl 17 . . . . 5 (𝜑 → ((𝐵𝐿) prefix (♯‘(𝐵𝐿))) = (𝐵𝐿))
333328, 330, 3323eqtrd 2837 . . . 4 (𝜑 → ((((𝐵𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (𝐵𝐿))
334229, 322, 3333eqtrd 2837 . . 3 (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) = (𝐵𝐿))
335 fnovrn 7304 . . . 4 (((𝑇‘(𝑆𝐶)) Fn ((0...(♯‘(𝑆𝐶))) × (𝐼 × 2o)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝑆𝐶))) ∧ 𝑈 ∈ (𝐼 × 2o)) → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) ∈ ran (𝑇‘(𝑆𝐶)))
336220, 227, 119, 335syl3anc 1368 . . 3 (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) ∈ ran (𝑇‘(𝑆𝐶)))
337334, 336eqeltrrd 2891 . 2 (𝜑 → (𝐵𝐿) ∈ ran (𝑇‘(𝑆𝐶)))
338223, 337jca 515 1 (𝜑 → ((𝐴𝐾) ∈ ran (𝑇‘(𝑆𝐶)) ∧ (𝐵𝐿) ∈ ran (𝑇‘(𝑆𝐶))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  {crab 3110   ∖ cdif 3878  ∅c0 4243  {csn 4525  ⟨cop 4531  ⟨cotp 4533  ∪ ciun 4881   class class class wbr 5030   ↦ cmpt 5110   I cid 5424   × cxp 5517  dom cdm 5519  ran crn 5520   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135   ∈ cmpo 7137  1oc1o 8080  2oc2o 8081  ℂcc 10526  ℝcr 10527  0cc0 10528  1c1 10529   + caddc 10531   < clt 10666   ≤ cle 10667   − cmin 10861  2c2 11682  ℕ0cn0 11887  ℤcz 11971  ℤ≥cuz 12233  ...cfz 12887  ..^cfzo 13030  ♯chash 13688  Word cword 13859   ++ cconcat 13915   substr csubstr 13995   prefix cpfx 14025   splice csplice 14104  ⟨“cs2 14196   ~FG cefg 18827 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7443  ax-cnex 10584  ax-resscn 10585  ax-1cn 10586  ax-icn 10587  ax-addcl 10588  ax-addrcl 10589  ax-mulcl 10590  ax-mulrcl 10591  ax-mulcom 10592  ax-addass 10593  ax-mulass 10594  ax-distr 10595  ax-i2m1 10596  ax-1ne0 10597  ax-1rid 10598  ax-rnegex 10599  ax-rrecex 10600  ax-cnre 10601  ax-pre-lttri 10602  ax-pre-lttrn 10603  ax-pre-ltadd 10604  ax-pre-mulgt0 10605 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-ot 4534  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7563  df-1st 7673  df-2nd 7674  df-wrecs 7932  df-recs 7993  df-rdg 8031  df-1o 8087  df-2o 8088  df-oadd 8091  df-er 8274  df-map 8393  df-en 8495  df-dom 8496  df-sdom 8497  df-fin 8498  df-card 9354  df-pnf 10668  df-mnf 10669  df-xr 10670  df-ltxr 10671  df-le 10672  df-sub 10863  df-neg 10864  df-nn 11628  df-2 11690  df-n0 11888  df-z 11972  df-uz 12234  df-fz 12888  df-fzo 13031  df-hash 13689  df-word 13860  df-concat 13916  df-s1 13943  df-substr 13996  df-pfx 14026  df-splice 14105  df-s2 14203 This theorem is referenced by:  efgredlemd  18865
 Copyright terms: Public domain W3C validator