Step | Hyp | Ref
| Expression |
1 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑡 → (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ↔ 𝑡 ∈ (𝑉 2SPathsOt 𝐸))) |
2 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑡 → (1st ‘𝑠) = (1st ‘𝑡)) |
3 | 2 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑡 → (2nd
‘(1st ‘𝑠)) = (2nd ‘(1st
‘𝑡))) |
4 | 3 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑡 → ((2nd
‘(1st ‘𝑠)) = 𝑎 ↔ (2nd
‘(1st ‘𝑡)) = 𝑎)) |
5 | 1, 4 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑠 = 𝑡 → ((𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎) ↔ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑎))) |
6 | 5 | cbvrabv 3172 |
. . . . . . . 8
⊢ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)} = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑎)} |
7 | 6 | mpteq2i 4669 |
. . . . . . 7
⊢ (𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)}) = (𝑎 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑡)) = 𝑎)}) |
8 | 7 | usgreg2spot 26594 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (𝑉 2SPathsOt 𝐸) = ∪
𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦))) |
9 | 8 | 3adant3 1074 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (𝑉 2SPathsOt 𝐸) = ∪
𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦))) |
10 | 9 | imp 444 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (𝑉 2SPathsOt 𝐸) = ∪
𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦)) |
11 | 10 | fveq2d 6107 |
. . 3
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (#‘(𝑉 2SPathsOt 𝐸)) = (#‘∪ 𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦))) |
12 | | simpl 472 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → 𝑉 ∈ Fin) |
13 | | simpr 476 |
. . . . . . 7
⊢ (((𝑉 ∈ Fin ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) ∧ 𝑦 ∈ 𝑉) → 𝑦 ∈ 𝑉) |
14 | | 3xpfi 8117 |
. . . . . . . . 9
⊢ (𝑉 ∈ Fin → ((𝑉 × 𝑉) × 𝑉) ∈ Fin) |
15 | | rabexg 4739 |
. . . . . . . . 9
⊢ (((𝑉 × 𝑉) × 𝑉) ∈ Fin → {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑦)} ∈ V) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ (𝑉 ∈ Fin → {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑦)} ∈ V) |
17 | 16 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝑉 ∈ Fin ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) ∧ 𝑦 ∈ 𝑉) → {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑦)} ∈ V) |
18 | | eqeq2 2621 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑦 → ((2nd
‘(1st ‘𝑠)) = 𝑎 ↔ (2nd
‘(1st ‘𝑠)) = 𝑦)) |
19 | 18 | anbi2d 736 |
. . . . . . . . 9
⊢ (𝑎 = 𝑦 → ((𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎) ↔ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑦))) |
20 | 19 | rabbidv 3164 |
. . . . . . . 8
⊢ (𝑎 = 𝑦 → {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)} = {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑦)}) |
21 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)}) = (𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)}) |
22 | 20, 21 | fvmptg 6189 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝑉 ∧ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑦)} ∈ V) → ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦) = {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑦)}) |
23 | 13, 17, 22 | syl2anc 691 |
. . . . . 6
⊢ (((𝑉 ∈ Fin ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) ∧ 𝑦 ∈ 𝑉) → ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦) = {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑦)}) |
24 | 14 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝑉 ∈ Fin ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) ∧ 𝑦 ∈ 𝑉) → ((𝑉 × 𝑉) × 𝑉) ∈ Fin) |
25 | | rabfi 8070 |
. . . . . . 7
⊢ (((𝑉 × 𝑉) × 𝑉) ∈ Fin → {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑦)} ∈ Fin) |
26 | 24, 25 | syl 17 |
. . . . . 6
⊢ (((𝑉 ∈ Fin ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) ∧ 𝑦 ∈ 𝑉) → {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑦)} ∈ Fin) |
27 | 23, 26 | eqeltrd 2688 |
. . . . 5
⊢ (((𝑉 ∈ Fin ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) ∧ 𝑦 ∈ 𝑉) → ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦) ∈ Fin) |
28 | 7 | 2spotmdisj 26595 |
. . . . . 6
⊢ (𝑉 ∈ Fin → Disj
𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦)) |
29 | 28 | adantr 480 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → Disj 𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦)) |
30 | 12, 27, 29 | hashiun 14395 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (#‘∪ 𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦)) = Σ𝑦 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦))) |
31 | 30 | 3ad2antl2 1217 |
. . 3
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (#‘∪ 𝑦 ∈ 𝑉 ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦)) = Σ𝑦 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦))) |
32 | 7 | usgreghash2spotv 26593 |
. . . . . . . . 9
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) → ∀𝑣 ∈ 𝑉 (((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑣)) = (𝐾 · (𝐾 − 1)))) |
33 | | ralim 2932 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
𝑉 (((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑣)) = (𝐾 · (𝐾 − 1))) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → ∀𝑣 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑣)) = (𝐾 · (𝐾 − 1)))) |
34 | 32, 33 | syl 17 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → ∀𝑣 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑣)) = (𝐾 · (𝐾 − 1)))) |
35 | 34 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → ∀𝑣 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑣)) = (𝐾 · (𝐾 − 1)))) |
36 | 35 | imp 444 |
. . . . . 6
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → ∀𝑣 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑣)) = (𝐾 · (𝐾 − 1))) |
37 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑣 = 𝑦 → ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑣) = ((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦)) |
38 | 37 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑣 = 𝑦 → (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑣)) = (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦))) |
39 | 38 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑣 = 𝑦 → ((#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑣)) = (𝐾 · (𝐾 − 1)) ↔ (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦)) = (𝐾 · (𝐾 − 1)))) |
40 | 39 | rspccva 3281 |
. . . . . 6
⊢
((∀𝑣 ∈
𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑣)) = (𝐾 · (𝐾 − 1)) ∧ 𝑦 ∈ 𝑉) → (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦)) = (𝐾 · (𝐾 − 1))) |
41 | 36, 40 | sylan 487 |
. . . . 5
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) ∧ 𝑦 ∈ 𝑉) → (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦)) = (𝐾 · (𝐾 − 1))) |
42 | 41 | sumeq2dv 14281 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → Σ𝑦 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦)) = Σ𝑦 ∈ 𝑉 (𝐾 · (𝐾 − 1))) |
43 | | simpl2 1058 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → 𝑉 ∈ Fin) |
44 | | usgfidegfi 26437 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) → ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ∈
ℕ0) |
45 | | r19.26 3046 |
. . . . . . . . . . 11
⊢
(∀𝑣 ∈
𝑉 (((𝑉 VDeg 𝐸)‘𝑣) ∈ ℕ0 ∧ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) ↔ (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ∈ ℕ0 ∧
∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾)) |
46 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (((𝑉 VDeg 𝐸)‘𝑣) ∈ ℕ0 ↔ 𝐾 ∈
ℕ0)) |
47 | 46 | biimpac 502 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 VDeg 𝐸)‘𝑣) ∈ ℕ0 ∧ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → 𝐾 ∈
ℕ0) |
48 | 47 | ralimi 2936 |
. . . . . . . . . . . 12
⊢
(∀𝑣 ∈
𝑉 (((𝑉 VDeg 𝐸)‘𝑣) ∈ ℕ0 ∧ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → ∀𝑣 ∈ 𝑉 𝐾 ∈
ℕ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
⊢
(∀𝑣 ∈
𝑉 (((𝑉 VDeg 𝐸)‘𝑣) ∈ ℕ0 ∧ ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (𝑉 ≠ ∅ → (𝐾 · (𝐾 − 1)) ∈
ℂ)) |
57 | 45, 56 | sylbir 224 |
. . . . . . . . . 10
⊢
((∀𝑣 ∈
𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ∈ ℕ0 ∧
∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (𝑉 ≠ ∅ → (𝐾 · (𝐾 − 1)) ∈
ℂ)) |
58 | 57 | ex 449 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ∈ ℕ0 →
(∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (𝑉 ≠ ∅ → (𝐾 · (𝐾 − 1)) ∈
ℂ))) |
59 | 58 | com23 84 |
. . . . . . . 8
⊢
(∀𝑣 ∈
𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ∈ ℕ0 → (𝑉 ≠ ∅ →
(∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (𝐾 · (𝐾 − 1)) ∈
ℂ))) |
60 | 44, 59 | syl 17 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) → (𝑉 ≠ ∅ → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (𝐾 · (𝐾 − 1)) ∈
ℂ))) |
61 | 60 | ex 449 |
. . . . . 6
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ Fin → (𝑉 ≠ ∅ → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (𝐾 · (𝐾 − 1)) ∈
ℂ)))) |
62 | 61 | 3imp1 1272 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (𝐾 · (𝐾 − 1)) ∈
ℂ) |
63 | | fsumconst 14364 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ (𝐾 · (𝐾 − 1)) ∈ ℂ) →
Σ𝑦 ∈ 𝑉 (𝐾 · (𝐾 − 1)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1)))) |
64 | 43, 62, 63 | syl2anc 691 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → Σ𝑦 ∈ 𝑉 (𝐾 · (𝐾 − 1)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1)))) |
65 | 42, 64 | eqtrd 2644 |
. . 3
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → Σ𝑦 ∈ 𝑉 (#‘((𝑎 ∈ 𝑉 ↦ {𝑠 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑠 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd
‘(1st ‘𝑠)) = 𝑎)})‘𝑦)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1)))) |
66 | 11, 31, 65 | 3eqtrd 2648 |
. 2
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (#‘(𝑉 2SPathsOt 𝐸)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1)))) |
67 | 66 | ex 449 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (#‘(𝑉 2SPathsOt 𝐸)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1))))) |