Metamath Proof Explorer

Theorem swrdval2

Description: Value of the subword extractor in its intended domain. (Contributed by Stefan O'Rear, 15-Aug-2015) (Proof shortened by AV, 2-May-2020)

Ref Expression
Assertion swrdval2 
|- ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S substr <. F , L >. ) = ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> S e. Word A )
2 elfzelz 
 |-  ( F e. ( 0 ... L ) -> F e. ZZ )
3 2 3ad2ant2 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> F e. ZZ )
4 elfzelz 
 |-  ( L e. ( 0 ... ( # ` S ) ) -> L e. ZZ )
5 4 3ad2ant3 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> L e. ZZ )
6 swrdval 
 |-  ( ( S e. Word A /\ F e. ZZ /\ L e. ZZ ) -> ( S substr <. F , L >. ) = if ( ( F ..^ L ) C_ dom S , ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) , (/) ) )
7 1 3 5 6 syl3anc 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S substr <. F , L >. ) = if ( ( F ..^ L ) C_ dom S , ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) , (/) ) )
8 elfzuz 
 |-  ( F e. ( 0 ... L ) -> F e. ( ZZ>= ` 0 ) )
9 8 3ad2ant2 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> F e. ( ZZ>= ` 0 ) )
10 fzoss1 
 |-  ( F e. ( ZZ>= ` 0 ) -> ( F ..^ L ) C_ ( 0 ..^ L ) )
11 9 10 syl 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( F ..^ L ) C_ ( 0 ..^ L ) )
12 elfzuz3 
 |-  ( L e. ( 0 ... ( # ` S ) ) -> ( # ` S ) e. ( ZZ>= ` L ) )
13 12 3ad2ant3 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( # ` S ) e. ( ZZ>= ` L ) )
14 fzoss2 
 |-  ( ( # ` S ) e. ( ZZ>= ` L ) -> ( 0 ..^ L ) C_ ( 0 ..^ ( # ` S ) ) )
15 13 14 syl 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( 0 ..^ L ) C_ ( 0 ..^ ( # ` S ) ) )
16 11 15 sstrd 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( F ..^ L ) C_ ( 0 ..^ ( # ` S ) ) )
17 wrddm 
 |-  ( S e. Word A -> dom S = ( 0 ..^ ( # ` S ) ) )
18 17 3ad2ant1 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> dom S = ( 0 ..^ ( # ` S ) ) )
19 16 18 sseqtrrd 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( F ..^ L ) C_ dom S )
20 19 iftrued 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> if ( ( F ..^ L ) C_ dom S , ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) , (/) ) = ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) )
21 7 20 eqtrd 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S substr <. F , L >. ) = ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) )