Metamath Proof Explorer

Theorem swrd00

Description: A zero length substring. (Contributed by Stefan O'Rear, 27-Aug-2015)

Ref Expression
Assertion swrd00 
|- ( S substr <. X , X >. ) = (/)

Proof

Step Hyp Ref Expression
1 opelxp 
 |-  ( <. S , <. X , X >. >. e. ( _V X. ( ZZ X. ZZ ) ) <-> ( S e. _V /\ <. X , X >. e. ( ZZ X. ZZ ) ) )
2 opelxp 
 |-  ( <. X , X >. e. ( ZZ X. ZZ ) <-> ( X e. ZZ /\ X e. ZZ ) )
3 swrdval 
 |-  ( ( S e. _V /\ X e. ZZ /\ X e. ZZ ) -> ( S substr <. X , X >. ) = if ( ( X ..^ X ) C_ dom S , ( x e. ( 0 ..^ ( X - X ) ) |-> ( S ` ( x + X ) ) ) , (/) ) )
4 fzo0 
 |-  ( X ..^ X ) = (/)
5 0ss 
 |-  (/) C_ dom S
6 4 5 eqsstri 
 |-  ( X ..^ X ) C_ dom S
7 6 iftruei 
 |-  if ( ( X ..^ X ) C_ dom S , ( x e. ( 0 ..^ ( X - X ) ) |-> ( S ` ( x + X ) ) ) , (/) ) = ( x e. ( 0 ..^ ( X - X ) ) |-> ( S ` ( x + X ) ) )
8 zcn 
 |-  ( X e. ZZ -> X e. CC )
9 8 subidd 
 |-  ( X e. ZZ -> ( X - X ) = 0 )
10 9 oveq2d 
 |-  ( X e. ZZ -> ( 0 ..^ ( X - X ) ) = ( 0 ..^ 0 ) )
11 10 3ad2ant2 
 |-  ( ( S e. _V /\ X e. ZZ /\ X e. ZZ ) -> ( 0 ..^ ( X - X ) ) = ( 0 ..^ 0 ) )
12 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
13 11 12 eqtrdi 
 |-  ( ( S e. _V /\ X e. ZZ /\ X e. ZZ ) -> ( 0 ..^ ( X - X ) ) = (/) )
14 13 mpteq1d 
 |-  ( ( S e. _V /\ X e. ZZ /\ X e. ZZ ) -> ( x e. ( 0 ..^ ( X - X ) ) |-> ( S ` ( x + X ) ) ) = ( x e. (/) |-> ( S ` ( x + X ) ) ) )
15 mpt0 
 |-  ( x e. (/) |-> ( S ` ( x + X ) ) ) = (/)
16 14 15 eqtrdi 
 |-  ( ( S e. _V /\ X e. ZZ /\ X e. ZZ ) -> ( x e. ( 0 ..^ ( X - X ) ) |-> ( S ` ( x + X ) ) ) = (/) )
17 7 16 eqtrid 
 |-  ( ( S e. _V /\ X e. ZZ /\ X e. ZZ ) -> if ( ( X ..^ X ) C_ dom S , ( x e. ( 0 ..^ ( X - X ) ) |-> ( S ` ( x + X ) ) ) , (/) ) = (/) )
18 3 17 eqtrd 
 |-  ( ( S e. _V /\ X e. ZZ /\ X e. ZZ ) -> ( S substr <. X , X >. ) = (/) )
19 18 3expb 
 |-  ( ( S e. _V /\ ( X e. ZZ /\ X e. ZZ ) ) -> ( S substr <. X , X >. ) = (/) )
20 2 19 sylan2b 
 |-  ( ( S e. _V /\ <. X , X >. e. ( ZZ X. ZZ ) ) -> ( S substr <. X , X >. ) = (/) )
21 1 20 sylbi 
 |-  ( <. S , <. X , X >. >. e. ( _V X. ( ZZ X. ZZ ) ) -> ( S substr <. X , X >. ) = (/) )
22 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 ) ) ) ) , (/) ) )
23 ovex 
 |-  ( 0 ..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) e. _V
24 23 mptex 
 |-  ( x e. ( 0 ..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) ) e. _V
25 0ex 
 |-  (/) e. _V
26 24 25 ifex 
 |-  if ( ( ( 1st ` b ) ..^ ( 2nd ` b ) ) C_ dom s , ( x e. ( 0 ..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) ) , (/) ) e. _V
27 22 26 dmmpo 
 |-  dom substr = ( _V X. ( ZZ X. ZZ ) )
28 21 27 eleq2s 
 |-  ( <. S , <. X , X >. >. e. dom substr -> ( S substr <. X , X >. ) = (/) )
29 df-ov 
 |-  ( S substr <. X , X >. ) = ( substr ` <. S , <. X , X >. >. )
30 ndmfv 
 |-  ( -. <. S , <. X , X >. >. e. dom substr -> ( substr ` <. S , <. X , X >. >. ) = (/) )
31 29 30 eqtrid 
 |-  ( -. <. S , <. X , X >. >. e. dom substr -> ( S substr <. X , X >. ) = (/) )
32 28 31 pm2.61i 
 |-  ( S substr <. X , X >. ) = (/)