Metamath Proof Explorer

Theorem repswrevw

Description: The reverse of a "repeated symbol word". (Contributed by AV, 6-Nov-2018)

Ref Expression
Assertion repswrevw 
|- ( ( S e. V /\ N e. NN0 ) -> ( reverse ` ( S repeatS N ) ) = ( S repeatS N ) )

Proof

Step Hyp Ref Expression
1 repswlen 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( # ` ( S repeatS N ) ) = N )
2 1 oveq2d 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( 0 ..^ ( # ` ( S repeatS N ) ) ) = ( 0 ..^ N ) )
3 2 mpteq1d 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) |-> ( ( S repeatS N ) ` ( ( ( # ` ( S repeatS N ) ) - 1 ) - x ) ) ) = ( x e. ( 0 ..^ N ) |-> ( ( S repeatS N ) ` ( ( ( # ` ( S repeatS N ) ) - 1 ) - x ) ) ) )
4 simpll 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ x e. ( 0 ..^ N ) ) -> S e. V )
5 simplr 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ x e. ( 0 ..^ N ) ) -> N e. NN0 )
6 1 adantr 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ x e. ( 0 ..^ N ) ) -> ( # ` ( S repeatS N ) ) = N )
7 6 oveq1d 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ x e. ( 0 ..^ N ) ) -> ( ( # ` ( S repeatS N ) ) - 1 ) = ( N - 1 ) )
8 7 oveq1d 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( # ` ( S repeatS N ) ) - 1 ) - x ) = ( ( N - 1 ) - x ) )
9 ubmelm1fzo 
 |-  ( x e. ( 0 ..^ N ) -> ( ( N - x ) - 1 ) e. ( 0 ..^ N ) )
10 elfzoelz 
 |-  ( x e. ( 0 ..^ N ) -> x e. ZZ )
11 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
12 11 ad2antll 
 |-  ( ( x e. ZZ /\ ( S e. V /\ N e. NN0 ) ) -> N e. CC )
13 zcn 
 |-  ( x e. ZZ -> x e. CC )
14 13 adantr 
 |-  ( ( x e. ZZ /\ ( S e. V /\ N e. NN0 ) ) -> x e. CC )
15 1cnd 
 |-  ( ( x e. ZZ /\ ( S e. V /\ N e. NN0 ) ) -> 1 e. CC )
16 12 14 15 sub32d 
 |-  ( ( x e. ZZ /\ ( S e. V /\ N e. NN0 ) ) -> ( ( N - x ) - 1 ) = ( ( N - 1 ) - x ) )
17 16 eleq1d 
 |-  ( ( x e. ZZ /\ ( S e. V /\ N e. NN0 ) ) -> ( ( ( N - x ) - 1 ) e. ( 0 ..^ N ) <-> ( ( N - 1 ) - x ) e. ( 0 ..^ N ) ) )
18 17 biimpd 
 |-  ( ( x e. ZZ /\ ( S e. V /\ N e. NN0 ) ) -> ( ( ( N - x ) - 1 ) e. ( 0 ..^ N ) -> ( ( N - 1 ) - x ) e. ( 0 ..^ N ) ) )
19 18 ex 
 |-  ( x e. ZZ -> ( ( S e. V /\ N e. NN0 ) -> ( ( ( N - x ) - 1 ) e. ( 0 ..^ N ) -> ( ( N - 1 ) - x ) e. ( 0 ..^ N ) ) ) )
20 10 19 syl 
 |-  ( x e. ( 0 ..^ N ) -> ( ( S e. V /\ N e. NN0 ) -> ( ( ( N - x ) - 1 ) e. ( 0 ..^ N ) -> ( ( N - 1 ) - x ) e. ( 0 ..^ N ) ) ) )
21 9 20 mpid 
 |-  ( x e. ( 0 ..^ N ) -> ( ( S e. V /\ N e. NN0 ) -> ( ( N - 1 ) - x ) e. ( 0 ..^ N ) ) )
22 21 impcom 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ x e. ( 0 ..^ N ) ) -> ( ( N - 1 ) - x ) e. ( 0 ..^ N ) )
23 8 22 eqeltrd 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ x e. ( 0 ..^ N ) ) -> ( ( ( # ` ( S repeatS N ) ) - 1 ) - x ) e. ( 0 ..^ N ) )
24 repswsymb 
 |-  ( ( S e. V /\ N e. NN0 /\ ( ( ( # ` ( S repeatS N ) ) - 1 ) - x ) e. ( 0 ..^ N ) ) -> ( ( S repeatS N ) ` ( ( ( # ` ( S repeatS N ) ) - 1 ) - x ) ) = S )
25 4 5 23 24 syl3anc 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ x e. ( 0 ..^ N ) ) -> ( ( S repeatS N ) ` ( ( ( # ` ( S repeatS N ) ) - 1 ) - x ) ) = S )
26 25 mpteq2dva 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( x e. ( 0 ..^ N ) |-> ( ( S repeatS N ) ` ( ( ( # ` ( S repeatS N ) ) - 1 ) - x ) ) ) = ( x e. ( 0 ..^ N ) |-> S ) )
27 3 26 eqtrd 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) |-> ( ( S repeatS N ) ` ( ( ( # ` ( S repeatS N ) ) - 1 ) - x ) ) ) = ( x e. ( 0 ..^ N ) |-> S ) )
28 ovex 
 |-  ( S repeatS N ) e. _V
29 revval 
 |-  ( ( S repeatS N ) e. _V -> ( reverse ` ( S repeatS N ) ) = ( x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) |-> ( ( S repeatS N ) ` ( ( ( # ` ( S repeatS N ) ) - 1 ) - x ) ) ) )
30 28 29 mp1i 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( reverse ` ( S repeatS N ) ) = ( x e. ( 0 ..^ ( # ` ( S repeatS N ) ) ) |-> ( ( S repeatS N ) ` ( ( ( # ` ( S repeatS N ) ) - 1 ) - x ) ) ) )
31 reps 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) = ( x e. ( 0 ..^ N ) |-> S ) )
32 27 30 31 3eqtr4d 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( reverse ` ( S repeatS N ) ) = ( S repeatS N ) )