Metamath Proof Explorer

Theorem swrdval

Description: Value of a subword. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion swrdval 
|- ( ( S e. V /\ F e. ZZ /\ L e. ZZ ) -> ( S substr <. F , L >. ) = if ( ( F ..^ L ) C_ dom S , ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) , (/) ) )

Proof

Step Hyp Ref Expression
1 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 ) ) ) ) , (/) ) )
2 1 a1i 
 |-  ( ( S e. V /\ F e. ZZ /\ L e. ZZ ) -> 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 ) ) ) ) , (/) ) ) )
3 simprl 
 |-  ( ( ( S e. V /\ F e. ZZ /\ L e. ZZ ) /\ ( s = S /\ b = <. F , L >. ) ) -> s = S )
4 fveq2 
 |-  ( b = <. F , L >. -> ( 1st ` b ) = ( 1st ` <. F , L >. ) )
5 4 adantl 
 |-  ( ( s = S /\ b = <. F , L >. ) -> ( 1st ` b ) = ( 1st ` <. F , L >. ) )
6 op1stg 
 |-  ( ( F e. ZZ /\ L e. ZZ ) -> ( 1st ` <. F , L >. ) = F )
7 6 3adant1 
 |-  ( ( S e. V /\ F e. ZZ /\ L e. ZZ ) -> ( 1st ` <. F , L >. ) = F )
8 5 7 sylan9eqr 
 |-  ( ( ( S e. V /\ F e. ZZ /\ L e. ZZ ) /\ ( s = S /\ b = <. F , L >. ) ) -> ( 1st ` b ) = F )
9 fveq2 
 |-  ( b = <. F , L >. -> ( 2nd ` b ) = ( 2nd ` <. F , L >. ) )
10 9 adantl 
 |-  ( ( s = S /\ b = <. F , L >. ) -> ( 2nd ` b ) = ( 2nd ` <. F , L >. ) )
11 op2ndg 
 |-  ( ( F e. ZZ /\ L e. ZZ ) -> ( 2nd ` <. F , L >. ) = L )
12 11 3adant1 
 |-  ( ( S e. V /\ F e. ZZ /\ L e. ZZ ) -> ( 2nd ` <. F , L >. ) = L )
13 10 12 sylan9eqr 
 |-  ( ( ( S e. V /\ F e. ZZ /\ L e. ZZ ) /\ ( s = S /\ b = <. F , L >. ) ) -> ( 2nd ` b ) = L )
14 simp2 
 |-  ( ( s = S /\ ( 1st ` b ) = F /\ ( 2nd ` b ) = L ) -> ( 1st ` b ) = F )
15 simp3 
 |-  ( ( s = S /\ ( 1st ` b ) = F /\ ( 2nd ` b ) = L ) -> ( 2nd ` b ) = L )
16 14 15 oveq12d 
 |-  ( ( s = S /\ ( 1st ` b ) = F /\ ( 2nd ` b ) = L ) -> ( ( 1st ` b ) ..^ ( 2nd ` b ) ) = ( F ..^ L ) )
17 simp1 
 |-  ( ( s = S /\ ( 1st ` b ) = F /\ ( 2nd ` b ) = L ) -> s = S )
18 17 dmeqd 
 |-  ( ( s = S /\ ( 1st ` b ) = F /\ ( 2nd ` b ) = L ) -> dom s = dom S )
19 16 18 sseq12d 
 |-  ( ( s = S /\ ( 1st ` b ) = F /\ ( 2nd ` b ) = L ) -> ( ( ( 1st ` b ) ..^ ( 2nd ` b ) ) C_ dom s <-> ( F ..^ L ) C_ dom S ) )
20 15 14 oveq12d 
 |-  ( ( s = S /\ ( 1st ` b ) = F /\ ( 2nd ` b ) = L ) -> ( ( 2nd ` b ) - ( 1st ` b ) ) = ( L - F ) )
21 20 oveq2d 
 |-  ( ( s = S /\ ( 1st ` b ) = F /\ ( 2nd ` b ) = L ) -> ( 0 ..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) = ( 0 ..^ ( L - F ) ) )
22 14 oveq2d 
 |-  ( ( s = S /\ ( 1st ` b ) = F /\ ( 2nd ` b ) = L ) -> ( x + ( 1st ` b ) ) = ( x + F ) )
23 17 22 fveq12d 
 |-  ( ( s = S /\ ( 1st ` b ) = F /\ ( 2nd ` b ) = L ) -> ( s ` ( x + ( 1st ` b ) ) ) = ( S ` ( x + F ) ) )
24 21 23 mpteq12dv 
 |-  ( ( s = S /\ ( 1st ` b ) = F /\ ( 2nd ` b ) = L ) -> ( x e. ( 0 ..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) ) = ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) )
25 19 24 ifbieq1d 
 |-  ( ( s = S /\ ( 1st ` b ) = F /\ ( 2nd ` b ) = L ) -> if ( ( ( 1st ` b ) ..^ ( 2nd ` b ) ) C_ dom s , ( x e. ( 0 ..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) ) , (/) ) = if ( ( F ..^ L ) C_ dom S , ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) , (/) ) )
26 3 8 13 25 syl3anc 
 |-  ( ( ( S e. V /\ F e. ZZ /\ L e. ZZ ) /\ ( s = S /\ b = <. F , L >. ) ) -> if ( ( ( 1st ` b ) ..^ ( 2nd ` b ) ) C_ dom s , ( x e. ( 0 ..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) ) , (/) ) = if ( ( F ..^ L ) C_ dom S , ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) , (/) ) )
27 elex 
 |-  ( S e. V -> S e. _V )
28 27 3ad2ant1 
 |-  ( ( S e. V /\ F e. ZZ /\ L e. ZZ ) -> S e. _V )
29 opelxpi 
 |-  ( ( F e. ZZ /\ L e. ZZ ) -> <. F , L >. e. ( ZZ X. ZZ ) )
30 29 3adant1 
 |-  ( ( S e. V /\ F e. ZZ /\ L e. ZZ ) -> <. F , L >. e. ( ZZ X. ZZ ) )
31 ovex 
 |-  ( 0 ..^ ( L - F ) ) e. _V
32 31 mptex 
 |-  ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) e. _V
33 0ex 
 |-  (/) e. _V
34 32 33 ifex 
 |-  if ( ( F ..^ L ) C_ dom S , ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) , (/) ) e. _V
35 34 a1i 
 |-  ( ( S e. V /\ F e. ZZ /\ L e. ZZ ) -> if ( ( F ..^ L ) C_ dom S , ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) , (/) ) e. _V )
36 2 26 28 30 35 ovmpod 
 |-  ( ( S e. V /\ F e. ZZ /\ L e. ZZ ) -> ( S substr <. F , L >. ) = if ( ( F ..^ L ) C_ dom S , ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) , (/) ) )