Metamath Proof Explorer

Theorem clwwlkndivn

Description: The size of the set of closed walks (defined as words) of length N is divisible by N if N is a prime number. (Contributed by Alexander van der Vekens, 17-Jun-2018) (Revised by AV, 2-May-2021)

Ref Expression
Assertion clwwlkndivn 
|- ( ( G e. FinUSGraph /\ N e. Prime ) -> N || ( # ` ( N ClWWalksN G ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 1 fusgrvtxfi 
 |-  ( G e. FinUSGraph -> ( Vtx ` G ) e. Fin )
3 2 adantr 
 |-  ( ( G e. FinUSGraph /\ N e. Prime ) -> ( Vtx ` G ) e. Fin )
4 eqid 
 |-  ( N ClWWalksN G ) = ( N ClWWalksN G )
5 eqid 
 |-  { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } = { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
6 4 5 qerclwwlknfi 
 |-  ( ( Vtx ` G ) e. Fin -> ( ( N ClWWalksN G ) /. { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } ) e. Fin )
7 hashcl 
 |-  ( ( ( N ClWWalksN G ) /. { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } ) e. Fin -> ( # ` ( ( N ClWWalksN G ) /. { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } ) ) e. NN0 )
8 3 6 7 3syl 
 |-  ( ( G e. FinUSGraph /\ N e. Prime ) -> ( # ` ( ( N ClWWalksN G ) /. { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } ) ) e. NN0 )
9 8 nn0zd 
 |-  ( ( G e. FinUSGraph /\ N e. Prime ) -> ( # ` ( ( N ClWWalksN G ) /. { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } ) ) e. ZZ )
10 prmz 
 |-  ( N e. Prime -> N e. ZZ )
11 10 adantl 
 |-  ( ( G e. FinUSGraph /\ N e. Prime ) -> N e. ZZ )
12 dvdsmul2 
 |-  ( ( ( # ` ( ( N ClWWalksN G ) /. { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } ) ) e. ZZ /\ N e. ZZ ) -> N || ( ( # ` ( ( N ClWWalksN G ) /. { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } ) ) x. N ) )
13 9 11 12 syl2anc 
 |-  ( ( G e. FinUSGraph /\ N e. Prime ) -> N || ( ( # ` ( ( N ClWWalksN G ) /. { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } ) ) x. N ) )
14 4 5 fusgrhashclwwlkn 
 |-  ( ( G e. FinUSGraph /\ N e. Prime ) -> ( # ` ( N ClWWalksN G ) ) = ( ( # ` ( ( N ClWWalksN G ) /. { <. t , u >. | ( t e. ( N ClWWalksN G ) /\ u e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } ) ) x. N ) )
15 13 14 breqtrrd 
 |-  ( ( G e. FinUSGraph /\ N e. Prime ) -> N || ( # ` ( N ClWWalksN G ) ) )