| Step | Hyp | Ref
| Expression |
| 1 | | fusgreghash2wsp.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
| 2 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝑠 = 𝑡 → (𝑠‘1) = (𝑡‘1)) |
| 3 | 2 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑠 = 𝑡 → ((𝑠‘1) = 𝑎 ↔ (𝑡‘1) = 𝑎)) |
| 4 | 3 | cbvrabv 3447 |
. . . . . . 7
⊢ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎} = {𝑡 ∈ (2 WSPathsN 𝐺) ∣ (𝑡‘1) = 𝑎} |
| 5 | 4 | mpteq2i 5247 |
. . . . . 6
⊢ (𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎}) = (𝑎 ∈ 𝑉 ↦ {𝑡 ∈ (2 WSPathsN 𝐺) ∣ (𝑡‘1) = 𝑎}) |
| 6 | 1, 5 | fusgreg2wsp 30355 |
. . . . 5
⊢ (𝐺 ∈ FinUSGraph → (2
WSPathsN 𝐺) = ∪ 𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) |
| 7 | 6 | ad2antrr 726 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (2 WSPathsN 𝐺) = ∪
𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) |
| 8 | 7 | fveq2d 6910 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (♯‘(2 WSPathsN 𝐺)) = (♯‘∪ 𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦))) |
| 9 | 1 | fusgrvtxfi 29336 |
. . . . 5
⊢ (𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin) |
| 10 | | eqeq2 2749 |
. . . . . . . . 9
⊢ (𝑎 = 𝑦 → ((𝑠‘1) = 𝑎 ↔ (𝑠‘1) = 𝑦)) |
| 11 | 10 | rabbidv 3444 |
. . . . . . . 8
⊢ (𝑎 = 𝑦 → {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎} = {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦}) |
| 12 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎}) = (𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎}) |
| 13 | | ovex 7464 |
. . . . . . . . 9
⊢ (2
WSPathsN 𝐺) ∈
V |
| 14 | 13 | rabex 5339 |
. . . . . . . 8
⊢ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦} ∈ V |
| 15 | 11, 12, 14 | fvmpt 7016 |
. . . . . . 7
⊢ (𝑦 ∈ 𝑉 → ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦) = {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦}) |
| 16 | 15 | adantl 481 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑦 ∈ 𝑉) → ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦) = {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦}) |
| 17 | | eqid 2737 |
. . . . . . . . 9
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 18 | 17 | fusgrvtxfi 29336 |
. . . . . . . 8
⊢ (𝐺 ∈ FinUSGraph →
(Vtx‘𝐺) ∈
Fin) |
| 19 | | wspthnfi 29939 |
. . . . . . . 8
⊢
((Vtx‘𝐺)
∈ Fin → (2 WSPathsN 𝐺) ∈ Fin) |
| 20 | | rabfi 9303 |
. . . . . . . 8
⊢ ((2
WSPathsN 𝐺) ∈ Fin
→ {𝑠 ∈ (2
WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦} ∈ Fin) |
| 21 | 18, 19, 20 | 3syl 18 |
. . . . . . 7
⊢ (𝐺 ∈ FinUSGraph → {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦} ∈ Fin) |
| 22 | 21 | adantr 480 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑦 ∈ 𝑉) → {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦} ∈ Fin) |
| 23 | 16, 22 | eqeltrd 2841 |
. . . . 5
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑦 ∈ 𝑉) → ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦) ∈ Fin) |
| 24 | 1, 5 | 2wspmdisj 30356 |
. . . . . 6
⊢
Disj 𝑦 ∈
𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦) |
| 25 | 24 | a1i 11 |
. . . . 5
⊢ (𝐺 ∈ FinUSGraph →
Disj 𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) |
| 26 | 9, 23, 25 | hashiun 15858 |
. . . 4
⊢ (𝐺 ∈ FinUSGraph →
(♯‘∪ 𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = Σ𝑦 ∈ 𝑉 (♯‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦))) |
| 27 | 26 | ad2antrr 726 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (♯‘∪ 𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = Σ𝑦 ∈ 𝑉 (♯‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦))) |
| 28 | 1, 5 | fusgreghash2wspv 30354 |
. . . . . . . . 9
⊢ (𝐺 ∈ FinUSGraph →
∀𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (♯‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1)))) |
| 29 | | ralim 3086 |
. . . . . . . . 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 480 |
. . . . . . 7
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ∀𝑣 ∈ 𝑉 (♯‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1)))) |
| 32 | 31 | imp 406 |
. . . . . 6
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → ∀𝑣 ∈ 𝑉 (♯‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1))) |
| 33 | | 2fveq3 6911 |
. . . . . . . 8
⊢ (𝑣 = 𝑦 → (♯‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (♯‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦))) |
| 34 | 33 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑣 = 𝑦 → ((♯‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1)) ↔ (♯‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = (𝐾 · (𝐾 − 1)))) |
| 35 | 34 | rspccva 3621 |
. . . . . 6
⊢
((∀𝑣 ∈
𝑉 (♯‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1)) ∧ 𝑦 ∈ 𝑉) → (♯‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = (𝐾 · (𝐾 − 1))) |
| 36 | 32, 35 | sylan 580 |
. . . . 5
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) ∧ 𝑦 ∈ 𝑉) → (♯‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = (𝐾 · (𝐾 − 1))) |
| 37 | 36 | sumeq2dv 15738 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → Σ𝑦 ∈ 𝑉 (♯‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = Σ𝑦 ∈ 𝑉 (𝐾 · (𝐾 − 1))) |
| 38 | 9 | adantr 480 |
. . . . 5
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) → 𝑉 ∈ Fin) |
| 39 | | eqid 2737 |
. . . . . . . . 9
⊢
(VtxDeg‘𝐺) =
(VtxDeg‘𝐺) |
| 40 | 1, 39 | fusgrregdegfi 29587 |
. . . . . . . 8
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → 𝐾 ∈
ℕ0)) |
| 41 | 40 | imp 406 |
. . . . . . 7
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → 𝐾 ∈
ℕ0) |
| 42 | 41 | nn0cnd 12589 |
. . . . . 6
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → 𝐾 ∈ ℂ) |
| 43 | | kcnktkm1cn 11694 |
. . . . . 6
⊢ (𝐾 ∈ ℂ → (𝐾 · (𝐾 − 1)) ∈
ℂ) |
| 44 | 42, 43 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐾 · (𝐾 − 1)) ∈
ℂ) |
| 45 | | fsumconst 15826 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ (𝐾 · (𝐾 − 1)) ∈ ℂ) →
Σ𝑦 ∈ 𝑉 (𝐾 · (𝐾 − 1)) = ((♯‘𝑉) · (𝐾 · (𝐾 − 1)))) |
| 46 | 38, 44, 45 | syl2an2r 685 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → Σ𝑦 ∈ 𝑉 (𝐾 · (𝐾 − 1)) = ((♯‘𝑉) · (𝐾 · (𝐾 − 1)))) |
| 47 | 37, 46 | eqtrd 2777 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → Σ𝑦 ∈ 𝑉 (♯‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = ((♯‘𝑉) · (𝐾 · (𝐾 − 1)))) |
| 48 | 8, 27, 47 | 3eqtrd 2781 |
. 2
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (♯‘(2 WSPathsN 𝐺)) = ((♯‘𝑉) · (𝐾 · (𝐾 − 1)))) |
| 49 | 48 | ex 412 |
1
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (♯‘(2 WSPathsN 𝐺)) = ((♯‘𝑉) · (𝐾 · (𝐾 − 1))))) |