Theorem repswlsw

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

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

Proof

Step	Hyp	Ref	Expression
1		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
2		repsw	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑆 repeatS 𝑁 ) ∈ Word 𝑉 )
3	1 2	sylan2	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑆 repeatS 𝑁 ) ∈ Word 𝑉 )
4		lsw	⊢ ( ( 𝑆 repeatS 𝑁 ) ∈ Word 𝑉 → ( lastS ‘ ( 𝑆 repeatS 𝑁 ) ) = ( ( 𝑆 repeatS 𝑁 ) ‘ ( ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) − 1 ) ) )
5	3 4	syl	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( lastS ‘ ( 𝑆 repeatS 𝑁 ) ) = ( ( 𝑆 repeatS 𝑁 ) ‘ ( ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) − 1 ) ) )
6		simpl	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → 𝑆 ∈ 𝑉 )
7	1	adantl	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
8		repswlen	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) = 𝑁 )
9	1 8	sylan2	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) = 𝑁 )
10	9	oveq1d	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) − 1 ) = ( 𝑁 − 1 ) )
11		fzo0end	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ( 0 ..^ 𝑁 ) )
12	11	adantl	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 1 ) ∈ ( 0 ..^ 𝑁 ) )
13	10 12	eqeltrd	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) − 1 ) ∈ ( 0 ..^ 𝑁 ) )
14		repswsymb	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ ( ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) − 1 ) ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑆 repeatS 𝑁 ) ‘ ( ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) − 1 ) ) = 𝑆 )
15	6 7 13 14	syl3anc	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( ( 𝑆 repeatS 𝑁 ) ‘ ( ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) − 1 ) ) = 𝑆 )
16	5 15	eqtrd	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ) → ( lastS ‘ ( 𝑆 repeatS 𝑁 ) ) = 𝑆 )