Metamath Proof Explorer

Theorem swrd0

Description: A subword of an empty set is always the empty set. (Contributed by AV, 31-Mar-2018) (Revised by AV, 20-Oct-2018) (Proof shortened by AV, 2-May-2020)

Ref Expression
Assertion swrd0 
|- ( (/) substr <. F , L >. ) = (/)

Proof

Step Hyp Ref Expression
1 opelxp 
 |-  ( <. (/) , <. F , L >. >. e. ( _V X. ( ZZ X. ZZ ) ) <-> ( (/) e. _V /\ <. F , L >. e. ( ZZ X. ZZ ) ) )
2 opelxp 
 |-  ( <. F , L >. e. ( ZZ X. ZZ ) <-> ( F e. ZZ /\ L e. ZZ ) )
3 swrdval 
 |-  ( ( (/) e. _V /\ F e. ZZ /\ L e. ZZ ) -> ( (/) substr <. F , L >. ) = if ( ( F ..^ L ) C_ dom (/) , ( x e. ( 0 ..^ ( L - F ) ) |-> ( (/) ` ( x + F ) ) ) , (/) ) )
4 fzonlt0 
 |-  ( ( F e. ZZ /\ L e. ZZ ) -> ( -. F < L <-> ( F ..^ L ) = (/) ) )
5 4 biimprd 
 |-  ( ( F e. ZZ /\ L e. ZZ ) -> ( ( F ..^ L ) = (/) -> -. F < L ) )
6 5 con2d 
 |-  ( ( F e. ZZ /\ L e. ZZ ) -> ( F < L -> -. ( F ..^ L ) = (/) ) )
7 6 impcom 
 |-  ( ( F < L /\ ( F e. ZZ /\ L e. ZZ ) ) -> -. ( F ..^ L ) = (/) )
8 ss0 
 |-  ( ( F ..^ L ) C_ (/) -> ( F ..^ L ) = (/) )
9 7 8 nsyl 
 |-  ( ( F < L /\ ( F e. ZZ /\ L e. ZZ ) ) -> -. ( F ..^ L ) C_ (/) )
10 dm0 
 |-  dom (/) = (/)
11 10 a1i 
 |-  ( ( F < L /\ ( F e. ZZ /\ L e. ZZ ) ) -> dom (/) = (/) )
12 11 sseq2d 
 |-  ( ( F < L /\ ( F e. ZZ /\ L e. ZZ ) ) -> ( ( F ..^ L ) C_ dom (/) <-> ( F ..^ L ) C_ (/) ) )
13 9 12 mtbird 
 |-  ( ( F < L /\ ( F e. ZZ /\ L e. ZZ ) ) -> -. ( F ..^ L ) C_ dom (/) )
14 13 iffalsed 
 |-  ( ( F < L /\ ( F e. ZZ /\ L e. ZZ ) ) -> if ( ( F ..^ L ) C_ dom (/) , ( x e. ( 0 ..^ ( L - F ) ) |-> ( (/) ` ( x + F ) ) ) , (/) ) = (/) )
15 ssidd 
 |-  ( ( -. F < L /\ ( F e. ZZ /\ L e. ZZ ) ) -> (/) C_ (/) )
16 4 biimpac 
 |-  ( ( -. F < L /\ ( F e. ZZ /\ L e. ZZ ) ) -> ( F ..^ L ) = (/) )
17 10 a1i 
 |-  ( ( -. F < L /\ ( F e. ZZ /\ L e. ZZ ) ) -> dom (/) = (/) )
18 15 16 17 3sstr4d 
 |-  ( ( -. F < L /\ ( F e. ZZ /\ L e. ZZ ) ) -> ( F ..^ L ) C_ dom (/) )
19 18 iftrued 
 |-  ( ( -. F < L /\ ( F e. ZZ /\ L e. ZZ ) ) -> if ( ( F ..^ L ) C_ dom (/) , ( x e. ( 0 ..^ ( L - F ) ) |-> ( (/) ` ( x + F ) ) ) , (/) ) = ( x e. ( 0 ..^ ( L - F ) ) |-> ( (/) ` ( x + F ) ) ) )
20 zre 
 |-  ( L e. ZZ -> L e. RR )
21 zre 
 |-  ( F e. ZZ -> F e. RR )
22 lenlt 
 |-  ( ( L e. RR /\ F e. RR ) -> ( L <_ F <-> -. F < L ) )
23 22 bicomd 
 |-  ( ( L e. RR /\ F e. RR ) -> ( -. F < L <-> L <_ F ) )
24 20 21 23 syl2anr 
 |-  ( ( F e. ZZ /\ L e. ZZ ) -> ( -. F < L <-> L <_ F ) )
25 fzo0n 
 |-  ( ( F e. ZZ /\ L e. ZZ ) -> ( L <_ F <-> ( 0 ..^ ( L - F ) ) = (/) ) )
26 24 25 bitrd 
 |-  ( ( F e. ZZ /\ L e. ZZ ) -> ( -. F < L <-> ( 0 ..^ ( L - F ) ) = (/) ) )
27 26 biimpac 
 |-  ( ( -. F < L /\ ( F e. ZZ /\ L e. ZZ ) ) -> ( 0 ..^ ( L - F ) ) = (/) )
28 27 mpteq1d 
 |-  ( ( -. F < L /\ ( F e. ZZ /\ L e. ZZ ) ) -> ( x e. ( 0 ..^ ( L - F ) ) |-> ( (/) ` ( x + F ) ) ) = ( x e. (/) |-> ( (/) ` ( x + F ) ) ) )
29 28 dmeqd 
 |-  ( ( -. F < L /\ ( F e. ZZ /\ L e. ZZ ) ) -> dom ( x e. ( 0 ..^ ( L - F ) ) |-> ( (/) ` ( x + F ) ) ) = dom ( x e. (/) |-> ( (/) ` ( x + F ) ) ) )
30 ral0 
 |-  A. x e. (/) ( (/) ` ( x + F ) ) e. _V
31 dmmptg 
 |-  ( A. x e. (/) ( (/) ` ( x + F ) ) e. _V -> dom ( x e. (/) |-> ( (/) ` ( x + F ) ) ) = (/) )
32 30 31 mp1i 
 |-  ( ( -. F < L /\ ( F e. ZZ /\ L e. ZZ ) ) -> dom ( x e. (/) |-> ( (/) ` ( x + F ) ) ) = (/) )
