# 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 ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{B}\right)\to \left({S}\mathrm{++}{T}=\varnothing ↔\left({S}=\varnothing \wedge {T}=\varnothing \right)\right)$

### Proof

Step Hyp Ref Expression
1 ccatlen ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{B}\right)\to \left|{S}\mathrm{++}{T}\right|=\left|{S}\right|+\left|{T}\right|$
2 1 eqeq1d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{B}\right)\to \left(\left|{S}\mathrm{++}{T}\right|=0↔\left|{S}\right|+\left|{T}\right|=0\right)$
3 ovex ${⊢}{S}\mathrm{++}{T}\in \mathrm{V}$
4 hasheq0 ${⊢}{S}\mathrm{++}{T}\in \mathrm{V}\to \left(\left|{S}\mathrm{++}{T}\right|=0↔{S}\mathrm{++}{T}=\varnothing \right)$
5 3 4 mp1i ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{B}\right)\to \left(\left|{S}\mathrm{++}{T}\right|=0↔{S}\mathrm{++}{T}=\varnothing \right)$
6 lencl ${⊢}{S}\in \mathrm{Word}{A}\to \left|{S}\right|\in {ℕ}_{0}$
7 nn0re ${⊢}\left|{S}\right|\in {ℕ}_{0}\to \left|{S}\right|\in ℝ$
8 nn0ge0 ${⊢}\left|{S}\right|\in {ℕ}_{0}\to 0\le \left|{S}\right|$
9 7 8 jca ${⊢}\left|{S}\right|\in {ℕ}_{0}\to \left(\left|{S}\right|\in ℝ\wedge 0\le \left|{S}\right|\right)$
10 6 9 syl ${⊢}{S}\in \mathrm{Word}{A}\to \left(\left|{S}\right|\in ℝ\wedge 0\le \left|{S}\right|\right)$
11 lencl ${⊢}{T}\in \mathrm{Word}{B}\to \left|{T}\right|\in {ℕ}_{0}$
12 nn0re ${⊢}\left|{T}\right|\in {ℕ}_{0}\to \left|{T}\right|\in ℝ$
13 nn0ge0 ${⊢}\left|{T}\right|\in {ℕ}_{0}\to 0\le \left|{T}\right|$
14 12 13 jca ${⊢}\left|{T}\right|\in {ℕ}_{0}\to \left(\left|{T}\right|\in ℝ\wedge 0\le \left|{T}\right|\right)$
15 11 14 syl ${⊢}{T}\in \mathrm{Word}{B}\to \left(\left|{T}\right|\in ℝ\wedge 0\le \left|{T}\right|\right)$
16 add20 ${⊢}\left(\left(\left|{S}\right|\in ℝ\wedge 0\le \left|{S}\right|\right)\wedge \left(\left|{T}\right|\in ℝ\wedge 0\le \left|{T}\right|\right)\right)\to \left(\left|{S}\right|+\left|{T}\right|=0↔\left(\left|{S}\right|=0\wedge \left|{T}\right|=0\right)\right)$
17 10 15 16 syl2an ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{B}\right)\to \left(\left|{S}\right|+\left|{T}\right|=0↔\left(\left|{S}\right|=0\wedge \left|{T}\right|=0\right)\right)$
18 2 5 17 3bitr3d ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{B}\right)\to \left({S}\mathrm{++}{T}=\varnothing ↔\left(\left|{S}\right|=0\wedge \left|{T}\right|=0\right)\right)$
19 hasheq0 ${⊢}{S}\in \mathrm{Word}{A}\to \left(\left|{S}\right|=0↔{S}=\varnothing \right)$
20 hasheq0 ${⊢}{T}\in \mathrm{Word}{B}\to \left(\left|{T}\right|=0↔{T}=\varnothing \right)$
21 19 20 bi2anan9 ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{B}\right)\to \left(\left(\left|{S}\right|=0\wedge \left|{T}\right|=0\right)↔\left({S}=\varnothing \wedge {T}=\varnothing \right)\right)$
22 18 21 bitrd ${⊢}\left({S}\in \mathrm{Word}{A}\wedge {T}\in \mathrm{Word}{B}\right)\to \left({S}\mathrm{++}{T}=\varnothing ↔\left({S}=\varnothing \wedge {T}=\varnothing \right)\right)$