Metamath Proof Explorer


Theorem repswcshw

Description: A cyclically shifted "repeated symbol word". (Contributed by Alexander van der Vekens, 7-Nov-2018) (Proof shortened by AV, 16-Oct-2022)

Ref Expression
Assertion repswcshw
|- ( ( S e. V /\ N e. NN0 /\ I e. ZZ ) -> ( ( S repeatS N ) cyclShift I ) = ( S repeatS N ) )

Proof

Step Hyp Ref Expression
1 0csh0
 |-  ( (/) cyclShift I ) = (/)
2 repsw0
 |-  ( S e. V -> ( S repeatS 0 ) = (/) )
3 2 oveq1d
 |-  ( S e. V -> ( ( S repeatS 0 ) cyclShift I ) = ( (/) cyclShift I ) )
4 1 3 2 3eqtr4a
 |-  ( S e. V -> ( ( S repeatS 0 ) cyclShift I ) = ( S repeatS 0 ) )
5 4 3ad2ant1
 |-  ( ( S e. V /\ N e. NN0 /\ I e. ZZ ) -> ( ( S repeatS 0 ) cyclShift I ) = ( S repeatS 0 ) )
6 oveq2
 |-  ( N = 0 -> ( S repeatS N ) = ( S repeatS 0 ) )
7 6 oveq1d
 |-  ( N = 0 -> ( ( S repeatS N ) cyclShift I ) = ( ( S repeatS 0 ) cyclShift I ) )
8 7 6 eqeq12d
 |-  ( N = 0 -> ( ( ( S repeatS N ) cyclShift I ) = ( S repeatS N ) <-> ( ( S repeatS 0 ) cyclShift I ) = ( S repeatS 0 ) ) )
9 5 8 syl5ibr
 |-  ( N = 0 -> ( ( S e. V /\ N e. NN0 /\ I e. ZZ ) -> ( ( S repeatS N ) cyclShift I ) = ( S repeatS N ) ) )
10 idd
 |-  ( -. N = 0 -> ( S e. V -> S e. V ) )
11 df-ne
 |-  ( N =/= 0 <-> -. N = 0 )
12 elnnne0
 |-  ( N e. NN <-> ( N e. NN0 /\ N =/= 0 ) )
13 12 simplbi2com
 |-  ( N =/= 0 -> ( N e. NN0 -> N e. NN ) )
14 11 13 sylbir
 |-  ( -. N = 0 -> ( N e. NN0 -> N e. NN ) )
15 idd
 |-  ( -. N = 0 -> ( I e. ZZ -> I e. ZZ ) )
16 10 14 15 3anim123d
 |-  ( -. N = 0 -> ( ( S e. V /\ N e. NN0 /\ I e. ZZ ) -> ( S e. V /\ N e. NN /\ I e. ZZ ) ) )
17 nnnn0
 |-  ( N e. NN -> N e. NN0 )
18 17 anim2i
 |-  ( ( S e. V /\ N e. NN ) -> ( S e. V /\ N e. NN0 ) )
19 repsw
 |-  ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) e. Word V )
20 18 19 syl
 |-  ( ( S e. V /\ N e. NN ) -> ( S repeatS N ) e. Word V )
