Metamath Proof Explorer

Theorem swrdco

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

Ref Expression
Assertion swrdco ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( ( 𝐹 ∘ 𝑊 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) )

Proof

Step Hyp Ref Expression
1 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
2 1 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 Fn 𝐴 )
3 swrdvalfn ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) Fn ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
4 3 3expb ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) Fn ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
5 4 3adant3 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) Fn ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
6 swrdrn ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ran ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ⊆ 𝐴 )
7 6 3expb ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) → ran ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ⊆ 𝐴 )
8 7 3adant3 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ran ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ⊆ 𝐴 )
9 fnco ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) Fn ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ran ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ⊆ 𝐴 ) → ( 𝐹 ∘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) Fn ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
10 2 5 8 9 syl3anc ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) Fn ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
11 wrdco ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝑊 ) ∈ Word 𝐵 )
12 11 3adant2 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝑊 ) ∈ Word 𝐵 )
13 simp2l ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝑀 ∈ ( 0 ... 𝑁 ) )
14 lenco ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) = ( ♯ ‘ 𝑊 ) )
15 14 eqcomd ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) )
16 15 oveq2d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 0 ... ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) )
17 16 eleq2d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) )
18 17 biimpd ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) )
19 18 expcom ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝑊 ∈ Word 𝐴 → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) ) )
20 19 com13 ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ∈ Word 𝐴 → ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) ) )
21 20 adantl ⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ∈ Word 𝐴 → ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) ) )
22 21 3imp21 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) )
23 swrdvalfn ⊢ ( ( ( 𝐹 ∘ 𝑊 ) ∈ Word 𝐵 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) → ( ( 𝐹 ∘ 𝑊 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) Fn ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
24 12 13 22 23 syl3anc ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( 𝐹 ∘ 𝑊 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) Fn ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
25 3anass ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ↔ ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) )
26 25 biimpri ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ) → ( 𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) )
27 26 3adant3 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) )
28 swrdfv ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) )
29 28 fveq2d ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝐹 ‘ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) ) = ( 𝐹 ‘ ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) ) )
30 27 29 sylan ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝐹 ‘ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) ) = ( 𝐹 ‘ ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) ) )
31 wrdfn ⊢ ( 𝑊 ∈ Word 𝐴 → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
32 31 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
33 elfzodifsumelfzo ⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) → ( 𝑖 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
34 33 3ad2ant2 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) → ( 𝑖 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
35 34 imp ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝑖 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
36 fvco2 ⊢ ( ( 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑖 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐹 ∘ 𝑊 ) ‘ ( 𝑖 + 𝑀 ) ) = ( 𝐹 ‘ ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) ) )
37 32 35 36 syl2an2r ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( 𝐹 ∘ 𝑊 ) ‘ ( 𝑖 + 𝑀 ) ) = ( 𝐹 ‘ ( 𝑊 ‘ ( 𝑖 + 𝑀 ) ) ) )
38 30 37 eqtr4d ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝐹 ‘ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝑊 ) ‘ ( 𝑖 + 𝑀 ) ) )
39 fvco2 ⊢ ( ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) Fn ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( 𝐹 ∘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ‘ 𝑖 ) = ( 𝐹 ‘ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) ) )
40 5 39 sylan ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( 𝐹 ∘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ‘ 𝑖 ) = ( 𝐹 ‘ ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) ) )
41 14 ancoms ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑊 ∈ Word 𝐴 ) → ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) = ( ♯ ‘ 𝑊 ) )
42 41 eqcomd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑊 ∈ Word 𝐴 ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) )
43 42 oveq2d ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑊 ∈ Word 𝐴 ) → ( 0 ... ( ♯ ‘ 𝑊 ) ) = ( 0 ... ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) )
44 43 eleq2d ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑊 ∈ Word 𝐴 ) → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) )
45 44 biimpd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑊 ∈ Word 𝐴 ) → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) )
46 45 ex ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝑊 ∈ Word 𝐴 → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) ) )
47 46 com13 ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ∈ Word 𝐴 → ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) ) )
48 47 adantl ⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ∈ Word 𝐴 → ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) ) )
49 48 3imp21 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) )
50 12 13 49 3jca ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( 𝐹 ∘ 𝑊 ) ∈ Word 𝐵 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) )
51 swrdfv ⊢ ( ( ( ( 𝐹 ∘ 𝑊 ) ∈ Word 𝐵 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐹 ∘ 𝑊 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( ( 𝐹 ∘ 𝑊 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝐹 ∘ 𝑊 ) ‘ ( 𝑖 + 𝑀 ) ) )
52 50 51 sylan ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( ( 𝐹 ∘ 𝑊 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) = ( ( 𝐹 ∘ 𝑊 ) ‘ ( 𝑖 + 𝑀 ) ) )
53 38 40 52 3eqtr4d ⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( 𝐹 ∘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ‘ 𝑖 ) = ( ( ( 𝐹 ∘ 𝑊 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑖 ) )
54 10 24 53 eqfnfvd ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) = ( ( 𝐹 ∘ 𝑊 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) )