Metamath Proof Explorer

Theorem numclwlk1

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. (Contributed by AV, 23-May-2022)

Ref Expression
Hypotheses numclwlk1.v 
|- V = ( Vtx ` G )
numclwlk1.c 
|- C = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` ( N - 2 ) ) = X ) }
numclwlk1.f 
|- F = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = ( N - 2 ) /\ ( ( 2nd ` w ) ` 0 ) = X ) }
Assertion numclwlk1 
|- ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 2 ) ) ) -> ( # ` C ) = ( K x. ( # ` F ) ) )

Proof

Step Hyp Ref Expression
1 numclwlk1.v 
 |-  V = ( Vtx ` G )
2 numclwlk1.c 
 |-  C = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = N /\ ( ( 2nd ` w ) ` 0 ) = X /\ ( ( 2nd ` w ) ` ( N - 2 ) ) = X ) }
3 numclwlk1.f 
 |-  F = { w e. ( ClWalks ` G ) | ( ( # ` ( 1st ` w ) ) = ( N - 2 ) /\ ( ( 2nd ` w ) ` 0 ) = X ) }
4 uzp1 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N = 2 \/ N e. ( ZZ>= ` ( 2 + 1 ) ) ) )
5 1 2 3 numclwlk1lem1 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N = 2 ) ) -> ( # ` C ) = ( K x. ( # ` F ) ) )
6 5 expcom 
 |-  ( ( X e. V /\ N = 2 ) -> ( ( V e. Fin /\ G RegUSGraph K ) -> ( # ` C ) = ( K x. ( # ` F ) ) ) )
7 6 expcom 
 |-  ( N = 2 -> ( X e. V -> ( ( V e. Fin /\ G RegUSGraph K ) -> ( # ` C ) = ( K x. ( # ` F ) ) ) ) )
8 1 2 3 numclwlk1lem2 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` C ) = ( K x. ( # ` F ) ) )
9 8 expcom 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( V e. Fin /\ G RegUSGraph K ) -> ( # ` C ) = ( K x. ( # ` F ) ) ) )
10 9 expcom 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( X e. V -> ( ( V e. Fin /\ G RegUSGraph K ) -> ( # ` C ) = ( K x. ( # ` F ) ) ) ) )
11 2p1e3 
 |-  ( 2 + 1 ) = 3
12 11 fveq2i 
 |-  ( ZZ>= ` ( 2 + 1 ) ) = ( ZZ>= ` 3 )
13 10 12 eleq2s 
 |-  ( N e. ( ZZ>= ` ( 2 + 1 ) ) -> ( X e. V -> ( ( V e. Fin /\ G RegUSGraph K ) -> ( # ` C ) = ( K x. ( # ` F ) ) ) ) )
14 7 13 jaoi 
 |-  ( ( N = 2 \/ N e. ( ZZ>= ` ( 2 + 1 ) ) ) -> ( X e. V -> ( ( V e. Fin /\ G RegUSGraph K ) -> ( # ` C ) = ( K x. ( # ` F ) ) ) ) )
15 4 14 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( X e. V -> ( ( V e. Fin /\ G RegUSGraph K ) -> ( # ` C ) = ( K x. ( # ` F ) ) ) ) )
16 15 impcom 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( ( V e. Fin /\ G RegUSGraph K ) -> ( # ` C ) = ( K x. ( # ` F ) ) ) )
17 16 impcom 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 2 ) ) ) -> ( # ` C ) = ( K x. ( # ` F ) ) )