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 )