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