Metamath Proof Explorer


Theorem swrds1

Description: Extract a single symbol from a word. (Contributed by Stefan O'Rear, 23-Aug-2015)

Ref Expression
Assertion swrds1
|- ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( W substr <. I , ( I + 1 ) >. ) = <" ( W ` I ) "> )

Proof

Step Hyp Ref Expression
1 swrdcl
 |-  ( W e. Word A -> ( W substr <. I , ( I + 1 ) >. ) e. Word A )
2 simpl
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> W e. Word A )
3 elfzouz
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> I e. ( ZZ>= ` 0 ) )
4 3 adantl
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> I e. ( ZZ>= ` 0 ) )
5 elfzoelz
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> I e. ZZ )
6 5 adantl
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> I e. ZZ )
7 uzid
 |-  ( I e. ZZ -> I e. ( ZZ>= ` I ) )
8 peano2uz
 |-  ( I e. ( ZZ>= ` I ) -> ( I + 1 ) e. ( ZZ>= ` I ) )
9 6 7 8 3syl
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( I + 1 ) e. ( ZZ>= ` I ) )
10 elfzuzb
 |-  ( I e. ( 0 ... ( I + 1 ) ) <-> ( I e. ( ZZ>= ` 0 ) /\ ( I + 1 ) e. ( ZZ>= ` I ) ) )
11 4 9 10 sylanbrc
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> I e. ( 0 ... ( I + 1 ) ) )
12 fzofzp1
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> ( I + 1 ) e. ( 0 ... ( # ` W ) ) )
13 12 adantl
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( I + 1 ) e. ( 0 ... ( # ` W ) ) )
14 swrdlen
 |-  ( ( W e. Word A /\ I e. ( 0 ... ( I + 1 ) ) /\ ( I + 1 ) e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W substr <. I , ( I + 1 ) >. ) ) = ( ( I + 1 ) - I ) )
15 2 11 13 14 syl3anc
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( # ` ( W substr <. I , ( I + 1 ) >. ) ) = ( ( I + 1 ) - I ) )
16 6 zcnd
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> I e. CC )
17 ax-1cn
 |-  1 e. CC
18 pncan2
 |-  ( ( I e. CC /\ 1 e. CC ) -> ( ( I + 1 ) - I ) = 1 )
19 16 17 18 sylancl
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( I + 1 ) - I ) = 1 )
20 15 19 eqtrd
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( # ` ( W substr <. I , ( I + 1 ) >. ) ) = 1 )
21 eqs1
 |-  ( ( ( W substr <. I , ( I + 1 ) >. ) e. Word A /\ ( # ` ( W substr <. I , ( I + 1 ) >. ) ) = 1 ) -> ( W substr <. I , ( I + 1 ) >. ) = <" ( ( W substr <. I , ( I + 1 ) >. ) ` 0 ) "> )
22 1 20 21 syl2an2r
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( W substr <. I , ( I + 1 ) >. ) = <" ( ( W substr <. I , ( I + 1 ) >. ) ` 0 ) "> )
23 0z
 |-  0 e. ZZ
24 snidg
 |-  ( 0 e. ZZ -> 0 e. { 0 } )
25 23 24 ax-mp
 |-  0 e. { 0 }
26 19 oveq2d
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( 0 ..^ ( ( I + 1 ) - I ) ) = ( 0 ..^ 1 ) )
27 fzo01
 |-  ( 0 ..^ 1 ) = { 0 }
28 26 27 eqtrdi
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( 0 ..^ ( ( I + 1 ) - I ) ) = { 0 } )
29 25 28 eleqtrrid
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> 0 e. ( 0 ..^ ( ( I + 1 ) - I ) ) )
30 swrdfv
 |-  ( ( ( W e. Word A /\ I e. ( 0 ... ( I + 1 ) ) /\ ( I + 1 ) e. ( 0 ... ( # ` W ) ) ) /\ 0 e. ( 0 ..^ ( ( I + 1 ) - I ) ) ) -> ( ( W substr <. I , ( I + 1 ) >. ) ` 0 ) = ( W ` ( 0 + I ) ) )
31 2 11 13 29 30 syl31anc
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W substr <. I , ( I + 1 ) >. ) ` 0 ) = ( W ` ( 0 + I ) ) )
32 addid2
 |-  ( I e. CC -> ( 0 + I ) = I )
33 32 eqcomd
 |-  ( I e. CC -> I = ( 0 + I ) )
34 16 33 syl
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> I = ( 0 + I ) )
35 34 fveq2d
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` I ) = ( W ` ( 0 + I ) ) )
36 31 35 eqtr4d
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W substr <. I , ( I + 1 ) >. ) ` 0 ) = ( W ` I ) )
37 36 s1eqd
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> <" ( ( W substr <. I , ( I + 1 ) >. ) ` 0 ) "> = <" ( W ` I ) "> )
38 22 37 eqtrd
 |-  ( ( W e. Word A /\ I e. ( 0 ..^ ( # ` W ) ) ) -> ( W substr <. I , ( I + 1 ) >. ) = <" ( W ` I ) "> )