Metamath Proof Explorer

Theorem pfxccat1

Description: Recover the left half of a concatenated word. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by AV, 6-May-2020)

Ref Expression
Assertion pfxccat1 
|- ( ( S e. Word B /\ T e. Word B ) -> ( ( S ++ T ) prefix ( # ` S ) ) = S )

Proof

Step Hyp Ref Expression
1 ccatcl 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( S ++ T ) e. Word B )
2 lencl 
 |-  ( S e. Word B -> ( # ` S ) e. NN0 )
3 lencl 
 |-  ( T e. Word B -> ( # ` T ) e. NN0 )
4 2 3 anim12i 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( # ` S ) e. NN0 /\ ( # ` T ) e. NN0 ) )
5 nn0fz0 
 |-  ( ( # ` S ) e. NN0 <-> ( # ` S ) e. ( 0 ... ( # ` S ) ) )
6 2 5 sylib 
 |-  ( S e. Word B -> ( # ` S ) e. ( 0 ... ( # ` S ) ) )
7 6 adantr 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( # ` S ) e. ( 0 ... ( # ` S ) ) )
8 elfz0add 
 |-  ( ( ( # ` S ) e. NN0 /\ ( # ` T ) e. NN0 ) -> ( ( # ` S ) e. ( 0 ... ( # ` S ) ) -> ( # ` S ) e. ( 0 ... ( ( # ` S ) + ( # ` T ) ) ) ) )
9 4 7 8 sylc 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( # ` S ) e. ( 0 ... ( ( # ` S ) + ( # ` T ) ) ) )
10 ccatlen 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( # ` ( S ++ T ) ) = ( ( # ` S ) + ( # ` T ) ) )
11 10 oveq2d 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( 0 ... ( # ` ( S ++ T ) ) ) = ( 0 ... ( ( # ` S ) + ( # ` T ) ) ) )
12 9 11 eleqtrrd 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( # ` S ) e. ( 0 ... ( # ` ( S ++ T ) ) ) )
13 pfxres 
 |-  ( ( ( S ++ T ) e. Word B /\ ( # ` S ) e. ( 0 ... ( # ` ( S ++ T ) ) ) ) -> ( ( S ++ T ) prefix ( # ` S ) ) = ( ( S ++ T ) |` ( 0 ..^ ( # ` S ) ) ) )
14 1 12 13 syl2anc 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( S ++ T ) prefix ( # ` S ) ) = ( ( S ++ T ) |` ( 0 ..^ ( # ` S ) ) ) )
15 ccatvalfn 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( S ++ T ) Fn ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) )
16 2 nn0zd 
 |-  ( S e. Word B -> ( # ` S ) e. ZZ )
17 16 uzidd 
 |-  ( S e. Word B -> ( # ` S ) e. ( ZZ>= ` ( # ` S ) ) )
18 uzaddcl 
 |-  ( ( ( # ` S ) e. ( ZZ>= ` ( # ` S ) ) /\ ( # ` T ) e. NN0 ) -> ( ( # ` S ) + ( # ` T ) ) e. ( ZZ>= ` ( # ` S ) ) )
19 17 3 18 syl2an 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( # ` S ) + ( # ` T ) ) e. ( ZZ>= ` ( # ` S ) ) )
20 fzoss2 
 |-  ( ( ( # ` S ) + ( # ` T ) ) e. ( ZZ>= ` ( # ` S ) ) -> ( 0 ..^ ( # ` S ) ) C_ ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) )
21 19 20 syl 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( 0 ..^ ( # ` S ) ) C_ ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) )
22 15 21 fnssresd 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( S ++ T ) |` ( 0 ..^ ( # ` S ) ) ) Fn ( 0 ..^ ( # ` S ) ) )
23 wrdfn 
 |-  ( S e. Word B -> S Fn ( 0 ..^ ( # ` S ) ) )
24 23 adantr 
 |-  ( ( S e. Word B /\ T e. Word B ) -> S Fn ( 0 ..^ ( # ` S ) ) )
25 fvres 
 |-  ( k e. ( 0 ..^ ( # ` S ) ) -> ( ( ( S ++ T ) |` ( 0 ..^ ( # ` S ) ) ) ` k ) = ( ( S ++ T ) ` k ) )
26 25 adantl 
 |-  ( ( ( S e. Word B /\ T e. Word B ) /\ k e. ( 0 ..^ ( # ` S ) ) ) -> ( ( ( S ++ T ) |` ( 0 ..^ ( # ` S ) ) ) ` k ) = ( ( S ++ T ) ` k ) )
27 ccatval1 
 |-  ( ( S e. Word B /\ T e. Word B /\ k e. ( 0 ..^ ( # ` S ) ) ) -> ( ( S ++ T ) ` k ) = ( S ` k ) )
28 27 3expa 
 |-  ( ( ( S e. Word B /\ T e. Word B ) /\ k e. ( 0 ..^ ( # ` S ) ) ) -> ( ( S ++ T ) ` k ) = ( S ` k ) )
29 26 28 eqtrd 
 |-  ( ( ( S e. Word B /\ T e. Word B ) /\ k e. ( 0 ..^ ( # ` S ) ) ) -> ( ( ( S ++ T ) |` ( 0 ..^ ( # ` S ) ) ) ` k ) = ( S ` k ) )
30 22 24 29 eqfnfvd 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( S ++ T ) |` ( 0 ..^ ( # ` S ) ) ) = S )
31 14 30 eqtrd 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( S ++ T ) prefix ( # ` S ) ) = S )