# Metamath Proof Explorer

## Theorem wrdco

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

Ref Expression
Assertion wrdco ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to {F}\circ {W}\in \mathrm{Word}{B}$

### Proof

Step Hyp Ref Expression
1 simpr ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to {F}:{A}⟶{B}$
2 wrdf ${⊢}{W}\in \mathrm{Word}{A}\to {W}:\left(0..^\left|{W}\right|\right)⟶{A}$
3 2 adantr ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to {W}:\left(0..^\left|{W}\right|\right)⟶{A}$
4 fco ${⊢}\left({F}:{A}⟶{B}\wedge {W}:\left(0..^\left|{W}\right|\right)⟶{A}\right)\to \left({F}\circ {W}\right):\left(0..^\left|{W}\right|\right)⟶{B}$
5 1 3 4 syl2anc ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to \left({F}\circ {W}\right):\left(0..^\left|{W}\right|\right)⟶{B}$
6 iswrdi ${⊢}\left({F}\circ {W}\right):\left(0..^\left|{W}\right|\right)⟶{B}\to {F}\circ {W}\in \mathrm{Word}{B}$
7 5 6 syl ${⊢}\left({W}\in \mathrm{Word}{A}\wedge {F}:{A}⟶{B}\right)\to {F}\circ {W}\in \mathrm{Word}{B}$