Metamath Proof Explorer

Theorem iwrdsplit

Description: Lemma for sseqp1 . (Contributed by Thierry Arnoux, 25-Apr-2019) (Proof shortened by AV, 14-Oct-2022)

Ref Expression
Hypotheses iwrdsplit.s 
|- ( ph -> S e. _V )
iwrdsplit.f 
|- ( ph -> F : NN0 --> S )
iwrdsplit.n 
|- ( ph -> N e. NN0 )
Assertion iwrdsplit 
|- ( ph -> ( F |` ( 0 ..^ ( N + 1 ) ) ) = ( ( F |` ( 0 ..^ N ) ) ++ <" ( F ` N ) "> ) )

Proof

Step Hyp Ref Expression
1 iwrdsplit.s 
 |-  ( ph -> S e. _V )
2 iwrdsplit.f 
 |-  ( ph -> F : NN0 --> S )
3 iwrdsplit.n 
 |-  ( ph -> N e. NN0 )
4 1nn0 
 |-  1 e. NN0
5 4 a1i 
 |-  ( ph -> 1 e. NN0 )
6 3 5 nn0addcld 
 |-  ( ph -> ( N + 1 ) e. NN0 )
7 1 2 6 subiwrd 
 |-  ( ph -> ( F |` ( 0 ..^ ( N + 1 ) ) ) e. Word S )
8 1re 
 |-  1 e. RR
9 nn0addge2 
 |-  ( ( 1 e. RR /\ N e. NN0 ) -> 1 <_ ( N + 1 ) )
10 8 3 9 sylancr 
 |-  ( ph -> 1 <_ ( N + 1 ) )
11 1 2 6 subiwrdlen 
 |-  ( ph -> ( # ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) = ( N + 1 ) )
12 10 11 breqtrrd 
 |-  ( ph -> 1 <_ ( # ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) )
13 wrdlenge1n0 
 |-  ( ( F |` ( 0 ..^ ( N + 1 ) ) ) e. Word S -> ( ( F |` ( 0 ..^ ( N + 1 ) ) ) =/= (/) <-> 1 <_ ( # ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) ) )
14 7 13 syl 
 |-  ( ph -> ( ( F |` ( 0 ..^ ( N + 1 ) ) ) =/= (/) <-> 1 <_ ( # ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) ) )
15 12 14 mpbird 
 |-  ( ph -> ( F |` ( 0 ..^ ( N + 1 ) ) ) =/= (/) )
16 pfxlswccat 
 |-  ( ( ( F |` ( 0 ..^ ( N + 1 ) ) ) e. Word S /\ ( F |` ( 0 ..^ ( N + 1 ) ) ) =/= (/) ) -> ( ( ( F |` ( 0 ..^ ( N + 1 ) ) ) prefix ( ( # ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) - 1 ) ) ++ <" ( lastS ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) "> ) = ( F |` ( 0 ..^ ( N + 1 ) ) ) )
17 7 15 16 syl2anc 
 |-  ( ph -> ( ( ( F |` ( 0 ..^ ( N + 1 ) ) ) prefix ( ( # ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) - 1 ) ) ++ <" ( lastS ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) "> ) = ( F |` ( 0 ..^ ( N + 1 ) ) ) )
18 3 nn0cnd 
 |-  ( ph -> N e. CC )
19 1cnd 
 |-  ( ph -> 1 e. CC )
20 18 19 11 mvrraddd 
 |-  ( ph -> ( ( # ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) - 1 ) = N )
21 20 oveq2d 
 |-  ( ph -> ( ( F |` ( 0 ..^ ( N + 1 ) ) ) prefix ( ( # ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) - 1 ) ) = ( ( F |` ( 0 ..^ ( N + 1 ) ) ) prefix N ) )
22 nn0fz0 
 |-  ( N e. NN0 <-> N e. ( 0 ... N ) )
23 3 22 sylib 
 |-  ( ph -> N e. ( 0 ... N ) )
24 elfz0add 
 |-  ( ( N e. NN0 /\ 1 e. NN0 ) -> ( N e. ( 0 ... N ) -> N e. ( 0 ... ( N + 1 ) ) ) )
25 24 imp 
 |-  ( ( ( N e. NN0 /\ 1 e. NN0 ) /\ N e. ( 0 ... N ) ) -> N e. ( 0 ... ( N + 1 ) ) )
26 3 5 23 25 syl21anc 
 |-  ( ph -> N e. ( 0 ... ( N + 1 ) ) )
27 11 oveq2d 
 |-  ( ph -> ( 0 ... ( # ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) ) = ( 0 ... ( N + 1 ) ) )
28 26 27 eleqtrrd 
 |-  ( ph -> N e. ( 0 ... ( # ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) ) )
29 pfxres 
 |-  ( ( ( F |` ( 0 ..^ ( N + 1 ) ) ) e. Word S /\ N e. ( 0 ... ( # ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) ) ) -> ( ( F |` ( 0 ..^ ( N + 1 ) ) ) prefix N ) = ( ( F |` ( 0 ..^ ( N + 1 ) ) ) |` ( 0 ..^ N ) ) )
30 7 28 29 syl2anc 
 |-  ( ph -> ( ( F |` ( 0 ..^ ( N + 1 ) ) ) prefix N ) = ( ( F |` ( 0 ..^ ( N + 1 ) ) ) |` ( 0 ..^ N ) ) )
31 fzossfzop1 
 |-  ( N e. NN0 -> ( 0 ..^ N ) C_ ( 0 ..^ ( N + 1 ) ) )
32 resabs1 
 |-  ( ( 0 ..^ N ) C_ ( 0 ..^ ( N + 1 ) ) -> ( ( F |` ( 0 ..^ ( N + 1 ) ) ) |` ( 0 ..^ N ) ) = ( F |` ( 0 ..^ N ) ) )
33 3 31 32 3syl 
 |-  ( ph -> ( ( F |` ( 0 ..^ ( N + 1 ) ) ) |` ( 0 ..^ N ) ) = ( F |` ( 0 ..^ N ) ) )
34 21 30 33 3eqtrd 
 |-  ( ph -> ( ( F |` ( 0 ..^ ( N + 1 ) ) ) prefix ( ( # ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) - 1 ) ) = ( F |` ( 0 ..^ N ) ) )
35 lsw 
 |-  ( ( F |` ( 0 ..^ ( N + 1 ) ) ) e. Word S -> ( lastS ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) = ( ( F |` ( 0 ..^ ( N + 1 ) ) ) ` ( ( # ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) - 1 ) ) )
36 7 35 syl 
 |-  ( ph -> ( lastS ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) = ( ( F |` ( 0 ..^ ( N + 1 ) ) ) ` ( ( # ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) - 1 ) ) )
37 20 fveq2d 
 |-  ( ph -> ( ( F |` ( 0 ..^ ( N + 1 ) ) ) ` ( ( # ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) - 1 ) ) = ( ( F |` ( 0 ..^ ( N + 1 ) ) ) ` N ) )
38 fzonn0p1 
 |-  ( N e. NN0 -> N e. ( 0 ..^ ( N + 1 ) ) )
39 fvres 
 |-  ( N e. ( 0 ..^ ( N + 1 ) ) -> ( ( F |` ( 0 ..^ ( N + 1 ) ) ) ` N ) = ( F ` N ) )
40 3 38 39 3syl 
 |-  ( ph -> ( ( F |` ( 0 ..^ ( N + 1 ) ) ) ` N ) = ( F ` N ) )
41 36 37 40 3eqtrd 
 |-  ( ph -> ( lastS ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) = ( F ` N ) )
42 41 s1eqd 
 |-  ( ph -> <" ( lastS ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) "> = <" ( F ` N ) "> )
43 34 42 oveq12d 
 |-  ( ph -> ( ( ( F |` ( 0 ..^ ( N + 1 ) ) ) prefix ( ( # ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) - 1 ) ) ++ <" ( lastS ` ( F |` ( 0 ..^ ( N + 1 ) ) ) ) "> ) = ( ( F |` ( 0 ..^ N ) ) ++ <" ( F ` N ) "> ) )
44 17 43 eqtr3d 
 |-  ( ph -> ( F |` ( 0 ..^ ( N + 1 ) ) ) = ( ( F |` ( 0 ..^ N ) ) ++ <" ( F ` N ) "> ) )