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

Theorem efgredlemc 19665
Description: The reduced word that forms the base of the sequence in efgsval 19651 is uniquely determined, given the ending representation. (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 (πœ‘ β†’ Β¬ (π΄β€˜πΎ) = (π΅β€˜πΏ))
Assertion
Ref Expression
efgredlemc (πœ‘ β†’ (𝑃 ∈ (β„€β‰₯β€˜π‘„) β†’ (π΄β€˜0) = (π΅β€˜0)))
Distinct variable groups:   π‘Ž,𝑏,𝐴   𝑦,π‘Ž,𝑧,𝑏   𝐿,π‘Ž,𝑏   𝐾,π‘Ž,𝑏   𝑑,𝑛,𝑣,𝑀,𝑦,𝑧,𝑃   π‘š,π‘Ž,𝑛,𝑑,𝑣,𝑀,π‘₯,𝑀,𝑏   π‘ˆ,𝑛,𝑣,𝑀,𝑦,𝑧   π‘˜,π‘Ž,𝑇,𝑏,π‘š,𝑑,π‘₯   𝑛,𝑉,𝑣,𝑀,𝑦,𝑧   𝑄,𝑛,𝑑,𝑣,𝑀,𝑦,𝑧   π‘Š,π‘Ž,𝑏   π‘˜,𝑛,𝑣,𝑀,𝑦,𝑧,π‘Š,π‘š,𝑑,π‘₯   ∼ ,π‘Ž,𝑏,π‘š,𝑑,π‘₯,𝑦,𝑧   𝐡,π‘Ž,𝑏   𝑆,π‘Ž,𝑏   𝐼,π‘Ž,𝑏,π‘š,𝑛,𝑑,𝑣,𝑀,π‘₯,𝑦,𝑧   𝐷,π‘Ž,𝑏,π‘š,𝑑
Allowed substitution hints:   πœ‘(π‘₯,𝑦,𝑧,𝑀,𝑣,𝑑,π‘˜,π‘š,𝑛,π‘Ž,𝑏)   𝐴(π‘₯,𝑦,𝑧,𝑀,𝑣,𝑑,π‘˜,π‘š,𝑛)   𝐡(π‘₯,𝑦,𝑧,𝑀,𝑣,𝑑,π‘˜,π‘š,𝑛)   𝐷(π‘₯,𝑦,𝑧,𝑀,𝑣,π‘˜,𝑛)   𝑃(π‘₯,π‘˜,π‘š,π‘Ž,𝑏)   𝑄(π‘₯,π‘˜,π‘š,π‘Ž,𝑏)   ∼ (𝑀,𝑣,π‘˜,𝑛)   𝑆(π‘₯,𝑦,𝑧,𝑀,𝑣,𝑑,π‘˜,π‘š,𝑛)   𝑇(𝑦,𝑧,𝑀,𝑣,𝑛)   π‘ˆ(π‘₯,𝑑,π‘˜,π‘š,π‘Ž,𝑏)   𝐼(π‘˜)   𝐾(π‘₯,𝑦,𝑧,𝑀,𝑣,𝑑,π‘˜,π‘š,𝑛)   𝐿(π‘₯,𝑦,𝑧,𝑀,𝑣,𝑑,π‘˜,π‘š,𝑛)   𝑀(𝑦,𝑧,π‘˜)   𝑉(π‘₯,𝑑,π‘˜,π‘š,π‘Ž,𝑏)

Proof of Theorem efgredlemc
Dummy variables 𝑐 𝑖 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uzp1 12867 . 2 (𝑃 ∈ (β„€β‰₯β€˜π‘„) β†’ (𝑃 = 𝑄 ∨ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 1))))
2 efgredlemb.8 . . . . . 6 (πœ‘ β†’ Β¬ (π΄β€˜πΎ) = (π΅β€˜πΏ))
3 efgval.w . . . . . . . . . . 11 π‘Š = ( I β€˜Word (𝐼 Γ— 2o))
4 fviss 6962 . . . . . . . . . . 11 ( I β€˜Word (𝐼 Γ— 2o)) βŠ† Word (𝐼 Γ— 2o)
53, 4eqsstri 4011 . . . . . . . . . 10 π‘Š βŠ† Word (𝐼 Γ— 2o)
6 efgredlem.2 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐴 ∈ dom 𝑆)
7 efgval.r . . . . . . . . . . . . . . . 16 ∼ = ( ~FG β€˜πΌ)
8 efgval2.m . . . . . . . . . . . . . . . 16 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)
9 efgval2.t . . . . . . . . . . . . . . . 16 𝑇 = (𝑣 ∈ π‘Š ↦ (𝑛 ∈ (0...(β™―β€˜π‘£)), 𝑀 ∈ (𝐼 Γ— 2o) ↦ (𝑣 splice βŸ¨π‘›, 𝑛, βŸ¨β€œπ‘€(π‘€β€˜π‘€)β€βŸ©βŸ©)))
10 efgred.d . . . . . . . . . . . . . . . 16 𝐷 = (π‘Š βˆ– βˆͺ π‘₯ ∈ π‘Š ran (π‘‡β€˜π‘₯))
11 efgred.s . . . . . . . . . . . . . . . 16 𝑆 = (π‘š ∈ {𝑑 ∈ (Word π‘Š βˆ– {βˆ…}) ∣ ((π‘‘β€˜0) ∈ 𝐷 ∧ βˆ€π‘˜ ∈ (1..^(β™―β€˜π‘‘))(π‘‘β€˜π‘˜) ∈ ran (π‘‡β€˜(π‘‘β€˜(π‘˜ βˆ’ 1))))} ↦ (π‘šβ€˜((β™―β€˜π‘š) βˆ’ 1)))
123, 7, 8, 9, 10, 11efgsdm 19650 . . . . . . . . . . . . . . 15 (𝐴 ∈ dom 𝑆 ↔ (𝐴 ∈ (Word π‘Š βˆ– {βˆ…}) ∧ (π΄β€˜0) ∈ 𝐷 ∧ βˆ€π‘– ∈ (1..^(β™―β€˜π΄))(π΄β€˜π‘–) ∈ ran (π‘‡β€˜(π΄β€˜(𝑖 βˆ’ 1)))))
1312simp1bi 1142 . . . . . . . . . . . . . 14 (𝐴 ∈ dom 𝑆 β†’ 𝐴 ∈ (Word π‘Š βˆ– {βˆ…}))
146, 13syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐴 ∈ (Word π‘Š βˆ– {βˆ…}))
1514eldifad 3955 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 ∈ Word π‘Š)
16 wrdf 14475 . . . . . . . . . . . 12 (𝐴 ∈ Word π‘Š β†’ 𝐴:(0..^(β™―β€˜π΄))βŸΆπ‘Š)
1715, 16syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴:(0..^(β™―β€˜π΄))βŸΆπ‘Š)
18 fzossfz 13657 . . . . . . . . . . . . 13 (0..^((β™―β€˜π΄) βˆ’ 1)) βŠ† (0...((β™―β€˜π΄) βˆ’ 1))
19 efgredlemb.k . . . . . . . . . . . . . 14 𝐾 = (((β™―β€˜π΄) βˆ’ 1) βˆ’ 1)
20 efgredlem.1 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ βˆ€π‘Ž ∈ dom π‘†βˆ€π‘ ∈ dom 𝑆((β™―β€˜(π‘†β€˜π‘Ž)) < (β™―β€˜(π‘†β€˜π΄)) β†’ ((π‘†β€˜π‘Ž) = (π‘†β€˜π‘) β†’ (π‘Žβ€˜0) = (π‘β€˜0))))
21 efgredlem.3 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐡 ∈ dom 𝑆)
22 efgredlem.4 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (π‘†β€˜π΄) = (π‘†β€˜π΅))
23 efgredlem.5 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ Β¬ (π΄β€˜0) = (π΅β€˜0))
243, 7, 8, 9, 10, 11, 20, 6, 21, 22, 23efgredlema 19660 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (((β™―β€˜π΄) βˆ’ 1) ∈ β„• ∧ ((β™―β€˜π΅) βˆ’ 1) ∈ β„•))
2524simpld 494 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((β™―β€˜π΄) βˆ’ 1) ∈ β„•)
26 fzo0end 13730 . . . . . . . . . . . . . . 15 (((β™―β€˜π΄) βˆ’ 1) ∈ β„• β†’ (((β™―β€˜π΄) βˆ’ 1) βˆ’ 1) ∈ (0..^((β™―β€˜π΄) βˆ’ 1)))
2725, 26syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (((β™―β€˜π΄) βˆ’ 1) βˆ’ 1) ∈ (0..^((β™―β€˜π΄) βˆ’ 1)))
2819, 27eqeltrid 2831 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐾 ∈ (0..^((β™―β€˜π΄) βˆ’ 1)))
2918, 28sselid 3975 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐾 ∈ (0...((β™―β€˜π΄) βˆ’ 1)))
30 lencl 14489 . . . . . . . . . . . . . . 15 (𝐴 ∈ Word π‘Š β†’ (β™―β€˜π΄) ∈ β„•0)
3115, 30syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (β™―β€˜π΄) ∈ β„•0)
3231nn0zd 12588 . . . . . . . . . . . . 13 (πœ‘ β†’ (β™―β€˜π΄) ∈ β„€)
33 fzoval 13639 . . . . . . . . . . . . 13 ((β™―β€˜π΄) ∈ β„€ β†’ (0..^(β™―β€˜π΄)) = (0...((β™―β€˜π΄) βˆ’ 1)))
3432, 33syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (0..^(β™―β€˜π΄)) = (0...((β™―β€˜π΄) βˆ’ 1)))
3529, 34eleqtrrd 2830 . . . . . . . . . . 11 (πœ‘ β†’ 𝐾 ∈ (0..^(β™―β€˜π΄)))
3617, 35ffvelcdmd 7081 . . . . . . . . . 10 (πœ‘ β†’ (π΄β€˜πΎ) ∈ π‘Š)
375, 36sselid 3975 . . . . . . . . 9 (πœ‘ β†’ (π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o))
38 efgredlemb.p . . . . . . . . 9 (πœ‘ β†’ 𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))))
39 lencl 14489 . . . . . . . . . . . 12 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ β„•0)
4037, 39syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ β„•0)
41 nn0uz 12868 . . . . . . . . . . 11 β„•0 = (β„€β‰₯β€˜0)
4240, 41eleqtrdi 2837 . . . . . . . . . 10 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜0))
43 eluzfz2 13515 . . . . . . . . . 10 ((β™―β€˜(π΄β€˜πΎ)) ∈ (β„€β‰₯β€˜0) β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (0...(β™―β€˜(π΄β€˜πΎ))))
4442, 43syl 17 . . . . . . . . 9 (πœ‘ β†’ (β™―β€˜(π΄β€˜πΎ)) ∈ (0...(β™―β€˜(π΄β€˜πΎ))))
45 ccatpfx 14657 . . . . . . . . 9 (((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) ∧ 𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))) ∧ (β™―β€˜(π΄β€˜πΎ)) ∈ (0...(β™―β€˜(π΄β€˜πΎ)))) β†’ (((π΄β€˜πΎ) prefix 𝑃) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((π΄β€˜πΎ) prefix (β™―β€˜(π΄β€˜πΎ))))
4637, 38, 44, 45syl3anc 1368 . . . . . . . 8 (πœ‘ β†’ (((π΄β€˜πΎ) prefix 𝑃) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((π΄β€˜πΎ) prefix (β™―β€˜(π΄β€˜πΎ))))
47 pfxid 14640 . . . . . . . . 9 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) prefix (β™―β€˜(π΄β€˜πΎ))) = (π΄β€˜πΎ))
4837, 47syl 17 . . . . . . . 8 (πœ‘ β†’ ((π΄β€˜πΎ) prefix (β™―β€˜(π΄β€˜πΎ))) = (π΄β€˜πΎ))
4946, 48eqtrd 2766 . . . . . . 7 (πœ‘ β†’ (((π΄β€˜πΎ) prefix 𝑃) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = (π΄β€˜πΎ))
503, 7, 8, 9, 10, 11efgsdm 19650 . . . . . . . . . . . . . . 15 (𝐡 ∈ dom 𝑆 ↔ (𝐡 ∈ (Word π‘Š βˆ– {βˆ…}) ∧ (π΅β€˜0) ∈ 𝐷 ∧ βˆ€π‘– ∈ (1..^(β™―β€˜π΅))(π΅β€˜π‘–) ∈ ran (π‘‡β€˜(π΅β€˜(𝑖 βˆ’ 1)))))
5150simp1bi 1142 . . . . . . . . . . . . . 14 (𝐡 ∈ dom 𝑆 β†’ 𝐡 ∈ (Word π‘Š βˆ– {βˆ…}))
5221, 51syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐡 ∈ (Word π‘Š βˆ– {βˆ…}))
5352eldifad 3955 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 ∈ Word π‘Š)
54 wrdf 14475 . . . . . . . . . . . 12 (𝐡 ∈ Word π‘Š β†’ 𝐡:(0..^(β™―β€˜π΅))βŸΆπ‘Š)
5553, 54syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝐡:(0..^(β™―β€˜π΅))βŸΆπ‘Š)
56 fzossfz 13657 . . . . . . . . . . . . 13 (0..^((β™―β€˜π΅) βˆ’ 1)) βŠ† (0...((β™―β€˜π΅) βˆ’ 1))
57 efgredlemb.l . . . . . . . . . . . . . 14 𝐿 = (((β™―β€˜π΅) βˆ’ 1) βˆ’ 1)
5824simprd 495 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((β™―β€˜π΅) βˆ’ 1) ∈ β„•)
59 fzo0end 13730 . . . . . . . . . . . . . . 15 (((β™―β€˜π΅) βˆ’ 1) ∈ β„• β†’ (((β™―β€˜π΅) βˆ’ 1) βˆ’ 1) ∈ (0..^((β™―β€˜π΅) βˆ’ 1)))
6058, 59syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (((β™―β€˜π΅) βˆ’ 1) βˆ’ 1) ∈ (0..^((β™―β€˜π΅) βˆ’ 1)))
6157, 60eqeltrid 2831 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐿 ∈ (0..^((β™―β€˜π΅) βˆ’ 1)))
6256, 61sselid 3975 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐿 ∈ (0...((β™―β€˜π΅) βˆ’ 1)))
63 lencl 14489 . . . . . . . . . . . . . . 15 (𝐡 ∈ Word π‘Š β†’ (β™―β€˜π΅) ∈ β„•0)
6453, 63syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (β™―β€˜π΅) ∈ β„•0)
6564nn0zd 12588 . . . . . . . . . . . . 13 (πœ‘ β†’ (β™―β€˜π΅) ∈ β„€)
66 fzoval 13639 . . . . . . . . . . . . 13 ((β™―β€˜π΅) ∈ β„€ β†’ (0..^(β™―β€˜π΅)) = (0...((β™―β€˜π΅) βˆ’ 1)))
6765, 66syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (0..^(β™―β€˜π΅)) = (0...((β™―β€˜π΅) βˆ’ 1)))
6862, 67eleqtrrd 2830 . . . . . . . . . . 11 (πœ‘ β†’ 𝐿 ∈ (0..^(β™―β€˜π΅)))
6955, 68ffvelcdmd 7081 . . . . . . . . . 10 (πœ‘ β†’ (π΅β€˜πΏ) ∈ π‘Š)
705, 69sselid 3975 . . . . . . . . 9 (πœ‘ β†’ (π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o))
71 efgredlemb.q . . . . . . . . 9 (πœ‘ β†’ 𝑄 ∈ (0...(β™―β€˜(π΅β€˜πΏ))))
72 lencl 14489 . . . . . . . . . . . 12 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ β„•0)
7370, 72syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ β„•0)
7473, 41eleqtrdi 2837 . . . . . . . . . 10 (πœ‘ β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ (β„€β‰₯β€˜0))
75 eluzfz2 13515 . . . . . . . . . 10 ((β™―β€˜(π΅β€˜πΏ)) ∈ (β„€β‰₯β€˜0) β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ (0...(β™―β€˜(π΅β€˜πΏ))))
7674, 75syl 17 . . . . . . . . 9 (πœ‘ β†’ (β™―β€˜(π΅β€˜πΏ)) ∈ (0...(β™―β€˜(π΅β€˜πΏ))))
77 ccatpfx 14657 . . . . . . . . 9 (((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) ∧ 𝑄 ∈ (0...(β™―β€˜(π΅β€˜πΏ))) ∧ (β™―β€˜(π΅β€˜πΏ)) ∈ (0...(β™―β€˜(π΅β€˜πΏ)))) β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)) = ((π΅β€˜πΏ) prefix (β™―β€˜(π΅β€˜πΏ))))
7870, 71, 76, 77syl3anc 1368 . . . . . . . 8 (πœ‘ β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)) = ((π΅β€˜πΏ) prefix (β™―β€˜(π΅β€˜πΏ))))
79 pfxid 14640 . . . . . . . . 9 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΅β€˜πΏ) prefix (β™―β€˜(π΅β€˜πΏ))) = (π΅β€˜πΏ))
8070, 79syl 17 . . . . . . . 8 (πœ‘ β†’ ((π΅β€˜πΏ) prefix (β™―β€˜(π΅β€˜πΏ))) = (π΅β€˜πΏ))
8178, 80eqtrd 2766 . . . . . . 7 (πœ‘ β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)) = (π΅β€˜πΏ))
8249, 81eqeq12d 2742 . . . . . 6 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑃) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)) ↔ (π΄β€˜πΎ) = (π΅β€˜πΏ)))
832, 82mtbird 325 . . . . 5 (πœ‘ β†’ Β¬ (((π΄β€˜πΎ) prefix 𝑃) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
84 efgredlemb.6 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘†β€˜π΄) = (𝑃(π‘‡β€˜(π΄β€˜πΎ))π‘ˆ))
85 efgredlemb.u . . . . . . . . . . . . . 14 (πœ‘ β†’ π‘ˆ ∈ (𝐼 Γ— 2o))
863, 7, 8, 9efgtval 19643 . . . . . . . . . . . . . 14 (((π΄β€˜πΎ) ∈ π‘Š ∧ 𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))) ∧ π‘ˆ ∈ (𝐼 Γ— 2o)) β†’ (𝑃(π‘‡β€˜(π΄β€˜πΎ))π‘ˆ) = ((π΄β€˜πΎ) splice βŸ¨π‘ƒ, 𝑃, βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©βŸ©))
8736, 38, 85, 86syl3anc 1368 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑃(π‘‡β€˜(π΄β€˜πΎ))π‘ˆ) = ((π΄β€˜πΎ) splice βŸ¨π‘ƒ, 𝑃, βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©βŸ©))
888efgmf 19633 . . . . . . . . . . . . . . . . 17 𝑀:(𝐼 Γ— 2o)⟢(𝐼 Γ— 2o)
8988ffvelcdmi 7079 . . . . . . . . . . . . . . . 16 (π‘ˆ ∈ (𝐼 Γ— 2o) β†’ (π‘€β€˜π‘ˆ) ∈ (𝐼 Γ— 2o))
9085, 89syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘€β€˜π‘ˆ) ∈ (𝐼 Γ— 2o))
9185, 90s2cld 14828 . . . . . . . . . . . . . 14 (πœ‘ β†’ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ∈ Word (𝐼 Γ— 2o))
92 splval 14707 . . . . . . . . . . . . . 14 (((π΄β€˜πΎ) ∈ π‘Š ∧ (𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))) ∧ 𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))) ∧ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ∈ Word (𝐼 Γ— 2o))) β†’ ((π΄β€˜πΎ) splice βŸ¨π‘ƒ, 𝑃, βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©βŸ©) = ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))
9336, 38, 38, 91, 92syl13anc 1369 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π΄β€˜πΎ) splice βŸ¨π‘ƒ, 𝑃, βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©βŸ©) = ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))
9484, 87, 933eqtrd 2770 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘†β€˜π΄) = ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))
95 efgredlemb.7 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘†β€˜π΅) = (𝑄(π‘‡β€˜(π΅β€˜πΏ))𝑉))
96 efgredlemb.v . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑉 ∈ (𝐼 Γ— 2o))
973, 7, 8, 9efgtval 19643 . . . . . . . . . . . . . 14 (((π΅β€˜πΏ) ∈ π‘Š ∧ 𝑄 ∈ (0...(β™―β€˜(π΅β€˜πΏ))) ∧ 𝑉 ∈ (𝐼 Γ— 2o)) β†’ (𝑄(π‘‡β€˜(π΅β€˜πΏ))𝑉) = ((π΅β€˜πΏ) splice βŸ¨π‘„, 𝑄, βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©βŸ©))
9869, 71, 96, 97syl3anc 1368 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑄(π‘‡β€˜(π΅β€˜πΏ))𝑉) = ((π΅β€˜πΏ) splice βŸ¨π‘„, 𝑄, βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©βŸ©))
9988ffvelcdmi 7079 . . . . . . . . . . . . . . . 16 (𝑉 ∈ (𝐼 Γ— 2o) β†’ (π‘€β€˜π‘‰) ∈ (𝐼 Γ— 2o))
10096, 99syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘€β€˜π‘‰) ∈ (𝐼 Γ— 2o))
10196, 100s2cld 14828 . . . . . . . . . . . . . 14 (πœ‘ β†’ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ∈ Word (𝐼 Γ— 2o))
102 splval 14707 . . . . . . . . . . . . . 14 (((π΅β€˜πΏ) ∈ π‘Š ∧ (𝑄 ∈ (0...(β™―β€˜(π΅β€˜πΏ))) ∧ 𝑄 ∈ (0...(β™―β€˜(π΅β€˜πΏ))) ∧ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ∈ Word (𝐼 Γ— 2o))) β†’ ((π΅β€˜πΏ) splice βŸ¨π‘„, 𝑄, βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©βŸ©) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
10369, 71, 71, 101, 102syl13anc 1369 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π΅β€˜πΏ) splice βŸ¨π‘„, 𝑄, βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©βŸ©) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
10495, 98, 1033eqtrd 2770 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘†β€˜π΅) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
10522, 94, 1043eqtr3d 2774 . . . . . . . . . . 11 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
106105adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
107 pfxcl 14633 . . . . . . . . . . . . . 14 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) prefix 𝑃) ∈ Word (𝐼 Γ— 2o))
10837, 107syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π΄β€˜πΎ) prefix 𝑃) ∈ Word (𝐼 Γ— 2o))
109108adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ ((π΄β€˜πΎ) prefix 𝑃) ∈ Word (𝐼 Γ— 2o))
11091adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ∈ Word (𝐼 Γ— 2o))
111 ccatcl 14530 . . . . . . . . . . . 12 ((((π΄β€˜πΎ) prefix 𝑃) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ∈ Word (𝐼 Γ— 2o)) β†’ (((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ∈ Word (𝐼 Γ— 2o))
112109, 110, 111syl2anc 583 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ (((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ∈ Word (𝐼 Γ— 2o))
113 swrdcl 14601 . . . . . . . . . . . . 13 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o))
11437, 113syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o))
115114adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o))
116 pfxcl 14633 . . . . . . . . . . . . . 14 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΅β€˜πΏ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o))
11770, 116syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π΅β€˜πΏ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o))
118117adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ ((π΅β€˜πΏ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o))
119101adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ∈ Word (𝐼 Γ— 2o))
120 ccatcl 14530 . . . . . . . . . . . 12 ((((π΅β€˜πΏ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ∈ Word (𝐼 Γ— 2o)) β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ∈ Word (𝐼 Γ— 2o))
121118, 119, 120syl2anc 583 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ∈ Word (𝐼 Γ— 2o))
122 swrdcl 14601 . . . . . . . . . . . . 13 ((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o))
12370, 122syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o))
124123adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o))
125 pfxlen 14639 . . . . . . . . . . . . . . . 16 (((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) ∧ 𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ)))) β†’ (β™―β€˜((π΄β€˜πΎ) prefix 𝑃)) = 𝑃)
12637, 38, 125syl2anc 583 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (β™―β€˜((π΄β€˜πΎ) prefix 𝑃)) = 𝑃)
127 pfxlen 14639 . . . . . . . . . . . . . . . 16 (((π΅β€˜πΏ) ∈ Word (𝐼 Γ— 2o) ∧ 𝑄 ∈ (0...(β™―β€˜(π΅β€˜πΏ)))) β†’ (β™―β€˜((π΅β€˜πΏ) prefix 𝑄)) = 𝑄)
12870, 71, 127syl2anc 583 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (β™―β€˜((π΅β€˜πΏ) prefix 𝑄)) = 𝑄)
129126, 128eqeq12d 2742 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((β™―β€˜((π΄β€˜πΎ) prefix 𝑃)) = (β™―β€˜((π΅β€˜πΏ) prefix 𝑄)) ↔ 𝑃 = 𝑄))
130129biimpar 477 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ (β™―β€˜((π΄β€˜πΎ) prefix 𝑃)) = (β™―β€˜((π΅β€˜πΏ) prefix 𝑄)))
131 s2len 14846 . . . . . . . . . . . . . . 15 (β™―β€˜βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) = 2
132 s2len 14846 . . . . . . . . . . . . . . 15 (β™―β€˜βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) = 2
133131, 132eqtr4i 2757 . . . . . . . . . . . . . 14 (β™―β€˜βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) = (β™―β€˜βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©)
134133a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ (β™―β€˜βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) = (β™―β€˜βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©))
135130, 134oveq12d 7423 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ ((β™―β€˜((π΄β€˜πΎ) prefix 𝑃)) + (β™―β€˜βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©)) = ((β™―β€˜((π΅β€˜πΏ) prefix 𝑄)) + (β™―β€˜βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©)))
136 ccatlen 14531 . . . . . . . . . . . . 13 ((((π΄β€˜πΎ) prefix 𝑃) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ∈ Word (𝐼 Γ— 2o)) β†’ (β™―β€˜(((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©)) = ((β™―β€˜((π΄β€˜πΎ) prefix 𝑃)) + (β™―β€˜βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©)))
137109, 110, 136syl2anc 583 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ (β™―β€˜(((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©)) = ((β™―β€˜((π΄β€˜πΎ) prefix 𝑃)) + (β™―β€˜βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©)))
138 ccatlen 14531 . . . . . . . . . . . . 13 ((((π΅β€˜πΏ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ∈ Word (𝐼 Γ— 2o)) β†’ (β™―β€˜(((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©)) = ((β™―β€˜((π΅β€˜πΏ) prefix 𝑄)) + (β™―β€˜βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©)))
139118, 119, 138syl2anc 583 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ (β™―β€˜(((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©)) = ((β™―β€˜((π΅β€˜πΏ) prefix 𝑄)) + (β™―β€˜βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©)))
140135, 137, 1393eqtr4d 2776 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ (β™―β€˜(((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©)) = (β™―β€˜(((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©)))
141 ccatopth 14672 . . . . . . . . . . 11 ((((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ∈ Word (𝐼 Γ— 2o) ∧ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o)) ∧ ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ∈ Word (𝐼 Γ— 2o) ∧ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o)) ∧ (β™―β€˜(((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©)) = (β™―β€˜(((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©))) β†’ (((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)) ↔ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) = (((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ∧ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) = ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩))))
142112, 115, 121, 124, 140, 141syl221anc 1378 . . . . . . . . . 10 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ (((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)) ↔ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) = (((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ∧ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) = ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩))))
143106, 142mpbid 231 . . . . . . . . 9 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) = (((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ∧ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) = ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
144143simpld 494 . . . . . . . 8 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ (((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) = (((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©))
145 ccatopth 14672 . . . . . . . . 9 (((((π΄β€˜πΎ) prefix 𝑃) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© ∈ Word (𝐼 Γ— 2o)) ∧ (((π΅β€˜πΏ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© ∈ Word (𝐼 Γ— 2o)) ∧ (β™―β€˜((π΄β€˜πΎ) prefix 𝑃)) = (β™―β€˜((π΅β€˜πΏ) prefix 𝑄))) β†’ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) = (((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ↔ (((π΄β€˜πΎ) prefix 𝑃) = ((π΅β€˜πΏ) prefix 𝑄) ∧ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© = βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©)))
146109, 110, 118, 119, 130, 145syl221anc 1378 . . . . . . . 8 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) = (((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ↔ (((π΄β€˜πΎ) prefix 𝑃) = ((π΅β€˜πΏ) prefix 𝑄) ∧ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© = βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©)))
147144, 146mpbid 231 . . . . . . 7 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ (((π΄β€˜πΎ) prefix 𝑃) = ((π΅β€˜πΏ) prefix 𝑄) ∧ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© = βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©))
148147simpld 494 . . . . . 6 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ ((π΄β€˜πΎ) prefix 𝑃) = ((π΅β€˜πΏ) prefix 𝑄))
149143simprd 495 . . . . . 6 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) = ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩))
150148, 149oveq12d 7423 . . . . 5 ((πœ‘ ∧ 𝑃 = 𝑄) β†’ (((π΄β€˜πΎ) prefix 𝑃) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
15183, 150mtand 813 . . . 4 (πœ‘ β†’ Β¬ 𝑃 = 𝑄)
152151pm2.21d 121 . . 3 (πœ‘ β†’ (𝑃 = 𝑄 β†’ (π΄β€˜0) = (π΅β€˜0)))
153 uzp1 12867 . . . 4 (𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 1)) β†’ (𝑃 = (𝑄 + 1) ∨ 𝑃 ∈ (β„€β‰₯β€˜((𝑄 + 1) + 1))))
15485s1cld 14559 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ βŸ¨β€œπ‘ˆβ€βŸ© ∈ Word (𝐼 Γ— 2o))
155 ccatcl 14530 . . . . . . . . . . . . . . . . 17 ((((π΄β€˜πΎ) prefix 𝑃) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œπ‘ˆβ€βŸ© ∈ Word (𝐼 Γ— 2o)) β†’ (((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) ∈ Word (𝐼 Γ— 2o))
156108, 154, 155syl2anc 583 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) ∈ Word (𝐼 Γ— 2o))
15790s1cld 14559 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© ∈ Word (𝐼 Γ— 2o))
158 ccatass 14544 . . . . . . . . . . . . . . . 16 (((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© ∈ Word (𝐼 Γ— 2o) ∧ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o)) β†’ (((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) ++ (βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))))
159156, 157, 114, 158syl3anc 1368 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) ++ (βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))))
160 ccatass 14544 . . . . . . . . . . . . . . . . . . 19 ((((π΄β€˜πΎ) prefix 𝑃) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œπ‘ˆβ€βŸ© ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© ∈ Word (𝐼 Γ— 2o)) β†’ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ©) = (((π΄β€˜πΎ) prefix 𝑃) ++ (βŸ¨β€œπ‘ˆβ€βŸ© ++ βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ©)))
161108, 154, 157, 160syl3anc 1368 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ©) = (((π΄β€˜πΎ) prefix 𝑃) ++ (βŸ¨β€œπ‘ˆβ€βŸ© ++ βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ©)))
162 df-s2 14805 . . . . . . . . . . . . . . . . . . 19 βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ© = (βŸ¨β€œπ‘ˆβ€βŸ© ++ βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ©)
163162oveq2i 7416 . . . . . . . . . . . . . . . . . 18 (((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) = (((π΄β€˜πΎ) prefix 𝑃) ++ (βŸ¨β€œπ‘ˆβ€βŸ© ++ βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ©))
164161, 163eqtr4di 2784 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ©) = (((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©))
165164oveq1d 7420 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))
16696s1cld 14559 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ βŸ¨β€œπ‘‰β€βŸ© ∈ Word (𝐼 Γ— 2o))
167100s1cld 14559 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ© ∈ Word (𝐼 Γ— 2o))
168 ccatass 14544 . . . . . . . . . . . . . . . . . . 19 ((((π΅β€˜πΏ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œπ‘‰β€βŸ© ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ© ∈ Word (𝐼 Γ— 2o)) β†’ ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©) = (((π΅β€˜πΏ) prefix 𝑄) ++ (βŸ¨β€œπ‘‰β€βŸ© ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©)))
169117, 166, 167, 168syl3anc 1368 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©) = (((π΅β€˜πΏ) prefix 𝑄) ++ (βŸ¨β€œπ‘‰β€βŸ© ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©)))
170 df-s2 14805 . . . . . . . . . . . . . . . . . . 19 βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ© = (βŸ¨β€œπ‘‰β€βŸ© ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©)
171170oveq2i 7416 . . . . . . . . . . . . . . . . . 18 (((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) = (((π΅β€˜πΏ) prefix 𝑄) ++ (βŸ¨β€œπ‘‰β€βŸ© ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©))
172169, 171eqtr4di 2784 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©) = (((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©))
173172oveq1d 7420 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
174105, 165, 1733eqtr4d 2776 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = (((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
175159, 174eqtr3d 2768 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) ++ (βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = (((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
176175adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) ++ (βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = (((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
177156adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) ∈ Word (𝐼 Γ— 2o))
178157adantr 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© ∈ Word (𝐼 Γ— 2o))
179114adantr 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o))
180 ccatcl 14530 . . . . . . . . . . . . . . 15 ((βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© ∈ Word (𝐼 Γ— 2o) ∧ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o)) β†’ (βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) ∈ Word (𝐼 Γ— 2o))
181178, 179, 180syl2anc 583 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) ∈ Word (𝐼 Γ— 2o))
182 ccatcl 14530 . . . . . . . . . . . . . . . . 17 ((((π΅β€˜πΏ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œπ‘‰β€βŸ© ∈ Word (𝐼 Γ— 2o)) β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ∈ Word (𝐼 Γ— 2o))
183117, 166, 182syl2anc 583 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ∈ Word (𝐼 Γ— 2o))
184183adantr 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ∈ Word (𝐼 Γ— 2o))
185167adantr 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ© ∈ Word (𝐼 Γ— 2o))
186 ccatcl 14530 . . . . . . . . . . . . . . 15 (((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ© ∈ Word (𝐼 Γ— 2o)) β†’ ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©) ∈ Word (𝐼 Γ— 2o))
187184, 185, 186syl2anc 583 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©) ∈ Word (𝐼 Γ— 2o))
188123adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o))
189 ccatlen 14531 . . . . . . . . . . . . . . . . . . . 20 ((((π΅β€˜πΏ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œπ‘‰β€βŸ© ∈ Word (𝐼 Γ— 2o)) β†’ (β™―β€˜(((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©)) = ((β™―β€˜((π΅β€˜πΏ) prefix 𝑄)) + (β™―β€˜βŸ¨β€œπ‘‰β€βŸ©)))
190117, 166, 189syl2anc 583 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (β™―β€˜(((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©)) = ((β™―β€˜((π΅β€˜πΏ) prefix 𝑄)) + (β™―β€˜βŸ¨β€œπ‘‰β€βŸ©)))
191 s1len 14562 . . . . . . . . . . . . . . . . . . . . 21 (β™―β€˜βŸ¨β€œπ‘‰β€βŸ©) = 1
192191a1i 11 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (β™―β€˜βŸ¨β€œπ‘‰β€βŸ©) = 1)
193128, 192oveq12d 7423 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((β™―β€˜((π΅β€˜πΏ) prefix 𝑄)) + (β™―β€˜βŸ¨β€œπ‘‰β€βŸ©)) = (𝑄 + 1))
194190, 193eqtrd 2766 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (β™―β€˜(((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©)) = (𝑄 + 1))
195126, 194eqeq12d 2742 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((β™―β€˜((π΄β€˜πΎ) prefix 𝑃)) = (β™―β€˜(((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©)) ↔ 𝑃 = (𝑄 + 1)))
196195biimpar 477 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (β™―β€˜((π΄β€˜πΎ) prefix 𝑃)) = (β™―β€˜(((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©)))
197 s1len 14562 . . . . . . . . . . . . . . . . . 18 (β™―β€˜βŸ¨β€œπ‘ˆβ€βŸ©) = 1
198 s1len 14562 . . . . . . . . . . . . . . . . . 18 (β™―β€˜βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©) = 1
199197, 198eqtr4i 2757 . . . . . . . . . . . . . . . . 17 (β™―β€˜βŸ¨β€œπ‘ˆβ€βŸ©) = (β™―β€˜βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©)
200199a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (β™―β€˜βŸ¨β€œπ‘ˆβ€βŸ©) = (β™―β€˜βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©))
201196, 200oveq12d 7423 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ ((β™―β€˜((π΄β€˜πΎ) prefix 𝑃)) + (β™―β€˜βŸ¨β€œπ‘ˆβ€βŸ©)) = ((β™―β€˜(((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©)) + (β™―β€˜βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©)))
202108adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ ((π΄β€˜πΎ) prefix 𝑃) ∈ Word (𝐼 Γ— 2o))
203154adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ βŸ¨β€œπ‘ˆβ€βŸ© ∈ Word (𝐼 Γ— 2o))
204 ccatlen 14531 . . . . . . . . . . . . . . . 16 ((((π΄β€˜πΎ) prefix 𝑃) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œπ‘ˆβ€βŸ© ∈ Word (𝐼 Γ— 2o)) β†’ (β™―β€˜(((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©)) = ((β™―β€˜((π΄β€˜πΎ) prefix 𝑃)) + (β™―β€˜βŸ¨β€œπ‘ˆβ€βŸ©)))
205202, 203, 204syl2anc 583 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (β™―β€˜(((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©)) = ((β™―β€˜((π΄β€˜πΎ) prefix 𝑃)) + (β™―β€˜βŸ¨β€œπ‘ˆβ€βŸ©)))
206 ccatlen 14531 . . . . . . . . . . . . . . . 16 (((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ© ∈ Word (𝐼 Γ— 2o)) β†’ (β™―β€˜((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©)) = ((β™―β€˜(((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©)) + (β™―β€˜βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©)))
207184, 185, 206syl2anc 583 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (β™―β€˜((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©)) = ((β™―β€˜(((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©)) + (β™―β€˜βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©)))
208201, 205, 2073eqtr4d 2776 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (β™―β€˜(((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©)) = (β™―β€˜((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©)))
209 ccatopth 14672 . . . . . . . . . . . . . 14 ((((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) ∈ Word (𝐼 Γ— 2o) ∧ (βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) ∈ Word (𝐼 Γ— 2o)) ∧ (((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©) ∈ Word (𝐼 Γ— 2o) ∧ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩) ∈ Word (𝐼 Γ— 2o)) ∧ (β™―β€˜(((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©)) = (β™―β€˜((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©))) β†’ (((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) ++ (βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = (((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)) ↔ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©) ∧ (βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩))))
210177, 181, 187, 188, 208, 209syl221anc 1378 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) ++ (βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = (((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)) ↔ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©) ∧ (βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩))))
211176, 210mpbid 231 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©) ∧ (βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
212211simpld 494 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©))
213 ccatopth 14672 . . . . . . . . . . . 12 (((((π΄β€˜πΎ) prefix 𝑃) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œπ‘ˆβ€βŸ© ∈ Word (𝐼 Γ— 2o)) ∧ ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ© ∈ Word (𝐼 Γ— 2o)) ∧ (β™―β€˜((π΄β€˜πΎ) prefix 𝑃)) = (β™―β€˜(((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©))) β†’ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©) ↔ (((π΄β€˜πΎ) prefix 𝑃) = (((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ∧ βŸ¨β€œπ‘ˆβ€βŸ© = βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©)))
214202, 203, 184, 185, 196, 213syl221anc 1378 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ ((((π΄β€˜πΎ) prefix 𝑃) ++ βŸ¨β€œπ‘ˆβ€βŸ©) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©) ↔ (((π΄β€˜πΎ) prefix 𝑃) = (((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ∧ βŸ¨β€œπ‘ˆβ€βŸ© = βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©)))
215212, 214mpbid 231 . . . . . . . . . 10 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (((π΄β€˜πΎ) prefix 𝑃) = (((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ∧ βŸ¨β€œπ‘ˆβ€βŸ© = βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©))
216215simpld 494 . . . . . . . . 9 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ ((π΄β€˜πΎ) prefix 𝑃) = (((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©))
217216oveq1d 7420 . . . . . . . 8 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (((π΄β€˜πΎ) prefix 𝑃) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))
218117adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ ((π΅β€˜πΏ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o))
219166adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ βŸ¨β€œπ‘‰β€βŸ© ∈ Word (𝐼 Γ— 2o))
220 ccatass 14544 . . . . . . . . 9 ((((π΅β€˜πΏ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o) ∧ βŸ¨β€œπ‘‰β€βŸ© ∈ Word (𝐼 Γ— 2o) ∧ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o)) β†’ ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΅β€˜πΏ) prefix 𝑄) ++ (βŸ¨β€œπ‘‰β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))))
221218, 219, 179, 220syl3anc 1368 . . . . . . . 8 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ ((((π΅β€˜πΏ) prefix 𝑄) ++ βŸ¨β€œπ‘‰β€βŸ©) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΅β€˜πΏ) prefix 𝑄) ++ (βŸ¨β€œπ‘‰β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))))
222215simprd 495 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ βŸ¨β€œπ‘ˆβ€βŸ© = βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ©)
223 s111 14571 . . . . . . . . . . . . . . . . 17 ((π‘ˆ ∈ (𝐼 Γ— 2o) ∧ (π‘€β€˜π‘‰) ∈ (𝐼 Γ— 2o)) β†’ (βŸ¨β€œπ‘ˆβ€βŸ© = βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ© ↔ π‘ˆ = (π‘€β€˜π‘‰)))
22485, 100, 223syl2anc 583 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (βŸ¨β€œπ‘ˆβ€βŸ© = βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ© ↔ π‘ˆ = (π‘€β€˜π‘‰)))
225224adantr 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (βŸ¨β€œπ‘ˆβ€βŸ© = βŸ¨β€œ(π‘€β€˜π‘‰)β€βŸ© ↔ π‘ˆ = (π‘€β€˜π‘‰)))
226222, 225mpbid 231 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ π‘ˆ = (π‘€β€˜π‘‰))
227226fveq2d 6889 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (π‘€β€˜π‘ˆ) = (π‘€β€˜(π‘€β€˜π‘‰)))
2288efgmnvl 19634 . . . . . . . . . . . . . . 15 (𝑉 ∈ (𝐼 Γ— 2o) β†’ (π‘€β€˜(π‘€β€˜π‘‰)) = 𝑉)
22996, 228syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘€β€˜(π‘€β€˜π‘‰)) = 𝑉)
230229adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (π‘€β€˜(π‘€β€˜π‘‰)) = 𝑉)
231227, 230eqtrd 2766 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (π‘€β€˜π‘ˆ) = 𝑉)
232231s1eqd 14557 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© = βŸ¨β€œπ‘‰β€βŸ©)
233232oveq1d 7420 . . . . . . . . . 10 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = (βŸ¨β€œπ‘‰β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)))
234211simprd 495 . . . . . . . . . 10 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (βŸ¨β€œ(π‘€β€˜π‘ˆ)β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩))
235233, 234eqtr3d 2768 . . . . . . . . 9 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (βŸ¨β€œπ‘‰β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩))
236235oveq2d 7421 . . . . . . . 8 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ (βŸ¨β€œπ‘‰β€βŸ© ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩))) = (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
237217, 221, 2363eqtrd 2770 . . . . . . 7 ((πœ‘ ∧ 𝑃 = (𝑄 + 1)) β†’ (((π΄β€˜πΎ) prefix 𝑃) ++ ((π΄β€˜πΎ) substr βŸ¨π‘ƒ, (β™―β€˜(π΄β€˜πΎ))⟩)) = (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΅β€˜πΏ) substr βŸ¨π‘„, (β™―β€˜(π΅β€˜πΏ))⟩)))
23883, 237mtand 813 . . . . . 6 (πœ‘ β†’ Β¬ 𝑃 = (𝑄 + 1))
239238pm2.21d 121 . . . . 5 (πœ‘ β†’ (𝑃 = (𝑄 + 1) β†’ (π΄β€˜0) = (π΅β€˜0)))
24071elfzelzd 13508 . . . . . . . . . . 11 (πœ‘ β†’ 𝑄 ∈ β„€)
241240zcnd 12671 . . . . . . . . . 10 (πœ‘ β†’ 𝑄 ∈ β„‚)
242 1cnd 11213 . . . . . . . . . 10 (πœ‘ β†’ 1 ∈ β„‚)
243241, 242, 242addassd 11240 . . . . . . . . 9 (πœ‘ β†’ ((𝑄 + 1) + 1) = (𝑄 + (1 + 1)))
244 df-2 12279 . . . . . . . . . 10 2 = (1 + 1)
245244oveq2i 7416 . . . . . . . . 9 (𝑄 + 2) = (𝑄 + (1 + 1))
246243, 245eqtr4di 2784 . . . . . . . 8 (πœ‘ β†’ ((𝑄 + 1) + 1) = (𝑄 + 2))
247246fveq2d 6889 . . . . . . 7 (πœ‘ β†’ (β„€β‰₯β€˜((𝑄 + 1) + 1)) = (β„€β‰₯β€˜(𝑄 + 2)))
248247eleq2d 2813 . . . . . 6 (πœ‘ β†’ (𝑃 ∈ (β„€β‰₯β€˜((𝑄 + 1) + 1)) ↔ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))))
2493, 7, 8, 9, 10, 11efgsfo 19659 . . . . . . . . . 10 𝑆:dom 𝑆–ontoβ†’π‘Š
250 swrdcl 14601 . . . . . . . . . . . . 13 ((π΄β€˜πΎ) ∈ Word (𝐼 Γ— 2o) β†’ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o))
25137, 250syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o))
252 ccatcl 14530 . . . . . . . . . . . 12 ((((π΅β€˜πΏ) prefix 𝑄) ∈ Word (𝐼 Γ— 2o) ∧ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩) ∈ Word (𝐼 Γ— 2o)) β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) ∈ Word (𝐼 Γ— 2o))
253117, 251, 252syl2anc 583 . . . . . . . . . . 11 (πœ‘ β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) ∈ Word (𝐼 Γ— 2o))
2543efgrcl 19635 . . . . . . . . . . . . 13 ((π΄β€˜πΎ) ∈ π‘Š β†’ (𝐼 ∈ V ∧ π‘Š = Word (𝐼 Γ— 2o)))
25536, 254syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐼 ∈ V ∧ π‘Š = Word (𝐼 Γ— 2o)))
256255simprd 495 . . . . . . . . . . 11 (πœ‘ β†’ π‘Š = Word (𝐼 Γ— 2o))
257253, 256eleqtrrd 2830 . . . . . . . . . 10 (πœ‘ β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) ∈ π‘Š)
258 foelrn 7102 . . . . . . . . . 10 ((𝑆:dom 𝑆–ontoβ†’π‘Š ∧ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) ∈ π‘Š) β†’ βˆƒπ‘ ∈ dom 𝑆(((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))
259249, 257, 258sylancr 586 . . . . . . . . 9 (πœ‘ β†’ βˆƒπ‘ ∈ dom 𝑆(((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))
260259adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) β†’ βˆƒπ‘ ∈ dom 𝑆(((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))
26120ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))) β†’ βˆ€π‘Ž ∈ dom π‘†βˆ€π‘ ∈ dom 𝑆((β™―β€˜(π‘†β€˜π‘Ž)) < (β™―β€˜(π‘†β€˜π΄)) β†’ ((π‘†β€˜π‘Ž) = (π‘†β€˜π‘) β†’ (π‘Žβ€˜0) = (π‘β€˜0))))
2626ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))) β†’ 𝐴 ∈ dom 𝑆)
26321ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))) β†’ 𝐡 ∈ dom 𝑆)
26422ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))) β†’ (π‘†β€˜π΄) = (π‘†β€˜π΅))
26523ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))) β†’ Β¬ (π΄β€˜0) = (π΅β€˜0))
26638ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))) β†’ 𝑃 ∈ (0...(β™―β€˜(π΄β€˜πΎ))))
26771ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))) β†’ 𝑄 ∈ (0...(β™―β€˜(π΅β€˜πΏ))))
26885ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))) β†’ π‘ˆ ∈ (𝐼 Γ— 2o))
26996ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))) β†’ 𝑉 ∈ (𝐼 Γ— 2o))
27084ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))) β†’ (π‘†β€˜π΄) = (𝑃(π‘‡β€˜(π΄β€˜πΎ))π‘ˆ))
27195ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))) β†’ (π‘†β€˜π΅) = (𝑄(π‘‡β€˜(π΅β€˜πΏ))𝑉))
2722ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))) β†’ Β¬ (π΄β€˜πΎ) = (π΅β€˜πΏ))
273 simplr 766 . . . . . . . . 9 (((πœ‘ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))) β†’ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2)))
274 simprl 768 . . . . . . . . 9 (((πœ‘ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))) β†’ 𝑐 ∈ dom 𝑆)
275 simprr 770 . . . . . . . . . 10 (((πœ‘ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))) β†’ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))
276275eqcomd 2732 . . . . . . . . 9 (((πœ‘ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))) β†’ (π‘†β€˜π‘) = (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)))
2773, 7, 8, 9, 10, 11, 261, 262, 263, 264, 265, 19, 57, 266, 267, 268, 269, 270, 271, 272, 273, 274, 276efgredlemd 19664 . . . . . . . 8 (((πœ‘ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((π΅β€˜πΏ) prefix 𝑄) ++ ((π΄β€˜πΎ) substr ⟨(𝑄 + 2), (β™―β€˜(π΄β€˜πΎ))⟩)) = (π‘†β€˜π‘))) β†’ (π΄β€˜0) = (π΅β€˜0))
278260, 277rexlimddv 3155 . . . . . . 7 ((πœ‘ ∧ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2))) β†’ (π΄β€˜0) = (π΅β€˜0))
279278ex 412 . . . . . 6 (πœ‘ β†’ (𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 2)) β†’ (π΄β€˜0) = (π΅β€˜0)))
280248, 279sylbid 239 . . . . 5 (πœ‘ β†’ (𝑃 ∈ (β„€β‰₯β€˜((𝑄 + 1) + 1)) β†’ (π΄β€˜0) = (π΅β€˜0)))
281239, 280jaod 856 . . . 4 (πœ‘ β†’ ((𝑃 = (𝑄 + 1) ∨ 𝑃 ∈ (β„€β‰₯β€˜((𝑄 + 1) + 1))) β†’ (π΄β€˜0) = (π΅β€˜0)))
282153, 281syl5 34 . . 3 (πœ‘ β†’ (𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 1)) β†’ (π΄β€˜0) = (π΅β€˜0)))
283152, 282jaod 856 . 2 (πœ‘ β†’ ((𝑃 = 𝑄 ∨ 𝑃 ∈ (β„€β‰₯β€˜(𝑄 + 1))) β†’ (π΄β€˜0) = (π΅β€˜0)))
2841, 283syl5 34 1 (πœ‘ β†’ (𝑃 ∈ (β„€β‰₯β€˜π‘„) β†’ (π΄β€˜0) = (π΅β€˜0)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   = wceq 1533   ∈ wcel 2098  βˆ€wral 3055  βˆƒwrex 3064  {crab 3426  Vcvv 3468   βˆ– cdif 3940  βˆ…c0 4317  {csn 4623  βŸ¨cop 4629  βŸ¨cotp 4631  βˆͺ ciun 4990   class class class wbr 5141   ↦ cmpt 5224   I cid 5566   Γ— cxp 5667  dom cdm 5669  ran crn 5670  βŸΆwf 6533  β€“ontoβ†’wfo 6535  β€˜cfv 6537  (class class class)co 7405   ∈ cmpo 7407  1oc1o 8460  2oc2o 8461  0cc0 11112  1c1 11113   + caddc 11115   < clt 11252   βˆ’ cmin 11448  β„•cn 12216  2c2 12271  β„•0cn0 12476  β„€cz 12562  β„€β‰₯cuz 12826  ...cfz 13490  ..^cfzo 13633  β™―chash 14295  Word cword 14470   ++ cconcat 14526  βŸ¨β€œcs1 14551   substr csubstr 14596   prefix cpfx 14626   splice csplice 14705  βŸ¨β€œcs2 14798   ~FG cefg 19626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  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 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-ot 4632  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7853  df-1st 7974  df-2nd 7975  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-2o 8468  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-n0 12477  df-xnn0 12549  df-z 12563  df-uz 12827  df-rp 12981  df-fz 13491  df-fzo 13634  df-hash 14296  df-word 14471  df-concat 14527  df-s1 14552  df-substr 14597  df-pfx 14627  df-splice 14706  df-s2 14805
This theorem is referenced by:  efgredlemb  19666
  Copyright terms: Public domain W3C validator