Metamath Proof Explorer

Theorem swrdlend

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 swrdlend 
|- ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( L <_ F -> ( W substr <. F , L >. ) = (/) ) )

Proof

Step Hyp Ref Expression
1 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 ) ) ) , (/) ) )
2 1 adantr 
 |-  ( ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) /\ L <_ F ) -> ( W substr <. F , L >. ) = if ( ( F ..^ L ) C_ dom W , ( i e. ( 0 ..^ ( L - F ) ) |-> ( W ` ( i + F ) ) ) , (/) ) )
3 simpr 
 |-  ( ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) /\ L <_ F ) -> L <_ F )
4 3simpc 
 |-  ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( F e. ZZ /\ L e. ZZ ) )
5 4 adantr 
 |-  ( ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) /\ L <_ F ) -> ( F e. ZZ /\ L e. ZZ ) )
6 fzon 
 |-  ( ( F e. ZZ /\ L e. ZZ ) -> ( L <_ F <-> ( F ..^ L ) = (/) ) )
7 5 6 syl 
 |-  ( ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) /\ L <_ F ) -> ( L <_ F <-> ( F ..^ L ) = (/) ) )
8 3 7 mpbid 
 |-  ( ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) /\ L <_ F ) -> ( F ..^ L ) = (/) )
9 0ss 
 |-  (/) C_ dom W
10 8 9 eqsstrdi 
 |-  ( ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) /\ L <_ F ) -> ( F ..^ L ) C_ dom W )
11 10 iftrued 
 |-  ( ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) /\ L <_ F ) -> if ( ( F ..^ L ) C_ dom W , ( i e. ( 0 ..^ ( L - F ) ) |-> ( W ` ( i + F ) ) ) , (/) ) = ( i e. ( 0 ..^ ( L - F ) ) |-> ( W ` ( i + F ) ) ) )
12 fzo0n 
 |-  ( ( F e. ZZ /\ L e. ZZ ) -> ( L <_ F <-> ( 0 ..^ ( L - F ) ) = (/) ) )
13 12 biimpa 
 |-  ( ( ( F e. ZZ /\ L e. ZZ ) /\ L <_ F ) -> ( 0 ..^ ( L - F ) ) = (/) )
14 13 3adantl1 
 |-  ( ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) /\ L <_ F ) -> ( 0 ..^ ( L - F ) ) = (/) )
15 14 mpteq1d 
 |-  ( ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) /\ L <_ F ) -> ( i e. ( 0 ..^ ( L - F ) ) |-> ( W ` ( i + F ) ) ) = ( i e. (/) |-> ( W ` ( i + F ) ) ) )
16 mpt0 
 |-  ( i e. (/) |-> ( W ` ( i + F ) ) ) = (/)
17 15 16 eqtrdi 
 |-  ( ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) /\ L <_ F ) -> ( i e. ( 0 ..^ ( L - F ) ) |-> ( W ` ( i + F ) ) ) = (/) )
18 2 11 17 3eqtrd 
 |-  ( ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) /\ L <_ F ) -> ( W substr <. F , L >. ) = (/) )
19 18 ex 
 |-  ( ( W e. Word V /\ F e. ZZ /\ L e. ZZ ) -> ( L <_ F -> ( W substr <. F , L >. ) = (/) ) )