This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pfxco

Description: Mapping of words commutes with the prefix operation. (Contributed by AV, 15-May-2020)

Ref Expression
Assertion pfxco 
|- ( ( W e. Word A /\ N e. ( 0 ... ( # ` W ) ) /\ F : A --> B ) -> ( F o. ( W prefix N ) ) = ( ( F o. W ) prefix N ) )

Proof

Step Hyp Ref Expression
1 elfznn0 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> N e. NN0 )
2 1 3ad2ant2 
 |-  ( ( W e. Word A /\ N e. ( 0 ... ( # ` W ) ) /\ F : A --> B ) -> N e. NN0 )
3 0elfz 
 |-  ( N e. NN0 -> 0 e. ( 0 ... N ) )
4 2 3 syl 
 |-  ( ( W e. Word A /\ N e. ( 0 ... ( # ` W ) ) /\ F : A --> B ) -> 0 e. ( 0 ... N ) )
5 simp2 
 |-  ( ( W e. Word A /\ N e. ( 0 ... ( # ` W ) ) /\ F : A --> B ) -> N e. ( 0 ... ( # ` W ) ) )
6 4 5 jca 
 |-  ( ( W e. Word A /\ N e. ( 0 ... ( # ` W ) ) /\ F : A --> B ) -> ( 0 e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) )
7 swrdco 
 |-  ( ( W e. Word A /\ ( 0 e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) -> ( F o. ( W substr <. 0 , N >. ) ) = ( ( F o. W ) substr <. 0 , N >. ) )
8 6 7 syld3an2 
 |-  ( ( W e. Word A /\ N e. ( 0 ... ( # ` W ) ) /\ F : A --> B ) -> ( F o. ( W substr <. 0 , N >. ) ) = ( ( F o. W ) substr <. 0 , N >. ) )
9 pfxval 
 |-  ( ( W e. Word A /\ N e. NN0 ) -> ( W prefix N ) = ( W substr <. 0 , N >. ) )
10 1 9 sylan2 
 |-  ( ( W e. Word A /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W prefix N ) = ( W substr <. 0 , N >. ) )
11 10 coeq2d 
 |-  ( ( W e. Word A /\ N e. ( 0 ... ( # ` W ) ) ) -> ( F o. ( W prefix N ) ) = ( F o. ( W substr <. 0 , N >. ) ) )
12 11 3adant3 
 |-  ( ( W e. Word A /\ N e. ( 0 ... ( # ` W ) ) /\ F : A --> B ) -> ( F o. ( W prefix N ) ) = ( F o. ( W substr <. 0 , N >. ) ) )
13 ffun 
 |-  ( F : A --> B -> Fun F )
14 13 anim2i 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( W e. Word A /\ Fun F ) )
15 14 ancomd 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( Fun F /\ W e. Word A ) )
16 15 3adant2 
 |-  ( ( W e. Word A /\ N e. ( 0 ... ( # ` W ) ) /\ F : A --> B ) -> ( Fun F /\ W e. Word A ) )
17 cofunexg 
 |-  ( ( Fun F /\ W e. Word A ) -> ( F o. W ) e. _V )
18 16 17 syl 
 |-  ( ( W e. Word A /\ N e. ( 0 ... ( # ` W ) ) /\ F : A --> B ) -> ( F o. W ) e. _V )
19 18 2 jca 
 |-  ( ( W e. Word A /\ N e. ( 0 ... ( # ` W ) ) /\ F : A --> B ) -> ( ( F o. W ) e. _V /\ N e. NN0 ) )
20 pfxval 
 |-  ( ( ( F o. W ) e. _V /\ N e. NN0 ) -> ( ( F o. W ) prefix N ) = ( ( F o. W ) substr <. 0 , N >. ) )
21 19 20 syl 
 |-  ( ( W e. Word A /\ N e. ( 0 ... ( # ` W ) ) /\ F : A --> B ) -> ( ( F o. W ) prefix N ) = ( ( F o. W ) substr <. 0 , N >. ) )
22 8 12 21 3eqtr4d 
 |-  ( ( W e. Word A /\ N e. ( 0 ... ( # ` W ) ) /\ F : A --> B ) -> ( F o. ( W prefix N ) ) = ( ( F o. W ) prefix N ) )