Metamath Proof Explorer

Theorem pfxco

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

Ref Expression
Assertion pfxco ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( 𝑊 prefix 𝑁 ) ) = ( ( 𝐹 ∘ 𝑊 ) prefix 𝑁 ) )

Proof

Step Hyp Ref Expression
1 elfznn0 ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑁 ∈ ℕ0 )
2 1 3ad2ant2 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝑁 ∈ ℕ0 )
3 0elfz ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
4 2 3 syl ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 0 ∈ ( 0 ... 𝑁 ) )
5 simp2 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
6 4 5 jca ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) )
7 swrdco ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ ( 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( 𝑊 substr ⟨ 0 , 𝑁 ⟩ ) ) = ( ( 𝐹 ∘ 𝑊 ) substr ⟨ 0 , 𝑁 ⟩ ) )
8 6 7 syld3an2 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( 𝑊 substr ⟨ 0 , 𝑁 ⟩ ) ) = ( ( 𝐹 ∘ 𝑊 ) substr ⟨ 0 , 𝑁 ⟩ ) )
9 pfxval ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 prefix 𝑁 ) = ( 𝑊 substr ⟨ 0 , 𝑁 ⟩ ) )
10 1 9 sylan2 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 prefix 𝑁 ) = ( 𝑊 substr ⟨ 0 , 𝑁 ⟩ ) )
11 10 coeq2d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝐹 ∘ ( 𝑊 prefix 𝑁 ) ) = ( 𝐹 ∘ ( 𝑊 substr ⟨ 0 , 𝑁 ⟩ ) ) )
12 11 3adant3 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( 𝑊 prefix 𝑁 ) ) = ( 𝐹 ∘ ( 𝑊 substr ⟨ 0 , 𝑁 ⟩ ) ) )
13 ffun ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → Fun 𝐹 )
14 13 anim2i ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝑊 ∈ Word 𝐴 ∧ Fun 𝐹 ) )
15 14 ancomd ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( Fun 𝐹 ∧ 𝑊 ∈ Word 𝐴 ) )
16 15 3adant2 ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( Fun 𝐹 ∧ 𝑊 ∈ Word 𝐴 ) )
17 cofunexg ⊢ ( ( Fun 𝐹 ∧ 𝑊 ∈ Word 𝐴 ) → ( 𝐹 ∘ 𝑊 ) ∈ V )
18 16 17 syl ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝑊 ) ∈ V )
19 18 2 jca ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( 𝐹 ∘ 𝑊 ) ∈ V ∧ 𝑁 ∈ ℕ0 ) )
20 pfxval ⊢ ( ( ( 𝐹 ∘ 𝑊 ) ∈ V ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐹 ∘ 𝑊 ) prefix 𝑁 ) = ( ( 𝐹 ∘ 𝑊 ) substr ⟨ 0 , 𝑁 ⟩ ) )
21 19 20 syl ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( 𝐹 ∘ 𝑊 ) prefix 𝑁 ) = ( ( 𝐹 ∘ 𝑊 ) substr ⟨ 0 , 𝑁 ⟩ ) )
22 8 12 21 3eqtr4d ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( 𝑊 prefix 𝑁 ) ) = ( ( 𝐹 ∘ 𝑊 ) prefix 𝑁 ) )