Metamath Proof Explorer

Theorem numclwwlk6

Description: For a prime divisor P of K - 1 , the total number of closed walks of length P in a K-regular friendship graph is equal modulo P to the number of vertices. (Contributed by Alexander van der Vekens, 7-Oct-2018) (Revised by AV, 3-Jun-2021) (Proof shortened by AV, 7-Mar-2022)

Ref Expression
Hypothesis numclwwlk6.v 
|- V = ( Vtx ` G )
Assertion numclwwlk6 
|- ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( # ` ( P ClWWalksN G ) ) mod P ) = ( ( # ` V ) mod P ) )

Proof

Step Hyp Ref Expression
1 numclwwlk6.v 
 |-  V = ( Vtx ` G )
2 1 finrusgrfusgr 
 |-  ( ( G RegUSGraph K /\ V e. Fin ) -> G e. FinUSGraph )
3 2 3adant2 
 |-  ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) -> G e. FinUSGraph )
4 prmnn 
 |-  ( P e. Prime -> P e. NN )
5 4 adantr 
 |-  ( ( P e. Prime /\ P || ( K - 1 ) ) -> P e. NN )
6 1 numclwwlk4 
 |-  ( ( G e. FinUSGraph /\ P e. NN ) -> ( # ` ( P ClWWalksN G ) ) = sum_ x e. V ( # ` ( x ( ClWWalksNOn ` G ) P ) ) )
7 3 5 6 syl2an 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( # ` ( P ClWWalksN G ) ) = sum_ x e. V ( # ` ( x ( ClWWalksNOn ` G ) P ) ) )
8 7 oveq1d 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( # ` ( P ClWWalksN G ) ) mod P ) = ( sum_ x e. V ( # ` ( x ( ClWWalksNOn ` G ) P ) ) mod P ) )
9 5 adantl 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> P e. NN )
10 simp3 
 |-  ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) -> V e. Fin )
11 10 adantr 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> V e. Fin )
12 11 adantr 
 |-  ( ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) /\ x e. V ) -> V e. Fin )
13 1 clwwlknonfin 
 |-  ( V e. Fin -> ( x ( ClWWalksNOn ` G ) P ) e. Fin )
14 hashcl 
 |-  ( ( x ( ClWWalksNOn ` G ) P ) e. Fin -> ( # ` ( x ( ClWWalksNOn ` G ) P ) ) e. NN0 )
15 12 13 14 3syl 
 |-  ( ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) /\ x e. V ) -> ( # ` ( x ( ClWWalksNOn ` G ) P ) ) e. NN0 )
16 15 nn0zd 
 |-  ( ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) /\ x e. V ) -> ( # ` ( x ( ClWWalksNOn ` G ) P ) ) e. ZZ )
17 16 ralrimiva 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> A. x e. V ( # ` ( x ( ClWWalksNOn ` G ) P ) ) e. ZZ )
18 9 11 17 modfsummod 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( sum_ x e. V ( # ` ( x ( ClWWalksNOn ` G ) P ) ) mod P ) = ( sum_ x e. V ( ( # ` ( x ( ClWWalksNOn ` G ) P ) ) mod P ) mod P ) )
19 simpl 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) )
20 simpr 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( P e. Prime /\ P || ( K - 1 ) ) )
21 20 anim1ci 
 |-  ( ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) /\ x e. V ) -> ( x e. V /\ ( P e. Prime /\ P || ( K - 1 ) ) ) )
22 3anass 
 |-  ( ( x e. V /\ P e. Prime /\ P || ( K - 1 ) ) <-> ( x e. V /\ ( P e. Prime /\ P || ( K - 1 ) ) ) )
23 21 22 sylibr 
 |-  ( ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) /\ x e. V ) -> ( x e. V /\ P e. Prime /\ P || ( K - 1 ) ) )
24 1 numclwwlk5 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( x e. V /\ P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( # ` ( x ( ClWWalksNOn ` G ) P ) ) mod P ) = 1 )
25 19 23 24 syl2an2r 
 |-  ( ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) /\ x e. V ) -> ( ( # ` ( x ( ClWWalksNOn ` G ) P ) ) mod P ) = 1 )
26 25 sumeq2dv 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> sum_ x e. V ( ( # ` ( x ( ClWWalksNOn ` G ) P ) ) mod P ) = sum_ x e. V 1 )
27 26 oveq1d 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( sum_ x e. V ( ( # ` ( x ( ClWWalksNOn ` G ) P ) ) mod P ) mod P ) = ( sum_ x e. V 1 mod P ) )
28 18 27 eqtrd 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( sum_ x e. V ( # ` ( x ( ClWWalksNOn ` G ) P ) ) mod P ) = ( sum_ x e. V 1 mod P ) )
29 1cnd 
 |-  ( ( P e. Prime /\ P || ( K - 1 ) ) -> 1 e. CC )
30 fsumconst 
 |-  ( ( V e. Fin /\ 1 e. CC ) -> sum_ x e. V 1 = ( ( # ` V ) x. 1 ) )
31 10 29 30 syl2an 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> sum_ x e. V 1 = ( ( # ` V ) x. 1 ) )
32 hashcl 
 |-  ( V e. Fin -> ( # ` V ) e. NN0 )
33 32 nn0red 
 |-  ( V e. Fin -> ( # ` V ) e. RR )
34 ax-1rid 
 |-  ( ( # ` V ) e. RR -> ( ( # ` V ) x. 1 ) = ( # ` V ) )
35 33 34 syl 
 |-  ( V e. Fin -> ( ( # ` V ) x. 1 ) = ( # ` V ) )
36 35 3ad2ant3 
 |-  ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) -> ( ( # ` V ) x. 1 ) = ( # ` V ) )
37 36 adantr 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( # ` V ) x. 1 ) = ( # ` V ) )
38 31 37 eqtrd 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> sum_ x e. V 1 = ( # ` V ) )
39 38 oveq1d 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( sum_ x e. V 1 mod P ) = ( ( # ` V ) mod P ) )
40 8 28 39 3eqtrd 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph /\ V e. Fin ) /\ ( P e. Prime /\ P || ( K - 1 ) ) ) -> ( ( # ` ( P ClWWalksN G ) ) mod P ) = ( ( # ` V ) mod P ) )