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 "> e. Word _V
2 s1len 
 |-  ( # ` <" S "> ) = 1
3 1nn 
 |-  1 e. NN
4 2 3 eqeltri 
 |-  ( # ` <" S "> ) e. NN
5 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` <" S "> ) ) <-> ( # ` <" S "> ) e. NN )
6 4 5 mpbir 
 |-  0 e. ( 0 ..^ ( # ` <" S "> ) )
7 revfv 
 |-  ( ( <" S "> e. Word _V /\ 0 e. ( 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 ) e. _V
19 s1fv 
 |-  ( ( _I ` S ) e. _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 "> e. Word _V -> ( reverse ` <" S "> ) e. Word _V )
27 1 26 ax-mp 
 |-  ( reverse ` <" S "> ) e. Word _V
28 revlen 
 |-  ( <" S "> e. Word _V -> ( # ` ( reverse ` <" S "> ) ) = ( # ` <" S "> ) )
29 1 28 ax-mp 
 |-  ( # ` ( reverse ` <" S "> ) ) = ( # ` <" S "> )
30 29 2 eqtri 
 |-  ( # ` ( reverse ` <" S "> ) ) = 1
31 eqs1 
 |-  ( ( ( reverse ` <" S "> ) e. 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 ">