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