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 𝐵 )