Metamath Proof Explorer

Theorem ccatcan2d

Description: Cancellation law for concatenation. (Contributed by SN, 6-Sep-2023)

Ref Expression
Hypotheses ccatcan2d.a ⊢ φ → A ∈ Word V
ccatcan2d.b ⊢ φ → B ∈ Word V
ccatcan2d.c ⊢ φ → C ∈ Word V
Assertion ccatcan2d ⊢ φ → A ++ C = B ++ C ↔ A = B

Proof

Step Hyp Ref Expression
1 ccatcan2d.a ⊢ φ → A ∈ Word V
2 ccatcan2d.b ⊢ φ → B ∈ Word V
3 ccatcan2d.c ⊢ φ → C ∈ Word V
4 simpr ⊢ φ ∧ A ++ C = B ++ C → A ++ C = B ++ C
5 lencl ⊢ A ∈ Word V → A ∈ ℕ 0
6 1 5 syl ⊢ φ → A ∈ ℕ 0
7 6 nn0cnd ⊢ φ → A ∈ ℂ
8 7 adantr ⊢ φ ∧ A ++ C = B ++ C → A ∈ ℂ
9 lencl ⊢ B ∈ Word V → B ∈ ℕ 0
10 2 9 syl ⊢ φ → B ∈ ℕ 0
11 10 nn0cnd ⊢ φ → B ∈ ℂ
12 11 adantr ⊢ φ ∧ A ++ C = B ++ C → B ∈ ℂ
13 lencl ⊢ C ∈ Word V → C ∈ ℕ 0
14 3 13 syl ⊢ φ → C ∈ ℕ 0
15 14 nn0cnd ⊢ φ → C ∈ ℂ
16 15 adantr ⊢ φ ∧ A ++ C = B ++ C → C ∈ ℂ
17 ccatlen ⊢ A ∈ Word V ∧ C ∈ Word V → A ++ C = A + C
18 1 3 17 syl2anc ⊢ φ → A ++ C = A + C
19 fveq2 ⊢ A ++ C = B ++ C → A ++ C = B ++ C
20 18 19 sylan9req ⊢ φ ∧ A ++ C = B ++ C → A + C = B ++ C
21 ccatlen ⊢ B ∈ Word V ∧ C ∈ Word V → B ++ C = B + C
22 2 3 21 syl2anc ⊢ φ → B ++ C = B + C
23 22 adantr ⊢ φ ∧ A ++ C = B ++ C → B ++ C = B + C
24 20 23 eqtrd ⊢ φ ∧ A ++ C = B ++ C → A + C = B + C
25 8 12 16 24 addcan2ad ⊢ φ ∧ A ++ C = B ++ C → A = B
26 4 25 oveq12d ⊢ φ ∧ A ++ C = B ++ C → A ++ C prefix A = B ++ C prefix B
27 26 ex ⊢ φ → A ++ C = B ++ C → A ++ C prefix A = B ++ C prefix B
28 pfxccat1 ⊢ A ∈ Word V ∧ C ∈ Word V → A ++ C prefix A = A
29 1 3 28 syl2anc ⊢ φ → A ++ C prefix A = A
30 pfxccat1 ⊢ B ∈ Word V ∧ C ∈ Word V → B ++ C prefix B = B
31 2 3 30 syl2anc ⊢ φ → B ++ C prefix B = B
32 29 31 eqeq12d ⊢ φ → A ++ C prefix A = B ++ C prefix B ↔ A = B
33 27 32 sylibd ⊢ φ → A ++ C = B ++ C → A = B
34 oveq1 ⊢ A = B → A ++ C = B ++ C
35 33 34 impbid1 ⊢ φ → A ++ C = B ++ C ↔ A = B