Theorem repswfsts

Description: The first symbol of a nonempty "repeated symbol word". (Contributed by AV, 4-Nov-2018)

	Ref	Expression
Assertion	repswfsts	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑆 repeatS 𝑁 ) ‘ 0 ) = 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → 𝑆 ∈ 𝑉 )
2		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
3	2	adantl	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
4		lbfzo0	⊢ ( 0 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑁 ∈ ℕ )
5	4	bilanri	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → 0 ∈ ( 0 ..^ 𝑁 ) )
6		repswsymb	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 0 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 repeatS 𝑁 ) ‘ 0 ) = 𝑆 )
7	1 3 5 6	syl3anc	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑆 repeatS 𝑁 ) ‘ 0 ) = 𝑆 )