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 ) ) ) )