Metamath Proof Explorer

Theorem revs1

Description: Singleton words are their own reverses. (Contributed by Stefan O'Rear, 26-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion revs1 ⊢ reverse ⁡ ⟨“ S ”⟩ = ⟨“ S ”⟩

Proof

Step Hyp Ref Expression
1 s1cli ⊢ ⟨“ S ”⟩ ∈ Word V
2 s1len ⊢ ⟨“ S ”⟩ = 1
3 1nn ⊢ 1 ∈ ℕ
4 2 3 eqeltri ⊢ ⟨“ S ”⟩ ∈ ℕ
5 lbfzo0 ⊢ 0 ∈ 0 ..^ ⟨“ S ”⟩ ↔ ⟨“ S ”⟩ ∈ ℕ
6 4 5 mpbir ⊢ 0 ∈ 0 ..^ ⟨“ S ”⟩
7 revfv ⊢ ⟨“ S ”⟩ ∈ Word V ∧ 0 ∈ 0 ..^ ⟨“ S ”⟩ → reverse ⁡ ⟨“ S ”⟩ ⁡ 0 = ⟨“ S ”⟩ ⁡ ⟨“ S ”⟩ - 1 - 0
8 1 6 7 mp2an ⊢ reverse ⁡ ⟨“ S ”⟩ ⁡ 0 = ⟨“ S ”⟩ ⁡ ⟨“ S ”⟩ - 1 - 0
9 2 oveq1i ⊢ ⟨“ S ”⟩ − 1 = 1 − 1
10 1m1e0 ⊢ 1 − 1 = 0
11 9 10 eqtri ⊢ ⟨“ S ”⟩ − 1 = 0
12 11 oveq1i ⊢ ⟨“ S ”⟩ - 1 - 0 = 0 − 0
13 0m0e0 ⊢ 0 − 0 = 0
14 12 13 eqtri ⊢ ⟨“ S ”⟩ - 1 - 0 = 0
15 14 fveq2i ⊢ ⟨“ S ”⟩ ⁡ ⟨“ S ”⟩ - 1 - 0 = ⟨“ S ”⟩ ⁡ 0
16 ids1 ⊢ ⟨“ S ”⟩ = ⟨“ I ⁡ S ”⟩
17 16 fveq1i ⊢ ⟨“ S ”⟩ ⁡ 0 = ⟨“ I ⁡ S ”⟩ ⁡ 0
18 fvex ⊢ I ⁡ S ∈ V
19 s1fv ⊢ I ⁡ S ∈ V → ⟨“ I ⁡ S ”⟩ ⁡ 0 = I ⁡ S
20 18 19 ax-mp ⊢ ⟨“ I ⁡ S ”⟩ ⁡ 0 = I ⁡ S
21 17 20 eqtri ⊢ ⟨“ S ”⟩ ⁡ 0 = I ⁡ S
22 15 21 eqtri ⊢ ⟨“ S ”⟩ ⁡ ⟨“ S ”⟩ - 1 - 0 = I ⁡ S
23 8 22 eqtri ⊢ reverse ⁡ ⟨“ S ”⟩ ⁡ 0 = I ⁡ S
24 s1eq ⊢ reverse ⁡ ⟨“ S ”⟩ ⁡ 0 = I ⁡ S → ⟨“ reverse ⁡ ⟨“ S ”⟩ ⁡ 0 ”⟩ = ⟨“ I ⁡ S ”⟩
25 23 24 ax-mp ⊢ ⟨“ reverse ⁡ ⟨“ S ”⟩ ⁡ 0 ”⟩ = ⟨“ I ⁡ S ”⟩
26 revcl ⊢ ⟨“ S ”⟩ ∈ Word V → reverse ⁡ ⟨“ S ”⟩ ∈ Word V
27 1 26 ax-mp ⊢ reverse ⁡ ⟨“ S ”⟩ ∈ Word V
28 revlen ⊢ ⟨“ S ”⟩ ∈ Word V → reverse ⁡ ⟨“ S ”⟩ = ⟨“ S ”⟩
29 1 28 ax-mp ⊢ reverse ⁡ ⟨“ S ”⟩ = ⟨“ S ”⟩
30 29 2 eqtri ⊢ reverse ⁡ ⟨“ S ”⟩ = 1
31 eqs1 ⊢ reverse ⁡ ⟨“ S ”⟩ ∈ Word V ∧ reverse ⁡ ⟨“ S ”⟩ = 1 → reverse ⁡ ⟨“ S ”⟩ = ⟨“ reverse ⁡ ⟨“ S ”⟩ ⁡ 0 ”⟩
32 27 30 31 mp2an ⊢ reverse ⁡ ⟨“ S ”⟩ = ⟨“ reverse ⁡ ⟨“ S ”⟩ ⁡ 0 ”⟩
33 25 32 16 3eqtr4i ⊢ reverse ⁡ ⟨“ S ”⟩ = ⟨“ S ”⟩