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 syl6eq 
 |-  ( ( 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 ) "> )