Metamath Proof Explorer

Theorem swrdco

Description: Mapping of words commutes with the substring operation. (Contributed by AV, 11-Nov-2018)

Ref Expression
Assertion swrdco 
|- ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) -> ( F o. ( W substr <. M , N >. ) ) = ( ( F o. W ) substr <. M , N >. ) )

Proof

Step Hyp Ref Expression
1 ffn 
 |-  ( F : A --> B -> F Fn A )
2 1 3ad2ant3 
 |-  ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) -> F Fn A )
3 swrdvalfn 
 |-  ( ( W e. Word A /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) )
4 3 3expb 
 |-  ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) ) -> ( W substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) )
5 4 3adant3 
 |-  ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) -> ( W substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) )
6 swrdrn 
 |-  ( ( W e. Word A /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ran ( W substr <. M , N >. ) C_ A )
7 6 3expb 
 |-  ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) ) -> ran ( W substr <. M , N >. ) C_ A )
8 7 3adant3 
 |-  ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) -> ran ( W substr <. M , N >. ) C_ A )
9 fnco 
 |-  ( ( F Fn A /\ ( W substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) /\ ran ( W substr <. M , N >. ) C_ A ) -> ( F o. ( W substr <. M , N >. ) ) Fn ( 0 ..^ ( N - M ) ) )
10 2 5 8 9 syl3anc 
 |-  ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) -> ( F o. ( W substr <. M , N >. ) ) Fn ( 0 ..^ ( N - M ) ) )
11 wrdco 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( F o. W ) e. Word B )
12 11 3adant2 
 |-  ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) -> ( F o. W ) e. Word B )
13 simp2l 
 |-  ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) -> M e. ( 0 ... N ) )
