Step | Hyp | Ref
| Expression |
1 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝑃𝐿𝑥) = (𝑃𝐿0)) |
2 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝐾↑𝑥) = (𝐾↑0)) |
3 | 1, 2 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑥 = 0 → ((𝑃𝐿𝑥) = (𝐾↑𝑥) ↔ (𝑃𝐿0) = (𝐾↑0))) |
4 | 3 | imbi2d 329 |
. . . . . 6
⊢ (𝑥 = 0 → ((((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝑃𝐿𝑥) = (𝐾↑𝑥)) ↔ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝑃𝐿0) = (𝐾↑0)))) |
5 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑃𝐿𝑥) = (𝑃𝐿𝑦)) |
6 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐾↑𝑥) = (𝐾↑𝑦)) |
7 | 5, 6 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑃𝐿𝑥) = (𝐾↑𝑥) ↔ (𝑃𝐿𝑦) = (𝐾↑𝑦))) |
8 | 7 | imbi2d 329 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝑃𝐿𝑥) = (𝐾↑𝑥)) ↔ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝑃𝐿𝑦) = (𝐾↑𝑦)))) |
9 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 1) → (𝑃𝐿𝑥) = (𝑃𝐿(𝑦 + 1))) |
10 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 1) → (𝐾↑𝑥) = (𝐾↑(𝑦 + 1))) |
11 | 9, 10 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → ((𝑃𝐿𝑥) = (𝐾↑𝑥) ↔ (𝑃𝐿(𝑦 + 1)) = (𝐾↑(𝑦 + 1)))) |
12 | 11 | imbi2d 329 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → ((((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝑃𝐿𝑥) = (𝐾↑𝑥)) ↔ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝑃𝐿(𝑦 + 1)) = (𝐾↑(𝑦 + 1))))) |
13 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝑃𝐿𝑥) = (𝑃𝐿𝑁)) |
14 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝐾↑𝑥) = (𝐾↑𝑁)) |
15 | 13, 14 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → ((𝑃𝐿𝑥) = (𝐾↑𝑥) ↔ (𝑃𝐿𝑁) = (𝐾↑𝑁))) |
16 | 15 | imbi2d 329 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝑃𝐿𝑥) = (𝐾↑𝑥)) ↔ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝑃𝐿𝑁) = (𝐾↑𝑁)))) |
17 | | rusisusgra 26458 |
. . . . . . . 8
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝑉 USGrph 𝐸) |
18 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) → 𝑃 ∈ 𝑉) |
19 | | rusgranumwlk.w |
. . . . . . . . 9
⊢ 𝑊 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑛}) |
20 | | rusgranumwlk.l |
. . . . . . . . 9
⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦
(#‘{𝑤 ∈ (𝑊‘𝑛) ∣ ((2nd ‘𝑤)‘0) = 𝑣})) |
21 | 19, 20 | rusgranumwlkb0 26480 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉) → (𝑃𝐿0) = 1) |
22 | 17, 18, 21 | syl2anr 494 |
. . . . . . 7
⊢ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝑃𝐿0) = 1) |
23 | | rusgraprop 26456 |
. . . . . . . . . 10
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑖 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑖) = 𝐾)) |
24 | | nn0cn 11179 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℂ) |
25 | 24 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑖 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑖) = 𝐾) → 𝐾 ∈ ℂ) |
26 | | exp0 12726 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℂ → (𝐾↑0) = 1) |
27 | 23, 25, 26 | 3syl 18 |
. . . . . . . . 9
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝐾↑0) = 1) |
28 | 27 | eqcomd 2616 |
. . . . . . . 8
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 1 = (𝐾↑0)) |
29 | 28 | adantl 481 |
. . . . . . 7
⊢ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → 1 = (𝐾↑0)) |
30 | 22, 29 | eqtrd 2644 |
. . . . . 6
⊢ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝑃𝐿0) = (𝐾↑0)) |
31 | | simplr 788 |
. . . . . . . . 9
⊢ ((((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ 𝑦 ∈ ℕ0) →
〈𝑉, 𝐸〉 RegUSGrph 𝐾) |
32 | | simpl 472 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉)) |
33 | 32 | anim1i 590 |
. . . . . . . . . 10
⊢ ((((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ 𝑦 ∈ ℕ0) → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝑦 ∈
ℕ0)) |
34 | | df-3an 1033 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑦 ∈ ℕ0) ↔ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝑦 ∈
ℕ0)) |
35 | 33, 34 | sylibr 223 |
. . . . . . . . 9
⊢ ((((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ 𝑦 ∈ ℕ0) → (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑦 ∈
ℕ0)) |
36 | 19, 20 | rusgranumwlks 26483 |
. . . . . . . . 9
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑦 ∈ ℕ0)) → ((𝑃𝐿𝑦) = (𝐾↑𝑦) → (𝑃𝐿(𝑦 + 1)) = (𝐾↑(𝑦 + 1)))) |
37 | 31, 35, 36 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ 𝑦 ∈ ℕ0) → ((𝑃𝐿𝑦) = (𝐾↑𝑦) → (𝑃𝐿(𝑦 + 1)) = (𝐾↑(𝑦 + 1)))) |
38 | 37 | expcom 450 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ0
→ (((𝑉 ∈ Fin
∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → ((𝑃𝐿𝑦) = (𝐾↑𝑦) → (𝑃𝐿(𝑦 + 1)) = (𝐾↑(𝑦 + 1))))) |
39 | 38 | a2d 29 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0
→ ((((𝑉 ∈ Fin
∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝑃𝐿𝑦) = (𝐾↑𝑦)) → (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝑃𝐿(𝑦 + 1)) = (𝐾↑(𝑦 + 1))))) |
40 | 4, 8, 12, 16, 30, 39 | nn0ind 11348 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (((𝑉 ∈ Fin
∧ 𝑃 ∈ 𝑉) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝑃𝐿𝑁) = (𝐾↑𝑁))) |
41 | 40 | expd 451 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ((𝑉 ∈ Fin ∧
𝑃 ∈ 𝑉) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑃𝐿𝑁) = (𝐾↑𝑁)))) |
42 | 41 | com12 32 |
. . 3
⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) → (𝑁 ∈ ℕ0 →
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑃𝐿𝑁) = (𝐾↑𝑁)))) |
43 | 42 | 3impia 1253 |
. 2
⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑃𝐿𝑁) = (𝐾↑𝑁))) |
44 | 43 | impcom 445 |
1
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (𝑃𝐿𝑁) = (𝐾↑𝑁)) |