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 ) ) ) ) )