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∈V,n∈ℕ⟼w∈nWWalksNG|w⁡0=v∧lastS⁡w≠v
numclwwlk.h ⊢H=v∈V,n∈ℤ≥2⟼w∈vClWWalksNOn⁡Gn|w⁡n−2≠v
Assertion numclwwlk2 ⊢GRegUSGraphK∧G∈FriendGraph∧V∈Fin∧X∈V∧N∈ℤ≥3→XHN=KN−2−XClWWalksNOn⁡GN−2

Proof

Step Hyp Ref Expression
1 numclwwlk.v ⊢V=Vtx⁡G
2 numclwwlk.q ⊢Q=v∈V,n∈ℕ⟼w∈nWWalksNG|w⁡0=v∧lastS⁡w≠v
3 numclwwlk.h ⊢H=v∈V,n∈ℤ≥2⟼w∈vClWWalksNOn⁡Gn|w⁡n−2≠v
4 eluzelcn ⊢N∈ℤ≥3→N∈ℂ
5 2cnd ⊢N∈ℤ≥3→2∈ℂ
6 4 5 npcand ⊢N∈ℤ≥3→N-2+2=N
7 6 eqcomd ⊢N∈ℤ≥3→N=N-2+2
8 7 3ad2ant3 ⊢V∈Fin∧X∈V∧N∈ℤ≥3→N=N-2+2
9 8 adantl ⊢GRegUSGraphK∧G∈FriendGraph∧V∈Fin∧X∈V∧N∈ℤ≥3→N=N-2+2
10 9 oveq2d ⊢GRegUSGraphK∧G∈FriendGraph∧V∈Fin∧X∈V∧N∈ℤ≥3→XHN=XHN-2+2
11 10 fveq2d ⊢GRegUSGraphK∧G∈FriendGraph∧V∈Fin∧X∈V∧N∈ℤ≥3→XHN=XHN-2+2
12 simplr ⊢GRegUSGraphK∧G∈FriendGraph∧V∈Fin∧X∈V∧N∈ℤ≥3→G∈FriendGraph
13 simpr2 ⊢GRegUSGraphK∧G∈FriendGraph∧V∈Fin∧X∈V∧N∈ℤ≥3→X∈V
14 uz3m2nn ⊢N∈ℤ≥3→N−2∈ℕ
15 14 3ad2ant3 ⊢V∈Fin∧X∈V∧N∈ℤ≥3→N−2∈ℕ
16 15 adantl ⊢GRegUSGraphK∧G∈FriendGraph∧V∈Fin∧X∈V∧N∈ℤ≥3→N−2∈ℕ
17 1 2 3 numclwwlk2lem3 ⊢G∈FriendGraph∧X∈V∧N−2∈ℕ→XQN−2=XHN-2+2
18 12 13 16 17 syl3anc ⊢GRegUSGraphK∧G∈FriendGraph∧V∈Fin∧X∈V∧N∈ℤ≥3→XQN−2=XHN-2+2
19 simpl ⊢GRegUSGraphK∧G∈FriendGraph→GRegUSGraphK
20 simp1 ⊢V∈Fin∧X∈V∧N∈ℤ≥3→V∈Fin
21 19 20 anim12i ⊢GRegUSGraphK∧G∈FriendGraph∧V∈Fin∧X∈V∧N∈ℤ≥3→GRegUSGraphK∧V∈Fin
22 14 anim2i ⊢X∈V∧N∈ℤ≥3→X∈V∧N−2∈ℕ
23 22 3adant1 ⊢V∈Fin∧X∈V∧N∈ℤ≥3→X∈V∧N−2∈ℕ
24 23 adantl ⊢GRegUSGraphK∧G∈FriendGraph∧V∈Fin∧X∈V∧N∈ℤ≥3→X∈V∧N−2∈ℕ
25 1 2 numclwwlkqhash ⊢GRegUSGraphK∧V∈Fin∧X∈V∧N−2∈ℕ→XQN−2=KN−2−XClWWalksNOn⁡GN−2
26 21 24 25 syl2anc ⊢GRegUSGraphK∧G∈FriendGraph∧V∈Fin∧X∈V∧N∈ℤ≥3→XQN−2=KN−2−XClWWalksNOn⁡GN−2
27 11 18 26 3eqtr2d ⊢GRegUSGraphK∧G∈FriendGraph∧V∈Fin∧X∈V∧N∈ℤ≥3→XHN=KN−2−XClWWalksNOn⁡GN−2