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

Metamath Proof Explorer

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 𝑁 ) ) = 𝑆 )