Metamath Proof Explorer

Theorem numclwwlk1

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, but not for n=2, since F = (/) , but ( X C 2 ) , the set of closed walks with length 2 on X , see 2clwwlk2 , needs not be (/) in this case. This is because of the special definition of F and the usage of words to represent (closed) walks, and does not contradict Huneke's statement, which would read "the number of closed 2-walks v(0) v(1) v(2) from v = v(0) = v(2) ... is kf(0)", where f(0)=1 is the number of empty closed walks on v, see numclwlk1lem1 . If the general representation of (closed) walk is used, Huneke's statement can be proven even for n = 2, see numclwlk1 . This case, however, is not required to prove the friendship theorem. (Contributed by Alexander van der Vekens, 26-Sep-2018) (Revised by AV, 29-May-2021) (Revised by AV, 6-Mar-2022) (Proof shortened by AV, 31-Jul-2022)

Ref Expression
Hypotheses extwwlkfab.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
extwwlkfab.c ⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
extwwlkfab.f ⊢ 𝐹 = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
Assertion numclwwlk1 ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝑋 𝐶 𝑁 ) ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 extwwlkfab.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 extwwlkfab.c ⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
3 extwwlkfab.f ⊢ 𝐹 = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
4 rusgrusgr ⊢ ( 𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph )
5 4 ad2antlr ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝐺 ∈ USGraph )
6 simprl ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝑋 ∈ 𝑉 )
7 simprr ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
8 1 2 3 numclwwlk1lem2 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑋 𝐶 𝑁 ) ≈ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) )
9 5 6 7 8 syl3anc ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( 𝑋 𝐶 𝑁 ) ≈ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) )
10 hasheni ⊢ ( ( 𝑋 𝐶 𝑁 ) ≈ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) → ( ♯ ‘ ( 𝑋 𝐶 𝑁 ) ) = ( ♯ ‘ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) ) )
11 9 10 syl ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝑋 𝐶 𝑁 ) ) = ( ♯ ‘ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) ) )
12 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
13 12 clwwlknonfin ⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∈ Fin )
14 1 eleq1i ⊢ ( 𝑉 ∈ Fin ↔ ( Vtx ‘ 𝐺 ) ∈ Fin )
15 3 eleq1i ⊢ ( 𝐹 ∈ Fin ↔ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∈ Fin )
16 13 14 15 3imtr4i ⊢ ( 𝑉 ∈ Fin → 𝐹 ∈ Fin )
17 16 adantr ⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → 𝐹 ∈ Fin )
18 17 adantr ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝐹 ∈ Fin )
19 1 finrusgrfusgr ⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) → 𝐺 ∈ FinUSGraph )
20 19 ancoms ⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → 𝐺 ∈ FinUSGraph )
21 fusgrfis ⊢ ( 𝐺 ∈ FinUSGraph → ( Edg ‘ 𝐺 ) ∈ Fin )
22 20 21 syl ⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( Edg ‘ 𝐺 ) ∈ Fin )
23 22 adantr ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( Edg ‘ 𝐺 ) ∈ Fin )
24 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
25 1 24 nbusgrfi ⊢ ( ( 𝐺 ∈ USGraph ∧ ( Edg ‘ 𝐺 ) ∈ Fin ∧ 𝑋 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑋 ) ∈ Fin )
26 5 23 6 25 syl3anc ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( 𝐺 NeighbVtx 𝑋 ) ∈ Fin )
27 hashxp ⊢ ( ( 𝐹 ∈ Fin ∧ ( 𝐺 NeighbVtx 𝑋 ) ∈ Fin ) → ( ♯ ‘ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) ) = ( ( ♯ ‘ 𝐹 ) · ( ♯ ‘ ( 𝐺 NeighbVtx 𝑋 ) ) ) )
28 18 26 27 syl2anc ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) ) = ( ( ♯ ‘ 𝐹 ) · ( ♯ ‘ ( 𝐺 NeighbVtx 𝑋 ) ) ) )
29 1 rusgrpropnb ⊢ ( 𝐺 RegUSGraph 𝐾 → ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑥 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑥 ) ) = 𝐾 ) )
30 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐺 NeighbVtx 𝑥 ) = ( 𝐺 NeighbVtx 𝑋 ) )
31 30 fveqeq2d ⊢ ( 𝑥 = 𝑋 → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑥 ) ) = 𝐾 ↔ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑋 ) ) = 𝐾 ) )
32 31 rspccv ⊢ ( ∀ 𝑥 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑥 ) ) = 𝐾 → ( 𝑋 ∈ 𝑉 → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑋 ) ) = 𝐾 ) )
33 32 3ad2ant3 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀ 𝑥 ∈ 𝑉 ( ♯ ‘ ( 𝐺 NeighbVtx 𝑥 ) ) = 𝐾 ) → ( 𝑋 ∈ 𝑉 → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑋 ) ) = 𝐾 ) )
34 29 33 syl ⊢ ( 𝐺 RegUSGraph 𝐾 → ( 𝑋 ∈ 𝑉 → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑋 ) ) = 𝐾 ) )
35 34 adantl ⊢ ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( 𝑋 ∈ 𝑉 → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑋 ) ) = 𝐾 ) )
36 35 com12 ⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑋 ) ) = 𝐾 ) )
37 36 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑋 ) ) = 𝐾 ) )
38 37 impcom ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑋 ) ) = 𝐾 )
39 38 oveq2d ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ( ♯ ‘ 𝐹 ) · ( ♯ ‘ ( 𝐺 NeighbVtx 𝑋 ) ) ) = ( ( ♯ ‘ 𝐹 ) · 𝐾 ) )
40 hashcl ⊢ ( 𝐹 ∈ Fin → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
41 nn0cn ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℂ )
42 18 40 41 3syl ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ♯ ‘ 𝐹 ) ∈ ℂ )
43 20 adantr ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝐺 ∈ FinUSGraph )
44 simplr ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝐺 RegUSGraph 𝐾 )
45 ne0i ⊢ ( 𝑋 ∈ 𝑉 → 𝑉 ≠ ∅ )
46 45 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑉 ≠ ∅ )
47 46 adantl ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝑉 ≠ ∅ )
48 1 frusgrnn0 ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅ ) → 𝐾 ∈ ℕ0 )
49 43 44 47 48 syl3anc ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝐾 ∈ ℕ0 )
50 49 nn0cnd ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝐾 ∈ ℂ )
51 42 50 mulcomd ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ( ♯ ‘ 𝐹 ) · 𝐾 ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) )
52 39 51 eqtrd ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ( ♯ ‘ 𝐹 ) · ( ♯ ‘ ( 𝐺 NeighbVtx 𝑋 ) ) ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) )
53 11 28 52 3eqtrd ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ♯ ‘ ( 𝑋 𝐶 𝑁 ) ) = ( 𝐾 · ( ♯ ‘ 𝐹 ) ) )