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 𝑉 = ( Vtx ‘ 𝐺 )
Assertion numclwwlk3 ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) = ( ( ( 𝐾 − 1 ) · ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ) + ( 𝐾 ↑ ( 𝑁 − 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 numclwwlk3.v 𝑉 = ( Vtx ‘ 𝐺 )
2 simpl ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) → 𝐺 RegUSGraph 𝐾 )
3 simp1 ( ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → 𝑉 ∈ Fin )
4 1 finrusgrfusgr ( ( 𝐺 RegUSGraph 𝐾𝑉 ∈ Fin ) → 𝐺 ∈ FinUSGraph )
5 2 3 4 syl2an ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → 𝐺 ∈ FinUSGraph )
6 simpr2 ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → 𝑋𝑉 )
7 uzuzle23 ( 𝑁 ∈ ( ℤ ‘ 3 ) → 𝑁 ∈ ( ℤ ‘ 2 ) )
8 7 3ad2ant3 ( ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → 𝑁 ∈ ( ℤ ‘ 2 ) )
9 8 adantl ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → 𝑁 ∈ ( ℤ ‘ 2 ) )
10 eqid ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } ) = ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
11 eqid ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } ) = ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
12 10 11 numclwwlk3lem2 ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑋𝑉 ) ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) = ( ( ♯ ‘ ( 𝑋 ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } ) 𝑁 ) ) + ( ♯ ‘ ( 𝑋 ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } ) 𝑁 ) ) ) )
13 5 6 9 12 syl21anc ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) = ( ( ♯ ‘ ( 𝑋 ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } ) 𝑁 ) ) + ( ♯ ‘ ( 𝑋 ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } ) 𝑁 ) ) ) )
14 eqid ( 𝑣𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } ) = ( 𝑣𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } )
15 1 14 11 numclwwlk2 ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝑋 ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } ) 𝑁 ) ) = ( ( 𝐾 ↑ ( 𝑁 − 2 ) ) − ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ) )
16 2 3 anim12ci ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) )
17 3simpc ( ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) )
18 17 adantl ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) )
19 eqid ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
20 1 10 19 numclwwlk1 ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝑋 ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } ) 𝑁 ) ) = ( 𝐾 · ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ) )
21 16 18 20 syl2anc ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝑋 ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } ) 𝑁 ) ) = ( 𝐾 · ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ) )
22 15 21 oveq12d ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( ( ♯ ‘ ( 𝑋 ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } ) 𝑁 ) ) + ( ♯ ‘ ( 𝑋 ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } ) 𝑁 ) ) ) = ( ( ( 𝐾 ↑ ( 𝑁 − 2 ) ) − ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ) + ( 𝐾 · ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ) ) )
23 simpll ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → 𝐺 RegUSGraph 𝐾 )
24 ne0i ( 𝑋𝑉𝑉 ≠ ∅ )
25 24 3ad2ant2 ( ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → 𝑉 ≠ ∅ )
26 25 adantl ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → 𝑉 ≠ ∅ )
27 1 frusgrnn0 ( ( 𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾𝑉 ≠ ∅ ) → 𝐾 ∈ ℕ0 )
28 5 23 26 27 syl3anc ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → 𝐾 ∈ ℕ0 )
29 28 nn0cnd ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → 𝐾 ∈ ℂ )
30 uz3m2nn ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ℕ )
31 30 3anim3i ( ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( 𝑉 ∈ Fin ∧ 𝑋𝑉 ∧ ( 𝑁 − 2 ) ∈ ℕ ) )
32 31 adantl ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( 𝑉 ∈ Fin ∧ 𝑋𝑉 ∧ ( 𝑁 − 2 ) ∈ ℕ ) )
33 1 clwwlknonfin ( 𝑉 ∈ Fin → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∈ Fin )
34 33 3ad2ant1 ( ( 𝑉 ∈ Fin ∧ 𝑋𝑉 ∧ ( 𝑁 − 2 ) ∈ ℕ ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∈ Fin )
35 hashcl ( ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∈ Fin → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ∈ ℕ0 )
36 35 nn0cnd ( ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∈ Fin → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ∈ ℂ )
37 32 34 36 3syl ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ∈ ℂ )
38 numclwwlk3lem1 ( ( 𝐾 ∈ ℂ ∧ ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ∈ ℂ ∧ 𝑁 ∈ ( ℤ ‘ 2 ) ) → ( ( ( 𝐾 ↑ ( 𝑁 − 2 ) ) − ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ) + ( 𝐾 · ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ) ) = ( ( ( 𝐾 − 1 ) · ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ) + ( 𝐾 ↑ ( 𝑁 − 2 ) ) ) )
39 29 37 9 38 syl3anc ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( ( ( 𝐾 ↑ ( 𝑁 − 2 ) ) − ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ) + ( 𝐾 · ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ) ) = ( ( ( 𝐾 − 1 ) · ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ) + ( 𝐾 ↑ ( 𝑁 − 2 ) ) ) )
40 13 22 39 3eqtrd ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) = ( ( ( 𝐾 − 1 ) · ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ) + ( 𝐾 ↑ ( 𝑁 − 2 ) ) ) )