Metamath Proof Explorer

Theorem cshweqdif2

Description: If cyclically shifting two words (of the same length) results in the same word, cyclically shifting one of the words by the difference of the numbers of shifts results in the other word. (Contributed by AV, 21-Apr-2018) (Revised by AV, 6-Jun-2018) (Revised by AV, 1-Nov-2018)

Ref Expression
Assertion cshweqdif2 
|- ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( ( W cyclShift N ) = ( U cyclShift M ) -> ( U cyclShift ( M - N ) ) = W ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( W e. Word V /\ U e. Word V ) -> U e. Word V )
2 1 adantr 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> U e. Word V )
3 zsubcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M - N ) e. ZZ )
4 3 ancoms 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( M - N ) e. ZZ )
5 4 adantl 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( M - N ) e. ZZ )
6 simpr 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> M e. ZZ )
7 6 adantl 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> M e. ZZ )
8 2 5 7 3jca 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( U e. Word V /\ ( M - N ) e. ZZ /\ M e. ZZ ) )
9 8 adantr 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( U e. Word V /\ ( M - N ) e. ZZ /\ M e. ZZ ) )
10 3cshw 
 |-  ( ( U e. Word V /\ ( M - N ) e. ZZ /\ M e. ZZ ) -> ( U cyclShift ( M - N ) ) = ( ( ( U cyclShift M ) cyclShift ( M - N ) ) cyclShift ( ( # ` U ) - M ) ) )
11 9 10 syl 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( U cyclShift ( M - N ) ) = ( ( ( U cyclShift M ) cyclShift ( M - N ) ) cyclShift ( ( # ` U ) - M ) ) )
12 simpl 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( W e. Word V /\ U e. Word V ) )
13 12 ancomd 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( U e. Word V /\ W e. Word V ) )
14 13 adantr 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( U e. Word V /\ W e. Word V ) )
15 simpr 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( N e. ZZ /\ M e. ZZ ) )
16 15 ancomd 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( M e. ZZ /\ N e. ZZ ) )
17 16 adantr 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( M e. ZZ /\ N e. ZZ ) )
18 simpr 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( W cyclShift N ) = ( U cyclShift M ) )
19 18 eqcomd 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( U cyclShift M ) = ( W cyclShift N ) )
20 cshwleneq 
 |-  ( ( ( U e. Word V /\ W e. Word V ) /\ ( M e. ZZ /\ N e. ZZ ) /\ ( U cyclShift M ) = ( W cyclShift N ) ) -> ( # ` U ) = ( # ` W ) )
21 14 17 19 20 syl3anc 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( # ` U ) = ( # ` W ) )
22 21 oveq1d 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( ( # ` U ) - M ) = ( ( # ` W ) - M ) )
23 22 oveq2d 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( ( ( U cyclShift M ) cyclShift ( M - N ) ) cyclShift ( ( # ` U ) - M ) ) = ( ( ( U cyclShift M ) cyclShift ( M - N ) ) cyclShift ( ( # ` W ) - M ) ) )
24 11 23 eqtrd 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( U cyclShift ( M - N ) ) = ( ( ( U cyclShift M ) cyclShift ( M - N ) ) cyclShift ( ( # ` W ) - M ) ) )
25 19 oveq1d 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( ( U cyclShift M ) cyclShift ( M - N ) ) = ( ( W cyclShift N ) cyclShift ( M - N ) ) )
26 simpl 
 |-  ( ( W e. Word V /\ U e. Word V ) -> W e. Word V )
27 26 adantr 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> W e. Word V )
28 simpl 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> N e. ZZ )
29 28 adantl 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> N e. ZZ )
30 27 29 5 3jca 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( W e. Word V /\ N e. ZZ /\ ( M - N ) e. ZZ ) )
31 30 adantr 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( W e. Word V /\ N e. ZZ /\ ( M - N ) e. ZZ ) )
32 2cshw 
 |-  ( ( W e. Word V /\ N e. ZZ /\ ( M - N ) e. ZZ ) -> ( ( W cyclShift N ) cyclShift ( M - N ) ) = ( W cyclShift ( N + ( M - N ) ) ) )
33 31 32 syl 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( ( W cyclShift N ) cyclShift ( M - N ) ) = ( W cyclShift ( N + ( M - N ) ) ) )
34 zcn 
 |-  ( N e. ZZ -> N e. CC )
35 zcn 
 |-  ( M e. ZZ -> M e. CC )
36 34 35 anim12i 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( N e. CC /\ M e. CC ) )
37 36 adantl 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( N e. CC /\ M e. CC ) )
38 37 adantr 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( N e. CC /\ M e. CC ) )
39 pncan3 
 |-  ( ( N e. CC /\ M e. CC ) -> ( N + ( M - N ) ) = M )
40 38 39 syl 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( N + ( M - N ) ) = M )
41 40 oveq2d 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( W cyclShift ( N + ( M - N ) ) ) = ( W cyclShift M ) )
42 25 33 41 3eqtrd 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( ( U cyclShift M ) cyclShift ( M - N ) ) = ( W cyclShift M ) )
43 42 oveq1d 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( ( ( U cyclShift M ) cyclShift ( M - N ) ) cyclShift ( ( # ` W ) - M ) ) = ( ( W cyclShift M ) cyclShift ( ( # ` W ) - M ) ) )
44 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
45 44 nn0zd 
 |-  ( W e. Word V -> ( # ` W ) e. ZZ )
46 45 adantr 
 |-  ( ( W e. Word V /\ U e. Word V ) -> ( # ` W ) e. ZZ )
47 zsubcl 
 |-  ( ( ( # ` W ) e. ZZ /\ M e. ZZ ) -> ( ( # ` W ) - M ) e. ZZ )
48 46 6 47 syl2an 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( ( # ` W ) - M ) e. ZZ )
49 27 7 48 3jca 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( W e. Word V /\ M e. ZZ /\ ( ( # ` W ) - M ) e. ZZ ) )
50 49 adantr 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( W e. Word V /\ M e. ZZ /\ ( ( # ` W ) - M ) e. ZZ ) )
51 2cshw 
 |-  ( ( W e. Word V /\ M e. ZZ /\ ( ( # ` W ) - M ) e. ZZ ) -> ( ( W cyclShift M ) cyclShift ( ( # ` W ) - M ) ) = ( W cyclShift ( M + ( ( # ` W ) - M ) ) ) )
52 50 51 syl 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( ( W cyclShift M ) cyclShift ( ( # ` W ) - M ) ) = ( W cyclShift ( M + ( ( # ` W ) - M ) ) ) )
53 24 43 52 3eqtrd 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( U cyclShift ( M - N ) ) = ( W cyclShift ( M + ( ( # ` W ) - M ) ) ) )
54 44 nn0cnd 
 |-  ( W e. Word V -> ( # ` W ) e. CC )
55 54 adantr 
 |-  ( ( W e. Word V /\ U e. Word V ) -> ( # ` W ) e. CC )
56 35 adantl 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> M e. CC )
57 55 56 anim12i 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( ( # ` W ) e. CC /\ M e. CC ) )
58 57 ancomd 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( M e. CC /\ ( # ` W ) e. CC ) )
59 58 adantr 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( M e. CC /\ ( # ` W ) e. CC ) )
60 pncan3 
 |-  ( ( M e. CC /\ ( # ` W ) e. CC ) -> ( M + ( ( # ` W ) - M ) ) = ( # ` W ) )
61 59 60 syl 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( M + ( ( # ` W ) - M ) ) = ( # ` W ) )
62 61 oveq2d 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( W cyclShift ( M + ( ( # ` W ) - M ) ) ) = ( W cyclShift ( # ` W ) ) )
63 cshwn 
 |-  ( W e. Word V -> ( W cyclShift ( # ` W ) ) = W )
64 27 63 syl 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( W cyclShift ( # ` W ) ) = W )
65 64 adantr 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( W cyclShift ( # ` W ) ) = W )
66 53 62 65 3eqtrd 
 |-  ( ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) /\ ( W cyclShift N ) = ( U cyclShift M ) ) -> ( U cyclShift ( M - N ) ) = W )
67 66 ex 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( ( W cyclShift N ) = ( U cyclShift M ) -> ( U cyclShift ( M - N ) ) = W ) )