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 )