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

Metamath Proof Explorer

Theorem lsw1

Description: The last symbol of a word of length 1 is the first symbol of this word. (Contributed by Alexander van der Vekens, 19-Mar-2018)

Ref Expression
Assertion lsw1 ⊢ W ∈ Word V ∧ W = 1 → lastS ⁡ W = W ⁡ 0

Proof

Step Hyp Ref Expression
1 lsw ⊢ W ∈ Word V → lastS ⁡ W = W ⁡ W − 1
2 oveq1 ⊢ W = 1 → W − 1 = 1 − 1
3 1m1e0 ⊢ 1 − 1 = 0
4 2 3 eqtrdi ⊢ W = 1 → W − 1 = 0
5 4 fveq2d ⊢ W = 1 → W ⁡ W − 1 = W ⁡ 0
6 1 5 sylan9eq ⊢ W ∈ Word V ∧ W = 1 → lastS ⁡ W = W ⁡ 0