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

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 ‘ ⟨“ 𝑆 ”⟩ ) = ⟨“ 𝑆 ”⟩

Proof

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