Metamath Proof Explorer

Theorem swrdfv2

Description: A symbol in an extracted subword, indexed using the word's indices. (Contributed by AV, 5-May-2020)

Ref Expression
Assertion swrdfv2 
|- ( ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) /\ X e. ( F ..^ L ) ) -> ( ( S substr <. F , L >. ) ` ( X - F ) ) = ( S ` X ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> S e. Word V )
2 simpl 
 |-  ( ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) -> F e. NN0 )
3 eluznn0 
 |-  ( ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) -> L e. NN0 )
4 eluzle 
 |-  ( L e. ( ZZ>= ` F ) -> F <_ L )
5 4 adantl 
 |-  ( ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) -> F <_ L )
6 2 3 5 3jca 
 |-  ( ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) -> ( F e. NN0 /\ L e. NN0 /\ F <_ L ) )
7 6 3ad2ant2 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> ( F e. NN0 /\ L e. NN0 /\ F <_ L ) )
8 elfz2nn0 
 |-  ( F e. ( 0 ... L ) <-> ( F e. NN0 /\ L e. NN0 /\ F <_ L ) )
9 7 8 sylibr 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> F e. ( 0 ... L ) )
10 3 anim1i 
 |-  ( ( ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> ( L e. NN0 /\ L <_ ( # ` S ) ) )
11 10 3adant1 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> ( L e. NN0 /\ L <_ ( # ` S ) ) )
12 lencl 
 |-  ( S e. Word V -> ( # ` S ) e. NN0 )
13 12 3ad2ant1 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> ( # ` S ) e. NN0 )
14 fznn0 
 |-  ( ( # ` S ) e. NN0 -> ( L e. ( 0 ... ( # ` S ) ) <-> ( L e. NN0 /\ L <_ ( # ` S ) ) ) )
15 13 14 syl 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> ( L e. ( 0 ... ( # ` S ) ) <-> ( L e. NN0 /\ L <_ ( # ` S ) ) ) )
16 11 15 mpbird 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> L e. ( 0 ... ( # ` S ) ) )
17 1 9 16 3jca 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> ( S e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) )
18 17 adantr 
 |-  ( ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) /\ X e. ( F ..^ L ) ) -> ( S e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) )
19 nn0cn 
 |-  ( F e. NN0 -> F e. CC )
20 eluzelcn 
 |-  ( L e. ( ZZ>= ` F ) -> L e. CC )
21 pncan3 
 |-  ( ( F e. CC /\ L e. CC ) -> ( F + ( L - F ) ) = L )
22 19 20 21 syl2an 
 |-  ( ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) -> ( F + ( L - F ) ) = L )
23 22 eqcomd 
 |-  ( ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) -> L = ( F + ( L - F ) ) )
24 23 3ad2ant2 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> L = ( F + ( L - F ) ) )
25 24 oveq2d 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> ( F ..^ L ) = ( F ..^ ( F + ( L - F ) ) ) )
26 25 eleq2d 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> ( X e. ( F ..^ L ) <-> X e. ( F ..^ ( F + ( L - F ) ) ) ) )
27 26 biimpa 
 |-  ( ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) /\ X e. ( F ..^ L ) ) -> X e. ( F ..^ ( F + ( L - F ) ) ) )
28 eluzelz 
 |-  ( L e. ( ZZ>= ` F ) -> L e. ZZ )
29 28 adantl 
 |-  ( ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) -> L e. ZZ )
30 nn0z 
 |-  ( F e. NN0 -> F e. ZZ )
31 30 adantr 
 |-  ( ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) -> F e. ZZ )
32 29 31 zsubcld 
 |-  ( ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) -> ( L - F ) e. ZZ )
33 32 3ad2ant2 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> ( L - F ) e. ZZ )
34 33 adantr 
 |-  ( ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) /\ X e. ( F ..^ L ) ) -> ( L - F ) e. ZZ )
35 fzosubel3 
 |-  ( ( X e. ( F ..^ ( F + ( L - F ) ) ) /\ ( L - F ) e. ZZ ) -> ( X - F ) e. ( 0 ..^ ( L - F ) ) )
36 27 34 35 syl2anc 
 |-  ( ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) /\ X e. ( F ..^ L ) ) -> ( X - F ) e. ( 0 ..^ ( L - F ) ) )
37 swrdfv 
 |-  ( ( ( S e. Word V /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) /\ ( X - F ) e. ( 0 ..^ ( L - F ) ) ) -> ( ( S substr <. F , L >. ) ` ( X - F ) ) = ( S ` ( ( X - F ) + F ) ) )
38 18 36 37 syl2anc 
 |-  ( ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) /\ X e. ( F ..^ L ) ) -> ( ( S substr <. F , L >. ) ` ( X - F ) ) = ( S ` ( ( X - F ) + F ) ) )
39 elfzoelz 
 |-  ( X e. ( F ..^ L ) -> X e. ZZ )
40 39 zcnd 
 |-  ( X e. ( F ..^ L ) -> X e. CC )
41 19 adantr 
 |-  ( ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) -> F e. CC )
42 41 3ad2ant2 
 |-  ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) -> F e. CC )
43 npcan 
 |-  ( ( X e. CC /\ F e. CC ) -> ( ( X - F ) + F ) = X )
44 40 42 43 syl2anr 
 |-  ( ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) /\ X e. ( F ..^ L ) ) -> ( ( X - F ) + F ) = X )
45 44 fveq2d 
 |-  ( ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) /\ X e. ( F ..^ L ) ) -> ( S ` ( ( X - F ) + F ) ) = ( S ` X ) )
46 38 45 eqtrd 
 |-  ( ( ( S e. Word V /\ ( F e. NN0 /\ L e. ( ZZ>= ` F ) ) /\ L <_ ( # ` S ) ) /\ X e. ( F ..^ L ) ) -> ( ( S substr <. F , L >. ) ` ( X - F ) ) = ( S ` X ) )