Metamath Proof Explorer


Theorem cats1co

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

Ref Expression
Hypotheses cats1cld.1
|- T = ( S ++ <" X "> )
cats1cld.2
|- ( ph -> S e. Word A )
cats1cld.3
|- ( ph -> X e. A )
cats1co.4
|- ( ph -> F : A --> B )
cats1co.5
|- ( ph -> ( F o. S ) = U )
cats1co.6
|- V = ( U ++ <" ( F ` X ) "> )
Assertion cats1co
|- ( ph -> ( F o. T ) = V )

Proof

Step Hyp Ref Expression
1 cats1cld.1
 |-  T = ( S ++ <" X "> )
2 cats1cld.2
 |-  ( ph -> S e. Word A )
3 cats1cld.3
 |-  ( ph -> X e. A )
4 cats1co.4
 |-  ( ph -> F : A --> B )
5 cats1co.5
 |-  ( ph -> ( F o. S ) = U )
6 cats1co.6
 |-  V = ( U ++ <" ( F ` X ) "> )
7 3 s1cld
 |-  ( ph -> <" X "> e. Word A )
8 ccatco
 |-  ( ( S e. Word A /\ <" X "> e. Word A /\ F : A --> B ) -> ( F o. ( S ++ <" X "> ) ) = ( ( F o. S ) ++ ( F o. <" X "> ) ) )
9 2 7 4 8 syl3anc
 |-  ( ph -> ( F o. ( S ++ <" X "> ) ) = ( ( F o. S ) ++ ( F o. <" X "> ) ) )
10 s1co
 |-  ( ( X e. A /\ F : A --> B ) -> ( F o. <" X "> ) = <" ( F ` X ) "> )
11 3 4 10 syl2anc
 |-  ( ph -> ( F o. <" X "> ) = <" ( F ` X ) "> )
12 5 11 oveq12d
 |-  ( ph -> ( ( F o. S ) ++ ( F o. <" X "> ) ) = ( U ++ <" ( F ` X ) "> ) )
13 9 12 eqtrd
 |-  ( ph -> ( F o. ( S ++ <" X "> ) ) = ( U ++ <" ( F ` X ) "> ) )
14 1 coeq2i
 |-  ( F o. T ) = ( F o. ( S ++ <" X "> ) )
15 13 14 6 3eqtr4g
 |-  ( ph -> ( F o. T ) = V )