Theorem cats1co

Description: Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Hypotheses	cats1cld.1	⊢ 𝑇 = ( 𝑆 ++ ⟨“ 𝑋 ”⟩ )
	cats1cld.2	⊢ ( 𝜑 → 𝑆 ∈ Word 𝐴 )
	cats1cld.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	cats1co.4	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	cats1co.5	⊢ ( 𝜑 → ( 𝐹 ∘ 𝑆 ) = 𝑈 )
	cats1co.6	⊢ 𝑉 = ( 𝑈 ++ ⟨“ ( 𝐹 ‘ 𝑋 ) ”⟩ )
Assertion	cats1co	⊢ ( 𝜑 → ( 𝐹 ∘ 𝑇 ) = 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		cats1cld.1	⊢ 𝑇 = ( 𝑆 ++ ⟨“ 𝑋 ”⟩ )
2		cats1cld.2	⊢ ( 𝜑 → 𝑆 ∈ Word 𝐴 )
3		cats1cld.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
4		cats1co.4	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
5		cats1co.5	⊢ ( 𝜑 → ( 𝐹 ∘ 𝑆 ) = 𝑈 )
6		cats1co.6	⊢ 𝑉 = ( 𝑈 ++ ⟨“ ( 𝐹 ‘ 𝑋 ) ”⟩ )
7	3	s1cld	⊢ ( 𝜑 → ⟨“ 𝑋 ”⟩ ∈ Word 𝐴 )
8		ccatco	⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) ) = ( ( 𝐹 ∘ 𝑆 ) ++ ( 𝐹 ∘ ⟨“ 𝑋 ”⟩ ) ) )
9	2 7 4 8	syl3anc	⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) ) = ( ( 𝐹 ∘ 𝑆 ) ++ ( 𝐹 ∘ ⟨“ 𝑋 ”⟩ ) ) )
10		s1co	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ⟨“ 𝑋 ”⟩ ) = ⟨“ ( 𝐹 ‘ 𝑋 ) ”⟩ )
11	3 4 10	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘ ⟨“ 𝑋 ”⟩ ) = ⟨“ ( 𝐹 ‘ 𝑋 ) ”⟩ )
12	5 11	oveq12d	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝑆 ) ++ ( 𝐹 ∘ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑈 ++ ⟨“ ( 𝐹 ‘ 𝑋 ) ”⟩ ) )
13	9 12	eqtrd	⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) ) = ( 𝑈 ++ ⟨“ ( 𝐹 ‘ 𝑋 ) ”⟩ ) )
14	1	coeq2i	⊢ ( 𝐹 ∘ 𝑇 ) = ( 𝐹 ∘ ( 𝑆 ++ ⟨“ 𝑋 ”⟩ ) )
15	13 14 6	3eqtr4g	⊢ ( 𝜑 → ( 𝐹 ∘ 𝑇 ) = 𝑉 )