Metamath Proof Explorer

Theorem numclwwlk3

Description: Statement 12 in Huneke p. 2: "Thus f(n) = (k - 1)f(n - 2) + k^(n-2)." - the number of the closed walks v(0) ... v(n-2) v(n-1) v(n) is the sum of the number of the closed walks v(0) ... v(n-2) v(n-1) v(n) with v(n-2) = v(n) (see numclwwlk1 ) and with v(n-2) =/= v(n) (see numclwwlk2 ): f(n) = kf(n-2) + k^(n-2) - f(n-2) = (k-1)f(n-2) + k^(n-2). (Contributed by Alexander van der Vekens, 26-Aug-2018) (Revised by AV, 6-Mar-2022)

Ref Expression
Hypothesis numclwwlk3.v 
|- V = ( Vtx ` G )
Assertion numclwwlk3 
|- ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( X ( ClWWalksNOn ` G ) N ) ) = ( ( ( K - 1 ) x. ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) ) + ( K ^ ( N - 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 numclwwlk3.v 
 |-  V = ( Vtx ` G )
2 simpl 
 |-  ( ( G RegUSGraph K /\ G e. FriendGraph ) -> G RegUSGraph K )
3 simp1 
 |-  ( ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> V e. Fin )
4 1 finrusgrfusgr 
 |-  ( ( G RegUSGraph K /\ V e. Fin ) -> G e. FinUSGraph )
5 2 3 4 syl2an 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> G e. FinUSGraph )
6 simpr2 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> X e. V )
7 uzuzle23 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
8 7 3ad2ant3 
 |-  ( ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> N e. ( ZZ>= ` 2 ) )
9 8 adantl 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> N e. ( ZZ>= ` 2 ) )
10 eqid 
 |-  ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } ) = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
11 eqid 
 |-  ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } ) = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } )
12 10 11 numclwwlk3lem2 
 |-  ( ( ( G e. FinUSGraph /\ X e. V ) /\ N e. ( ZZ>= ` 2 ) ) -> ( # ` ( X ( ClWWalksNOn ` G ) N ) ) = ( ( # ` ( X ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } ) N ) ) + ( # ` ( X ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } ) N ) ) ) )
13 5 6 9 12 syl21anc 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( X ( ClWWalksNOn ` G ) N ) ) = ( ( # ` ( X ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } ) N ) ) + ( # ` ( X ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } ) N ) ) ) )
14 eqid 
 |-  ( v e. V , n e. NN |-> { w e. ( n WWalksN G ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } ) = ( v e. V , n e. NN |-> { w e. ( n WWalksN G ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } )
15 1 14 11 numclwwlk2 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( X ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } ) N ) ) = ( ( K ^ ( N - 2 ) ) - ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) ) )
16 2 3 anim12ci 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( V e. Fin /\ G RegUSGraph K ) )
17 3simpc 
 |-  ( ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( X e. V /\ N e. ( ZZ>= ` 3 ) ) )
18 17 adantl 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( X e. V /\ N e. ( ZZ>= ` 3 ) ) )
19 eqid 
 |-  ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) = ( X ( ClWWalksNOn ` G ) ( N - 2 ) )
20 1 10 19 numclwwlk1 
 |-  ( ( ( V e. Fin /\ G RegUSGraph K ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( X ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } ) N ) ) = ( K x. ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) ) )
21 16 18 20 syl2anc 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( X ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } ) N ) ) = ( K x. ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) ) )
22 15 21 oveq12d 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( ( # ` ( X ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } ) N ) ) + ( # ` ( X ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } ) N ) ) ) = ( ( ( K ^ ( N - 2 ) ) - ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) ) + ( K x. ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) ) ) )
23 simpll 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> G RegUSGraph K )
24 ne0i 
 |-  ( X e. V -> V =/= (/) )
25 24 3ad2ant2 
 |-  ( ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> V =/= (/) )
26 25 adantl 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> V =/= (/) )
27 1 frusgrnn0 
 |-  ( ( G e. FinUSGraph /\ G RegUSGraph K /\ V =/= (/) ) -> K e. NN0 )
28 5 23 26 27 syl3anc 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> K e. NN0 )
29 28 nn0cnd 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> K e. CC )
30 uz3m2nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. NN )
31 30 3anim3i 
 |-  ( ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( V e. Fin /\ X e. V /\ ( N - 2 ) e. NN ) )
32 31 adantl 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( V e. Fin /\ X e. V /\ ( N - 2 ) e. NN ) )
33 1 clwwlknonfin 
 |-  ( V e. Fin -> ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) e. Fin )
34 33 3ad2ant1 
 |-  ( ( V e. Fin /\ X e. V /\ ( N - 2 ) e. NN ) -> ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) e. Fin )
35 hashcl 
 |-  ( ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) e. Fin -> ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) e. NN0 )
36 35 nn0cnd 
 |-  ( ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) e. Fin -> ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) e. CC )
37 32 34 36 3syl 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) e. CC )
38 numclwwlk3lem1 
 |-  ( ( K e. CC /\ ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) e. CC /\ N e. ( ZZ>= ` 2 ) ) -> ( ( ( K ^ ( N - 2 ) ) - ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) ) + ( K x. ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) ) ) = ( ( ( K - 1 ) x. ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) ) + ( K ^ ( N - 2 ) ) ) )
39 29 37 9 38 syl3anc 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( ( ( K ^ ( N - 2 ) ) - ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) ) + ( K x. ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) ) ) = ( ( ( K - 1 ) x. ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) ) + ( K ^ ( N - 2 ) ) ) )
40 13 22 39 3eqtrd 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V e. Fin /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( # ` ( X ( ClWWalksNOn ` G ) N ) ) = ( ( ( K - 1 ) x. ( # ` ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) ) + ( K ^ ( N - 2 ) ) ) )