rusgrnumwlkg - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > rusgrnumwlkg		Structured version Visualization version GIF version

Theorem rusgrnumwlkg 26944

Description: In a k-regular graph, the number of walks of a fixed length n from a fixed vertex is k to the power of n. This theorem corresponds to statement 11 in [Huneke] p. 2: "The total number of walks v(0) v(1) ... v(n-2) from a fixed vertex v = v(0) is k^(n-2) as G is k-regular.". This theorem even holds for n=0: then the walk consists of only one vertex v(0), so the number of walks of length n=0 starting with v=v(0) is 1=k^0. (Contributed by Alexander van der Vekens, 24-Aug-2018.) (Revised by AV, 7-May-2021.)

**Hypothesis**
Ref	Expression
rusgrnumwwlkg.v	⊢ 𝑉 = (Vtx‘𝐺)

**Assertion**
Ref	Expression
rusgrnumwlkg	⊢ ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (#‘{𝑤 ∈ (Walks‘𝐺) ∣ ((#‘(1^st ‘𝑤)) = 𝑁 ∧ ((2^nd ‘𝑤)‘0) = 𝑃)}) = (𝐾↑𝑁))

Distinct variable groups: 𝑤,𝐺 𝑤,𝐾 𝑤,𝑁 𝑤,𝑃 𝑤,𝑉

Proof of Theorem rusgrnumwlkg Dummy variables 𝑓 𝑔 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ovex 6718	. . . 4 ⊢ (𝑁 WWalksN 𝐺) ∈ V
2	1	rabex 4845	. . 3 ⊢ {𝑝 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑝‘0) = 𝑃} ∈ V
3		rusgrusgr 26516	. . . . . 6 ⊢ (𝐺RegUSGraph𝐾 → 𝐺 ∈ USGraph)
4	3	adantr 480	. . . . 5 ⊢ ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝐺 ∈ USGraph)
5		simpr3 1089	. . . . 5 ⊢ ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑁 ∈ ℕ₀)
6		rusgrnumwwlkg.v	. . . . . . . . 9 ⊢ 𝑉 = (Vtx‘𝐺)
7	6	eleq2i 2722	. . . . . . . 8 ⊢ (𝑃 ∈ 𝑉 ↔ 𝑃 ∈ (Vtx‘𝐺))
8	7	biimpi 206	. . . . . . 7 ⊢ (𝑃 ∈ 𝑉 → 𝑃 ∈ (Vtx‘𝐺))
9	8	3ad2ant2 1103	. . . . . 6 ⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → 𝑃 ∈ (Vtx‘𝐺))
10	9	adantl 481	. . . . 5 ⊢ ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑃 ∈ (Vtx‘𝐺))
11		wlksnwwlknvbij 26871	. . . . 5 ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ₀ ∧ 𝑃 ∈ (Vtx‘𝐺)) → ∃𝑓 𝑓:{𝑤 ∈ (Walks‘𝐺) ∣ ((#‘(1^st ‘𝑤)) = 𝑁 ∧ ((2^nd ‘𝑤)‘0) = 𝑃)}–1-1-onto→{𝑝 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑝‘0) = 𝑃})
12	4, 5, 10, 11	syl3anc 1366	. . . 4 ⊢ ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → ∃𝑓 𝑓:{𝑤 ∈ (Walks‘𝐺) ∣ ((#‘(1^st ‘𝑤)) = 𝑁 ∧ ((2^nd ‘𝑤)‘0) = 𝑃)}–1-1-onto→{𝑝 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑝‘0) = 𝑃})
13		f1oexbi 7158	. . . 4 ⊢ (∃𝑔 𝑔:{𝑝 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑝‘0) = 𝑃}–1-1-onto→{𝑤 ∈ (Walks‘𝐺) ∣ ((#‘(1^st ‘𝑤)) = 𝑁 ∧ ((2^nd ‘𝑤)‘0) = 𝑃)} ↔ ∃𝑓 𝑓:{𝑤 ∈ (Walks‘𝐺) ∣ ((#‘(1^st ‘𝑤)) = 𝑁 ∧ ((2^nd ‘𝑤)‘0) = 𝑃)}–1-1-onto→{𝑝 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑝‘0) = 𝑃})
14	12, 13	sylibr 224	. . 3 ⊢ ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → ∃𝑔 𝑔:{𝑝 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑝‘0) = 𝑃}–1-1-onto→{𝑤 ∈ (Walks‘𝐺) ∣ ((#‘(1^st ‘𝑤)) = 𝑁 ∧ ((2^nd ‘𝑤)‘0) = 𝑃)})
15		hasheqf1oi 13180	. . 3 ⊢ ({𝑝 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑝‘0) = 𝑃} ∈ V → (∃𝑔 𝑔:{𝑝 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑝‘0) = 𝑃}–1-1-onto→{𝑤 ∈ (Walks‘𝐺) ∣ ((#‘(1^st ‘𝑤)) = 𝑁 ∧ ((2^nd ‘𝑤)‘0) = 𝑃)} → (#‘{𝑝 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑝‘0) = 𝑃}) = (#‘{𝑤 ∈ (Walks‘𝐺) ∣ ((#‘(1^st ‘𝑤)) = 𝑁 ∧ ((2^nd ‘𝑤)‘0) = 𝑃)})))
16	2, 14, 15	mpsyl 68	. 2 ⊢ ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (#‘{𝑝 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑝‘0) = 𝑃}) = (#‘{𝑤 ∈ (Walks‘𝐺) ∣ ((#‘(1^st ‘𝑤)) = 𝑁 ∧ ((2^nd ‘𝑤)‘0) = 𝑃)}))
17	6	rusgrnumwwlkg 26943	. 2 ⊢ ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (#‘{𝑝 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑝‘0) = 𝑃}) = (𝐾↑𝑁))
18	16, 17	eqtr3d 2687	1 ⊢ ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (#‘{𝑤 ∈ (Walks‘𝐺) ∣ ((#‘(1^st ‘𝑤)) = 𝑁 ∧ ((2^nd ‘𝑤)‘0) = 𝑃)}) = (𝐾↑𝑁))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1054 = wceq 1523 ∃wex 1744 ∈ wcel 2030 {crab 2945 Vcvv 3231 class class class wbr 4685 –1-1-onto→wf1o 5925 ‘cfv 5926 (class class class)co 6690 1^st c1st 7208 2^nd c2nd 7209 Fincfn 7997 0cc0 9974 ℕ₀cn0 11330 ↑cexp 12900 #chash 13157 Vtxcvtx 25919 USGraphcusgr 26089 RegUSGraphcrusgr 26508 Walkscwlks 26548 WWalksN cwwlksn 26774

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-8 2032 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-rep 4804 ax-sep 4814 ax-nul 4822 ax-pow 4873 ax-pr 4936 ax-un 6991 ax-inf2 8576 ax-cnex 10030 ax-resscn 10031 ax-1cn 10032 ax-icn 10033 ax-addcl 10034 ax-addrcl 10035 ax-mulcl 10036 ax-mulrcl 10037 ax-mulcom 10038 ax-addass 10039 ax-mulass 10040 ax-distr 10041 ax-i2m1 10042 ax-1ne0 10043 ax-1rid 10044 ax-rnegex 10045 ax-rrecex 10046 ax-cnre 10047 ax-pre-lttri 10048 ax-pre-lttrn 10049 ax-pre-ltadd 10050 ax-pre-mulgt0 10051 ax-pre-sup 10052

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-ifp 1033 df-3or 1055 df-3an 1056 df-tru 1526 df-fal 1529 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ne 2824 df-nel 2927 df-ral 2946 df-rex 2947 df-reu 2948 df-rmo 2949 df-rab 2950 df-v 3233 df-sbc 3469 df-csb 3567 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-pss 3623 df-nul 3949 df-if 4120 df-pw 4193 df-sn 4211 df-pr 4213 df-tp 4215 df-op 4217 df-uni 4469 df-int 4508 df-iun 4554 df-disj 4653 df-br 4686 df-opab 4746 df-mpt 4763 df-tr 4786 df-id 5053 df-eprel 5058 df-po 5064 df-so 5065 df-fr 5102 df-se 5103 df-we 5104 df-xp 5149 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-rn 5154 df-res 5155 df-ima 5156 df-pred 5718 df-ord 5764 df-on 5765 df-lim 5766 df-suc 5767 df-iota 5889 df-fun 5928 df-fn 5929 df-f 5930 df-f1 5931 df-fo 5932 df-f1o 5933 df-fv 5934 df-isom 5935 df-riota 6651 df-ov 6693 df-oprab 6694 df-mpt2 6695 df-om 7108 df-1st 7210 df-2nd 7211 df-wrecs 7452 df-recs 7513 df-rdg 7551 df-1o 7605 df-2o 7606 df-oadd 7609 df-er 7787 df-map 7901 df-pm 7902 df-en 7998 df-dom 7999 df-sdom 8000 df-fin 8001 df-sup 8389 df-oi 8456 df-card 8803 df-cda 9028 df-pnf 10114 df-mnf 10115 df-xr 10116 df-ltxr 10117 df-le 10118 df-sub 10306 df-neg 10307 df-div 10723 df-nn 11059 df-2 11117 df-3 11118 df-n0 11331 df-xnn0 11402 df-z 11416 df-uz 11726 df-rp 11871 df-xadd 11985 df-fz 12365 df-fzo 12505 df-seq 12842 df-exp 12901 df-hash 13158 df-word 13331 df-lsw 13332 df-concat 13333 df-s1 13334 df-substr 13335 df-cj 13883 df-re 13884 df-im 13885 df-sqrt 14019 df-abs 14020 df-clim 14263 df-sum 14461 df-vtx 25921 df-iedg 25922 df-edg 25985 df-uhgr 25998 df-ushgr 25999 df-upgr 26022 df-umgr 26023 df-uspgr 26090 df-usgr 26091 df-fusgr 26254 df-nbgr 26270 df-vtxdg 26418 df-rgr 26509 df-rusgr 26510 df-wlks 26551 df-wwlks 26778 df-wwlksn 26779

This theorem is referenced by: (None)

W3C validator