21 cshword
 |-  ( ( ( S repeatS N ) e. Word V /\ I e. ZZ ) -> ( ( S repeatS N ) cyclShift I ) = ( ( ( S repeatS N ) substr <. ( I mod ( # ` ( S repeatS N ) ) ) , ( # ` ( S repeatS N ) ) >. ) ++ ( ( S repeatS N ) prefix ( I mod ( # ` ( S repeatS N ) ) ) ) ) )
22 20 21 stoic3
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( S repeatS N ) cyclShift I ) = ( ( ( S repeatS N ) substr <. ( I mod ( # ` ( S repeatS N ) ) ) , ( # ` ( S repeatS N ) ) >. ) ++ ( ( S repeatS N ) prefix ( I mod ( # ` ( S repeatS N ) ) ) ) ) )
23 repswlen
 |-  ( ( S e. V /\ N e. NN0 ) -> ( # ` ( S repeatS N ) ) = N )
24 18 23 syl
 |-  ( ( S e. V /\ N e. NN ) -> ( # ` ( S repeatS N ) ) = N )
25 24 oveq2d
 |-  ( ( S e. V /\ N e. NN ) -> ( I mod ( # ` ( S repeatS N ) ) ) = ( I mod N ) )
26 25 24 opeq12d
 |-  ( ( S e. V /\ N e. NN ) -> <. ( I mod ( # ` ( S repeatS N ) ) ) , ( # ` ( S repeatS N ) ) >. = <. ( I mod N ) , N >. )
27 26 oveq2d
 |-  ( ( S e. V /\ N e. NN ) -> ( ( S repeatS N ) substr <. ( I mod ( # ` ( S repeatS N ) ) ) , ( # ` ( S repeatS N ) ) >. ) = ( ( S repeatS N ) substr <. ( I mod N ) , N >. ) )
28 25 oveq2d
 |-  ( ( S e. V /\ N e. NN ) -> ( ( S repeatS N ) prefix ( I mod ( # ` ( S repeatS N ) ) ) ) = ( ( S repeatS N ) prefix ( I mod N ) ) )
29 27 28 oveq12d
 |-  ( ( S e. V /\ N e. NN ) -> ( ( ( S repeatS N ) substr <. ( I mod ( # ` ( S repeatS N ) ) ) , ( # ` ( S repeatS N ) ) >. ) ++ ( ( S repeatS N ) prefix ( I mod ( # ` ( S repeatS N ) ) ) ) ) = ( ( ( S repeatS N ) substr <. ( I mod N ) , N >. ) ++ ( ( S repeatS N ) prefix ( I mod N ) ) ) )
30 29 3adant3
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( ( S repeatS N ) substr <. ( I mod ( # ` ( S repeatS N ) ) ) , ( # ` ( S repeatS N ) ) >. ) ++ ( ( S repeatS N ) prefix ( I mod ( # ` ( S repeatS N ) ) ) ) ) = ( ( ( S repeatS N ) substr <. ( I mod N ) , N >. ) ++ ( ( S repeatS N ) prefix ( I mod N ) ) ) )
31 18 3adant3
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( S e. V /\ N e. NN0 ) )
32 zmodcl
 |-  ( ( I e. ZZ /\ N e. NN ) -> ( I mod N ) e. NN0 )
33 32 ancoms
 |-  ( ( N e. NN /\ I e. ZZ ) -> ( I mod N ) e. NN0 )
34 17 adantr
 |-  ( ( N e. NN /\ I e. ZZ ) -> N e. NN0 )
35 33 34 jca
 |-  ( ( N e. NN /\ I e. ZZ ) -> ( ( I mod N ) e. NN0 /\ N e. NN0 ) )
36 35 3adant1
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( I mod N ) e. NN0 /\ N e. NN0 ) )
37 nnre
 |-  ( N e. NN -> N e. RR )
38 37 leidd
 |-  ( N e. NN -> N <_ N )
39 38 3ad2ant2
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> N <_ N )
40 repswswrd
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ ( ( I mod N ) e. NN0 /\ N e. NN0 ) /\ N <_ N ) -> ( ( S repeatS N ) substr <. ( I mod N ) , N >. ) = ( S repeatS ( N - ( I mod N ) ) ) )
41 31 36 39 40 syl3anc
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( S repeatS N ) substr <. ( I mod N ) , N >. ) = ( S repeatS ( N - ( I mod N ) ) ) )
42 simp1
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> S e. V )
43 17 3ad2ant2
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> N e. NN0 )
44 zmodfzp1
 |-  ( ( I e. ZZ /\ N e. NN ) -> ( I mod N ) e. ( 0 ... N ) )
45 44 ancoms
 |-  ( ( N e. NN /\ I e. ZZ ) -> ( I mod N ) e. ( 0 ... N ) )
46 45 3adant1
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( I mod N ) e. ( 0 ... N ) )
47 repswpfx
 |-  ( ( S e. V /\ N e. NN0 /\ ( I mod N ) e. ( 0 ... N ) ) -> ( ( S repeatS N ) prefix ( I mod N ) ) = ( S repeatS ( I mod N ) ) )
48 42 43 46 47 syl3anc
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( S repeatS N ) prefix ( I mod N ) ) = ( S repeatS ( I mod N ) ) )
49 41 48 oveq12d
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( ( S repeatS N ) substr <. ( I mod N ) , N >. ) ++ ( ( S repeatS N ) prefix ( I mod N ) ) ) = ( ( S repeatS ( N - ( I mod N ) ) ) ++ ( S repeatS ( I mod N ) ) ) )
50 32 nn0red
 |-  ( ( I e. ZZ /\ N e. NN ) -> ( I mod N ) e. RR )
51 50 ancoms
 |-  ( ( N e. NN /\ I e. ZZ ) -> ( I mod N ) e. RR )
52 37 adantr
 |-  ( ( N e. NN /\ I e. ZZ ) -> N e. RR )
53 zre
 |-  ( I e. ZZ -> I e. RR )
54 nnrp
 |-  ( N e. NN -> N e. RR+ )
55 modlt
 |-  ( ( I e. RR /\ N e. RR+ ) -> ( I mod N ) < N )
56 53 54 55 syl2anr
 |-  ( ( N e. NN /\ I e. ZZ ) -> ( I mod N ) < N )
57 51 52 56 ltled
 |-  ( ( N e. NN /\ I e. ZZ ) -> ( I mod N ) <_ N )
58 57 3adant1
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( I mod N ) <_ N )
59 33 3adant1
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( I mod N ) e. NN0 )
60 nn0sub
 |-  ( ( ( I mod N ) e. NN0 /\ N e. NN0 ) -> ( ( I mod N ) <_ N <-> ( N - ( I mod N ) ) e. NN0 ) )
61 59 43 60 syl2anc
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( I mod N ) <_ N <-> ( N - ( I mod N ) ) e. NN0 ) )
62 58 61 mpbid
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( N - ( I mod N ) ) e. NN0 )
63 repswccat
 |-  ( ( S e. V /\ ( N - ( I mod N ) ) e. NN0 /\ ( I mod N ) e. NN0 ) -> ( ( S repeatS ( N - ( I mod N ) ) ) ++ ( S repeatS ( I mod N ) ) ) = ( S repeatS ( ( N - ( I mod N ) ) + ( I mod N ) ) ) )
64 42 62 59 63 syl3anc
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( S repeatS ( N - ( I mod N ) ) ) ++ ( S repeatS ( I mod N ) ) ) = ( S repeatS ( ( N - ( I mod N ) ) + ( I mod N ) ) ) )
65 nncn
 |-  ( N e. NN -> N e. CC )
66 65 adantl
 |-  ( ( I e. ZZ /\ N e. NN ) -> N e. CC )
67 32 nn0cnd
 |-  ( ( I e. ZZ /\ N e. NN ) -> ( I mod N ) e. CC )
68 66 67 npcand
 |-  ( ( I e. ZZ /\ N e. NN ) -> ( ( N - ( I mod N ) ) + ( I mod N ) ) = N )
69 68 ancoms
 |-  ( ( N e. NN /\ I e. ZZ ) -> ( ( N - ( I mod N ) ) + ( I mod N ) ) = N )
70 69 3adant1
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( N - ( I mod N ) ) + ( I mod N ) ) = N )
71 70 oveq2d
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( S repeatS ( ( N - ( I mod N ) ) + ( I mod N ) ) ) = ( S repeatS N ) )
72 49 64 71 3eqtrd
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( ( S repeatS N ) substr <. ( I mod N ) , N >. ) ++ ( ( S repeatS N ) prefix ( I mod N ) ) ) = ( S repeatS N ) )
73 22 30 72 3eqtrd
 |-  ( ( S e. V /\ N e. NN /\ I e. ZZ ) -> ( ( S repeatS N ) cyclShift I ) = ( S repeatS N ) )
74 16 73 syl6
 |-  ( -. N = 0 -> ( ( S e. V /\ N e. NN0 /\ I e. ZZ ) -> ( ( S repeatS N ) cyclShift I ) = ( S repeatS N ) ) )
75 9 74 pm2.61i
 |-  ( ( S e. V /\ N e. NN0 /\ I e. ZZ ) -> ( ( S repeatS N ) cyclShift I ) = ( S repeatS N ) )