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|1st⁡w=N∧2nd⁡w⁡0=X∧2nd⁡w⁡N−2=X
numclwlk1.f ⊢F=w∈ClWalks⁡G|1st⁡w=N−2∧2nd⁡w⁡0=X
Assertion numclwlk1 ⊢V∈Fin∧GRegUSGraphK∧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|1st⁡w=N∧2nd⁡w⁡0=X∧2nd⁡w⁡N−2=X
3 numclwlk1.f ⊢F=w∈ClWalks⁡G|1st⁡w=N−2∧2nd⁡w⁡0=X
4 uzp1 ⊢N∈ℤ≥2→N=2∨N∈ℤ≥2+1
5 1 2 3 numclwlk1lem1 ⊢V∈Fin∧GRegUSGraphK∧X∈V∧N=2→C=K⁢F
6 5 expcom ⊢X∈V∧N=2→V∈Fin∧GRegUSGraphK→C=K⁢F
7 6 expcom ⊢N=2→X∈V→V∈Fin∧GRegUSGraphK→C=K⁢F
8 1 2 3 numclwlk1lem2 ⊢V∈Fin∧GRegUSGraphK∧X∈V∧N∈ℤ≥3→C=K⁢F
9 8 expcom ⊢X∈V∧N∈ℤ≥3→V∈Fin∧GRegUSGraphK→C=K⁢F
10 9 expcom ⊢N∈ℤ≥3→X∈V→V∈Fin∧GRegUSGraphK→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∧GRegUSGraphK→C=K⁢F
14 7 13 jaoi ⊢N=2∨N∈ℤ≥2+1→X∈V→V∈Fin∧GRegUSGraphK→C=K⁢F
15 4 14 syl ⊢N∈ℤ≥2→X∈V→V∈Fin∧GRegUSGraphK→C=K⁢F
16 15 impcom ⊢X∈V∧N∈ℤ≥2→V∈Fin∧GRegUSGraphK→C=K⁢F
17 16 impcom ⊢V∈Fin∧GRegUSGraphK∧X∈V∧N∈ℤ≥2→C=K⁢F