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

Metamath Proof Explorer

Theorem wrdco

Description: Mapping a word by a function. (Contributed by Stefan O'Rear, 27-Aug-2015)

Ref Expression
Assertion wrdco ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝑊 ) ∈ Word 𝐵 )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
2 wrdf ⊢ ( 𝑊 ∈ Word 𝐴 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )
3 2 adantr ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )
4 fco ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 ) → ( 𝐹 ∘ 𝑊 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐵 )
5 1 3 4 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝑊 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐵 )
6 iswrdi ⊢ ( ( 𝐹 ∘ 𝑊 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐵 → ( 𝐹 ∘ 𝑊 ) ∈ Word 𝐵 )
7 5 6 syl ⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝑊 ) ∈ Word 𝐵 )