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 ( ( 𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr ⟨ 𝐼 , ( 𝐼 + 1 ) ⟩ ) = ⟨“ ( 𝑊 ‘ 𝐼 ) ”⟩ )

Proof

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 ) ⟩ ) = ⟨“ ( 𝑊 ‘ 𝐼 ) ”⟩ )