Metamath Proof Explorer

Theorem ofcs2

Description: Letterwise operations on a double letter word. (Contributed by Thierry Arnoux, 9-Oct-2018)

Ref Expression
Assertion ofcs2 
|- ( ( A e. S /\ B e. S /\ C e. T ) -> ( <" A B "> oFC R C ) = <" ( A R C ) ( B R C ) "> )

Proof

Step Hyp Ref Expression
1 df-s2 
 |-  <" A B "> = ( <" A "> ++ <" B "> )
2 1 oveq1i 
 |-  ( <" A B "> oFC R C ) = ( ( <" A "> ++ <" B "> ) oFC R C )
3 simp1 
 |-  ( ( A e. S /\ B e. S /\ C e. T ) -> A e. S )
4 3 s1cld 
 |-  ( ( A e. S /\ B e. S /\ C e. T ) -> <" A "> e. Word S )
5 simp2 
 |-  ( ( A e. S /\ B e. S /\ C e. T ) -> B e. S )
6 5 s1cld 
 |-  ( ( A e. S /\ B e. S /\ C e. T ) -> <" B "> e. Word S )
7 simp3 
 |-  ( ( A e. S /\ B e. S /\ C e. T ) -> C e. T )
8 4 6 7 ofcccat 
 |-  ( ( A e. S /\ B e. S /\ C e. T ) -> ( ( <" A "> ++ <" B "> ) oFC R C ) = ( ( <" A "> oFC R C ) ++ ( <" B "> oFC R C ) ) )
9 2 8 syl5eq 
 |-  ( ( A e. S /\ B e. S /\ C e. T ) -> ( <" A B "> oFC R C ) = ( ( <" A "> oFC R C ) ++ ( <" B "> oFC R C ) ) )
10 ofcs1 
 |-  ( ( A e. S /\ C e. T ) -> ( <" A "> oFC R C ) = <" ( A R C ) "> )
11 3 7 10 syl2anc 
 |-  ( ( A e. S /\ B e. S /\ C e. T ) -> ( <" A "> oFC R C ) = <" ( A R C ) "> )
12 ofcs1 
 |-  ( ( B e. S /\ C e. T ) -> ( <" B "> oFC R C ) = <" ( B R C ) "> )
13 5 7 12 syl2anc 
 |-  ( ( A e. S /\ B e. S /\ C e. T ) -> ( <" B "> oFC R C ) = <" ( B R C ) "> )
14 11 13 oveq12d 
 |-  ( ( A e. S /\ B e. S /\ C e. T ) -> ( ( <" A "> oFC R C ) ++ ( <" B "> oFC R C ) ) = ( <" ( A R C ) "> ++ <" ( B R C ) "> ) )
15 df-s2 
 |-  <" ( A R C ) ( B R C ) "> = ( <" ( A R C ) "> ++ <" ( B R C ) "> )
16 14 15 eqtr4di 
 |-  ( ( A e. S /\ B e. S /\ C e. T ) -> ( ( <" A "> oFC R C ) ++ ( <" B "> oFC R C ) ) = <" ( A R C ) ( B R C ) "> )
17 9 16 eqtrd 
 |-  ( ( A e. S /\ B e. S /\ C e. T ) -> ( <" A B "> oFC R C ) = <" ( A R C ) ( B R C ) "> )