Metamath Proof Explorer

Theorem fusgrhashclwwlkn

Description: The size of the set of closed walks (defined as words) with a fixed length which is a prime number is the product of the number of equivalence classes for .~ over the set of closed walks and the fixed 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 e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
Assertion fusgrhashclwwlkn 
|- ( ( G e. FinUSGraph /\ N e. Prime ) -> ( # ` W ) = ( ( # ` ( W /. .~ ) ) x. 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 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
4 3 fusgrvtxfi 
 |-  ( G e. FinUSGraph -> ( Vtx ` G ) e. Fin )
5 4 adantr 
 |-  ( ( G e. FinUSGraph /\ N e. Prime ) -> ( Vtx ` G ) e. Fin )
6 1 2 hashclwwlkn0 
 |-  ( ( Vtx ` G ) e. Fin -> ( # ` W ) = sum_ x e. ( W /. .~ ) ( # ` x ) )
7 5 6 syl 
 |-  ( ( G e. FinUSGraph /\ N e. Prime ) -> ( # ` W ) = sum_ x e. ( W /. .~ ) ( # ` x ) )
8 fusgrusgr 
 |-  ( G e. FinUSGraph -> G e. USGraph )
9 usgrumgr 
 |-  ( G e. USGraph -> G e. UMGraph )
10 8 9 syl 
 |-  ( G e. FinUSGraph -> G e. UMGraph )
11 1 2 umgrhashecclwwlk 
 |-  ( ( G e. UMGraph /\ N e. Prime ) -> ( x e. ( W /. .~ ) -> ( # ` x ) = N ) )
12 10 11 sylan 
 |-  ( ( G e. FinUSGraph /\ N e. Prime ) -> ( x e. ( W /. .~ ) -> ( # ` x ) = N ) )
13 12 imp 
 |-  ( ( ( G e. FinUSGraph /\ N e. Prime ) /\ x e. ( W /. .~ ) ) -> ( # ` x ) = N )
14 13 sumeq2dv 
 |-  ( ( G e. FinUSGraph /\ N e. Prime ) -> sum_ x e. ( W /. .~ ) ( # ` x ) = sum_ x e. ( W /. .~ ) N )
15 1 2 qerclwwlknfi 
 |-  ( ( Vtx ` G ) e. Fin -> ( W /. .~ ) e. Fin )
16 5 15 syl 
 |-  ( ( G e. FinUSGraph /\ N e. Prime ) -> ( W /. .~ ) e. Fin )
17 prmnn 
 |-  ( N e. Prime -> N e. NN )
18 17 nncnd 
 |-  ( N e. Prime -> N e. CC )
19 18 adantl 
 |-  ( ( G e. FinUSGraph /\ N e. Prime ) -> N e. CC )
20 fsumconst 
 |-  ( ( ( W /. .~ ) e. Fin /\ N e. CC ) -> sum_ x e. ( W /. .~ ) N = ( ( # ` ( W /. .~ ) ) x. N ) )
21 16 19 20 syl2anc 
 |-  ( ( G e. FinUSGraph /\ N e. Prime ) -> sum_ x e. ( W /. .~ ) N = ( ( # ` ( W /. .~ ) ) x. N ) )
22 7 14 21 3eqtrd 
 |-  ( ( G e. FinUSGraph /\ N e. Prime ) -> ( # ` W ) = ( ( # ` ( W /. .~ ) ) x. N ) )