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 ) )