Metamath Proof Explorer

Theorem ccat0

Description: The concatenation of two words is empty iff the two words are empty. (Contributed by AV, 4-Mar-2022) (Revised by JJ, 18-Jan-2024)

Ref Expression
Assertion ccat0 ⊢ S ∈ Word A ∧ T ∈ Word B → S ++ T = ∅ ↔ S = ∅ ∧ T = ∅

Proof

Step Hyp Ref Expression
1 ccatlen ⊢ S ∈ Word A ∧ T ∈ Word B → S ++ T = S + T
2 1 eqeq1d ⊢ S ∈ Word A ∧ T ∈ Word B → S ++ T = 0 ↔ S + T = 0
3 ovex ⊢ S ++ T ∈ V
4 hasheq0 ⊢ S ++ T ∈ V → S ++ T = 0 ↔ S ++ T = ∅
5 3 4 mp1i ⊢ S ∈ Word A ∧ T ∈ Word B → S ++ T = 0 ↔ S ++ T = ∅
6 lencl ⊢ S ∈ Word A → S ∈ ℕ 0
7 nn0re ⊢ S ∈ ℕ 0 → S ∈ ℝ
8 nn0ge0 ⊢ S ∈ ℕ 0 → 0 ≤ S
9 7 8 jca ⊢ S ∈ ℕ 0 → S ∈ ℝ ∧ 0 ≤ S
10 6 9 syl ⊢ S ∈ Word A → S ∈ ℝ ∧ 0 ≤ S
11 lencl ⊢ T ∈ Word B → T ∈ ℕ 0
12 nn0re ⊢ T ∈ ℕ 0 → T ∈ ℝ
13 nn0ge0 ⊢ T ∈ ℕ 0 → 0 ≤ T
14 12 13 jca ⊢ T ∈ ℕ 0 → T ∈ ℝ ∧ 0 ≤ T
15 11 14 syl ⊢ T ∈ Word B → T ∈ ℝ ∧ 0 ≤ T
16 add20 ⊢ S ∈ ℝ ∧ 0 ≤ S ∧ T ∈ ℝ ∧ 0 ≤ T → S + T = 0 ↔ S = 0 ∧ T = 0
17 10 15 16 syl2an ⊢ S ∈ Word A ∧ T ∈ Word B → S + T = 0 ↔ S = 0 ∧ T = 0
18 2 5 17 3bitr3d ⊢ S ∈ Word A ∧ T ∈ Word B → S ++ T = ∅ ↔ S = 0 ∧ T = 0
19 hasheq0 ⊢ S ∈ Word A → S = 0 ↔ S = ∅
20 hasheq0 ⊢ T ∈ Word B → T = 0 ↔ T = ∅
21 19 20 bi2anan9 ⊢ S ∈ Word A ∧ T ∈ Word B → S = 0 ∧ T = 0 ↔ S = ∅ ∧ T = ∅
22 18 21 bitrd ⊢ S ∈ Word A ∧ T ∈ Word B → S ++ T = ∅ ↔ S = ∅ ∧ T = ∅