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

Theorem efgredleme 19762
Description: Lemma for efgred 19767. (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 19748 . . . . . . . 8 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
98fdmi 6746 . . . . . . . . 9 dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
109feq2i 6727 . . . . . . . 8 (𝑆:dom 𝑆𝑊𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊)
118, 10mpbir 231 . . . . . . 7 𝑆:dom 𝑆𝑊
1211ffvelcdmi 7102 . . . . . 6 (𝐶 ∈ dom 𝑆 → (𝑆𝐶) ∈ 𝑊)
131, 12syl 17 . . . . 5 (𝜑 → (𝑆𝐶) ∈ 𝑊)
14 efgredlemb.q . . . . . . 7 (𝜑𝑄 ∈ (0...(♯‘(𝐵𝐿))))
15 elfzuz 13561 . . . . . . 7 (𝑄 ∈ (0...(♯‘(𝐵𝐿))) → 𝑄 ∈ (ℤ‘0))
1614, 15syl 17 . . . . . 6 (𝜑𝑄 ∈ (ℤ‘0))
17 efgredlemd.sc . . . . . . . . . 10 (𝜑 → (𝑆𝐶) = (((𝐵𝐿) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
1817fveq2d 6909 . . . . . . . . 9 (𝜑 → (♯‘(𝑆𝐶)) = (♯‘(((𝐵𝐿) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))))
19 fviss 6985 . . . . . . . . . . . . 13 ( I ‘Word (𝐼 × 2o)) ⊆ Word (𝐼 × 2o)
202, 19eqsstri 4029 . . . . . . . . . . . 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 19760 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐾) ∈ 𝑊 ∧ (𝐵𝐿) ∈ 𝑊))
2928simprd 495 . . . . . . . . . . . 12 (𝜑 → (𝐵𝐿) ∈ 𝑊)
3020, 29sselid 3980 . . . . . . . . . . 11 (𝜑 → (𝐵𝐿) ∈ Word (𝐼 × 2o))
31 pfxcl 14716 . . . . . . . . . . 11 ((𝐵𝐿) ∈ Word (𝐼 × 2o) → ((𝐵𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o))
3230, 31syl 17 . . . . . . . . . 10 (𝜑 → ((𝐵𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o))
3328simpld 494 . . . . . . . . . . . 12 (𝜑 → (𝐴𝐾) ∈ 𝑊)
3420, 33sselid 3980 . . . . . . . . . . 11 (𝜑 → (𝐴𝐾) ∈ Word (𝐼 × 2o))
35 swrdcl 14684 . . . . . . . . . . 11 ((𝐴𝐾) ∈ Word (𝐼 × 2o) → ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2o))
3634, 35syl 17 . . . . . . . . . 10 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2o))
37 ccatlen 14614 . . . . . . . . . 10 ((((𝐵𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2o)) → (♯‘(((𝐵𝐿) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))) = ((♯‘((𝐵𝐿) prefix 𝑄)) + (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))))
3832, 36, 37syl2anc 584 . . . . . . . . 9 (𝜑 → (♯‘(((𝐵𝐿) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))) = ((♯‘((𝐵𝐿) prefix 𝑄)) + (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))))
39 pfxlen 14722 . . . . . . . . . . . 12 (((𝐵𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(♯‘(𝐵𝐿)))) → (♯‘((𝐵𝐿) prefix 𝑄)) = 𝑄)
4030, 14, 39syl2anc 584 . . . . . . . . . . 11 (𝜑 → (♯‘((𝐵𝐿) prefix 𝑄)) = 𝑄)
41 2nn0 12545 . . . . . . . . . . . . . 14 2 ∈ ℕ0
42 uzaddcl 12947 . . . . . . . . . . . . . 14 ((𝑄 ∈ (ℤ‘0) ∧ 2 ∈ ℕ0) → (𝑄 + 2) ∈ (ℤ‘0))
4316, 41, 42sylancl 586 . . . . . . . . . . . . 13 (𝜑 → (𝑄 + 2) ∈ (ℤ‘0))
44 efgredlemb.p . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ (0...(♯‘(𝐴𝐾))))
45 elfzuz3 13562 . . . . . . . . . . . . . . 15 (𝑃 ∈ (0...(♯‘(𝐴𝐾))) → (♯‘(𝐴𝐾)) ∈ (ℤ𝑃))
4644, 45syl 17 . . . . . . . . . . . . . 14 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ𝑃))
47 efgredlemd.9 . . . . . . . . . . . . . 14 (𝜑𝑃 ∈ (ℤ‘(𝑄 + 2)))
48 uztrn 12897 . . . . . . . . . . . . . 14 (((♯‘(𝐴𝐾)) ∈ (ℤ𝑃) ∧ 𝑃 ∈ (ℤ‘(𝑄 + 2))) → (♯‘(𝐴𝐾)) ∈ (ℤ‘(𝑄 + 2)))
4946, 47, 48syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ‘(𝑄 + 2)))
50 elfzuzb 13559 . . . . . . . . . . . . 13 ((𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾))) ↔ ((𝑄 + 2) ∈ (ℤ‘0) ∧ (♯‘(𝐴𝐾)) ∈ (ℤ‘(𝑄 + 2))))
5143, 49, 50sylanbrc 583 . . . . . . . . . . . 12 (𝜑 → (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾))))
52 lencl 14572 . . . . . . . . . . . . . . 15 ((𝐴𝐾) ∈ Word (𝐼 × 2o) → (♯‘(𝐴𝐾)) ∈ ℕ0)
5334, 52syl 17 . . . . . . . . . . . . . 14 (𝜑 → (♯‘(𝐴𝐾)) ∈ ℕ0)
54 nn0uz 12921 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
5553, 54eleqtrdi 2850 . . . . . . . . . . . . 13 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ‘0))
56 eluzfz2 13573 . . . . . . . . . . . . 13 ((♯‘(𝐴𝐾)) ∈ (ℤ‘0) → (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾))))
5755, 56syl 17 . . . . . . . . . . . 12 (𝜑 → (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾))))
58 swrdlen 14686 . . . . . . . . . . . 12 (((𝐴𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾))) ∧ (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾)))) → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((♯‘(𝐴𝐾)) − (𝑄 + 2)))
5934, 51, 57, 58syl3anc 1372 . . . . . . . . . . 11 (𝜑 → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((♯‘(𝐴𝐾)) − (𝑄 + 2)))
6040, 59oveq12d 7450 . . . . . . . . . 10 (𝜑 → ((♯‘((𝐵𝐿) prefix 𝑄)) + (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))) = (𝑄 + ((♯‘(𝐴𝐾)) − (𝑄 + 2))))
6114elfzelzd 13566 . . . . . . . . . . . 12 (𝜑𝑄 ∈ ℤ)
6261zcnd 12725 . . . . . . . . . . 11 (𝜑𝑄 ∈ ℂ)
6353nn0cnd 12591 . . . . . . . . . . 11 (𝜑 → (♯‘(𝐴𝐾)) ∈ ℂ)
64 2z 12651 . . . . . . . . . . . . 13 2 ∈ ℤ
65 zaddcl 12659 . . . . . . . . . . . . 13 ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑄 + 2) ∈ ℤ)
6661, 64, 65sylancl 586 . . . . . . . . . . . 12 (𝜑 → (𝑄 + 2) ∈ ℤ)
6766zcnd 12725 . . . . . . . . . . 11 (𝜑 → (𝑄 + 2) ∈ ℂ)
6862, 63, 67addsubassd 11641 . . . . . . . . . 10 (𝜑 → ((𝑄 + (♯‘(𝐴𝐾))) − (𝑄 + 2)) = (𝑄 + ((♯‘(𝐴𝐾)) − (𝑄 + 2))))
69 2cn 12342 . . . . . . . . . . . 12 2 ∈ ℂ
7069a1i 11 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℂ)
7162, 63, 70pnpcand 11658 . . . . . . . . . 10 (𝜑 → ((𝑄 + (♯‘(𝐴𝐾))) − (𝑄 + 2)) = ((♯‘(𝐴𝐾)) − 2))
7260, 68, 713eqtr2d 2782 . . . . . . . . 9 (𝜑 → ((♯‘((𝐵𝐿) prefix 𝑄)) + (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))) = ((♯‘(𝐴𝐾)) − 2))
7318, 38, 723eqtrd 2780 . . . . . . . 8 (𝜑 → (♯‘(𝑆𝐶)) = ((♯‘(𝐴𝐾)) − 2))
7444elfzelzd 13566 . . . . . . . . . 10 (𝜑𝑃 ∈ ℤ)
75 zsubcl 12661 . . . . . . . . . 10 ((𝑃 ∈ ℤ ∧ 2 ∈ ℤ) → (𝑃 − 2) ∈ ℤ)
7674, 64, 75sylancl 586 . . . . . . . . 9 (𝜑 → (𝑃 − 2) ∈ ℤ)
7764a1i 11 . . . . . . . . 9 (𝜑 → 2 ∈ ℤ)
7874zcnd 12725 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℂ)
79 npcan 11518 . . . . . . . . . . . 12 ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑃 − 2) + 2) = 𝑃)
8078, 69, 79sylancl 586 . . . . . . . . . . 11 (𝜑 → ((𝑃 − 2) + 2) = 𝑃)
8180fveq2d 6909 . . . . . . . . . 10 (𝜑 → (ℤ‘((𝑃 − 2) + 2)) = (ℤ𝑃))
8246, 81eleqtrrd 2843 . . . . . . . . 9 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ‘((𝑃 − 2) + 2)))
83 eluzsub 12909 . . . . . . . . 9 (((𝑃 − 2) ∈ ℤ ∧ 2 ∈ ℤ ∧ (♯‘(𝐴𝐾)) ∈ (ℤ‘((𝑃 − 2) + 2))) → ((♯‘(𝐴𝐾)) − 2) ∈ (ℤ‘(𝑃 − 2)))
8476, 77, 82, 83syl3anc 1372 . . . . . . . 8 (𝜑 → ((♯‘(𝐴𝐾)) − 2) ∈ (ℤ‘(𝑃 − 2)))
8573, 84eqeltrd 2840 . . . . . . 7 (𝜑 → (♯‘(𝑆𝐶)) ∈ (ℤ‘(𝑃 − 2)))
86 eluzsub 12909 . . . . . . . 8 ((𝑄 ∈ ℤ ∧ 2 ∈ ℤ ∧ 𝑃 ∈ (ℤ‘(𝑄 + 2))) → (𝑃 − 2) ∈ (ℤ𝑄))
8761, 77, 47, 86syl3anc 1372 . . . . . . 7 (𝜑 → (𝑃 − 2) ∈ (ℤ𝑄))
88 uztrn 12897 . . . . . . 7 (((♯‘(𝑆𝐶)) ∈ (ℤ‘(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (ℤ𝑄)) → (♯‘(𝑆𝐶)) ∈ (ℤ𝑄))
8985, 87, 88syl2anc 584 . . . . . 6 (𝜑 → (♯‘(𝑆𝐶)) ∈ (ℤ𝑄))
90 elfzuzb 13559 . . . . . 6 (𝑄 ∈ (0...(♯‘(𝑆𝐶))) ↔ (𝑄 ∈ (ℤ‘0) ∧ (♯‘(𝑆𝐶)) ∈ (ℤ𝑄)))
9116, 89, 90sylanbrc 583 . . . . 5 (𝜑𝑄 ∈ (0...(♯‘(𝑆𝐶))))
92 efgredlemb.v . . . . 5 (𝜑𝑉 ∈ (𝐼 × 2o))
932, 3, 4, 5efgtval 19742 . . . . 5 (((𝑆𝐶) ∈ 𝑊𝑄 ∈ (0...(♯‘(𝑆𝐶))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝑆𝐶))𝑉) = ((𝑆𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
9413, 91, 92, 93syl3anc 1372 . . . 4 (𝜑 → (𝑄(𝑇‘(𝑆𝐶))𝑉) = ((𝑆𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
95 pfxcl 14716 . . . . . 6 ((𝐴𝐾) ∈ Word (𝐼 × 2o) → ((𝐴𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o))
9634, 95syl 17 . . . . 5 (𝜑 → ((𝐴𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o))
97 wrd0 14578 . . . . . 6 ∅ ∈ Word (𝐼 × 2o)
9897a1i 11 . . . . 5 (𝜑 → ∅ ∈ Word (𝐼 × 2o))
994efgmf 19732 . . . . . . . 8 𝑀:(𝐼 × 2o)⟶(𝐼 × 2o)
10099ffvelcdmi 7102 . . . . . . 7 (𝑉 ∈ (𝐼 × 2o) → (𝑀𝑉) ∈ (𝐼 × 2o))
10192, 100syl 17 . . . . . 6 (𝜑 → (𝑀𝑉) ∈ (𝐼 × 2o))
10292, 101s2cld 14911 . . . . 5 (𝜑 → ⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2o))
10361zred 12724 . . . . . . . . . . . . . . . . 17 (𝜑𝑄 ∈ ℝ)
104 nn0addge1 12574 . . . . . . . . . . . . . . . . 17 ((𝑄 ∈ ℝ ∧ 2 ∈ ℕ0) → 𝑄 ≤ (𝑄 + 2))
105103, 41, 104sylancl 586 . . . . . . . . . . . . . . . 16 (𝜑𝑄 ≤ (𝑄 + 2))
106 eluz2 12885 . . . . . . . . . . . . . . . 16 ((𝑄 + 2) ∈ (ℤ𝑄) ↔ (𝑄 ∈ ℤ ∧ (𝑄 + 2) ∈ ℤ ∧ 𝑄 ≤ (𝑄 + 2)))
10761, 66, 105, 106syl3anbrc 1343 . . . . . . . . . . . . . . 15 (𝜑 → (𝑄 + 2) ∈ (ℤ𝑄))
108 uztrn 12897 . . . . . . . . . . . . . . 15 ((𝑃 ∈ (ℤ‘(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (ℤ𝑄)) → 𝑃 ∈ (ℤ𝑄))
10947, 107, 108syl2anc 584 . . . . . . . . . . . . . 14 (𝜑𝑃 ∈ (ℤ𝑄))
110 elfzuzb 13559 . . . . . . . . . . . . . 14 (𝑄 ∈ (0...𝑃) ↔ (𝑄 ∈ (ℤ‘0) ∧ 𝑃 ∈ (ℤ𝑄)))
11116, 109, 110sylanbrc 583 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ (0...𝑃))
112 ccatpfx 14740 . . . . . . . . . . . . 13 (((𝐴𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾)))) → (((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴𝐾) prefix 𝑃))
11334, 111, 44, 112syl3anc 1372 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) = ((𝐴𝐾) prefix 𝑃))
114113oveq1d 7447 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))))
115 pfxcl 14716 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2o) → ((𝐴𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o))
11634, 115syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o))
117 efgredlemb.u . . . . . . . . . . . . 13 (𝜑𝑈 ∈ (𝐼 × 2o))
11899ffvelcdmi 7102 . . . . . . . . . . . . . 14 (𝑈 ∈ (𝐼 × 2o) → (𝑀𝑈) ∈ (𝐼 × 2o))
119117, 118syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑀𝑈) ∈ (𝐼 × 2o))
120117, 119s2cld 14911 . . . . . . . . . . . 12 (𝜑 → ⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2o))
121 swrdcl 14684 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2o) → ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2o))
12234, 121syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2o))
123 ccatass 14627 . . . . . . . . . . . 12 ((((𝐴𝐾) prefix 𝑃) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2o)) → ((((𝐴𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐴𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))))
124116, 120, 122, 123syl3anc 1372 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐴𝐾) prefix 𝑃) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))))
125 efgredlemb.6 . . . . . . . . . . . . 13 (𝜑 → (𝑆𝐴) = (𝑃(𝑇‘(𝐴𝐾))𝑈))
1262, 3, 4, 5efgtval 19742 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ 𝑊𝑃 ∈ (0...(♯‘(𝐴𝐾))) ∧ 𝑈 ∈ (𝐼 × 2o)) → (𝑃(𝑇‘(𝐴𝐾))𝑈) = ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩))
12733, 44, 117, 126syl3anc 1372 . . . . . . . . . . . . 13 (𝜑 → (𝑃(𝑇‘(𝐴𝐾))𝑈) = ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩))
128 splval 14790 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ 𝑊 ∧ (𝑃 ∈ (0...(♯‘(𝐴𝐾))) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾))) ∧ ⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2o))) → ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩) = ((((𝐴𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))
12933, 44, 44, 120, 128syl13anc 1373 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝐾) splice ⟨𝑃, 𝑃, ⟨“𝑈(𝑀𝑈)”⟩⟩) = ((((𝐴𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))
130125, 127, 1293eqtrd 2780 . . . . . . . . . . . 12 (𝜑 → (𝑆𝐴) = ((((𝐴𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))
131 efgredlemb.7 . . . . . . . . . . . . 13 (𝜑 → (𝑆𝐵) = (𝑄(𝑇‘(𝐵𝐿))𝑉))
1322, 3, 4, 5efgtval 19742 . . . . . . . . . . . . . 14 (((𝐵𝐿) ∈ 𝑊𝑄 ∈ (0...(♯‘(𝐵𝐿))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝐵𝐿))𝑉) = ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
13329, 14, 92, 132syl3anc 1372 . . . . . . . . . . . . 13 (𝜑 → (𝑄(𝑇‘(𝐵𝐿))𝑉) = ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩))
134 splval 14790 . . . . . . . . . . . . . 14 (((𝐵𝐿) ∈ 𝑊 ∧ (𝑄 ∈ (0...(♯‘(𝐵𝐿))) ∧ 𝑄 ∈ (0...(♯‘(𝐵𝐿))) ∧ ⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2o))) → ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩) = ((((𝐵𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
13529, 14, 14, 102, 134syl13anc 1373 . . . . . . . . . . . . 13 (𝜑 → ((𝐵𝐿) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩) = ((((𝐵𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
136131, 133, 1353eqtrd 2780 . . . . . . . . . . . 12 (𝜑 → (𝑆𝐵) = ((((𝐵𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
13724, 130, 1363eqtr3d 2784 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) prefix 𝑃) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((((𝐵𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
138114, 124, 1373eqtr2d 2782 . . . . . . . . . 10 (𝜑 → ((((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = ((((𝐵𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
139 swrdcl 14684 . . . . . . . . . . . 12 ((𝐴𝐾) ∈ Word (𝐼 × 2o) → ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o))
14034, 139syl 17 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o))
141 ccatcl 14613 . . . . . . . . . . . 12 ((⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2o)) → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2o))
142120, 122, 141syl2anc 584 . . . . . . . . . . 11 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2o))
143 ccatass 14627 . . . . . . . . . . 11 ((((𝐴𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2o)) → ((((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) prefix 𝑄) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))))
14496, 140, 142, 143syl3anc 1372 . . . . . . . . . 10 (𝜑 → ((((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) prefix 𝑄) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))))
145 swrdcl 14684 . . . . . . . . . . . 12 ((𝐵𝐿) ∈ Word (𝐼 × 2o) → ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o))
14630, 145syl 17 . . . . . . . . . . 11 (𝜑 → ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o))
147 ccatass 14627 . . . . . . . . . . 11 ((((𝐵𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o)) → ((((𝐵𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
14832, 102, 146, 147syl3anc 1372 . . . . . . . . . 10 (𝜑 → ((((𝐵𝐿) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
149138, 144, 1483eqtr3d 2784 . . . . . . . . 9 (𝜑 → (((𝐴𝐾) prefix 𝑄) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))) = (((𝐵𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
150 ccatcl 14613 . . . . . . . . . . 11 ((((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2o)) → (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2o))
151140, 142, 150syl2anc 584 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2o))
152 ccatcl 14613 . . . . . . . . . . 11 ((⟨“𝑉(𝑀𝑉)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o)) → (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) ∈ Word (𝐼 × 2o))
153102, 146, 152syl2anc 584 . . . . . . . . . 10 (𝜑 → (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) ∈ Word (𝐼 × 2o))
154 uztrn 12897 . . . . . . . . . . . . . 14 (((♯‘(𝐴𝐾)) ∈ (ℤ𝑃) ∧ 𝑃 ∈ (ℤ𝑄)) → (♯‘(𝐴𝐾)) ∈ (ℤ𝑄))
15546, 109, 154syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → (♯‘(𝐴𝐾)) ∈ (ℤ𝑄))
156 elfzuzb 13559 . . . . . . . . . . . . 13 (𝑄 ∈ (0...(♯‘(𝐴𝐾))) ↔ (𝑄 ∈ (ℤ‘0) ∧ (♯‘(𝐴𝐾)) ∈ (ℤ𝑄)))
15716, 155, 156sylanbrc 583 . . . . . . . . . . . 12 (𝜑𝑄 ∈ (0...(♯‘(𝐴𝐾))))
158 pfxlen 14722 . . . . . . . . . . . 12 (((𝐴𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(♯‘(𝐴𝐾)))) → (♯‘((𝐴𝐾) prefix 𝑄)) = 𝑄)
15934, 157, 158syl2anc 584 . . . . . . . . . . 11 (𝜑 → (♯‘((𝐴𝐾) prefix 𝑄)) = 𝑄)
160159, 40eqtr4d 2779 . . . . . . . . . 10 (𝜑 → (♯‘((𝐴𝐾) prefix 𝑄)) = (♯‘((𝐵𝐿) prefix 𝑄)))
161 ccatopth 14755 . . . . . . . . . 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 ⟨𝑄, (♯‘(𝐵𝐿))⟩)))))
16296, 151, 32, 153, 160, 161syl221anc 1382 . . . . . . . . 9 (𝜑 → ((((𝐴𝐾) prefix 𝑄) ++ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))) = (((𝐵𝐿) prefix 𝑄) ++ (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))) ↔ (((𝐴𝐾) prefix 𝑄) = ((𝐵𝐿) prefix 𝑄) ∧ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))))
163149, 162mpbid 232 . . . . . . . 8 (𝜑 → (((𝐴𝐾) prefix 𝑄) = ((𝐵𝐿) prefix 𝑄) ∧ (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
164163simpld 494 . . . . . . 7 (𝜑 → ((𝐴𝐾) prefix 𝑄) = ((𝐵𝐿) prefix 𝑄))
165164oveq1d 7447 . . . . . 6 (𝜑 → (((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
166 ccatrid 14626 . . . . . . . 8 (((𝐴𝐾) prefix 𝑄) ∈ Word (𝐼 × 2o) → (((𝐴𝐾) prefix 𝑄) ++ ∅) = ((𝐴𝐾) prefix 𝑄))
16796, 166syl 17 . . . . . . 7 (𝜑 → (((𝐴𝐾) prefix 𝑄) ++ ∅) = ((𝐴𝐾) prefix 𝑄))
168167oveq1d 7447 . . . . . 6 (𝜑 → ((((𝐴𝐾) prefix 𝑄) ++ ∅) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
169165, 168, 173eqtr4rd 2787 . . . . 5 (𝜑 → (𝑆𝐶) = ((((𝐴𝐾) prefix 𝑄) ++ ∅) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
170159eqcomd 2742 . . . . 5 (𝜑𝑄 = (♯‘((𝐴𝐾) prefix 𝑄)))
171 hash0 14407 . . . . . . 7 (♯‘∅) = 0
172171oveq2i 7443 . . . . . 6 (𝑄 + (♯‘∅)) = (𝑄 + 0)
17362addridd 11462 . . . . . 6 (𝜑 → (𝑄 + 0) = 𝑄)
174172, 173eqtr2id 2789 . . . . 5 (𝜑𝑄 = (𝑄 + (♯‘∅)))
17596, 98, 36, 102, 169, 170, 174splval2 14796 . . . 4 (𝜑 → ((𝑆𝐶) splice ⟨𝑄, 𝑄, ⟨“𝑉(𝑀𝑉)”⟩⟩) = ((((𝐴𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
176 elfzuzb 13559 . . . . . . . . . . . . . 14 (𝑄 ∈ (0...(𝑄 + 2)) ↔ (𝑄 ∈ (ℤ‘0) ∧ (𝑄 + 2) ∈ (ℤ𝑄)))
17716, 107, 176sylanbrc 583 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ (0...(𝑄 + 2)))
178 elfzuzb 13559 . . . . . . . . . . . . . 14 ((𝑄 + 2) ∈ (0...𝑃) ↔ ((𝑄 + 2) ∈ (ℤ‘0) ∧ 𝑃 ∈ (ℤ‘(𝑄 + 2))))
17943, 47, 178sylanbrc 583 . . . . . . . . . . . . 13 (𝜑 → (𝑄 + 2) ∈ (0...𝑃))
180 ccatswrd 14707 . . . . . . . . . . . . 13 (((𝐴𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩))
18134, 177, 179, 44, 180syl13anc 1373 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = ((𝐴𝐾) substr ⟨𝑄, 𝑃⟩))
182181oveq1d 7447 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))))
183 swrdcl 14684 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2o) → ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2o))
18434, 183syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2o))
185 swrdcl 14684 . . . . . . . . . . . . 13 ((𝐴𝐾) ∈ Word (𝐼 × 2o) → ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
18634, 185syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
187 ccatass 14627 . . . . . . . . . . . 12 ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ∈ Word (𝐼 × 2o) ∧ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2o)) → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))))
188184, 186, 142, 187syl3anc 1372 . . . . . . . . . . 11 (𝜑 → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))))
189163simprd 495 . . . . . . . . . . 11 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
190182, 188, 1893eqtr3d 2784 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
191 ccatcl 14613 . . . . . . . . . . . 12 ((((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) ∈ Word (𝐼 × 2o)) → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2o))
192186, 142, 191syl2anc 584 . . . . . . . . . . 11 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) ∈ Word (𝐼 × 2o))
193 swrdlen 14686 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾)))) → (♯‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
19434, 177, 51, 193syl3anc 1372 . . . . . . . . . . . . 13 (𝜑 → (♯‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝑄 + 2) − 𝑄))
195 pncan2 11516 . . . . . . . . . . . . . 14 ((𝑄 ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑄 + 2) − 𝑄) = 2)
19662, 69, 195sylancl 586 . . . . . . . . . . . . 13 (𝜑 → ((𝑄 + 2) − 𝑄) = 2)
197194, 196eqtrd 2776 . . . . . . . . . . . 12 (𝜑 → (♯‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = 2)
198 s2len 14929 . . . . . . . . . . . 12 (♯‘⟨“𝑉(𝑀𝑉)”⟩) = 2
199197, 198eqtr4di 2794 . . . . . . . . . . 11 (𝜑 → (♯‘((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (♯‘⟨“𝑉(𝑀𝑉)”⟩))
200 ccatopth 14755 . . . . . . . . . . 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 ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
201184, 192, 102, 146, 199, 200syl221anc 1382 . . . . . . . . . 10 (𝜑 → ((((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) ++ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)))) = (⟨“𝑉(𝑀𝑉)”⟩ ++ ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)) ↔ (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩ ∧ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))))
202190, 201mpbid 232 . . . . . . . . 9 (𝜑 → (((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩ ∧ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩)))
203202simpld 494 . . . . . . . 8 (𝜑 → ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩) = ⟨“𝑉(𝑀𝑉)”⟩)
204203oveq2d 7448 . . . . . . 7 (𝜑 → (((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = (((𝐴𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩))
205 ccatpfx 14740 . . . . . . . 8 (((𝐴𝐾) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾)))) → (((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴𝐾) prefix (𝑄 + 2)))
20634, 177, 51, 205syl3anc 1372 . . . . . . 7 (𝜑 → (((𝐴𝐾) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨𝑄, (𝑄 + 2)⟩)) = ((𝐴𝐾) prefix (𝑄 + 2)))
207204, 206eqtr3d 2778 . . . . . 6 (𝜑 → (((𝐴𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) = ((𝐴𝐾) prefix (𝑄 + 2)))
208207oveq1d 7447 . . . . 5 (𝜑 → ((((𝐴𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (((𝐴𝐾) prefix (𝑄 + 2)) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)))
209 ccatpfx 14740 . . . . . 6 (((𝐴𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈ (0...(♯‘(𝐴𝐾))) ∧ (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾)))) → (((𝐴𝐾) prefix (𝑄 + 2)) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((𝐴𝐾) prefix (♯‘(𝐴𝐾))))
21034, 51, 57, 209syl3anc 1372 . . . . 5 (𝜑 → (((𝐴𝐾) prefix (𝑄 + 2)) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((𝐴𝐾) prefix (♯‘(𝐴𝐾))))
211 pfxid 14723 . . . . . 6 ((𝐴𝐾) ∈ Word (𝐼 × 2o) → ((𝐴𝐾) prefix (♯‘(𝐴𝐾))) = (𝐴𝐾))
21234, 211syl 17 . . . . 5 (𝜑 → ((𝐴𝐾) prefix (♯‘(𝐴𝐾))) = (𝐴𝐾))
213208, 210, 2123eqtrd 2780 . . . 4 (𝜑 → ((((𝐴𝐾) prefix 𝑄) ++ ⟨“𝑉(𝑀𝑉)”⟩) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (𝐴𝐾))
21494, 175, 2133eqtrd 2780 . . 3 (𝜑 → (𝑄(𝑇‘(𝑆𝐶))𝑉) = (𝐴𝐾))
2152, 3, 4, 5efgtf 19741 . . . . . . 7 ((𝑆𝐶) ∈ 𝑊 → ((𝑇‘(𝑆𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆𝐶))), 𝑖 ∈ (𝐼 × 2o) ↦ ((𝑆𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐶)):((0...(♯‘(𝑆𝐶))) × (𝐼 × 2o))⟶𝑊))
21613, 215syl 17 . . . . . 6 (𝜑 → ((𝑇‘(𝑆𝐶)) = (𝑎 ∈ (0...(♯‘(𝑆𝐶))), 𝑖 ∈ (𝐼 × 2o) ↦ ((𝑆𝐶) splice ⟨𝑎, 𝑎, ⟨“𝑖(𝑀𝑖)”⟩⟩)) ∧ (𝑇‘(𝑆𝐶)):((0...(♯‘(𝑆𝐶))) × (𝐼 × 2o))⟶𝑊))
217216simprd 495 . . . . 5 (𝜑 → (𝑇‘(𝑆𝐶)):((0...(♯‘(𝑆𝐶))) × (𝐼 × 2o))⟶𝑊)
218217ffnd 6736 . . . 4 (𝜑 → (𝑇‘(𝑆𝐶)) Fn ((0...(♯‘(𝑆𝐶))) × (𝐼 × 2o)))
219 fnovrn 7609 . . . 4 (((𝑇‘(𝑆𝐶)) Fn ((0...(♯‘(𝑆𝐶))) × (𝐼 × 2o)) ∧ 𝑄 ∈ (0...(♯‘(𝑆𝐶))) ∧ 𝑉 ∈ (𝐼 × 2o)) → (𝑄(𝑇‘(𝑆𝐶))𝑉) ∈ ran (𝑇‘(𝑆𝐶)))
220218, 91, 92, 219syl3anc 1372 . . 3 (𝜑 → (𝑄(𝑇‘(𝑆𝐶))𝑉) ∈ ran (𝑇‘(𝑆𝐶)))
221214, 220eqeltrrd 2841 . 2 (𝜑 → (𝐴𝐾) ∈ ran (𝑇‘(𝑆𝐶)))
222 uztrn 12897 . . . . . . 7 (((𝑃 − 2) ∈ (ℤ𝑄) ∧ 𝑄 ∈ (ℤ‘0)) → (𝑃 − 2) ∈ (ℤ‘0))
22387, 16, 222syl2anc 584 . . . . . 6 (𝜑 → (𝑃 − 2) ∈ (ℤ‘0))
224 elfzuzb 13559 . . . . . 6 ((𝑃 − 2) ∈ (0...(♯‘(𝑆𝐶))) ↔ ((𝑃 − 2) ∈ (ℤ‘0) ∧ (♯‘(𝑆𝐶)) ∈ (ℤ‘(𝑃 − 2))))
225223, 85, 224sylanbrc 583 . . . . 5 (𝜑 → (𝑃 − 2) ∈ (0...(♯‘(𝑆𝐶))))
2262, 3, 4, 5efgtval 19742 . . . . 5 (((𝑆𝐶) ∈ 𝑊 ∧ (𝑃 − 2) ∈ (0...(♯‘(𝑆𝐶))) ∧ 𝑈 ∈ (𝐼 × 2o)) → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) = ((𝑆𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀𝑈)”⟩⟩))
22713, 225, 117, 226syl3anc 1372 . . . 4 (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) = ((𝑆𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀𝑈)”⟩⟩))
228 pfxcl 14716 . . . . . 6 ((𝐵𝐿) ∈ Word (𝐼 × 2o) → ((𝐵𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o))
22930, 228syl 17 . . . . 5 (𝜑 → ((𝐵𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o))
230 swrdcl 14684 . . . . . 6 ((𝐵𝐿) ∈ Word (𝐼 × 2o) → ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o))
23130, 230syl 17 . . . . 5 (𝜑 → ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o))
232 ccatswrd 14707 . . . . . . . . . . 11 (((𝐴𝐾) ∈ Word (𝐼 × 2o) ∧ ((𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾))) ∧ (♯‘(𝐴𝐾)) ∈ (0...(♯‘(𝐴𝐾))))) → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))
23334, 179, 44, 57, 232syl13anc 1373 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩))
234202simprd 495 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))
235 elfzuzb 13559 . . . . . . . . . . . . . . . 16 (𝑄 ∈ (0...(𝑃 − 2)) ↔ (𝑄 ∈ (ℤ‘0) ∧ (𝑃 − 2) ∈ (ℤ𝑄)))
23616, 87, 235sylanbrc 583 . . . . . . . . . . . . . . 15 (𝜑𝑄 ∈ (0...(𝑃 − 2)))
2372, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27, 44, 14, 117, 92, 125, 131efgredlemg 19761 . . . . . . . . . . . . . . . . . 18 (𝜑 → (♯‘(𝐴𝐾)) = (♯‘(𝐵𝐿)))
238237, 46eqeltrrd 2841 . . . . . . . . . . . . . . . . 17 (𝜑 → (♯‘(𝐵𝐿)) ∈ (ℤ𝑃))
239 0le2 12369 . . . . . . . . . . . . . . . . . . . 20 0 ≤ 2
240239a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ≤ 2)
24174zred 12724 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑃 ∈ ℝ)
242 2re 12341 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
243 subge02 11780 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℝ ∧ 2 ∈ ℝ) → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
244241, 242, 243sylancl 586 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (0 ≤ 2 ↔ (𝑃 − 2) ≤ 𝑃))
245240, 244mpbid 232 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑃 − 2) ≤ 𝑃)
246 eluz2 12885 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ (ℤ‘(𝑃 − 2)) ↔ ((𝑃 − 2) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑃 − 2) ≤ 𝑃))
24776, 74, 245, 246syl3anbrc 1343 . . . . . . . . . . . . . . . . 17 (𝜑𝑃 ∈ (ℤ‘(𝑃 − 2)))
248 uztrn 12897 . . . . . . . . . . . . . . . . 17 (((♯‘(𝐵𝐿)) ∈ (ℤ𝑃) ∧ 𝑃 ∈ (ℤ‘(𝑃 − 2))) → (♯‘(𝐵𝐿)) ∈ (ℤ‘(𝑃 − 2)))
249238, 247, 248syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘(𝐵𝐿)) ∈ (ℤ‘(𝑃 − 2)))
250 elfzuzb 13559 . . . . . . . . . . . . . . . 16 ((𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿))) ↔ ((𝑃 − 2) ∈ (ℤ‘0) ∧ (♯‘(𝐵𝐿)) ∈ (ℤ‘(𝑃 − 2))))
251223, 249, 250sylanbrc 583 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿))))
252 lencl 14572 . . . . . . . . . . . . . . . . . 18 ((𝐵𝐿) ∈ Word (𝐼 × 2o) → (♯‘(𝐵𝐿)) ∈ ℕ0)
25330, 252syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (♯‘(𝐵𝐿)) ∈ ℕ0)
254253, 54eleqtrdi 2850 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘(𝐵𝐿)) ∈ (ℤ‘0))
255 eluzfz2 13573 . . . . . . . . . . . . . . . 16 ((♯‘(𝐵𝐿)) ∈ (ℤ‘0) → (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿))))
256254, 255syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿))))
257 ccatswrd 14707 . . . . . . . . . . . . . . 15 (((𝐵𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿))) ∧ (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))
25830, 236, 251, 256, 257syl13anc 1373 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨𝑄, (♯‘(𝐵𝐿))⟩))
259234, 258eqtr4d 2779 . . . . . . . . . . . . 13 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩)))
260 swrdcl 14684 . . . . . . . . . . . . . . 15 ((𝐵𝐿) ∈ Word (𝐼 × 2o) → ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2o))
26130, 260syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2o))
262 swrdcl 14684 . . . . . . . . . . . . . . 15 ((𝐵𝐿) ∈ Word (𝐼 × 2o) → ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o))
26330, 262syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o))
264 swrdlen 14686 . . . . . . . . . . . . . . . 16 (((𝐴𝐾) ∈ Word (𝐼 × 2o) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐴𝐾)))) → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
26534, 179, 44, 264syl3anc 1372 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (𝑃 − (𝑄 + 2)))
266 swrdlen 14686 . . . . . . . . . . . . . . . . 17 (((𝐵𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿)))) → (♯‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
26730, 236, 251, 266syl3anc 1372 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝑃 − 2) − 𝑄))
26878, 62, 70sub32d 11653 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑃𝑄) − 2) = ((𝑃 − 2) − 𝑄))
26978, 62, 70subsub4d 11652 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑃𝑄) − 2) = (𝑃 − (𝑄 + 2)))
270267, 268, 2693eqtr2d 2782 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = (𝑃 − (𝑄 + 2)))
271265, 270eqtr4d 2779 . . . . . . . . . . . . . 14 (𝜑 → (♯‘((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩)) = (♯‘((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)))
272 ccatopth 14755 . . . . . . . . . . . . . 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), (♯‘(𝐵𝐿))⟩))))
273186, 142, 261, 263, 271, 272syl221anc 1382 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩))) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩)) ↔ (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩))))
274259, 273mpbid 232 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∧ (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩)))
275274simpld 494 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) = ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩))
276274simprd 495 . . . . . . . . . . . . . 14 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩))
277 elfzuzb 13559 . . . . . . . . . . . . . . . 16 ((𝑃 − 2) ∈ (0...𝑃) ↔ ((𝑃 − 2) ∈ (ℤ‘0) ∧ 𝑃 ∈ (ℤ‘(𝑃 − 2))))
278223, 247, 277sylanbrc 583 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃 − 2) ∈ (0...𝑃))
279 elfzuz 13561 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ (0...(♯‘(𝐴𝐾))) → 𝑃 ∈ (ℤ‘0))
28044, 279syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑃 ∈ (ℤ‘0))
281 elfzuzb 13559 . . . . . . . . . . . . . . . 16 (𝑃 ∈ (0...(♯‘(𝐵𝐿))) ↔ (𝑃 ∈ (ℤ‘0) ∧ (♯‘(𝐵𝐿)) ∈ (ℤ𝑃)))
282280, 238, 281sylanbrc 583 . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ (0...(♯‘(𝐵𝐿))))
283 ccatswrd 14707 . . . . . . . . . . . . . . 15 (((𝐵𝐿) ∈ Word (𝐼 × 2o) ∧ ((𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵𝐿))) ∧ (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿))))) → (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩))
28430, 278, 282, 256, 283syl13anc 1373 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) substr ⟨(𝑃 − 2), (♯‘(𝐵𝐿))⟩))
285276, 284eqtr4d 2779 . . . . . . . . . . . . 13 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
286 swrdcl 14684 . . . . . . . . . . . . . . 15 ((𝐵𝐿) ∈ Word (𝐼 × 2o) → ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
28730, 286syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2o))
288 s2len 14929 . . . . . . . . . . . . . . 15 (♯‘⟨“𝑈(𝑀𝑈)”⟩) = 2
289 swrdlen 14686 . . . . . . . . . . . . . . . . 17 (((𝐵𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵𝐿)))) → (♯‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
29030, 278, 282, 289syl3anc 1372 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = (𝑃 − (𝑃 − 2)))
291 nncan 11539 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑃 − (𝑃 − 2)) = 2)
29278, 69, 291sylancl 586 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃 − (𝑃 − 2)) = 2)
293290, 292eqtr2d 2777 . . . . . . . . . . . . . . 15 (𝜑 → 2 = (♯‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
294288, 293eqtrid 2788 . . . . . . . . . . . . . 14 (𝜑 → (♯‘⟨“𝑈(𝑀𝑈)”⟩) = (♯‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
295 ccatopth 14755 . . . . . . . . . . . . . 14 (((⟨“𝑈(𝑀𝑈)”⟩ ∈ Word (𝐼 × 2o) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) ∈ Word (𝐼 × 2o)) ∧ (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∈ Word (𝐼 × 2o) ∧ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o)) ∧ (♯‘⟨“𝑈(𝑀𝑈)”⟩) = (♯‘((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩))) → ((⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) ↔ (⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))))
296120, 122, 287, 231, 294, 295syl221anc 1382 . . . . . . . . . . . . 13 (𝜑 → ((⟨“𝑈(𝑀𝑈)”⟩ ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) ↔ (⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))))
297285, 296mpbid 232 . . . . . . . . . . . 12 (𝜑 → (⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩) ∧ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
298297simprd 495 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩) = ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))
299275, 298oveq12d 7450 . . . . . . . . . 10 (𝜑 → (((𝐴𝐾) substr ⟨(𝑄 + 2), 𝑃⟩) ++ ((𝐴𝐾) substr ⟨𝑃, (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
300233, 299eqtr3d 2778 . . . . . . . . 9 (𝜑 → ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩) = (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
301300oveq2d 7448 . . . . . . . 8 (𝜑 → (((𝐵𝐿) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = (((𝐵𝐿) prefix 𝑄) ++ (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))))
302 ccatass 14627 . . . . . . . . 9 ((((𝐵𝐿) prefix 𝑄) ∈ Word (𝐼 × 2o) ∧ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ∈ Word (𝐼 × 2o) ∧ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩) ∈ Word (𝐼 × 2o)) → ((((𝐵𝐿) prefix 𝑄) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) prefix 𝑄) ++ (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))))
30332, 261, 231, 302syl3anc 1372 . . . . . . . 8 (𝜑 → ((((𝐵𝐿) prefix 𝑄) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) prefix 𝑄) ++ (((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩))))
304301, 303eqtr4d 2779 . . . . . . 7 (𝜑 → (((𝐵𝐿) prefix 𝑄) ++ ((𝐴𝐾) substr ⟨(𝑄 + 2), (♯‘(𝐴𝐾))⟩)) = ((((𝐵𝐿) prefix 𝑄) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
305 ccatpfx 14740 . . . . . . . . 9 (((𝐵𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑄 ∈ (0...(𝑃 − 2)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿)))) → (((𝐵𝐿) prefix 𝑄) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵𝐿) prefix (𝑃 − 2)))
30630, 236, 251, 305syl3anc 1372 . . . . . . . 8 (𝜑 → (((𝐵𝐿) prefix 𝑄) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) = ((𝐵𝐿) prefix (𝑃 − 2)))
307306oveq1d 7447 . . . . . . 7 (𝜑 → ((((𝐵𝐿) prefix 𝑄) ++ ((𝐵𝐿) substr ⟨𝑄, (𝑃 − 2)⟩)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) prefix (𝑃 − 2)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
30817, 304, 3073eqtrd 2780 . . . . . 6 (𝜑 → (𝑆𝐶) = (((𝐵𝐿) prefix (𝑃 − 2)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
309 ccatrid 14626 . . . . . . . 8 (((𝐵𝐿) prefix (𝑃 − 2)) ∈ Word (𝐼 × 2o) → (((𝐵𝐿) prefix (𝑃 − 2)) ++ ∅) = ((𝐵𝐿) prefix (𝑃 − 2)))
310229, 309syl 17 . . . . . . 7 (𝜑 → (((𝐵𝐿) prefix (𝑃 − 2)) ++ ∅) = ((𝐵𝐿) prefix (𝑃 − 2)))
311310oveq1d 7447 . . . . . 6 (𝜑 → ((((𝐵𝐿) prefix (𝑃 − 2)) ++ ∅) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) prefix (𝑃 − 2)) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
312308, 311eqtr4d 2779 . . . . 5 (𝜑 → (𝑆𝐶) = ((((𝐵𝐿) prefix (𝑃 − 2)) ++ ∅) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
313 pfxlen 14722 . . . . . . 7 (((𝐵𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝐵𝐿)))) → (♯‘((𝐵𝐿) prefix (𝑃 − 2))) = (𝑃 − 2))
31430, 251, 313syl2anc 584 . . . . . 6 (𝜑 → (♯‘((𝐵𝐿) prefix (𝑃 − 2))) = (𝑃 − 2))
315314eqcomd 2742 . . . . 5 (𝜑 → (𝑃 − 2) = (♯‘((𝐵𝐿) prefix (𝑃 − 2))))
316171oveq2i 7443 . . . . . 6 ((𝑃 − 2) + (♯‘∅)) = ((𝑃 − 2) + 0)
31776zcnd 12725 . . . . . . 7 (𝜑 → (𝑃 − 2) ∈ ℂ)
318317addridd 11462 . . . . . 6 (𝜑 → ((𝑃 − 2) + 0) = (𝑃 − 2))
319316, 318eqtr2id 2789 . . . . 5 (𝜑 → (𝑃 − 2) = ((𝑃 − 2) + (♯‘∅)))
320229, 98, 231, 120, 312, 315, 319splval2 14796 . . . 4 (𝜑 → ((𝑆𝐶) splice ⟨(𝑃 − 2), (𝑃 − 2), ⟨“𝑈(𝑀𝑈)”⟩⟩) = ((((𝐵𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
321297simpld 494 . . . . . . . 8 (𝜑 → ⟨“𝑈(𝑀𝑈)”⟩ = ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩))
322321oveq2d 7448 . . . . . . 7 (𝜑 → (((𝐵𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀𝑈)”⟩) = (((𝐵𝐿) prefix (𝑃 − 2)) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)))
323 ccatpfx 14740 . . . . . . . 8 (((𝐵𝐿) ∈ Word (𝐼 × 2o) ∧ (𝑃 − 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(♯‘(𝐵𝐿)))) → (((𝐵𝐿) prefix (𝑃 − 2)) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵𝐿) prefix 𝑃))
32430, 278, 282, 323syl3anc 1372 . . . . . . 7 (𝜑 → (((𝐵𝐿) prefix (𝑃 − 2)) ++ ((𝐵𝐿) substr ⟨(𝑃 − 2), 𝑃⟩)) = ((𝐵𝐿) prefix 𝑃))
325322, 324eqtrd 2776 . . . . . 6 (𝜑 → (((𝐵𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀𝑈)”⟩) = ((𝐵𝐿) prefix 𝑃))
326325oveq1d 7447 . . . . 5 (𝜑 → ((((𝐵𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (((𝐵𝐿) prefix 𝑃) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)))
327 ccatpfx 14740 . . . . . 6 (((𝐵𝐿) ∈ Word (𝐼 × 2o) ∧ 𝑃 ∈ (0...(♯‘(𝐵𝐿))) ∧ (♯‘(𝐵𝐿)) ∈ (0...(♯‘(𝐵𝐿)))) → (((𝐵𝐿) prefix 𝑃) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) prefix (♯‘(𝐵𝐿))))
32830, 282, 256, 327syl3anc 1372 . . . . 5 (𝜑 → (((𝐵𝐿) prefix 𝑃) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = ((𝐵𝐿) prefix (♯‘(𝐵𝐿))))
329 pfxid 14723 . . . . . 6 ((𝐵𝐿) ∈ Word (𝐼 × 2o) → ((𝐵𝐿) prefix (♯‘(𝐵𝐿))) = (𝐵𝐿))
33030, 329syl 17 . . . . 5 (𝜑 → ((𝐵𝐿) prefix (♯‘(𝐵𝐿))) = (𝐵𝐿))
331326, 328, 3303eqtrd 2780 . . . 4 (𝜑 → ((((𝐵𝐿) prefix (𝑃 − 2)) ++ ⟨“𝑈(𝑀𝑈)”⟩) ++ ((𝐵𝐿) substr ⟨𝑃, (♯‘(𝐵𝐿))⟩)) = (𝐵𝐿))
332227, 320, 3313eqtrd 2780 . . 3 (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) = (𝐵𝐿))
333 fnovrn 7609 . . . 4 (((𝑇‘(𝑆𝐶)) Fn ((0...(♯‘(𝑆𝐶))) × (𝐼 × 2o)) ∧ (𝑃 − 2) ∈ (0...(♯‘(𝑆𝐶))) ∧ 𝑈 ∈ (𝐼 × 2o)) → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) ∈ ran (𝑇‘(𝑆𝐶)))
334218, 225, 117, 333syl3anc 1372 . . 3 (𝜑 → ((𝑃 − 2)(𝑇‘(𝑆𝐶))𝑈) ∈ ran (𝑇‘(𝑆𝐶)))
335332, 334eqeltrrd 2841 . 2 (𝜑 → (𝐵𝐿) ∈ ran (𝑇‘(𝑆𝐶)))
336221, 335jca 511 1 (𝜑 → ((𝐴𝐾) ∈ ran (𝑇‘(𝑆𝐶)) ∧ (𝐵𝐿) ∈ ran (𝑇‘(𝑆𝐶))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1539  wcel 2107  wral 3060  {crab 3435  cdif 3947  c0 4332  {csn 4625  cop 4631  cotp 4633   ciun 4990   class class class wbr 5142  cmpt 5224   I cid 5576   × cxp 5682  dom cdm 5684  ran crn 5685   Fn wfn 6555  wf 6556  cfv 6560  (class class class)co 7432  cmpo 7434  1oc1o 8500  2oc2o 8501  cc 11154  cr 11155  0cc0 11156  1c1 11157   + caddc 11159   < clt 11296  cle 11297  cmin 11493  2c2 12322  0cn0 12528  cz 12615  cuz 12879  ...cfz 13548  ..^cfzo 13695  chash 14370  Word cword 14553   ++ cconcat 14609   substr csubstr 14679   prefix cpfx 14709   splice csplice 14788  ⟨“cs2 14881   ~FG cefg 19725
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-ot 4634  df-uni 4907  df-int 4946  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1st 8015  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-2o 8508  df-er 8746  df-map 8869  df-en 8987  df-dom 8988  df-sdom 8989  df-fin 8990  df-card 9980  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-nn 12268  df-2 12330  df-n0 12529  df-z 12616  df-uz 12880  df-fz 13549  df-fzo 13696  df-hash 14371  df-word 14554  df-concat 14610  df-s1 14635  df-substr 14680  df-pfx 14710  df-splice 14789  df-s2 14888
This theorem is referenced by:  efgredlemd  19763
  Copyright terms: Public domain W3C validator