Metamath Proof Explorer

Theorem ccatopth2

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

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

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( ( A ++ B ) = ( C ++ D ) -> ( # ` ( A ++ B ) ) = ( # ` ( C ++ D ) ) )
2 ccatlen 
 |-  ( ( A e. Word X /\ B e. Word X ) -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
3 2 3ad2ant1 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
4 simp3 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> ( # ` B ) = ( # ` D ) )
5 4 oveq2d 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> ( ( # ` A ) + ( # ` B ) ) = ( ( # ` A ) + ( # ` D ) ) )
6 3 5 eqtrd 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` D ) ) )
7 ccatlen 
 |-  ( ( C e. Word X /\ D e. Word X ) -> ( # ` ( C ++ D ) ) = ( ( # ` C ) + ( # ` D ) ) )
8 7 3ad2ant2 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> ( # ` ( C ++ D ) ) = ( ( # ` C ) + ( # ` D ) ) )
9 6 8 eqeq12d 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> ( ( # ` ( A ++ B ) ) = ( # ` ( C ++ D ) ) <-> ( ( # ` A ) + ( # ` D ) ) = ( ( # ` C ) + ( # ` D ) ) ) )
10 simp1l 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> A e. Word X )
11 lencl 
 |-  ( A e. Word X -> ( # ` A ) e. NN0 )
12 10 11 syl 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> ( # ` A ) e. NN0 )
13 12 nn0cnd 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> ( # ` A ) e. CC )
14 simp2l 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> C e. Word X )
15 lencl 
 |-  ( C e. Word X -> ( # ` C ) e. NN0 )
16 14 15 syl 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> ( # ` C ) e. NN0 )
17 16 nn0cnd 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> ( # ` C ) e. CC )
18 simp2r 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> D e. Word X )
19 lencl 
 |-  ( D e. Word X -> ( # ` D ) e. NN0 )
20 18 19 syl 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> ( # ` D ) e. NN0 )
21 20 nn0cnd 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> ( # ` D ) e. CC )
22 13 17 21 addcan2d 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> ( ( ( # ` A ) + ( # ` D ) ) = ( ( # ` C ) + ( # ` D ) ) <-> ( # ` A ) = ( # ` C ) ) )
23 9 22 bitrd 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> ( ( # ` ( A ++ B ) ) = ( # ` ( C ++ D ) ) <-> ( # ` A ) = ( # ` C ) ) )
24 1 23 syl5ib 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> ( ( A ++ B ) = ( C ++ D ) -> ( # ` A ) = ( # ` C ) ) )
25 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 ) ) )
26 25 biimpd 
 |-  ( ( ( 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 ) ) )
27 26 3expia 
 |-  ( ( ( 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 27 com23 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) ) -> ( ( A ++ B ) = ( C ++ D ) -> ( ( # ` A ) = ( # ` C ) -> ( A = C /\ B = D ) ) ) )
29 28 3adant3 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> ( ( A ++ B ) = ( C ++ D ) -> ( ( # ` A ) = ( # ` C ) -> ( A = C /\ B = D ) ) ) )
30 24 29 mpdd 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> ( ( A ++ B ) = ( C ++ D ) -> ( A = C /\ B = D ) ) )
31 oveq12 
 |-  ( ( A = C /\ B = D ) -> ( A ++ B ) = ( C ++ D ) )
32 30 31 impbid1 
 |-  ( ( ( A e. Word X /\ B e. Word X ) /\ ( C e. Word X /\ D e. Word X ) /\ ( # ` B ) = ( # ` D ) ) -> ( ( A ++ B ) = ( C ++ D ) <-> ( A = C /\ B = D ) ) )