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 ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ) → ( ( 𝑆 ++ 𝑇 ) = ∅ ↔ ( 𝑆 = ∅ ∧ 𝑇 = ∅ ) ) )

Proof

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