Step |
Hyp |
Ref |
Expression |
1 |
|
swrdcl |
⊢ ( 𝑊 ∈ Word 𝐴 → ( 𝑊 substr 〈 𝐼 , ( 𝐼 + 1 ) 〉 ) ∈ Word 𝐴 ) |
2 |
|
simpl |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑊 ∈ Word 𝐴 ) |
3 |
|
elfzouz |
⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ( ℤ≥ ‘ 0 ) ) |
4 |
3
|
adantl |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐼 ∈ ( ℤ≥ ‘ 0 ) ) |
5 |
|
elfzoelz |
⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ℤ ) |
6 |
5
|
adantl |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐼 ∈ ℤ ) |
7 |
|
uzid |
⊢ ( 𝐼 ∈ ℤ → 𝐼 ∈ ( ℤ≥ ‘ 𝐼 ) ) |
8 |
|
peano2uz |
⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 𝐼 ) → ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ 𝐼 ) ) |
9 |
6 7 8
|
3syl |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ 𝐼 ) ) |
10 |
|
elfzuzb |
⊢ ( 𝐼 ∈ ( 0 ... ( 𝐼 + 1 ) ) ↔ ( 𝐼 ∈ ( ℤ≥ ‘ 0 ) ∧ ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ 𝐼 ) ) ) |
11 |
4 9 10
|
sylanbrc |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐼 ∈ ( 0 ... ( 𝐼 + 1 ) ) ) |
12 |
|
fzofzp1 |
⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝐼 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) |
13 |
12
|
adantl |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐼 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) |
14 |
|
swrdlen |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ... ( 𝐼 + 1 ) ) ∧ ( 𝐼 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 substr 〈 𝐼 , ( 𝐼 + 1 ) 〉 ) ) = ( ( 𝐼 + 1 ) − 𝐼 ) ) |
15 |
2 11 13 14
|
syl3anc |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 substr 〈 𝐼 , ( 𝐼 + 1 ) 〉 ) ) = ( ( 𝐼 + 1 ) − 𝐼 ) ) |
16 |
6
|
zcnd |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐼 ∈ ℂ ) |
17 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
18 |
|
pncan2 |
⊢ ( ( 𝐼 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐼 + 1 ) − 𝐼 ) = 1 ) |
19 |
16 17 18
|
sylancl |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐼 + 1 ) − 𝐼 ) = 1 ) |
20 |
15 19
|
eqtrd |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 substr 〈 𝐼 , ( 𝐼 + 1 ) 〉 ) ) = 1 ) |
21 |
|
eqs1 |
⊢ ( ( ( 𝑊 substr 〈 𝐼 , ( 𝐼 + 1 ) 〉 ) ∈ Word 𝐴 ∧ ( ♯ ‘ ( 𝑊 substr 〈 𝐼 , ( 𝐼 + 1 ) 〉 ) ) = 1 ) → ( 𝑊 substr 〈 𝐼 , ( 𝐼 + 1 ) 〉 ) = 〈“ ( ( 𝑊 substr 〈 𝐼 , ( 𝐼 + 1 ) 〉 ) ‘ 0 ) ”〉 ) |
22 |
1 20 21
|
syl2an2r |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr 〈 𝐼 , ( 𝐼 + 1 ) 〉 ) = 〈“ ( ( 𝑊 substr 〈 𝐼 , ( 𝐼 + 1 ) 〉 ) ‘ 0 ) ”〉 ) |
23 |
|
0z |
⊢ 0 ∈ ℤ |
24 |
|
snidg |
⊢ ( 0 ∈ ℤ → 0 ∈ { 0 } ) |
25 |
23 24
|
ax-mp |
⊢ 0 ∈ { 0 } |
26 |
19
|
oveq2d |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 0 ..^ ( ( 𝐼 + 1 ) − 𝐼 ) ) = ( 0 ..^ 1 ) ) |
27 |
|
fzo01 |
⊢ ( 0 ..^ 1 ) = { 0 } |
28 |
26 27
|
eqtrdi |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 0 ..^ ( ( 𝐼 + 1 ) − 𝐼 ) ) = { 0 } ) |
29 |
25 28
|
eleqtrrid |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 0 ∈ ( 0 ..^ ( ( 𝐼 + 1 ) − 𝐼 ) ) ) |
30 |
|
swrdfv |
⊢ ( ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ... ( 𝐼 + 1 ) ) ∧ ( 𝐼 + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) ∧ 0 ∈ ( 0 ..^ ( ( 𝐼 + 1 ) − 𝐼 ) ) ) → ( ( 𝑊 substr 〈 𝐼 , ( 𝐼 + 1 ) 〉 ) ‘ 0 ) = ( 𝑊 ‘ ( 0 + 𝐼 ) ) ) |
31 |
2 11 13 29 30
|
syl31anc |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 substr 〈 𝐼 , ( 𝐼 + 1 ) 〉 ) ‘ 0 ) = ( 𝑊 ‘ ( 0 + 𝐼 ) ) ) |
32 |
|
addid2 |
⊢ ( 𝐼 ∈ ℂ → ( 0 + 𝐼 ) = 𝐼 ) |
33 |
32
|
eqcomd |
⊢ ( 𝐼 ∈ ℂ → 𝐼 = ( 0 + 𝐼 ) ) |
34 |
16 33
|
syl |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐼 = ( 0 + 𝐼 ) ) |
35 |
34
|
fveq2d |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 𝐼 ) = ( 𝑊 ‘ ( 0 + 𝐼 ) ) ) |
36 |
31 35
|
eqtr4d |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 substr 〈 𝐼 , ( 𝐼 + 1 ) 〉 ) ‘ 0 ) = ( 𝑊 ‘ 𝐼 ) ) |
37 |
36
|
s1eqd |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 〈“ ( ( 𝑊 substr 〈 𝐼 , ( 𝐼 + 1 ) 〉 ) ‘ 0 ) ”〉 = 〈“ ( 𝑊 ‘ 𝐼 ) ”〉 ) |
38 |
22 37
|
eqtrd |
⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr 〈 𝐼 , ( 𝐼 + 1 ) 〉 ) = 〈“ ( 𝑊 ‘ 𝐼 ) ”〉 ) |