Metamath Proof Explorer

Theorem ofs2

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

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

Proof

Step Hyp Ref Expression
1 df-s2 
 |-  <" A B "> = ( <" A "> ++ <" B "> )
2 df-s2 
 |-  <" C D "> = ( <" C "> ++ <" D "> )
3 1 2 oveq12i 
 |-  ( <" A B "> oF R <" C D "> ) = ( ( <" A "> ++ <" B "> ) oF R ( <" C "> ++ <" D "> ) )
4 simpll 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. T /\ D e. T ) ) -> A e. S )
5 4 s1cld 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. T /\ D e. T ) ) -> <" A "> e. Word S )
6 simplr 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. T /\ D e. T ) ) -> B e. S )
7 6 s1cld 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. T /\ D e. T ) ) -> <" B "> e. Word S )
8 simprl 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. T /\ D e. T ) ) -> C e. T )
9 8 s1cld 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. T /\ D e. T ) ) -> <" C "> e. Word T )
10 simprr 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. T /\ D e. T ) ) -> D e. T )
11 10 s1cld 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. T /\ D e. T ) ) -> <" D "> e. Word T )
12 s1len 
 |-  ( # ` <" A "> ) = 1
13 s1len 
 |-  ( # ` <" C "> ) = 1
14 12 13 eqtr4i 
 |-  ( # ` <" A "> ) = ( # ` <" C "> )
15 14 a1i 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. T /\ D e. T ) ) -> ( # ` <" A "> ) = ( # ` <" C "> ) )
16 s1len 
 |-  ( # ` <" B "> ) = 1
17 s1len 
 |-  ( # ` <" D "> ) = 1
18 16 17 eqtr4i 
 |-  ( # ` <" B "> ) = ( # ` <" D "> )
19 18 a1i 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. T /\ D e. T ) ) -> ( # ` <" B "> ) = ( # ` <" D "> ) )
20 5 7 9 11 15 19 ofccat 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. T /\ D e. T ) ) -> ( ( <" A "> ++ <" B "> ) oF R ( <" C "> ++ <" D "> ) ) = ( ( <" A "> oF R <" C "> ) ++ ( <" B "> oF R <" D "> ) ) )
21 3 20 eqtrid 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. T /\ D e. T ) ) -> ( <" A B "> oF R <" C D "> ) = ( ( <" A "> oF R <" C "> ) ++ ( <" B "> oF R <" D "> ) ) )
22 ofs1 
 |-  ( ( A e. S /\ C e. T ) -> ( <" A "> oF R <" C "> ) = <" ( A R C ) "> )
23 4 8 22 syl2anc 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. T /\ D e. T ) ) -> ( <" A "> oF R <" C "> ) = <" ( A R C ) "> )
24 ofs1 
 |-  ( ( B e. S /\ D e. T ) -> ( <" B "> oF R <" D "> ) = <" ( B R D ) "> )
25 6 10 24 syl2anc 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. T /\ D e. T ) ) -> ( <" B "> oF R <" D "> ) = <" ( B R D ) "> )
26 23 25 oveq12d 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. T /\ D e. T ) ) -> ( ( <" A "> oF R <" C "> ) ++ ( <" B "> oF R <" D "> ) ) = ( <" ( A R C ) "> ++ <" ( B R D ) "> ) )
27 df-s2 
 |-  <" ( A R C ) ( B R D ) "> = ( <" ( A R C ) "> ++ <" ( B R D ) "> )
28 26 27 eqtr4di 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. T /\ D e. T ) ) -> ( ( <" A "> oF R <" C "> ) ++ ( <" B "> oF R <" D "> ) ) = <" ( A R C ) ( B R D ) "> )
29 21 28 eqtrd 
 |-  ( ( ( A e. S /\ B e. S ) /\ ( C e. T /\ D e. T ) ) -> ( <" A B "> oF R <" C D "> ) = <" ( A R C ) ( B R D ) "> )