This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem swrdfv0

Description: The first symbol in an extracted subword. (Contributed by AV, 27-Apr-2022)

Ref Expression
Assertion swrdfv0 ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ..^ 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ‘ 0 ) = ( 𝑆 ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 elfzofz ⊢ ( 𝐹 ∈ ( 0 ..^ 𝐿 ) → 𝐹 ∈ ( 0 ... 𝐿 ) )
2 1 3anim2i ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ..^ 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) )
3 fzonnsub ⊢ ( 𝐹 ∈ ( 0 ..^ 𝐿 ) → ( 𝐿 − 𝐹 ) ∈ ℕ )
4 3 3ad2ant2 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ..^ 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝐿 − 𝐹 ) ∈ ℕ )
5 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ↔ ( 𝐿 − 𝐹 ) ∈ ℕ )
6 4 5 sylibr ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ..^ 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → 0 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) )
7 swrdfv ⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) ∧ 0 ∈ ( 0 ..^ ( 𝐿 − 𝐹 ) ) ) → ( ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ‘ 0 ) = ( 𝑆 ‘ ( 0 + 𝐹 ) ) )
8 2 6 7 syl2anc ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ..^ 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ‘ 0 ) = ( 𝑆 ‘ ( 0 + 𝐹 ) ) )
9 elfzoelz ⊢ ( 𝐹 ∈ ( 0 ..^ 𝐿 ) → 𝐹 ∈ ℤ )
10 9 zcnd ⊢ ( 𝐹 ∈ ( 0 ..^ 𝐿 ) → 𝐹 ∈ ℂ )
11 10 addlidd ⊢ ( 𝐹 ∈ ( 0 ..^ 𝐿 ) → ( 0 + 𝐹 ) = 𝐹 )
12 11 fveq2d ⊢ ( 𝐹 ∈ ( 0 ..^ 𝐿 ) → ( 𝑆 ‘ ( 0 + 𝐹 ) ) = ( 𝑆 ‘ 𝐹 ) )
13 12 3ad2ant2 ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ..^ 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ‘ ( 0 + 𝐹 ) ) = ( 𝑆 ‘ 𝐹 ) )
14 8 13 eqtrd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ..^ 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) ‘ 0 ) = ( 𝑆 ‘ 𝐹 ) )