Metamath Proof Explorer

Theorem numclwwlk1

Description: Statement 9 in Huneke p. 2: "If n > 1, then the number of closed n-walks v(0) ... v(n-2) v(n-1) v(n) from v = v(0) = v(n) with v(n-2) = v is kf(n-2)". Since G is k-regular, the vertex v(n-2) = v has k neighbors v(n-1), so there are k walks from v(n-2) = v to v(n) = v (via each of v's neighbors) completing each of the f(n-2) walks from v=v(0) to v(n-2)=v. This theorem holds even for k=0, but not for n=2, since F = (/) , but ( X C 2 ) , the set of closed walks with length 2 on X , see 2clwwlk2 , needs not be (/) in this case. This is because of the special definition of F and the usage of words to represent (closed) walks, and does not contradict Huneke's statement, which would read "the number of closed 2-walks v(0) v(1) v(2) from v = v(0) = v(2) ... is kf(0)", where f(0)=1 is the number of empty closed walks on v, see numclwlk1lem1 . If the general representation of (closed) walk is used, Huneke's statement can be proven even for n = 2, see numclwlk1 . This case, however, is not required to prove the friendship theorem. (Contributed by Alexander van der Vekens, 26-Sep-2018) (Revised by AV, 29-May-2021) (Revised by AV, 6-Mar-2022) (Proof shortened by AV, 31-Jul-2022)

Ref Expression
Hypotheses extwwlkfab.v 
|- V = ( Vtx ` G )
extwwlkfab.c 
|- C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
extwwlkfab.f 
|- F = ( X ( ClWWalksNOn ` G ) ( N - 2 ) )
Assertion numclwwlk1 
|- ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( X C N ) ) = ( K x. ( # ` F ) ) )

Proof

Step Hyp Ref Expression
1 extwwlkfab.v 
 |-  V = ( Vtx ` G )
2 extwwlkfab.c 
 |-  C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
3 extwwlkfab.f 
 |-  F = ( X ( ClWWalksNOn ` G ) ( N - 2 ) )
4 rusgrusgr 
 |-  ( G RegUSGraph K -> G e. USGraph )
5 4 ad2antlr 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> G e. USGraph )
6 simprl 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> X e. V )
7 simprr 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> N e. ( ZZ>= ` 3 ) )
8 1 2 3 numclwwlk1lem2 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( X C N ) ~~ ( F X. ( G NeighbVtx X ) ) )
9 5 6 7 8 syl3anc 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( X C N ) ~~ ( F X. ( G NeighbVtx X ) ) )
10 hasheni 
 |-  ( ( X C N ) ~~ ( F X. ( G NeighbVtx X ) ) -> ( # ` ( X C N ) ) = ( # ` ( F X. ( G NeighbVtx X ) ) ) )
11 9 10 syl 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( X C N ) ) = ( # ` ( F X. ( G NeighbVtx X ) ) ) )
12 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
13 12 clwwlknonfin 
 |-  ( ( Vtx ` G ) e. Fin -> ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) e. Fin )
14 1 eleq1i 
 |-  ( V e. Fin <-> ( Vtx ` G ) e. Fin )
15 3 eleq1i 
 |-  ( F e. Fin <-> ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) e. Fin )
16 13 14 15 3imtr4i 
 |-  ( V e. Fin -> F e. Fin )
17 16 adantr 
 |-  ( ( V e. Fin /\ G RegUSGraph K ) -> F e. Fin )
18 17 adantr 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> F e. Fin )
19 1 finrusgrfusgr 
 |-  ( ( G RegUSGraph K /\ V e. Fin ) -> G e. FinUSGraph )
20 19 ancoms 
 |-  ( ( V e. Fin /\ G RegUSGraph K ) -> G e. FinUSGraph )
21 fusgrfis 
 |-  ( G e. FinUSGraph -> ( Edg ` G ) e. Fin )
22 20 21 syl 
 |-  ( ( V e. Fin /\ G RegUSGraph K ) -> ( Edg ` G ) e. Fin )
