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∈WordA∧T∈WordB→S++T=∅↔S=∅∧T=∅

Proof

Step Hyp Ref Expression
1 ccatlen ⊢S∈WordA∧T∈WordB→S++T=S+T
2 1 eqeq1d ⊢S∈WordA∧T∈WordB→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∈WordA∧T∈WordB→S++T=0↔S++T=∅
6 lencl ⊢S∈WordA→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∈WordA→S∈ℝ∧0≤S
11 lencl ⊢T∈WordB→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∈WordB→T∈ℝ∧0≤T
16 add20 ⊢S∈ℝ∧0≤S∧T∈ℝ∧0≤T→S+T=0↔S=0∧T=0
17 10 15 16 syl2an ⊢S∈WordA∧T∈WordB→S+T=0↔S=0∧T=0
18 2 5 17 3bitr3d ⊢S∈WordA∧T∈WordB→S++T=∅↔S=0∧T=0
19 hasheq0 ⊢S∈WordA→S=0↔S=∅
20 hasheq0 ⊢T∈WordB→T=0↔T=∅
21 19 20 bi2anan9 ⊢S∈WordA∧T∈WordB→S=0∧T=0↔S=∅∧T=∅
22 18 21 bitrd ⊢S∈WordA∧T∈WordB→S++T=∅↔S=∅∧T=∅