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