Step | Hyp | Ref
| Expression |
1 | | rusisusgra 26458 |
. . . 4
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝑉 USGrph 𝐸) |
2 | 1 | adantr 480 |
. . 3
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑉 USGrph 𝐸) |
3 | | simpr2 1061 |
. . 3
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑃 ∈ 𝑉) |
4 | | simp3 1056 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈
ℕ0) |
5 | 4 | adantl 481 |
. . 3
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑁 ∈
ℕ0) |
6 | | rusgranumwlk.w |
. . . . 5
⊢ 𝑊 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑛}) |
7 | | rusgranumwlk.l |
. . . . 5
⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦
(#‘{𝑤 ∈ (𝑊‘𝑛) ∣ ((2nd ‘𝑤)‘0) = 𝑣})) |
8 | 6, 7 | rusgranumwlklem4 26479 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑃𝐿𝑁) = (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃})) |
9 | 8 | eqeq1d 2612 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑃𝐿𝑁) = (𝐾↑𝑁) ↔ (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁))) |
10 | 2, 3, 5, 9 | syl3anc 1318 |
. 2
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑃𝐿𝑁) = (𝐾↑𝑁) ↔ (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁))) |
11 | | wwlknredwwlkn0 26255 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸))) |
12 | 11 | ex 449 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)))) |
13 | 12 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)))) |
14 | 13 | adantl 481 |
. . . . . . . . 9
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)))) |
15 | 14 | imp 444 |
. . . . . . . 8
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → ((𝑤‘0) = 𝑃 ↔ ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸))) |
16 | 15 | rabbidva 3163 |
. . . . . . 7
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ (𝑤‘0) = 𝑃} = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) |
17 | 16 | adantr 480 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ (𝑤‘0) = 𝑃} = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) |
18 | 17 | fveq2d 6107 |
. . . . 5
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ (𝑤‘0) = 𝑃}) = (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)})) |
19 | | simp2 1055 |
. . . . . . . . . . . . 13
⊢ (((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸) → (𝑦‘0) = 𝑃) |
20 | 19 | pm4.71ri 663 |
. . . . . . . . . . . 12
⊢ (((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸) ↔ ((𝑦‘0) = 𝑃 ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸))) |
21 | 20 | a1i 11 |
. . . . . . . . . . 11
⊢
((((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) ∧ 𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) → (((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸) ↔ ((𝑦‘0) = 𝑃 ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)))) |
22 | 21 | rexbidva 3031 |
. . . . . . . . . 10
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → (∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸) ↔ ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑦‘0) = 𝑃 ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)))) |
23 | | fveq1 6102 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑥‘0) = (𝑦‘0)) |
24 | 23 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((𝑥‘0) = 𝑃 ↔ (𝑦‘0) = 𝑃)) |
25 | 24 | rexrab 3337 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈
{𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑥‘0) = 𝑃} ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸) ↔ ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑦‘0) = 𝑃 ∧ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸))) |
26 | 22, 25 | syl6bbr 277 |
. . . . . . . . 9
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → (∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸) ↔ ∃𝑦 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑥‘0) = 𝑃} ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸))) |
27 | 26 | rabbidva 3163 |
. . . . . . . 8
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)} = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ∃𝑦 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑥‘0) = 𝑃} ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) |
28 | 27 | adantr 480 |
. . . . . . 7
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)} = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ∃𝑦 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑥‘0) = 𝑃} ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) |
29 | 28 | fveq2d 6107 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) = (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ∃𝑦 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑥‘0) = 𝑃} ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)})) |
30 | | simplr1 1096 |
. . . . . . 7
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → 𝑉 ∈ Fin) |
31 | | eqid 2610 |
. . . . . . . 8
⊢ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) = ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) |
32 | | eqid 2610 |
. . . . . . . 8
⊢ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑥‘0) = 𝑃} = {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑥‘0) = 𝑃} |
33 | 31, 32 | hashwwlkext 26274 |
. . . . . . 7
⊢ (𝑉 ∈ Fin →
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ∃𝑦 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑥‘0) = 𝑃} ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) = Σ𝑦 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑥‘0) = 𝑃} (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)})) |
34 | 30, 33 | syl 17 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ∃𝑦 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑥‘0) = 𝑃} ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) = Σ𝑦 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑥‘0) = 𝑃} (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)})) |
35 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑤 → (𝑥‘0) = (𝑤‘0)) |
36 | 35 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑥 = 𝑤 → ((𝑥‘0) = 𝑃 ↔ (𝑤‘0) = 𝑃)) |
37 | 36 | cbvrabv 3172 |
. . . . . . . 8
⊢ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑥‘0) = 𝑃} = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} |
38 | 37 | sumeq1i 14276 |
. . . . . . 7
⊢
Σ𝑦 ∈
{𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑥‘0) = 𝑃} (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) = Σ𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) |
39 | 38 | a1i 11 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → Σ𝑦 ∈ {𝑥 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑥‘0) = 𝑃} (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) = Σ𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)})) |
40 | 29, 34, 39 | 3eqtrd 2648 |
. . . . 5
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) = Σ𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)})) |
41 | | rusgranumwlklem0 26475 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} → {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)} = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) |
42 | 41 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} → {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)} = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) |
43 | 42 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) = (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)})) |
44 | 43 | adantl 481 |
. . . . . . . 8
⊢
((((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) = (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)})) |
45 | | elrabi 3328 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} → 𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) |
46 | 45 | adantl 481 |
. . . . . . . . 9
⊢
((((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) → 𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) |
47 | | wwlkexthasheq 26262 |
. . . . . . . . 9
⊢ (𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) = (#‘{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑦), 𝑛} ∈ ran 𝐸})) |
48 | 46, 47 | syl 17 |
. . . . . . . 8
⊢
((((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) = (#‘{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑦), 𝑛} ∈ ran 𝐸})) |
49 | | rusgraprop3 26470 |
. . . . . . . . . 10
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑝 ∈ 𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ ran 𝐸}) = 𝐾)) |
50 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑦 → (𝑤‘0) = (𝑦‘0)) |
51 | 50 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑦 → ((𝑤‘0) = 𝑃 ↔ (𝑦‘0) = 𝑃)) |
52 | 51 | elrab 3331 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} ↔ (𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑦‘0) = 𝑃)) |
53 | | wwlknimp 26215 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ ran 𝐸)) |
54 | 53 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑦‘0) = 𝑃) → (𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ ran 𝐸)) |
55 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑦 ∈ Word 𝑉) |
56 | | nn0p1gt0 11199 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ0
→ 0 < (𝑁 +
1)) |
57 | 56 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 0 <
(𝑁 + 1)) |
58 | 57 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 0 <
(𝑁 + 1)) |
59 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝑦) =
(𝑁 + 1) → (0 <
(#‘𝑦) ↔ 0 <
(𝑁 + 1))) |
60 | 59 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (0 <
(#‘𝑦) ↔ 0 <
(𝑁 + 1))) |
61 | 58, 60 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 0 <
(#‘𝑦)) |
62 | | hashle00 13049 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ Word 𝑉 → ((#‘𝑦) ≤ 0 ↔ 𝑦 = ∅)) |
63 | | lencl 13179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ Word 𝑉 → (#‘𝑦) ∈
ℕ0) |
64 | 63 | nn0red 11229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ Word 𝑉 → (#‘𝑦) ∈ ℝ) |
65 | | 0re 9919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ∈
ℝ |
66 | | lenlt 9995 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#‘𝑦) ∈
ℝ ∧ 0 ∈ ℝ) → ((#‘𝑦) ≤ 0 ↔ ¬ 0 < (#‘𝑦))) |
67 | 66 | bicomd 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#‘𝑦) ∈
ℝ ∧ 0 ∈ ℝ) → (¬ 0 < (#‘𝑦) ↔ (#‘𝑦) ≤ 0)) |
68 | 64, 65, 67 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ Word 𝑉 → (¬ 0 < (#‘𝑦) ↔ (#‘𝑦) ≤ 0)) |
69 | | nne 2786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
𝑦 ≠ ∅ ↔ 𝑦 = ∅) |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ Word 𝑉 → (¬ 𝑦 ≠ ∅ ↔ 𝑦 = ∅)) |
71 | 62, 68, 70 | 3bitr4rd 300 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ Word 𝑉 → (¬ 𝑦 ≠ ∅ ↔ ¬ 0 <
(#‘𝑦))) |
72 | 71 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (¬
𝑦 ≠ ∅ ↔ ¬
0 < (#‘𝑦))) |
73 | 72 | con4bid 306 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (𝑦 ≠ ∅ ↔ 0 <
(#‘𝑦))) |
74 | 61, 73 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑦 ≠ ∅) |
75 | 55, 74 | jca 553 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅)) |
76 | 75 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1)) → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅))) |
77 | 76 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ Word 𝑉 ∧ (#‘𝑦) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑦‘𝑖), (𝑦‘(𝑖 + 1))} ∈ ran 𝐸) → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅))) |
78 | 54, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ (𝑦‘0) = 𝑃) → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅))) |
79 | 52, 78 | sylbi 206 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅))) |
80 | 79 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅)) |
81 | | lswcl 13208 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ Word 𝑉 ∧ 𝑦 ≠ ∅) → ( lastS ‘𝑦) ∈ 𝑉) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ( lastS
‘𝑦) ∈ 𝑉) |
83 | 82 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ ((((𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ ∀𝑝 ∈ 𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ ran 𝐸}) = 𝐾) → ( lastS ‘𝑦) ∈ 𝑉) |
84 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = ( lastS ‘𝑦) → {𝑝, 𝑛} = {( lastS ‘𝑦), 𝑛}) |
85 | 84 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = ( lastS ‘𝑦) → ({𝑝, 𝑛} ∈ ran 𝐸 ↔ {( lastS ‘𝑦), 𝑛} ∈ ran 𝐸)) |
86 | 85 | rabbidv 3164 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = ( lastS ‘𝑦) → {𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ ran 𝐸} = {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑦), 𝑛} ∈ ran 𝐸}) |
87 | 86 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = ( lastS ‘𝑦) → (#‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ ran 𝐸}) = (#‘{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑦), 𝑛} ∈ ran 𝐸})) |
88 | 87 | eqeq1d 2612 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = ( lastS ‘𝑦) → ((#‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ ran 𝐸}) = 𝐾 ↔ (#‘{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑦), 𝑛} ∈ ran 𝐸}) = 𝐾)) |
89 | 88 | rspcva 3280 |
. . . . . . . . . . . . . 14
⊢ ((( lastS
‘𝑦) ∈ 𝑉 ∧ ∀𝑝 ∈ 𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ ran 𝐸}) = 𝐾) → (#‘{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑦), 𝑛} ∈ ran 𝐸}) = 𝐾) |
90 | 83, 89 | sylancom 698 |
. . . . . . . . . . . . 13
⊢ ((((𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ ∀𝑝 ∈ 𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ ran 𝐸}) = 𝐾) → (#‘{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑦), 𝑛} ∈ ran 𝐸}) = 𝐾) |
91 | 90 | exp41 636 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
((#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁) → (∀𝑝 ∈ 𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ ran 𝐸}) = 𝐾 → (#‘{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑦), 𝑛} ∈ ran 𝐸}) = 𝐾)))) |
92 | 91 | com14 94 |
. . . . . . . . . . 11
⊢
(∀𝑝 ∈
𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ ran 𝐸}) = 𝐾 → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
((#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁) → (𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} → (#‘{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑦), 𝑛} ∈ ran 𝐸}) = 𝐾)))) |
93 | 92 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑝 ∈ 𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ ran 𝐸}) = 𝐾) → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
((#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁) → (𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} → (#‘{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑦), 𝑛} ∈ ran 𝐸}) = 𝐾)))) |
94 | 49, 93 | syl 17 |
. . . . . . . . 9
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
((#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁) → (𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} → (#‘{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑦), 𝑛} ∈ ran 𝐸}) = 𝐾)))) |
95 | 94 | imp41 617 |
. . . . . . . 8
⊢
((((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) → (#‘{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑦), 𝑛} ∈ ran 𝐸}) = 𝐾) |
96 | 44, 48, 95 | 3eqtrd 2648 |
. . . . . . 7
⊢
((((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) ∧ 𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) = 𝐾) |
97 | 96 | sumeq2dv 14281 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → Σ𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) = Σ𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}𝐾) |
98 | | oveq1 6556 |
. . . . . . . 8
⊢
((#‘{𝑤 ∈
((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁) → ((#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) · 𝐾) = ((𝐾↑𝑁) · 𝐾)) |
99 | 98 | adantl 481 |
. . . . . . 7
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → ((#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) · 𝐾) = ((𝐾↑𝑁) · 𝐾)) |
100 | | wwlknfi 26266 |
. . . . . . . . . . 11
⊢ (𝑉 ∈ Fin → ((𝑉 WWalksN 𝐸)‘𝑁) ∈ Fin) |
101 | 100 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑉 WWalksN 𝐸)‘𝑁) ∈ Fin) |
102 | 101 | ad2antlr 759 |
. . . . . . . . 9
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → ((𝑉 WWalksN 𝐸)‘𝑁) ∈ Fin) |
103 | | rabfi 8070 |
. . . . . . . . 9
⊢ (((𝑉 WWalksN 𝐸)‘𝑁) ∈ Fin → {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} ∈ Fin) |
104 | 102, 103 | syl 17 |
. . . . . . . 8
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} ∈ Fin) |
105 | | rusgraprop 26456 |
. . . . . . . . . 10
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑝 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑝) = 𝐾)) |
106 | | nn0cn 11179 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℂ) |
107 | 106 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑝 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑝) = 𝐾) → 𝐾 ∈ ℂ) |
108 | 105, 107 | syl 17 |
. . . . . . . . 9
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝐾 ∈ ℂ) |
109 | 108 | ad2antrr 758 |
. . . . . . . 8
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → 𝐾 ∈ ℂ) |
110 | | fsumconst 14364 |
. . . . . . . 8
⊢ (({𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} ∈ Fin ∧ 𝐾 ∈ ℂ) → Σ𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}𝐾 = ((#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) · 𝐾)) |
111 | 104, 109,
110 | syl2anc 691 |
. . . . . . 7
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → Σ𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}𝐾 = ((#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) · 𝐾)) |
112 | | expp1 12729 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝐾↑(𝑁 + 1)) = ((𝐾↑𝑁) · 𝐾)) |
113 | 108, 4, 112 | syl2an 493 |
. . . . . . . 8
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (𝐾↑(𝑁 + 1)) = ((𝐾↑𝑁) · 𝐾)) |
114 | 113 | adantr 480 |
. . . . . . 7
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (𝐾↑(𝑁 + 1)) = ((𝐾↑𝑁) · 𝐾)) |
115 | 99, 111, 114 | 3eqtr4d 2654 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → Σ𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}𝐾 = (𝐾↑(𝑁 + 1))) |
116 | 97, 115 | eqtrd 2644 |
. . . . 5
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → Σ𝑦 ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑤)} ∈ ran 𝐸)}) = (𝐾↑(𝑁 + 1))) |
117 | 18, 40, 116 | 3eqtrd 2648 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1))) |
118 | | peano2nn0 11210 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
119 | 118 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ∈
ℕ0) |
120 | 119 | adantl 481 |
. . . . . 6
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈
ℕ0) |
121 | 6, 7 | rusgranumwlklem4 26479 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉 ∧ (𝑁 + 1) ∈ ℕ0) →
(𝑃𝐿(𝑁 + 1)) = (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ (𝑤‘0) = 𝑃})) |
122 | 121 | eqeq1d 2612 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉 ∧ (𝑁 + 1) ∈ ℕ0) →
((𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)) ↔ (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1)))) |
123 | 2, 3, 120, 122 | syl3anc 1318 |
. . . . 5
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)) ↔ (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1)))) |
124 | 123 | adantr 480 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → ((𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)) ↔ (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑(𝑁 + 1)))) |
125 | 117, 124 | mpbird 246 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧
(#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) → (𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1))) |
126 | 125 | ex 449 |
. 2
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
((#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁) → (𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)))) |
127 | 10, 126 | sylbid 229 |
1
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑃𝐿𝑁) = (𝐾↑𝑁) → (𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)))) |