23 22 adantr 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( Edg ` G ) e. Fin )
24 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
25 1 24 nbusgrfi 
 |-  ( ( G e. USGraph /\ ( Edg ` G ) e. Fin /\ X e. V ) -> ( G NeighbVtx X ) e. Fin )
26 5 23 6 25 syl3anc 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( G NeighbVtx X ) e. Fin )
27 hashxp 
 |-  ( ( F e. Fin /\ ( G NeighbVtx X ) e. Fin ) -> ( # ` ( F X. ( G NeighbVtx X ) ) ) = ( ( # ` F ) x. ( # ` ( G NeighbVtx X ) ) ) )
28 18 26 27 syl2anc 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( F X. ( G NeighbVtx X ) ) ) = ( ( # ` F ) x. ( # ` ( G NeighbVtx X ) ) ) )
29 1 rusgrpropnb 
 |-  ( G RegUSGraph K -> ( G e. USGraph /\ K e. NN0* /\ A. x e. V ( # ` ( G NeighbVtx x ) ) = K ) )
30 oveq2 
 |-  ( x = X -> ( G NeighbVtx x ) = ( G NeighbVtx X ) )
31 30 fveqeq2d 
 |-  ( x = X -> ( ( # ` ( G NeighbVtx x ) ) = K <-> ( # ` ( G NeighbVtx X ) ) = K ) )
32 31 rspccv 
 |-  ( A. x e. V ( # ` ( G NeighbVtx x ) ) = K -> ( X e. V -> ( # ` ( G NeighbVtx X ) ) = K ) )
33 32 3ad2ant3 
 |-  ( ( G e. USGraph /\ K e. NN0* /\ A. x e. V ( # ` ( G NeighbVtx x ) ) = K ) -> ( X e. V -> ( # ` ( G NeighbVtx X ) ) = K ) )
34 29 33 syl 
 |-  ( G RegUSGraph K -> ( X e. V -> ( # ` ( G NeighbVtx X ) ) = K ) )
35 34 adantl 
 |-  ( ( V e. Fin /\ G RegUSGraph K ) -> ( X e. V -> ( # ` ( G NeighbVtx X ) ) = K ) )
36 35 com12 
 |-  ( X e. V -> ( ( V e. Fin /\ G RegUSGraph K ) -> ( # ` ( G NeighbVtx X ) ) = K ) )
37 36 adantr 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( V e. Fin /\ G RegUSGraph K ) -> ( # ` ( G NeighbVtx X ) ) = K ) )
38 37 impcom 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( G NeighbVtx X ) ) = K )
39 38 oveq2d 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( ( # ` F ) x. ( # ` ( G NeighbVtx X ) ) ) = ( ( # ` F ) x. K ) )
40 hashcl 
 |-  ( F e. Fin -> ( # ` F ) e. NN0 )
41 nn0cn 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. CC )
42 18 40 41 3syl 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` F ) e. CC )
43 20 adantr 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> G e. FinUSGraph )
44 simplr 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> G RegUSGraph K )
45 ne0i 
 |-  ( X e. V -> V =/= (/) )
46 45 adantr 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> V =/= (/) )
47 46 adantl 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> V =/= (/) )
48 1 frusgrnn0 
 |-  ( ( G e. FinUSGraph /\ G RegUSGraph K /\ V =/= (/) ) -> K e. NN0 )
49 43 44 47 48 syl3anc 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> K e. NN0 )
50 49 nn0cnd 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> K e. CC )
51 42 50 mulcomd 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( ( # ` F ) x. K ) = ( K x. ( # ` F ) ) )
52 39 51 eqtrd 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( ( # ` F ) x. ( # ` ( G NeighbVtx X ) ) ) = ( K x. ( # ` F ) ) )
53 11 28 52 3eqtrd 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( X C N ) ) = ( K x. ( # ` F ) ) )