Metamath Proof Explorer

Theorem swrdnd2

Description: Value of the subword extractor outside its intended domain. (Contributed by Alexander van der Vekens, 24-May-2018)

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

Proof

Step Hyp Ref Expression
1 3orass 
 |-  ( ( B <_ A \/ ( # ` W ) <_ A \/ B <_ 0 ) <-> ( B <_ A \/ ( ( # ` W ) <_ A \/ B <_ 0 ) ) )
2 pm2.24 
 |-  ( B <_ A -> ( -. B <_ A -> ( ( W e. Word V /\ A e. ZZ /\ B e. ZZ ) -> ( W substr <. A , B >. ) = (/) ) ) )
3 swrdval 
 |-  ( ( W e. Word V /\ A e. ZZ /\ B e. ZZ ) -> ( W substr <. A , B >. ) = if ( ( A ..^ B ) C_ dom W , ( x e. ( 0 ..^ ( B - A ) ) |-> ( W ` ( x + A ) ) ) , (/) ) )
4 3 ad2antrr 
 |-  ( ( ( ( W e. Word V /\ A e. ZZ /\ B e. ZZ ) /\ ( ( # ` W ) <_ A \/ B <_ 0 ) ) /\ -. B <_ A ) -> ( W substr <. A , B >. ) = if ( ( A ..^ B ) C_ dom W , ( x e. ( 0 ..^ ( B - A ) ) |-> ( W ` ( x + A ) ) ) , (/) ) )
5 wrddm 
 |-  ( W e. Word V -> dom W = ( 0 ..^ ( # ` W ) ) )
6 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
7 3anass 
 |-  ( ( ( # ` W ) e. NN0 /\ A e. ZZ /\ B e. ZZ ) <-> ( ( # ` W ) e. NN0 /\ ( A e. ZZ /\ B e. ZZ ) ) )
8 ssfzoulel 
 |-  ( ( ( # ` W ) e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( ( ( # ` W ) <_ A \/ B <_ 0 ) -> ( ( A ..^ B ) C_ ( 0 ..^ ( # ` W ) ) -> B <_ A ) ) )
9 8 imp 
 |-  ( ( ( ( # ` W ) e. NN0 /\ A e. ZZ /\ B e. ZZ ) /\ ( ( # ` W ) <_ A \/ B <_ 0 ) ) -> ( ( A ..^ B ) C_ ( 0 ..^ ( # ` W ) ) -> B <_ A ) )
10 7 9 sylanbr 
 |-  ( ( ( ( # ` W ) e. NN0 /\ ( A e. ZZ /\ B e. ZZ ) ) /\ ( ( # ` W ) <_ A \/ B <_ 0 ) ) -> ( ( A ..^ B ) C_ ( 0 ..^ ( # ` W ) ) -> B <_ A ) )
11 10 con3dimp 
 |-  ( ( ( ( ( # ` W ) e. NN0 /\ ( A e. ZZ /\ B e. ZZ ) ) /\ ( ( # ` W ) <_ A \/ B <_ 0 ) ) /\ -. B <_ A ) -> -. ( A ..^ B ) C_ ( 0 ..^ ( # ` W ) ) )
12 sseq2 
 |-  ( dom W = ( 0 ..^ ( # ` W ) ) -> ( ( A ..^ B ) C_ dom W <-> ( A ..^ B ) C_ ( 0 ..^ ( # ` W ) ) ) )
13 12 notbid 
 |-  ( dom W = ( 0 ..^ ( # ` W ) ) -> ( -. ( A ..^ B ) C_ dom W <-> -. ( A ..^ B ) C_ ( 0 ..^ ( # ` W ) ) ) )
14 11 13 syl5ibr 
 |-  ( dom W = ( 0 ..^ ( # ` W ) ) -> ( ( ( ( ( # ` W ) e. NN0 /\ ( A e. ZZ /\ B e. ZZ ) ) /\ ( ( # ` W ) <_ A \/ B <_ 0 ) ) /\ -. B <_ A ) -> -. ( A ..^ B ) C_ dom W ) )
15 14 exp5j 
 |-  ( dom W = ( 0 ..^ ( # ` W ) ) -> ( ( # ` W ) e. NN0 -> ( ( A e. ZZ /\ B e. ZZ ) -> ( ( ( # ` W ) <_ A \/ B <_ 0 ) -> ( -. B <_ A -> -. ( A ..^ B ) C_ dom W ) ) ) ) )
16 5 6 15 sylc 
 |-  ( W e. Word V -> ( ( A e. ZZ /\ B e. ZZ ) -> ( ( ( # ` W ) <_ A \/ B <_ 0 ) -> ( -. B <_ A -> -. ( A ..^ B ) C_ dom W ) ) ) )
17 16 3impib 
 |-  ( ( W e. Word V /\ A e. ZZ /\ B e. ZZ ) -> ( ( ( # ` W ) <_ A \/ B <_ 0 ) -> ( -. B <_ A -> -. ( A ..^ B ) C_ dom W ) ) )
18 17 imp31 
 |-  ( ( ( ( W e. Word V /\ A e. ZZ /\ B e. ZZ ) /\ ( ( # ` W ) <_ A \/ B <_ 0 ) ) /\ -. B <_ A ) -> -. ( A ..^ B ) C_ dom W )
19 18 iffalsed 
 |-  ( ( ( ( W e. Word V /\ A e. ZZ /\ B e. ZZ ) /\ ( ( # ` W ) <_ A \/ B <_ 0 ) ) /\ -. B <_ A ) -> if ( ( A ..^ B ) C_ dom W , ( x e. ( 0 ..^ ( B - A ) ) |-> ( W ` ( x + A ) ) ) , (/) ) = (/) )
20 4 19 eqtrd 
 |-  ( ( ( ( W e. Word V /\ A e. ZZ /\ B e. ZZ ) /\ ( ( # ` W ) <_ A \/ B <_ 0 ) ) /\ -. B <_ A ) -> ( W substr <. A , B >. ) = (/) )
21 20 ex 
 |-  ( ( ( W e. Word V /\ A e. ZZ /\ B e. ZZ ) /\ ( ( # ` W ) <_ A \/ B <_ 0 ) ) -> ( -. B <_ A -> ( W substr <. A , B >. ) = (/) ) )
22 21 expcom 
 |-  ( ( ( # ` W ) <_ A \/ B <_ 0 ) -> ( ( W e. Word V /\ A e. ZZ /\ B e. ZZ ) -> ( -. B <_ A -> ( W substr <. A , B >. ) = (/) ) ) )
23 22 com23 
 |-  ( ( ( # ` W ) <_ A \/ B <_ 0 ) -> ( -. B <_ A -> ( ( W e. Word V /\ A e. ZZ /\ B e. ZZ ) -> ( W substr <. A , B >. ) = (/) ) ) )
24 2 23 jaoi 
 |-  ( ( B <_ A \/ ( ( # ` W ) <_ A \/ B <_ 0 ) ) -> ( -. B <_ A -> ( ( W e. Word V /\ A e. ZZ /\ B e. ZZ ) -> ( W substr <. A , B >. ) = (/) ) ) )
25 swrdlend 
 |-  ( ( W e. Word V /\ A e. ZZ /\ B e. ZZ ) -> ( B <_ A -> ( W substr <. A , B >. ) = (/) ) )
26 25 com12 
 |-  ( B <_ A -> ( ( W e. Word V /\ A e. ZZ /\ B e. ZZ ) -> ( W substr <. A , B >. ) = (/) ) )
27 24 26 pm2.61d2 
 |-  ( ( B <_ A \/ ( ( # ` W ) <_ A \/ B <_ 0 ) ) -> ( ( W e. Word V /\ A e. ZZ /\ B e. ZZ ) -> ( W substr <. A , B >. ) = (/) ) )
28 1 27 sylbi 
 |-  ( ( B <_ A \/ ( # ` W ) <_ A \/ B <_ 0 ) -> ( ( W e. Word V /\ A e. ZZ /\ B e. ZZ ) -> ( W substr <. A , B >. ) = (/) ) )
29 28 com12 
 |-  ( ( W e. Word V /\ A e. ZZ /\ B e. ZZ ) -> ( ( B <_ A \/ ( # ` W ) <_ A \/ B <_ 0 ) -> ( W substr <. A , B >. ) = (/) ) )