Theorem numclwwlk1 30841

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 𝐺 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 𝐹 = ∅, but (𝑋𝐶2), the set of closed walks with length 2 on 𝑋, see 2clwwlk2 30828, needs not be ∅ in this case. This is because of the special definition of 𝐹 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 30849. If the general representation of (closed) walk is used, Huneke's statement can be proven even for n = 2, see numclwlk1 30851. 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.)

Hypotheses

Ref	Expression
extwwlkfab.v	⊢ 𝑉 = (Vtx‘𝐺)
extwwlkfab.c	⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})
extwwlkfab.f	⊢ 𝐹 = (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))

Assertion

Ref	Expression
numclwwlk1	⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))) → (♯‘(𝑋𝐶𝑁)) = (𝐾 · (♯‘𝐹)))

Distinct variable groups:   𝑛,𝐺,𝑣,𝑤   𝑛,𝑁,𝑣,𝑤   𝑛,𝑉,𝑣,𝑤   𝑛,𝑋,𝑣,𝑤   𝑤,𝐹

Allowed substitution hints:   𝐶(𝑤, 𝑣, 𝑛)   𝐹(𝑣, 𝑛)   𝐾(𝑤, 𝑣, 𝑛)

Proof of Theorem numclwwlk1

Dummy variable 𝑥 is distinct from all other variables.

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2955  ∀wral 3076  {crab 3412  ∅c0 4279   class class class wbr 5103   × cxp 5653  ‘cfv 6533  (class class class)co 7413   ∈ cmpo 7415   ≈ cen 8949  Fincfn 8952  ℂcc 11122   · cmul 11129   − cmin 11465  2c2 12319  3c3 12320  ℕ₀cn0 12528  ℕ₀^*cxnn0 12601  ℤ_≥cuz 12887  ♯chash 14394  Vtxcvtx 29453  Edgcedg 29504  USGraphcusgr 29609  FinUSGraphcfusgr 29776   NeighbVtx cnbgr 29792   RegUSGraph crusgr 30016  ClWWalksNOncclwwlknon 30557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7863  df-1st 7986  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-2o 8456  df-oadd 8459  df-er 8696  df-map 8828  df-pm 8829  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-dju 9906  df-card 9944  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11467  df-neg 11468  df-nn 12258  df-2 12327  df-3 12328  df-n0 12529  df-xnn0 12602  df-z 12616  df-uz 12888  df-rp 13043  df-xadd 13164  df-fz 13562  df-fzo 13710  df-seq 14066  df-exp 14126  df-hash 14395  df-word 14579  df-lsw 14628  df-concat 14636  df-s1 14663  df-substr 14709  df-pfx 14741  df-s2 14919  df-vtx 29455  df-iedg 29456  df-edg 29505  df-uhgr 29515  df-ushgr 29516  df-upgr 29539  df-umgr 29540  df-uspgr 29610  df-usgr 29611  df-fusgr 29777  df-nbgr 29793  df-vtxdg 29926  df-rgr 30017  df-rusgr 30018  df-wwlks 30298  df-wwlksn 30299  df-clwwlk 30452  df-clwwlkn 30495  df-clwwlknon 30558

This theorem is used by:  numclwlk1lem2  30850  numclwwlk3  30865