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

Theorem efgredleme 19611
Description: Lemma for efgred 19616. (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 19597 . . . . . . . 8 𝑆:{𝑑 ∈ (Word π‘Š βˆ– {βˆ…}) ∣ ((π‘‘β€˜0) ∈ 𝐷 ∧ βˆ€π‘˜ ∈ (1..^(β™―β€˜π‘‘))(π‘‘β€˜π‘˜) ∈ ran (π‘‡β€˜(π‘‘β€˜(π‘˜ βˆ’ 1))))}βŸΆπ‘Š
98fdmi 6730 . . . . . . . . 9 dom 𝑆 = {𝑑 ∈ (Word π‘Š βˆ– {βˆ…}) ∣ ((π‘‘β€˜0) ∈ 𝐷 ∧ βˆ€π‘˜ ∈ (1..^(β™―β€˜π‘‘))(π‘‘β€˜π‘˜) ∈ ran (π‘‡β€˜(π‘‘β€˜(π‘˜ βˆ’ 1))))}
109feq2i 6710 . . . . . . . 8 (𝑆:dom π‘†βŸΆπ‘Š ↔ 𝑆:{𝑑 ∈ (Word π‘Š βˆ– {βˆ…}) ∣ ((π‘‘β€˜0) ∈ 𝐷 ∧ βˆ€π‘˜ ∈ (1..^(β™―β€˜π‘‘))(π‘‘β€˜π‘˜) ∈ ran (π‘‡β€˜(π‘‘β€˜(π‘˜ βˆ’ 1))))}βŸΆπ‘Š)
118, 10mpbir 230 . . . . . . 7 𝑆:dom π‘†βŸΆπ‘Š
1211ffvelcdmi 7086 . . . . . 6 (𝐢 ∈ dom 𝑆 β†’ (π‘†β€˜πΆ) ∈ π‘Š)
131, 12syl 17 . . . . 5 (πœ‘ β†’ (π‘†β€˜πΆ) ∈ π‘Š)
14 efgredlemb.q . . . . . . 7 (πœ‘ β†’ 𝑄 ∈ (0...(β™―β€˜(π΅β€˜πΏ))))
15 elfzuz 13497 . . . . . . 7 (𝑄 ∈ (0...(β™―β€˜(π΅β€˜πΏ))) β†’ 𝑄 ∈ (β„€β‰₯β€˜0))
1614, 15syl 17 . . . . . 6 (πœ‘ β†’ 𝑄 ∈ (β„€β‰₯β€˜0))
17 efgredlemd.sc . . . . . . . . . 10 (πœ‘ β†’ (π‘†β€˜πΆ) = (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)))
1817fveq2d 6896 . . . . . . . . 9 (πœ‘ β†’ (β™―β€˜(π‘†β€˜πΆ)) = (β™―β€˜(((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩))))
19 fviss 6969 . . . . . . . . . . . . 13 ( I β€˜Word (𝐼 Γ— 2o)) βŠ† Word (𝐼 Γ— 2o)
202, 19eqsstri 4017 . . . . . . . . . . . 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 19609 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π΄β€˜πΎ) ∈ π‘Š ∧ (π΅β€˜πΏ) ∈ π‘Š))
2928simprd 497 . . . . . . . . . . . 12 (πœ‘ β†’ (π΅β€˜πΏ) ∈ π‘Š)
3020, 29sselid 3981 . . . . . . . . . . 11 (πœ‘ β†’ (π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o))
31 pfxcl 14627 . . . . . . . . . . 11 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΅β€˜πΏ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o))
3230, 31syl 17 . . . . . . . . . 10 (πœ‘ β†’ ((π΅β€˜πΏ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o))
3328simpld 496 . . . . . . . . . . . 12 (πœ‘ β†’ (π΄β€˜πΎ) ∈ π‘Š)
3420, 33sselid 3981 . . . . . . . . . . 11 (πœ‘ β†’ (π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o))
35 swrdcl 14595 . . . . . . . . . . 11 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o))
3634, 35syl 17 . . . . . . . . . 10 (πœ‘ β†’ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o))
37 ccatlen 14525 . . . . . . . . . 10 ((((π΅β€˜πΏ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o) ∧ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o)) β†’ (β™―β€˜(((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩))) = ((β™―β€˜((π΅β€˜πΏ) prefix 𝑄)) + (β™―β€˜((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩))))
3832, 36, 37syl2anc 585 . . . . . . . . 9 (πœ‘ β†’ (β™―β€˜(((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩))) = ((β™―β€˜((π΅β€˜πΏ) prefix 𝑄)) + (β™―β€˜((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩))))
39 pfxlen 14633 . . . . . . . . . . . 12 (((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) ∧ 𝑄 ∈ (0...(β™―β€˜(π΅β€˜πΏ)))) β†’ (β™―β€˜((π΅β€˜πΏ) prefix 𝑄)) = 𝑄)
4030, 14, 39syl2anc 585 . . . . . . . . . . 11 (πœ‘ β†’ (β™―β€˜((π΅β€˜πΏ) prefix 𝑄)) = 𝑄)
41 2nn0 12489 . . . . . . . . . . . . . 14 2 ∈ β„•0
42 uzaddcl 12888 . . . . . . . . . . . . . 14 ((𝑄 ∈ (β„€β‰₯β€˜0) ∧ 2 ∈ β„•0) β†’ (𝑄 + 2) ∈ (β„€β‰₯β€˜0))
4316, 41, 42sylancl 587 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑄 + 2) ∈ (β„€β‰₯β€˜0))
44 efgredlemb.p . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))))
45 elfzuz3 13498 . . . . . . . . . . . . . . 15 (𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))) β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜π‘ƒ))
4644, 45syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜π‘ƒ))
47 efgredlemd.9 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2)))
48 uztrn 12840 . . . . . . . . . . . . . 14 (((β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜π‘ƒ) ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜(𝑄 + 2)))
4946, 47, 48syl2anc 585 . . . . . . . . . . . . 13 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜(𝑄 + 2)))
50 elfzuzb 13495 . . . . . . . . . . . . 13 ((𝑄 + 2) ∈ (0...(β™―β€˜(π΄β€˜πΎ))) ↔ ((𝑄 + 2) ∈ (β„€β‰₯β€˜0) ∧ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜(𝑄 + 2))))
5143, 49, 50sylanbrc 584 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑄 + 2) ∈ (0...(β™―β€˜(π΄β€˜πΎ))))
52 lencl 14483 . . . . . . . . . . . . . . 15 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ β„•0)
5334, 52syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ β„•0)
54 nn0uz 12864 . . . . . . . . . . . . . 14 β„•0 = (β„€β‰₯β€˜0)
5553, 54eleqtrdi 2844 . . . . . . . . . . . . 13 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜0))
56 eluzfz2 13509 . . . . . . . . . . . . 13 ((β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜0) β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (0...(β™―β€˜(π΄β€˜πΎ))))
5755, 56syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (0...(β™―β€˜(π΄β€˜πΎ))))
58 swrdlen 14597 . . . . . . . . . . . 12 (((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) ∧ (𝑄 + 2) ∈ (0...(β™―β€˜(π΄β€˜πΎ))) ∧ (β™―β€˜(π΄β€˜πΎ)) ∈ (0...(β™―β€˜(π΄β€˜πΎ)))) β†’ (β™―β€˜((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = ((β™―β€˜(π΄β€˜πΎ)) βˆ’ (𝑄 + 2)))
5934, 51, 57, 58syl3anc 1372 . . . . . . . . . . 11 (πœ‘ β†’ (β™―β€˜((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = ((β™―β€˜(π΄β€˜πΎ)) βˆ’ (𝑄 + 2)))
6040, 59oveq12d 7427 . . . . . . . . . 10 (πœ‘ β†’ ((β™―β€˜((π΅β€˜πΏ) prefix 𝑄)) + (β™―β€˜((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩))) = (𝑄 + ((β™―β€˜(π΄β€˜πΎ)) βˆ’ (𝑄 + 2))))
6114elfzelzd 13502 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑄 ∈ β„€)
6261zcnd 12667 . . . . . . . . . . 11 (πœ‘ β†’ 𝑄 ∈ β„‚)
6353nn0cnd 12534 . . . . . . . . . . 11 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ β„‚)
64 2z 12594 . . . . . . . . . . . . 13 2 ∈ β„€
65 zaddcl 12602 . . . . . . . . . . . . 13 ((𝑄 ∈ β„€ ∧ 2 ∈ β„€) β†’ (𝑄 + 2) ∈ β„€)
6661, 64, 65sylancl 587 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑄 + 2) ∈ β„€)
6766zcnd 12667 . . . . . . . . . . 11 (πœ‘ β†’ (𝑄 + 2) ∈ β„‚)
6862, 63, 67addsubassd 11591 . . . . . . . . . 10 (πœ‘ β†’ ((𝑄 + (β™―β€˜(π΄β€˜πΎ))) βˆ’ (𝑄 + 2)) = (𝑄 + ((β™―β€˜(π΄β€˜πΎ)) βˆ’ (𝑄 + 2))))
69 2cn 12287 . . . . . . . . . . . 12 2 ∈ β„‚
7069a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ 2 ∈ β„‚)
7162, 63, 70pnpcand 11608 . . . . . . . . . 10 (πœ‘ β†’ ((𝑄 + (β™―β€˜(π΄β€˜πΎ))) βˆ’ (𝑄 + 2)) = ((β™―β€˜(π΄β€˜πΎ)) βˆ’ 2))
7260, 68, 713eqtr2d 2779 . . . . . . . . 9 (πœ‘ β†’ ((β™―β€˜((π΅β€˜πΏ) prefix 𝑄)) + (β™―β€˜((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩))) = ((β™―β€˜(π΄β€˜πΎ)) βˆ’ 2))
7318, 38, 723eqtrd 2777 . . . . . . . 8 (πœ‘ β†’ (β™―β€˜(π‘†β€˜πΆ)) = ((β™―β€˜(π΄β€˜πΎ)) βˆ’ 2))
7444elfzelzd 13502 . . . . . . . . . 10 (πœ‘ β†’ 𝑃 ∈ β„€)
75 zsubcl 12604 . . . . . . . . . 10 ((𝑃 ∈ β„€ ∧ 2 ∈ β„€) β†’ (𝑃 βˆ’ 2) ∈ β„€)
7674, 64, 75sylancl 587 . . . . . . . . 9 (πœ‘ β†’ (𝑃 βˆ’ 2) ∈ β„€)
7764a1i 11 . . . . . . . . 9 (πœ‘ β†’ 2 ∈ β„€)
7874zcnd 12667 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑃 ∈ β„‚)
79 npcan 11469 . . . . . . . . . . . 12 ((𝑃 ∈ β„‚ ∧ 2 ∈ β„‚) β†’ ((𝑃 βˆ’ 2) + 2) = 𝑃)
8078, 69, 79sylancl 587 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑃 βˆ’ 2) + 2) = 𝑃)
8180fveq2d 6896 . . . . . . . . . 10 (πœ‘ β†’ (β„€β‰₯β€˜((𝑃 βˆ’ 2) + 2)) = (β„€β‰₯β€˜π‘ƒ))
8246, 81eleqtrrd 2837 . . . . . . . . 9 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜((𝑃 βˆ’ 2) + 2)))
83 eluzsub 12852 . . . . . . . . 9 (((𝑃 βˆ’ 2) ∈ β„€ ∧ 2 ∈ β„€ ∧ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜((𝑃 βˆ’ 2) + 2))) β†’ ((β™―β€˜(π΄β€˜πΎ)) βˆ’ 2) ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2)))
8476, 77, 82, 83syl3anc 1372 . . . . . . . 8 (πœ‘ β†’ ((β™―β€˜(π΄β€˜πΎ)) βˆ’ 2) ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2)))
8573, 84eqeltrd 2834 . . . . . . 7 (πœ‘ β†’ (β™―β€˜(π‘†β€˜πΆ)) ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2)))
86 eluzsub 12852 . . . . . . . 8 ((𝑄 ∈ β„€ ∧ 2 ∈ β„€ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) β†’ (𝑃 βˆ’ 2) ∈ (β„€β‰₯β€˜π‘„))
8761, 77, 47, 86syl3anc 1372 . . . . . . 7 (πœ‘ β†’ (𝑃 βˆ’ 2) ∈ (β„€β‰₯β€˜π‘„))
88 uztrn 12840 . . . . . . 7 (((β™―β€˜(π‘†β€˜πΆ)) ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2)) ∧ (𝑃 βˆ’ 2) ∈ (β„€β‰₯β€˜π‘„)) β†’ (β™―β€˜(π‘†β€˜πΆ)) ∈ (β„€β‰₯β€˜π‘„))
8985, 87, 88syl2anc 585 . . . . . 6 (πœ‘ β†’ (β™―β€˜(π‘†β€˜πΆ)) ∈ (β„€β‰₯β€˜π‘„))
90 elfzuzb 13495 . . . . . 6 (𝑄 ∈ (0...(β™―β€˜(π‘†β€˜πΆ))) ↔ (𝑄 ∈ (β„€β‰₯β€˜0) ∧ (β™―β€˜(π‘†β€˜πΆ)) ∈ (β„€β‰₯β€˜π‘„)))
9116, 89, 90sylanbrc 584 . . . . 5 (πœ‘ β†’ 𝑄 ∈ (0...(β™―β€˜(π‘†β€˜πΆ))))
92 efgredlemb.v . . . . 5 (πœ‘ β†’ 𝑉 ∈ (𝐼 Γ— 2o))
932, 3, 4, 5efgtval 19591 . . . . 5 (((π‘†β€˜πΆ) ∈ π‘Š ∧ 𝑄 ∈ (0...(β™―β€˜(π‘†β€˜πΆ))) ∧ 𝑉 ∈ (𝐼 Γ— 2o)) β†’ (𝑄(π‘‡β€˜(π‘†β€˜πΆ))𝑉) = ((π‘†β€˜πΆ) splice βŸ¨π‘„, 𝑄, βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©βŸ©))
9413, 91, 92, 93syl3anc 1372 . . . 4 (πœ‘ β†’ (𝑄(π‘‡β€˜(π‘†β€˜πΆ))𝑉) = ((π‘†β€˜πΆ) splice βŸ¨π‘„, 𝑄, βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©βŸ©))
95 pfxcl 14627 . . . . . 6 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o))
9634, 95syl 17 . . . . 5 (πœ‘ β†’ ((π΄β€˜πΎ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o))
97 wrd0 14489 . . . . . 6 βˆ… ∈ Word (𝐼 Γ— 2o)
9897a1i 11 . . . . 5 (πœ‘ β†’ βˆ… ∈ Word (𝐼 Γ— 2o))
994efgmf 19581 . . . . . . . 8 𝑀:(𝐼 Γ— 2o)⟢(𝐼 Γ— 2o)
10099ffvelcdmi 7086 . . . . . . 7 (𝑉 ∈ (𝐼 Γ— 2o) β†’ (π‘€β€˜π‘‰) ∈ (𝐼 Γ— 2o))
10192, 100syl 17 . . . . . 6 (πœ‘ β†’ (π‘€β€˜π‘‰) ∈ (𝐼 Γ— 2o))
10292, 101s2cld 14822 . . . . 5 (πœ‘ β†’ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ∈ Word (𝐼 Γ— 2o))
10361zred 12666 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑄 ∈ ℝ)
104 nn0addge1 12518 . . . . . . . . . . . . . . . . 17 ((𝑄 ∈ ℝ ∧ 2 ∈ β„•0) β†’ 𝑄 ≀ (𝑄 + 2))
105103, 41, 104sylancl 587 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑄 ≀ (𝑄 + 2))
106 eluz2 12828 . . . . . . . . . . . . . . . 16 ((𝑄 + 2) ∈ (β„€β‰₯β€˜π‘„) ↔ (𝑄 ∈ β„€ ∧ (𝑄 + 2) ∈ β„€ ∧ 𝑄 ≀ (𝑄 + 2)))
10761, 66, 105, 106syl3anbrc 1344 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑄 + 2) ∈ (β„€β‰₯β€˜π‘„))
108 uztrn 12840 . . . . . . . . . . . . . . 15 ((𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (β„€β‰₯β€˜π‘„)) β†’ 𝑃 ∈ (β„€β‰₯β€˜π‘„))
10947, 107, 108syl2anc 585 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑃 ∈ (β„€β‰₯β€˜π‘„))
110 elfzuzb 13495 . . . . . . . . . . . . . 14 (𝑄 ∈ (0...𝑃) ↔ (𝑄 ∈ (β„€β‰₯β€˜0) ∧ 𝑃 ∈ (β„€β‰₯β€˜π‘„)))
11116, 109, 110sylanbrc 584 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑄 ∈ (0...𝑃))
112 ccatpfx 14651 . . . . . . . . . . . . 13 (((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) ∧ 𝑄 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ)))) β†’ (((π΄β€˜πΎ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©)) = ((π΄β€˜πΎ) prefix 𝑃))
11334, 111, 44, 112syl3anc 1372 . . . . . . . . . . . 12 (πœ‘ β†’ (((π΄β€˜πΎ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©)) = ((π΄β€˜πΎ) prefix 𝑃))
114113oveq1d 7424 . . . . . . . . . . 11 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©)) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = (((π΄β€˜πΎ) prefix 𝑃) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))))
115 pfxcl 14627 . . . . . . . . . . . . 13 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) prefix 𝑃) ∈ Word (𝐼 Γ— 2o))
11634, 115syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ ((π΄β€˜πΎ) prefix 𝑃) ∈ Word (𝐼 Γ— 2o))
117 efgredlemb.u . . . . . . . . . . . . 13 (πœ‘ β†’ π‘ˆ ∈ (𝐼 Γ— 2o))
11899ffvelcdmi 7086 . . . . . . . . . . . . . 14 (π‘ˆ ∈ (𝐼 Γ— 2o) β†’ (π‘€β€˜π‘ˆ) ∈ (𝐼 Γ— 2o))
119117, 118syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘€β€˜π‘ˆ) ∈ (𝐼 Γ— 2o))
120117, 119s2cld 14822 . . . . . . . . . . . 12 (πœ‘ β†’ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ∈ Word (𝐼 Γ— 2o))
121 swrdcl 14595 . . . . . . . . . . . . 13 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o))
12234, 121syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o))
123 ccatass 14538 . . . . . . . . . . . 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 19591 . . . . . . . . . . . . . 14 (((π΄β€˜πΎ) ∈ π‘Š ∧ 𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))) ∧ π‘ˆ ∈ (𝐼 Γ— 2o)) β†’ (𝑃(π‘‡β€˜(π΄β€˜πΎ))π‘ˆ) = ((π΄β€˜πΎ) splice βŸ¨π‘ƒ, 𝑃, βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©βŸ©))
12733, 44, 117, 126syl3anc 1372 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑃(π‘‡β€˜(π΄β€˜πΎ))π‘ˆ) = ((π΄β€˜πΎ) splice βŸ¨π‘ƒ, 𝑃, βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©βŸ©))
128 splval 14701 . . . . . . . . . . . . . 14 (((π΄β€˜πΎ) ∈ π‘Š ∧ (𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))) ∧ 𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))) ∧ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ∈ Word (𝐼 Γ— 2o))) β†’ ((π΄β€˜πΎ) splice βŸ¨π‘ƒ, 𝑃, βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©βŸ©) = ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))
12933, 44, 44, 120, 128syl13anc 1373 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π΄β€˜πΎ) splice βŸ¨π‘ƒ, 𝑃, βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©βŸ©) = ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))
130125, 127, 1293eqtrd 2777 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘†β€˜π΄) = ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))
131 efgredlemb.7 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘†β€˜π΅) = (𝑄(π‘‡β€˜(π΅β€˜πΏ))𝑉))
1322, 3, 4, 5efgtval 19591 . . . . . . . . . . . . . 14 (((π΅β€˜πΏ) ∈ π‘Š ∧ 𝑄 ∈ (0...(β™―β€˜(π΅β€˜πΏ))) ∧ 𝑉 ∈ (𝐼 Γ— 2o)) β†’ (𝑄(π‘‡β€˜(π΅β€˜πΏ))𝑉) = ((π΅β€˜πΏ) splice βŸ¨π‘„, 𝑄, βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©βŸ©))
13329, 14, 92, 132syl3anc 1372 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑄(π‘‡β€˜(π΅β€˜πΏ))𝑉) = ((π΅β€˜πΏ) splice βŸ¨π‘„, 𝑄, βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©βŸ©))
134 splval 14701 . . . . . . . . . . . . . 14 (((π΅β€˜πΏ) ∈ π‘Š ∧ (𝑄 ∈ (0...(β™―β€˜(π΅β€˜πΏ))) ∧ 𝑄 ∈ (0...(β™―β€˜(π΅β€˜πΏ))) ∧ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ∈ Word (𝐼 Γ— 2o))) β†’ ((π΅β€˜πΏ) splice βŸ¨π‘„, 𝑄, βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©βŸ©) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
13529, 14, 14, 102, 134syl13anc 1373 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π΅β€˜πΏ) splice βŸ¨π‘„, 𝑄, βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©βŸ©) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
136131, 133, 1353eqtrd 2777 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘†β€˜π΅) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
13724, 130, 1363eqtr3d 2781 . . . . . . . . . . 11 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
138114, 124, 1373eqtr2d 2779 . . . . . . . . . 10 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©)) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
139 swrdcl 14595 . . . . . . . . . . . 12 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ∈ Word (𝐼 Γ— 2o))
14034, 139syl 17 . . . . . . . . . . 11 (πœ‘ β†’ ((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ∈ Word (𝐼 Γ— 2o))
141 ccatcl 14524 . . . . . . . . . . . 12 ((βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ∈ Word (𝐼 Γ— 2o) ∧ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o)) β†’ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) ∈ Word (𝐼 Γ— 2o))
142120, 122, 141syl2anc 585 . . . . . . . . . . 11 (πœ‘ β†’ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) ∈ Word (𝐼 Γ— 2o))
143 ccatass 14538 . . . . . . . . . . 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 14595 . . . . . . . . . . . 12 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o))
14630, 145syl 17 . . . . . . . . . . 11 (πœ‘ β†’ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o))
147 ccatass 14538 . . . . . . . . . . 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 2781 . . . . . . . . 9 (πœ‘ β†’ (((π΄β€˜πΎ) prefix 𝑄) ++ (((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))) = (((π΅β€˜πΏ) prefix 𝑄) ++ (βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩))))
150 ccatcl 14524 . . . . . . . . . . 11 ((((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ∈ Word (𝐼 Γ— 2o) ∧ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) ∈ Word (𝐼 Γ— 2o)) β†’ (((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) ∈ Word (𝐼 Γ— 2o))
151140, 142, 150syl2anc 585 . . . . . . . . . 10 (πœ‘ β†’ (((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) ∈ Word (𝐼 Γ— 2o))
152 ccatcl 14524 . . . . . . . . . . 11 ((βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ∈ Word (𝐼 Γ— 2o) ∧ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o)) β†’ (βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)) ∈ Word (𝐼 Γ— 2o))
153102, 146, 152syl2anc 585 . . . . . . . . . 10 (πœ‘ β†’ (βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)) ∈ Word (𝐼 Γ— 2o))
154 uztrn 12840 . . . . . . . . . . . . . 14 (((β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜π‘ƒ) ∧ 𝑃 ∈ (β„€β‰₯β€˜π‘„)) β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜π‘„))
15546, 109, 154syl2anc 585 . . . . . . . . . . . . 13 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜π‘„))
156 elfzuzb 13495 . . . . . . . . . . . . 13 (𝑄 ∈ (0...(β™―β€˜(π΄β€˜πΎ))) ↔ (𝑄 ∈ (β„€β‰₯β€˜0) ∧ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜π‘„)))
15716, 155, 156sylanbrc 584 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑄 ∈ (0...(β™―β€˜(π΄β€˜πΎ))))
158 pfxlen 14633 . . . . . . . . . . . 12 (((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) ∧ 𝑄 ∈ (0...(β™―β€˜(π΄β€˜πΎ)))) β†’ (β™―β€˜((π΄β€˜πΎ) prefix 𝑄)) = 𝑄)
15934, 157, 158syl2anc 585 . . . . . . . . . . 11 (πœ‘ β†’ (β™―β€˜((π΄β€˜πΎ) prefix 𝑄)) = 𝑄)
160159, 40eqtr4d 2776 . . . . . . . . . 10 (πœ‘ β†’ (β™―β€˜((π΄β€˜πΎ) prefix 𝑄)) = (β™―β€˜((π΅β€˜πΏ) prefix 𝑄)))
161 ccatopth 14666 . . . . . . . . . 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 231 . . . . . . . 8 (πœ‘ β†’ (((π΄β€˜πΎ) prefix 𝑄) = ((π΅β€˜πΏ) prefix 𝑄) ∧ (((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = (βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩))))
164163simpld 496 . . . . . . 7 (πœ‘ β†’ ((π΄β€˜πΎ) prefix 𝑄) = ((π΅β€˜πΏ) prefix 𝑄))
165164oveq1d 7424 . . . . . 6 (πœ‘ β†’ (((π΄β€˜πΎ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)))
166 ccatrid 14537 . . . . . . . 8 (((π΄β€˜πΎ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o) β†’ (((π΄β€˜πΎ) prefix 𝑄) ++ βˆ…) = ((π΄β€˜πΎ) prefix 𝑄))
16796, 166syl 17 . . . . . . 7 (πœ‘ β†’ (((π΄β€˜πΎ) prefix 𝑄) ++ βˆ…) = ((π΄β€˜πΎ) prefix 𝑄))
168167oveq1d 7424 . . . . . 6 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑄) ++ βˆ…) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΄β€˜πΎ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)))
169165, 168, 173eqtr4rd 2784 . . . . 5 (πœ‘ β†’ (π‘†β€˜πΆ) = ((((π΄β€˜πΎ) prefix 𝑄) ++ βˆ…) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)))
170159eqcomd 2739 . . . . 5 (πœ‘ β†’ 𝑄 = (β™―β€˜((π΄β€˜πΎ) prefix 𝑄)))
171 hash0 14327 . . . . . . 7 (β™―β€˜βˆ…) = 0
172171oveq2i 7420 . . . . . 6 (𝑄 + (β™―β€˜βˆ…)) = (𝑄 + 0)
17362addridd 11414 . . . . . 6 (πœ‘ β†’ (𝑄 + 0) = 𝑄)
174172, 173eqtr2id 2786 . . . . 5 (πœ‘ β†’ 𝑄 = (𝑄 + (β™―β€˜βˆ…)))
17596, 98, 36, 102, 169, 170, 174splval2 14707 . . . 4 (πœ‘ β†’ ((π‘†β€˜πΆ) splice βŸ¨π‘„, 𝑄, βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©βŸ©) = ((((π΄β€˜πΎ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)))
176 elfzuzb 13495 . . . . . . . . . . . . . 14 (𝑄 ∈ (0...(𝑄 + 2)) ↔ (𝑄 ∈ (β„€β‰₯β€˜0) ∧ (𝑄 + 2) ∈ (β„€β‰₯β€˜π‘„)))
17716, 107, 176sylanbrc 584 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑄 ∈ (0...(𝑄 + 2)))
178 elfzuzb 13495 . . . . . . . . . . . . . 14 ((𝑄 + 2) ∈ (0...𝑃) ↔ ((𝑄 + 2) ∈ (β„€β‰₯β€˜0) ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))))
17943, 47, 178sylanbrc 584 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑄 + 2) ∈ (0...𝑃))
180 ccatswrd 14618 . . . . . . . . . . . . 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 7424 . . . . . . . . . . 11 (πœ‘ β†’ ((((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©)) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = (((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))))
183 swrdcl 14595 . . . . . . . . . . . . 13 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩) ∈ Word (𝐼 Γ— 2o))
18434, 183syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ ((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩) ∈ Word (𝐼 Γ— 2o))
185 swrdcl 14595 . . . . . . . . . . . . 13 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ∈ Word (𝐼 Γ— 2o))
18634, 185syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ∈ Word (𝐼 Γ— 2o))
187 ccatass 14538 . . . . . . . . . . . 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 497 . . . . . . . . . . 11 (πœ‘ β†’ (((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = (βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
190182, 188, 1893eqtr3d 2781 . . . . . . . . . 10 (πœ‘ β†’ (((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩) ++ (((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))) = (βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
191 ccatcl 14524 . . . . . . . . . . . 12 ((((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ∈ Word (𝐼 Γ— 2o) ∧ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) ∈ Word (𝐼 Γ— 2o)) β†’ (((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) ∈ Word (𝐼 Γ— 2o))
192186, 142, 191syl2anc 585 . . . . . . . . . . 11 (πœ‘ β†’ (((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) ∈ Word (𝐼 Γ— 2o))
193 swrdlen 14597 . . . . . . . . . . . . . 14 (((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(β™―β€˜(π΄β€˜πΎ)))) β†’ (β™―β€˜((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩)) = ((𝑄 + 2) βˆ’ 𝑄))
19434, 177, 51, 193syl3anc 1372 . . . . . . . . . . . . 13 (πœ‘ β†’ (β™―β€˜((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩)) = ((𝑄 + 2) βˆ’ 𝑄))
195 pncan2 11467 . . . . . . . . . . . . . 14 ((𝑄 ∈ β„‚ ∧ 2 ∈ β„‚) β†’ ((𝑄 + 2) βˆ’ 𝑄) = 2)
19662, 69, 195sylancl 587 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝑄 + 2) βˆ’ 𝑄) = 2)
197194, 196eqtrd 2773 . . . . . . . . . . . 12 (πœ‘ β†’ (β™―β€˜((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩)) = 2)
198 s2len 14840 . . . . . . . . . . . 12 (β™―β€˜βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) = 2
199197, 198eqtr4di 2791 . . . . . . . . . . 11 (πœ‘ β†’ (β™―β€˜((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩)) = (β™―β€˜βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©))
200 ccatopth 14666 . . . . . . . . . . 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 231 . . . . . . . . 9 (πœ‘ β†’ (((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩) = βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ∧ (((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
203202simpld 496 . . . . . . . 8 (πœ‘ β†’ ((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩) = βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©)
204203oveq2d 7425 . . . . . . 7 (πœ‘ β†’ (((π΄β€˜πΎ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩)) = (((π΄β€˜πΎ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©))
205 ccatpfx 14651 . . . . . . . 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 2775 . . . . . 6 (πœ‘ β†’ (((π΄β€˜πΎ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) = ((π΄β€˜πΎ) prefix (𝑄 + 2)))
208207oveq1d 7424 . . . . 5 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΄β€˜πΎ) prefix (𝑄 + 2)) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)))
209 ccatpfx 14651 . . . . . 6 (((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) ∧ (𝑄 + 2) ∈ (0...(β™―β€˜(π΄β€˜πΎ))) ∧ (β™―β€˜(π΄β€˜πΎ)) ∈ (0...(β™―β€˜(π΄β€˜πΎ)))) β†’ (((π΄β€˜πΎ) prefix (𝑄 + 2)) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = ((π΄β€˜πΎ) prefix (β™―β€˜(π΄β€˜πΎ))))
21034, 51, 57, 209syl3anc 1372 . . . . 5 (πœ‘ β†’ (((π΄β€˜πΎ) prefix (𝑄 + 2)) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = ((π΄β€˜πΎ) prefix (β™―β€˜(π΄β€˜πΎ))))
211 pfxid 14634 . . . . . 6 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) prefix (β™―β€˜(π΄β€˜πΎ))) = (π΄β€˜πΎ))
21234, 211syl 17 . . . . 5 (πœ‘ β†’ ((π΄β€˜πΎ) prefix (β™―β€˜(π΄β€˜πΎ))) = (π΄β€˜πΎ))
213208, 210, 2123eqtrd 2777 . . . 4 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π΄β€˜πΎ))
21494, 175, 2133eqtrd 2777 . . 3 (πœ‘ β†’ (𝑄(π‘‡β€˜(π‘†β€˜πΆ))𝑉) = (π΄β€˜πΎ))
2152, 3, 4, 5efgtf 19590 . . . . . . 7 ((π‘†β€˜πΆ) ∈ π‘Š β†’ ((π‘‡β€˜(π‘†β€˜πΆ)) = (π‘Ž ∈ (0...(β™―β€˜(π‘†β€˜πΆ))), 𝑖 ∈ (𝐼 Γ— 2o) ↦ ((π‘†β€˜πΆ) splice βŸ¨π‘Ž, π‘Ž, βŸ¨β€œπ‘–(π‘€β€˜π‘–)β€βŸ©βŸ©)) ∧ (π‘‡β€˜(π‘†β€˜πΆ)):((0...(β™―β€˜(π‘†β€˜πΆ))) Γ— (𝐼 Γ— 2o))βŸΆπ‘Š))
21613, 215syl 17 . . . . . 6 (πœ‘ β†’ ((π‘‡β€˜(π‘†β€˜πΆ)) = (π‘Ž ∈ (0...(β™―β€˜(π‘†β€˜πΆ))), 𝑖 ∈ (𝐼 Γ— 2o) ↦ ((π‘†β€˜πΆ) splice βŸ¨π‘Ž, π‘Ž, βŸ¨β€œπ‘–(π‘€β€˜π‘–)β€βŸ©βŸ©)) ∧ (π‘‡β€˜(π‘†β€˜πΆ)):((0...(β™―β€˜(π‘†β€˜πΆ))) Γ— (𝐼 Γ— 2o))βŸΆπ‘Š))
217216simprd 497 . . . . 5 (πœ‘ β†’ (π‘‡β€˜(π‘†β€˜πΆ)):((0...(β™―β€˜(π‘†β€˜πΆ))) Γ— (𝐼 Γ— 2o))βŸΆπ‘Š)
218217ffnd 6719 . . . 4 (πœ‘ β†’ (π‘‡β€˜(π‘†β€˜πΆ)) Fn ((0...(β™―β€˜(π‘†β€˜πΆ))) Γ— (𝐼 Γ— 2o)))
219 fnovrn 7582 . . . 4 (((π‘‡β€˜(π‘†β€˜πΆ)) Fn ((0...(β™―β€˜(π‘†β€˜πΆ))) Γ— (𝐼 Γ— 2o)) ∧ 𝑄 ∈ (0...(β™―β€˜(π‘†β€˜πΆ))) ∧ 𝑉 ∈ (𝐼 Γ— 2o)) β†’ (𝑄(π‘‡β€˜(π‘†β€˜πΆ))𝑉) ∈ ran (π‘‡β€˜(π‘†β€˜πΆ)))
220218, 91, 92, 219syl3anc 1372 . . 3 (πœ‘ β†’ (𝑄(π‘‡β€˜(π‘†β€˜πΆ))𝑉) ∈ ran (π‘‡β€˜(π‘†β€˜πΆ)))
221214, 220eqeltrrd 2835 . 2 (πœ‘ β†’ (π΄β€˜πΎ) ∈ ran (π‘‡β€˜(π‘†β€˜πΆ)))
222 uztrn 12840 . . . . . . 7 (((𝑃 βˆ’ 2) ∈ (β„€β‰₯β€˜π‘„) ∧ 𝑄 ∈ (β„€β‰₯β€˜0)) β†’ (𝑃 βˆ’ 2) ∈ (β„€β‰₯β€˜0))
22387, 16, 222syl2anc 585 . . . . . 6 (πœ‘ β†’ (𝑃 βˆ’ 2) ∈ (β„€β‰₯β€˜0))
224 elfzuzb 13495 . . . . . 6 ((𝑃 βˆ’ 2) ∈ (0...(β™―β€˜(π‘†β€˜πΆ))) ↔ ((𝑃 βˆ’ 2) ∈ (β„€β‰₯β€˜0) ∧ (β™―β€˜(π‘†β€˜πΆ)) ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2))))
225223, 85, 224sylanbrc 584 . . . . 5 (πœ‘ β†’ (𝑃 βˆ’ 2) ∈ (0...(β™―β€˜(π‘†β€˜πΆ))))
2262, 3, 4, 5efgtval 19591 . . . . 5 (((π‘†β€˜πΆ) ∈ π‘Š ∧ (𝑃 βˆ’ 2) ∈ (0...(β™―β€˜(π‘†β€˜πΆ))) ∧ π‘ˆ ∈ (𝐼 Γ— 2o)) β†’ ((𝑃 βˆ’ 2)(π‘‡β€˜(π‘†β€˜πΆ))π‘ˆ) = ((π‘†β€˜πΆ) splice ⟨(𝑃 βˆ’ 2), (𝑃 βˆ’ 2), βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©βŸ©))
22713, 225, 117, 226syl3anc 1372 . . . 4 (πœ‘ β†’ ((𝑃 βˆ’ 2)(π‘‡β€˜(π‘†β€˜πΆ))π‘ˆ) = ((π‘†β€˜πΆ) splice ⟨(𝑃 βˆ’ 2), (𝑃 βˆ’ 2), βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©βŸ©))
228 pfxcl 14627 . . . . . 6 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ∈ Word (𝐼 Γ— 2o))
22930, 228syl 17 . . . . 5 (πœ‘ β†’ ((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ∈ Word (𝐼 Γ— 2o))
230 swrdcl 14595 . . . . . 6 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o))
23130, 230syl 17 . . . . 5 (πœ‘ β†’ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o))
232 ccatswrd 14618 . . . . . . . . . . 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 497 . . . . . . . . . . . . . 14 (πœ‘ β†’ (((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩))
235 elfzuzb 13495 . . . . . . . . . . . . . . . 16 (𝑄 ∈ (0...(𝑃 βˆ’ 2)) ↔ (𝑄 ∈ (β„€β‰₯β€˜0) ∧ (𝑃 βˆ’ 2) ∈ (β„€β‰₯β€˜π‘„)))
23616, 87, 235sylanbrc 584 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑄 ∈ (0...(𝑃 βˆ’ 2)))
2372, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27, 44, 14, 117, 92, 125, 131efgredlemg 19610 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) = (β™―β€˜(π΅β€˜πΏ)))
238237, 46eqeltrrd 2835 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ (β„€β‰₯β€˜π‘ƒ))
239 0le2 12314 . . . . . . . . . . . . . . . . . . . 20 0 ≀ 2
240239a1i 11 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 0 ≀ 2)
24174zred 12666 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝑃 ∈ ℝ)
242 2re 12286 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
243 subge02 11730 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℝ ∧ 2 ∈ ℝ) β†’ (0 ≀ 2 ↔ (𝑃 βˆ’ 2) ≀ 𝑃))
244241, 242, 243sylancl 587 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (0 ≀ 2 ↔ (𝑃 βˆ’ 2) ≀ 𝑃))
245240, 244mpbid 231 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝑃 βˆ’ 2) ≀ 𝑃)
246 eluz2 12828 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2)) ↔ ((𝑃 βˆ’ 2) ∈ β„€ ∧ 𝑃 ∈ β„€ ∧ (𝑃 βˆ’ 2) ≀ 𝑃))
24776, 74, 245, 246syl3anbrc 1344 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑃 ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2)))
248 uztrn 12840 . . . . . . . . . . . . . . . . 17 (((β™―β€˜(π΅β€˜πΏ)) ∈ (β„€β‰₯β€˜π‘ƒ) ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2))) β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2)))
249238, 247, 248syl2anc 585 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2)))
250 elfzuzb 13495 . . . . . . . . . . . . . . . 16 ((𝑃 βˆ’ 2) ∈ (0...(β™―β€˜(π΅β€˜πΏ))) ↔ ((𝑃 βˆ’ 2) ∈ (β„€β‰₯β€˜0) ∧ (β™―β€˜(π΅β€˜πΏ)) ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2))))
251223, 249, 250sylanbrc 584 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑃 βˆ’ 2) ∈ (0...(β™―β€˜(π΅β€˜πΏ))))
252 lencl 14483 . . . . . . . . . . . . . . . . . 18 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ β„•0)
25330, 252syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ β„•0)
254253, 54eleqtrdi 2844 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ (β„€β‰₯β€˜0))
255 eluzfz2 13509 . . . . . . . . . . . . . . . 16 ((β™―β€˜(π΅β€˜πΏ)) ∈ (β„€β‰₯β€˜0) β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ (0...(β™―β€˜(π΅β€˜πΏ))))
256254, 255syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ (0...(β™―β€˜(π΅β€˜πΏ))))
257 ccatswrd 14618 . . . . . . . . . . . . . . 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 2776 . . . . . . . . . . . . 13 (πœ‘ β†’ (((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = (((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩) ++ ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), (β™―β€˜(π΅β€˜πΏ))⟩)))
260 swrdcl 14595 . . . . . . . . . . . . . . 15 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩) ∈ Word (𝐼 Γ— 2o))
26130, 260syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩) ∈ Word (𝐼 Γ— 2o))
262 swrdcl 14595 . . . . . . . . . . . . . . 15 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o))
26330, 262syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o))
264 swrdlen 14597 . . . . . . . . . . . . . . . 16 (((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ)))) β†’ (β™―β€˜((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©)) = (𝑃 βˆ’ (𝑄 + 2)))
26534, 179, 44, 264syl3anc 1372 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (β™―β€˜((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©)) = (𝑃 βˆ’ (𝑄 + 2)))
266 swrdlen 14597 . . . . . . . . . . . . . . . . 17 (((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) ∧ 𝑄 ∈ (0...(𝑃 βˆ’ 2)) ∧ (𝑃 βˆ’ 2) ∈ (0...(β™―β€˜(π΅β€˜πΏ)))) β†’ (β™―β€˜((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩)) = ((𝑃 βˆ’ 2) βˆ’ 𝑄))
26730, 236, 251, 266syl3anc 1372 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (β™―β€˜((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩)) = ((𝑃 βˆ’ 2) βˆ’ 𝑄))
26878, 62, 70sub32d 11603 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((𝑃 βˆ’ 𝑄) βˆ’ 2) = ((𝑃 βˆ’ 2) βˆ’ 𝑄))
26978, 62, 70subsub4d 11602 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((𝑃 βˆ’ 𝑄) βˆ’ 2) = (𝑃 βˆ’ (𝑄 + 2)))
270267, 268, 2693eqtr2d 2779 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (β™―β€˜((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩)) = (𝑃 βˆ’ (𝑄 + 2)))
271265, 270eqtr4d 2776 . . . . . . . . . . . . . 14 (πœ‘ β†’ (β™―β€˜((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©)) = (β™―β€˜((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩)))
272 ccatopth 14666 . . . . . . . . . . . . . 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 231 . . . . . . . . . . . 12 (πœ‘ β†’ (((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) = ((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩) ∧ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), (β™―β€˜(π΅β€˜πΏ))⟩)))
275274simpld 496 . . . . . . . . . . 11 (πœ‘ β†’ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) = ((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩))
276274simprd 497 . . . . . . . . . . . . . 14 (πœ‘ β†’ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), (β™―β€˜(π΅β€˜πΏ))⟩))
277 elfzuzb 13495 . . . . . . . . . . . . . . . 16 ((𝑃 βˆ’ 2) ∈ (0...𝑃) ↔ ((𝑃 βˆ’ 2) ∈ (β„€β‰₯β€˜0) ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2))))
278223, 247, 277sylanbrc 584 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑃 βˆ’ 2) ∈ (0...𝑃))
279 elfzuz 13497 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))) β†’ 𝑃 ∈ (β„€β‰₯β€˜0))
28044, 279syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑃 ∈ (β„€β‰₯β€˜0))
281 elfzuzb 13495 . . . . . . . . . . . . . . . 16 (𝑃 ∈ (0...(β™―β€˜(π΅β€˜πΏ))) ↔ (𝑃 ∈ (β„€β‰₯β€˜0) ∧ (β™―β€˜(π΅β€˜πΏ)) ∈ (β„€β‰₯β€˜π‘ƒ)))
282280, 238, 281sylanbrc 584 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑃 ∈ (0...(β™―β€˜(π΅β€˜πΏ))))
283 ccatswrd 14618 . . . . . . . . . . . . . . 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 2776 . . . . . . . . . . . . 13 (πœ‘ β†’ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
286 swrdcl 14595 . . . . . . . . . . . . . . 15 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©) ∈ Word (𝐼 Γ— 2o))
28730, 286syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©) ∈ Word (𝐼 Γ— 2o))
288 s2len 14840 . . . . . . . . . . . . . . 15 (β™―β€˜βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) = 2
289 swrdlen 14597 . . . . . . . . . . . . . . . . 17 (((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) ∧ (𝑃 βˆ’ 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(β™―β€˜(π΅β€˜πΏ)))) β†’ (β™―β€˜((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©)) = (𝑃 βˆ’ (𝑃 βˆ’ 2)))
29030, 278, 282, 289syl3anc 1372 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (β™―β€˜((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©)) = (𝑃 βˆ’ (𝑃 βˆ’ 2)))
291 nncan 11489 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ β„‚ ∧ 2 ∈ β„‚) β†’ (𝑃 βˆ’ (𝑃 βˆ’ 2)) = 2)
29278, 69, 291sylancl 587 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑃 βˆ’ (𝑃 βˆ’ 2)) = 2)
293290, 292eqtr2d 2774 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 2 = (β™―β€˜((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©)))
294288, 293eqtrid 2785 . . . . . . . . . . . . . 14 (πœ‘ β†’ (β™―β€˜βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) = (β™―β€˜((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©)))
295 ccatopth 14666 . . . . . . . . . . . . . 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 231 . . . . . . . . . . . 12 (πœ‘ β†’ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© = ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©) ∧ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) = ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
298297simprd 497 . . . . . . . . . . 11 (πœ‘ β†’ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) = ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩))
299275, 298oveq12d 7427 . . . . . . . . . 10 (πœ‘ β†’ (((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
300233, 299eqtr3d 2775 . . . . . . . . 9 (πœ‘ β†’ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩) = (((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
301300oveq2d 7425 . . . . . . . 8 (πœ‘ β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΅β€˜πΏ) prefix 𝑄) ++ (((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩))))
302 ccatass 14538 . . . . . . . . 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 2776 . . . . . . 7 (πœ‘ β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = ((((π΅β€˜πΏ) prefix 𝑄) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩)) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
305 ccatpfx 14651 . . . . . . . . 9 (((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) ∧ 𝑄 ∈ (0...(𝑃 βˆ’ 2)) ∧ (𝑃 βˆ’ 2) ∈ (0...(β™―β€˜(π΅β€˜πΏ)))) β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩)) = ((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)))
30630, 236, 251, 305syl3anc 1372 . . . . . . . 8 (πœ‘ β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩)) = ((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)))
307306oveq1d 7424 . . . . . . 7 (πœ‘ β†’ ((((π΅β€˜πΏ) prefix 𝑄) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩)) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)) = (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
30817, 304, 3073eqtrd 2777 . . . . . 6 (πœ‘ β†’ (π‘†β€˜πΆ) = (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
309 ccatrid 14537 . . . . . . . 8 (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ∈ Word (𝐼 Γ— 2o) β†’ (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ βˆ…) = ((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)))
310229, 309syl 17 . . . . . . 7 (πœ‘ β†’ (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ βˆ…) = ((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)))
311310oveq1d 7424 . . . . . 6 (πœ‘ β†’ ((((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ βˆ…) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)) = (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
312308, 311eqtr4d 2776 . . . . 5 (πœ‘ β†’ (π‘†β€˜πΆ) = ((((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ βˆ…) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
313 pfxlen 14633 . . . . . . 7 (((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) ∧ (𝑃 βˆ’ 2) ∈ (0...(β™―β€˜(π΅β€˜πΏ)))) β†’ (β™―β€˜((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2))) = (𝑃 βˆ’ 2))
31430, 251, 313syl2anc 585 . . . . . 6 (πœ‘ β†’ (β™―β€˜((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2))) = (𝑃 βˆ’ 2))
315314eqcomd 2739 . . . . 5 (πœ‘ β†’ (𝑃 βˆ’ 2) = (β™―β€˜((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2))))
316171oveq2i 7420 . . . . . 6 ((𝑃 βˆ’ 2) + (β™―β€˜βˆ…)) = ((𝑃 βˆ’ 2) + 0)
31776zcnd 12667 . . . . . . 7 (πœ‘ β†’ (𝑃 βˆ’ 2) ∈ β„‚)
318317addridd 11414 . . . . . 6 (πœ‘ β†’ ((𝑃 βˆ’ 2) + 0) = (𝑃 βˆ’ 2))
319316, 318eqtr2id 2786 . . . . 5 (πœ‘ β†’ (𝑃 βˆ’ 2) = ((𝑃 βˆ’ 2) + (β™―β€˜βˆ…)))
320229, 98, 231, 120, 312, 315, 319splval2 14707 . . . 4 (πœ‘ β†’ ((π‘†β€˜πΆ) splice ⟨(𝑃 βˆ’ 2), (𝑃 βˆ’ 2), βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©βŸ©) = ((((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
321297simpld 496 . . . . . . . 8 (πœ‘ β†’ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© = ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©))
322321oveq2d 7425 . . . . . . 7 (πœ‘ β†’ (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) = (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©)))
323 ccatpfx 14651 . . . . . . . 8 (((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) ∧ (𝑃 βˆ’ 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(β™―β€˜(π΅β€˜πΏ)))) β†’ (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©)) = ((π΅β€˜πΏ) prefix 𝑃))
32430, 278, 282, 323syl3anc 1372 . . . . . . 7 (πœ‘ β†’ (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©)) = ((π΅β€˜πΏ) prefix 𝑃))
325322, 324eqtrd 2773 . . . . . 6 (πœ‘ β†’ (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) = ((π΅β€˜πΏ) prefix 𝑃))
326325oveq1d 7424 . . . . 5 (πœ‘ β†’ ((((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)) = (((π΅β€˜πΏ) prefix 𝑃) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
327 ccatpfx 14651 . . . . . 6 (((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) ∧ 𝑃 ∈ (0...(β™―β€˜(π΅β€˜πΏ))) ∧ (β™―β€˜(π΅β€˜πΏ)) ∈ (0...(β™―β€˜(π΅β€˜πΏ)))) β†’ (((π΅β€˜πΏ) prefix 𝑃) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)) = ((π΅β€˜πΏ) prefix (β™―β€˜(π΅β€˜πΏ))))
32830, 282, 256, 327syl3anc 1372 . . . . 5 (πœ‘ β†’ (((π΅β€˜πΏ) prefix 𝑃) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)) = ((π΅β€˜πΏ) prefix (β™―β€˜(π΅β€˜πΏ))))
329 pfxid 14634 . . . . . 6 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΅β€˜πΏ) prefix (β™―β€˜(π΅β€˜πΏ))) = (π΅β€˜πΏ))
33030, 329syl 17 . . . . 5 (πœ‘ β†’ ((π΅β€˜πΏ) prefix (β™―β€˜(π΅β€˜πΏ))) = (π΅β€˜πΏ))
331326, 328, 3303eqtrd 2777 . . . 4 (πœ‘ β†’ ((((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)) = (π΅β€˜πΏ))
332227, 320, 3313eqtrd 2777 . . 3 (πœ‘ β†’ ((𝑃 βˆ’ 2)(π‘‡β€˜(π‘†β€˜πΆ))π‘ˆ) = (π΅β€˜πΏ))
333 fnovrn 7582 . . . 4 (((π‘‡β€˜(π‘†β€˜πΆ)) Fn ((0...(β™―β€˜(π‘†β€˜πΆ))) Γ— (𝐼 Γ— 2o)) ∧ (𝑃 βˆ’ 2) ∈ (0...(β™―β€˜(π‘†β€˜πΆ))) ∧ π‘ˆ ∈ (𝐼 Γ— 2o)) β†’ ((𝑃 βˆ’ 2)(π‘‡β€˜(π‘†β€˜πΆ))π‘ˆ) ∈ ran (π‘‡β€˜(π‘†β€˜πΆ)))
334218, 225, 117, 333syl3anc 1372 . . 3 (πœ‘ β†’ ((𝑃 βˆ’ 2)(π‘‡β€˜(π‘†β€˜πΆ))π‘ˆ) ∈ ran (π‘‡β€˜(π‘†β€˜πΆ)))
335332, 334eqeltrrd 2835 . 2 (πœ‘ β†’ (π΅β€˜πΏ) ∈ ran (π‘‡β€˜(π‘†β€˜πΆ)))
336221, 335jca 513 1 (πœ‘ β†’ ((π΄β€˜πΎ) ∈ ran (π‘‡β€˜(π‘†β€˜πΆ)) ∧ (π΅β€˜πΏ) ∈ ran (π‘‡β€˜(π‘†β€˜πΆ))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  {crab 3433   βˆ– cdif 3946  βˆ…c0 4323  {csn 4629  βŸ¨cop 4635  βŸ¨cotp 4637  βˆͺ ciun 4998   class class class wbr 5149   ↦ cmpt 5232   I cid 5574   Γ— cxp 5675  dom cdm 5677  ran crn 5678   Fn wfn 6539  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409   ∈ cmpo 7411  1oc1o 8459  2oc2o 8460  β„‚cc 11108  β„cr 11109  0cc0 11110  1c1 11111   + caddc 11113   < clt 11248   ≀ cle 11249   βˆ’ cmin 11444  2c2 12267  β„•0cn0 12472  β„€cz 12558  β„€β‰₯cuz 12822  ...cfz 13484  ..^cfzo 13627  β™―chash 14290  Word cword 14464   ++ cconcat 14520   substr csubstr 14590   prefix cpfx 14620   splice csplice 14699  βŸ¨β€œcs2 14792   ~FG cefg 19574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-ot 4638  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-2 12275  df-n0 12473  df-z 12559  df-uz 12823  df-fz 13485  df-fzo 13628  df-hash 14291  df-word 14465  df-concat 14521  df-s1 14546  df-substr 14591  df-pfx 14621  df-splice 14700  df-s2 14799
This theorem is referenced by:  efgredlemd  19612
  Copyright terms: Public domain W3C validator