Metamath Proof Explorer

Theorem umgrhashecclwwlk

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 equals this length (in an undirected simple graph). (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 e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
Assertion umgrhashecclwwlk 
|- ( ( G e. UMGraph /\ N e. Prime ) -> ( U e. ( W /. .~ ) -> ( # ` U ) = N ) )

Proof

Step Hyp Ref Expression
1 erclwwlkn.w 
 |-  W = ( N ClWWalksN G )
2 erclwwlkn.r 
 |-  .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
3 1 2 eclclwwlkn1 
 |-  ( U e. ( W /. .~ ) -> ( U e. ( W /. .~ ) <-> E. x e. W U = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) )
4 rabeq 
 |-  ( W = ( N ClWWalksN G ) -> { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } = { y e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } )
5 1 4 mp1i 
 |-  ( ( ( G e. UMGraph /\ N e. Prime ) /\ x e. W ) -> { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } = { y e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } )
6 prmnn 
 |-  ( N e. Prime -> N e. NN )
7 6 nnnn0d 
 |-  ( N e. Prime -> N e. NN0 )
8 7 adantl 
 |-  ( ( G e. UMGraph /\ N e. Prime ) -> N e. NN0 )
9 1 eleq2i 
 |-  ( x e. W <-> x e. ( N ClWWalksN G ) )
10 9 biimpi 
 |-  ( x e. W -> x e. ( N ClWWalksN G ) )
11 clwwlknscsh 
 |-  ( ( N e. NN0 /\ x e. ( N ClWWalksN G ) ) -> { y e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } )
12 8 10 11 syl2an 
 |-  ( ( ( G e. UMGraph /\ N e. Prime ) /\ x e. W ) -> { y e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } )
13 5 12 eqtrd 
 |-  ( ( ( G e. UMGraph /\ N e. Prime ) /\ x e. W ) -> { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } )
14 13 eqeq2d 
 |-  ( ( ( G e. UMGraph /\ N e. Prime ) /\ x e. W ) -> ( U = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } <-> U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) )
15 6 adantl 
 |-  ( ( G e. UMGraph /\ N e. Prime ) -> N e. NN )
16 simpll 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) /\ N e. NN ) -> x e. Word ( Vtx ` G ) )
17 elnnne0 
 |-  ( N e. NN <-> ( N e. NN0 /\ N =/= 0 ) )
18 eqeq1 
 |-  ( N = ( # ` x ) -> ( N = 0 <-> ( # ` x ) = 0 ) )
19 18 eqcoms 
 |-  ( ( # ` x ) = N -> ( N = 0 <-> ( # ` x ) = 0 ) )
20 hasheq0 
 |-  ( x e. Word ( Vtx ` G ) -> ( ( # ` x ) = 0 <-> x = (/) ) )
21 19 20 sylan9bbr 
 |-  ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) -> ( N = 0 <-> x = (/) ) )
22 21 necon3bid 
 |-  ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) -> ( N =/= 0 <-> x =/= (/) ) )
23 22 biimpcd 
 |-  ( N =/= 0 -> ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) -> x =/= (/) ) )
24 17 23 simplbiim 
 |-  ( N e. NN -> ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) -> x =/= (/) ) )
25 24 impcom 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) /\ N e. NN ) -> x =/= (/) )
26 simplr 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) /\ N e. NN ) -> ( # ` x ) = N )
27 26 eqcomd 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) /\ N e. NN ) -> N = ( # ` x ) )
28 16 25 27 3jca 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) /\ N e. NN ) -> ( x e. Word ( Vtx ` G ) /\ x =/= (/) /\ N = ( # ` x ) ) )
29 28 ex 
 |-  ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) -> ( N e. NN -> ( x e. Word ( Vtx ` G ) /\ x =/= (/) /\ N = ( # ` x ) ) ) )
30 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
31 30 clwwlknbp 
 |-  ( x e. ( N ClWWalksN G ) -> ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) )
