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 e. Word A /\ T e. Word B ) -> ( ( S ++ T ) = (/) <-> ( S = (/) /\ T = (/) ) ) )

Proof

Step Hyp Ref Expression
1 ccatlen 
 |-  ( ( S e. Word A /\ T e. Word B ) -> ( # ` ( S ++ T ) ) = ( ( # ` S ) + ( # ` T ) ) )
2 1 eqeq1d 
 |-  ( ( S e. Word A /\ T e. Word B ) -> ( ( # ` ( S ++ T ) ) = 0 <-> ( ( # ` S ) + ( # ` T ) ) = 0 ) )
3 ovex 
 |-  ( S ++ T ) e. _V
4 hasheq0 
 |-  ( ( S ++ T ) e. _V -> ( ( # ` ( S ++ T ) ) = 0 <-> ( S ++ T ) = (/) ) )
5 3 4 mp1i 
 |-  ( ( S e. Word A /\ T e. Word B ) -> ( ( # ` ( S ++ T ) ) = 0 <-> ( S ++ T ) = (/) ) )
6 lencl 
 |-  ( S e. Word A -> ( # ` S ) e. NN0 )
7 nn0re 
 |-  ( ( # ` S ) e. NN0 -> ( # ` S ) e. RR )
8 nn0ge0 
 |-  ( ( # ` S ) e. NN0 -> 0 <_ ( # ` S ) )
9 7 8 jca 
 |-  ( ( # ` S ) e. NN0 -> ( ( # ` S ) e. RR /\ 0 <_ ( # ` S ) ) )
10 6 9 syl 
 |-  ( S e. Word A -> ( ( # ` S ) e. RR /\ 0 <_ ( # ` S ) ) )
11 lencl 
 |-  ( T e. Word B -> ( # ` T ) e. NN0 )
12 nn0re 
 |-  ( ( # ` T ) e. NN0 -> ( # ` T ) e. RR )
13 nn0ge0 
 |-  ( ( # ` T ) e. NN0 -> 0 <_ ( # ` T ) )
14 12 13 jca 
 |-  ( ( # ` T ) e. NN0 -> ( ( # ` T ) e. RR /\ 0 <_ ( # ` T ) ) )
15 11 14 syl 
 |-  ( T e. Word B -> ( ( # ` T ) e. RR /\ 0 <_ ( # ` T ) ) )
16 add20 
 |-  ( ( ( ( # ` S ) e. RR /\ 0 <_ ( # ` S ) ) /\ ( ( # ` T ) e. RR /\ 0 <_ ( # ` T ) ) ) -> ( ( ( # ` S ) + ( # ` T ) ) = 0 <-> ( ( # ` S ) = 0 /\ ( # ` T ) = 0 ) ) )
17 10 15 16 syl2an 
 |-  ( ( S e. Word A /\ T e. Word B ) -> ( ( ( # ` S ) + ( # ` T ) ) = 0 <-> ( ( # ` S ) = 0 /\ ( # ` T ) = 0 ) ) )
18 2 5 17 3bitr3d 
 |-  ( ( S e. Word A /\ T e. Word B ) -> ( ( S ++ T ) = (/) <-> ( ( # ` S ) = 0 /\ ( # ` T ) = 0 ) ) )
19 hasheq0 
 |-  ( S e. Word A -> ( ( # ` S ) = 0 <-> S = (/) ) )
20 hasheq0 
 |-  ( T e. Word B -> ( ( # ` T ) = 0 <-> T = (/) ) )
21 19 20 bi2anan9 
 |-  ( ( S e. Word A /\ T e. Word B ) -> ( ( ( # ` S ) = 0 /\ ( # ` T ) = 0 ) <-> ( S = (/) /\ T = (/) ) ) )
22 18 21 bitrd 
 |-  ( ( S e. Word A /\ T e. Word B ) -> ( ( S ++ T ) = (/) <-> ( S = (/) /\ T = (/) ) ) )