Metamath Proof Explorer

Theorem swrdnd

Description: The value of the subword extractor is the empty set (undefined) if the range is not valid. (Contributed by Alexander van der Vekens, 16-Mar-2018) (Proof shortened by AV, 2-May-2020)

Ref Expression
Assertion swrdnd 
|- ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( ( F < 0 \/ L <_ F \/ ( # ` W ) < L ) -> ( W substr <. F , L >. ) = (/) ) )

Proof

Step Hyp Ref Expression
1 3orcomb 
 |-  ( ( F < 0 \/ L <_ F \/ ( # ` W ) < L ) <-> ( F < 0 \/ ( # ` W ) < L \/ L <_ F ) )
2 df-3or 
 |-  ( ( F < 0 \/ ( # ` W ) < L \/ L <_ F ) <-> ( ( F < 0 \/ ( # ` W ) < L ) \/ L <_ F ) )
3 1 2 bitri 
 |-  ( ( F < 0 \/ L <_ F \/ ( # ` W ) < L ) <-> ( ( F < 0 \/ ( # ` W ) < L ) \/ L <_ F ) )
4 swrdlend 
 |-  ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( L <_ F -> ( W substr <. F , L >. ) = (/) ) )
5 4 com12 
 |-  ( L <_ F -> ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( W substr <. F , L >. ) = (/) ) )
6 swrdval 
 |-  ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( W substr <. F , L >. ) = if ( ( F ..^ L ) C_ dom W , ( i e. ( 0 ..^ ( L - F ) ) |-> ( W ` ( i + F ) ) ) , (/) ) )
7 6 adantl 
 |-  ( ( ( ( F < 0 \/ ( # ` W ) < L ) /\ -. L <_ F ) /\ ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) ) -> ( W substr <. F , L >. ) = if ( ( F ..^ L ) C_ dom W , ( i e. ( 0 ..^ ( L - F ) ) |-> ( W ` ( i + F ) ) ) , (/) ) )
8 zre 
 |-  ( F e. ZZ -> F e. RR )
9 0red 
 |-  ( F e. ZZ -> 0 e. RR )
10 8 9 ltnled 
 |-  ( F e. ZZ -> ( F < 0 <-> -. 0 <_ F ) )
11 10 3ad2ant2 
 |-  ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( F < 0 <-> -. 0 <_ F ) )
12 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
13 12 nn0red 
 |-  ( W e. Word V -> ( # ` W ) e. RR )
14 zre 
 |-  ( L e. ZZ -> L e. RR )
15 13 14 anim12i 
 |-  ( ( W e. Word V /\ L e. ZZ ) -> ( ( # ` W ) e. RR /\ L e. RR ) )
16 15 3adant2 
 |-  ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( ( # ` W ) e. RR /\ L e. RR ) )
17 ltnle 
 |-  ( ( ( # ` W ) e. RR /\ L e. RR ) -> ( ( # ` W ) < L <-> -. L <_ ( # ` W ) ) )
18 16 17 syl 
 |-  ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( ( # ` W ) < L <-> -. L <_ ( # ` W ) ) )
19 11 18 orbi12d 
 |-  ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( ( F < 0 \/ ( # ` W ) < L ) <-> ( -. 0 <_ F \/ -. L <_ ( # ` W ) ) ) )
20 19 biimpcd 
 |-  ( ( F < 0 \/ ( # ` W ) < L ) -> ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( -. 0 <_ F \/ -. L <_ ( # ` W ) ) ) )
21 20 adantr 
 |-  ( ( ( F < 0 \/ ( # ` W ) < L ) /\ -. L <_ F ) -> ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( -. 0 <_ F \/ -. L <_ ( # ` W ) ) ) )
22 21 imp 
 |-  ( ( ( ( F < 0 \/ ( # ` W ) < L ) /\ -. L <_ F ) /\ ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) ) -> ( -. 0 <_ F \/ -. L <_ ( # ` W ) ) )
23 ianor 
 |-  ( -. ( 0 <_ F /\ L <_ ( # ` W ) ) <-> ( -. 0 <_ F \/ -. L <_ ( # ` W ) ) )
24 22 23 sylibr 
 |-  ( ( ( ( F < 0 \/ ( # ` W ) < L ) /\ -. L <_ F ) /\ ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) ) -> -. ( 0 <_ F /\ L <_ ( # ` W ) ) )
25 3simpc 
 |-  ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( F e. ZZ /\ L e. ZZ ) )
26 12 nn0zd 
 |-  ( W e. Word V -> ( # ` W ) e. ZZ )
27 0z 
 |-  0 e. ZZ
28 26 27 jctil 
 |-  ( W e. Word V -> ( 0 e. ZZ /\ ( # ` W ) e. ZZ ) )
29 28 3ad2ant1 
 |-  ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( 0 e. ZZ /\ ( # ` W ) e. ZZ ) )
30 ltnle 
 |-  ( ( F e. RR /\ L e. RR ) -> ( F < L <-> -. L <_ F ) )
31 8 14 30 syl2an 
 |-  ( ( F e. ZZ /\ L e. ZZ ) -> ( F < L <-> -. L <_ F ) )
32 31 3adant1 
 |-  ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( F < L <-> -. L <_ F ) )
33 32 biimprcd 
 |-  ( -. L <_ F -> ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> F < L ) )
34 33 adantl 
 |-  ( ( ( F < 0 \/ ( # ` W ) < L ) /\ -. L <_ F ) -> ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> F < L ) )
35 34 imp 
 |-  ( ( ( ( F < 0 \/ ( # ` W ) < L ) /\ -. L <_ F ) /\ ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) ) -> F < L )
36 ssfzo12bi 
 |-  ( ( ( F e. ZZ /\ L e. ZZ ) /\ ( 0 e. ZZ /\ ( # ` W ) e. ZZ ) /\ F < L ) -> ( ( F ..^ L ) C_ ( 0 ..^ ( # ` W ) ) <-> ( 0 <_ F /\ L <_ ( # ` W ) ) ) )
37 25 29 35 36 syl2an23an 
 |-  ( ( ( ( F < 0 \/ ( # ` W ) < L ) /\ -. L <_ F ) /\ ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) ) -> ( ( F ..^ L ) C_ ( 0 ..^ ( # ` W ) ) <-> ( 0 <_ F /\ L <_ ( # ` W ) ) ) )
38 24 37 mtbird 
 |-  ( ( ( ( F < 0 \/ ( # ` W ) < L ) /\ -. L <_ F ) /\ ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) ) -> -. ( F ..^ L ) C_ ( 0 ..^ ( # ` W ) ) )
39 wrddm 
 |-  ( W e. Word V -> dom W = ( 0 ..^ ( # ` W ) ) )
40 39 sseq2d 
 |-  ( W e. Word V -> ( ( F ..^ L ) C_ dom W <-> ( F ..^ L ) C_ ( 0 ..^ ( # ` W ) ) ) )
41 40 notbid 
 |-  ( W e. Word V -> ( -. ( F ..^ L ) C_ dom W <-> -. ( F ..^ L ) C_ ( 0 ..^ ( # ` W ) ) ) )
42 41 3ad2ant1 
 |-  ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( -. ( F ..^ L ) C_ dom W <-> -. ( F ..^ L ) C_ ( 0 ..^ ( # ` W ) ) ) )
43 42 adantl 
 |-  ( ( ( ( F < 0 \/ ( # ` W ) < L ) /\ -. L <_ F ) /\ ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) ) -> ( -. ( F ..^ L ) C_ dom W <-> -. ( F ..^ L ) C_ ( 0 ..^ ( # ` W ) ) ) )
44 38 43 mpbird 
 |-  ( ( ( ( F < 0 \/ ( # ` W ) < L ) /\ -. L <_ F ) /\ ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) ) -> -. ( F ..^ L ) C_ dom W )
45 44 iffalsed 
 |-  ( ( ( ( F < 0 \/ ( # ` W ) < L ) /\ -. L <_ F ) /\ ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) ) -> if ( ( F ..^ L ) C_ dom W , ( i e. ( 0 ..^ ( L - F ) ) |-> ( W ` ( i + F ) ) ) , (/) ) = (/) )
46 7 45 eqtrd 
 |-  ( ( ( ( F < 0 \/ ( # ` W ) < L ) /\ -. L <_ F ) /\ ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) ) -> ( W substr <. F , L >. ) = (/) )
47 46 exp31 
 |-  ( ( F < 0 \/ ( # ` W ) < L ) -> ( -. L <_ F -> ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( W substr <. F , L >. ) = (/) ) ) )
48 47 impcom 
 |-  ( ( -. L <_ F /\ ( F < 0 \/ ( # ` W ) < L ) ) -> ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( W substr <. F , L >. ) = (/) ) )
49 5 48 jaoi3 
 |-  ( ( L <_ F \/ ( F < 0 \/ ( # ` W ) < L ) ) -> ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( W substr <. F , L >. ) = (/) ) )
50 49 orcoms 
 |-  ( ( ( F < 0 \/ ( # ` W ) < L ) \/ L <_ F ) -> ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( W substr <. F , L >. ) = (/) ) )
51 3 50 sylbi 
 |-  ( ( F < 0 \/ L <_ F \/ ( # ` W ) < L ) -> ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( W substr <. F , L >. ) = (/) ) )
52 51 com12 
 |-  ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( ( F < 0 \/ L <_ F \/ ( # ` W ) < L ) -> ( W substr <. F , L >. ) = (/) ) )