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