32 29 31 syl11 
 |-  ( N e. NN -> ( x e. ( N ClWWalksN G ) -> ( x e. Word ( Vtx ` G ) /\ x =/= (/) /\ N = ( # ` x ) ) ) )
33 9 32 biimtrid 
 |-  ( N e. NN -> ( x e. W -> ( x e. Word ( Vtx ` G ) /\ x =/= (/) /\ N = ( # ` x ) ) ) )
34 15 33 syl 
 |-  ( ( G e. UMGraph /\ N e. Prime ) -> ( x e. W -> ( x e. Word ( Vtx ` G ) /\ x =/= (/) /\ N = ( # ` x ) ) ) )
35 34 imp 
 |-  ( ( ( G e. UMGraph /\ N e. Prime ) /\ x e. W ) -> ( x e. Word ( Vtx ` G ) /\ x =/= (/) /\ N = ( # ` x ) ) )
36 scshwfzeqfzo 
 |-  ( ( x e. Word ( Vtx ` G ) /\ x =/= (/) /\ N = ( # ` x ) ) -> { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } )
37 35 36 syl 
 |-  ( ( ( G e. UMGraph /\ N e. Prime ) /\ x e. W ) -> { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } )
38 37 eqeq2d 
 |-  ( ( ( G e. UMGraph /\ N e. Prime ) /\ x e. W ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } <-> U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } ) )
