Metamath Proof Explorer

Theorem ccatopth

Description: An opth -like theorem for recovering the two halves of a concatenated word. (Contributed by Mario Carneiro, 1-Oct-2015) (Proof shortened by AV, 12-Oct-2022)

Ref Expression
Assertion ccatopth 
|- ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) -> ( ( A ++ B ) = ( C ++ D ) <-> ( A = C /\ B = D ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( ( A ++ B ) = ( C ++ D ) -> ( ( A ++ B ) prefix ( # ` A ) ) = ( ( C ++ D ) prefix ( # ` A ) ) )
2 pfxccat1 
 |-  ( ( A e. Word X /\ B e. Word X ) -> ( ( A ++ B ) prefix ( # ` A ) ) = A )
3 oveq2 
 |-  ( ( # ` A ) = ( # ` C ) -> ( ( C ++ D ) prefix ( # ` A ) ) = ( ( C ++ D ) prefix ( # ` C ) ) )
4 pfxccat1 
 |-  ( ( C e. Word X /\ D e. Word X ) -> ( ( C ++ D ) prefix ( # ` C ) ) = C )
5 3 4 sylan9eqr 
 |-  ( ( ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) -> ( ( C ++ D ) prefix ( # ` A ) ) = C )
6 2 5 eqeqan12d 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) ) -> ( ( ( A ++ B ) prefix ( # ` A ) ) = ( ( C ++ D ) prefix ( # ` A ) ) <-> A = C ) )
7 1 6 imbitrid 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) ) -> ( ( A ++ B ) = ( C ++ D ) -> A = C ) )
8 7 3impb 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) -> ( ( A ++ B ) = ( C ++ D ) -> A = C ) )
9 simpr 
 |-  ( ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) /\ ( A ++ B ) = ( C ++ D ) ) -> ( A ++ B ) = ( C ++ D ) )
10 simpl3 
 |-  ( ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) /\ ( A ++ B ) = ( C ++ D ) ) -> ( # ` A ) = ( # ` C ) )
11 9 fveq2d 
 |-  ( ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) /\ ( A ++ B ) = ( C ++ D ) ) -> ( # ` ( A ++ B ) ) = ( # ` ( C ++ D ) ) )
12 simpl1 
 |-  ( ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) /\ ( A ++ B ) = ( C ++ D ) ) -> ( A e. Word X /\ B e. Word X ) )
13 ccatlen 
 |-  ( ( A e. Word X /\ B e. Word X ) -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
14 12 13 syl 
 |-  ( ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) /\ ( A ++ B ) = ( C ++ D ) ) -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
15 simpl2 
 |-  ( ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) /\ ( A ++ B ) = ( C ++ D ) ) -> ( C e. Word X /\ D e. Word X ) )
16 ccatlen 
 |-  ( ( C e. Word X /\ D e. Word X ) -> ( # ` ( C ++ D ) ) = ( ( # ` C ) + ( # ` D ) ) )
17 15 16 syl 
 |-  ( ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) /\ ( A ++ B ) = ( C ++ D ) ) -> ( # ` ( C ++ D ) ) = ( ( # ` C ) + ( # ` D ) ) )
18 11 14 17 3eqtr3d 
 |-  ( ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) /\ ( A ++ B ) = ( C ++ D ) ) -> ( ( # ` A ) + ( # ` B ) ) = ( ( # ` C ) + ( # ` D ) ) )
19 10 18 opeq12d 
 |-  ( ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) /\ ( A ++ B ) = ( C ++ D ) ) -> <. ( # ` A ) , ( ( # ` A ) + ( # ` B ) ) >. = <. ( # ` C ) , ( ( # ` C ) + ( # ` D ) ) >. )
20 9 19 oveq12d 
 |-  ( ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) /\ ( A ++ B ) = ( C ++ D ) ) -> ( ( A ++ B ) substr <. ( # ` A ) , ( ( # ` A ) + ( # ` B ) ) >. ) = ( ( C ++ D ) substr <. ( # ` C ) , ( ( # ` C ) + ( # ` D ) ) >. ) )
21 swrdccat2 
 |-  ( ( A e. Word X /\ B e. Word X ) -> ( ( A ++ B ) substr <. ( # ` A ) , ( ( # ` A ) + ( # ` B ) ) >. ) = B )
22 12 21 syl 
 |-  ( ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) /\ ( A ++ B ) = ( C ++ D ) ) -> ( ( A ++ B ) substr <. ( # ` A ) , ( ( # ` A ) + ( # ` B ) ) >. ) = B )
23 swrdccat2 
 |-  ( ( C e. Word X /\ D e. Word X ) -> ( ( C ++ D ) substr <. ( # ` C ) , ( ( # ` C ) + ( # ` D ) ) >. ) = D )
24 15 23 syl 
 |-  ( ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) /\ ( A ++ B ) = ( C ++ D ) ) -> ( ( C ++ D ) substr <. ( # ` C ) , ( ( # ` C ) + ( # ` D ) ) >. ) = D )
25 20 22 24 3eqtr3d 
 |-  ( ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) /\ ( A ++ B ) = ( C ++ D ) ) -> B = D )
26 25 ex 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) -> ( ( A ++ B ) = ( C ++ D ) -> B = D ) )
27 8 26 jcad 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) -> ( ( A ++ B ) = ( C ++ D ) -> ( A = C /\ B = D ) ) )
28 oveq12 
 |-  ( ( A = C /\ B = D ) -> ( A ++ B ) = ( C ++ D ) )
29 27 28 impbid1 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` A ) = ( # ` C ) ) -> ( ( A ++ B ) = ( C ++ D ) <-> ( A = C /\ B = D ) ) )