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

Theorem rusgrnumwwlks 27178
Description: Induction step for rusgrnumwwlk 27179. (Contributed by Alexander van der Vekens, 24-Aug-2018.) (Revised by AV, 7-May-2021.)
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 1250 . . 3 ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 𝑃𝑉)
2 simpr3 1252 . . 3 ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 𝑁 ∈ ℕ0)
3 rusgrnumwwlk.v . . . . 5 𝑉 = (Vtx‘𝐺)
4 rusgrnumwwlk.l . . . . 5 𝐿 = (𝑣𝑉, 𝑛 ∈ ℕ0 ↦ (♯‘{𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑣}))
53, 4rusgrnumwwlklem 27174 . . . 4 ((𝑃𝑉𝑁 ∈ ℕ0) → (𝑃𝐿𝑁) = (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}))
65eqeq1d 2766 . . 3 ((𝑃𝑉𝑁 ∈ ℕ0) → ((𝑃𝐿𝑁) = (𝐾𝑁) ↔ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)))
71, 2, 6syl2anc 579 . 2 ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → ((𝑃𝐿𝑁) = (𝐾𝑁) ↔ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)))
8 eqid 2764 . . . . . . . . . . . . 13 (Edg‘𝐺) = (Edg‘𝐺)
98wwlksnredwwlkn0 27095 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺)) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))))
109ex 401 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → (𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
11103ad2ant3 1165 . . . . . . . . . 10 ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → (𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
1211adantl 473 . . . . . . . . 9 ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
1312imp 395 . . . . . . . 8 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ 𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺)) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))))
1413rabbidva 3336 . . . . . . 7 ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
1514adantr 472 . . . . . 6 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
1615fveq2d 6378 . . . . 5 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
17 simp2 1167 . . . . . . . . . . . . 13 (((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) → (𝑦‘0) = 𝑃)
1817pm4.71ri 556 . . . . . . . . . . . 12 (((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) ↔ ((𝑦‘0) = 𝑃 ∧ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))))
1918a1i 11 . . . . . . . . . . 11 ((((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ 𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺)) ∧ 𝑦 ∈ (𝑁 WWalksN 𝐺)) → (((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) ↔ ((𝑦‘0) = 𝑃 ∧ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
2019rexbidva 3195 . . . . . . . . . 10 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ 𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺)) → (∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑦‘0) = 𝑃 ∧ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)))))
21 fveq1 6373 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑥‘0) = (𝑦‘0))
2221eqeq1d 2766 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((𝑥‘0) = 𝑃 ↔ (𝑦‘0) = 𝑃))
2322rexrab 3526 . . . . . . . . . 10 (∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) ↔ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑦‘0) = 𝑃 ∧ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))))
2420, 23syl6bbr 280 . . . . . . . . 9 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ 𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺)) → (∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺)) ↔ ∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))))
2524rabbidva 3336 . . . . . . . 8 ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
2625adantr 472 . . . . . . 7 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
2726fveq2d 6378 . . . . . 6 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
28 simplr1 1275 . . . . . . 7 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → 𝑉 ∈ Fin)
293eleq1i 2834 . . . . . . . 8 (𝑉 ∈ Fin ↔ (Vtx‘𝐺) ∈ Fin)
3029biimpi 207 . . . . . . 7 (𝑉 ∈ Fin → (Vtx‘𝐺) ∈ Fin)
31 eqid 2764 . . . . . . . 8 ((𝑁 + 1) WWalksN 𝐺) = ((𝑁 + 1) WWalksN 𝐺)
32 eqid 2764 . . . . . . . 8 {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} = {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃}
3331, 8, 32hashwwlksnext 27114 . . . . . . 7 ((Vtx‘𝐺) ∈ Fin → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
3428, 30, 333syl 18 . . . . . 6 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
35 fveq1 6373 . . . . . . . . . 10 (𝑥 = 𝑤 → (𝑥‘0) = (𝑤‘0))
3635eqeq1d 2766 . . . . . . . . 9 (𝑥 = 𝑤 → ((𝑥‘0) = 𝑃 ↔ (𝑤‘0) = 𝑃))
3736cbvrabv 3347 . . . . . . . 8 {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}
3837sumeq1i 14714 . . . . . . 7 Σ𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
3938a1i 11 . . . . . 6 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → Σ𝑦 ∈ {𝑥 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑥‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
4027, 34, 393eqtrd 2802 . . . . 5 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ∃𝑦 ∈ (𝑁 WWalksN 𝐺)((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
41 rusgrnumwwlkslem 27173 . . . . . . . . . . 11 (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
4241eqcomd 2770 . . . . . . . . . 10 (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))} = {𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))})
4342fveq2d 6378 . . . . . . . . 9 (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
4443adantl 473 . . . . . . . 8 ((((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}))
45 elrabi 3513 . . . . . . . . . 10 (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → 𝑦 ∈ (𝑁 WWalksN 𝐺))
4645adantl 473 . . . . . . . . 9 ((((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → 𝑦 ∈ (𝑁 WWalksN 𝐺))
473, 8wwlksnexthasheq 27102 . . . . . . . . 9 (𝑦 ∈ (𝑁 WWalksN 𝐺) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (♯‘{𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}))
4846, 47syl 17 . . . . . . . 8 ((((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (♯‘{𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}))
493rusgrpropadjvtx 26771 . . . . . . . . . 10 (𝐺RegUSGraph𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑝𝑉 (♯‘{𝑛𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))
50 fveq1 6373 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑦 → (𝑤‘0) = (𝑦‘0))
5150eqeq1d 2766 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑦 → ((𝑤‘0) = 𝑃 ↔ (𝑦‘0) = 𝑃))
5251elrab 3518 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ↔ (𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑦‘0) = 𝑃))
533, 8wwlknp 27026 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝑁 WWalksN 𝐺) → (𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
5453adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑦‘0) = 𝑃) → (𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
55 simpll 783 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 𝑦 ∈ Word 𝑉)
56 nn0p1gt0 11568 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑁 ∈ ℕ0 → 0 < (𝑁 + 1))
57563ad2ant3 1165 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → 0 < (𝑁 + 1))
5857adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 0 < (𝑁 + 1))
59 breq2 4812 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((♯‘𝑦) = (𝑁 + 1) → (0 < (♯‘𝑦) ↔ 0 < (𝑁 + 1)))
6059ad2antlr 718 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (0 < (♯‘𝑦) ↔ 0 < (𝑁 + 1)))
6158, 60mpbird 248 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 0 < (♯‘𝑦))
62 hashle00 13388 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ Word 𝑉 → ((♯‘𝑦) ≤ 0 ↔ 𝑦 = ∅))
63 lencl 13504 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ Word 𝑉 → (♯‘𝑦) ∈ ℕ0)
6463nn0red 11598 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ Word 𝑉 → (♯‘𝑦) ∈ ℝ)
65 0re 10294 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ∈ ℝ
66 lenlt 10369 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((♯‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → ((♯‘𝑦) ≤ 0 ↔ ¬ 0 < (♯‘𝑦)))
6766bicomd 214 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((♯‘𝑦) ∈ ℝ ∧ 0 ∈ ℝ) → (¬ 0 < (♯‘𝑦) ↔ (♯‘𝑦) ≤ 0))
6864, 65, 67sylancl 580 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ Word 𝑉 → (¬ 0 < (♯‘𝑦) ↔ (♯‘𝑦) ≤ 0))
69 nne 2940 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑦 ≠ ∅ ↔ 𝑦 = ∅)
7069a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ Word 𝑉 → (¬ 𝑦 ≠ ∅ ↔ 𝑦 = ∅))
7162, 68, 703bitr4rd 303 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ Word 𝑉 → (¬ 𝑦 ≠ ∅ ↔ ¬ 0 < (♯‘𝑦)))
7271ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (¬ 𝑦 ≠ ∅ ↔ ¬ 0 < (♯‘𝑦)))
7372con4bid 308 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (𝑦 ≠ ∅ ↔ 0 < (♯‘𝑦)))
7461, 73mpbird 248 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 𝑦 ≠ ∅)
7555, 74jca 507 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (𝑦 ∈ Word 𝑉𝑦 ≠ ∅))
7675ex 401 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1)) → ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → (𝑦 ∈ Word 𝑉𝑦 ≠ ∅)))
77763adant3 1162 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ Word 𝑉 ∧ (♯‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦𝑖), (𝑦‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → (𝑦 ∈ Word 𝑉𝑦 ≠ ∅)))
7854, 77syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑦‘0) = 𝑃) → ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → (𝑦 ∈ Word 𝑉𝑦 ≠ ∅)))
7952, 78sylbi 208 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → (𝑦 ∈ Word 𝑉𝑦 ≠ ∅)))
8079imp 395 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (𝑦 ∈ Word 𝑉𝑦 ≠ ∅))
81 lswcl 13538 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ Word 𝑉𝑦 ≠ ∅) → (lastS‘𝑦) ∈ 𝑉)
8280, 81syl 17 . . . . . . . . . . . . . . 15 ((𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (lastS‘𝑦) ∈ 𝑉)
8382ad2antrr 717 . . . . . . . . . . . . . 14 ((((𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) ∧ ∀𝑝𝑉 (♯‘{𝑛𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾) → (lastS‘𝑦) ∈ 𝑉)
84 preq1 4422 . . . . . . . . . . . . . . . . . 18 (𝑝 = (lastS‘𝑦) → {𝑝, 𝑛} = {(lastS‘𝑦), 𝑛})
8584eleq1d 2828 . . . . . . . . . . . . . . . . 17 (𝑝 = (lastS‘𝑦) → ({𝑝, 𝑛} ∈ (Edg‘𝐺) ↔ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)))
8685rabbidv 3337 . . . . . . . . . . . . . . . 16 (𝑝 = (lastS‘𝑦) → {𝑛𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)} = {𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)})
8786fveqeq2d 6382 . . . . . . . . . . . . . . 15 (𝑝 = (lastS‘𝑦) → ((♯‘{𝑛𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾 ↔ (♯‘{𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))
8887rspcva 3458 . . . . . . . . . . . . . 14 (((lastS‘𝑦) ∈ 𝑉 ∧ ∀𝑝𝑉 (♯‘{𝑛𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾) → (♯‘{𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾)
8983, 88sylancom 582 . . . . . . . . . . . . 13 ((((𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) ∧ ∀𝑝𝑉 (♯‘{𝑛𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾) → (♯‘{𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾)
9089exp41 425 . . . . . . . . . . . 12 (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁) → (∀𝑝𝑉 (♯‘{𝑛𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾 → (♯‘{𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))))
9190com14 96 . . . . . . . . . . 11 (∀𝑝𝑉 (♯‘{𝑛𝑉 ∣ {𝑝, 𝑛} ∈ (Edg‘𝐺)}) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁) → (𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} → (♯‘{𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾))))
92913ad2ant3 1165 . . . . . . . . . 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 416 . . . . . . . 8 ((((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → (♯‘{𝑛𝑉 ∣ {(lastS‘𝑦), 𝑛} ∈ (Edg‘𝐺)}) = 𝐾)
9544, 48, 943eqtrd 2802 . . . . . . 7 ((((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = 𝐾)
9695sumeq2dv 14719 . . . . . 6 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}𝐾)
97 oveq1 6848 . . . . . . . 8 ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) · 𝐾) = ((𝐾𝑁) · 𝐾))
9897adantl 473 . . . . . . 7 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) · 𝐾) = ((𝐾𝑁) · 𝐾))
99 wwlksnfi 27105 . . . . . . . . . . . 12 ((Vtx‘𝐺) ∈ Fin → (𝑁 WWalksN 𝐺) ∈ Fin)
10029, 99sylbi 208 . . . . . . . . . . 11 (𝑉 ∈ Fin → (𝑁 WWalksN 𝐺) ∈ Fin)
1011003ad2ant1 1163 . . . . . . . . . 10 ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → (𝑁 WWalksN 𝐺) ∈ Fin)
102101ad2antlr 718 . . . . . . . . 9 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → (𝑁 WWalksN 𝐺) ∈ Fin)
103 rabfi 8391 . . . . . . . . 9 ((𝑁 WWalksN 𝐺) ∈ Fin → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∈ Fin)
104102, 103syl 17 . . . . . . . 8 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∈ Fin)
105 rusgrusgr 26750 . . . . . . . . . . . . 13 (𝐺RegUSGraph𝐾𝐺 ∈ USGraph)
106 simp1 1166 . . . . . . . . . . . . 13 ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → 𝑉 ∈ Fin)
107105, 106anim12i 606 . . . . . . . . . . . 12 ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin))
1083isfusgr 26488 . . . . . . . . . . . 12 (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin))
109107, 108sylibr 225 . . . . . . . . . . 11 ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 𝐺 ∈ FinUSGraph)
110 simpl 474 . . . . . . . . . . 11 ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 𝐺RegUSGraph𝐾)
111 ne0i 4084 . . . . . . . . . . . . 13 (𝑃𝑉𝑉 ≠ ∅)
1121113ad2ant2 1164 . . . . . . . . . . . 12 ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → 𝑉 ≠ ∅)
113112adantl 473 . . . . . . . . . . 11 ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 𝑉 ≠ ∅)
1143frusgrnn0 26757 . . . . . . . . . . 11 ((𝐺 ∈ FinUSGraph ∧ 𝐺RegUSGraph𝐾𝑉 ≠ ∅) → 𝐾 ∈ ℕ0)
115109, 110, 113, 114syl3anc 1490 . . . . . . . . . 10 ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 𝐾 ∈ ℕ0)
116115nn0cnd 11599 . . . . . . . . 9 ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → 𝐾 ∈ ℂ)
117116adantr 472 . . . . . . . 8 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → 𝐾 ∈ ℂ)
118 fsumconst 14807 . . . . . . . 8 (({𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} ∈ Fin ∧ 𝐾 ∈ ℂ) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}𝐾 = ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) · 𝐾))
119104, 117, 118syl2anc 579 . . . . . . 7 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}𝐾 = ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) · 𝐾))
120116, 2expp1d 13215 . . . . . . . 8 ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (𝐾↑(𝑁 + 1)) = ((𝐾𝑁) · 𝐾))
121120adantr 472 . . . . . . 7 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → (𝐾↑(𝑁 + 1)) = ((𝐾𝑁) · 𝐾))
12298, 119, 1213eqtr4d 2808 . . . . . 6 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}𝐾 = (𝐾↑(𝑁 + 1)))
12396, 122eqtrd 2798 . . . . 5 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → Σ𝑦 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ ((𝑤 substr ⟨0, (𝑁 + 1)⟩) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {(lastS‘𝑦), (lastS‘𝑤)} ∈ (Edg‘𝐺))}) = (𝐾↑(𝑁 + 1)))
12416, 40, 1233eqtrd 2802 . . . 4 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1)))
125 peano2nn0 11579 . . . . . . . 8 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
1261253ad2ant3 1165 . . . . . . 7 ((𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0) → (𝑁 + 1) ∈ ℕ0)
127126adantl 473 . . . . . 6 ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈ ℕ0)
1283, 4rusgrnumwwlklem 27174 . . . . . . 7 ((𝑃𝑉 ∧ (𝑁 + 1) ∈ ℕ0) → (𝑃𝐿(𝑁 + 1)) = (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}))
129128eqeq1d 2766 . . . . . 6 ((𝑃𝑉 ∧ (𝑁 + 1) ∈ ℕ0) → ((𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)) ↔ (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1))))
1301, 127, 129syl2anc 579 . . . . 5 ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → ((𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)) ↔ (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1))))
131130adantr 472 . . . 4 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → ((𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)) ↔ (♯‘{𝑤 ∈ ((𝑁 + 1) WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1))))
132124, 131mpbird 248 . . 3 (((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) ∧ (♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁)) → (𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)))
133132ex 401 . 2 ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → ((♯‘{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (𝐾𝑁) → (𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1))))
1347, 133sylbid 231 1 ((𝐺RegUSGraph𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃𝑉𝑁 ∈ ℕ0)) → ((𝑃𝐿𝑁) = (𝐾𝑁) → (𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2936  wral 3054  wrex 3055  {crab 3058  c0 4078  {cpr 4335  cop 4339   class class class wbr 4808  cfv 6067  (class class class)co 6841  cmpt2 6843  Fincfn 8159  cc 10186  cr 10187  0cc0 10188  1c1 10189   + caddc 10191   · cmul 10193   < clt 10327  cle 10328  0cn0 11537  0*cxnn0 11609  ..^cfzo 12672  cexp 13066  chash 13320  Word cword 13485  lastSclsw 13532   substr csubstr 13615  Σcsu 14702  Vtxcvtx 26164  Edgcedg 26215  USGraphcusgr 26321  FinUSGraphcfusgr 26486  RegUSGraphcrusgr 26742   WWalksN cwwlksn 27009
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-inf2 8752  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265  ax-pre-sup 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-disj 4777  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-se 5236  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-isom 6076  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-om 7263  df-1st 7365  df-2nd 7366  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-2o 7764  df-oadd 7767  df-er 7946  df-map 8061  df-pm 8062  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-sup 8554  df-oi 8621  df-card 9015  df-cda 9242  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-div 10938  df-nn 11274  df-2 11334  df-3 11335  df-n0 11538  df-xnn0 11610  df-z 11624  df-uz 11886  df-rp 12028  df-xadd 12146  df-fz 12533  df-fzo 12673  df-seq 13008  df-exp 13067  df-hash 13321  df-word 13486  df-lsw 13533  df-concat 13541  df-s1 13566  df-substr 13616  df-cj 14125  df-re 14126  df-im 14127  df-sqrt 14261  df-abs 14262  df-clim 14505  df-sum 14703  df-vtx 26166  df-iedg 26167  df-edg 26216  df-uhgr 26229  df-ushgr 26230  df-upgr 26253  df-umgr 26254  df-uspgr 26322  df-usgr 26323  df-fusgr 26487  df-nbgr 26503  df-vtxdg 26652  df-rgr 26743  df-rusgr 26744  df-wwlks 27013  df-wwlksn 27014
This theorem is referenced by:  rusgrnumwwlk  27179
  Copyright terms: Public domain W3C validator