Theorem s2co

Description: Mapping a doubleton word by a function. (Contributed by Mario Carneiro, 27-Feb-2016)

	Ref	Expression
Hypotheses	s2co.1	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
	s2co.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
	s2co.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑋 )
Assertion	s2co	⊢ ( 𝜑 → ( 𝐹 ∘ ⟨“ 𝐴 𝐵 ”⟩ ) = ⟨“ ( 𝐹 ‘ 𝐴 ) ( 𝐹 ‘ 𝐵 ) ”⟩ )

Proof

Step	Hyp	Ref	Expression
1		s2co.1	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
2		s2co.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
3		s2co.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑋 )
4		df-s2	⊢ ⟨“ 𝐴 𝐵 ”⟩ = ( ⟨“ 𝐴 ”⟩ ++ ⟨“ 𝐵 ”⟩ )
5	2	s1cld	⊢ ( 𝜑 → ⟨“ 𝐴 ”⟩ ∈ Word 𝑋 )
6		s1co	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝐹 ∘ ⟨“ 𝐴 ”⟩ ) = ⟨“ ( 𝐹 ‘ 𝐴 ) ”⟩ )
7	2 1 6	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘ ⟨“ 𝐴 ”⟩ ) = ⟨“ ( 𝐹 ‘ 𝐴 ) ”⟩ )
8		df-s2	⊢ ⟨“ ( 𝐹 ‘ 𝐴 ) ( 𝐹 ‘ 𝐵 ) ”⟩ = ( ⟨“ ( 𝐹 ‘ 𝐴 ) ”⟩ ++ ⟨“ ( 𝐹 ‘ 𝐵 ) ”⟩ )
9	4 5 3 1 7 8	cats1co	⊢ ( 𝜑 → ( 𝐹 ∘ ⟨“ 𝐴 𝐵 ”⟩ ) = ⟨“ ( 𝐹 ‘ 𝐴 ) ( 𝐹 ‘ 𝐵 ) ”⟩ )