Metamath Proof Explorer

Theorem swrdcl

Description: Closure of the subword extractor. (Contributed by Stefan O'Rear, 16-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion swrdcl 
|- ( S e. Word A -> ( S substr <. F , L >. ) e. Word A )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( ( S substr <. F , L >. ) = (/) -> ( ( S substr <. F , L >. ) e. Word A <-> (/) e. Word A ) )
2 n0 
 |-  ( ( S substr <. F , L >. ) =/= (/) <-> E. x x e. ( S substr <. F , L >. ) )
3 df-substr 
 |-  substr = ( s e. _V , b e. ( ZZ X. ZZ ) |-> if ( ( ( 1st ` b ) ..^ ( 2nd ` b ) ) C_ dom s , ( x e. ( 0 ..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) ) , (/) ) )
4 3 elmpocl2 
 |-  ( x e. ( S substr <. F , L >. ) -> <. F , L >. e. ( ZZ X. ZZ ) )
5 opelxp 
 |-  ( <. F , L >. e. ( ZZ X. ZZ ) <-> ( F e. ZZ /\ L e. ZZ ) )
6 4 5 sylib 
 |-  ( x e. ( S substr <. F , L >. ) -> ( F e. ZZ /\ L e. ZZ ) )
7 6 exlimiv 
 |-  ( E. x x e. ( S substr <. F , L >. ) -> ( F e. ZZ /\ L e. ZZ ) )
8 2 7 sylbi 
 |-  ( ( S substr <. F , L >. ) =/= (/) -> ( F e. ZZ /\ L e. ZZ ) )
9 swrdval 
 |-  ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) -> ( S substr <. F , L >. ) = if ( ( F ..^ L ) C_ dom S , ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) , (/) ) )
10 wrdf 
 |-  ( S e. Word A -> S : ( 0 ..^ ( # ` S ) ) --> A )
11 10 3ad2ant1 
 |-  ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) -> S : ( 0 ..^ ( # ` S ) ) --> A )
12 11 ad2antrr 
 |-  ( ( ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) /\ ( F ..^ L ) C_ dom S ) /\ x e. ( 0 ..^ ( L - F ) ) ) -> S : ( 0 ..^ ( # ` S ) ) --> A )
13 simplr 
 |-  ( ( ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) /\ ( F ..^ L ) C_ dom S ) /\ x e. ( 0 ..^ ( L - F ) ) ) -> ( F ..^ L ) C_ dom S )
14 simpr 
 |-  ( ( ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) /\ ( F ..^ L ) C_ dom S ) /\ x e. ( 0 ..^ ( L - F ) ) ) -> x e. ( 0 ..^ ( L - F ) ) )
15 simpll3 
 |-  ( ( ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) /\ ( F ..^ L ) C_ dom S ) /\ x e. ( 0 ..^ ( L - F ) ) ) -> L e. ZZ )
16 simpll2 
 |-  ( ( ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) /\ ( F ..^ L ) C_ dom S ) /\ x e. ( 0 ..^ ( L - F ) ) ) -> F e. ZZ )
17 fzoaddel2 
 |-  ( ( x e. ( 0 ..^ ( L - F ) ) /\ L e. ZZ /\ F e. ZZ ) -> ( x + F ) e. ( F ..^ L ) )
18 14 15 16 17 syl3anc 
 |-  ( ( ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) /\ ( F ..^ L ) C_ dom S ) /\ x e. ( 0 ..^ ( L - F ) ) ) -> ( x + F ) e. ( F ..^ L ) )
19 13 18 sseldd 
 |-  ( ( ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) /\ ( F ..^ L ) C_ dom S ) /\ x e. ( 0 ..^ ( L - F ) ) ) -> ( x + F ) e. dom S )
20 12 fdmd 
 |-  ( ( ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) /\ ( F ..^ L ) C_ dom S ) /\ x e. ( 0 ..^ ( L - F ) ) ) -> dom S = ( 0 ..^ ( # ` S ) ) )
21 19 20 eleqtrd 
 |-  ( ( ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) /\ ( F ..^ L ) C_ dom S ) /\ x e. ( 0 ..^ ( L - F ) ) ) -> ( x + F ) e. ( 0 ..^ ( # ` S ) ) )
22 12 21 ffvelrnd 
 |-  ( ( ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) /\ ( F ..^ L ) C_ dom S ) /\ x e. ( 0 ..^ ( L - F ) ) ) -> ( S ` ( x + F ) ) e. A )
23 22 fmpttd 
 |-  ( ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) /\ ( F ..^ L ) C_ dom S ) -> ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) : ( 0 ..^ ( L - F ) ) --> A )
24 iswrdi 
 |-  ( ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) : ( 0 ..^ ( L - F ) ) --> A -> ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) e. Word A )
25 23 24 syl 
 |-  ( ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) /\ ( F ..^ L ) C_ dom S ) -> ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) e. Word A )
26 wrd0 
 |-  (/) e. Word A
27 26 a1i 
 |-  ( ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) /\ -. ( F ..^ L ) C_ dom S ) -> (/) e. Word A )
28 25 27 ifclda 
 |-  ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) -> if ( ( F ..^ L ) C_ dom S , ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) , (/) ) e. Word A )
29 9 28 eqeltrd 
 |-  ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) -> ( S substr <. F , L >. ) e. Word A )
30 29 3expb 
 |-  ( ( S e. Word A /\ ( F e. ZZ /\ L e. ZZ ) ) -> ( S substr <. F , L >. ) e. Word A )
31 8 30 sylan2 
 |-  ( ( S e. Word A /\ ( S substr <. F , L >. ) =/= (/) ) -> ( S substr <. F , L >. ) e. Word A )
32 26 a1i 
 |-  ( S e. Word A -> (/) e. Word A )
33 1 31 32 pm2.61ne 
 |-  ( S e. Word A -> ( S substr <. F , L >. ) e. Word A )