rusgrnumwwlks - Metamath Proof Explorer

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

Theorem rusgrnumwwlks 28347

Description: Induction step for rusgrnumwwlk 28348. (Contributed by Alexander van der Vekens, 24-Aug-2018.) (Revised by AV, 7-May-2021.) (Proof shortened by AV, 27-May-2022.)

**Hypotheses**
Ref	Expression
rusgrnumwwlk.v	⊢ 𝑉 = (Vtx‘𝐺)
rusgrnumwwlk.l	⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ₀ ↦ (♯‘{𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑣}))

**Assertion**
Ref	Expression
rusgrnumwwlks	⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → ((𝑃𝐿𝑁) = (𝐾↑𝑁) → (𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1))))

Distinct variable groups: 𝑛,𝐺,𝑣,𝑤 𝑛,𝑁,𝑣,𝑤 𝑃,𝑛,𝑣,𝑤 𝑛,𝑉,𝑣,𝑤 𝑤,𝐾 Allowed substitution hints: 𝐾(𝑣,𝑛) 𝐿(𝑤,𝑣,𝑛)

Proof of Theorem rusgrnumwwlks Dummy variables 𝑖 𝑝 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr2 1194	. . 3 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑃 ∈ 𝑉)
2		simpr3 1195	. . 3 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑁 ∈ ℕ₀)
3		rusgrnumwwlk.v	. . . . 5 ⊢ 𝑉 = (Vtx‘𝐺)
4		rusgrnumwwlk.l	. . . . 5 ⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ₀ ↦ (♯‘{𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑣}))
5	3, 4	rusgrnumwwlklem 28343	. . . 4 ⊢ ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (𝑃𝐿𝑁) = (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}))
6	5	eqeq1d 2740	. . 3 ⊢ ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → ((𝑃𝐿𝑁) = (𝐾↑𝑁) ↔ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)))
7	1, 2, 6	syl2anc 584	. 2 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → ((𝑃𝐿𝑁) = (𝐾↑𝑁) ↔ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)))
8		eqid 2738	. . . . . . . . . . . . 13 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
9	8	wwlksnredwwlkn0 28269	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺)) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))))
10	9	ex 413	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → (𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
11	10	3ad2ant3 1134	. . . . . . . . . 10 ⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
12	11	adantl 482	. . . . . . . . 9 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
13	12	imp 407	. . . . . . . 8 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ 𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺)) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))))
14	13	rabbidva 3410	. . . . . . 7 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
15	14	adantr 481	. . . . . 6 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
16	15	fveq2d 6770	. . . . 5 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
17		simp2 1136	. . . . . . . . . . . . 13 ⊢ (((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) → (𝑦‘0) = 𝑃)
18	17	pm4.71ri 561	. . . . . . . . . . . 12 ⊢ (((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) ↔ ((𝑦‘0) = 𝑃 ∧ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))))
19	18	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ 𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺)) ∧ 𝑦 ∈ (𝑁 WWalksN 𝐺)) → (((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) ↔ ((𝑦‘0) = 𝑃 ∧ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
20	19	rexbidva 3223	. . . . . . . . . 10 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ 𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺)) → (∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑦‘0) = 𝑃 ∧ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
21		fveq1 6765	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑥‘0) = (𝑦‘0))
22	21	eqeq1d 2740	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑥‘0) = 𝑃 ↔ (𝑦‘0) = 𝑃))
23	22	rexrab 3632	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑦‘0) = 𝑃 ∧ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))))
24	20, 23	bitr4di 289	. . . . . . . . 9 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ 𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺)) → (∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) ↔ ∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))))
25	24	rabbidva 3410	. . . . . . . 8 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
26	25	adantr 481	. . . . . . 7 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
27	26	fveq2d 6770	. . . . . 6 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
28		simplr1 1214	. . . . . . 7 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → 𝑉 ∈ Fin)
29	3	eleq1i 2829	. . . . . . . 8 ⊢ (𝑉 ∈ Fin ↔ (Vtx‘𝐺) ∈ Fin)
30	29	biimpi 215	. . . . . . 7 ⊢ (𝑉 ∈ Fin → (Vtx‘𝐺) ∈ Fin)
31		eqid 2738	. . . . . . . 8 ⊢ ((𝑁 + 1) WWalksN 𝐺) = ((𝑁 + 1) WWalksN 𝐺)
32		eqid 2738	. . . . . . . 8 ⊢ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} = {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃}
33	31, 8, 32	hashwwlksnext 28287	. . . . . . 7 ⊢ ((Vtx‘𝐺) ∈ Fin → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
34	28, 30, 33	3syl 18	. . . . . 6 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
35		fveq1 6765	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (𝑥‘0) = (𝑤‘0))
36	35	eqeq1d 2740	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → ((𝑥‘0) = 𝑃 ↔ (𝑤‘0) = 𝑃))
37	36	cbvrabv 3423	. . . . . . . 8 ⊢ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}
38	37	sumeq1i 15420	. . . . . . 7 ⊢ Σ𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
39	38	a1i 11	. . . . . 6 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → Σ𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
40	27, 34, 39	3eqtrd 2782	. . . . 5 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
41		rusgrnumwwlkslem 28342	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
42	41	eqcomd 2744	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
43	42	fveq2d 6770	. . . . . . . . 9 ⊢ (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
44	43	adantl 482	. . . . . . . 8 ⊢ ((((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
45		elrabi 3617	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → 𝑦 ∈ (𝑁 WWalksN 𝐺))
46	45	adantl 482	. . . . . . . . 9 ⊢ ((((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → 𝑦 ∈ (𝑁 WWalksN 𝐺))
47	3, 8	wwlksnexthasheq 28276	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝑁 WWalksN 𝐺) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (♯‘{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}))
48	46, 47	syl 17	. . . . . . . 8 ⊢ ((((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (♯‘{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}))
49	3	rusgrpropadjvtx 27962	. . . . . . . . . 10 ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ₀^* ∧ ∀𝑝 ∈ 𝑉 (♯‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))
50		fveq1 6765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑦 → (𝑤‘0) = (𝑦‘0))
51	50	eqeq1d 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑦 → ((𝑤‘0) = 𝑃 ↔ (𝑦‘0) = 𝑃))
52	51	elrab 3623	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ↔ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑦‘0) = 𝑃))
53	3, 8	wwlknp 28216	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝑁 WWalksN 𝐺) → (𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
54	53	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑦‘0) = 𝑃) → (𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
55		simpll 764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑦 ∈ Word 𝑉)
56		nn0p1gt0 12272	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ₀ → 0 < (𝑁 + 1))
57	56	3ad2ant3 1134	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → 0 < (𝑁 + 1))
58	57	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 0 < (𝑁 + 1))
59		breq2 5077	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((♯‘𝑦) = (𝑁 + 1) → (0 < (♯‘𝑦) ↔ 0 < (𝑁 + 1)))
60	59	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (0 < (♯‘𝑦) ↔ 0 < (𝑁 + 1)))
61	58, 60	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 0 < (♯‘𝑦))
62		hashle00 14125	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ Word 𝑉 → ((♯‘𝑦) ≤ 0 ↔ 𝑦 = ∅))
63		lencl 14246	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ Word 𝑉 → (♯‘𝑦) ∈ ℕ₀)
64	63	nn0red 12304	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ Word 𝑉 → (♯‘𝑦) ∈ ℝ)
65		0re 10987	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ∈ ℝ
66		lenlt 11063	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((♯‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → ((♯‘𝑦) ≤ 0 ↔ ¬ 0 < (♯‘𝑦)))
67	66	bicomd 222	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → (¬ 0 < (♯‘𝑦) ↔ (♯‘𝑦) ≤ 0))
68	64, 65, 67	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ Word 𝑉 → (¬ 0 < (♯‘𝑦) ↔ (♯‘𝑦) ≤ 0))
69		nne 2947	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ 𝑦 ≠ ∅ ↔ 𝑦 = ∅)
70	69	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ Word 𝑉 → (¬ 𝑦 ≠ ∅ ↔ 𝑦 = ∅))
71	62, 68, 70	3bitr4rd 312	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ Word 𝑉 → (¬ 𝑦 ≠ ∅ ↔ ¬ 0 < (♯‘𝑦)))
72	71	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (¬ 𝑦 ≠ ∅ ↔ ¬ 0 < (♯‘𝑦)))
73	72	con4bid 317	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (𝑦 ≠ ∅ ↔ 0 < (♯‘𝑦)))
74	61, 73	mpbird 256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑦 ≠ ∅)
75	55, 74	jca 512	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅))
76	75	ex 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅)))
77	76	3adant3 1131	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅)))
78	54, 77	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑦‘0) = 𝑃) → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅)))
79	52, 78	sylbi 216	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅)))
80	79	imp 407	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅))
81		lswcl 14281	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅) → (lastS‘𝑦) ∈ 𝑉)
82	80, 81	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (lastS‘𝑦) ∈ 𝑉)
83	82	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ ∀𝑝 ∈ 𝑉 (♯‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾) → (lastS‘𝑦) ∈ 𝑉)
84		preq1 4669	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = (lastS‘𝑦) → {𝑝, 𝑛} = {(lastS‘𝑦), 𝑛})
85	84	eleq1d 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = (lastS‘𝑦) → ({𝑝, 𝑛} ∈ (Edg‘𝐺) ↔ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)))
86	85	rabbidv 3411	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = (lastS‘𝑦) → {𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)} = {𝑛 ∈ 𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)})
87	86	fveqeq2d 6774	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = (lastS‘𝑦) → ((♯‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾 ↔ (♯‘{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))
88	87	rspcva 3557	. . . . . . . . . . . . . 14 ⊢ (((lastS‘𝑦) ∈ 𝑉 ∧ ∀𝑝 ∈ 𝑉 (♯‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾) → (♯‘{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾)
89	83, 88	sylancom 588	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ ∀𝑝 ∈ 𝑉 (♯‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾) → (♯‘{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾)
90	89	exp41 435	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁) → (∀𝑝 ∈ 𝑉 (♯‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾 → (♯‘{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))))
91	90	com14 96	. . . . . . . . . . 11 ⊢ (∀𝑝 ∈ 𝑉 (♯‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁) → (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → (♯‘{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))))
92	91	3ad2ant3 1134	. . . . . . . . . 10 ⊢ ((𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ₀^* ∧ ∀𝑝 ∈ 𝑉 (♯‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾) → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁) → (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → (♯‘{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))))
93	49, 92	syl 17	. . . . . . . . 9 ⊢ (𝐺 RegUSGraph 𝐾 → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁) → (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → (♯‘{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))))
94	93	imp41 426	. . . . . . . 8 ⊢ ((((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → (♯‘{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾)
95	44, 48, 94	3eqtrd 2782	. . . . . . 7 ⊢ ((((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = 𝐾)
96	95	sumeq2dv 15425	. . . . . 6 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}𝐾)
97		oveq1 7274	. . . . . . . 8 ⊢ ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) · 𝐾) = ((𝐾↑𝑁) · 𝐾))
98	97	adantl 482	. . . . . . 7 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) · 𝐾) = ((𝐾↑𝑁) · 𝐾))
99		wwlksnfi 28279	. . . . . . . . . . . 12 ⊢ ((Vtx‘𝐺) ∈ Fin → (𝑁 WWalksN 𝐺) ∈ Fin)
100	29, 99	sylbi 216	. . . . . . . . . . 11 ⊢ (𝑉 ∈ Fin → (𝑁 WWalksN 𝐺) ∈ Fin)
101	100	3ad2ant1 1132	. . . . . . . . . 10 ⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (𝑁 WWalksN 𝐺) ∈ Fin)
102	101	ad2antlr 724	. . . . . . . . 9 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (𝑁 WWalksN 𝐺) ∈ Fin)
103		rabfi 9031	. . . . . . . . 9 ⊢ ((𝑁 WWalksN 𝐺) ∈ Fin → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∈ Fin)
104	102, 103	syl 17	. . . . . . . 8 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∈ Fin)
105		rusgrusgr 27941	. . . . . . . . . . . . 13 ⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph)
106		simp1 1135	. . . . . . . . . . . . 13 ⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → 𝑉 ∈ Fin)
107	105, 106	anim12i 613	. . . . . . . . . . . 12 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin))
108	3	isfusgr 27695	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin))
109	107, 108	sylibr 233	. . . . . . . . . . 11 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝐺 ∈ FinUSGraph)
110		simpl 483	. . . . . . . . . . 11 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝐺 RegUSGraph 𝐾)
111		ne0i 4268	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ 𝑉 → 𝑉 ≠ ∅)
112	111	3ad2ant2 1133	. . . . . . . . . . . 12 ⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → 𝑉 ≠ ∅)
113	112	adantl 482	. . . . . . . . . . 11 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑉 ≠ ∅)
114	3	frusgrnn0 27948	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅) → 𝐾 ∈ ℕ₀)
115	109, 110, 113, 114	syl3anc 1370	. . . . . . . . . 10 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝐾 ∈ ℕ₀)
116	115	nn0cnd 12305	. . . . . . . . 9 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝐾 ∈ ℂ)
117	116	adantr 481	. . . . . . . 8 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → 𝐾 ∈ ℂ)
118		fsumconst 15512	. . . . . . . 8 ⊢ (({𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∈ Fin ∧ 𝐾 ∈ ℂ) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}𝐾 = ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) · 𝐾))
119	104, 117, 118	syl2anc 584	. . . . . . 7 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}𝐾 = ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) · 𝐾))
120	116, 2	expp1d 13875	. . . . . . . 8 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (𝐾↑(𝑁 + 1)) = ((𝐾↑𝑁) · 𝐾))
121	120	adantr 481	. . . . . . 7 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (𝐾↑(𝑁 + 1)) = ((𝐾↑𝑁) · 𝐾))
122	98, 119, 121	3eqtr4d 2788	. . . . . 6 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}𝐾 = (𝐾↑(𝑁 + 1)))
123	96, 122	eqtrd 2778	. . . . 5 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (𝐾↑(𝑁 + 1)))
124	16, 40, 123	3eqtrd 2782	. . . 4 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1)))
125		peano2nn0 12283	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ₀)
126	125	3ad2ant3 1134	. . . . . . 7 ⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (𝑁 + 1) ∈ ℕ₀)
127	126	adantl 482	. . . . . 6 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (𝑁 + 1) ∈ ℕ₀)
128	3, 4	rusgrnumwwlklem 28343	. . . . . . 7 ⊢ ((𝑃 ∈ 𝑉 ∧ (𝑁 + 1) ∈ ℕ₀) → (𝑃𝐿(𝑁 + 1)) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}))
129	128	eqeq1d 2740	. . . . . 6 ⊢ ((𝑃 ∈ 𝑉 ∧ (𝑁 + 1) ∈ ℕ₀) → ((𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)) ↔ (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1))))
130	1, 127, 129	syl2anc 584	. . . . 5 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → ((𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)) ↔ (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1))))
131	130	adantr 481	. . . 4 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → ((𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)) ↔ (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1))))
132	124, 131	mpbird 256	. . 3 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)))
133	132	ex 413	. 2 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁) → (𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1))))
134	7, 133	sylbid 239	1 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → ((𝑃𝐿𝑁) = (𝐾↑𝑁) → (𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3065 {crab 3068 ∅c0 4256 {cpr 4563 class class class wbr 5073 ‘cfv 6426 (class class class)co 7267 ∈ cmpo 7269 Fincfn 8720 ℂcc 10879 ℝcr 10880 0cc0 10881 1c1 10882 + caddc 10884 · cmul 10886 < clt 11019 ≤ cle 11020 ℕ₀cn0 12243 ℕ₀^*cxnn0 12315 ..^cfzo 13392 ↑cexp 13792 ♯chash 14054 Word cword 14227 lastSclsw 14275 prefix cpfx 14393 Σcsu 15407 Vtxcvtx 27376 Edgcedg 27427 USGraphcusgr 27529 FinUSGraphcfusgr 27693 RegUSGraph crusgr 27933 WWalksN cwwlksn 28199

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5208 ax-sep 5221 ax-nul 5228 ax-pow 5286 ax-pr 5350 ax-un 7578 ax-inf2 9386 ax-cnex 10937 ax-resscn 10938 ax-1cn 10939 ax-icn 10940 ax-addcl 10941 ax-addrcl 10942 ax-mulcl 10943 ax-mulrcl 10944 ax-mulcom 10945 ax-addass 10946 ax-mulass 10947 ax-distr 10948 ax-i2m1 10949 ax-1ne0 10950 ax-1rid 10951 ax-rnegex 10952 ax-rrecex 10953 ax-cnre 10954 ax-pre-lttri 10955 ax-pre-lttrn 10956 ax-pre-ltadd 10957 ax-pre-mulgt0 10958 ax-pre-sup 10959

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rmo 3072 df-rab 3073 df-v 3431 df-sbc 3716 df-csb 3832 df-dif 3889 df-un 3891 df-in 3893 df-ss 3903 df-pss 3905 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-disj 5039 df-br 5074 df-opab 5136 df-mpt 5157 df-tr 5191 df-id 5484 df-eprel 5490 df-po 5498 df-so 5499 df-fr 5539 df-se 5540 df-we 5541 df-xp 5590 df-rel 5591 df-cnv 5592 df-co 5593 df-dm 5594 df-rn 5595 df-res 5596 df-ima 5597 df-pred 6195 df-ord 6262 df-on 6263 df-lim 6264 df-suc 6265 df-iota 6384 df-fun 6428 df-fn 6429 df-f 6430 df-f1 6431 df-fo 6432 df-f1o 6433 df-fv 6434 df-isom 6435 df-riota 7224 df-ov 7270 df-oprab 7271 df-mpo 7272 df-om 7703 df-1st 7820 df-2nd 7821 df-frecs 8084 df-wrecs 8115 df-recs 8189 df-rdg 8228 df-1o 8284 df-2o 8285 df-oadd 8288 df-er 8485 df-map 8604 df-pm 8605 df-en 8721 df-dom 8722 df-sdom 8723 df-fin 8724 df-sup 9188 df-oi 9256 df-dju 9669 df-card 9707 df-pnf 11021 df-mnf 11022 df-xr 11023 df-ltxr 11024 df-le 11025 df-sub 11217 df-neg 11218 df-div 11643 df-nn 11984 df-2 12046 df-3 12047 df-n0 12244 df-xnn0 12316 df-z 12330 df-uz 12593 df-rp 12741 df-xadd 12859 df-fz 13250 df-fzo 13393 df-seq 13732 df-exp 13793 df-hash 14055 df-word 14228 df-lsw 14276 df-concat 14284 df-s1 14311 df-substr 14364 df-pfx 14394 df-cj 14820 df-re 14821 df-im 14822 df-sqrt 14956 df-abs 14957 df-clim 15207 df-sum 15408 df-vtx 27378 df-iedg 27379 df-edg 27428 df-uhgr 27438 df-ushgr 27439 df-upgr 27462 df-umgr 27463 df-uspgr 27530 df-usgr 27531 df-fusgr 27694 df-nbgr 27710 df-vtxdg 27843 df-rgr 27934 df-rusgr 27935 df-wwlks 28203 df-wwlksn 28204

This theorem is referenced by: rusgrnumwwlk 28348

W3C validator