Metamath Proof Explorer


Theorem swrdfv0

Description: The first symbol in an extracted subword. (Contributed by AV, 27-Apr-2022)

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

Proof

Step Hyp Ref Expression
1 elfzofz
 |-  ( F e. ( 0 ..^ L ) -> F e. ( 0 ... L ) )
2 1 3anim2i
 |-  ( ( S e. Word A /\ F e. ( 0 ..^ L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) )
3 fzonnsub
 |-  ( F e. ( 0 ..^ L ) -> ( L - F ) e. NN )
4 3 3ad2ant2
 |-  ( ( S e. Word A /\ F e. ( 0 ..^ L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( L - F ) e. NN )
5 lbfzo0
 |-  ( 0 e. ( 0 ..^ ( L - F ) ) <-> ( L - F ) e. NN )
6 4 5 sylibr
 |-  ( ( S e. Word A /\ F e. ( 0 ..^ L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> 0 e. ( 0 ..^ ( L - F ) ) )
7 swrdfv
 |-  ( ( ( S e. Word A /\ F e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` S ) ) ) /\ 0 e. ( 0 ..^ ( L - F ) ) ) -> ( ( S substr <. F , L >. ) ` 0 ) = ( S ` ( 0 + F ) ) )
8 2 6 7 syl2anc
 |-  ( ( S e. Word A /\ F e. ( 0 ..^ L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( ( S substr <. F , L >. ) ` 0 ) = ( S ` ( 0 + F ) ) )
9 elfzoelz
 |-  ( F e. ( 0 ..^ L ) -> F e. ZZ )
10 9 zcnd
 |-  ( F e. ( 0 ..^ L ) -> F e. CC )
11 10 addid2d
 |-  ( F e. ( 0 ..^ L ) -> ( 0 + F ) = F )
12 11 fveq2d
 |-  ( F e. ( 0 ..^ L ) -> ( S ` ( 0 + F ) ) = ( S ` F ) )
13 12 3ad2ant2
 |-  ( ( S e. Word A /\ F e. ( 0 ..^ L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( S ` ( 0 + F ) ) = ( S ` F ) )
14 8 13 eqtrd
 |-  ( ( S e. Word A /\ F e. ( 0 ..^ L ) /\ L e. ( 0 ... ( # ` S ) ) ) -> ( ( S substr <. F , L >. ) ` 0 ) = ( S ` F ) )