Metamath Proof Explorer

Theorem pfxmpt

Description: Value of the prefix extractor as a mapping. (Contributed by AV, 2-May-2020)

Ref Expression
Assertion pfxmpt 
|- ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S prefix L ) = ( x e. ( 0 ..^ L ) |-> ( S ` x ) ) )

Proof

Step Hyp Ref Expression
1 elfznn0 
 |-  ( L e. ( 0 ... ( # ` S ) ) -> L e. NN0 )
2 pfxval 
 |-  ( ( S e. Word A /\ L e. NN0 ) -> ( S prefix L ) = ( S substr <. 0 , L >. ) )
3 1 2 sylan2 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S prefix L ) = ( S substr <. 0 , L >. ) )
4 simpl 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> S e. Word A )
5 1 adantl 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> L e. NN0 )
6 0elfz 
 |-  ( L e. NN0 -> 0 e. ( 0 ... L ) )
7 5 6 syl 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> 0 e. ( 0 ... L ) )
8 simpr 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> L e. ( 0 ... ( # ` S ) ) )
9 swrdval2 
 |-  ( ( S e. Word A /\ 0 e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S substr <. 0 , L >. ) = ( x e. ( 0 ..^ ( L - 0 ) ) |-> ( S ` ( x + 0 ) ) ) )
10 4 7 8 9 syl3anc 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S substr <. 0 , L >. ) = ( x e. ( 0 ..^ ( L - 0 ) ) |-> ( S ` ( x + 0 ) ) ) )
11 nn0cn 
 |-  ( L e. NN0 -> L e. CC )
12 11 subid1d 
 |-  ( L e. NN0 -> ( L - 0 ) = L )
13 1 12 syl 
 |-  ( L e. ( 0 ... ( # ` S ) ) -> ( L - 0 ) = L )
14 13 oveq2d 
 |-  ( L e. ( 0 ... ( # ` S ) ) -> ( 0 ..^ ( L - 0 ) ) = ( 0 ..^ L ) )
15 14 adantl 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( 0 ..^ ( L - 0 ) ) = ( 0 ..^ L ) )
16 elfzonn0 
 |-  ( x e. ( 0 ..^ ( L - 0 ) ) -> x e. NN0 )
17 nn0cn 
 |-  ( x e. NN0 -> x e. CC )
18 17 addid1d 
 |-  ( x e. NN0 -> ( x + 0 ) = x )
19 16 18 syl 
 |-  ( x e. ( 0 ..^ ( L - 0 ) ) -> ( x + 0 ) = x )
20 19 fveq2d 
 |-  ( x e. ( 0 ..^ ( L - 0 ) ) -> ( S ` ( x + 0 ) ) = ( S ` x ) )
21 20 adantl 
 |-  ( ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) /\ x e. ( 0 ..^ ( L - 0 ) ) ) -> ( S ` ( x + 0 ) ) = ( S ` x ) )
22 15 21 mpteq12dva 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( x e. ( 0 ..^ ( L - 0 ) ) |-> ( S ` ( x + 0 ) ) ) = ( x e. ( 0 ..^ L ) |-> ( S ` x ) ) )
23 3 10 22 3eqtrd 
 |-  ( ( S e. Word A /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S prefix L ) = ( x e. ( 0 ..^ L ) |-> ( S ` x ) ) )