Metamath Proof Explorer

Theorem s3eqs2s1eq

Description: Two length 3 words are equal iff the corresponding length 2 words and singleton words consisting of their symbols are equal. (Contributed by AV, 4-Jan-2022)

Ref Expression
Assertion s3eqs2s1eq 
|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( D e. V /\ E e. V /\ F e. V ) ) -> ( <" A B C "> = <" D E F "> <-> ( <" A B "> = <" D E "> /\ <" C "> = <" F "> ) ) )

Proof

Step Hyp Ref Expression
1 df-s3 
 |-  <" A B C "> = ( <" A B "> ++ <" C "> )
2 1 a1i 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( D e. V /\ E e. V /\ F e. V ) ) -> <" A B C "> = ( <" A B "> ++ <" C "> ) )
3 df-s3 
 |-  <" D E F "> = ( <" D E "> ++ <" F "> )
4 3 a1i 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( D e. V /\ E e. V /\ F e. V ) ) -> <" D E F "> = ( <" D E "> ++ <" F "> ) )
5 2 4 eqeq12d 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( D e. V /\ E e. V /\ F e. V ) ) -> ( <" A B C "> = <" D E F "> <-> ( <" A B "> ++ <" C "> ) = ( <" D E "> ++ <" F "> ) ) )
6 s2cl 
 |-  ( ( A e. V /\ B e. V ) -> <" A B "> e. Word V )
7 s1cl 
 |-  ( C e. V -> <" C "> e. Word V )
8 6 7 anim12i 
 |-  ( ( ( A e. V /\ B e. V ) /\ C e. V ) -> ( <" A B "> e. Word V /\ <" C "> e. Word V ) )
9 8 3impa 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( <" A B "> e. Word V /\ <" C "> e. Word V ) )
10 9 adantr 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( D e. V /\ E e. V /\ F e. V ) ) -> ( <" A B "> e. Word V /\ <" C "> e. Word V ) )
11 s2cl 
 |-  ( ( D e. V /\ E e. V ) -> <" D E "> e. Word V )
12 s1cl 
 |-  ( F e. V -> <" F "> e. Word V )
13 11 12 anim12i 
 |-  ( ( ( D e. V /\ E e. V ) /\ F e. V ) -> ( <" D E "> e. Word V /\ <" F "> e. Word V ) )
14 13 3impa 
 |-  ( ( D e. V /\ E e. V /\ F e. V ) -> ( <" D E "> e. Word V /\ <" F "> e. Word V ) )
15 14 adantl 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( D e. V /\ E e. V /\ F e. V ) ) -> ( <" D E "> e. Word V /\ <" F "> e. Word V ) )
16 s2len 
 |-  ( # ` <" A B "> ) = 2
17 s2len 
 |-  ( # ` <" D E "> ) = 2
18 16 17 eqtr4i 
 |-  ( # ` <" A B "> ) = ( # ` <" D E "> )
19 18 a1i 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( D e. V /\ E e. V /\ F e. V ) ) -> ( # ` <" A B "> ) = ( # ` <" D E "> ) )
20 ccatopth 
 |-  ( ( ( <" A B "> e. Word V /\ <" C "> e. Word V ) /\ ( <" D E "> e. Word V /\ <" F "> e. Word V ) /\ ( # ` <" A B "> ) = ( # ` <" D E "> ) ) -> ( ( <" A B "> ++ <" C "> ) = ( <" D E "> ++ <" F "> ) <-> ( <" A B "> = <" D E "> /\ <" C "> = <" F "> ) ) )
21 10 15 19 20 syl3anc 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( D e. V /\ E e. V /\ F e. V ) ) -> ( ( <" A B "> ++ <" C "> ) = ( <" D E "> ++ <" F "> ) <-> ( <" A B "> = <" D E "> /\ <" C "> = <" F "> ) ) )
22 5 21 bitrd 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( D e. V /\ E e. V /\ F e. V ) ) -> ( <" A B C "> = <" D E F "> <-> ( <" A B "> = <" D E "> /\ <" C "> = <" F "> ) ) )