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 ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ 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 ∈ Word X ∧ B ∈ Word X → A ++ B prefix A = A
3 oveq2 ⊢ A = C → C ++ D prefix A = C ++ D prefix C
4 pfxccat1 ⊢ C ∈ Word X ∧ D ∈ Word X → C ++ D prefix C = C
5 3 4 sylan9eqr ⊢ C ∈ Word X ∧ D ∈ Word X ∧ A = C → C ++ D prefix A = C
6 2 5 eqeqan12d ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C → A ++ B prefix A = C ++ D prefix A ↔ A = C
7 1 6 imbitrid ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C → A ++ B = C ++ D → A = C
8 7 3impb ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C → A ++ B = C ++ D → A = C
9 simpr ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C ∧ A ++ B = C ++ D → A ++ B = C ++ D
10 simpl3 ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C ∧ A ++ B = C ++ D → A = C
11 9 fveq2d ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C ∧ A ++ B = C ++ D → A ++ B = C ++ D
12 simpl1 ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C ∧ A ++ B = C ++ D → A ∈ Word X ∧ B ∈ Word X
13 ccatlen ⊢ A ∈ Word X ∧ B ∈ Word X → A ++ B = A + B
14 12 13 syl ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C ∧ A ++ B = C ++ D → A ++ B = A + B
15 simpl2 ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C ∧ A ++ B = C ++ D → C ∈ Word X ∧ D ∈ Word X
16 ccatlen ⊢ C ∈ Word X ∧ D ∈ Word X → C ++ D = C + D
17 15 16 syl ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C ∧ A ++ B = C ++ D → C ++ D = C + D
18 11 14 17 3eqtr3d ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C ∧ A ++ B = C ++ D → A + B = C + D
19 10 18 opeq12d ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C ∧ A ++ B = C ++ D → A A + B = C C + D
20 9 19 oveq12d ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C ∧ A ++ B = C ++ D → A ++ B substr A A + B = C ++ D substr C C + D
21 swrdccat2 ⊢ A ∈ Word X ∧ B ∈ Word X → A ++ B substr A A + B = B
22 12 21 syl ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C ∧ A ++ B = C ++ D → A ++ B substr A A + B = B
23 swrdccat2 ⊢ C ∈ Word X ∧ D ∈ Word X → C ++ D substr C C + D = D
24 15 23 syl ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C ∧ A ++ B = C ++ D → C ++ D substr C C + D = D
25 20 22 24 3eqtr3d ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C ∧ A ++ B = C ++ D → B = D
26 25 ex ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C → A ++ B = C ++ D → B = D
27 8 26 jcad ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ 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 ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C → A ++ B = C ++ D ↔ A = C ∧ B = D