Metamath Proof Explorer

Theorem numclwlk1

Description: Statement 9 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 kf(n-2)". Since G is k-regular, the vertex v(n-2) = v has k neighbors v(n-1), so there are k walks from v(n-2) = v to v(n) = v (via each of v's neighbors) completing each of the f(n-2) walks from v=v(0) to v(n-2)=v. This theorem holds even for k=0. (Contributed by AV, 23-May-2022)

Ref Expression
Hypotheses numclwlk1.v ⊢ V = Vtx ⁡ G
numclwlk1.c ⊢ C = w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ∧ 2 nd ⁡ w ⁡ N − 2 = X
numclwlk1.f ⊢ F = w ∈ ClWalks ⁡ G | 1 st ⁡ w = N − 2 ∧ 2 nd ⁡ w ⁡ 0 = X
Assertion numclwlk1 ⊢ V ∈ Fin ∧ G RegUSGraph K ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → C = K ⁢ F

Proof

Step Hyp Ref Expression
1 numclwlk1.v ⊢ V = Vtx ⁡ G
2 numclwlk1.c ⊢ C = w ∈ ClWalks ⁡ G | 1 st ⁡ w = N ∧ 2 nd ⁡ w ⁡ 0 = X ∧ 2 nd ⁡ w ⁡ N − 2 = X
3 numclwlk1.f ⊢ F = w ∈ ClWalks ⁡ G | 1 st ⁡ w = N − 2 ∧ 2 nd ⁡ w ⁡ 0 = X
4 uzp1 ⊢ N ∈ ℤ ≥ 2 → N = 2 ∨ N ∈ ℤ ≥ 2 + 1
5 1 2 3 numclwlk1lem1 ⊢ V ∈ Fin ∧ G RegUSGraph K ∧ X ∈ V ∧ N = 2 → C = K ⁢ F
6 5 expcom ⊢ X ∈ V ∧ N = 2 → V ∈ Fin ∧ G RegUSGraph K → C = K ⁢ F
7 6 expcom ⊢ N = 2 → X ∈ V → V ∈ Fin ∧ G RegUSGraph K → C = K ⁢ F
8 1 2 3 numclwlk1lem2 ⊢ V ∈ Fin ∧ G RegUSGraph K ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → C = K ⁢ F
9 8 expcom ⊢ X ∈ V ∧ N ∈ ℤ ≥ 3 → V ∈ Fin ∧ G RegUSGraph K → C = K ⁢ F
10 9 expcom ⊢ N ∈ ℤ ≥ 3 → X ∈ V → V ∈ Fin ∧ G RegUSGraph K → C = K ⁢ F
11 2p1e3 ⊢ 2 + 1 = 3
12 11 fveq2i ⊢ ℤ ≥ 2 + 1 = ℤ ≥ 3
13 10 12 eleq2s ⊢ N ∈ ℤ ≥ 2 + 1 → X ∈ V → V ∈ Fin ∧ G RegUSGraph K → C = K ⁢ F
14 7 13 jaoi ⊢ N = 2 ∨ N ∈ ℤ ≥ 2 + 1 → X ∈ V → V ∈ Fin ∧ G RegUSGraph K → C = K ⁢ F
15 4 14 syl ⊢ N ∈ ℤ ≥ 2 → X ∈ V → V ∈ Fin ∧ G RegUSGraph K → C = K ⁢ F
16 15 impcom ⊢ X ∈ V ∧ N ∈ ℤ ≥ 2 → V ∈ Fin ∧ G RegUSGraph K → C = K ⁢ F
17 16 impcom ⊢ V ∈ Fin ∧ G RegUSGraph K ∧ X ∈ V ∧ N ∈ ℤ ≥ 2 → C = K ⁢ F