Theorem repswsymb

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

	Ref	Expression
Assertion	repswsymb	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 repeatS 𝑁 ) ‘ 𝐼 ) = 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		reps	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑆 repeatS 𝑁 ) = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) )
2	1	3adant3	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 repeatS 𝑁 ) = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ 𝑆 ) )
3		eqidd	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑥 = 𝐼 ) → 𝑆 = 𝑆 )
4		simp3	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ( 0 ..^ 𝑁 ) ) → 𝐼 ∈ ( 0 ..^ 𝑁 ) )
5		simp1	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆 ∈ 𝑉 )
6	2 3 4 5	fvmptd	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 repeatS 𝑁 ) ‘ 𝐼 ) = 𝑆 )