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 ) = ( 𝑆 ‘ 𝐹 ) )