14 lenco 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( # ` ( F o. W ) ) = ( # ` W ) )
15 14 eqcomd 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( # ` W ) = ( # ` ( F o. W ) ) )
16 15 oveq2d 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( 0 ... ( # ` W ) ) = ( 0 ... ( # ` ( F o. W ) ) ) )
17 16 eleq2d 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( N e. ( 0 ... ( # ` W ) ) <-> N e. ( 0 ... ( # ` ( F o. W ) ) ) ) )
18 17 biimpd 
 |-  ( ( W e. Word A /\ F : A --> B ) -> ( N e. ( 0 ... ( # ` W ) ) -> N e. ( 0 ... ( # ` ( F o. W ) ) ) ) )
19 18 expcom 
 |-  ( F : A --> B -> ( W e. Word A -> ( N e. ( 0 ... ( # ` W ) ) -> N e. ( 0 ... ( # ` ( F o. W ) ) ) ) ) )
20 19 com13 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> ( W e. Word A -> ( F : A --> B -> N e. ( 0 ... ( # ` ( F o. W ) ) ) ) ) )
21 20 adantl 
 |-  ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W e. Word A -> ( F : A --> B -> N e. ( 0 ... ( # ` ( F o. W ) ) ) ) ) )
22 21 3imp21 
 |-  ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) -> N e. ( 0 ... ( # ` ( F o. W ) ) ) )
23 swrdvalfn 
 |-  ( ( ( F o. W ) e. Word B /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` ( F o. W ) ) ) ) -> ( ( F o. W ) substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) )
24 12 13 22 23 syl3anc 
 |-  ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) -> ( ( F o. W ) substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) )
25 3anass 
 |-  ( ( W e. Word A /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) <-> ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) ) )
26 25 biimpri 
 |-  ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) ) -> ( W e. Word A /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) )
27 26 3adant3 
 |-  ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) -> ( W e. Word A /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) )
28 swrdfv 
 |-  ( ( ( W e. Word A /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ i e. ( 0 ..^ ( N - M ) ) ) -> ( ( W substr <. M , N >. ) ` i ) = ( W ` ( i + M ) ) )
29 28 fveq2d 
 |-  ( ( ( W e. Word A /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ i e. ( 0 ..^ ( N - M ) ) ) -> ( F ` ( ( W substr <. M , N >. ) ` i ) ) = ( F ` ( W ` ( i + M ) ) ) )
30 27 29 sylan 
 |-  ( ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) /\ i e. ( 0 ..^ ( N - M ) ) ) -> ( F ` ( ( W substr <. M , N >. ) ` i ) ) = ( F ` ( W ` ( i + M ) ) ) )
31 wrdfn 
 |-  ( W e. Word A -> W Fn ( 0 ..^ ( # ` W ) ) )
32 31 3ad2ant1 
 |-  ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) -> W Fn ( 0 ..^ ( # ` W ) ) )
33 elfzodifsumelfzo 
 |-  ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( i e. ( 0 ..^ ( N - M ) ) -> ( i + M ) e. ( 0 ..^ ( # ` W ) ) ) )
34 33 3ad2ant2 
 |-  ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) -> ( i e. ( 0 ..^ ( N - M ) ) -> ( i + M ) e. ( 0 ..^ ( # ` W ) ) ) )
35 34 imp 
 |-  ( ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) /\ i e. ( 0 ..^ ( N - M ) ) ) -> ( i + M ) e. ( 0 ..^ ( # ` W ) ) )
36 fvco2 
 |-  ( ( W Fn ( 0 ..^ ( # ` W ) ) /\ ( i + M ) e. ( 0 ..^ ( # ` W ) ) ) -> ( ( F o. W ) ` ( i + M ) ) = ( F ` ( W ` ( i + M ) ) ) )
37 32 35 36 syl2an2r 
 |-  ( ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) /\ i e. ( 0 ..^ ( N - M ) ) ) -> ( ( F o. W ) ` ( i + M ) ) = ( F ` ( W ` ( i + M ) ) ) )
38 30 37 eqtr4d 
 |-  ( ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) /\ i e. ( 0 ..^ ( N - M ) ) ) -> ( F ` ( ( W substr <. M , N >. ) ` i ) ) = ( ( F o. W ) ` ( i + M ) ) )
39 fvco2 
 |-  ( ( ( W substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) /\ i e. ( 0 ..^ ( N - M ) ) ) -> ( ( F o. ( W substr <. M , N >. ) ) ` i ) = ( F ` ( ( W substr <. M , N >. ) ` i ) ) )
40 5 39 sylan 
 |-  ( ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) /\ i e. ( 0 ..^ ( N - M ) ) ) -> ( ( F o. ( W substr <. M , N >. ) ) ` i ) = ( F ` ( ( W substr <. M , N >. ) ` i ) ) )
41 14 ancoms 
 |-  ( ( F : A --> B /\ W e. Word A ) -> ( # ` ( F o. W ) ) = ( # ` W ) )
42 41 eqcomd 
 |-  ( ( F : A --> B /\ W e. Word A ) -> ( # ` W ) = ( # ` ( F o. W ) ) )
43 42 oveq2d 
 |-  ( ( F : A --> B /\ W e. Word A ) -> ( 0 ... ( # ` W ) ) = ( 0 ... ( # ` ( F o. W ) ) ) )
44 43 eleq2d 
 |-  ( ( F : A --> B /\ W e. Word A ) -> ( N e. ( 0 ... ( # ` W ) ) <-> N e. ( 0 ... ( # ` ( F o. W ) ) ) ) )
45 44 biimpd 
 |-  ( ( F : A --> B /\ W e. Word A ) -> ( N e. ( 0 ... ( # ` W ) ) -> N e. ( 0 ... ( # ` ( F o. W ) ) ) ) )
46 45 ex 
 |-  ( F : A --> B -> ( W e. Word A -> ( N e. ( 0 ... ( # ` W ) ) -> N e. ( 0 ... ( # ` ( F o. W ) ) ) ) ) )
47 46 com13 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> ( W e. Word A -> ( F : A --> B -> N e. ( 0 ... ( # ` ( F o. W ) ) ) ) ) )
48 47 adantl 
 |-  ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W e. Word A -> ( F : A --> B -> N e. ( 0 ... ( # ` ( F o. W ) ) ) ) ) )
49 48 3imp21 
 |-  ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) -> N e. ( 0 ... ( # ` ( F o. W ) ) ) )
50 12 13 49 3jca 
 |-  ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) -> ( ( F o. W ) e. Word B /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` ( F o. W ) ) ) ) )
51 swrdfv 
 |-  ( ( ( ( F o. W ) e. Word B /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` ( F o. W ) ) ) ) /\ i e. ( 0 ..^ ( N - M ) ) ) -> ( ( ( F o. W ) substr <. M , N >. ) ` i ) = ( ( F o. W ) ` ( i + M ) ) )
52 50 51 sylan 
 |-  ( ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) /\ i e. ( 0 ..^ ( N - M ) ) ) -> ( ( ( F o. W ) substr <. M , N >. ) ` i ) = ( ( F o. W ) ` ( i + M ) ) )
53 38 40 52 3eqtr4d 
 |-  ( ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) /\ i e. ( 0 ..^ ( N - M ) ) ) -> ( ( F o. ( W substr <. M , N >. ) ) ` i ) = ( ( ( F o. W ) substr <. M , N >. ) ` i ) )
54 10 24 53 eqfnfvd 
 |-  ( ( W e. Word A /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ F : A --> B ) -> ( F o. ( W substr <. M , N >. ) ) = ( ( F o. W ) substr <. M , N >. ) )