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 ∈ n WWalksN G | w ⁡ 0 = v ∧ lastS ⁡ w ≠ v
numclwwlk.h ⊢ H = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 ≠ v
Assertion numclwwlk2 ⊢ G RegUSGraph K ∧ G ∈ FriendGraph ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → X H N = K N − 2 − X ClWWalksNOn ⁡ G N − 2

Proof

Step Hyp Ref Expression
1 numclwwlk.v ⊢ V = Vtx ⁡ G
2 numclwwlk.q ⊢ Q = v ∈ V , n ∈ ℕ ⟼ w ∈ n WWalksN G | w ⁡ 0 = v ∧ lastS ⁡ w ≠ v
3 numclwwlk.h ⊢ H = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | 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 ⊢ G RegUSGraph K ∧ G ∈ FriendGraph ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → N = N - 2 + 2
10 9 oveq2d ⊢ G RegUSGraph K ∧ G ∈ FriendGraph ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → X H N = X H N - 2 + 2
11 10 fveq2d ⊢ G RegUSGraph K ∧ G ∈ FriendGraph ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → X H N = X H N - 2 + 2
12 simplr ⊢ G RegUSGraph K ∧ G ∈ FriendGraph ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → G ∈ FriendGraph
13 simpr2 ⊢ G RegUSGraph K ∧ 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 ⊢ G RegUSGraph K ∧ G ∈ FriendGraph ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → N − 2 ∈ ℕ
17 1 2 3 numclwwlk2lem3 ⊢ G ∈ FriendGraph ∧ X ∈ V ∧ N − 2 ∈ ℕ → X Q N − 2 = X H N - 2 + 2
18 12 13 16 17 syl3anc ⊢ G RegUSGraph K ∧ G ∈ FriendGraph ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → X Q N − 2 = X H N - 2 + 2
19 simpl ⊢ G RegUSGraph K ∧ G ∈ FriendGraph → G RegUSGraph K
20 simp1 ⊢ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → V ∈ Fin
21 19 20 anim12i ⊢ G RegUSGraph K ∧ G ∈ FriendGraph ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → G RegUSGraph K ∧ 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 ⊢ G RegUSGraph K ∧ G ∈ FriendGraph ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → X ∈ V ∧ N − 2 ∈ ℕ
25 1 2 numclwwlkqhash ⊢ G RegUSGraph K ∧ V ∈ Fin ∧ X ∈ V ∧ N − 2 ∈ ℕ → X Q N − 2 = K N − 2 − X ClWWalksNOn ⁡ G N − 2
26 21 24 25 syl2anc ⊢ G RegUSGraph K ∧ G ∈ FriendGraph ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → X Q N − 2 = K N − 2 − X ClWWalksNOn ⁡ G N − 2
27 11 18 26 3eqtr2d ⊢ G RegUSGraph K ∧ G ∈ FriendGraph ∧ V ∈ Fin ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → X H N = K N − 2 − X ClWWalksNOn ⁡ G N − 2