Metamath Proof Explorer

Theorem numclwwlk2

Description: Statement 10 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 k^(n-2) - f(n-2)." According to rusgrnumwlkg , we have k^(n-2) different walks of length (n-2): v(0) ... v(n-2). From this number, the number of closed walks of length (n-2), which is f(n-2) per definition, must be subtracted, because for these walks v(n-2) =/= v(0) = v would hold. Because of the friendship condition, there is exactly one vertex v(n-1) which is a neighbor of v(n-2) as well as of v(n)=v=v(0), because v(n-2) and v(n)=v are different, so the number of walks v(0) ... v(n-2) is identical with the number of walks v(0) ... v(n), that means each (not closed) walk v(0) ... v(n-2) can be extended by two edges to a closed walk v(0) ... v(n)=v=v(0) in exactly one way. (Contributed by Alexander van der Vekens, 6-Oct-2018) (Revised by AV, 31-May-2021) (Revised by AV, 1-May-2022)

Ref Expression
Hypotheses numclwwlk.v 
|- V = ( Vtx ` G )
numclwwlk.q 
|- Q = ( v e. V , n e. NN |-> { w e. ( n WWalksN G ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } )
numclwwlk.h 
|- H = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } )
Assertion numclwwlk2 
|- ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( X H N ) ) = ( ( K ^ ( N - 2 ) ) - ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 numclwwlk.v 
 |-  V = ( Vtx ` G )
2 numclwwlk.q 
 |-  Q = ( v e. V , n e. NN |-> { w e. ( n WWalksN G ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } )
3 numclwwlk.h 
 |-  H = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } )
4 eluzelcn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. CC )
5 2cnd 
 |-  ( N e. ( ZZ>= ` 3 ) -> 2 e. CC )
6 4 5 npcand 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( N - 2 ) + 2 ) = N )
7 6 eqcomd 
 |-  ( N e. ( ZZ>= ` 3 ) -> N = ( ( N - 2 ) + 2 ) )
8 7 3ad2ant3 
 |-  ( ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> N = ( ( N - 2 ) + 2 ) )
9 8 adantl 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> N = ( ( N - 2 ) + 2 ) )
10 9 oveq2d 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( X H N ) = ( X H ( ( N - 2 ) + 2 ) ) )
11 10 fveq2d 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( X H N ) ) = ( # ` ( X H ( ( N - 2 ) + 2 ) ) ) )
12 simplr 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> G e. FriendGraph )
13 simpr2 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> X e. V )
14 uz3m2nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. NN )
15 14 3ad2ant3 
 |-  ( ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( N - 2 ) e. NN )
16 15 adantl 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( N - 2 ) e. NN )
17 1 2 3 numclwwlk2lem3 
 |-  ( ( G e. FriendGraph /\ X e. V /\ ( N - 2 ) e. NN ) -> ( # ` ( X Q ( N - 2 ) ) ) = ( # ` ( X H ( ( N - 2 ) + 2 ) ) ) )
18 12 13 16 17 syl3anc 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( X Q ( N - 2 ) ) ) = ( # ` ( X H ( ( N - 2 ) + 2 ) ) ) )
19 simpl 
 |-  ( ( G RegUSGraph K /\ G e. FriendGraph ) -> G RegUSGraph K )
20 simp1 
 |-  ( ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> V e. Fin )
21 19 20 anim12i 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( G RegUSGraph K /\ V e. Fin ) )
22 14 anim2i 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( X e. V /\ ( N - 2 ) e. NN ) )
23 22 3adant1 
 |-  ( ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( X e. V /\ ( N - 2 ) e. NN ) )
24 23 adantl 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( X e. V /\ ( N - 2 ) e. NN ) )
25 1 2 numclwwlkqhash 
 |-  ( ( ( G RegUSGraph K /\ V e. Fin ) /\ ( X e. V /\ ( N - 2 ) e. NN ) ) -> ( # ` ( X Q ( N - 2 ) ) ) = ( ( K ^ ( N - 2 ) ) - ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) ) )
26 21 24 25 syl2anc 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( X Q ( N - 2 ) ) ) = ( ( K ^ ( N - 2 ) ) - ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) ) )
27 11 18 26 3eqtr2d 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( X H N ) ) = ( ( K ^ ( N - 2 ) ) - ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) ) )