Metamath Proof Explorer

Theorem pfxfv

Description: A symbol in a prefix of a word, indexed using the prefix' indices. (Contributed by Alexander van der Vekens, 16-Jun-2018) (Revised by AV, 3-May-2020)

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

Proof

Step Hyp Ref Expression
1 elfznn0 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> L e. NN0 )
2 pfxval 
 |-  ( ( W e. Word V /\ L e. NN0 ) -> ( W prefix L ) = ( W substr <. 0 , L >. ) )
3 1 2 sylan2 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) ) -> ( W prefix L ) = ( W substr <. 0 , L >. ) )
4 3 3adant3 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> ( W prefix L ) = ( W substr <. 0 , L >. ) )
5 4 fveq1d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> ( ( W prefix L ) ` I ) = ( ( W substr <. 0 , L >. ) ` I ) )
6 simp1 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> W e. Word V )
7 0elfz 
 |-  ( L e. NN0 -> 0 e. ( 0 ... L ) )
8 1 7 syl 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> 0 e. ( 0 ... L ) )
9 8 3ad2ant2 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> 0 e. ( 0 ... L ) )
10 simp2 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> L e. ( 0 ... ( # ` W ) ) )
11 1 nn0cnd 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> L e. CC )
12 11 subid1d 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> ( L - 0 ) = L )
13 12 eqcomd 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> L = ( L - 0 ) )
14 13 oveq2d 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> ( 0 ..^ L ) = ( 0 ..^ ( L - 0 ) ) )
15 14 eleq2d 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> ( I e. ( 0 ..^ L ) <-> I e. ( 0 ..^ ( L - 0 ) ) ) )
16 15 biimpd 
 |-  ( L e. ( 0 ... ( # ` W ) ) -> ( I e. ( 0 ..^ L ) -> I e. ( 0 ..^ ( L - 0 ) ) ) )
17 16 a1i 
 |-  ( W e. Word V -> ( L e. ( 0 ... ( # ` W ) ) -> ( I e. ( 0 ..^ L ) -> I e. ( 0 ..^ ( L - 0 ) ) ) ) )
18 17 3imp 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> I e. ( 0 ..^ ( L - 0 ) ) )
19 swrdfv 
 |-  ( ( ( W e. Word V /\ 0 e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` W ) ) ) /\ I e. ( 0 ..^ ( L - 0 ) ) ) -> ( ( W substr <. 0 , L >. ) ` I ) = ( W ` ( I + 0 ) ) )
20 6 9 10 18 19 syl31anc 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> ( ( W substr <. 0 , L >. ) ` I ) = ( W ` ( I + 0 ) ) )
21 elfzoelz 
 |-  ( I e. ( 0 ..^ L ) -> I e. ZZ )
22 21 zcnd 
 |-  ( I e. ( 0 ..^ L ) -> I e. CC )
23 22 addid1d 
 |-  ( I e. ( 0 ..^ L ) -> ( I + 0 ) = I )
24 23 3ad2ant3 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> ( I + 0 ) = I )
25 24 fveq2d 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> ( W ` ( I + 0 ) ) = ( W ` I ) )
26 5 20 25 3eqtrd 
 |-  ( ( W e. Word V /\ L e. ( 0 ... ( # ` W ) ) /\ I e. ( 0 ..^ L ) ) -> ( ( W prefix L ) ` I ) = ( W ` I ) )