| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝑃𝐿𝑥) = (𝑃𝐿0)) |
| 2 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝐾↑𝑥) = (𝐾↑0)) |
| 3 | 1, 2 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑥 = 0 → ((𝑃𝐿𝑥) = (𝐾↑𝑥) ↔ (𝑃𝐿0) = (𝐾↑0))) |
| 4 | 3 | imbi2d 340 |
. . . . . 6
⊢ (𝑥 = 0 → ((((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → (𝑃𝐿𝑥) = (𝐾↑𝑥)) ↔ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → (𝑃𝐿0) = (𝐾↑0)))) |
| 5 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑃𝐿𝑥) = (𝑃𝐿𝑦)) |
| 6 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐾↑𝑥) = (𝐾↑𝑦)) |
| 7 | 5, 6 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑃𝐿𝑥) = (𝐾↑𝑥) ↔ (𝑃𝐿𝑦) = (𝐾↑𝑦))) |
| 8 | 7 | imbi2d 340 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → (𝑃𝐿𝑥) = (𝐾↑𝑥)) ↔ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → (𝑃𝐿𝑦) = (𝐾↑𝑦)))) |
| 9 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 1) → (𝑃𝐿𝑥) = (𝑃𝐿(𝑦 + 1))) |
| 10 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 1) → (𝐾↑𝑥) = (𝐾↑(𝑦 + 1))) |
| 11 | 9, 10 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → ((𝑃𝐿𝑥) = (𝐾↑𝑥) ↔ (𝑃𝐿(𝑦 + 1)) = (𝐾↑(𝑦 + 1)))) |
| 12 | 11 | imbi2d 340 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → ((((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → (𝑃𝐿𝑥) = (𝐾↑𝑥)) ↔ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → (𝑃𝐿(𝑦 + 1)) = (𝐾↑(𝑦 + 1))))) |
| 13 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝑃𝐿𝑥) = (𝑃𝐿𝑁)) |
| 14 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝐾↑𝑥) = (𝐾↑𝑁)) |
| 15 | 13, 14 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → ((𝑃𝐿𝑥) = (𝐾↑𝑥) ↔ (𝑃𝐿𝑁) = (𝐾↑𝑁))) |
| 16 | 15 | imbi2d 340 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → (𝑃𝐿𝑥) = (𝐾↑𝑥)) ↔ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → (𝑃𝐿𝑁) = (𝐾↑𝑁)))) |
| 17 | | rusgrusgr 29582 |
. . . . . . . . 9
⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph) |
| 18 | | usgruspgr 29197 |
. . . . . . . . 9
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
USPGraph) |
| 19 | 17, 18 | syl 17 |
. . . . . . . 8
⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USPGraph) |
| 20 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) → 𝑃 ∈ 𝑉) |
| 21 | | rusgrnumwwlk.v |
. . . . . . . . 9
⊢ 𝑉 = (Vtx‘𝐺) |
| 22 | | rusgrnumwwlk.l |
. . . . . . . . 9
⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦
(♯‘{𝑤 ∈
(𝑛 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})) |
| 23 | 21, 22 | rusgrnumwwlkb0 29991 |
. . . . . . . 8
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉) → (𝑃𝐿0) = 1) |
| 24 | 19, 20, 23 | syl2anr 597 |
. . . . . . 7
⊢ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → (𝑃𝐿0) = 1) |
| 25 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) → 𝑉 ∈ Fin) |
| 26 | 25, 17 | anim12ci 614 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin)) |
| 27 | 21 | isfusgr 29335 |
. . . . . . . . . 10
⊢ (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin)) |
| 28 | 26, 27 | sylibr 234 |
. . . . . . . . 9
⊢ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → 𝐺 ∈ FinUSGraph) |
| 29 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → 𝐺 RegUSGraph 𝐾) |
| 30 | | ne0i 4341 |
. . . . . . . . . 10
⊢ (𝑃 ∈ 𝑉 → 𝑉 ≠ ∅) |
| 31 | 30 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → 𝑉 ≠ ∅) |
| 32 | 21 | frusgrnn0 29589 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅) → 𝐾 ∈
ℕ0) |
| 33 | 32 | nn0cnd 12589 |
. . . . . . . . 9
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅) → 𝐾 ∈ ℂ) |
| 34 | 28, 29, 31, 33 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → 𝐾 ∈ ℂ) |
| 35 | 34 | exp0d 14180 |
. . . . . . 7
⊢ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → (𝐾↑0) = 1) |
| 36 | 24, 35 | eqtr4d 2780 |
. . . . . 6
⊢ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → (𝑃𝐿0) = (𝐾↑0)) |
| 37 | | simpl 482 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉)) |
| 38 | 37 | anim1i 615 |
. . . . . . . . . 10
⊢ ((((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) ∧ 𝑦 ∈ ℕ0) → ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝑦 ∈
ℕ0)) |
| 39 | | df-3an 1089 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑦 ∈ ℕ0) ↔ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝑦 ∈
ℕ0)) |
| 40 | 38, 39 | sylibr 234 |
. . . . . . . . 9
⊢ ((((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) ∧ 𝑦 ∈ ℕ0) → (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑦 ∈
ℕ0)) |
| 41 | 21, 22 | rusgrnumwwlks 29994 |
. . . . . . . . 9
⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑦 ∈ ℕ0)) → ((𝑃𝐿𝑦) = (𝐾↑𝑦) → (𝑃𝐿(𝑦 + 1)) = (𝐾↑(𝑦 + 1)))) |
| 42 | 29, 40, 41 | syl2an2r 685 |
. . . . . . . 8
⊢ ((((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) ∧ 𝑦 ∈ ℕ0) → ((𝑃𝐿𝑦) = (𝐾↑𝑦) → (𝑃𝐿(𝑦 + 1)) = (𝐾↑(𝑦 + 1)))) |
| 43 | 42 | expcom 413 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ0
→ (((𝑉 ∈ Fin
∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → ((𝑃𝐿𝑦) = (𝐾↑𝑦) → (𝑃𝐿(𝑦 + 1)) = (𝐾↑(𝑦 + 1))))) |
| 44 | 43 | a2d 29 |
. . . . . 6
⊢ (𝑦 ∈ ℕ0
→ ((((𝑉 ∈ Fin
∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → (𝑃𝐿𝑦) = (𝐾↑𝑦)) → (((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → (𝑃𝐿(𝑦 + 1)) = (𝐾↑(𝑦 + 1))))) |
| 45 | 4, 8, 12, 16, 36, 44 | nn0ind 12713 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (((𝑉 ∈ Fin
∧ 𝑃 ∈ 𝑉) ∧ 𝐺 RegUSGraph 𝐾) → (𝑃𝐿𝑁) = (𝐾↑𝑁))) |
| 46 | 45 | expd 415 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ((𝑉 ∈ Fin ∧
𝑃 ∈ 𝑉) → (𝐺 RegUSGraph 𝐾 → (𝑃𝐿𝑁) = (𝐾↑𝑁)))) |
| 47 | 46 | com12 32 |
. . 3
⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉) → (𝑁 ∈ ℕ0 → (𝐺 RegUSGraph 𝐾 → (𝑃𝐿𝑁) = (𝐾↑𝑁)))) |
| 48 | 47 | 3impia 1118 |
. 2
⊢ ((𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝐺 RegUSGraph 𝐾 → (𝑃𝐿𝑁) = (𝐾↑𝑁))) |
| 49 | 48 | impcom 407 |
1
⊢ ((𝐺 RegUSGraph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (𝑃𝐿𝑁) = (𝐾↑𝑁)) |