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

Theorem rusgrnumwwlks 29995
Description: Induction step for rusgrnumwwlk 29996. (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 𝐿 = (𝑣𝑉, 𝑛 ∈ ℕ0 ↦ (♯‘{𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑣}))
Assertion
Ref Expression
rusgrnumwwlks ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → ((𝑃𝐿𝑁) = (𝐾𝑁) → (𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1))))
Distinct variable groups:   𝑛,𝐺,𝑣,𝑤   𝑛,𝑁,𝑣,𝑤   𝑃,𝑛,𝑣,𝑤   𝑛,𝑉,𝑣,𝑤   𝑤,𝐾
Allowed substitution hints:   𝐾(𝑣,𝑛)   𝐿(𝑤,𝑣,𝑛)

Proof of Theorem rusgrnumwwlks
Dummy variables 𝑖 𝑝 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr2 1195 . . 3 ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 𝑃𝑉)
2 simpr3 1196 . . 3 ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 𝑁 ∈ ℕ0)
3 rusgrnumwwlk.v . . . . 5 𝑉 = (Vtx‘𝐺)
4 rusgrnumwwlk.l . . . . 5 𝐿 = (𝑣𝑉, 𝑛 ∈ ℕ0 ↦ (♯‘{𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑣}))
53, 4rusgrnumwwlklem 29991 . . . 4 ((𝑃𝑉𝑁 ∈ ℕ0) → (𝑃𝐿𝑁) = (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}))
65eqeq1d 2738 . . 3 ((𝑃𝑉𝑁 ∈ ℕ0) → ((𝑃𝐿𝑁) = (𝐾𝑁) ↔ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)))
71, 2, 6syl2anc 584 . 2 ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → ((𝑃𝐿𝑁) = (𝐾𝑁) ↔ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)))
8 eqid 2736 . . . . . . . . . . . . 13 (Edg‘𝐺) = (Edg‘𝐺)
98wwlksnredwwlkn0 29917 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺)) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))))
109ex 412 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → (𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
11103ad2ant3 1135 . . . . . . . . . 10 ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → (𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
1211adantl 481 . . . . . . . . 9 ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
1312imp 406 . . . . . . . 8 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ 𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺)) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))))
1413rabbidva 3442 . . . . . . 7 ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
1514adantr 480 . . . . . 6 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
1615fveq2d 6909 . . . . 5 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 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) = 𝑃)
1817pm4.71ri 560 . . . . . . . . . . . 12 (((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) ↔ ((𝑦‘0) = 𝑃 ∧ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))))
1918a1i 11 . . . . . . . . . . 11 ((((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ 𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺)) ∧ 𝑦 ∈ (𝑁 WWalksN 𝐺)) → (((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) ↔ ((𝑦‘0) = 𝑃 ∧ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
2019rexbidva 3176 . . . . . . . . . 10 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ 𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺)) → (∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑦‘0) = 𝑃 ∧ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
21 fveq1 6904 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥‘0) = (𝑦‘0))
2221eqeq1d 2738 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((𝑥‘0) = 𝑃 ↔ (𝑦‘0) = 𝑃))
2322rexrab 3701 . . . . . . . . . 10 (∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑦‘0) = 𝑃 ∧ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))))
2420, 23bitr4di 289 . . . . . . . . 9 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ 𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺)) → (∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) ↔ ∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))))
2524rabbidva 3442 . . . . . . . 8 ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
2625adantr 480 . . . . . . 7 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
2726fveq2d 6909 . . . . . 6 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
28 simplr1 1215 . . . . . . 7 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → 𝑉 ∈ Fin)
293eleq1i 2831 . . . . . . . 8 (𝑉 ∈ Fin ↔ (Vtx‘𝐺) ∈ Fin)
3029biimpi 216 . . . . . . 7 (𝑉 ∈ Fin → (Vtx‘𝐺) ∈ Fin)
31 eqid 2736 . . . . . . . 8 ((𝑁 + 1) WWalksN 𝐺) = ((𝑁 + 1) WWalksN 𝐺)
32 eqid 2736 . . . . . . . 8 {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} = {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃}
3331, 8, 32hashwwlksnext 29935 . . . . . . 7 ((Vtx‘𝐺) ∈ Fin → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
3428, 30, 333syl 18 . . . . . 6 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
35 fveq1 6904 . . . . . . . . . 10 (𝑥 = 𝑤 → (𝑥‘0) = (𝑤‘0))
3635eqeq1d 2738 . . . . . . . . 9 (𝑥 = 𝑤 → ((𝑥‘0) = 𝑃 ↔ (𝑤‘0) = 𝑃))
3736cbvrabv 3446 . . . . . . . 8 {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}
3837sumeq1i 15734 . . . . . . 7 Σ𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
3938a1i 11 . . . . . 6 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → Σ𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
4027, 34, 393eqtrd 2780 . . . . 5 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
41 rusgrnumwwlkslem 29990 . . . . . . . . . . 11 (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
4241eqcomd 2742 . . . . . . . . . 10 (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
4342fveq2d 6909 . . . . . . . . 9 (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
4443adantl 481 . . . . . . . 8 ((((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
45 elrabi 3686 . . . . . . . . . 10 (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → 𝑦 ∈ (𝑁 WWalksN 𝐺))
4645adantl 481 . . . . . . . . 9 ((((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → 𝑦 ∈ (𝑁 WWalksN 𝐺))
473, 8wwlksnexthasheq 29924 . . . . . . . . 9 (𝑦 ∈ (𝑁 WWalksN 𝐺) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (♯‘{𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}))
4846, 47syl 17 . . . . . . . 8 ((((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (♯‘{𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}))
493rusgrpropadjvtx 29604 . . . . . . . . . 10 (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑝𝑉 (♯‘{𝑛𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))
50 fveq1 6904 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑦 → (𝑤‘0) = (𝑦‘0))
5150eqeq1d 2738 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑦 → ((𝑤‘0) = 𝑃 ↔ (𝑦‘0) = 𝑃))
5251elrab 3691 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ↔ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑦‘0) = 𝑃))
533, 8wwlknp 29864 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝑁 WWalksN 𝐺) → (𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
5453adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑦‘0) = 𝑃) → (𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
55 simpll 766 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 𝑦 ∈ Word 𝑉)
56 nn0p1gt0 12557 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ0 → 0 < (𝑁 + 1))
57563ad2ant3 1135 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → 0 < (𝑁 + 1))
5857adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 0 < (𝑁 + 1))
59 breq2 5146 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((♯‘𝑦) = (𝑁 + 1) → (0 < (♯‘𝑦) ↔ 0 < (𝑁 + 1)))
6059ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (0 < (♯‘𝑦) ↔ 0 < (𝑁 + 1)))
6158, 60mpbird 257 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 0 < (♯‘𝑦))
62 hashle00 14440 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ Word 𝑉 → ((♯‘𝑦) ≤ 0 ↔ 𝑦 = ∅))
63 lencl 14572 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ Word 𝑉 → (♯‘𝑦) ∈ ℕ0)
6463nn0red 12590 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ Word 𝑉 → (♯‘𝑦) ∈ ℝ)
65 0re 11264 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ∈ ℝ
66 lenlt 11340 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((♯‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → ((♯‘𝑦) ≤ 0 ↔ ¬ 0 < (♯‘𝑦)))
6766bicomd 223 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((♯‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → (¬ 0 < (♯‘𝑦) ↔ (♯‘𝑦) ≤ 0))
6864, 65, 67sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ Word 𝑉 → (¬ 0 < (♯‘𝑦) ↔ (♯‘𝑦) ≤ 0))
69 nne 2943 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑦 ≠ ∅ ↔ 𝑦 = ∅)
7069a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ Word 𝑉 → (¬ 𝑦 ≠ ∅ ↔ 𝑦 = ∅))
7162, 68, 703bitr4rd 312 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ Word 𝑉 → (¬ 𝑦 ≠ ∅ ↔ ¬ 0 < (♯‘𝑦)))
7271ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (¬ 𝑦 ≠ ∅ ↔ ¬ 0 < (♯‘𝑦)))
7372con4bid 317 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (𝑦 ≠ ∅ ↔ 0 < (♯‘𝑦)))
7461, 73mpbird 257 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 𝑦 ≠ ∅)
7555, 74jca 511 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (𝑦 ∈ Word 𝑉𝑦 ≠ ∅))
7675ex 412 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) → ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → (𝑦 ∈ Word 𝑉𝑦 ≠ ∅)))
77763adant3 1132 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → (𝑦 ∈ Word 𝑉𝑦 ≠ ∅)))
7854, 77syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑦‘0) = 𝑃) → ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → (𝑦 ∈ Word 𝑉𝑦 ≠ ∅)))
7952, 78sylbi 217 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → (𝑦 ∈ Word 𝑉𝑦 ≠ ∅)))
8079imp 406 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (𝑦 ∈ Word 𝑉𝑦 ≠ ∅))
81 lswcl 14607 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ Word 𝑉𝑦 ≠ ∅) → (lastS‘𝑦) ∈ 𝑉)
8280, 81syl 17 . . . . . . . . . . . . . . 15 ((𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (lastS‘𝑦) ∈ 𝑉)
8382ad2antrr 726 . . . . . . . . . . . . . 14 ((((𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) ∧ ∀𝑝𝑉 (♯‘{𝑛𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾) → (lastS‘𝑦) ∈ 𝑉)
84 preq1 4732 . . . . . . . . . . . . . . . . . 18 (𝑝 = (lastS‘𝑦) → {𝑝, 𝑛} = {(lastS‘𝑦), 𝑛})
8584eleq1d 2825 . . . . . . . . . . . . . . . . 17 (𝑝 = (lastS‘𝑦) → ({𝑝, 𝑛} ∈ (Edg‘𝐺) ↔ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)))
8685rabbidv 3443 . . . . . . . . . . . . . . . 16 (𝑝 = (lastS‘𝑦) → {𝑛𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)} = {𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)})
8786fveqeq2d 6913 . . . . . . . . . . . . . . 15 (𝑝 = (lastS‘𝑦) → ((♯‘{𝑛𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾 ↔ (♯‘{𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))
8887rspcva 3619 . . . . . . . . . . . . . 14 (((lastS‘𝑦) ∈ 𝑉 ∧ ∀𝑝𝑉 (♯‘{𝑛𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾) → (♯‘{𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾)
8983, 88sylancom 588 . . . . . . . . . . . . 13 ((((𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) ∧ ∀𝑝𝑉 (♯‘{𝑛𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾) → (♯‘{𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾)
9089exp41 434 . . . . . . . . . . . 12 (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁) → (∀𝑝𝑉 (♯‘{𝑛𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾 → (♯‘{𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))))
9190com14 96 . . . . . . . . . . 11 (∀𝑝𝑉 (♯‘{𝑛𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁) → (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → (♯‘{𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))))
92913ad2ant3 1135 . . . . . . . . . 10 ((𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑝𝑉 (♯‘{𝑛𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾) → ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁) → (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → (♯‘{𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))))
9349, 92syl 17 . . . . . . . . 9 (𝐺 RegUSGraph 𝐾 → ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁) → (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → (♯‘{𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))))
9493imp41 425 . . . . . . . 8 ((((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → (♯‘{𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾)
9544, 48, 943eqtrd 2780 . . . . . . 7 ((((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = 𝐾)
9695sumeq2dv 15739 . . . . . 6 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}𝐾)
97 oveq1 7439 . . . . . . . 8 ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) · 𝐾) = ((𝐾𝑁) · 𝐾))
9897adantl 481 . . . . . . 7 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) · 𝐾) = ((𝐾𝑁) · 𝐾))
99 wwlksnfi 29927 . . . . . . . . . . . 12 ((Vtx‘𝐺) ∈ Fin → (𝑁 WWalksN 𝐺) ∈ Fin)
10029, 99sylbi 217 . . . . . . . . . . 11 (𝑉 ∈ Fin → (𝑁 WWalksN 𝐺) ∈ Fin)
1011003ad2ant1 1133 . . . . . . . . . 10 ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → (𝑁 WWalksN 𝐺) ∈ Fin)
102101ad2antlr 727 . . . . . . . . 9 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → (𝑁 WWalksN 𝐺) ∈ Fin)
103 rabfi 9304 . . . . . . . . 9 ((𝑁 WWalksN 𝐺) ∈ Fin → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∈ Fin)
104102, 103syl 17 . . . . . . . 8 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∈ Fin)
105 rusgrusgr 29583 . . . . . . . . . . . . 13 (𝐺 RegUSGraph 𝐾𝐺 ∈ USGraph)
106 simp1 1136 . . . . . . . . . . . . 13 ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → 𝑉 ∈ Fin)
107105, 106anim12i 613 . . . . . . . . . . . 12 ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin))
1083isfusgr 29336 . . . . . . . . . . . 12 (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin))
109107, 108sylibr 234 . . . . . . . . . . 11 ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 𝐺 ∈ FinUSGraph)
110 simpl 482 . . . . . . . . . . 11 ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 𝐺 RegUSGraph 𝐾)
111 ne0i 4340 . . . . . . . . . . . . 13 (𝑃𝑉𝑉 ≠ ∅)
1121113ad2ant2 1134 . . . . . . . . . . . 12 ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → 𝑉 ≠ ∅)
113112adantl 481 . . . . . . . . . . 11 ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 𝑉 ≠ ∅)
1143frusgrnn0 29590 . . . . . . . . . . 11 ((𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾𝑉 ≠ ∅) → 𝐾 ∈ ℕ0)
115109, 110, 113, 114syl3anc 1372 . . . . . . . . . 10 ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 𝐾 ∈ ℕ0)
116115nn0cnd 12591 . . . . . . . . 9 ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 𝐾 ∈ ℂ)
117116adantr 480 . . . . . . . 8 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → 𝐾 ∈ ℂ)
118 fsumconst 15827 . . . . . . . 8 (({𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∈ Fin ∧ 𝐾 ∈ ℂ) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}𝐾 = ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) · 𝐾))
119104, 117, 118syl2anc 584 . . . . . . 7 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}𝐾 = ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) · 𝐾))
120116, 2expp1d 14188 . . . . . . . 8 ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (𝐾↑(𝑁 + 1)) = ((𝐾𝑁) · 𝐾))
121120adantr 480 . . . . . . 7 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → (𝐾↑(𝑁 + 1)) = ((𝐾𝑁) · 𝐾))
12298, 119, 1213eqtr4d 2786 . . . . . 6 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}𝐾 = (𝐾↑(𝑁 + 1)))
12396, 122eqtrd 2776 . . . . 5 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 + 1)) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (𝐾↑(𝑁 + 1)))
12416, 40, 1233eqtrd 2780 . . . 4 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1)))
125 peano2nn0 12568 . . . . . . . 8 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
1261253ad2ant3 1135 . . . . . . 7 ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → (𝑁 + 1) ∈ ℕ0)
127126adantl 481 . . . . . 6 ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈ ℕ0)
1283, 4rusgrnumwwlklem 29991 . . . . . . 7 ((𝑃𝑉 ∧ (𝑁 + 1) ∈ ℕ0) → (𝑃𝐿(𝑁 + 1)) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}))
129128eqeq1d 2738 . . . . . 6 ((𝑃𝑉 ∧ (𝑁 + 1) ∈ ℕ0) → ((𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)) ↔ (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1))))
1301, 127, 129syl2anc 584 . . . . 5 ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → ((𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)) ↔ (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1))))
131130adantr 480 . . . 4 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → ((𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)) ↔ (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1))))
132124, 131mpbird 257 . . 3 (((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → (𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)))
133132ex 412 . 2 ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁) → (𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1))))
1347, 133sylbid 240 1 ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → ((𝑃𝐿𝑁) = (𝐾𝑁) → (𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1539  wcel 2107  wne 2939  wral 3060  wrex 3069  {crab 3435  c0 4332  {cpr 4627   class class class wbr 5142  cfv 6560  (class class class)co 7432  cmpo 7434  Fincfn 8986  cc 11154  cr 11155  0cc0 11156  1c1 11157   + caddc 11159   · cmul 11161   < clt 11296  cle 11297  0cn0 12528  0*cxnn0 12601  ..^cfzo 13695  cexp 14103  chash 14370  Word cword 14553  lastSclsw 14601   prefix cpfx 14709  Σcsu 15723  Vtxcvtx 29014  Edgcedg 29065  USGraphcusgr 29167  FinUSGraphcfusgr 29334   RegUSGraph crusgr 29575   WWalksN cwwlksn 29847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-inf2 9682  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233  ax-pre-sup 11234
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-disj 5110  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-se 5637  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-isom 6569  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1st 8015  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-2o 8508  df-oadd 8511  df-er 8746  df-map 8869  df-pm 8870  df-en 8987  df-dom 8988  df-sdom 8989  df-fin 8990  df-sup 9483  df-oi 9551  df-dju 9942  df-card 9980  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-div 11922  df-nn 12268  df-2 12330  df-3 12331  df-n0 12529  df-xnn0 12602  df-z 12616  df-uz 12880  df-rp 13036  df-xadd 13156  df-fz 13549  df-fzo 13696  df-seq 14044  df-exp 14104  df-hash 14371  df-word 14554  df-lsw 14602  df-concat 14610  df-s1 14635  df-substr 14680  df-pfx 14710  df-cj 15139  df-re 15140  df-im 15141  df-sqrt 15275  df-abs 15276  df-clim 15525  df-sum 15724  df-vtx 29016  df-iedg 29017  df-edg 29066  df-uhgr 29076  df-ushgr 29077  df-upgr 29100  df-umgr 29101  df-uspgr 29168  df-usgr 29169  df-fusgr 29335  df-nbgr 29351  df-vtxdg 29485  df-rgr 29576  df-rusgr 29577  df-wwlks 29851  df-wwlksn 29852
This theorem is referenced by:  rusgrnumwwlk  29996
  Copyright terms: Public domain W3C validator