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 ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ 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 ∈ Word X ∧ B ∈ Word X → A ++ B = A + B
3 2 3ad2ant1 ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → A ++ B = A + B
4 simp3 ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → B = D
5 4 oveq2d ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → A + B = A + D
6 3 5 eqtrd ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → A ++ B = A + D
7 ccatlen ⊢ C ∈ Word X ∧ D ∈ Word X → C ++ D = C + D
8 7 3ad2ant2 ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → C ++ D = C + D
9 6 8 eqeq12d ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → A ++ B = C ++ D ↔ A + D = C + D
10 simp1l ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → A ∈ Word X
11 lencl ⊢ A ∈ Word X → A ∈ ℕ 0
12 10 11 syl ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → A ∈ ℕ 0
13 12 nn0cnd ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → A ∈ ℂ
14 simp2l ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → C ∈ Word X
15 lencl ⊢ C ∈ Word X → C ∈ ℕ 0
16 14 15 syl ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → C ∈ ℕ 0
17 16 nn0cnd ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → C ∈ ℂ
18 simp2r ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → D ∈ Word X
19 lencl ⊢ D ∈ Word X → D ∈ ℕ 0
20 18 19 syl ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → D ∈ ℕ 0
21 20 nn0cnd ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → D ∈ ℂ
22 13 17 21 addcan2d ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → A + D = C + D ↔ A = C
23 9 22 bitrd ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → A ++ B = C ++ D ↔ A = C
24 1 23 imbitrid ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → A ++ B = C ++ D → A = C
25 ccatopth ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C → A ++ B = C ++ D ↔ A = C ∧ B = D
26 25 biimpd ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ A = C → A ++ B = C ++ D → A = C ∧ B = D
27 26 3expia ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X → A = C → A ++ B = C ++ D → A = C ∧ B = D
28 27 com23 ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X → A ++ B = C ++ D → A = C → A = C ∧ B = D
29 28 3adant3 ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → A ++ B = C ++ D → A = C → A = C ∧ B = D
30 24 29 mpdd ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ 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 ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ D ∈ Word X ∧ B = D → A ++ B = C ++ D ↔ A = C ∧ B = D