33 29 32 eqtrd 
 |-  ( ( -. F < L /\ ( F e. ZZ /\ L e. ZZ ) ) -> dom ( x e. ( 0 ..^ ( L - F ) ) |-> ( (/) ` ( x + F ) ) ) = (/) )
34 mptrel 
 |-  Rel ( x e. ( 0 ..^ ( L - F ) ) |-> ( (/) ` ( x + F ) ) )
35 reldm0 
 |-  ( Rel ( x e. ( 0 ..^ ( L - F ) ) |-> ( (/) ` ( x + F ) ) ) -> ( ( x e. ( 0 ..^ ( L - F ) ) |-> ( (/) ` ( x + F ) ) ) = (/) <-> dom ( x e. ( 0 ..^ ( L - F ) ) |-> ( (/) ` ( x + F ) ) ) = (/) ) )
36 34 35 mp1i 
 |-  ( ( -. F < L /\ ( F e. ZZ /\ L e. ZZ ) ) -> ( ( x e. ( 0 ..^ ( L - F ) ) |-> ( (/) ` ( x + F ) ) ) = (/) <-> dom ( x e. ( 0 ..^ ( L - F ) ) |-> ( (/) ` ( x + F ) ) ) = (/) ) )
37 33 36 mpbird 
 |-  ( ( -. F < L /\ ( F e. ZZ /\ L e. ZZ ) ) -> ( x e. ( 0 ..^ ( L - F ) ) |-> ( (/) ` ( x + F ) ) ) = (/) )
38 19 37 eqtrd 
 |-  ( ( -. F < L /\ ( F e. ZZ /\ L e. ZZ ) ) -> if ( ( F ..^ L ) C_ dom (/) , ( x e. ( 0 ..^ ( L - F ) ) |-> ( (/) ` ( x + F ) ) ) , (/) ) = (/) )
39 14 38 pm2.61ian 
 |-  ( ( F e. ZZ /\ L e. ZZ ) -> if ( ( F ..^ L ) C_ dom (/) , ( x e. ( 0 ..^ ( L - F ) ) |-> ( (/) ` ( x + F ) ) ) , (/) ) = (/) )
40 39 3adant1 
 |-  ( ( (/) e. _V /\ F e. ZZ /\ L e. ZZ ) -> if ( ( F ..^ L ) C_ dom (/) , ( x e. ( 0 ..^ ( L - F ) ) |-> ( (/) ` ( x + F ) ) ) , (/) ) = (/) )
41 3 40 eqtrd 
 |-  ( ( (/) e. _V /\ F e. ZZ /\ L e. ZZ ) -> ( (/) substr <. F , L >. ) = (/) )
42 41 3expb 
 |-  ( ( (/) e. _V /\ ( F e. ZZ /\ L e. ZZ ) ) -> ( (/) substr <. F , L >. ) = (/) )
43 2 42 sylan2b 
 |-  ( ( (/) e. _V /\ <. F , L >. e. ( ZZ X. ZZ ) ) -> ( (/) substr <. F , L >. ) = (/) )
44 1 43 sylbi 
 |-  ( <. (/) , <. F , L >. >. e. ( _V X. ( ZZ X. ZZ ) ) -> ( (/) substr <. F , L >. ) = (/) )
45 df-substr 
 |-  substr = ( s e. _V , b e. ( ZZ X. ZZ ) |-> if ( ( ( 1st ` b ) ..^ ( 2nd ` b ) ) C_ dom s , ( z e. ( 0 ..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( z + ( 1st ` b ) ) ) ) , (/) ) )
46 ovex 
 |-  ( 0 ..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) e. _V
47 46 mptex 
 |-  ( z e. ( 0 ..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( z + ( 1st ` b ) ) ) ) e. _V
48 0ex 
 |-  (/) e. _V
49 47 48 ifex 
 |-  if ( ( ( 1st ` b ) ..^ ( 2nd ` b ) ) C_ dom s , ( z e. ( 0 ..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( z + ( 1st ` b ) ) ) ) , (/) ) e. _V
50 45 49 dmmpo 
 |-  dom substr = ( _V X. ( ZZ X. ZZ ) )
51 44 50 eleq2s 
 |-  ( <. (/) , <. F , L >. >. e. dom substr -> ( (/) substr <. F , L >. ) = (/) )
52 df-ov 
 |-  ( (/) substr <. F , L >. ) = ( substr ` <. (/) , <. F , L >. >. )
53 ndmfv 
 |-  ( -. <. (/) , <. F , L >. >. e. dom substr -> ( substr ` <. (/) , <. F , L >. >. ) = (/) )
54 52 53 eqtrid 
 |-  ( -. <. (/) , <. F , L >. >. e. dom substr -> ( (/) substr <. F , L >. ) = (/) )
55 51 54 pm2.61i 
 |-  ( (/) substr <. F , L >. ) = (/)