Metamath Proof Explorer


Theorem swrdccat2

Description: Recover the right half of a concatenated word. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Assertion swrdccat2
|- ( ( S e. Word B /\ T e. Word B ) -> ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) = T )

Proof

Step Hyp Ref Expression
1 ccatcl
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( S ++ T ) e. Word B )
2 swrdcl
 |-  ( ( S ++ T ) e. Word B -> ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) e. Word B )
3 wrdfn
 |-  ( ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) e. Word B -> ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) Fn ( 0 ..^ ( # ` ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) ) ) )
4 1 2 3 3syl
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) Fn ( 0 ..^ ( # ` ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) ) ) )
5 lencl
 |-  ( S e. Word B -> ( # ` S ) e. NN0 )
6 nn0uz
 |-  NN0 = ( ZZ>= ` 0 )
7 5 6 eleqtrdi
 |-  ( S e. Word B -> ( # ` S ) e. ( ZZ>= ` 0 ) )
8 7 adantr
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( # ` S ) e. ( ZZ>= ` 0 ) )
9 5 nn0zd
 |-  ( S e. Word B -> ( # ` S ) e. ZZ )
10 9 uzidd
 |-  ( S e. Word B -> ( # ` S ) e. ( ZZ>= ` ( # ` S ) ) )
11 lencl
 |-  ( T e. Word B -> ( # ` T ) e. NN0 )
12 uzaddcl
 |-  ( ( ( # ` S ) e. ( ZZ>= ` ( # ` S ) ) /\ ( # ` T ) e. NN0 ) -> ( ( # ` S ) + ( # ` T ) ) e. ( ZZ>= ` ( # ` S ) ) )
13 10 11 12 syl2an
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( # ` S ) + ( # ` T ) ) e. ( ZZ>= ` ( # ` S ) ) )
14 elfzuzb
 |-  ( ( # ` S ) e. ( 0 ... ( ( # ` S ) + ( # ` T ) ) ) <-> ( ( # ` S ) e. ( ZZ>= ` 0 ) /\ ( ( # ` S ) + ( # ` T ) ) e. ( ZZ>= ` ( # ` S ) ) ) )
15 8 13 14 sylanbrc
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( # ` S ) e. ( 0 ... ( ( # ` S ) + ( # ` T ) ) ) )
16 nn0addcl
 |-  ( ( ( # ` S ) e. NN0 /\ ( # ` T ) e. NN0 ) -> ( ( # ` S ) + ( # ` T ) ) e. NN0 )
17 5 11 16 syl2an
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( # ` S ) + ( # ` T ) ) e. NN0 )
18 17 6 eleqtrdi
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( # ` S ) + ( # ` T ) ) e. ( ZZ>= ` 0 ) )
19 17 nn0zd
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( # ` S ) + ( # ` T ) ) e. ZZ )
20 19 uzidd
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( # ` S ) + ( # ` T ) ) e. ( ZZ>= ` ( ( # ` S ) + ( # ` T ) ) ) )
21 elfzuzb
 |-  ( ( ( # ` S ) + ( # ` T ) ) e. ( 0 ... ( ( # ` S ) + ( # ` T ) ) ) <-> ( ( ( # ` S ) + ( # ` T ) ) e. ( ZZ>= ` 0 ) /\ ( ( # ` S ) + ( # ` T ) ) e. ( ZZ>= ` ( ( # ` S ) + ( # ` T ) ) ) ) )
22 18 20 21 sylanbrc
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( # ` S ) + ( # ` T ) ) e. ( 0 ... ( ( # ` S ) + ( # ` T ) ) ) )
23 ccatlen
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( # ` ( S ++ T ) ) = ( ( # ` S ) + ( # ` T ) ) )
24 23 oveq2d
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( 0 ... ( # ` ( S ++ T ) ) ) = ( 0 ... ( ( # ` S ) + ( # ` T ) ) ) )
25 22 24 eleqtrrd
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( # ` S ) + ( # ` T ) ) e. ( 0 ... ( # ` ( S ++ T ) ) ) )
26 swrdlen
 |-  ( ( ( S ++ T ) e. Word B /\ ( # ` S ) e. ( 0 ... ( ( # ` S ) + ( # ` T ) ) ) /\ ( ( # ` S ) + ( # ` T ) ) e. ( 0 ... ( # ` ( S ++ T ) ) ) ) -> ( # ` ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) ) = ( ( ( # ` S ) + ( # ` T ) ) - ( # ` S ) ) )
27 1 15 25 26 syl3anc
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( # ` ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) ) = ( ( ( # ` S ) + ( # ` T ) ) - ( # ` S ) ) )
28 5 nn0cnd
 |-  ( S e. Word B -> ( # ` S ) e. CC )
29 11 nn0cnd
 |-  ( T e. Word B -> ( # ` T ) e. CC )
30 pncan2
 |-  ( ( ( # ` S ) e. CC /\ ( # ` T ) e. CC ) -> ( ( ( # ` S ) + ( # ` T ) ) - ( # ` S ) ) = ( # ` T ) )
31 28 29 30 syl2an
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( ( # ` S ) + ( # ` T ) ) - ( # ` S ) ) = ( # ` T ) )
32 27 31 eqtrd
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( # ` ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) ) = ( # ` T ) )
33 32 oveq2d
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( 0 ..^ ( # ` ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) ) ) = ( 0 ..^ ( # ` T ) ) )
34 33 fneq2d
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) Fn ( 0 ..^ ( # ` ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) ) ) <-> ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) Fn ( 0 ..^ ( # ` T ) ) ) )
35 4 34 mpbid
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) Fn ( 0 ..^ ( # ` T ) ) )
36 wrdfn
 |-  ( T e. Word B -> T Fn ( 0 ..^ ( # ` T ) ) )
37 36 adantl
 |-  ( ( S e. Word B /\ T e. Word B ) -> T Fn ( 0 ..^ ( # ` T ) ) )
38 1 15 25 3jca
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( S ++ T ) e. Word B /\ ( # ` S ) e. ( 0 ... ( ( # ` S ) + ( # ` T ) ) ) /\ ( ( # ` S ) + ( # ` T ) ) e. ( 0 ... ( # ` ( S ++ T ) ) ) ) )
39 31 oveq2d
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( 0 ..^ ( ( ( # ` S ) + ( # ` T ) ) - ( # ` S ) ) ) = ( 0 ..^ ( # ` T ) ) )
40 39 eleq2d
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( k e. ( 0 ..^ ( ( ( # ` S ) + ( # ` T ) ) - ( # ` S ) ) ) <-> k e. ( 0 ..^ ( # ` T ) ) ) )
41 40 biimpar
 |-  ( ( ( S e. Word B /\ T e. Word B ) /\ k e. ( 0 ..^ ( # ` T ) ) ) -> k e. ( 0 ..^ ( ( ( # ` S ) + ( # ` T ) ) - ( # ` S ) ) ) )
42 swrdfv
 |-  ( ( ( ( S ++ T ) e. Word B /\ ( # ` S ) e. ( 0 ... ( ( # ` S ) + ( # ` T ) ) ) /\ ( ( # ` S ) + ( # ` T ) ) e. ( 0 ... ( # ` ( S ++ T ) ) ) ) /\ k e. ( 0 ..^ ( ( ( # ` S ) + ( # ` T ) ) - ( # ` S ) ) ) ) -> ( ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) ` k ) = ( ( S ++ T ) ` ( k + ( # ` S ) ) ) )
43 38 41 42 syl2an2r
 |-  ( ( ( S e. Word B /\ T e. Word B ) /\ k e. ( 0 ..^ ( # ` T ) ) ) -> ( ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) ` k ) = ( ( S ++ T ) ` ( k + ( # ` S ) ) ) )
44 ccatval3
 |-  ( ( S e. Word B /\ T e. Word B /\ k e. ( 0 ..^ ( # ` T ) ) ) -> ( ( S ++ T ) ` ( k + ( # ` S ) ) ) = ( T ` k ) )
45 44 3expa
 |-  ( ( ( S e. Word B /\ T e. Word B ) /\ k e. ( 0 ..^ ( # ` T ) ) ) -> ( ( S ++ T ) ` ( k + ( # ` S ) ) ) = ( T ` k ) )
46 43 45 eqtrd
 |-  ( ( ( S e. Word B /\ T e. Word B ) /\ k e. ( 0 ..^ ( # ` T ) ) ) -> ( ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) ` k ) = ( T ` k ) )
47 35 37 46 eqfnfvd
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( S ++ T ) substr <. ( # ` S ) , ( ( # ` S ) + ( # ` T ) ) >. ) = T )