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 29954

Description: Induction step for rusgrnumwwlk 29955. (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 1196	. . 3 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑃 ∈ 𝑉)
2		simpr3 1197	. . 3 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑁 ∈ ℕ₀)
3		rusgrnumwwlk.v	. . . . 5 ⊢ 𝑉 = (Vtx‘𝐺)
4		rusgrnumwwlk.l	. . . . 5 ⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ₀ ↦ (♯‘{𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑣}))
5	3, 4	rusgrnumwwlklem 29950	. . . 4 ⊢ ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (𝑃𝐿𝑁) = (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}))
6	5	eqeq1d 2731	. . 3 ⊢ ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → ((𝑃𝐿𝑁) = (𝐾↑𝑁) ↔ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)))
7	1, 2, 6	syl2anc 584	. 2 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → ((𝑃𝐿𝑁) = (𝐾↑𝑁) ↔ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)))
8		eqid 2729	. . . . . . . . . . . . 13 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
9	8	wwlksnredwwlkn0 29876	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺)) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))))
10	9	ex 412	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → (𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
11	10	3ad2ant3 1135	. . . . . . . . . 10 ⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
12	11	adantl 481	. . . . . . . . 9 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
13	12	imp 406	. . . . . . . 8 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ 𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺)) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))))
14	13	rabbidva 3409	. . . . . . 7 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
15	14	adantr 480	. . . . . 6 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
16	15	fveq2d 6844	. . . . 5 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
17		simp2 1137	. . . . . . . . . . . . 13 ⊢ (((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) → (𝑦‘0) = 𝑃)
18	17	pm4.71ri 560	. . . . . . . . . . . 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 3155	. . . . . . . . . 10 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ 𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺)) → (∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑦‘0) = 𝑃 ∧ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
21		fveq1 6839	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑥‘0) = (𝑦‘0))
22	21	eqeq1d 2731	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑥‘0) = 𝑃 ↔ (𝑦‘0) = 𝑃))
23	22	rexrab 3664	. . . . . . . . . 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 3409	. . . . . . . 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 480	. . . . . . 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 6844	. . . . . 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 1216	. . . . . . 7 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → 𝑉 ∈ Fin)
29	3	eleq1i 2819	. . . . . . . 8 ⊢ (𝑉 ∈ Fin ↔ (Vtx‘𝐺) ∈ Fin)
30	29	biimpi 216	. . . . . . 7 ⊢ (𝑉 ∈ Fin → (Vtx‘𝐺) ∈ Fin)
31		eqid 2729	. . . . . . . 8 ⊢ ((𝑁 + 1) WWalksN 𝐺) = ((𝑁 + 1) WWalksN 𝐺)
32		eqid 2729	. . . . . . . 8 ⊢ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} = {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃}
33	31, 8, 32	hashwwlksnext 29894	. . . . . . 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 6839	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (𝑥‘0) = (𝑤‘0))
36	35	eqeq1d 2731	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → ((𝑥‘0) = 𝑃 ↔ (𝑤‘0) = 𝑃))
37	36	cbvrabv 3413	. . . . . . . 8 ⊢ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}
38	37	sumeq1i 15639	. . . . . . 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 2768	. . . . 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 29949	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
42	41	eqcomd 2735	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
43	42	fveq2d 6844	. . . . . . . . 9 ⊢ (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
44	43	adantl 481	. . . . . . . 8 ⊢ ((((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
45		elrabi 3651	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → 𝑦 ∈ (𝑁 WWalksN 𝐺))
46	45	adantl 481	. . . . . . . . 9 ⊢ ((((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → 𝑦 ∈ (𝑁 WWalksN 𝐺))
47	3, 8	wwlksnexthasheq 29883	. . . . . . . . 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 29566	. . . . . . . . . 10 ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ₀^* ∧ ∀𝑝 ∈ 𝑉 (♯‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))
50		fveq1 6839	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑦 → (𝑤‘0) = (𝑦‘0))
51	50	eqeq1d 2731	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑦 → ((𝑤‘0) = 𝑃 ↔ (𝑦‘0) = 𝑃))
52	51	elrab 3656	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ↔ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑦‘0) = 𝑃))
53	3, 8	wwlknp 29823	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝑁 WWalksN 𝐺) → (𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
54	53	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑦‘0) = 𝑃) → (𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
55		simpll 766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑦 ∈ Word 𝑉)
56		nn0p1gt0 12447	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ₀ → 0 < (𝑁 + 1))
57	56	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → 0 < (𝑁 + 1))
58	57	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 0 < (𝑁 + 1))
59		breq2 5106	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((♯‘𝑦) = (𝑁 + 1) → (0 < (♯‘𝑦) ↔ 0 < (𝑁 + 1)))
60	59	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (0 < (♯‘𝑦) ↔ 0 < (𝑁 + 1)))
61	58, 60	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 0 < (♯‘𝑦))
62		hashle00 14341	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ Word 𝑉 → ((♯‘𝑦) ≤ 0 ↔ 𝑦 = ∅))
63		lencl 14474	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ Word 𝑉 → (♯‘𝑦) ∈ ℕ₀)
64	63	nn0red 12480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ Word 𝑉 → (♯‘𝑦) ∈ ℝ)
65		0re 11152	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ∈ ℝ
66		lenlt 11228	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((♯‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → ((♯‘𝑦) ≤ 0 ↔ ¬ 0 < (♯‘𝑦)))
67	66	bicomd 223	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → (¬ 0 < (♯‘𝑦) ↔ (♯‘𝑦) ≤ 0))
68	64, 65, 67	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ Word 𝑉 → (¬ 0 < (♯‘𝑦) ↔ (♯‘𝑦) ≤ 0))
69		nne 2929	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ 𝑦 ≠ ∅ ↔ 𝑦 = ∅)
70	69	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ Word 𝑉 → (¬ 𝑦 ≠ ∅ ↔ 𝑦 = ∅))
71	62, 68, 70	3bitr4rd 312	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ Word 𝑉 → (¬ 𝑦 ≠ ∅ ↔ ¬ 0 < (♯‘𝑦)))
72	71	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (¬ 𝑦 ≠ ∅ ↔ ¬ 0 < (♯‘𝑦)))
73	72	con4bid 317	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (𝑦 ≠ ∅ ↔ 0 < (♯‘𝑦)))
74	61, 73	mpbird 257	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑦 ≠ ∅)
75	55, 74	jca 511	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅))
76	75	ex 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅)))
77	76	3adant3 1132	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅)))
78	54, 77	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑦‘0) = 𝑃) → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅)))
79	52, 78	sylbi 217	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅)))
80	79	imp 406	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅))
81		lswcl 14509	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅) → (lastS‘𝑦) ∈ 𝑉)
82	80, 81	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (lastS‘𝑦) ∈ 𝑉)
83	82	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ ∀𝑝 ∈ 𝑉 (♯‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾) → (lastS‘𝑦) ∈ 𝑉)
84		preq1 4693	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = (lastS‘𝑦) → {𝑝, 𝑛} = {(lastS‘𝑦), 𝑛})
85	84	eleq1d 2813	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = (lastS‘𝑦) → ({𝑝, 𝑛} ∈ (Edg‘𝐺) ↔ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)))
86	85	rabbidv 3410	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = (lastS‘𝑦) → {𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)} = {𝑛 ∈ 𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)})
87	86	fveqeq2d 6848	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = (lastS‘𝑦) → ((♯‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾 ↔ (♯‘{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))
88	87	rspcva 3583	. . . . . . . . . . . . . 14 ⊢ (((lastS‘𝑦) ∈ 𝑉 ∧ ∀𝑝 ∈ 𝑉 (♯‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾) → (♯‘{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾)
89	83, 88	sylancom 588	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ ∀𝑝 ∈ 𝑉 (♯‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾) → (♯‘{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾)
90	89	exp41 434	. . . . . . . . . . . 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 1135	. . . . . . . . . 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 425	. . . . . . . 8 ⊢ ((((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → (♯‘{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾)
95	44, 48, 94	3eqtrd 2768	. . . . . . 7 ⊢ ((((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = 𝐾)
96	95	sumeq2dv 15644	. . . . . 6 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}𝐾)
97		oveq1 7376	. . . . . . . 8 ⊢ ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) · 𝐾) = ((𝐾↑𝑁) · 𝐾))
98	97	adantl 481	. . . . . . 7 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) · 𝐾) = ((𝐾↑𝑁) · 𝐾))
99		wwlksnfi 29886	. . . . . . . . . . . 12 ⊢ ((Vtx‘𝐺) ∈ Fin → (𝑁 WWalksN 𝐺) ∈ Fin)
100	29, 99	sylbi 217	. . . . . . . . . . 11 ⊢ (𝑉 ∈ Fin → (𝑁 WWalksN 𝐺) ∈ Fin)
101	100	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (𝑁 WWalksN 𝐺) ∈ Fin)
102	101	ad2antlr 727	. . . . . . . . 9 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (𝑁 WWalksN 𝐺) ∈ Fin)
103		rabfi 9190	. . . . . . . . 9 ⊢ ((𝑁 WWalksN 𝐺) ∈ Fin → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∈ Fin)
104	102, 103	syl 17	. . . . . . . 8 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∈ Fin)
105		rusgrusgr 29545	. . . . . . . . . . . . 13 ⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph)
106		simp1 1136	. . . . . . . . . . . . 13 ⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → 𝑉 ∈ Fin)
107	105, 106	anim12i 613	. . . . . . . . . . . 12 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin))
108	3	isfusgr 29298	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin))
109	107, 108	sylibr 234	. . . . . . . . . . 11 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝐺 ∈ FinUSGraph)
110		simpl 482	. . . . . . . . . . 11 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝐺 RegUSGraph 𝐾)
111		ne0i 4300	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ 𝑉 → 𝑉 ≠ ∅)
112	111	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → 𝑉 ≠ ∅)
113	112	adantl 481	. . . . . . . . . . 11 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑉 ≠ ∅)
114	3	frusgrnn0 29552	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅) → 𝐾 ∈ ℕ₀)
115	109, 110, 113, 114	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝐾 ∈ ℕ₀)
116	115	nn0cnd 12481	. . . . . . . . 9 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝐾 ∈ ℂ)
117	116	adantr 480	. . . . . . . 8 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → 𝐾 ∈ ℂ)
118		fsumconst 15732	. . . . . . . 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 14088	. . . . . . . 8 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (𝐾↑(𝑁 + 1)) = ((𝐾↑𝑁) · 𝐾))
121	120	adantr 480	. . . . . . 7 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (𝐾↑(𝑁 + 1)) = ((𝐾↑𝑁) · 𝐾))
122	98, 119, 121	3eqtr4d 2774	. . . . . 6 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}𝐾 = (𝐾↑(𝑁 + 1)))
123	96, 122	eqtrd 2764	. . . . 5 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (𝐾↑(𝑁 + 1)))
124	16, 40, 123	3eqtrd 2768	. . . 4 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1)))
125		peano2nn0 12458	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ₀)
126	125	3ad2ant3 1135	. . . . . . 7 ⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (𝑁 + 1) ∈ ℕ₀)
127	126	adantl 481	. . . . . 6 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (𝑁 + 1) ∈ ℕ₀)
128	3, 4	rusgrnumwwlklem 29950	. . . . . . 7 ⊢ ((𝑃 ∈ 𝑉 ∧ (𝑁 + 1) ∈ ℕ₀) → (𝑃𝐿(𝑁 + 1)) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}))
129	128	eqeq1d 2731	. . . . . 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 480	. . . 4 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → ((𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)) ↔ (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1))))
132	124, 131	mpbird 257	. . 3 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)))
133	132	ex 412	. 2 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁) → (𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1))))
134	7, 133	sylbid 240	1 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → ((𝑃𝐿𝑁) = (𝐾↑𝑁) → (𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 {crab 3402 ∅c0 4292 {cpr 4587 class class class wbr 5102 ‘cfv 6499 (class class class)co 7369 ∈ cmpo 7371 Fincfn 8895 ℂcc 11042 ℝcr 11043 0cc0 11044 1c1 11045 + caddc 11047 · cmul 11049 < clt 11184 ≤ cle 11185 ℕ₀cn0 12418 ℕ₀^*cxnn0 12491 ..^cfzo 13591 ↑cexp 14002 ♯chash 14271 Word cword 14454 lastSclsw 14503 prefix cpfx 14611 Σcsu 15628 Vtxcvtx 28976 Edgcedg 29027 USGraphcusgr 29129 FinUSGraphcfusgr 29296 RegUSGraph crusgr 29537 WWalksN cwwlksn 29806

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-inf2 9570 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-pre-sup 11122

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-disj 5070 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-2o 8412 df-oadd 8415 df-er 8648 df-map 8778 df-pm 8779 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-sup 9369 df-oi 9439 df-dju 9830 df-card 9868 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-3 12226 df-n0 12419 df-xnn0 12492 df-z 12506 df-uz 12770 df-rp 12928 df-xadd 13049 df-fz 13445 df-fzo 13592 df-seq 13943 df-exp 14003 df-hash 14272 df-word 14455 df-lsw 14504 df-concat 14512 df-s1 14537 df-substr 14582 df-pfx 14612 df-cj 15041 df-re 15042 df-im 15043 df-sqrt 15177 df-abs 15178 df-clim 15430 df-sum 15629 df-vtx 28978 df-iedg 28979 df-edg 29028 df-uhgr 29038 df-ushgr 29039 df-upgr 29062 df-umgr 29063 df-uspgr 29130 df-usgr 29131 df-fusgr 29297 df-nbgr 29313 df-vtxdg 29447 df-rgr 29538 df-rusgr 29539 df-wwlks 29810 df-wwlksn 29811

This theorem is referenced by: rusgrnumwwlk 29955

W3C validator