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 30064

Description: Induction step for rusgrnumwwlk 30065. (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 1197	. . 3 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑃 ∈ 𝑉)
2		simpr3 1198	. . 3 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑁 ∈ ℕ₀)
3		rusgrnumwwlk.v	. . . . 5 ⊢ 𝑉 = (Vtx‘𝐺)
4		rusgrnumwwlk.l	. . . . 5 ⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ₀ ↦ (♯‘{𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑣}))
5	3, 4	rusgrnumwwlklem 30060	. . . 4 ⊢ ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (𝑃𝐿𝑁) = (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}))
6	5	eqeq1d 2739	. . 3 ⊢ ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → ((𝑃𝐿𝑁) = (𝐾↑𝑁) ↔ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)))
7	1, 2, 6	syl2anc 585	. 2 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → ((𝑃𝐿𝑁) = (𝐾↑𝑁) ↔ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)))
8		eqid 2737	. . . . . . . . . . . . 13 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
9	8	wwlksnredwwlkn0 29983	. . . . . . . . . . . 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 1136	. . . . . . . . . 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 3396	. . . . . . 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 6840	. . . . 5 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
17		simp2 1138	. . . . . . . . . . . . 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 3160	. . . . . . . . . 10 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ 𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺)) → (∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑦‘0) = 𝑃 ∧ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
21		fveq1 6835	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑥‘0) = (𝑦‘0))
22	21	eqeq1d 2739	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑥‘0) = 𝑃 ↔ (𝑦‘0) = 𝑃))
23	22	rexrab 3643	. . . . . . . . . 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 3396	. . . . . . . 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 6840	. . . . . 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 1217	. . . . . . 7 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → 𝑉 ∈ Fin)
29	3	eleq1i 2828	. . . . . . . 8 ⊢ (𝑉 ∈ Fin ↔ (Vtx‘𝐺) ∈ Fin)
30	29	biimpi 216	. . . . . . 7 ⊢ (𝑉 ∈ Fin → (Vtx‘𝐺) ∈ Fin)
31		eqid 2737	. . . . . . . 8 ⊢ ((𝑁 + 1) WWalksN 𝐺) = ((𝑁 + 1) WWalksN 𝐺)
32		eqid 2737	. . . . . . . 8 ⊢ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} = {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃}
33	31, 8, 32	hashwwlksnext 30001	. . . . . . 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 6835	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (𝑥‘0) = (𝑤‘0))
36	35	eqeq1d 2739	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → ((𝑥‘0) = 𝑃 ↔ (𝑤‘0) = 𝑃))
37	36	cbvrabv 3400	. . . . . . . 8 ⊢ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}
38	37	sumeq1i 15654	. . . . . . 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 2776	. . . . 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 30059	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
42	41	eqcomd 2743	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
43	42	fveq2d 6840	. . . . . . . . 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 3631	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → 𝑦 ∈ (𝑁 WWalksN 𝐺))
46	45	adantl 481	. . . . . . . . 9 ⊢ ((((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → 𝑦 ∈ (𝑁 WWalksN 𝐺))
47	3, 8	wwlksnexthasheq 29990	. . . . . . . . 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 29673	. . . . . . . . . 10 ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ₀^* ∧ ∀𝑝 ∈ 𝑉 (♯‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))
50		fveq1 6835	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑦 → (𝑤‘0) = (𝑦‘0))
51	50	eqeq1d 2739	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑦 → ((𝑤‘0) = 𝑃 ↔ (𝑦‘0) = 𝑃))
52	51	elrab 3635	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ↔ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑦‘0) = 𝑃))
53	3, 8	wwlknp 29930	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝑁 WWalksN 𝐺) → (𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
54	53	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑦‘0) = 𝑃) → (𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
55		simpll 767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑦 ∈ Word 𝑉)
56		nn0p1gt0 12461	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 ∈ ℕ₀ → 0 < (𝑁 + 1))
57	56	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → 0 < (𝑁 + 1))
58	57	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 0 < (𝑁 + 1))
59		breq2 5090	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((♯‘𝑦) = (𝑁 + 1) → (0 < (♯‘𝑦) ↔ 0 < (𝑁 + 1)))
60	59	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (0 < (♯‘𝑦) ↔ 0 < (𝑁 + 1)))
61	58, 60	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 0 < (♯‘𝑦))
62		hashle00 14357	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ Word 𝑉 → ((♯‘𝑦) ≤ 0 ↔ 𝑦 = ∅))
63		lencl 14490	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ Word 𝑉 → (♯‘𝑦) ∈ ℕ₀)
64	63	nn0red 12494	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ Word 𝑉 → (♯‘𝑦) ∈ ℝ)
65		0re 11141	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ∈ ℝ
66		lenlt 11219	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((♯‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → ((♯‘𝑦) ≤ 0 ↔ ¬ 0 < (♯‘𝑦)))
67	66	bicomd 223	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((♯‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → (¬ 0 < (♯‘𝑦) ↔ (♯‘𝑦) ≤ 0))
68	64, 65, 67	sylancl 587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ Word 𝑉 → (¬ 0 < (♯‘𝑦) ↔ (♯‘𝑦) ≤ 0))
69		nne 2937	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ 𝑦 ≠ ∅ ↔ 𝑦 = ∅)
70	69	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ Word 𝑉 → (¬ 𝑦 ≠ ∅ ↔ 𝑦 = ∅))
71	62, 68, 70	3bitr4rd 312	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ Word 𝑉 → (¬ 𝑦 ≠ ∅ ↔ ¬ 0 < (♯‘𝑦)))
72	71	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . 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 1133	. . . . . . . . . . . . . . . . . . 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 14525	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅) → (lastS‘𝑦) ∈ 𝑉)
82	80, 81	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (lastS‘𝑦) ∈ 𝑉)
83	82	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ ∀𝑝 ∈ 𝑉 (♯‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾) → (lastS‘𝑦) ∈ 𝑉)
84		preq1 4678	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = (lastS‘𝑦) → {𝑝, 𝑛} = {(lastS‘𝑦), 𝑛})
85	84	eleq1d 2822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = (lastS‘𝑦) → ({𝑝, 𝑛} ∈ (Edg‘𝐺) ↔ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)))
86	85	rabbidv 3397	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = (lastS‘𝑦) → {𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)} = {𝑛 ∈ 𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)})
87	86	fveqeq2d 6844	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = (lastS‘𝑦) → ((♯‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾 ↔ (♯‘{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))
88	87	rspcva 3563	. . . . . . . . . . . . . 14 ⊢ (((lastS‘𝑦) ∈ 𝑉 ∧ ∀𝑝 ∈ 𝑉 (♯‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾) → (♯‘{𝑛 ∈ 𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾)
89	83, 88	sylancom 589	. . . . . . . . . . . . 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 1136	. . . . . . . . . 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 2776	. . . . . . 7 ⊢ ((((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = 𝐾)
96	95	sumeq2dv 15659	. . . . . 6 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}𝐾)
97		oveq1 7369	. . . . . . . 8 ⊢ ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) · 𝐾) = ((𝐾↑𝑁) · 𝐾))
98	97	adantl 481	. . . . . . 7 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) · 𝐾) = ((𝐾↑𝑁) · 𝐾))
99		wwlksnfi 29993	. . . . . . . . . . . 12 ⊢ ((Vtx‘𝐺) ∈ Fin → (𝑁 WWalksN 𝐺) ∈ Fin)
100	29, 99	sylbi 217	. . . . . . . . . . 11 ⊢ (𝑉 ∈ Fin → (𝑁 WWalksN 𝐺) ∈ Fin)
101	100	3ad2ant1 1134	. . . . . . . . . 10 ⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (𝑁 WWalksN 𝐺) ∈ Fin)
102	101	ad2antlr 728	. . . . . . . . 9 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (𝑁 WWalksN 𝐺) ∈ Fin)
103		rabfi 9176	. . . . . . . . 9 ⊢ ((𝑁 WWalksN 𝐺) ∈ Fin → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∈ Fin)
104	102, 103	syl 17	. . . . . . . 8 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∈ Fin)
105		rusgrusgr 29652	. . . . . . . . . . . . 13 ⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph)
106		simp1 1137	. . . . . . . . . . . . 13 ⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → 𝑉 ∈ Fin)
107	105, 106	anim12i 614	. . . . . . . . . . . 12 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin))
108	3	isfusgr 29405	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin))
109	107, 108	sylibr 234	. . . . . . . . . . 11 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝐺 ∈ FinUSGraph)
110		simpl 482	. . . . . . . . . . 11 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝐺 RegUSGraph 𝐾)
111		ne0i 4282	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ 𝑉 → 𝑉 ≠ ∅)
112	111	3ad2ant2 1135	. . . . . . . . . . . 12 ⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → 𝑉 ≠ ∅)
113	112	adantl 481	. . . . . . . . . . 11 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑉 ≠ ∅)
114	3	frusgrnn0 29659	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅) → 𝐾 ∈ ℕ₀)
115	109, 110, 113, 114	syl3anc 1374	. . . . . . . . . 10 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝐾 ∈ ℕ₀)
116	115	nn0cnd 12495	. . . . . . . . 9 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝐾 ∈ ℂ)
117	116	adantr 480	. . . . . . . 8 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → 𝐾 ∈ ℂ)
118		fsumconst 15747	. . . . . . . 8 ⊢ (({𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∈ Fin ∧ 𝐾 ∈ ℂ) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}𝐾 = ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) · 𝐾))
119	104, 117, 118	syl2anc 585	. . . . . . 7 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}𝐾 = ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) · 𝐾))
120	116, 2	expp1d 14104	. . . . . . . 8 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (𝐾↑(𝑁 + 1)) = ((𝐾↑𝑁) · 𝐾))
121	120	adantr 480	. . . . . . 7 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (𝐾↑(𝑁 + 1)) = ((𝐾↑𝑁) · 𝐾))
122	98, 119, 121	3eqtr4d 2782	. . . . . 6 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}𝐾 = (𝐾↑(𝑁 + 1)))
123	96, 122	eqtrd 2772	. . . . 5 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (𝐾↑(𝑁 + 1)))
124	16, 40, 123	3eqtrd 2776	. . . 4 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1)))
125		peano2nn0 12472	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ₀)
126	125	3ad2ant3 1136	. . . . . . 7 ⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (𝑁 + 1) ∈ ℕ₀)
127	126	adantl 481	. . . . . 6 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (𝑁 + 1) ∈ ℕ₀)
128	3, 4	rusgrnumwwlklem 30060	. . . . . . 7 ⊢ ((𝑃 ∈ 𝑉 ∧ (𝑁 + 1) ∈ ℕ₀) → (𝑃𝐿(𝑁 + 1)) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}))
129	128	eqeq1d 2739	. . . . . 6 ⊢ ((𝑃 ∈ 𝑉 ∧ (𝑁 + 1) ∈ ℕ₀) → ((𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)) ↔ (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1))))
130	1, 127, 129	syl2anc 585	. . . . 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 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 {crab 3390 ∅c0 4274 {cpr 4570 class class class wbr 5086 ‘cfv 6494 (class class class)co 7362 ∈ cmpo 7364 Fincfn 8888 ℂcc 11031 ℝcr 11032 0cc0 11033 1c1 11034 + caddc 11036 · cmul 11038 < clt 11174 ≤ cle 11175 ℕ₀cn0 12432 ℕ₀^*cxnn0 12505 ..^cfzo 13603 ↑cexp 14018 ♯chash 14287 Word cword 14470 lastSclsw 14519 prefix cpfx 14628 Σcsu 15643 Vtxcvtx 29083 Edgcedg 29134 USGraphcusgr 29236 FinUSGraphcfusgr 29403 RegUSGraph crusgr 29644 WWalksN cwwlksn 29913

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5304 ax-pr 5372 ax-un 7684 ax-inf2 9557 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110 ax-pre-sup 11111

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-disj 5054 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5521 df-eprel 5526 df-po 5534 df-so 5535 df-fr 5579 df-se 5580 df-we 5581 df-xp 5632 df-rel 5633 df-cnv 5634 df-co 5635 df-dm 5636 df-rn 5637 df-res 5638 df-ima 5639 df-pred 6261 df-ord 6322 df-on 6323 df-lim 6324 df-suc 6325 df-iota 6450 df-fun 6496 df-fn 6497 df-f 6498 df-f1 6499 df-fo 6500 df-f1o 6501 df-fv 6502 df-isom 6503 df-riota 7319 df-ov 7365 df-oprab 7366 df-mpo 7367 df-om 7813 df-1st 7937 df-2nd 7938 df-frecs 8226 df-wrecs 8257 df-recs 8306 df-rdg 8344 df-1o 8400 df-2o 8401 df-oadd 8404 df-er 8638 df-map 8770 df-pm 8771 df-en 8889 df-dom 8890 df-sdom 8891 df-fin 8892 df-sup 9350 df-oi 9420 df-dju 9820 df-card 9858 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-div 11803 df-nn 12170 df-2 12239 df-3 12240 df-n0 12433 df-xnn0 12506 df-z 12520 df-uz 12784 df-rp 12938 df-xadd 13059 df-fz 13457 df-fzo 13604 df-seq 13959 df-exp 14019 df-hash 14288 df-word 14471 df-lsw 14520 df-concat 14528 df-s1 14554 df-substr 14599 df-pfx 14629 df-cj 15056 df-re 15057 df-im 15058 df-sqrt 15192 df-abs 15193 df-clim 15445 df-sum 15644 df-vtx 29085 df-iedg 29086 df-edg 29135 df-uhgr 29145 df-ushgr 29146 df-upgr 29169 df-umgr 29170 df-uspgr 29237 df-usgr 29238 df-fusgr 29404 df-nbgr 29420 df-vtxdg 29554 df-rgr 29645 df-rusgr 29646 df-wwlks 29917 df-wwlksn 29918

This theorem is referenced by: rusgrnumwwlk 30065

W3C validator