Metamath Proof Explorer


Theorem hashecclwwlkn1

Description: The size of every equivalence class of the equivalence relation over the set of closed walks (defined as words) with a fixed length which is a prime number is 1 or equals this length. (Contributed by Alexander van der Vekens, 17-Jun-2018) (Revised by AV, 1-May-2021)

Ref Expression
Hypotheses erclwwlkn.w W = N ClWWalksN G
erclwwlkn.r ˙ = t u | t W u W n 0 N t = u cyclShift n
Assertion hashecclwwlkn1 N U W / ˙ U = 1 U = N

Proof

Step Hyp Ref Expression
1 erclwwlkn.w W = N ClWWalksN G
2 erclwwlkn.r ˙ = t u | t W u W n 0 N t = u cyclShift n
3 1 2 eclclwwlkn1 U W / ˙ U W / ˙ x W U = y W | n 0 N y = x cyclShift n
4 rabeq W = N ClWWalksN G y W | n 0 N y = x cyclShift n = y N ClWWalksN G | n 0 N y = x cyclShift n
5 1 4 mp1i N x W y W | n 0 N y = x cyclShift n = y N ClWWalksN G | n 0 N y = x cyclShift n
6 prmnn N N
7 6 nnnn0d N N 0
8 1 eleq2i x W x N ClWWalksN G
9 8 biimpi x W x N ClWWalksN G
10 clwwlknscsh N 0 x N ClWWalksN G y N ClWWalksN G | n 0 N y = x cyclShift n = y Word Vtx G | n 0 N y = x cyclShift n
11 7 9 10 syl2an N x W y N ClWWalksN G | n 0 N y = x cyclShift n = y Word Vtx G | n 0 N y = x cyclShift n
12 5 11 eqtrd N x W y W | n 0 N y = x cyclShift n = y Word Vtx G | n 0 N y = x cyclShift n
13 12 eqeq2d N x W U = y W | n 0 N y = x cyclShift n U = y Word Vtx G | n 0 N y = x cyclShift n
14 simpll x Word Vtx G x = N N x Word Vtx G
15 elnnne0 N N 0 N 0
16 eqeq1 N = x N = 0 x = 0
17 16 eqcoms x = N N = 0 x = 0
18 hasheq0 x Word Vtx G x = 0 x =
19 17 18 sylan9bbr x Word Vtx G x = N N = 0 x =
20 19 necon3bid x Word Vtx G x = N N 0 x
21 20 biimpcd N 0 x Word Vtx G x = N x
22 15 21 simplbiim N x Word Vtx G x = N x
23 22 impcom x Word Vtx G x = N N x
24 simplr x Word Vtx G x = N N x = N
25 24 eqcomd x Word Vtx G x = N N N = x
26 14 23 25 3jca x Word Vtx G x = N N x Word Vtx G x N = x
27 26 ex x Word Vtx G x = N N x Word Vtx G x N = x
28 eqid Vtx G = Vtx G
29 28 clwwlknbp x N ClWWalksN G x Word Vtx G x = N
30 27 29 syl11 N x N ClWWalksN G x Word Vtx G x N = x
31 8 30 syl5bi N x W x Word Vtx G x N = x
32 6 31 syl N x W x Word Vtx G x N = x
33 32 imp N x W x Word Vtx G x N = x
34 scshwfzeqfzo x Word Vtx G x N = x y Word Vtx G | n 0 N y = x cyclShift n = y Word Vtx G | n 0 ..^ N y = x cyclShift n
35 33 34 syl N x W y Word Vtx G | n 0 N y = x cyclShift n = y Word Vtx G | n 0 ..^ N y = x cyclShift n
36 35 eqeq2d N x W U = y Word Vtx G | n 0 N y = x cyclShift n U = y Word Vtx G | n 0 ..^ N y = x cyclShift n
37 oveq2 n = m x cyclShift n = x cyclShift m
38 37 eqeq2d n = m y = x cyclShift n y = x cyclShift m
39 38 cbvrexvw n 0 ..^ x y = x cyclShift n m 0 ..^ x y = x cyclShift m
40 eqeq1 y = u y = x cyclShift m u = x cyclShift m
41 eqcom u = x cyclShift m x cyclShift m = u
42 40 41 bitrdi y = u y = x cyclShift m x cyclShift m = u
43 42 rexbidv y = u m 0 ..^ x y = x cyclShift m m 0 ..^ x x cyclShift m = u
44 39 43 syl5bb y = u n 0 ..^ x y = x cyclShift n m 0 ..^ x x cyclShift m = u
45 44 cbvrabv y Word Vtx G | n 0 ..^ x y = x cyclShift n = u Word Vtx G | m 0 ..^ x x cyclShift m = u
46 45 cshwshash x Word Vtx G x y Word Vtx G | n 0 ..^ x y = x cyclShift n = x y Word Vtx G | n 0 ..^ x y = x cyclShift n = 1
47 46 adantr x Word Vtx G x U = y Word Vtx G | n 0 ..^ x y = x cyclShift n y Word Vtx G | n 0 ..^ x y = x cyclShift n = x y Word Vtx G | n 0 ..^ x y = x cyclShift n = 1
48 47 orcomd x Word Vtx G x U = y Word Vtx G | n 0 ..^ x y = x cyclShift n y Word Vtx G | n 0 ..^ x y = x cyclShift n = 1 y Word Vtx G | n 0 ..^ x y = x cyclShift n = x
49 fveqeq2 U = y Word Vtx G | n 0 ..^ x y = x cyclShift n U = 1 y Word Vtx G | n 0 ..^ x y = x cyclShift n = 1
50 fveqeq2 U = y Word Vtx G | n 0 ..^ x y = x cyclShift n U = x y Word Vtx G | n 0 ..^ x y = x cyclShift n = x
51 49 50 orbi12d U = y Word Vtx G | n 0 ..^ x y = x cyclShift n U = 1 U = x y Word Vtx G | n 0 ..^ x y = x cyclShift n = 1 y Word Vtx G | n 0 ..^ x y = x cyclShift n = x
52 51 adantl x Word Vtx G x U = y Word Vtx G | n 0 ..^ x y = x cyclShift n U = 1 U = x y Word Vtx G | n 0 ..^ x y = x cyclShift n = 1 y Word Vtx G | n 0 ..^ x y = x cyclShift n = x
53 48 52 mpbird x Word Vtx G x U = y Word Vtx G | n 0 ..^ x y = x cyclShift n U = 1 U = x
54 53 ex x Word Vtx G x U = y Word Vtx G | n 0 ..^ x y = x cyclShift n U = 1 U = x
55 54 ex x Word Vtx G x U = y Word Vtx G | n 0 ..^ x y = x cyclShift n U = 1 U = x
56 55 adantr x Word Vtx G x = N x U = y Word Vtx G | n 0 ..^ x y = x cyclShift n U = 1 U = x
57 eleq1 N = x N x
58 oveq2 N = x 0 ..^ N = 0 ..^ x
59 58 rexeqdv N = x n 0 ..^ N y = x cyclShift n n 0 ..^ x y = x cyclShift n
60 59 rabbidv N = x y Word Vtx G | n 0 ..^ N y = x cyclShift n = y Word Vtx G | n 0 ..^ x y = x cyclShift n
61 60 eqeq2d N = x U = y Word Vtx G | n 0 ..^ N y = x cyclShift n U = y Word Vtx G | n 0 ..^ x y = x cyclShift n
62 eqeq2 N = x U = N U = x
63 62 orbi2d N = x U = 1 U = N U = 1 U = x
64 61 63 imbi12d N = x U = y Word Vtx G | n 0 ..^ N y = x cyclShift n U = 1 U = N U = y Word Vtx G | n 0 ..^ x y = x cyclShift n U = 1 U = x
65 57 64 imbi12d N = x N U = y Word Vtx G | n 0 ..^ N y = x cyclShift n U = 1 U = N x U = y Word Vtx G | n 0 ..^ x y = x cyclShift n U = 1 U = x
66 65 eqcoms x = N N U = y Word Vtx G | n 0 ..^ N y = x cyclShift n U = 1 U = N x U = y Word Vtx G | n 0 ..^ x y = x cyclShift n U = 1 U = x
67 66 adantl x Word Vtx G x = N N U = y Word Vtx G | n 0 ..^ N y = x cyclShift n U = 1 U = N x U = y Word Vtx G | n 0 ..^ x y = x cyclShift n U = 1 U = x
68 56 67 mpbird x Word Vtx G x = N N U = y Word Vtx G | n 0 ..^ N y = x cyclShift n U = 1 U = N
69 29 68 syl x N ClWWalksN G N U = y Word Vtx G | n 0 ..^ N y = x cyclShift n U = 1 U = N
70 69 1 eleq2s x W N U = y Word Vtx G | n 0 ..^ N y = x cyclShift n U = 1 U = N
71 70 impcom N x W U = y Word Vtx G | n 0 ..^ N y = x cyclShift n U = 1 U = N
72 36 71 sylbid N x W U = y Word Vtx G | n 0 N y = x cyclShift n U = 1 U = N
73 13 72 sylbid N x W U = y W | n 0 N y = x cyclShift n U = 1 U = N
74 73 rexlimdva N x W U = y W | n 0 N y = x cyclShift n U = 1 U = N
75 74 com12 x W U = y W | n 0 N y = x cyclShift n N U = 1 U = N
76 3 75 syl6bi U W / ˙ U W / ˙ N U = 1 U = N
77 76 pm2.43i U W / ˙ N U = 1 U = N
78 77 impcom N U W / ˙ U = 1 U = N