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