Metamath Proof Explorer

Theorem swrdfv

Description: A symbol in an extracted subword, indexed using the subword's indices. (Contributed by Stefan O'Rear, 16-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 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 ) ) ) )
2 1 fveq1d 
 |-  ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( ( S substr <. F , L >. ) ` X ) = ( ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) ` X ) )
3 fvoveq1 
 |-  ( x = X -> ( S ` ( x + F ) ) = ( S ` ( X + F ) ) )
4 eqid 
 |-  ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) = ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) )
5 fvex 
 |-  ( S ` ( X + F ) ) e. _V
6 3 4 5 fvmpt 
 |-  ( X e. ( 0 ..^ ( L - F ) ) -> ( ( x e. ( 0 ..^ ( L - F ) ) |-> ( S ` ( x + F ) ) ) ` X ) = ( S ` ( X + F ) ) )
7 2 6 sylan9eq 
 |-  ( ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) /\ X e. ( 0 ..^ ( L - F ) ) ) -> ( ( S substr <. F , L >. ) ` X ) = ( S ` ( X + F ) ) )