Step | Hyp | Ref
| Expression |
1 | | frisusgra 26519 |
. . . . 5
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 USGrph 𝐸) |
2 | | usgrav 25867 |
. . . . 5
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
3 | | 2spot2iun2spont 26418 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 2SPathsOt 𝐸) = ∪
𝑎 ∈ 𝑉 ∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) |
4 | 1, 2, 3 | 3syl 18 |
. . . 4
⊢ (𝑉 FriendGrph 𝐸 → (𝑉 2SPathsOt 𝐸) = ∪
𝑎 ∈ 𝑉 ∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) |
5 | 4 | fveq2d 6107 |
. . 3
⊢ (𝑉 FriendGrph 𝐸 → (#‘(𝑉 2SPathsOt 𝐸)) = (#‘∪ 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏))) |
6 | 5 | adantr 480 |
. 2
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → (#‘(𝑉 2SPathsOt 𝐸)) = (#‘∪ 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏))) |
7 | | simpl 472 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 𝑉 ∈ Fin) |
8 | 7 | adantl 481 |
. . 3
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → 𝑉 ∈ Fin) |
9 | | diffi 8077 |
. . . . . . 7
⊢ (𝑉 ∈ Fin → (𝑉 ∖ {𝑎}) ∈ Fin) |
10 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝑉 ∖ {𝑎}) ∈ Fin) |
11 | 10 | adantl 481 |
. . . . 5
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → (𝑉 ∖ {𝑎}) ∈ Fin) |
12 | 11 | adantr 480 |
. . . 4
⊢ (((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑎 ∈ 𝑉) → (𝑉 ∖ {𝑎}) ∈ Fin) |
13 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → 𝐸 ∈ V) |
14 | 1, 2, 13 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑉 FriendGrph 𝐸 → 𝐸 ∈ V) |
15 | 14, 7 | anim12ci 589 |
. . . . . . . 8
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → (𝑉 ∈ Fin ∧ 𝐸 ∈ V)) |
16 | 15 | adantr 480 |
. . . . . . 7
⊢ (((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑎 ∈ 𝑉) → (𝑉 ∈ Fin ∧ 𝐸 ∈ V)) |
17 | 16 | adantr 480 |
. . . . . 6
⊢ ((((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → (𝑉 ∈ Fin ∧ 𝐸 ∈ V)) |
18 | | simpr 476 |
. . . . . . 7
⊢ (((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑎 ∈ 𝑉) → 𝑎 ∈ 𝑉) |
19 | | eldifi 3694 |
. . . . . . 7
⊢ (𝑏 ∈ (𝑉 ∖ {𝑎}) → 𝑏 ∈ 𝑉) |
20 | 18, 19 | anim12i 588 |
. . . . . 6
⊢ ((((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) |
21 | | 2spotfi 26419 |
. . . . . 6
⊢ (((𝑉 ∈ Fin ∧ 𝐸 ∈ V) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ∈ Fin) |
22 | 17, 20, 21 | syl2anc 691 |
. . . . 5
⊢ ((((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → (𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ∈ Fin) |
23 | 22 | ralrimiva 2949 |
. . . 4
⊢ (((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑎 ∈ 𝑉) → ∀𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ∈ Fin) |
24 | | iunfi 8137 |
. . . 4
⊢ (((𝑉 ∖ {𝑎}) ∈ Fin ∧ ∀𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ∈ Fin) → ∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ∈ Fin) |
25 | 12, 23, 24 | syl2anc 691 |
. . 3
⊢ (((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑎 ∈ 𝑉) → ∪
𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏) ∈ Fin) |
26 | | 2spotiundisj 26589 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → Disj
𝑎 ∈ 𝑉 ∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) |
27 | 1, 2, 26 | 3syl 18 |
. . . 4
⊢ (𝑉 FriendGrph 𝐸 → Disj 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) |
28 | 27 | adantr 480 |
. . 3
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → Disj 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) |
29 | 8, 25, 28 | hashiun 14395 |
. 2
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → (#‘∪ 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) = Σ𝑎 ∈ 𝑉 (#‘∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏))) |
30 | | 2spotdisj 26588 |
. . . . . . 7
⊢ (((𝑉 ∈ Fin ∧ 𝐸 ∈ V) ∧ 𝑎 ∈ 𝑉) → Disj 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) |
31 | 15, 30 | sylan 487 |
. . . . . 6
⊢ (((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑎 ∈ 𝑉) → Disj 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) |
32 | 12, 22, 31 | hashiun 14395 |
. . . . 5
⊢ (((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑎 ∈ 𝑉) → (#‘∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) = Σ𝑏 ∈ (𝑉 ∖ {𝑎})(#‘(𝑎(𝑉 2SPathOnOt 𝐸)𝑏))) |
33 | | simplll 794 |
. . . . . . 7
⊢ ((((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → 𝑉 FriendGrph 𝐸) |
34 | | eldifsni 4261 |
. . . . . . . . 9
⊢ (𝑏 ∈ (𝑉 ∖ {𝑎}) → 𝑏 ≠ 𝑎) |
35 | 34 | necomd 2837 |
. . . . . . . 8
⊢ (𝑏 ∈ (𝑉 ∖ {𝑎}) → 𝑎 ≠ 𝑏) |
36 | 35 | adantl 481 |
. . . . . . 7
⊢ ((((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → 𝑎 ≠ 𝑏) |
37 | | frg2spot1 26585 |
. . . . . . 7
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ 𝑎 ≠ 𝑏) → (#‘(𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) = 1) |
38 | 33, 20, 36, 37 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑎 ∈ 𝑉) ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → (#‘(𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) = 1) |
39 | 38 | sumeq2dv 14281 |
. . . . 5
⊢ (((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑎 ∈ 𝑉) → Σ𝑏 ∈ (𝑉 ∖ {𝑎})(#‘(𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) = Σ𝑏 ∈ (𝑉 ∖ {𝑎})1) |
40 | | ax-1cn 9873 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
41 | 9, 40 | jctir 559 |
. . . . . . . . . 10
⊢ (𝑉 ∈ Fin → ((𝑉 ∖ {𝑎}) ∈ Fin ∧ 1 ∈
ℂ)) |
42 | 41 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝑉 ∖ {𝑎}) ∈ Fin ∧ 1 ∈
ℂ)) |
43 | 42 | adantr 480 |
. . . . . . . 8
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝑎 ∈ 𝑉) → ((𝑉 ∖ {𝑎}) ∈ Fin ∧ 1 ∈
ℂ)) |
44 | | fsumconst 14364 |
. . . . . . . 8
⊢ (((𝑉 ∖ {𝑎}) ∈ Fin ∧ 1 ∈ ℂ) →
Σ𝑏 ∈ (𝑉 ∖ {𝑎})1 = ((#‘(𝑉 ∖ {𝑎})) · 1)) |
45 | 43, 44 | syl 17 |
. . . . . . 7
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝑎 ∈ 𝑉) → Σ𝑏 ∈ (𝑉 ∖ {𝑎})1 = ((#‘(𝑉 ∖ {𝑎})) · 1)) |
46 | | hashdifsn 13063 |
. . . . . . . . 9
⊢ ((𝑉 ∈ Fin ∧ 𝑎 ∈ 𝑉) → (#‘(𝑉 ∖ {𝑎})) = ((#‘𝑉) − 1)) |
47 | 46 | adantlr 747 |
. . . . . . . 8
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝑎 ∈ 𝑉) → (#‘(𝑉 ∖ {𝑎})) = ((#‘𝑉) − 1)) |
48 | 47 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝑎 ∈ 𝑉) → ((#‘(𝑉 ∖ {𝑎})) · 1) = (((#‘𝑉) − 1) ·
1)) |
49 | | hashnncl 13018 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ Fin →
((#‘𝑉) ∈ ℕ
↔ 𝑉 ≠
∅)) |
50 | 49 | biimpar 501 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
(#‘𝑉) ∈
ℕ) |
51 | | nnm1nn0 11211 |
. . . . . . . . . . 11
⊢
((#‘𝑉) ∈
ℕ → ((#‘𝑉)
− 1) ∈ ℕ0) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
((#‘𝑉) − 1)
∈ ℕ0) |
53 | 52 | nn0red 11229 |
. . . . . . . . 9
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
((#‘𝑉) − 1)
∈ ℝ) |
54 | | ax-1rid 9885 |
. . . . . . . . 9
⊢
(((#‘𝑉)
− 1) ∈ ℝ → (((#‘𝑉) − 1) · 1) = ((#‘𝑉) − 1)) |
55 | 53, 54 | syl 17 |
. . . . . . . 8
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
(((#‘𝑉) − 1)
· 1) = ((#‘𝑉)
− 1)) |
56 | 55 | adantr 480 |
. . . . . . 7
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝑎 ∈ 𝑉) → (((#‘𝑉) − 1) · 1) = ((#‘𝑉) − 1)) |
57 | 45, 48, 56 | 3eqtrd 2648 |
. . . . . 6
⊢ (((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝑎 ∈ 𝑉) → Σ𝑏 ∈ (𝑉 ∖ {𝑎})1 = ((#‘𝑉) − 1)) |
58 | 57 | adantll 746 |
. . . . 5
⊢ (((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑎 ∈ 𝑉) → Σ𝑏 ∈ (𝑉 ∖ {𝑎})1 = ((#‘𝑉) − 1)) |
59 | 32, 39, 58 | 3eqtrd 2648 |
. . . 4
⊢ (((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ 𝑎 ∈ 𝑉) → (#‘∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) = ((#‘𝑉) − 1)) |
60 | 59 | sumeq2dv 14281 |
. . 3
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → Σ𝑎 ∈ 𝑉 (#‘∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) = Σ𝑎 ∈ 𝑉 ((#‘𝑉) − 1)) |
61 | | hashcl 13009 |
. . . . . . . 8
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℕ0) |
62 | 61 | nn0cnd 11230 |
. . . . . . 7
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℂ) |
63 | | 1cnd 9935 |
. . . . . . 7
⊢ (𝑉 ∈ Fin → 1 ∈
ℂ) |
64 | 62, 63 | subcld 10271 |
. . . . . 6
⊢ (𝑉 ∈ Fin →
((#‘𝑉) − 1)
∈ ℂ) |
65 | | fsumconst 14364 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧
((#‘𝑉) − 1)
∈ ℂ) → Σ𝑎 ∈ 𝑉 ((#‘𝑉) − 1) = ((#‘𝑉) · ((#‘𝑉) − 1))) |
66 | 64, 65 | mpdan 699 |
. . . . 5
⊢ (𝑉 ∈ Fin → Σ𝑎 ∈ 𝑉 ((#‘𝑉) − 1) = ((#‘𝑉) · ((#‘𝑉) − 1))) |
67 | 66 | adantr 480 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
Σ𝑎 ∈ 𝑉 ((#‘𝑉) − 1) = ((#‘𝑉) · ((#‘𝑉) − 1))) |
68 | 67 | adantl 481 |
. . 3
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → Σ𝑎 ∈ 𝑉 ((#‘𝑉) − 1) = ((#‘𝑉) · ((#‘𝑉) − 1))) |
69 | 60, 68 | eqtrd 2644 |
. 2
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → Σ𝑎 ∈ 𝑉 (#‘∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) = ((#‘𝑉) · ((#‘𝑉) − 1))) |
70 | 6, 29, 69 | 3eqtrd 2648 |
1
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → (#‘(𝑉 2SPathsOt 𝐸)) = ((#‘𝑉) · ((#‘𝑉) − 1))) |