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

Theorem efgredleme 19613
Description: Lemma for efgred 19618. (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 19599 . . . . . . . 8 𝑆:{𝑑 ∈ (Word π‘Š βˆ– {βˆ…}) ∣ ((π‘‘β€˜0) ∈ 𝐷 ∧ βˆ€π‘˜ ∈ (1..^(β™―β€˜π‘‘))(π‘‘β€˜π‘˜) ∈ ran (π‘‡β€˜(π‘‘β€˜(π‘˜ βˆ’ 1))))}βŸΆπ‘Š
98fdmi 6729 . . . . . . . . 9 dom 𝑆 = {𝑑 ∈ (Word π‘Š βˆ– {βˆ…}) ∣ ((π‘‘β€˜0) ∈ 𝐷 ∧ βˆ€π‘˜ ∈ (1..^(β™―β€˜π‘‘))(π‘‘β€˜π‘˜) ∈ ran (π‘‡β€˜(π‘‘β€˜(π‘˜ βˆ’ 1))))}
109feq2i 6709 . . . . . . . 8 (𝑆:dom π‘†βŸΆπ‘Š ↔ 𝑆:{𝑑 ∈ (Word π‘Š βˆ– {βˆ…}) ∣ ((π‘‘β€˜0) ∈ 𝐷 ∧ βˆ€π‘˜ ∈ (1..^(β™―β€˜π‘‘))(π‘‘β€˜π‘˜) ∈ ran (π‘‡β€˜(π‘‘β€˜(π‘˜ βˆ’ 1))))}βŸΆπ‘Š)
118, 10mpbir 230 . . . . . . 7 𝑆:dom π‘†βŸΆπ‘Š
1211ffvelcdmi 7085 . . . . . 6 (𝐢 ∈ dom 𝑆 β†’ (π‘†β€˜πΆ) ∈ π‘Š)
131, 12syl 17 . . . . 5 (πœ‘ β†’ (π‘†β€˜πΆ) ∈ π‘Š)
14 efgredlemb.q . . . . . . 7 (πœ‘ β†’ 𝑄 ∈ (0...(β™―β€˜(π΅β€˜πΏ))))
15 elfzuz 13499 . . . . . . 7 (𝑄 ∈ (0...(β™―β€˜(π΅β€˜πΏ))) β†’ 𝑄 ∈ (β„€β‰₯β€˜0))
1614, 15syl 17 . . . . . 6 (πœ‘ β†’ 𝑄 ∈ (β„€β‰₯β€˜0))
17 efgredlemd.sc . . . . . . . . . 10 (πœ‘ β†’ (π‘†β€˜πΆ) = (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)))
1817fveq2d 6895 . . . . . . . . 9 (πœ‘ β†’ (β™―β€˜(π‘†β€˜πΆ)) = (β™―β€˜(((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩))))
19 fviss 6968 . . . . . . . . . . . . 13 ( I β€˜Word (𝐼 Γ— 2o)) βŠ† Word (𝐼 Γ— 2o)
202, 19eqsstri 4016 . . . . . . . . . . . 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 19611 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π΄β€˜πΎ) ∈ π‘Š ∧ (π΅β€˜πΏ) ∈ π‘Š))
2928simprd 496 . . . . . . . . . . . 12 (πœ‘ β†’ (π΅β€˜πΏ) ∈ π‘Š)
3020, 29sselid 3980 . . . . . . . . . . 11 (πœ‘ β†’ (π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o))
31 pfxcl 14629 . . . . . . . . . . 11 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΅β€˜πΏ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o))
3230, 31syl 17 . . . . . . . . . 10 (πœ‘ β†’ ((π΅β€˜πΏ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o))
3328simpld 495 . . . . . . . . . . . 12 (πœ‘ β†’ (π΄β€˜πΎ) ∈ π‘Š)
3420, 33sselid 3980 . . . . . . . . . . 11 (πœ‘ β†’ (π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o))
35 swrdcl 14597 . . . . . . . . . . 11 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o))
3634, 35syl 17 . . . . . . . . . 10 (πœ‘ β†’ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o))
37 ccatlen 14527 . . . . . . . . . 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 14635 . . . . . . . . . . . 12 (((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) ∧ 𝑄 ∈ (0...(β™―β€˜(π΅β€˜πΏ)))) β†’ (β™―β€˜((π΅β€˜πΏ) prefix 𝑄)) = 𝑄)
4030, 14, 39syl2anc 584 . . . . . . . . . . 11 (πœ‘ β†’ (β™―β€˜((π΅β€˜πΏ) prefix 𝑄)) = 𝑄)
41 2nn0 12491 . . . . . . . . . . . . . 14 2 ∈ β„•0
42 uzaddcl 12890 . . . . . . . . . . . . . 14 ((𝑄 ∈ (β„€β‰₯β€˜0) ∧ 2 ∈ β„•0) β†’ (𝑄 + 2) ∈ (β„€β‰₯β€˜0))
4316, 41, 42sylancl 586 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑄 + 2) ∈ (β„€β‰₯β€˜0))
44 efgredlemb.p . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))))
45 elfzuz3 13500 . . . . . . . . . . . . . . 15 (𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))) β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜π‘ƒ))
4644, 45syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜π‘ƒ))
47 efgredlemd.9 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2)))
48 uztrn 12842 . . . . . . . . . . . . . 14 (((β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜π‘ƒ) ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜(𝑄 + 2)))
4946, 47, 48syl2anc 584 . . . . . . . . . . . . 13 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜(𝑄 + 2)))
50 elfzuzb 13497 . . . . . . . . . . . . 13 ((𝑄 + 2) ∈ (0...(β™―β€˜(π΄β€˜πΎ))) ↔ ((𝑄 + 2) ∈ (β„€β‰₯β€˜0) ∧ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜(𝑄 + 2))))
5143, 49, 50sylanbrc 583 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑄 + 2) ∈ (0...(β™―β€˜(π΄β€˜πΎ))))
52 lencl 14485 . . . . . . . . . . . . . . 15 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ β„•0)
5334, 52syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ β„•0)
54 nn0uz 12866 . . . . . . . . . . . . . 14 β„•0 = (β„€β‰₯β€˜0)
5553, 54eleqtrdi 2843 . . . . . . . . . . . . 13 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜0))
56 eluzfz2 13511 . . . . . . . . . . . . 13 ((β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜0) β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (0...(β™―β€˜(π΄β€˜πΎ))))
5755, 56syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (0...(β™―β€˜(π΄β€˜πΎ))))
58 swrdlen 14599 . . . . . . . . . . . 12 (((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) ∧ (𝑄 + 2) ∈ (0...(β™―β€˜(π΄β€˜πΎ))) ∧ (β™―β€˜(π΄β€˜πΎ)) ∈ (0...(β™―β€˜(π΄β€˜πΎ)))) β†’ (β™―β€˜((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = ((β™―β€˜(π΄β€˜πΎ)) βˆ’ (𝑄 + 2)))
5934, 51, 57, 58syl3anc 1371 . . . . . . . . . . 11 (πœ‘ β†’ (β™―β€˜((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = ((β™―β€˜(π΄β€˜πΎ)) βˆ’ (𝑄 + 2)))
6040, 59oveq12d 7429 . . . . . . . . . 10 (πœ‘ β†’ ((β™―β€˜((π΅β€˜πΏ) prefix 𝑄)) + (β™―β€˜((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩))) = (𝑄 + ((β™―β€˜(π΄β€˜πΎ)) βˆ’ (𝑄 + 2))))
6114elfzelzd 13504 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑄 ∈ β„€)
6261zcnd 12669 . . . . . . . . . . 11 (πœ‘ β†’ 𝑄 ∈ β„‚)
6353nn0cnd 12536 . . . . . . . . . . 11 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ β„‚)
64 2z 12596 . . . . . . . . . . . . 13 2 ∈ β„€
65 zaddcl 12604 . . . . . . . . . . . . 13 ((𝑄 ∈ β„€ ∧ 2 ∈ β„€) β†’ (𝑄 + 2) ∈ β„€)
6661, 64, 65sylancl 586 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑄 + 2) ∈ β„€)
6766zcnd 12669 . . . . . . . . . . 11 (πœ‘ β†’ (𝑄 + 2) ∈ β„‚)
6862, 63, 67addsubassd 11593 . . . . . . . . . 10 (πœ‘ β†’ ((𝑄 + (β™―β€˜(π΄β€˜πΎ))) βˆ’ (𝑄 + 2)) = (𝑄 + ((β™―β€˜(π΄β€˜πΎ)) βˆ’ (𝑄 + 2))))
69 2cn 12289 . . . . . . . . . . . 12 2 ∈ β„‚
7069a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ 2 ∈ β„‚)
7162, 63, 70pnpcand 11610 . . . . . . . . . 10 (πœ‘ β†’ ((𝑄 + (β™―β€˜(π΄β€˜πΎ))) βˆ’ (𝑄 + 2)) = ((β™―β€˜(π΄β€˜πΎ)) βˆ’ 2))
7260, 68, 713eqtr2d 2778 . . . . . . . . 9 (πœ‘ β†’ ((β™―β€˜((π΅β€˜πΏ) prefix 𝑄)) + (β™―β€˜((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩))) = ((β™―β€˜(π΄β€˜πΎ)) βˆ’ 2))
7318, 38, 723eqtrd 2776 . . . . . . . 8 (πœ‘ β†’ (β™―β€˜(π‘†β€˜πΆ)) = ((β™―β€˜(π΄β€˜πΎ)) βˆ’ 2))
7444elfzelzd 13504 . . . . . . . . . 10 (πœ‘ β†’ 𝑃 ∈ β„€)
75 zsubcl 12606 . . . . . . . . . 10 ((𝑃 ∈ β„€ ∧ 2 ∈ β„€) β†’ (𝑃 βˆ’ 2) ∈ β„€)
7674, 64, 75sylancl 586 . . . . . . . . 9 (πœ‘ β†’ (𝑃 βˆ’ 2) ∈ β„€)
7764a1i 11 . . . . . . . . 9 (πœ‘ β†’ 2 ∈ β„€)
7874zcnd 12669 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑃 ∈ β„‚)
79 npcan 11471 . . . . . . . . . . . 12 ((𝑃 ∈ β„‚ ∧ 2 ∈ β„‚) β†’ ((𝑃 βˆ’ 2) + 2) = 𝑃)
8078, 69, 79sylancl 586 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑃 βˆ’ 2) + 2) = 𝑃)
8180fveq2d 6895 . . . . . . . . . 10 (πœ‘ β†’ (β„€β‰₯β€˜((𝑃 βˆ’ 2) + 2)) = (β„€β‰₯β€˜π‘ƒ))
8246, 81eleqtrrd 2836 . . . . . . . . 9 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜((𝑃 βˆ’ 2) + 2)))
83 eluzsub 12854 . . . . . . . . 9 (((𝑃 βˆ’ 2) ∈ β„€ ∧ 2 ∈ β„€ ∧ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜((𝑃 βˆ’ 2) + 2))) β†’ ((β™―β€˜(π΄β€˜πΎ)) βˆ’ 2) ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2)))
8476, 77, 82, 83syl3anc 1371 . . . . . . . 8 (πœ‘ β†’ ((β™―β€˜(π΄β€˜πΎ)) βˆ’ 2) ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2)))
8573, 84eqeltrd 2833 . . . . . . 7 (πœ‘ β†’ (β™―β€˜(π‘†β€˜πΆ)) ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2)))
86 eluzsub 12854 . . . . . . . 8 ((𝑄 ∈ β„€ ∧ 2 ∈ β„€ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) β†’ (𝑃 βˆ’ 2) ∈ (β„€β‰₯β€˜π‘„))
8761, 77, 47, 86syl3anc 1371 . . . . . . 7 (πœ‘ β†’ (𝑃 βˆ’ 2) ∈ (β„€β‰₯β€˜π‘„))
88 uztrn 12842 . . . . . . 7 (((β™―β€˜(π‘†β€˜πΆ)) ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2)) ∧ (𝑃 βˆ’ 2) ∈ (β„€β‰₯β€˜π‘„)) β†’ (β™―β€˜(π‘†β€˜πΆ)) ∈ (β„€β‰₯β€˜π‘„))
8985, 87, 88syl2anc 584 . . . . . 6 (πœ‘ β†’ (β™―β€˜(π‘†β€˜πΆ)) ∈ (β„€β‰₯β€˜π‘„))
90 elfzuzb 13497 . . . . . 6 (𝑄 ∈ (0...(β™―β€˜(π‘†β€˜πΆ))) ↔ (𝑄 ∈ (β„€β‰₯β€˜0) ∧ (β™―β€˜(π‘†β€˜πΆ)) ∈ (β„€β‰₯β€˜π‘„)))
9116, 89, 90sylanbrc 583 . . . . 5 (πœ‘ β†’ 𝑄 ∈ (0...(β™―β€˜(π‘†β€˜πΆ))))
92 efgredlemb.v . . . . 5 (πœ‘ β†’ 𝑉 ∈ (𝐼 Γ— 2o))
932, 3, 4, 5efgtval 19593 . . . . 5 (((π‘†β€˜πΆ) ∈ π‘Š ∧ 𝑄 ∈ (0...(β™―β€˜(π‘†β€˜πΆ))) ∧ 𝑉 ∈ (𝐼 Γ— 2o)) β†’ (𝑄(π‘‡β€˜(π‘†β€˜πΆ))𝑉) = ((π‘†β€˜πΆ) splice βŸ¨π‘„, 𝑄, βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©βŸ©))
9413, 91, 92, 93syl3anc 1371 . . . 4 (πœ‘ β†’ (𝑄(π‘‡β€˜(π‘†β€˜πΆ))𝑉) = ((π‘†β€˜πΆ) splice βŸ¨π‘„, 𝑄, βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©βŸ©))
95 pfxcl 14629 . . . . . 6 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o))
9634, 95syl 17 . . . . 5 (πœ‘ β†’ ((π΄β€˜πΎ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o))
97 wrd0 14491 . . . . . 6 βˆ… ∈ Word (𝐼 Γ— 2o)
9897a1i 11 . . . . 5 (πœ‘ β†’ βˆ… ∈ Word (𝐼 Γ— 2o))
994efgmf 19583 . . . . . . . 8 𝑀:(𝐼 Γ— 2o)⟢(𝐼 Γ— 2o)
10099ffvelcdmi 7085 . . . . . . 7 (𝑉 ∈ (𝐼 Γ— 2o) β†’ (π‘€β€˜π‘‰) ∈ (𝐼 Γ— 2o))
10192, 100syl 17 . . . . . 6 (πœ‘ β†’ (π‘€β€˜π‘‰) ∈ (𝐼 Γ— 2o))
10292, 101s2cld 14824 . . . . 5 (πœ‘ β†’ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ∈ Word (𝐼 Γ— 2o))
10361zred 12668 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑄 ∈ ℝ)
104 nn0addge1 12520 . . . . . . . . . . . . . . . . 17 ((𝑄 ∈ ℝ ∧ 2 ∈ β„•0) β†’ 𝑄 ≀ (𝑄 + 2))
105103, 41, 104sylancl 586 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑄 ≀ (𝑄 + 2))
106 eluz2 12830 . . . . . . . . . . . . . . . 16 ((𝑄 + 2) ∈ (β„€β‰₯β€˜π‘„) ↔ (𝑄 ∈ β„€ ∧ (𝑄 + 2) ∈ β„€ ∧ 𝑄 ≀ (𝑄 + 2)))
10761, 66, 105, 106syl3anbrc 1343 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑄 + 2) ∈ (β„€β‰₯β€˜π‘„))
108 uztrn 12842 . . . . . . . . . . . . . . 15 ((𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (β„€β‰₯β€˜π‘„)) β†’ 𝑃 ∈ (β„€β‰₯β€˜π‘„))
10947, 107, 108syl2anc 584 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑃 ∈ (β„€β‰₯β€˜π‘„))
110 elfzuzb 13497 . . . . . . . . . . . . . 14 (𝑄 ∈ (0...𝑃) ↔ (𝑄 ∈ (β„€β‰₯β€˜0) ∧ 𝑃 ∈ (β„€β‰₯β€˜π‘„)))
11116, 109, 110sylanbrc 583 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑄 ∈ (0...𝑃))
112 ccatpfx 14653 . . . . . . . . . . . . 13 (((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) ∧ 𝑄 ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ)))) β†’ (((π΄β€˜πΎ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©)) = ((π΄β€˜πΎ) prefix 𝑃))
11334, 111, 44, 112syl3anc 1371 . . . . . . . . . . . 12 (πœ‘ β†’ (((π΄β€˜πΎ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©)) = ((π΄β€˜πΎ) prefix 𝑃))
114113oveq1d 7426 . . . . . . . . . . 11 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©)) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = (((π΄β€˜πΎ) prefix 𝑃) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))))
115 pfxcl 14629 . . . . . . . . . . . . 13 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) prefix 𝑃) ∈ Word (𝐼 Γ— 2o))
11634, 115syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ ((π΄β€˜πΎ) prefix 𝑃) ∈ Word (𝐼 Γ— 2o))
117 efgredlemb.u . . . . . . . . . . . . 13 (πœ‘ β†’ π‘ˆ ∈ (𝐼 Γ— 2o))
11899ffvelcdmi 7085 . . . . . . . . . . . . . 14 (π‘ˆ ∈ (𝐼 Γ— 2o) β†’ (π‘€β€˜π‘ˆ) ∈ (𝐼 Γ— 2o))
119117, 118syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘€β€˜π‘ˆ) ∈ (𝐼 Γ— 2o))
120117, 119s2cld 14824 . . . . . . . . . . . 12 (πœ‘ β†’ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ∈ Word (𝐼 Γ— 2o))
121 swrdcl 14597 . . . . . . . . . . . . 13 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o))
12234, 121syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o))
123 ccatass 14540 . . . . . . . . . . . 12 ((((π΄β€˜πΎ) prefix 𝑃) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ∈ Word (𝐼 Γ— 2o) ∧ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o)) β†’ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΄β€˜πΎ) prefix 𝑃) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))))
124116, 120, 122, 123syl3anc 1371 . . . . . . . . . . 11 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΄β€˜πΎ) prefix 𝑃) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))))
125 efgredlemb.6 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘†β€˜π΄) = (𝑃(π‘‡β€˜(π΄β€˜πΎ))π‘ˆ))
1262, 3, 4, 5efgtval 19593 . . . . . . . . . . . . . 14 (((π΄β€˜πΎ) ∈ π‘Š ∧ 𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))) ∧ π‘ˆ ∈ (𝐼 Γ— 2o)) β†’ (𝑃(π‘‡β€˜(π΄β€˜πΎ))π‘ˆ) = ((π΄β€˜πΎ) splice βŸ¨π‘ƒ, 𝑃, βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©βŸ©))
12733, 44, 117, 126syl3anc 1371 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑃(π‘‡β€˜(π΄β€˜πΎ))π‘ˆ) = ((π΄β€˜πΎ) splice βŸ¨π‘ƒ, 𝑃, βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©βŸ©))
128 splval 14703 . . . . . . . . . . . . . 14 (((π΄β€˜πΎ) ∈ π‘Š ∧ (𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))) ∧ 𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))) ∧ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ∈ Word (𝐼 Γ— 2o))) β†’ ((π΄β€˜πΎ) splice βŸ¨π‘ƒ, 𝑃, βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©βŸ©) = ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))
12933, 44, 44, 120, 128syl13anc 1372 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π΄β€˜πΎ) splice βŸ¨π‘ƒ, 𝑃, βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©βŸ©) = ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))
130125, 127, 1293eqtrd 2776 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘†β€˜π΄) = ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))
131 efgredlemb.7 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘†β€˜π΅) = (𝑄(π‘‡β€˜(π΅β€˜πΏ))𝑉))
1322, 3, 4, 5efgtval 19593 . . . . . . . . . . . . . 14 (((π΅β€˜πΏ) ∈ π‘Š ∧ 𝑄 ∈ (0...(β™―β€˜(π΅β€˜πΏ))) ∧ 𝑉 ∈ (𝐼 Γ— 2o)) β†’ (𝑄(π‘‡β€˜(π΅β€˜πΏ))𝑉) = ((π΅β€˜πΏ) splice βŸ¨π‘„, 𝑄, βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©βŸ©))
13329, 14, 92, 132syl3anc 1371 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑄(π‘‡β€˜(π΅β€˜πΏ))𝑉) = ((π΅β€˜πΏ) splice βŸ¨π‘„, 𝑄, βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©βŸ©))
134 splval 14703 . . . . . . . . . . . . . 14 (((π΅β€˜πΏ) ∈ π‘Š ∧ (𝑄 ∈ (0...(β™―β€˜(π΅β€˜πΏ))) ∧ 𝑄 ∈ (0...(β™―β€˜(π΅β€˜πΏ))) ∧ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ∈ Word (𝐼 Γ— 2o))) β†’ ((π΅β€˜πΏ) splice βŸ¨π‘„, 𝑄, βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©βŸ©) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
13529, 14, 14, 102, 134syl13anc 1372 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π΅β€˜πΏ) splice βŸ¨π‘„, 𝑄, βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©βŸ©) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
136131, 133, 1353eqtrd 2776 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘†β€˜π΅) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
13724, 130, 1363eqtr3d 2780 . . . . . . . . . . 11 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
138114, 124, 1373eqtr2d 2778 . . . . . . . . . 10 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©)) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
139 swrdcl 14597 . . . . . . . . . . . 12 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ∈ Word (𝐼 Γ— 2o))
14034, 139syl 17 . . . . . . . . . . 11 (πœ‘ β†’ ((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ∈ Word (𝐼 Γ— 2o))
141 ccatcl 14526 . . . . . . . . . . . 12 ((βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ∈ Word (𝐼 Γ— 2o) ∧ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o)) β†’ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) ∈ Word (𝐼 Γ— 2o))
142120, 122, 141syl2anc 584 . . . . . . . . . . 11 (πœ‘ β†’ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) ∈ Word (𝐼 Γ— 2o))
143 ccatass 14540 . . . . . . . . . . 11 ((((π΄β€˜πΎ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o) ∧ ((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ∈ Word (𝐼 Γ— 2o) ∧ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) ∈ Word (𝐼 Γ— 2o)) β†’ ((((π΄β€˜πΎ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©)) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = (((π΄β€˜πΎ) prefix 𝑄) ++ (((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))))
14496, 140, 142, 143syl3anc 1371 . . . . . . . . . 10 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©)) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = (((π΄β€˜πΎ) prefix 𝑄) ++ (((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))))
145 swrdcl 14597 . . . . . . . . . . . 12 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o))
14630, 145syl 17 . . . . . . . . . . 11 (πœ‘ β†’ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o))
147 ccatass 14540 . . . . . . . . . . 11 ((((π΅β€˜πΏ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ∈ Word (𝐼 Γ— 2o) ∧ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o)) β†’ ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)) = (((π΅β€˜πΏ) prefix 𝑄) ++ (βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩))))
14832, 102, 146, 147syl3anc 1371 . . . . . . . . . 10 (πœ‘ β†’ ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)) = (((π΅β€˜πΏ) prefix 𝑄) ++ (βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩))))
149138, 144, 1483eqtr3d 2780 . . . . . . . . 9 (πœ‘ β†’ (((π΄β€˜πΎ) prefix 𝑄) ++ (((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))) = (((π΅β€˜πΏ) prefix 𝑄) ++ (βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩))))
150 ccatcl 14526 . . . . . . . . . . 11 ((((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ∈ Word (𝐼 Γ— 2o) ∧ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) ∈ Word (𝐼 Γ— 2o)) β†’ (((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) ∈ Word (𝐼 Γ— 2o))
151140, 142, 150syl2anc 584 . . . . . . . . . 10 (πœ‘ β†’ (((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) ∈ Word (𝐼 Γ— 2o))
152 ccatcl 14526 . . . . . . . . . . 11 ((βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ∈ Word (𝐼 Γ— 2o) ∧ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o)) β†’ (βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)) ∈ Word (𝐼 Γ— 2o))
153102, 146, 152syl2anc 584 . . . . . . . . . 10 (πœ‘ β†’ (βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)) ∈ Word (𝐼 Γ— 2o))
154 uztrn 12842 . . . . . . . . . . . . . 14 (((β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜π‘ƒ) ∧ 𝑃 ∈ (β„€β‰₯β€˜π‘„)) β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜π‘„))
15546, 109, 154syl2anc 584 . . . . . . . . . . . . 13 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜π‘„))
156 elfzuzb 13497 . . . . . . . . . . . . 13 (𝑄 ∈ (0...(β™―β€˜(π΄β€˜πΎ))) ↔ (𝑄 ∈ (β„€β‰₯β€˜0) ∧ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜π‘„)))
15716, 155, 156sylanbrc 583 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑄 ∈ (0...(β™―β€˜(π΄β€˜πΎ))))
158 pfxlen 14635 . . . . . . . . . . . 12 (((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) ∧ 𝑄 ∈ (0...(β™―β€˜(π΄β€˜πΎ)))) β†’ (β™―β€˜((π΄β€˜πΎ) prefix 𝑄)) = 𝑄)
15934, 157, 158syl2anc 584 . . . . . . . . . . 11 (πœ‘ β†’ (β™―β€˜((π΄β€˜πΎ) prefix 𝑄)) = 𝑄)
160159, 40eqtr4d 2775 . . . . . . . . . 10 (πœ‘ β†’ (β™―β€˜((π΄β€˜πΎ) prefix 𝑄)) = (β™―β€˜((π΅β€˜πΏ) prefix 𝑄)))
161 ccatopth 14668 . . . . . . . . . 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 1381 . . . . . . . . 9 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑄) ++ (((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))) = (((π΅β€˜πΏ) prefix 𝑄) ++ (βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩))) ↔ (((π΄β€˜πΎ) prefix 𝑄) = ((π΅β€˜πΏ) prefix 𝑄) ∧ (((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = (βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))))
163149, 162mpbid 231 . . . . . . . 8 (πœ‘ β†’ (((π΄β€˜πΎ) prefix 𝑄) = ((π΅β€˜πΏ) prefix 𝑄) ∧ (((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = (βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩))))
164163simpld 495 . . . . . . 7 (πœ‘ β†’ ((π΄β€˜πΎ) prefix 𝑄) = ((π΅β€˜πΏ) prefix 𝑄))
165164oveq1d 7426 . . . . . 6 (πœ‘ β†’ (((π΄β€˜πΎ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)))
166 ccatrid 14539 . . . . . . . 8 (((π΄β€˜πΎ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o) β†’ (((π΄β€˜πΎ) prefix 𝑄) ++ βˆ…) = ((π΄β€˜πΎ) prefix 𝑄))
16796, 166syl 17 . . . . . . 7 (πœ‘ β†’ (((π΄β€˜πΎ) prefix 𝑄) ++ βˆ…) = ((π΄β€˜πΎ) prefix 𝑄))
168167oveq1d 7426 . . . . . 6 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑄) ++ βˆ…) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΄β€˜πΎ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)))
169165, 168, 173eqtr4rd 2783 . . . . 5 (πœ‘ β†’ (π‘†β€˜πΆ) = ((((π΄β€˜πΎ) prefix 𝑄) ++ βˆ…) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)))
170159eqcomd 2738 . . . . 5 (πœ‘ β†’ 𝑄 = (β™―β€˜((π΄β€˜πΎ) prefix 𝑄)))
171 hash0 14329 . . . . . . 7 (β™―β€˜βˆ…) = 0
172171oveq2i 7422 . . . . . 6 (𝑄 + (β™―β€˜βˆ…)) = (𝑄 + 0)
17362addridd 11416 . . . . . 6 (πœ‘ β†’ (𝑄 + 0) = 𝑄)
174172, 173eqtr2id 2785 . . . . 5 (πœ‘ β†’ 𝑄 = (𝑄 + (β™―β€˜βˆ…)))
17596, 98, 36, 102, 169, 170, 174splval2 14709 . . . 4 (πœ‘ β†’ ((π‘†β€˜πΆ) splice βŸ¨π‘„, 𝑄, βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©βŸ©) = ((((π΄β€˜πΎ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)))
176 elfzuzb 13497 . . . . . . . . . . . . . 14 (𝑄 ∈ (0...(𝑄 + 2)) ↔ (𝑄 ∈ (β„€β‰₯β€˜0) ∧ (𝑄 + 2) ∈ (β„€β‰₯β€˜π‘„)))
17716, 107, 176sylanbrc 583 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑄 ∈ (0...(𝑄 + 2)))
178 elfzuzb 13497 . . . . . . . . . . . . . 14 ((𝑄 + 2) ∈ (0...𝑃) ↔ ((𝑄 + 2) ∈ (β„€β‰₯β€˜0) ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))))
17943, 47, 178sylanbrc 583 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑄 + 2) ∈ (0...𝑃))
180 ccatswrd 14620 . . . . . . . . . . . . 13 (((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) ∧ (𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))))) β†’ (((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©)) = ((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©))
18134, 177, 179, 44, 180syl13anc 1372 . . . . . . . . . . . 12 (πœ‘ β†’ (((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©)) = ((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©))
182181oveq1d 7426 . . . . . . . . . . 11 (πœ‘ β†’ ((((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©)) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = (((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))))
183 swrdcl 14597 . . . . . . . . . . . . 13 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩) ∈ Word (𝐼 Γ— 2o))
18434, 183syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ ((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩) ∈ Word (𝐼 Γ— 2o))
185 swrdcl 14597 . . . . . . . . . . . . 13 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ∈ Word (𝐼 Γ— 2o))
18634, 185syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ∈ Word (𝐼 Γ— 2o))
187 ccatass 14540 . . . . . . . . . . . 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 1371 . . . . . . . . . . 11 (πœ‘ β†’ ((((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©)) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = (((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩) ++ (((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))))
189163simprd 496 . . . . . . . . . . 11 (πœ‘ β†’ (((π΄β€˜πΎ) substr βŸ¨π‘„, π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = (βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
190182, 188, 1893eqtr3d 2780 . . . . . . . . . 10 (πœ‘ β†’ (((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩) ++ (((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))) = (βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
191 ccatcl 14526 . . . . . . . . . . . 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 14599 . . . . . . . . . . . . . 14 (((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(β™―β€˜(π΄β€˜πΎ)))) β†’ (β™―β€˜((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩)) = ((𝑄 + 2) βˆ’ 𝑄))
19434, 177, 51, 193syl3anc 1371 . . . . . . . . . . . . 13 (πœ‘ β†’ (β™―β€˜((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩)) = ((𝑄 + 2) βˆ’ 𝑄))
195 pncan2 11469 . . . . . . . . . . . . . 14 ((𝑄 ∈ β„‚ ∧ 2 ∈ β„‚) β†’ ((𝑄 + 2) βˆ’ 𝑄) = 2)
19662, 69, 195sylancl 586 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝑄 + 2) βˆ’ 𝑄) = 2)
197194, 196eqtrd 2772 . . . . . . . . . . . 12 (πœ‘ β†’ (β™―β€˜((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩)) = 2)
198 s2len 14842 . . . . . . . . . . . 12 (β™―β€˜βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) = 2
199197, 198eqtr4di 2790 . . . . . . . . . . 11 (πœ‘ β†’ (β™―β€˜((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩)) = (β™―β€˜βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©))
200 ccatopth 14668 . . . . . . . . . . 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 1381 . . . . . . . . . 10 (πœ‘ β†’ ((((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩) ++ (((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))) = (βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)) ↔ (((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩) = βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ∧ (((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩))))
202190, 201mpbid 231 . . . . . . . . 9 (πœ‘ β†’ (((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩) = βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ∧ (((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
203202simpld 495 . . . . . . . 8 (πœ‘ β†’ ((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩) = βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©)
204203oveq2d 7427 . . . . . . 7 (πœ‘ β†’ (((π΄β€˜πΎ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩)) = (((π΄β€˜πΎ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©))
205 ccatpfx 14653 . . . . . . . 8 (((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) ∧ 𝑄 ∈ (0...(𝑄 + 2)) ∧ (𝑄 + 2) ∈ (0...(β™―β€˜(π΄β€˜πΎ)))) β†’ (((π΄β€˜πΎ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩)) = ((π΄β€˜πΎ) prefix (𝑄 + 2)))
20634, 177, 51, 205syl3anc 1371 . . . . . . 7 (πœ‘ β†’ (((π΄β€˜πΎ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr βŸ¨π‘„, (𝑄 + 2)⟩)) = ((π΄β€˜πΎ) prefix (𝑄 + 2)))
207204, 206eqtr3d 2774 . . . . . 6 (πœ‘ β†’ (((π΄β€˜πΎ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) = ((π΄β€˜πΎ) prefix (𝑄 + 2)))
208207oveq1d 7426 . . . . 5 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΄β€˜πΎ) prefix (𝑄 + 2)) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)))
209 ccatpfx 14653 . . . . . 6 (((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) ∧ (𝑄 + 2) ∈ (0...(β™―β€˜(π΄β€˜πΎ))) ∧ (β™―β€˜(π΄β€˜πΎ)) ∈ (0...(β™―β€˜(π΄β€˜πΎ)))) β†’ (((π΄β€˜πΎ) prefix (𝑄 + 2)) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = ((π΄β€˜πΎ) prefix (β™―β€˜(π΄β€˜πΎ))))
21034, 51, 57, 209syl3anc 1371 . . . . 5 (πœ‘ β†’ (((π΄β€˜πΎ) prefix (𝑄 + 2)) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = ((π΄β€˜πΎ) prefix (β™―β€˜(π΄β€˜πΎ))))
211 pfxid 14636 . . . . . 6 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) prefix (β™―β€˜(π΄β€˜πΎ))) = (π΄β€˜πΎ))
21234, 211syl 17 . . . . 5 (πœ‘ β†’ ((π΄β€˜πΎ) prefix (β™―β€˜(π΄β€˜πΎ))) = (π΄β€˜πΎ))
213208, 210, 2123eqtrd 2776 . . . 4 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π΄β€˜πΎ))
21494, 175, 2133eqtrd 2776 . . 3 (πœ‘ β†’ (𝑄(π‘‡β€˜(π‘†β€˜πΆ))𝑉) = (π΄β€˜πΎ))
2152, 3, 4, 5efgtf 19592 . . . . . . 7 ((π‘†β€˜πΆ) ∈ π‘Š β†’ ((π‘‡β€˜(π‘†β€˜πΆ)) = (π‘Ž ∈ (0...(β™―β€˜(π‘†β€˜πΆ))), 𝑖 ∈ (𝐼 Γ— 2o) ↦ ((π‘†β€˜πΆ) splice βŸ¨π‘Ž, π‘Ž, βŸ¨β€œπ‘–(π‘€β€˜π‘–)β€βŸ©βŸ©)) ∧ (π‘‡β€˜(π‘†β€˜πΆ)):((0...(β™―β€˜(π‘†β€˜πΆ))) Γ— (𝐼 Γ— 2o))βŸΆπ‘Š))
21613, 215syl 17 . . . . . 6 (πœ‘ β†’ ((π‘‡β€˜(π‘†β€˜πΆ)) = (π‘Ž ∈ (0...(β™―β€˜(π‘†β€˜πΆ))), 𝑖 ∈ (𝐼 Γ— 2o) ↦ ((π‘†β€˜πΆ) splice βŸ¨π‘Ž, π‘Ž, βŸ¨β€œπ‘–(π‘€β€˜π‘–)β€βŸ©βŸ©)) ∧ (π‘‡β€˜(π‘†β€˜πΆ)):((0...(β™―β€˜(π‘†β€˜πΆ))) Γ— (𝐼 Γ— 2o))βŸΆπ‘Š))
217216simprd 496 . . . . 5 (πœ‘ β†’ (π‘‡β€˜(π‘†β€˜πΆ)):((0...(β™―β€˜(π‘†β€˜πΆ))) Γ— (𝐼 Γ— 2o))βŸΆπ‘Š)
218217ffnd 6718 . . . 4 (πœ‘ β†’ (π‘‡β€˜(π‘†β€˜πΆ)) Fn ((0...(β™―β€˜(π‘†β€˜πΆ))) Γ— (𝐼 Γ— 2o)))
219 fnovrn 7584 . . . 4 (((π‘‡β€˜(π‘†β€˜πΆ)) Fn ((0...(β™―β€˜(π‘†β€˜πΆ))) Γ— (𝐼 Γ— 2o)) ∧ 𝑄 ∈ (0...(β™―β€˜(π‘†β€˜πΆ))) ∧ 𝑉 ∈ (𝐼 Γ— 2o)) β†’ (𝑄(π‘‡β€˜(π‘†β€˜πΆ))𝑉) ∈ ran (π‘‡β€˜(π‘†β€˜πΆ)))
220218, 91, 92, 219syl3anc 1371 . . 3 (πœ‘ β†’ (𝑄(π‘‡β€˜(π‘†β€˜πΆ))𝑉) ∈ ran (π‘‡β€˜(π‘†β€˜πΆ)))
221214, 220eqeltrrd 2834 . 2 (πœ‘ β†’ (π΄β€˜πΎ) ∈ ran (π‘‡β€˜(π‘†β€˜πΆ)))
222 uztrn 12842 . . . . . . 7 (((𝑃 βˆ’ 2) ∈ (β„€β‰₯β€˜π‘„) ∧ 𝑄 ∈ (β„€β‰₯β€˜0)) β†’ (𝑃 βˆ’ 2) ∈ (β„€β‰₯β€˜0))
22387, 16, 222syl2anc 584 . . . . . 6 (πœ‘ β†’ (𝑃 βˆ’ 2) ∈ (β„€β‰₯β€˜0))
224 elfzuzb 13497 . . . . . 6 ((𝑃 βˆ’ 2) ∈ (0...(β™―β€˜(π‘†β€˜πΆ))) ↔ ((𝑃 βˆ’ 2) ∈ (β„€β‰₯β€˜0) ∧ (β™―β€˜(π‘†β€˜πΆ)) ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2))))
225223, 85, 224sylanbrc 583 . . . . 5 (πœ‘ β†’ (𝑃 βˆ’ 2) ∈ (0...(β™―β€˜(π‘†β€˜πΆ))))
2262, 3, 4, 5efgtval 19593 . . . . 5 (((π‘†β€˜πΆ) ∈ π‘Š ∧ (𝑃 βˆ’ 2) ∈ (0...(β™―β€˜(π‘†β€˜πΆ))) ∧ π‘ˆ ∈ (𝐼 Γ— 2o)) β†’ ((𝑃 βˆ’ 2)(π‘‡β€˜(π‘†β€˜πΆ))π‘ˆ) = ((π‘†β€˜πΆ) splice ⟨(𝑃 βˆ’ 2), (𝑃 βˆ’ 2), βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©βŸ©))
22713, 225, 117, 226syl3anc 1371 . . . 4 (πœ‘ β†’ ((𝑃 βˆ’ 2)(π‘‡β€˜(π‘†β€˜πΆ))π‘ˆ) = ((π‘†β€˜πΆ) splice ⟨(𝑃 βˆ’ 2), (𝑃 βˆ’ 2), βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©βŸ©))
228 pfxcl 14629 . . . . . 6 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ∈ Word (𝐼 Γ— 2o))
22930, 228syl 17 . . . . 5 (πœ‘ β†’ ((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ∈ Word (𝐼 Γ— 2o))
230 swrdcl 14597 . . . . . 6 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o))
23130, 230syl 17 . . . . 5 (πœ‘ β†’ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o))
232 ccatswrd 14620 . . . . . . . . . . 11 (((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) ∧ ((𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))) ∧ (β™―β€˜(π΄β€˜πΎ)) ∈ (0...(β™―β€˜(π΄β€˜πΎ))))) β†’ (((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩))
23334, 179, 44, 57, 232syl13anc 1372 . . . . . . . . . 10 (πœ‘ β†’ (((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩))
234202simprd 496 . . . . . . . . . . . . . 14 (πœ‘ β†’ (((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩))
235 elfzuzb 13497 . . . . . . . . . . . . . . . 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 19612 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) = (β™―β€˜(π΅β€˜πΏ)))
238237, 46eqeltrrd 2834 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ (β„€β‰₯β€˜π‘ƒ))
239 0le2 12316 . . . . . . . . . . . . . . . . . . . 20 0 ≀ 2
240239a1i 11 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 0 ≀ 2)
24174zred 12668 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝑃 ∈ ℝ)
242 2re 12288 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
243 subge02 11732 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℝ ∧ 2 ∈ ℝ) β†’ (0 ≀ 2 ↔ (𝑃 βˆ’ 2) ≀ 𝑃))
244241, 242, 243sylancl 586 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (0 ≀ 2 ↔ (𝑃 βˆ’ 2) ≀ 𝑃))
245240, 244mpbid 231 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝑃 βˆ’ 2) ≀ 𝑃)
246 eluz2 12830 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2)) ↔ ((𝑃 βˆ’ 2) ∈ β„€ ∧ 𝑃 ∈ β„€ ∧ (𝑃 βˆ’ 2) ≀ 𝑃))
24776, 74, 245, 246syl3anbrc 1343 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑃 ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2)))
248 uztrn 12842 . . . . . . . . . . . . . . . . 17 (((β™―β€˜(π΅β€˜πΏ)) ∈ (β„€β‰₯β€˜π‘ƒ) ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2))) β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2)))
249238, 247, 248syl2anc 584 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2)))
250 elfzuzb 13497 . . . . . . . . . . . . . . . 16 ((𝑃 βˆ’ 2) ∈ (0...(β™―β€˜(π΅β€˜πΏ))) ↔ ((𝑃 βˆ’ 2) ∈ (β„€β‰₯β€˜0) ∧ (β™―β€˜(π΅β€˜πΏ)) ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2))))
251223, 249, 250sylanbrc 583 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑃 βˆ’ 2) ∈ (0...(β™―β€˜(π΅β€˜πΏ))))
252 lencl 14485 . . . . . . . . . . . . . . . . . 18 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ β„•0)
25330, 252syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ β„•0)
254253, 54eleqtrdi 2843 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ (β„€β‰₯β€˜0))
255 eluzfz2 13511 . . . . . . . . . . . . . . . 16 ((β™―β€˜(π΅β€˜πΏ)) ∈ (β„€β‰₯β€˜0) β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ (0...(β™―β€˜(π΅β€˜πΏ))))
256254, 255syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ (0...(β™―β€˜(π΅β€˜πΏ))))
257 ccatswrd 14620 . . . . . . . . . . . . . . 15 (((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) ∧ (𝑄 ∈ (0...(𝑃 βˆ’ 2)) ∧ (𝑃 βˆ’ 2) ∈ (0...(β™―β€˜(π΅β€˜πΏ))) ∧ (β™―β€˜(π΅β€˜πΏ)) ∈ (0...(β™―β€˜(π΅β€˜πΏ))))) β†’ (((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩) ++ ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), (β™―β€˜(π΅β€˜πΏ))⟩)) = ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩))
25830, 236, 251, 256, 257syl13anc 1372 . . . . . . . . . . . . . 14 (πœ‘ β†’ (((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩) ++ ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), (β™―β€˜(π΅β€˜πΏ))⟩)) = ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩))
259234, 258eqtr4d 2775 . . . . . . . . . . . . 13 (πœ‘ β†’ (((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ++ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = (((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩) ++ ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), (β™―β€˜(π΅β€˜πΏ))⟩)))
260 swrdcl 14597 . . . . . . . . . . . . . . 15 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩) ∈ Word (𝐼 Γ— 2o))
26130, 260syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩) ∈ Word (𝐼 Γ— 2o))
262 swrdcl 14597 . . . . . . . . . . . . . . 15 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o))
26330, 262syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o))
264 swrdlen 14599 . . . . . . . . . . . . . . . 16 (((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) ∧ (𝑄 + 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ)))) β†’ (β™―β€˜((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©)) = (𝑃 βˆ’ (𝑄 + 2)))
26534, 179, 44, 264syl3anc 1371 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (β™―β€˜((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©)) = (𝑃 βˆ’ (𝑄 + 2)))
266 swrdlen 14599 . . . . . . . . . . . . . . . . 17 (((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) ∧ 𝑄 ∈ (0...(𝑃 βˆ’ 2)) ∧ (𝑃 βˆ’ 2) ∈ (0...(β™―β€˜(π΅β€˜πΏ)))) β†’ (β™―β€˜((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩)) = ((𝑃 βˆ’ 2) βˆ’ 𝑄))
26730, 236, 251, 266syl3anc 1371 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (β™―β€˜((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩)) = ((𝑃 βˆ’ 2) βˆ’ 𝑄))
26878, 62, 70sub32d 11605 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((𝑃 βˆ’ 𝑄) βˆ’ 2) = ((𝑃 βˆ’ 2) βˆ’ 𝑄))
26978, 62, 70subsub4d 11604 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((𝑃 βˆ’ 𝑄) βˆ’ 2) = (𝑃 βˆ’ (𝑄 + 2)))
270267, 268, 2693eqtr2d 2778 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (β™―β€˜((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩)) = (𝑃 βˆ’ (𝑄 + 2)))
271265, 270eqtr4d 2775 . . . . . . . . . . . . . 14 (πœ‘ β†’ (β™―β€˜((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©)) = (β™―β€˜((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩)))
272 ccatopth 14668 . . . . . . . . . . . . . 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 1381 . . . . . . . . . . . . 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 495 . . . . . . . . . . 11 (πœ‘ β†’ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) = ((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩))
276274simprd 496 . . . . . . . . . . . . . 14 (πœ‘ β†’ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), (β™―β€˜(π΅β€˜πΏ))⟩))
277 elfzuzb 13497 . . . . . . . . . . . . . . . 16 ((𝑃 βˆ’ 2) ∈ (0...𝑃) ↔ ((𝑃 βˆ’ 2) ∈ (β„€β‰₯β€˜0) ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑃 βˆ’ 2))))
278223, 247, 277sylanbrc 583 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑃 βˆ’ 2) ∈ (0...𝑃))
279 elfzuz 13499 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))) β†’ 𝑃 ∈ (β„€β‰₯β€˜0))
28044, 279syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑃 ∈ (β„€β‰₯β€˜0))
281 elfzuzb 13497 . . . . . . . . . . . . . . . 16 (𝑃 ∈ (0...(β™―β€˜(π΅β€˜πΏ))) ↔ (𝑃 ∈ (β„€β‰₯β€˜0) ∧ (β™―β€˜(π΅β€˜πΏ)) ∈ (β„€β‰₯β€˜π‘ƒ)))
282280, 238, 281sylanbrc 583 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑃 ∈ (0...(β™―β€˜(π΅β€˜πΏ))))
283 ccatswrd 14620 . . . . . . . . . . . . . . 15 (((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) ∧ ((𝑃 βˆ’ 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(β™―β€˜(π΅β€˜πΏ))) ∧ (β™―β€˜(π΅β€˜πΏ)) ∈ (0...(β™―β€˜(π΅β€˜πΏ))))) β†’ (((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)) = ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), (β™―β€˜(π΅β€˜πΏ))⟩))
28430, 278, 282, 256, 283syl13anc 1372 . . . . . . . . . . . . . 14 (πœ‘ β†’ (((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)) = ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), (β™―β€˜(π΅β€˜πΏ))⟩))
285276, 284eqtr4d 2775 . . . . . . . . . . . . 13 (πœ‘ β†’ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
286 swrdcl 14597 . . . . . . . . . . . . . . 15 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©) ∈ Word (𝐼 Γ— 2o))
28730, 286syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©) ∈ Word (𝐼 Γ— 2o))
288 s2len 14842 . . . . . . . . . . . . . . 15 (β™―β€˜βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) = 2
289 swrdlen 14599 . . . . . . . . . . . . . . . . 17 (((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) ∧ (𝑃 βˆ’ 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(β™―β€˜(π΅β€˜πΏ)))) β†’ (β™―β€˜((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©)) = (𝑃 βˆ’ (𝑃 βˆ’ 2)))
29030, 278, 282, 289syl3anc 1371 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (β™―β€˜((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©)) = (𝑃 βˆ’ (𝑃 βˆ’ 2)))
291 nncan 11491 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ β„‚ ∧ 2 ∈ β„‚) β†’ (𝑃 βˆ’ (𝑃 βˆ’ 2)) = 2)
29278, 69, 291sylancl 586 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑃 βˆ’ (𝑃 βˆ’ 2)) = 2)
293290, 292eqtr2d 2773 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 2 = (β™―β€˜((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©)))
294288, 293eqtrid 2784 . . . . . . . . . . . . . 14 (πœ‘ β†’ (β™―β€˜βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) = (β™―β€˜((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©)))
295 ccatopth 14668 . . . . . . . . . . . . . 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 1381 . . . . . . . . . . . . 13 (πœ‘ β†’ ((βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)) ↔ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© = ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©) ∧ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) = ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩))))
297285, 296mpbid 231 . . . . . . . . . . . 12 (πœ‘ β†’ (βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© = ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©) ∧ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) = ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
298297simprd 496 . . . . . . . . . . 11 (πœ‘ β†’ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) = ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩))
299275, 298oveq12d 7429 . . . . . . . . . 10 (πœ‘ β†’ (((π΄β€˜πΎ) substr ⟨(𝑄 + 2), π‘ƒβŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
300233, 299eqtr3d 2774 . . . . . . . . 9 (πœ‘ β†’ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩) = (((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
301300oveq2d 7427 . . . . . . . 8 (πœ‘ β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΅β€˜πΏ) prefix 𝑄) ++ (((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩))))
302 ccatass 14540 . . . . . . . . 9 ((((π΅β€˜πΏ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o) ∧ ((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩) ∈ Word (𝐼 Γ— 2o) ∧ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o)) β†’ ((((π΅β€˜πΏ) prefix 𝑄) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩)) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)) = (((π΅β€˜πΏ) prefix 𝑄) ++ (((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩))))
30332, 261, 231, 302syl3anc 1371 . . . . . . . 8 (πœ‘ β†’ ((((π΅β€˜πΏ) prefix 𝑄) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩)) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)) = (((π΅β€˜πΏ) prefix 𝑄) ++ (((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩))))
304301, 303eqtr4d 2775 . . . . . . 7 (πœ‘ β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = ((((π΅β€˜πΏ) prefix 𝑄) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩)) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
305 ccatpfx 14653 . . . . . . . . 9 (((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) ∧ 𝑄 ∈ (0...(𝑃 βˆ’ 2)) ∧ (𝑃 βˆ’ 2) ∈ (0...(β™―β€˜(π΅β€˜πΏ)))) β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩)) = ((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)))
30630, 236, 251, 305syl3anc 1371 . . . . . . . 8 (πœ‘ β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩)) = ((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)))
307306oveq1d 7426 . . . . . . 7 (πœ‘ β†’ ((((π΅β€˜πΏ) prefix 𝑄) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (𝑃 βˆ’ 2)⟩)) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)) = (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
30817, 304, 3073eqtrd 2776 . . . . . 6 (πœ‘ β†’ (π‘†β€˜πΆ) = (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
309 ccatrid 14539 . . . . . . . 8 (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ∈ Word (𝐼 Γ— 2o) β†’ (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ βˆ…) = ((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)))
310229, 309syl 17 . . . . . . 7 (πœ‘ β†’ (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ βˆ…) = ((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)))
311310oveq1d 7426 . . . . . 6 (πœ‘ β†’ ((((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ βˆ…) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)) = (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
312308, 311eqtr4d 2775 . . . . 5 (πœ‘ β†’ (π‘†β€˜πΆ) = ((((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ βˆ…) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
313 pfxlen 14635 . . . . . . 7 (((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) ∧ (𝑃 βˆ’ 2) ∈ (0...(β™―β€˜(π΅β€˜πΏ)))) β†’ (β™―β€˜((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2))) = (𝑃 βˆ’ 2))
31430, 251, 313syl2anc 584 . . . . . 6 (πœ‘ β†’ (β™―β€˜((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2))) = (𝑃 βˆ’ 2))
315314eqcomd 2738 . . . . 5 (πœ‘ β†’ (𝑃 βˆ’ 2) = (β™―β€˜((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2))))
316171oveq2i 7422 . . . . . 6 ((𝑃 βˆ’ 2) + (β™―β€˜βˆ…)) = ((𝑃 βˆ’ 2) + 0)
31776zcnd 12669 . . . . . . 7 (πœ‘ β†’ (𝑃 βˆ’ 2) ∈ β„‚)
318317addridd 11416 . . . . . 6 (πœ‘ β†’ ((𝑃 βˆ’ 2) + 0) = (𝑃 βˆ’ 2))
319316, 318eqtr2id 2785 . . . . 5 (πœ‘ β†’ (𝑃 βˆ’ 2) = ((𝑃 βˆ’ 2) + (β™―β€˜βˆ…)))
320229, 98, 231, 120, 312, 315, 319splval2 14709 . . . 4 (πœ‘ β†’ ((π‘†β€˜πΆ) splice ⟨(𝑃 βˆ’ 2), (𝑃 βˆ’ 2), βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©βŸ©) = ((((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
321297simpld 495 . . . . . . . 8 (πœ‘ β†’ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© = ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©))
322321oveq2d 7427 . . . . . . 7 (πœ‘ β†’ (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) = (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©)))
323 ccatpfx 14653 . . . . . . . 8 (((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) ∧ (𝑃 βˆ’ 2) ∈ (0...𝑃) ∧ 𝑃 ∈ (0...(β™―β€˜(π΅β€˜πΏ)))) β†’ (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©)) = ((π΅β€˜πΏ) prefix 𝑃))
32430, 278, 282, 323syl3anc 1371 . . . . . . 7 (πœ‘ β†’ (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ ((π΅β€˜πΏ) substr ⟨(𝑃 βˆ’ 2), π‘ƒβŸ©)) = ((π΅β€˜πΏ) prefix 𝑃))
325322, 324eqtrd 2772 . . . . . 6 (πœ‘ β†’ (((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) = ((π΅β€˜πΏ) prefix 𝑃))
326325oveq1d 7426 . . . . 5 (πœ‘ β†’ ((((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)) = (((π΅β€˜πΏ) prefix 𝑃) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)))
327 ccatpfx 14653 . . . . . 6 (((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) ∧ 𝑃 ∈ (0...(β™―β€˜(π΅β€˜πΏ))) ∧ (β™―β€˜(π΅β€˜πΏ)) ∈ (0...(β™―β€˜(π΅β€˜πΏ)))) β†’ (((π΅β€˜πΏ) prefix 𝑃) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)) = ((π΅β€˜πΏ) prefix (β™―β€˜(π΅β€˜πΏ))))
32830, 282, 256, 327syl3anc 1371 . . . . 5 (πœ‘ β†’ (((π΅β€˜πΏ) prefix 𝑃) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)) = ((π΅β€˜πΏ) prefix (β™―β€˜(π΅β€˜πΏ))))
329 pfxid 14636 . . . . . 6 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΅β€˜πΏ) prefix (β™―β€˜(π΅β€˜πΏ))) = (π΅β€˜πΏ))
33030, 329syl 17 . . . . 5 (πœ‘ β†’ ((π΅β€˜πΏ) prefix (β™―β€˜(π΅β€˜πΏ))) = (π΅β€˜πΏ))
331326, 328, 3303eqtrd 2776 . . . 4 (πœ‘ β†’ ((((π΅β€˜πΏ) prefix (𝑃 βˆ’ 2)) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘ƒ, (β™―β€˜(π΅β€˜πΏ))⟩)) = (π΅β€˜πΏ))
332227, 320, 3313eqtrd 2776 . . 3 (πœ‘ β†’ ((𝑃 βˆ’ 2)(π‘‡β€˜(π‘†β€˜πΆ))π‘ˆ) = (π΅β€˜πΏ))
333 fnovrn 7584 . . . 4 (((π‘‡β€˜(π‘†β€˜πΆ)) Fn ((0...(β™―β€˜(π‘†β€˜πΆ))) Γ— (𝐼 Γ— 2o)) ∧ (𝑃 βˆ’ 2) ∈ (0...(β™―β€˜(π‘†β€˜πΆ))) ∧ π‘ˆ ∈ (𝐼 Γ— 2o)) β†’ ((𝑃 βˆ’ 2)(π‘‡β€˜(π‘†β€˜πΆ))π‘ˆ) ∈ ran (π‘‡β€˜(π‘†β€˜πΆ)))
334218, 225, 117, 333syl3anc 1371 . . 3 (πœ‘ β†’ ((𝑃 βˆ’ 2)(π‘‡β€˜(π‘†β€˜πΆ))π‘ˆ) ∈ ran (π‘‡β€˜(π‘†β€˜πΆ)))
335332, 334eqeltrrd 2834 . 2 (πœ‘ β†’ (π΅β€˜πΏ) ∈ ran (π‘‡β€˜(π‘†β€˜πΆ)))
336221, 335jca 512 1 (πœ‘ β†’ ((π΄β€˜πΎ) ∈ ran (π‘‡β€˜(π‘†β€˜πΆ)) ∧ (π΅β€˜πΏ) ∈ ran (π‘‡β€˜(π‘†β€˜πΆ))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061  {crab 3432   βˆ– cdif 3945  βˆ…c0 4322  {csn 4628  βŸ¨cop 4634  βŸ¨cotp 4636  βˆͺ ciun 4997   class class class wbr 5148   ↦ cmpt 5231   I cid 5573   Γ— cxp 5674  dom cdm 5676  ran crn 5677   Fn wfn 6538  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7411   ∈ cmpo 7413  1oc1o 8461  2oc2o 8462  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   < clt 11250   ≀ cle 11251   βˆ’ cmin 11446  2c2 12269  β„•0cn0 12474  β„€cz 12560  β„€β‰₯cuz 12824  ...cfz 13486  ..^cfzo 13629  β™―chash 14292  Word cword 14466   ++ cconcat 14522   substr csubstr 14592   prefix cpfx 14622   splice csplice 14701  βŸ¨β€œcs2 14794   ~FG cefg 19576
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-ot 4637  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-card 9936  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-nn 12215  df-2 12277  df-n0 12475  df-z 12561  df-uz 12825  df-fz 13487  df-fzo 13630  df-hash 14293  df-word 14467  df-concat 14523  df-s1 14548  df-substr 14593  df-pfx 14623  df-splice 14702  df-s2 14801
This theorem is referenced by:  efgredlemd  19614
  Copyright terms: Public domain W3C validator