Step | Hyp | Ref
| Expression |
1 | | frgrhash2wsp.v |
. . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | fusgreg2wsp.m |
. . . . . . 7
⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎}) |
3 | 1, 2 | fusgr2wsp2nb 27488 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → (𝑀‘𝑣) = ∪ 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
4 | 3 | fveq2d 6356 |
. . . . 5
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → (♯‘(𝑀‘𝑣)) = (♯‘∪ 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉})) |
5 | 4 | adantr 472 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (♯‘(𝑀‘𝑣)) = (♯‘∪ 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉})) |
6 | 1 | eleq2i 2831 |
. . . . . . 7
⊢ (𝑣 ∈ 𝑉 ↔ 𝑣 ∈ (Vtx‘𝐺)) |
7 | | nbfiusgrfi 26475 |
. . . . . . 7
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ (Vtx‘𝐺)) → (𝐺 NeighbVtx 𝑣) ∈ Fin) |
8 | 6, 7 | sylan2b 493 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → (𝐺 NeighbVtx 𝑣) ∈ Fin) |
9 | 8 | adantr 472 |
. . . . 5
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐺 NeighbVtx 𝑣) ∈ Fin) |
10 | | eqid 2760 |
. . . . 5
⊢ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}) = ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}) |
11 | | snfi 8203 |
. . . . . 6
⊢
{〈“𝑐𝑣𝑑”〉} ∈ Fin |
12 | 11 | a1i 11 |
. . . . 5
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) ∧ 𝑐 ∈ (𝐺 NeighbVtx 𝑣) ∧ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐})) → {〈“𝑐𝑣𝑑”〉} ∈ Fin) |
13 | 1 | nbgrssvtx 26435 |
. . . . . . . . . . 11
⊢ (𝐺 NeighbVtx 𝑣) ⊆ 𝑉 |
14 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ 𝑐 ∈ (𝐺 NeighbVtx 𝑣)) → (𝐺 NeighbVtx 𝑣) ⊆ 𝑉) |
15 | 14 | ssdifd 3889 |
. . . . . . . . 9
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ 𝑐 ∈ (𝐺 NeighbVtx 𝑣)) → ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}) ⊆ (𝑉 ∖ {𝑐})) |
16 | | iunss1 4684 |
. . . . . . . . 9
⊢ (((𝐺 NeighbVtx 𝑣) ∖ {𝑐}) ⊆ (𝑉 ∖ {𝑐}) → ∪
𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉} ⊆ ∪ 𝑑 ∈ (𝑉 ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
17 | 15, 16 | syl 17 |
. . . . . . . 8
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ 𝑐 ∈ (𝐺 NeighbVtx 𝑣)) → ∪
𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉} ⊆ ∪ 𝑑 ∈ (𝑉 ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
18 | 17 | ralrimiva 3104 |
. . . . . . 7
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → ∀𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉} ⊆ ∪ 𝑑 ∈ (𝑉 ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
19 | | simpr 479 |
. . . . . . . 8
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉) |
20 | | s3iunsndisj 13908 |
. . . . . . . 8
⊢ (𝑣 ∈ 𝑉 → Disj 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ (𝑉 ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
21 | 19, 20 | syl 17 |
. . . . . . 7
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → Disj 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ (𝑉 ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
22 | | disjss2 4775 |
. . . . . . 7
⊢
(∀𝑐 ∈
(𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉} ⊆ ∪ 𝑑 ∈ (𝑉 ∖ {𝑐}){〈“𝑐𝑣𝑑”〉} → (Disj 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ (𝑉 ∖ {𝑐}){〈“𝑐𝑣𝑑”〉} → Disj 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉})) |
23 | 18, 21, 22 | sylc 65 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → Disj 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
24 | 23 | adantr 472 |
. . . . 5
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → Disj 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
25 | 19 | adantr 472 |
. . . . . . . 8
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → 𝑣 ∈ 𝑉) |
26 | 25 | anim1i 593 |
. . . . . . 7
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) ∧ 𝑐 ∈ (𝐺 NeighbVtx 𝑣)) → (𝑣 ∈ 𝑉 ∧ 𝑐 ∈ (𝐺 NeighbVtx 𝑣))) |
27 | 26 | ancomd 466 |
. . . . . 6
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) ∧ 𝑐 ∈ (𝐺 NeighbVtx 𝑣)) → (𝑐 ∈ (𝐺 NeighbVtx 𝑣) ∧ 𝑣 ∈ 𝑉)) |
28 | | s3sndisj 13907 |
. . . . . 6
⊢ ((𝑐 ∈ (𝐺 NeighbVtx 𝑣) ∧ 𝑣 ∈ 𝑉) → Disj 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
29 | 27, 28 | syl 17 |
. . . . 5
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) ∧ 𝑐 ∈ (𝐺 NeighbVtx 𝑣)) → Disj 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
30 | | s3cli 13826 |
. . . . . 6
⊢
〈“𝑐𝑣𝑑”〉 ∈ Word V |
31 | | hashsng 13351 |
. . . . . 6
⊢
(〈“𝑐𝑣𝑑”〉 ∈ Word V →
(♯‘{〈“𝑐𝑣𝑑”〉}) = 1) |
32 | 30, 31 | mp1i 13 |
. . . . 5
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) ∧ 𝑐 ∈ (𝐺 NeighbVtx 𝑣) ∧ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐})) → (♯‘{〈“𝑐𝑣𝑑”〉}) = 1) |
33 | 9, 10, 12, 24, 29, 32 | hash2iun1dif1 14755 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (♯‘∪ 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) = ((♯‘(𝐺 NeighbVtx 𝑣)) · ((♯‘(𝐺 NeighbVtx 𝑣)) − 1))) |
34 | | fusgrusgr 26413 |
. . . . . . 7
⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈
USGraph) |
35 | 1 | hashnbusgrvd 26634 |
. . . . . . 7
⊢ ((𝐺 ∈ USGraph ∧ 𝑣 ∈ 𝑉) → (♯‘(𝐺 NeighbVtx 𝑣)) = ((VtxDeg‘𝐺)‘𝑣)) |
36 | 34, 35 | sylan 489 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → (♯‘(𝐺 NeighbVtx 𝑣)) = ((VtxDeg‘𝐺)‘𝑣)) |
37 | | id 22 |
. . . . . . 7
⊢
((♯‘(𝐺
NeighbVtx 𝑣)) =
((VtxDeg‘𝐺)‘𝑣) → (♯‘(𝐺 NeighbVtx 𝑣)) = ((VtxDeg‘𝐺)‘𝑣)) |
38 | | oveq1 6820 |
. . . . . . 7
⊢
((♯‘(𝐺
NeighbVtx 𝑣)) =
((VtxDeg‘𝐺)‘𝑣) → ((♯‘(𝐺 NeighbVtx 𝑣)) − 1) = (((VtxDeg‘𝐺)‘𝑣) − 1)) |
39 | 37, 38 | oveq12d 6831 |
. . . . . 6
⊢
((♯‘(𝐺
NeighbVtx 𝑣)) =
((VtxDeg‘𝐺)‘𝑣) → ((♯‘(𝐺 NeighbVtx 𝑣)) · ((♯‘(𝐺 NeighbVtx 𝑣)) − 1)) = (((VtxDeg‘𝐺)‘𝑣) · (((VtxDeg‘𝐺)‘𝑣) − 1))) |
40 | 36, 39 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → ((♯‘(𝐺 NeighbVtx 𝑣)) · ((♯‘(𝐺 NeighbVtx 𝑣)) − 1)) = (((VtxDeg‘𝐺)‘𝑣) · (((VtxDeg‘𝐺)‘𝑣) − 1))) |
41 | | id 22 |
. . . . . 6
⊢
(((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((VtxDeg‘𝐺)‘𝑣) = 𝐾) |
42 | | oveq1 6820 |
. . . . . 6
⊢
(((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (((VtxDeg‘𝐺)‘𝑣) − 1) = (𝐾 − 1)) |
43 | 41, 42 | oveq12d 6831 |
. . . . 5
⊢
(((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (((VtxDeg‘𝐺)‘𝑣) · (((VtxDeg‘𝐺)‘𝑣) − 1)) = (𝐾 · (𝐾 − 1))) |
44 | 40, 43 | sylan9eq 2814 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → ((♯‘(𝐺 NeighbVtx 𝑣)) · ((♯‘(𝐺 NeighbVtx 𝑣)) − 1)) = (𝐾 · (𝐾 − 1))) |
45 | 5, 33, 44 | 3eqtrd 2798 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (♯‘(𝑀‘𝑣)) = (𝐾 · (𝐾 − 1))) |
46 | 45 | ex 449 |
. 2
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → (((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (♯‘(𝑀‘𝑣)) = (𝐾 · (𝐾 − 1)))) |
47 | 46 | ralrimiva 3104 |
1
⊢ (𝐺 ∈ FinUSGraph →
∀𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (♯‘(𝑀‘𝑣)) = (𝐾 · (𝐾 − 1)))) |