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 )