Metamath Proof Explorer


Theorem wrdsplex

Description: Existence of a split of a word at a given index. (Contributed by Thierry Arnoux, 11-Oct-2018) (Proof shortened by AV, 3-Nov-2022)

Ref Expression
Assertion wrdsplex
|- ( ( W e. Word S /\ N e. ( 0 ... ( # ` W ) ) ) -> E. v e. Word S W = ( ( W |` ( 0 ..^ N ) ) ++ v ) )

Proof

Step Hyp Ref Expression
1 swrdcl
 |-  ( W e. Word S -> ( W substr <. N , ( # ` W ) >. ) e. Word S )
2 simpr
 |-  ( ( W e. Word S /\ N e. ( 0 ... ( # ` W ) ) ) -> N e. ( 0 ... ( # ` W ) ) )
3 elfzuz2
 |-  ( N e. ( 0 ... ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` 0 ) )
4 eluzfz2
 |-  ( ( # ` W ) e. ( ZZ>= ` 0 ) -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
5 2 3 4 3syl
 |-  ( ( W e. Word S /\ N e. ( 0 ... ( # ` W ) ) ) -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
6 ccatpfx
 |-  ( ( W e. Word S /\ N e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix N ) ++ ( W substr <. N , ( # ` W ) >. ) ) = ( W prefix ( # ` W ) ) )
7 5 6 mpd3an3
 |-  ( ( W e. Word S /\ N e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix N ) ++ ( W substr <. N , ( # ` W ) >. ) ) = ( W prefix ( # ` W ) ) )
8 pfxres
 |-  ( ( W e. Word S /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W prefix N ) = ( W |` ( 0 ..^ N ) ) )
9 8 oveq1d
 |-  ( ( W e. Word S /\ N e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix N ) ++ ( W substr <. N , ( # ` W ) >. ) ) = ( ( W |` ( 0 ..^ N ) ) ++ ( W substr <. N , ( # ` W ) >. ) ) )
10 pfxid
 |-  ( W e. Word S -> ( W prefix ( # ` W ) ) = W )
11 10 adantr
 |-  ( ( W e. Word S /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W prefix ( # ` W ) ) = W )
12 7 9 11 3eqtr3rd
 |-  ( ( W e. Word S /\ N e. ( 0 ... ( # ` W ) ) ) -> W = ( ( W |` ( 0 ..^ N ) ) ++ ( W substr <. N , ( # ` W ) >. ) ) )
13 oveq2
 |-  ( v = ( W substr <. N , ( # ` W ) >. ) -> ( ( W |` ( 0 ..^ N ) ) ++ v ) = ( ( W |` ( 0 ..^ N ) ) ++ ( W substr <. N , ( # ` W ) >. ) ) )
14 13 rspceeqv
 |-  ( ( ( W substr <. N , ( # ` W ) >. ) e. Word S /\ W = ( ( W |` ( 0 ..^ N ) ) ++ ( W substr <. N , ( # ` W ) >. ) ) ) -> E. v e. Word S W = ( ( W |` ( 0 ..^ N ) ) ++ v ) )
15 1 12 14 syl2an2r
 |-  ( ( W e. Word S /\ N e. ( 0 ... ( # ` W ) ) ) -> E. v e. Word S W = ( ( W |` ( 0 ..^ N ) ) ++ v ) )