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 𝑉 = ( Vtx ‘ 𝐺 )
numclwwlk.q 𝑄 = ( 𝑣𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } )
numclwwlk.h 𝐻 = ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
Assertion numclwwlk2 ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝑋 𝐻 𝑁 ) ) = ( ( 𝐾 ↑ ( 𝑁 − 2 ) ) − ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 numclwwlk.v 𝑉 = ( Vtx ‘ 𝐺 )
2 numclwwlk.q 𝑄 = ( 𝑣𝑉 , 𝑛 ∈ ℕ ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑣 ∧ ( lastS ‘ 𝑤 ) ≠ 𝑣 ) } )
3 numclwwlk.h 𝐻 = ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) ≠ 𝑣 } )
4 eluzelcn ( 𝑁 ∈ ( ℤ ‘ 3 ) → 𝑁 ∈ ℂ )
5 2cnd ( 𝑁 ∈ ( ℤ ‘ 3 ) → 2 ∈ ℂ )
6 4 5 npcand ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( ( 𝑁 − 2 ) + 2 ) = 𝑁 )
7 6 eqcomd ( 𝑁 ∈ ( ℤ ‘ 3 ) → 𝑁 = ( ( 𝑁 − 2 ) + 2 ) )
8 7 3ad2ant3 ( ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → 𝑁 = ( ( 𝑁 − 2 ) + 2 ) )
9 8 adantl ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → 𝑁 = ( ( 𝑁 − 2 ) + 2 ) )
10 9 oveq2d ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( 𝑋 𝐻 𝑁 ) = ( 𝑋 𝐻 ( ( 𝑁 − 2 ) + 2 ) ) )
11 10 fveq2d ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝑋 𝐻 𝑁 ) ) = ( ♯ ‘ ( 𝑋 𝐻 ( ( 𝑁 − 2 ) + 2 ) ) ) )
12 simplr ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → 𝐺 ∈ FriendGraph )
13 simpr2 ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → 𝑋𝑉 )
14 uz3m2nn ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ℕ )
15 14 3ad2ant3 ( ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( 𝑁 − 2 ) ∈ ℕ )
16 15 adantl ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( 𝑁 − 2 ) ∈ ℕ )
17 1 2 3 numclwwlk2lem3 ( ( 𝐺 ∈ FriendGraph ∧ 𝑋𝑉 ∧ ( 𝑁 − 2 ) ∈ ℕ ) → ( ♯ ‘ ( 𝑋 𝑄 ( 𝑁 − 2 ) ) ) = ( ♯ ‘ ( 𝑋 𝐻 ( ( 𝑁 − 2 ) + 2 ) ) ) )
18 12 13 16 17 syl3anc ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝑋 𝑄 ( 𝑁 − 2 ) ) ) = ( ♯ ‘ ( 𝑋 𝐻 ( ( 𝑁 − 2 ) + 2 ) ) ) )
19 simpl ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) → 𝐺 RegUSGraph 𝐾 )
20 simp1 ( ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → 𝑉 ∈ Fin )
21 19 20 anim12i ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( 𝐺 RegUSGraph 𝐾𝑉 ∈ Fin ) )
22 14 anim2i ( ( 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( 𝑋𝑉 ∧ ( 𝑁 − 2 ) ∈ ℕ ) )
23 22 3adant1 ( ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → ( 𝑋𝑉 ∧ ( 𝑁 − 2 ) ∈ ℕ ) )
24 23 adantl ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( 𝑋𝑉 ∧ ( 𝑁 − 2 ) ∈ ℕ ) )
25 1 2 numclwwlkqhash ( ( ( 𝐺 RegUSGraph 𝐾𝑉 ∈ Fin ) ∧ ( 𝑋𝑉 ∧ ( 𝑁 − 2 ) ∈ ℕ ) ) → ( ♯ ‘ ( 𝑋 𝑄 ( 𝑁 − 2 ) ) ) = ( ( 𝐾 ↑ ( 𝑁 − 2 ) ) − ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ) )
26 21 24 25 syl2anc ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝑋 𝑄 ( 𝑁 − 2 ) ) ) = ( ( 𝐾 ↑ ( 𝑁 − 2 ) ) − ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ) )
27 11 18 26 3eqtr2d ( ( ( 𝐺 RegUSGraph 𝐾𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ∈ Fin ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝑋 𝐻 𝑁 ) ) = ( ( 𝐾 ↑ ( 𝑁 − 2 ) ) − ( ♯ ‘ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) ) )