39 fveq2 
 |-  ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } -> ( # ` U ) = ( # ` { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) )
40 simprl 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ x e. ( ( # ` x ) ClWWalksN G ) ) /\ ( G e. UMGraph /\ ( # ` x ) e. Prime ) ) -> G e. UMGraph )
41 prmuz2 
 |-  ( ( # ` x ) e. Prime -> ( # ` x ) e. ( ZZ>= ` 2 ) )
42 41 adantl 
 |-  ( ( G e. UMGraph /\ ( # ` x ) e. Prime ) -> ( # ` x ) e. ( ZZ>= ` 2 ) )
43 42 adantl 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ x e. ( ( # ` x ) ClWWalksN G ) ) /\ ( G e. UMGraph /\ ( # ` x ) e. Prime ) ) -> ( # ` x ) e. ( ZZ>= ` 2 ) )
44 simplr 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ x e. ( ( # ` x ) ClWWalksN G ) ) /\ ( G e. UMGraph /\ ( # ` x ) e. Prime ) ) -> x e. ( ( # ` x ) ClWWalksN G ) )
45 umgr2cwwkdifex 
 |-  ( ( G e. UMGraph /\ ( # ` x ) e. ( ZZ>= ` 2 ) /\ x e. ( ( # ` x ) ClWWalksN G ) ) -> E. i e. ( 0 ..^ ( # ` x ) ) ( x ` i ) =/= ( x ` 0 ) )
46 40 43 44 45 syl3anc 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ x e. ( ( # ` x ) ClWWalksN G ) ) /\ ( G e. UMGraph /\ ( # ` x ) e. Prime ) ) -> E. i e. ( 0 ..^ ( # ` x ) ) ( x ` i ) =/= ( x ` 0 ) )
47 oveq2 
 |-  ( n = m -> ( x cyclShift n ) = ( x cyclShift m ) )
48 47 eqeq2d 
 |-  ( n = m -> ( y = ( x cyclShift n ) <-> y = ( x cyclShift m ) ) )
49 48 cbvrexvw 
 |-  ( E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) <-> E. m e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift m ) )
50 eqeq1 
 |-  ( y = u -> ( y = ( x cyclShift m ) <-> u = ( x cyclShift m ) ) )
51 eqcom 
 |-  ( u = ( x cyclShift m ) <-> ( x cyclShift m ) = u )
52 50 51 bitrdi 
 |-  ( y = u -> ( y = ( x cyclShift m ) <-> ( x cyclShift m ) = u ) )
53 52 rexbidv 
 |-  ( y = u -> ( E. m e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift m ) <-> E. m e. ( 0 ..^ ( # ` x ) ) ( x cyclShift m ) = u ) )
54 49 53 bitrid 
 |-  ( y = u -> ( E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) <-> E. m e. ( 0 ..^ ( # ` x ) ) ( x cyclShift m ) = u ) )
55 54 cbvrabv 
 |-  { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } = { u e. Word ( Vtx ` G ) | E. m e. ( 0 ..^ ( # ` x ) ) ( x cyclShift m ) = u }
56 55 cshwshashnsame 
 |-  ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) e. Prime ) -> ( E. i e. ( 0 ..^ ( # ` x ) ) ( x ` i ) =/= ( x ` 0 ) -> ( # ` { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) = ( # ` x ) ) )
57 56 ad2ant2rl 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ x e. ( ( # ` x ) ClWWalksN G ) ) /\ ( G e. UMGraph /\ ( # ` x ) e. Prime ) ) -> ( E. i e. ( 0 ..^ ( # ` x ) ) ( x ` i ) =/= ( x ` 0 ) -> ( # ` { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) = ( # ` x ) ) )
58 46 57 mpd 
 |-  ( ( ( x e. Word ( Vtx ` G ) /\ x e. ( ( # ` x ) ClWWalksN G ) ) /\ ( G e. UMGraph /\ ( # ` x ) e. Prime ) ) -> ( # ` { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) = ( # ` x ) )
59 39 58 sylan9eqr 
 |-  ( ( ( ( x e. Word ( Vtx ` G ) /\ x e. ( ( # ` x ) ClWWalksN G ) ) /\ ( G e. UMGraph /\ ( # ` x ) e. Prime ) ) /\ U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) -> ( # ` U ) = ( # ` x ) )
60 59 exp41 
 |-  ( x e. Word ( Vtx ` G ) -> ( x e. ( ( # ` x ) ClWWalksN G ) -> ( ( G e. UMGraph /\ ( # ` x ) e. Prime ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } -> ( # ` U ) = ( # ` x ) ) ) ) )
61 60 adantr 
 |-  ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) -> ( x e. ( ( # ` x ) ClWWalksN G ) -> ( ( G e. UMGraph /\ ( # ` x ) e. Prime ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } -> ( # ` U ) = ( # ` x ) ) ) ) )
62 oveq1 
 |-  ( N = ( # ` x ) -> ( N ClWWalksN G ) = ( ( # ` x ) ClWWalksN G ) )
63 62 eleq2d 
 |-  ( N = ( # ` x ) -> ( x e. ( N ClWWalksN G ) <-> x e. ( ( # ` x ) ClWWalksN G ) ) )
64 eleq1 
 |-  ( N = ( # ` x ) -> ( N e. Prime <-> ( # ` x ) e. Prime ) )
65 64 anbi2d 
 |-  ( N = ( # ` x ) -> ( ( G e. UMGraph /\ N e. Prime ) <-> ( G e. UMGraph /\ ( # ` x ) e. Prime ) ) )
66 oveq2 
 |-  ( N = ( # ` x ) -> ( 0 ..^ N ) = ( 0 ..^ ( # ` x ) ) )
67 66 rexeqdv 
 |-  ( N = ( # ` x ) -> ( E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) <-> E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) ) )
68 67 rabbidv 
 |-  ( N = ( # ` x ) -> { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } )
69 68 eqeq2d 
 |-  ( N = ( # ` x ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } <-> U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } ) )
70 eqeq2 
 |-  ( N = ( # ` x ) -> ( ( # ` U ) = N <-> ( # ` U ) = ( # ` x ) ) )
71 69 70 imbi12d 
 |-  ( N = ( # ` x ) -> ( ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } -> ( # ` U ) = N ) <-> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } -> ( # ` U ) = ( # ` x ) ) ) )
72 65 71 imbi12d 
 |-  ( N = ( # ` x ) -> ( ( ( G e. UMGraph /\ N e. Prime ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } -> ( # ` U ) = N ) ) <-> ( ( G e. UMGraph /\ ( # ` x ) e. Prime ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } -> ( # ` U ) = ( # ` x ) ) ) ) )
73 63 72 imbi12d 
 |-  ( N = ( # ` x ) -> ( ( x e. ( N ClWWalksN G ) -> ( ( G e. UMGraph /\ N e. Prime ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } -> ( # ` U ) = N ) ) ) <-> ( x e. ( ( # ` x ) ClWWalksN G ) -> ( ( G e. UMGraph /\ ( # ` x ) e. Prime ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } -> ( # ` U ) = ( # ` x ) ) ) ) ) )
74 73 eqcoms 
 |-  ( ( # ` x ) = N -> ( ( x e. ( N ClWWalksN G ) -> ( ( G e. UMGraph /\ N e. Prime ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } -> ( # ` U ) = N ) ) ) <-> ( x e. ( ( # ` x ) ClWWalksN G ) -> ( ( G e. UMGraph /\ ( # ` x ) e. Prime ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } -> ( # ` U ) = ( # ` x ) ) ) ) ) )
75 74 adantl 
 |-  ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) -> ( ( x e. ( N ClWWalksN G ) -> ( ( G e. UMGraph /\ N e. Prime ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } -> ( # ` U ) = N ) ) ) <-> ( x e. ( ( # ` x ) ClWWalksN G ) -> ( ( G e. UMGraph /\ ( # ` x ) e. Prime ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ ( # ` x ) ) y = ( x cyclShift n ) } -> ( # ` U ) = ( # ` x ) ) ) ) ) )
76 61 75 mpbird 
 |-  ( ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) -> ( x e. ( N ClWWalksN G ) -> ( ( G e. UMGraph /\ N e. Prime ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } -> ( # ` U ) = N ) ) ) )
77 31 76 mpcom 
 |-  ( x e. ( N ClWWalksN G ) -> ( ( G e. UMGraph /\ N e. Prime ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } -> ( # ` U ) = N ) ) )
78 77 1 eleq2s 
 |-  ( x e. W -> ( ( G e. UMGraph /\ N e. Prime ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } -> ( # ` U ) = N ) ) )
79 78 impcom 
 |-  ( ( ( G e. UMGraph /\ N e. Prime ) /\ x e. W ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ..^ N ) y = ( x cyclShift n ) } -> ( # ` U ) = N ) )
80 38 79 sylbid 
 |-  ( ( ( G e. UMGraph /\ N e. Prime ) /\ x e. W ) -> ( U = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } -> ( # ` U ) = N ) )
81 14 80 sylbid 
 |-  ( ( ( G e. UMGraph /\ N e. Prime ) /\ x e. W ) -> ( U = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } -> ( # ` U ) = N ) )
82 81 rexlimdva 
 |-  ( ( G e. UMGraph /\ N e. Prime ) -> ( E. x e. W U = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } -> ( # ` U ) = N ) )
83 82 com12 
 |-  ( E. x e. W U = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } -> ( ( G e. UMGraph /\ N e. Prime ) -> ( # ` U ) = N ) )
84 3 83 biimtrdi 
 |-  ( U e. ( W /. .~ ) -> ( U e. ( W /. .~ ) -> ( ( G e. UMGraph /\ N e. Prime ) -> ( # ` U ) = N ) ) )
85 84 pm2.43i 
 |-  ( U e. ( W /. .~ ) -> ( ( G e. UMGraph /\ N e. Prime ) -> ( # ` U ) = N ) )
86 85 com12 
 |-  ( ( G e. UMGraph /\ N e. Prime ) -> ( U e. ( W /. .~ ) -> ( # ` U ) = N ) )