This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ccatdmss

Description: The domain of a concatenated word is a superset of the domain of the first word. (Contributed by Thierry Arnoux, 19-Jun-2025)

Ref Expression
Hypotheses ccatdmss.1 
|- ( ph -> A e. Word S )
ccatdmss.2 
|- ( ph -> B e. Word S )
Assertion ccatdmss 
|- ( ph -> dom A C_ dom ( A ++ B ) )

Proof

Step Hyp Ref Expression
1 ccatdmss.1 
 |-  ( ph -> A e. Word S )
2 ccatdmss.2 
 |-  ( ph -> B e. Word S )
3 lencl 
 |-  ( A e. Word S -> ( # ` A ) e. NN0 )
4 1 3 syl 
 |-  ( ph -> ( # ` A ) e. NN0 )
5 4 nn0zd 
 |-  ( ph -> ( # ` A ) e. ZZ )
6 ccatcl 
 |-  ( ( A e. Word S /\ B e. Word S ) -> ( A ++ B ) e. Word S )
7 1 2 6 syl2anc 
 |-  ( ph -> ( A ++ B ) e. Word S )
8 lencl 
 |-  ( ( A ++ B ) e. Word S -> ( # ` ( A ++ B ) ) e. NN0 )
9 7 8 syl 
 |-  ( ph -> ( # ` ( A ++ B ) ) e. NN0 )
10 9 nn0zd 
 |-  ( ph -> ( # ` ( A ++ B ) ) e. ZZ )
11 4 nn0red 
 |-  ( ph -> ( # ` A ) e. RR )
12 lencl 
 |-  ( B e. Word S -> ( # ` B ) e. NN0 )
13 2 12 syl 
 |-  ( ph -> ( # ` B ) e. NN0 )
14 nn0addge1 
 |-  ( ( ( # ` A ) e. RR /\ ( # ` B ) e. NN0 ) -> ( # ` A ) <_ ( ( # ` A ) + ( # ` B ) ) )
15 11 13 14 syl2anc 
 |-  ( ph -> ( # ` A ) <_ ( ( # ` A ) + ( # ` B ) ) )
16 ccatlen 
 |-  ( ( A e. Word S /\ B e. Word S ) -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
17 1 2 16 syl2anc 
 |-  ( ph -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
18 15 17 breqtrrd 
 |-  ( ph -> ( # ` A ) <_ ( # ` ( A ++ B ) ) )
19 eluz2 
 |-  ( ( # ` ( A ++ B ) ) e. ( ZZ>= ` ( # ` A ) ) <-> ( ( # ` A ) e. ZZ /\ ( # ` ( A ++ B ) ) e. ZZ /\ ( # ` A ) <_ ( # ` ( A ++ B ) ) ) )
20 5 10 18 19 syl3anbrc 
 |-  ( ph -> ( # ` ( A ++ B ) ) e. ( ZZ>= ` ( # ` A ) ) )
21 fzoss2 
 |-  ( ( # ` ( A ++ B ) ) e. ( ZZ>= ` ( # ` A ) ) -> ( 0 ..^ ( # ` A ) ) C_ ( 0 ..^ ( # ` ( A ++ B ) ) ) )
22 20 21 syl 
 |-  ( ph -> ( 0 ..^ ( # ` A ) ) C_ ( 0 ..^ ( # ` ( A ++ B ) ) ) )
23 eqidd 
 |-  ( ph -> ( # ` A ) = ( # ` A ) )
24 23 1 wrdfd 
 |-  ( ph -> A : ( 0 ..^ ( # ` A ) ) --> S )
25 24 fdmd 
 |-  ( ph -> dom A = ( 0 ..^ ( # ` A ) ) )
26 eqidd 
 |-  ( ph -> ( # ` ( A ++ B ) ) = ( # ` ( A ++ B ) ) )
27 26 7 wrdfd 
 |-  ( ph -> ( A ++ B ) : ( 0 ..^ ( # ` ( A ++ B ) ) ) --> S )
28 27 fdmd 
 |-  ( ph -> dom ( A ++ B ) = ( 0 ..^ ( # ` ( A ++ B ) ) ) )
29 22 25 28 3sstr4d 
 |-  ( ph -> dom A C_ dom ( A ++ B ) )