This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) "> )