Step | Hyp | Ref
| Expression |
1 | | fusgreghash2wsp.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑠 = 𝑡 → (𝑠‘1) = (𝑡‘1)) |
3 | 2 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑠 = 𝑡 → ((𝑠‘1) = 𝑎 ↔ (𝑡‘1) = 𝑎)) |
4 | 3 | cbvrabv 3199 |
. . . . . . 7
⊢ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎} = {𝑡 ∈ (2 WSPathsN 𝐺) ∣ (𝑡‘1) = 𝑎} |
5 | 4 | mpteq2i 4741 |
. . . . . 6
⊢ (𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎}) = (𝑎 ∈ 𝑉 ↦ {𝑡 ∈ (2 WSPathsN 𝐺) ∣ (𝑡‘1) = 𝑎}) |
6 | 1, 5 | fusgreg2wsp 27200 |
. . . . 5
⊢ (𝐺 ∈ FinUSGraph → (2
WSPathsN 𝐺) = ∪ 𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) |
7 | 6 | ad2antrr 762 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (2 WSPathsN 𝐺) = ∪
𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) |
8 | 7 | fveq2d 6195 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (#‘(2 WSPathsN 𝐺)) = (#‘∪ 𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦))) |
9 | 1 | fusgrvtxfi 26211 |
. . . . 5
⊢ (𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin) |
10 | | eqeq2 2633 |
. . . . . . . . 9
⊢ (𝑎 = 𝑦 → ((𝑠‘1) = 𝑎 ↔ (𝑠‘1) = 𝑦)) |
11 | 10 | rabbidv 3189 |
. . . . . . . 8
⊢ (𝑎 = 𝑦 → {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎} = {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦}) |
12 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎}) = (𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎}) |
13 | | ovex 6678 |
. . . . . . . . 9
⊢ (2
WSPathsN 𝐺) ∈
V |
14 | 13 | rabex 4813 |
. . . . . . . 8
⊢ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦} ∈ V |
15 | 11, 12, 14 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑦 ∈ 𝑉 → ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦) = {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦}) |
16 | 15 | adantl 482 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑦 ∈ 𝑉) → ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦) = {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦}) |
17 | | eqid 2622 |
. . . . . . . . 9
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
18 | 17 | fusgrvtxfi 26211 |
. . . . . . . 8
⊢ (𝐺 ∈ FinUSGraph →
(Vtx‘𝐺) ∈
Fin) |
19 | | wspthnfi 26815 |
. . . . . . . 8
⊢
((Vtx‘𝐺)
∈ Fin → (2 WSPathsN 𝐺) ∈ Fin) |
20 | | rabfi 8185 |
. . . . . . . 8
⊢ ((2
WSPathsN 𝐺) ∈ Fin
→ {𝑠 ∈ (2
WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦} ∈ Fin) |
21 | 18, 19, 20 | 3syl 18 |
. . . . . . 7
⊢ (𝐺 ∈ FinUSGraph → {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦} ∈ Fin) |
22 | 21 | adantr 481 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑦 ∈ 𝑉) → {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦} ∈ Fin) |
23 | 16, 22 | eqeltrd 2701 |
. . . . 5
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑦 ∈ 𝑉) → ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦) ∈ Fin) |
24 | 1, 5 | 2wspmdisj 27201 |
. . . . . 6
⊢
Disj 𝑦 ∈
𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦) |
25 | 24 | a1i 11 |
. . . . 5
⊢ (𝐺 ∈ FinUSGraph →
Disj 𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) |
26 | 9, 23, 25 | hashiun 14554 |
. . . 4
⊢ (𝐺 ∈ FinUSGraph →
(#‘∪ 𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = Σ𝑦 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦))) |
27 | 26 | ad2antrr 762 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (#‘∪ 𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = Σ𝑦 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦))) |
28 | 1, 5 | fusgreghash2wspv 27199 |
. . . . . . . . 9
⊢ (𝐺 ∈ FinUSGraph →
∀𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1)))) |
29 | | ralim 2948 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
𝑉 (((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1))) → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ∀𝑣 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1)))) |
30 | 28, 29 | syl 17 |
. . . . . . . 8
⊢ (𝐺 ∈ FinUSGraph →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ∀𝑣 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1)))) |
31 | 30 | adantr 481 |
. . . . . . 7
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ∀𝑣 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1)))) |
32 | 31 | imp 445 |
. . . . . 6
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → ∀𝑣 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1))) |
33 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑣 = 𝑦 → ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣) = ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) |
34 | 33 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑣 = 𝑦 → (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦))) |
35 | 34 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑣 = 𝑦 → ((#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1)) ↔ (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = (𝐾 · (𝐾 − 1)))) |
36 | 35 | rspccva 3308 |
. . . . . 6
⊢
((∀𝑣 ∈
𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1)) ∧ 𝑦 ∈ 𝑉) → (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = (𝐾 · (𝐾 − 1))) |
37 | 32, 36 | sylan 488 |
. . . . 5
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) ∧ 𝑦 ∈ 𝑉) → (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = (𝐾 · (𝐾 − 1))) |
38 | 37 | sumeq2dv 14433 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → Σ𝑦 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = Σ𝑦 ∈ 𝑉 (𝐾 · (𝐾 − 1))) |
39 | 9 | adantr 481 |
. . . . 5
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) → 𝑉 ∈ Fin) |
40 | | eqid 2622 |
. . . . . . . . 9
⊢
(VtxDeg‘𝐺) =
(VtxDeg‘𝐺) |
41 | 1, 40 | fusgrregdegfi 26465 |
. . . . . . . 8
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → 𝐾 ∈
ℕ0)) |
42 | 41 | imp 445 |
. . . . . . 7
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → 𝐾 ∈
ℕ0) |
43 | 42 | nn0cnd 11353 |
. . . . . 6
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → 𝐾 ∈ ℂ) |
44 | | kcnktkm1cn 10461 |
. . . . . 6
⊢ (𝐾 ∈ ℂ → (𝐾 · (𝐾 − 1)) ∈
ℂ) |
45 | 43, 44 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐾 · (𝐾 − 1)) ∈
ℂ) |
46 | | fsumconst 14522 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ (𝐾 · (𝐾 − 1)) ∈ ℂ) →
Σ𝑦 ∈ 𝑉 (𝐾 · (𝐾 − 1)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1)))) |
47 | 39, 45, 46 | syl2an2r 876 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → Σ𝑦 ∈ 𝑉 (𝐾 · (𝐾 − 1)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1)))) |
48 | 38, 47 | eqtrd 2656 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → Σ𝑦 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1)))) |
49 | 8, 27, 48 | 3eqtrd 2660 |
. 2
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (#‘(2 WSPathsN 𝐺)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1)))) |
50 | 49 | ex 450 |
1
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (#‘(2 WSPathsN 𝐺)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1))))) |