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 ) )