Metamath Proof Explorer


Theorem s3co

Description: Mapping a length 3 string by a function. (Contributed by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses s2co.1
|- ( ph -> F : X --> Y )
s2co.2
|- ( ph -> A e. X )
s2co.3
|- ( ph -> B e. X )
s3co.4
|- ( ph -> C e. X )
Assertion s3co
|- ( ph -> ( F o. <" A B C "> ) = <" ( F ` A ) ( F ` B ) ( F ` C ) "> )

Proof

Step Hyp Ref Expression
1 s2co.1
 |-  ( ph -> F : X --> Y )
2 s2co.2
 |-  ( ph -> A e. X )
3 s2co.3
 |-  ( ph -> B e. X )
4 s3co.4
 |-  ( ph -> C e. X )
5 df-s3
 |-  <" A B C "> = ( <" A B "> ++ <" C "> )
6 2 3 s2cld
 |-  ( ph -> <" A B "> e. Word X )
7 1 2 3 s2co
 |-  ( ph -> ( F o. <" A B "> ) = <" ( F ` A ) ( F ` B ) "> )
8 df-s3
 |-  <" ( F ` A ) ( F ` B ) ( F ` C ) "> = ( <" ( F ` A ) ( F ` B ) "> ++ <" ( F ` C ) "> )
9 5 6 4 1 7 8 cats1co
 |-  ( ph -> ( F o. <" A B C "> ) = <" ( F ` A ) ( F ` B ) ( F ` C ) "> )