Step | Hyp | Ref
| Expression |
1 | | ovex 6577 |
. . 3
⊢ (𝑋𝐺𝑁) ∈ V |
2 | | rusisusgra 26458 |
. . . . 5
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝑉 USGrph 𝐸) |
3 | 2 | ad2antlr 759 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝑉 USGrph 𝐸) |
4 | | simprl 790 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝑋 ∈ 𝑉) |
5 | | simpr 476 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑁 ∈
(ℤ≥‘3)) |
6 | 5 | adantl 481 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝑁 ∈
(ℤ≥‘3)) |
7 | | numclwwlk.c |
. . . . 5
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛)) |
8 | | numclwwlk.f |
. . . . 5
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝐶‘𝑛) ∣ (𝑤‘0) = 𝑣}) |
9 | | numclwwlk.g |
. . . . 5
⊢ 𝐺 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝐶‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))}) |
10 | 7, 8, 9 | numclwlk1lem2 26624 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ∃𝑓 𝑓:(𝑋𝐺𝑁)–1-1-onto→((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋))) |
11 | 3, 4, 6, 10 | syl3anc 1318 |
. . 3
⊢ (((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ ∃𝑓 𝑓:(𝑋𝐺𝑁)–1-1-onto→((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋))) |
12 | | hasheqf1oi 13002 |
. . 3
⊢ ((𝑋𝐺𝑁) ∈ V → (∃𝑓 𝑓:(𝑋𝐺𝑁)–1-1-onto→((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋)) → (#‘(𝑋𝐺𝑁)) = (#‘((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋))))) |
13 | 1, 11, 12 | mpsyl 66 |
. 2
⊢ (((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (#‘(𝑋𝐺𝑁)) = (#‘((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋)))) |
14 | | usgrav 25867 |
. . . . . 6
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
15 | | simpr 476 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → 𝐸 ∈ V) |
16 | 2, 14, 15 | 3syl 18 |
. . . . 5
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝐸 ∈ V) |
17 | 16 | anim2i 591 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝑉 ∈ Fin ∧ 𝐸 ∈ V)) |
18 | | uzuzle23 11605 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘2)) |
19 | | uznn0sub 11595 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 2) ∈
ℕ0) |
20 | 18, 19 | syl 17 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈
ℕ0) |
21 | 20 | anim2i 591 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋 ∈ 𝑉 ∧ (𝑁 − 2) ∈
ℕ0)) |
22 | 7, 8 | numclwwlkffin 26609 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ (𝑁 − 2) ∈ ℕ0))
→ (𝑋𝐹(𝑁 − 2)) ∈ Fin) |
23 | 17, 21, 22 | syl2an 493 |
. . 3
⊢ (((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑋𝐹(𝑁 − 2)) ∈ Fin) |
24 | 2 | anim1i 590 |
. . . . . . 7
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) → (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin)) |
25 | 24 | ancoms 468 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin)) |
26 | | usgrafis 25944 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) → 𝐸 ∈ Fin) |
27 | 25, 26 | syl 17 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → 𝐸 ∈ Fin) |
28 | 27 | adantr 480 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝐸 ∈
Fin) |
29 | | nbusgrafi 25977 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → (〈𝑉, 𝐸〉 Neighbors 𝑋) ∈ Fin) |
30 | 3, 4, 28, 29 | syl3anc 1318 |
. . 3
⊢ (((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (〈𝑉, 𝐸〉 Neighbors 𝑋) ∈ Fin) |
31 | | hashxp 13081 |
. . 3
⊢ (((𝑋𝐹(𝑁 − 2)) ∈ Fin ∧ (〈𝑉, 𝐸〉 Neighbors 𝑋) ∈ Fin) → (#‘((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋))) = ((#‘(𝑋𝐹(𝑁 − 2))) · (#‘(〈𝑉, 𝐸〉 Neighbors 𝑋)))) |
32 | 23, 30, 31 | syl2anc 691 |
. 2
⊢ (((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (#‘((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋))) = ((#‘(𝑋𝐹(𝑁 − 2))) · (#‘(〈𝑉, 𝐸〉 Neighbors 𝑋)))) |
33 | | rusgraprop2 26469 |
. . . . . . . . 9
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑥 ∈ 𝑉 (#‘(〈𝑉, 𝐸〉 Neighbors 𝑥)) = 𝐾)) |
34 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑋 → (〈𝑉, 𝐸〉 Neighbors 𝑥) = (〈𝑉, 𝐸〉 Neighbors 𝑋)) |
35 | 34 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑥)) = (#‘(〈𝑉, 𝐸〉 Neighbors 𝑋))) |
36 | 35 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑥)) = 𝐾 ↔ (#‘(〈𝑉, 𝐸〉 Neighbors 𝑋)) = 𝐾)) |
37 | 36 | rspccv 3279 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑉 (#‘(〈𝑉, 𝐸〉 Neighbors 𝑥)) = 𝐾 → (𝑋 ∈ 𝑉 → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑋)) = 𝐾)) |
38 | 37 | 3ad2ant3 1077 |
. . . . . . . . 9
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑥 ∈ 𝑉 (#‘(〈𝑉, 𝐸〉 Neighbors 𝑥)) = 𝐾) → (𝑋 ∈ 𝑉 → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑋)) = 𝐾)) |
39 | 33, 38 | syl 17 |
. . . . . . . 8
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑋 ∈ 𝑉 → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑋)) = 𝐾)) |
40 | 39 | adantl 481 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝑋 ∈ 𝑉 → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑋)) = 𝐾)) |
41 | 40 | com12 32 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → ((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑋)) = 𝐾)) |
42 | 41 | adantr 480 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑉 ∈ Fin ∧
〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑋)) = 𝐾)) |
43 | 42 | impcom 445 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (#‘(〈𝑉,
𝐸〉 Neighbors 𝑋)) = 𝐾) |
44 | 43 | oveq2d 6565 |
. . 3
⊢ (((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ ((#‘(𝑋𝐹(𝑁 − 2))) · (#‘(〈𝑉, 𝐸〉 Neighbors 𝑋))) = ((#‘(𝑋𝐹(𝑁 − 2))) · 𝐾)) |
45 | | hashcl 13009 |
. . . . 5
⊢ ((𝑋𝐹(𝑁 − 2)) ∈ Fin →
(#‘(𝑋𝐹(𝑁 − 2))) ∈
ℕ0) |
46 | | nn0cn 11179 |
. . . . 5
⊢
((#‘(𝑋𝐹(𝑁 − 2))) ∈ ℕ0
→ (#‘(𝑋𝐹(𝑁 − 2))) ∈
ℂ) |
47 | 23, 45, 46 | 3syl 18 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (#‘(𝑋𝐹(𝑁 − 2))) ∈
ℂ) |
48 | | nn0cn 11179 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℂ) |
49 | 48 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑥 ∈ 𝑉 (#‘(〈𝑉, 𝐸〉 Neighbors 𝑥)) = 𝐾) → 𝐾 ∈ ℂ) |
50 | 33, 49 | syl 17 |
. . . . 5
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝐾 ∈ ℂ) |
51 | 50 | ad2antlr 759 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝐾 ∈
ℂ) |
52 | 47, 51 | mulcomd 9940 |
. . 3
⊢ (((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ ((#‘(𝑋𝐹(𝑁 − 2))) · 𝐾) = (𝐾 · (#‘(𝑋𝐹(𝑁 − 2))))) |
53 | 44, 52 | eqtrd 2644 |
. 2
⊢ (((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ ((#‘(𝑋𝐹(𝑁 − 2))) · (#‘(〈𝑉, 𝐸〉 Neighbors 𝑋))) = (𝐾 · (#‘(𝑋𝐹(𝑁 − 2))))) |
54 | 13, 32, 53 | 3eqtrd 2648 |
1
⊢ (((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (#‘(𝑋𝐺𝑁)) = (𝐾 · (#‘(𝑋𝐹(𝑁 − 2))))) |