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 Word A I 0 ..^ W W substr I I + 1 = ⟨“ W I ”⟩

Proof

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