Step | Hyp | Ref
| Expression |
1 | | fusgreghash2wsp.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑠 = 𝑡 → (𝑠‘1) = (𝑡‘1)) |
3 | 2 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑠 = 𝑡 → ((𝑠‘1) = 𝑎 ↔ (𝑡‘1) = 𝑎)) |
4 | 3 | cbvrabv 3172 |
. . . . . . 7
⊢ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎} = {𝑡 ∈ (2 WSPathsN 𝐺) ∣ (𝑡‘1) = 𝑎} |
5 | 4 | mpteq2i 4669 |
. . . . . 6
⊢ (𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎}) = (𝑎 ∈ 𝑉 ↦ {𝑡 ∈ (2 WSPathsN 𝐺) ∣ (𝑡‘1) = 𝑎}) |
6 | 1, 5 | fusgreg2wsp 41500 |
. . . . 5
⊢ (𝐺 ∈ FinUSGraph → (2
WSPathsN 𝐺) = ∪ 𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) |
7 | 6 | ad2antrr 758 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (2 WSPathsN 𝐺) = ∪
𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) |
8 | 7 | fveq2d 6107 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (#‘(2 WSPathsN 𝐺)) = (#‘∪ 𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦))) |
9 | 1 | fusgrvtxfi 40538 |
. . . . 5
⊢ (𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin) |
10 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎}) = (𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎}) |
11 | 10 | a1i 11 |
. . . . . . 7
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑦 ∈ 𝑉) → (𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎}) = (𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})) |
12 | | eqeq2 2621 |
. . . . . . . . 9
⊢ (𝑎 = 𝑦 → ((𝑠‘1) = 𝑎 ↔ (𝑠‘1) = 𝑦)) |
13 | 12 | rabbidv 3164 |
. . . . . . . 8
⊢ (𝑎 = 𝑦 → {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎} = {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦}) |
14 | 13 | adantl 481 |
. . . . . . 7
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑦 ∈ 𝑉) ∧ 𝑎 = 𝑦) → {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎} = {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦}) |
15 | | simpr 476 |
. . . . . . 7
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑦 ∈ 𝑉) → 𝑦 ∈ 𝑉) |
16 | | ovex 6577 |
. . . . . . . . 9
⊢ (2
WSPathsN 𝐺) ∈
V |
17 | 16 | rabex 4740 |
. . . . . . . 8
⊢ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦} ∈ V |
18 | 17 | a1i 11 |
. . . . . . 7
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑦 ∈ 𝑉) → {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦} ∈ V) |
19 | 11, 14, 15, 18 | fvmptd 6197 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑦 ∈ 𝑉) → ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦) = {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦}) |
20 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
21 | 20 | fusgrvtxfi 40538 |
. . . . . . . . 9
⊢ (𝐺 ∈ FinUSGraph →
(Vtx‘𝐺) ∈
Fin) |
22 | | wspthnfi 41126 |
. . . . . . . . 9
⊢
((Vtx‘𝐺)
∈ Fin → (2 WSPathsN 𝐺) ∈ Fin) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ (𝐺 ∈ FinUSGraph → (2
WSPathsN 𝐺) ∈
Fin) |
24 | | rabfi 8070 |
. . . . . . . 8
⊢ ((2
WSPathsN 𝐺) ∈ Fin
→ {𝑠 ∈ (2
WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦} ∈ Fin) |
25 | 23, 24 | syl 17 |
. . . . . . 7
⊢ (𝐺 ∈ FinUSGraph → {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦} ∈ Fin) |
26 | 25 | adantr 480 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑦 ∈ 𝑉) → {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑦} ∈ Fin) |
27 | 19, 26 | eqeltrd 2688 |
. . . . 5
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑦 ∈ 𝑉) → ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦) ∈ Fin) |
28 | 1, 5 | 2wspmdisj 41501 |
. . . . . 6
⊢
Disj 𝑦 ∈
𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦) |
29 | 28 | a1i 11 |
. . . . 5
⊢ (𝐺 ∈ FinUSGraph →
Disj 𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) |
30 | 9, 27, 29 | hashiun 14395 |
. . . 4
⊢ (𝐺 ∈ FinUSGraph →
(#‘∪ 𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = Σ𝑦 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦))) |
31 | 30 | ad2antrr 758 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (#‘∪ 𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = Σ𝑦 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦))) |
32 | 1, 5 | fusgreghash2wspv 41499 |
. . . . . . . . 9
⊢ (𝐺 ∈ FinUSGraph →
∀𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1)))) |
33 | | ralim 2932 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
𝑉 (((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1))) → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ∀𝑣 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1)))) |
34 | 32, 33 | syl 17 |
. . . . . . . 8
⊢ (𝐺 ∈ FinUSGraph →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ∀𝑣 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1)))) |
35 | 34 | adantr 480 |
. . . . . . 7
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ∀𝑣 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1)))) |
36 | 35 | imp 444 |
. . . . . 6
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → ∀𝑣 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1))) |
37 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑣 = 𝑦 → ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣) = ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) |
38 | 37 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑣 = 𝑦 → (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦))) |
39 | 38 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑣 = 𝑦 → ((#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1)) ↔ (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = (𝐾 · (𝐾 − 1)))) |
40 | 39 | rspccva 3281 |
. . . . . 6
⊢
((∀𝑣 ∈
𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑣)) = (𝐾 · (𝐾 − 1)) ∧ 𝑦 ∈ 𝑉) → (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = (𝐾 · (𝐾 − 1))) |
41 | 36, 40 | sylan 487 |
. . . . 5
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) ∧ 𝑦 ∈ 𝑉) → (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = (𝐾 · (𝐾 − 1))) |
42 | 41 | sumeq2dv 14281 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → Σ𝑦 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = Σ𝑦 ∈ 𝑉 (𝐾 · (𝐾 − 1))) |
43 | 9 | adantr 480 |
. . . . 5
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) → 𝑉 ∈ Fin) |
44 | 1 | vtxdgfusgr 40713 |
. . . . . . . 8
⊢ (𝐺 ∈ FinUSGraph →
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ∈
ℕ0) |
45 | | r19.26 3046 |
. . . . . . . . . . 11
⊢
(∀𝑣 ∈
𝑉 (((VtxDeg‘𝐺)‘𝑣) ∈ ℕ0 ∧
((VtxDeg‘𝐺)‘𝑣) = 𝐾) ↔ (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ∈ ℕ0 ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾)) |
46 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢
(((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (((VtxDeg‘𝐺)‘𝑣) ∈ ℕ0 ↔ 𝐾 ∈
ℕ0)) |
47 | 46 | biimpac 502 |
. . . . . . . . . . . . 13
⊢
((((VtxDeg‘𝐺)‘𝑣) ∈ ℕ0 ∧
((VtxDeg‘𝐺)‘𝑣) = 𝐾) → 𝐾 ∈
ℕ0) |
48 | 47 | ralimi 2936 |
. . . . . . . . . . . 12
⊢
(∀𝑣 ∈
𝑉 (((VtxDeg‘𝐺)‘𝑣) ∈ ℕ0 ∧
((VtxDeg‘𝐺)‘𝑣) = 𝐾) → ∀𝑣 ∈ 𝑉 𝐾 ∈
ℕ0) |
49 | | r19.2z 4012 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 ≠ ∅ ∧
∀𝑣 ∈ 𝑉 𝐾 ∈ ℕ0) →
∃𝑣 ∈ 𝑉 𝐾 ∈
ℕ0) |
50 | | nn0cn 11179 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℂ) |
51 | | kcnktkm1cn 10340 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℂ → (𝐾 · (𝐾 − 1)) ∈
ℂ) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ ℕ0
→ (𝐾 · (𝐾 − 1)) ∈
ℂ) |
53 | 52 | rexlimivw 3011 |
. . . . . . . . . . . . . 14
⊢
(∃𝑣 ∈
𝑉 𝐾 ∈ ℕ0 → (𝐾 · (𝐾 − 1)) ∈
ℂ) |
54 | 49, 53 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ≠ ∅ ∧
∀𝑣 ∈ 𝑉 𝐾 ∈ ℕ0) → (𝐾 · (𝐾 − 1)) ∈
ℂ) |
55 | 54 | expcom 450 |
. . . . . . . . . . . 12
⊢
(∀𝑣 ∈
𝑉 𝐾 ∈ ℕ0 → (𝑉 ≠ ∅ → (𝐾 · (𝐾 − 1)) ∈
ℂ)) |
56 | 48, 55 | syl 17 |
. . . . . . . . . . 11
⊢
(∀𝑣 ∈
𝑉 (((VtxDeg‘𝐺)‘𝑣) ∈ ℕ0 ∧
((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝑉 ≠ ∅ → (𝐾 · (𝐾 − 1)) ∈
ℂ)) |
57 | 45, 56 | sylbir 224 |
. . . . . . . . . 10
⊢
((∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) ∈ ℕ0 ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝑉 ≠ ∅ → (𝐾 · (𝐾 − 1)) ∈
ℂ)) |
58 | 57 | ex 449 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) ∈ ℕ0 →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝑉 ≠ ∅ → (𝐾 · (𝐾 − 1)) ∈
ℂ))) |
59 | 58 | com23 84 |
. . . . . . . 8
⊢
(∀𝑣 ∈
𝑉 ((VtxDeg‘𝐺)‘𝑣) ∈ ℕ0 → (𝑉 ≠ ∅ →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐾 · (𝐾 − 1)) ∈
ℂ))) |
60 | 44, 59 | syl 17 |
. . . . . . 7
⊢ (𝐺 ∈ FinUSGraph → (𝑉 ≠ ∅ →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐾 · (𝐾 − 1)) ∈
ℂ))) |
61 | 60 | imp 444 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (𝐾 · (𝐾 − 1)) ∈
ℂ)) |
62 | 61 | imp 444 |
. . . . 5
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐾 · (𝐾 − 1)) ∈
ℂ) |
63 | | fsumconst 14364 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ (𝐾 · (𝐾 − 1)) ∈ ℂ) →
Σ𝑦 ∈ 𝑉 (𝐾 · (𝐾 − 1)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1)))) |
64 | 43, 62, 63 | syl2an2r 872 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → Σ𝑦 ∈ 𝑉 (𝐾 · (𝐾 − 1)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1)))) |
65 | 42, 64 | eqtrd 2644 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → Σ𝑦 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ (2 WSPathsN 𝐺) ∣ (𝑠‘1) = 𝑎})‘𝑦)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1)))) |
66 | 8, 31, 65 | 3eqtrd 2648 |
. 2
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (#‘(2 WSPathsN 𝐺)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1)))) |
67 | 66 | ex 449 |
1
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (#‘(2 WSPathsN 𝐺)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1))))) |