Step | Hyp | Ref
| Expression |
1 | | ovex 6678 |
. . 3
⊢ (𝑋𝐶𝑁) ∈ V |
2 | | rusgrusgr 26460 |
. . . . 5
⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph ) |
3 | 2 | ad2antlr 763 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝐺 ∈ USGraph
) |
4 | | simprl 794 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝑋 ∈ 𝑉) |
5 | | simprr 796 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝑁 ∈
(ℤ≥‘3)) |
6 | | extwwlkfab.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
7 | | extwwlkfab.f |
. . . . 5
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣}) |
8 | | extwwlkfab.c |
. . . . 5
⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))}) |
9 | 6, 7, 8 | numclwlk1lem2 27230 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ∃𝑓 𝑓:(𝑋𝐶𝑁)–1-1-onto→((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋))) |
10 | 3, 4, 5, 9 | syl3anc 1326 |
. . 3
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ ∃𝑓 𝑓:(𝑋𝐶𝑁)–1-1-onto→((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋))) |
11 | | hasheqf1oi 13140 |
. . 3
⊢ ((𝑋𝐶𝑁) ∈ V → (∃𝑓 𝑓:(𝑋𝐶𝑁)–1-1-onto→((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋)) → (#‘(𝑋𝐶𝑁)) = (#‘((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋))))) |
12 | 1, 10, 11 | mpsyl 68 |
. 2
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (#‘(𝑋𝐶𝑁)) = (#‘((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋)))) |
13 | | simpll 790 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝑉 ∈
Fin) |
14 | | uz3m2nn 11731 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ ℕ) |
15 | 14 | adantl 482 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
ℕ) |
16 | 15 | adantl 482 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑁 − 2) ∈
ℕ) |
17 | 7, 6 | numclwwlkffin 27214 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ (𝑁 − 2) ∈ ℕ) → (𝑋𝐹(𝑁 − 2)) ∈ Fin) |
18 | 13, 4, 16, 17 | syl3anc 1326 |
. . 3
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑋𝐹(𝑁 − 2)) ∈ Fin) |
19 | 6 | finrusgrfusgr 26461 |
. . . . . . 7
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) → 𝐺 ∈ FinUSGraph ) |
20 | 19 | ancoms 469 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → 𝐺 ∈ FinUSGraph ) |
21 | | fusgrfis 26222 |
. . . . . 6
⊢ (𝐺 ∈ FinUSGraph →
(Edg‘𝐺) ∈
Fin) |
22 | 20, 21 | syl 17 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → (Edg‘𝐺) ∈ Fin) |
23 | 22 | adantr 481 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (Edg‘𝐺) ∈
Fin) |
24 | | eqid 2622 |
. . . . 5
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
25 | 6, 24 | nbusgrfi 26276 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧
(Edg‘𝐺) ∈ Fin
∧ 𝑋 ∈ 𝑉) → (𝐺 NeighbVtx 𝑋) ∈ Fin) |
26 | 3, 23, 4, 25 | syl3anc 1326 |
. . 3
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝐺 NeighbVtx 𝑋) ∈ Fin) |
27 | | hashxp 13221 |
. . 3
⊢ (((𝑋𝐹(𝑁 − 2)) ∈ Fin ∧ (𝐺 NeighbVtx 𝑋) ∈ Fin) → (#‘((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋))) = ((#‘(𝑋𝐹(𝑁 − 2))) · (#‘(𝐺 NeighbVtx 𝑋)))) |
28 | 18, 26, 27 | syl2anc 693 |
. 2
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (#‘((𝑋𝐹(𝑁 − 2)) × (𝐺 NeighbVtx 𝑋))) = ((#‘(𝑋𝐹(𝑁 − 2))) · (#‘(𝐺 NeighbVtx 𝑋)))) |
29 | 6 | rusgrpropnb 26479 |
. . . . . . . . 9
⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0*
∧ ∀𝑥 ∈
𝑉 (#‘(𝐺 NeighbVtx 𝑥)) = 𝐾)) |
30 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑋 → (𝐺 NeighbVtx 𝑥) = (𝐺 NeighbVtx 𝑋)) |
31 | 30 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → (#‘(𝐺 NeighbVtx 𝑥)) = (#‘(𝐺 NeighbVtx 𝑋))) |
32 | 31 | eqeq1d 2624 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → ((#‘(𝐺 NeighbVtx 𝑥)) = 𝐾 ↔ (#‘(𝐺 NeighbVtx 𝑋)) = 𝐾)) |
33 | 32 | rspccv 3306 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑉 (#‘(𝐺 NeighbVtx 𝑥)) = 𝐾 → (𝑋 ∈ 𝑉 → (#‘(𝐺 NeighbVtx 𝑋)) = 𝐾)) |
34 | 33 | 3ad2ant3 1084 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USGraph ∧ 𝐾 ∈
ℕ0* ∧ ∀𝑥 ∈ 𝑉 (#‘(𝐺 NeighbVtx 𝑥)) = 𝐾) → (𝑋 ∈ 𝑉 → (#‘(𝐺 NeighbVtx 𝑋)) = 𝐾)) |
35 | 29, 34 | syl 17 |
. . . . . . . 8
⊢ (𝐺 RegUSGraph 𝐾 → (𝑋 ∈ 𝑉 → (#‘(𝐺 NeighbVtx 𝑋)) = 𝐾)) |
36 | 35 | adantl 482 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → (𝑋 ∈ 𝑉 → (#‘(𝐺 NeighbVtx 𝑋)) = 𝐾)) |
37 | 36 | com12 32 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) → (#‘(𝐺 NeighbVtx 𝑋)) = 𝐾)) |
38 | 37 | adantr 481 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑉 ∈ Fin ∧
𝐺 RegUSGraph 𝐾) → (#‘(𝐺 NeighbVtx 𝑋)) = 𝐾)) |
39 | 38 | impcom 446 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (#‘(𝐺
NeighbVtx 𝑋)) = 𝐾) |
40 | 39 | oveq2d 6666 |
. . 3
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ ((#‘(𝑋𝐹(𝑁 − 2))) · (#‘(𝐺 NeighbVtx 𝑋))) = ((#‘(𝑋𝐹(𝑁 − 2))) · 𝐾)) |
41 | | hashcl 13147 |
. . . . 5
⊢ ((𝑋𝐹(𝑁 − 2)) ∈ Fin →
(#‘(𝑋𝐹(𝑁 − 2))) ∈
ℕ0) |
42 | | nn0cn 11302 |
. . . . 5
⊢
((#‘(𝑋𝐹(𝑁 − 2))) ∈ ℕ0
→ (#‘(𝑋𝐹(𝑁 − 2))) ∈
ℂ) |
43 | 18, 41, 42 | 3syl 18 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (#‘(𝑋𝐹(𝑁 − 2))) ∈
ℂ) |
44 | 20 | adantr 481 |
. . . . . 6
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝐺 ∈ FinUSGraph
) |
45 | | simplr 792 |
. . . . . 6
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝐺 RegUSGraph 𝐾) |
46 | | ne0i 3921 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → 𝑉 ≠ ∅) |
47 | 46 | adantr 481 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑉 ≠
∅) |
48 | 47 | adantl 482 |
. . . . . 6
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝑉 ≠
∅) |
49 | 6 | frusgrnn0 26467 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅) → 𝐾 ∈
ℕ0) |
50 | 44, 45, 48, 49 | syl3anc 1326 |
. . . . 5
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝐾 ∈
ℕ0) |
51 | 50 | nn0cnd 11353 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝐾 ∈
ℂ) |
52 | 43, 51 | mulcomd 10061 |
. . 3
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ ((#‘(𝑋𝐹(𝑁 − 2))) · 𝐾) = (𝐾 · (#‘(𝑋𝐹(𝑁 − 2))))) |
53 | 40, 52 | eqtrd 2656 |
. 2
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ ((#‘(𝑋𝐹(𝑁 − 2))) · (#‘(𝐺 NeighbVtx 𝑋))) = (𝐾 · (#‘(𝑋𝐹(𝑁 − 2))))) |
54 | 12, 28, 53 | 3eqtrd 2660 |
1
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (#‘(𝑋𝐶𝑁)) = (𝐾 · (#‘(𝑋𝐹(𝑁 − 2))))) |