Metamath Proof Explorer

Theorem pfxpfx

Description: A prefix of a prefix is a prefix. (Contributed by Alexander van der Vekens, 7-Apr-2018) (Revised by AV, 8-May-2020)

Ref Expression
Assertion pfxpfx 
|- ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ L e. ( 0 ... N ) ) -> ( ( W prefix N ) prefix L ) = ( W prefix L ) )

Proof

Step Hyp Ref Expression
1 elfznn0 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> N e. NN0 )
2 1 anim2i 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W e. Word V /\ N e. NN0 ) )
3 2 3adant3 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ L e. ( 0 ... N ) ) -> ( W e. Word V /\ N e. NN0 ) )
4 pfxval 
 |-  ( ( W e. Word V /\ N e. NN0 ) -> ( W prefix N ) = ( W substr <. 0 , N >. ) )
5 3 4 syl 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ L e. ( 0 ... N ) ) -> ( W prefix N ) = ( W substr <. 0 , N >. ) )
6 5 oveq1d 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ L e. ( 0 ... N ) ) -> ( ( W prefix N ) prefix L ) = ( ( W substr <. 0 , N >. ) prefix L ) )
7 simp1 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ L e. ( 0 ... N ) ) -> W e. Word V )
8 simp2 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ L e. ( 0 ... N ) ) -> N e. ( 0 ... ( # ` W ) ) )
9 0elfz 
 |-  ( N e. NN0 -> 0 e. ( 0 ... N ) )
10 1 9 syl 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> 0 e. ( 0 ... N ) )
11 10 3ad2ant2 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ L e. ( 0 ... N ) ) -> 0 e. ( 0 ... N ) )
12 7 8 11 3jca 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ L e. ( 0 ... N ) ) -> ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ 0 e. ( 0 ... N ) ) )
13 1 nn0cnd 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> N e. CC )
14 13 subid1d 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> ( N - 0 ) = N )
15 14 eqcomd 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> N = ( N - 0 ) )
16 15 adantl 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> N = ( N - 0 ) )
17 16 oveq2d 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( 0 ... N ) = ( 0 ... ( N - 0 ) ) )
18 17 eleq2d 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) ) -> ( L e. ( 0 ... N ) <-> L e. ( 0 ... ( N - 0 ) ) ) )
19 18 biimp3a 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ L e. ( 0 ... N ) ) -> L e. ( 0 ... ( N - 0 ) ) )
20 pfxswrd 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ 0 e. ( 0 ... N ) ) -> ( L e. ( 0 ... ( N - 0 ) ) -> ( ( W substr <. 0 , N >. ) prefix L ) = ( W substr <. 0 , ( 0 + L ) >. ) ) )
21 12 19 20 sylc 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ L e. ( 0 ... N ) ) -> ( ( W substr <. 0 , N >. ) prefix L ) = ( W substr <. 0 , ( 0 + L ) >. ) )
22 elfznn0 
 |-  ( L e. ( 0 ... N ) -> L e. NN0 )
23 22 nn0cnd 
 |-  ( L e. ( 0 ... N ) -> L e. CC )
24 23 addid2d 
 |-  ( L e. ( 0 ... N ) -> ( 0 + L ) = L )
25 24 opeq2d 
 |-  ( L e. ( 0 ... N ) -> <. 0 , ( 0 + L ) >. = <. 0 , L >. )
26 25 oveq2d 
 |-  ( L e. ( 0 ... N ) -> ( W substr <. 0 , ( 0 + L ) >. ) = ( W substr <. 0 , L >. ) )
27 26 3ad2ant3 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ L e. ( 0 ... N ) ) -> ( W substr <. 0 , ( 0 + L ) >. ) = ( W substr <. 0 , L >. ) )
28 22 anim2i 
 |-  ( ( W e. Word V /\ L e. ( 0 ... N ) ) -> ( W e. Word V /\ L e. NN0 ) )
29 28 3adant2 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ L e. ( 0 ... N ) ) -> ( W e. Word V /\ L e. NN0 ) )
30 pfxval 
 |-  ( ( W e. Word V /\ L e. NN0 ) -> ( W prefix L ) = ( W substr <. 0 , L >. ) )
31 29 30 syl 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ L e. ( 0 ... N ) ) -> ( W prefix L ) = ( W substr <. 0 , L >. ) )
32 27 31 eqtr4d 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ L e. ( 0 ... N ) ) -> ( W substr <. 0 , ( 0 + L ) >. ) = ( W prefix L ) )
33 6 21 32 3eqtrd 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ L e. ( 0 ... N ) ) -> ( ( W prefix N ) prefix L ) = ( W prefix L ) )