Step |
Hyp |
Ref |
Expression |
1 |
|
fusgreghash2wsp.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
fveq1 |
⊢ ( 𝑠 = 𝑡 → ( 𝑠 ‘ 1 ) = ( 𝑡 ‘ 1 ) ) |
3 |
2
|
eqeq1d |
⊢ ( 𝑠 = 𝑡 → ( ( 𝑠 ‘ 1 ) = 𝑎 ↔ ( 𝑡 ‘ 1 ) = 𝑎 ) ) |
4 |
3
|
cbvrabv |
⊢ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } = { 𝑡 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑡 ‘ 1 ) = 𝑎 } |
5 |
4
|
mpteq2i |
⊢ ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) = ( 𝑎 ∈ 𝑉 ↦ { 𝑡 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑡 ‘ 1 ) = 𝑎 } ) |
6 |
1 5
|
fusgreg2wsp |
⊢ ( 𝐺 ∈ FinUSGraph → ( 2 WSPathsN 𝐺 ) = ∪ 𝑦 ∈ 𝑉 ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) |
7 |
6
|
ad2antrr |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( 2 WSPathsN 𝐺 ) = ∪ 𝑦 ∈ 𝑉 ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) |
8 |
7
|
fveq2d |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( ♯ ‘ ( 2 WSPathsN 𝐺 ) ) = ( ♯ ‘ ∪ 𝑦 ∈ 𝑉 ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) ) |
9 |
1
|
fusgrvtxfi |
⊢ ( 𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin ) |
10 |
|
eqeq2 |
⊢ ( 𝑎 = 𝑦 → ( ( 𝑠 ‘ 1 ) = 𝑎 ↔ ( 𝑠 ‘ 1 ) = 𝑦 ) ) |
11 |
10
|
rabbidv |
⊢ ( 𝑎 = 𝑦 → { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } = { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑦 } ) |
12 |
|
eqid |
⊢ ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) = ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) |
13 |
|
ovex |
⊢ ( 2 WSPathsN 𝐺 ) ∈ V |
14 |
13
|
rabex |
⊢ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑦 } ∈ V |
15 |
11 12 14
|
fvmpt |
⊢ ( 𝑦 ∈ 𝑉 → ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) = { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑦 } ) |
16 |
15
|
adantl |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) = { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑦 } ) |
17 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
18 |
17
|
fusgrvtxfi |
⊢ ( 𝐺 ∈ FinUSGraph → ( Vtx ‘ 𝐺 ) ∈ Fin ) |
19 |
|
wspthnfi |
⊢ ( ( Vtx ‘ 𝐺 ) ∈ Fin → ( 2 WSPathsN 𝐺 ) ∈ Fin ) |
20 |
|
rabfi |
⊢ ( ( 2 WSPathsN 𝐺 ) ∈ Fin → { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑦 } ∈ Fin ) |
21 |
18 19 20
|
3syl |
⊢ ( 𝐺 ∈ FinUSGraph → { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑦 } ∈ Fin ) |
22 |
21
|
adantr |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑦 ∈ 𝑉 ) → { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑦 } ∈ Fin ) |
23 |
16 22
|
eqeltrd |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ∈ Fin ) |
24 |
1 5
|
2wspmdisj |
⊢ Disj 𝑦 ∈ 𝑉 ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) |
25 |
24
|
a1i |
⊢ ( 𝐺 ∈ FinUSGraph → Disj 𝑦 ∈ 𝑉 ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) |
26 |
9 23 25
|
hashiun |
⊢ ( 𝐺 ∈ FinUSGraph → ( ♯ ‘ ∪ 𝑦 ∈ 𝑉 ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) = Σ 𝑦 ∈ 𝑉 ( ♯ ‘ ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) ) |
27 |
26
|
ad2antrr |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( ♯ ‘ ∪ 𝑦 ∈ 𝑉 ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) = Σ 𝑦 ∈ 𝑉 ( ♯ ‘ ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) ) |
28 |
1 5
|
fusgreghash2wspv |
⊢ ( 𝐺 ∈ FinUSGraph → ∀ 𝑣 ∈ 𝑉 ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ♯ ‘ ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) ) |
29 |
|
ralim |
⊢ ( ∀ 𝑣 ∈ 𝑉 ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ♯ ‘ ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) ) |
30 |
28 29
|
syl |
⊢ ( 𝐺 ∈ FinUSGraph → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) ) |
31 |
30
|
adantr |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) ) |
32 |
31
|
imp |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) |
33 |
|
2fveq3 |
⊢ ( 𝑣 = 𝑦 → ( ♯ ‘ ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑣 ) ) = ( ♯ ‘ ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) ) |
34 |
33
|
eqeq1d |
⊢ ( 𝑣 = 𝑦 → ( ( ♯ ‘ ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ↔ ( ♯ ‘ ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) ) |
35 |
34
|
rspccva |
⊢ ( ( ∀ 𝑣 ∈ 𝑉 ( ♯ ‘ ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑣 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ∧ 𝑦 ∈ 𝑉 ) → ( ♯ ‘ ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) |
36 |
32 35
|
sylan |
⊢ ( ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) ∧ 𝑦 ∈ 𝑉 ) → ( ♯ ‘ ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) |
37 |
36
|
sumeq2dv |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → Σ 𝑦 ∈ 𝑉 ( ♯ ‘ ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) = Σ 𝑦 ∈ 𝑉 ( 𝐾 · ( 𝐾 − 1 ) ) ) |
38 |
9
|
adantr |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → 𝑉 ∈ Fin ) |
39 |
|
eqid |
⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 ) |
40 |
1 39
|
fusgrregdegfi |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → 𝐾 ∈ ℕ0 ) ) |
41 |
40
|
imp |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → 𝐾 ∈ ℕ0 ) |
42 |
41
|
nn0cnd |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → 𝐾 ∈ ℂ ) |
43 |
|
kcnktkm1cn |
⊢ ( 𝐾 ∈ ℂ → ( 𝐾 · ( 𝐾 − 1 ) ) ∈ ℂ ) |
44 |
42 43
|
syl |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( 𝐾 · ( 𝐾 − 1 ) ) ∈ ℂ ) |
45 |
|
fsumconst |
⊢ ( ( 𝑉 ∈ Fin ∧ ( 𝐾 · ( 𝐾 − 1 ) ) ∈ ℂ ) → Σ 𝑦 ∈ 𝑉 ( 𝐾 · ( 𝐾 − 1 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) ) |
46 |
38 44 45
|
syl2an2r |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → Σ 𝑦 ∈ 𝑉 ( 𝐾 · ( 𝐾 − 1 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) ) |
47 |
37 46
|
eqtrd |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → Σ 𝑦 ∈ 𝑉 ( ♯ ‘ ( ( 𝑎 ∈ 𝑉 ↦ { 𝑠 ∈ ( 2 WSPathsN 𝐺 ) ∣ ( 𝑠 ‘ 1 ) = 𝑎 } ) ‘ 𝑦 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) ) |
48 |
8 27 47
|
3eqtrd |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( ♯ ‘ ( 2 WSPathsN 𝐺 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) ) |
49 |
48
|
ex |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ♯ ‘ ( 2 WSPathsN 𝐺 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) ) ) |