cats1co

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

Step	Hyp	Ref	Expression
1		cats1cld.1	$⊢ T = S ++ ⟨“ X ”⟩$
2		cats1cld.2	$⊢ φ \to S \in Word A$
3		cats1cld.3	$⊢ φ \to X \in A$
4		cats1co.4	$⊢ φ \to F : A ⟶ B$
5		cats1co.5	$⊢ φ \to F \circ S = U$
6		cats1co.6	$⊢ V = U ++ ⟨“ F (X) ”⟩$
7	3	s1cld	$⊢ φ \to ⟨“ X ”⟩ \in Word A$
8		ccatco	$⊢ (S \in Word A \land ⟨“ X ”⟩ \in Word A \land F : A ⟶ B) \to F \circ (S ++ ⟨“ X ”⟩) = (F \circ S) ++ (F \circ ⟨“ X ”⟩)$
9	2 7 4 8	syl3anc	$⊢ φ \to F \circ (S ++ ⟨“ X ”⟩) = (F \circ S) ++ (F \circ ⟨“ X ”⟩)$
10		s1co	$⊢ (X \in A \land F : A ⟶ B) \to F \circ ⟨“ X ”⟩ = ⟨“ F (X) ”⟩$
11	3 4 10	syl2anc	$⊢ φ \to F \circ ⟨“ X ”⟩ = ⟨“ F (X) ”⟩$
12	5 11	oveq12d	$⊢ φ \to (F \circ S) ++ (F \circ ⟨“ X ”⟩) = U ++ ⟨“ F (X) ”⟩$
13	9 12	eqtrd	$⊢ φ \to F \circ (S ++ ⟨“ X ”⟩) = U ++ ⟨“ F (X) ”⟩$
14	1	coeq2i	$⊢ F \circ T = F \circ (S ++ ⟨“ X ”⟩)$
15	13 14 6	3eqtr4g	$⊢ φ \to F \circ T = V$

Metamath Proof Explorer