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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
numclwlk1.c ⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) }
numclwlk1.f ⊢ 𝐹 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = ( 𝑁 − 2 ) ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) }
Assertion numclwlk1 ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ) → ( ♯ ‘ 𝐶 ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 numclwlk1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 numclwlk1.c ⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = 𝑁 ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ∧ ( ( 2nd ‘ 𝑤 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) }
3 numclwlk1.f ⊢ 𝐹 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = ( 𝑁 − 2 ) ∧ ( ( 2nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) }
4 uzp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 = 2 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) ) )
5 1 2 3 numclwlk1lem1 ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 2 ) ) → ( ♯ ‘ 𝐶 ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) )
6 5 expcom ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 = 2 ) → ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( ♯ ‘ 𝐶 ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) ) )
7 6 expcom ⊢ ( 𝑁 = 2 → ( 𝑋 ∈ 𝑉 → ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( ♯ ‘ 𝐶 ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) ) ) )
8 1 2 3 numclwlk1lem2 ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ♯ ‘ 𝐶 ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) )
9 8 expcom ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( ♯ ‘ 𝐶 ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) ) )
10 9 expcom ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑋 ∈ 𝑉 → ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( ♯ ‘ 𝐶 ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) ) ) )
11 2p1e3 ⊢ ( 2 + 1 ) = 3
12 11 fveq2i ⊢ ( ℤ≥ ‘ ( 2 + 1 ) ) = ( ℤ≥ ‘ 3 )
13 10 12 eleq2s ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) → ( 𝑋 ∈ 𝑉 → ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( ♯ ‘ 𝐶 ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) ) ) )
14 7 13 jaoi ⊢ ( ( 𝑁 = 2 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 2 + 1 ) ) ) → ( 𝑋 ∈ 𝑉 → ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( ♯ ‘ 𝐶 ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) ) ) )
15 4 14 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑋 ∈ 𝑉 → ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( ♯ ‘ 𝐶 ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) ) ) )
16 15 impcom ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( ♯ ‘ 𝐶 ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) ) )
17 16 impcom ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ) → ( ♯ ‘ 𝐶 ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) )