| Step | Hyp | Ref
| Expression |
| 1 | | frgrhash2wsp.v |
. . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) |
| 2 | | fusgreg2wsp.m |
. . . . . . 7
⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎}) |
| 3 | 1, 2 | fusgr2wsp2nb 30353 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → (𝑀‘𝑣) = ∪ 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
| 4 | 3 | fveq2d 6910 |
. . . . 5
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → (♯‘(𝑀‘𝑣)) = (♯‘∪ 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉})) |
| 5 | 4 | adantr 480 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (♯‘(𝑀‘𝑣)) = (♯‘∪ 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉})) |
| 6 | 1 | eleq2i 2833 |
. . . . . . 7
⊢ (𝑣 ∈ 𝑉 ↔ 𝑣 ∈ (Vtx‘𝐺)) |
| 7 | | nbfiusgrfi 29392 |
. . . . . . 7
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ (Vtx‘𝐺)) → (𝐺 NeighbVtx 𝑣) ∈ Fin) |
| 8 | 6, 7 | sylan2b 594 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → (𝐺 NeighbVtx 𝑣) ∈ Fin) |
| 9 | 8 | adantr 480 |
. . . . 5
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐺 NeighbVtx 𝑣) ∈ Fin) |
| 10 | | eqid 2737 |
. . . . 5
⊢ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}) = ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}) |
| 11 | | snfi 9083 |
. . . . . 6
⊢
{〈“𝑐𝑣𝑑”〉} ∈ Fin |
| 12 | 11 | a1i 11 |
. . . . 5
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) ∧ 𝑐 ∈ (𝐺 NeighbVtx 𝑣) ∧ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐})) → {〈“𝑐𝑣𝑑”〉} ∈ Fin) |
| 13 | 1 | nbgrssvtx 29359 |
. . . . . . . . . . 11
⊢ (𝐺 NeighbVtx 𝑣) ⊆ 𝑉 |
| 14 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ 𝑐 ∈ (𝐺 NeighbVtx 𝑣)) → (𝐺 NeighbVtx 𝑣) ⊆ 𝑉) |
| 15 | 14 | ssdifd 4145 |
. . . . . . . . 9
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ 𝑐 ∈ (𝐺 NeighbVtx 𝑣)) → ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}) ⊆ (𝑉 ∖ {𝑐})) |
| 16 | | iunss1 5006 |
. . . . . . . . 9
⊢ (((𝐺 NeighbVtx 𝑣) ∖ {𝑐}) ⊆ (𝑉 ∖ {𝑐}) → ∪
𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉} ⊆ ∪ 𝑑 ∈ (𝑉 ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
| 17 | 15, 16 | syl 17 |
. . . . . . . 8
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ 𝑐 ∈ (𝐺 NeighbVtx 𝑣)) → ∪
𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉} ⊆ ∪ 𝑑 ∈ (𝑉 ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
| 18 | 17 | ralrimiva 3146 |
. . . . . . 7
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → ∀𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉} ⊆ ∪ 𝑑 ∈ (𝑉 ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
| 19 | | simpr 484 |
. . . . . . . 8
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉) |
| 20 | | s3iunsndisj 15007 |
. . . . . . . 8
⊢ (𝑣 ∈ 𝑉 → Disj 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ (𝑉 ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
| 21 | 19, 20 | syl 17 |
. . . . . . 7
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → Disj 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ (𝑉 ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
| 22 | | disjss2 5113 |
. . . . . . 7
⊢
(∀𝑐 ∈
(𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉} ⊆ ∪ 𝑑 ∈ (𝑉 ∖ {𝑐}){〈“𝑐𝑣𝑑”〉} → (Disj 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ (𝑉 ∖ {𝑐}){〈“𝑐𝑣𝑑”〉} → Disj 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉})) |
| 23 | 18, 21, 22 | sylc 65 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → Disj 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
| 24 | 23 | adantr 480 |
. . . . 5
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → Disj 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
| 25 | 19 | adantr 480 |
. . . . . . 7
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → 𝑣 ∈ 𝑉) |
| 26 | 25 | anim1ci 616 |
. . . . . 6
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) ∧ 𝑐 ∈ (𝐺 NeighbVtx 𝑣)) → (𝑐 ∈ (𝐺 NeighbVtx 𝑣) ∧ 𝑣 ∈ 𝑉)) |
| 27 | | s3sndisj 15006 |
. . . . . 6
⊢ ((𝑐 ∈ (𝐺 NeighbVtx 𝑣) ∧ 𝑣 ∈ 𝑉) → Disj 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
| 28 | 26, 27 | syl 17 |
. . . . 5
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) ∧ 𝑐 ∈ (𝐺 NeighbVtx 𝑣)) → Disj 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) |
| 29 | | s3cli 14920 |
. . . . . 6
⊢
〈“𝑐𝑣𝑑”〉 ∈ Word V |
| 30 | | hashsng 14408 |
. . . . . 6
⊢
(〈“𝑐𝑣𝑑”〉 ∈ Word V →
(♯‘{〈“𝑐𝑣𝑑”〉}) = 1) |
| 31 | 29, 30 | mp1i 13 |
. . . . 5
⊢ ((((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) ∧ 𝑐 ∈ (𝐺 NeighbVtx 𝑣) ∧ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐})) → (♯‘{〈“𝑐𝑣𝑑”〉}) = 1) |
| 32 | 9, 10, 12, 24, 28, 31 | hash2iun1dif1 15860 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (♯‘∪ 𝑐 ∈ (𝐺 NeighbVtx 𝑣)∪ 𝑑 ∈ ((𝐺 NeighbVtx 𝑣) ∖ {𝑐}){〈“𝑐𝑣𝑑”〉}) = ((♯‘(𝐺 NeighbVtx 𝑣)) · ((♯‘(𝐺 NeighbVtx 𝑣)) − 1))) |
| 33 | | fusgrusgr 29339 |
. . . . . . 7
⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈
USGraph) |
| 34 | 1 | hashnbusgrvd 29546 |
. . . . . . 7
⊢ ((𝐺 ∈ USGraph ∧ 𝑣 ∈ 𝑉) → (♯‘(𝐺 NeighbVtx 𝑣)) = ((VtxDeg‘𝐺)‘𝑣)) |
| 35 | 33, 34 | sylan 580 |
. . . . . 6
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → (♯‘(𝐺 NeighbVtx 𝑣)) = ((VtxDeg‘𝐺)‘𝑣)) |
| 36 | | id 22 |
. . . . . . 7
⊢
((♯‘(𝐺
NeighbVtx 𝑣)) =
((VtxDeg‘𝐺)‘𝑣) → (♯‘(𝐺 NeighbVtx 𝑣)) = ((VtxDeg‘𝐺)‘𝑣)) |
| 37 | | oveq1 7438 |
. . . . . . 7
⊢
((♯‘(𝐺
NeighbVtx 𝑣)) =
((VtxDeg‘𝐺)‘𝑣) → ((♯‘(𝐺 NeighbVtx 𝑣)) − 1) = (((VtxDeg‘𝐺)‘𝑣) − 1)) |
| 38 | 36, 37 | oveq12d 7449 |
. . . . . 6
⊢
((♯‘(𝐺
NeighbVtx 𝑣)) =
((VtxDeg‘𝐺)‘𝑣) → ((♯‘(𝐺 NeighbVtx 𝑣)) · ((♯‘(𝐺 NeighbVtx 𝑣)) − 1)) = (((VtxDeg‘𝐺)‘𝑣) · (((VtxDeg‘𝐺)‘𝑣) − 1))) |
| 39 | 35, 38 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → ((♯‘(𝐺 NeighbVtx 𝑣)) · ((♯‘(𝐺 NeighbVtx 𝑣)) − 1)) = (((VtxDeg‘𝐺)‘𝑣) · (((VtxDeg‘𝐺)‘𝑣) − 1))) |
| 40 | | id 22 |
. . . . . 6
⊢
(((VtxDeg‘𝐺)‘𝑣) = 𝐾 → ((VtxDeg‘𝐺)‘𝑣) = 𝐾) |
| 41 | | oveq1 7438 |
. . . . . 6
⊢
(((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (((VtxDeg‘𝐺)‘𝑣) − 1) = (𝐾 − 1)) |
| 42 | 40, 41 | oveq12d 7449 |
. . . . 5
⊢
(((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (((VtxDeg‘𝐺)‘𝑣) · (((VtxDeg‘𝐺)‘𝑣) − 1)) = (𝐾 · (𝐾 − 1))) |
| 43 | 39, 42 | sylan9eq 2797 |
. . . 4
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → ((♯‘(𝐺 NeighbVtx 𝑣)) · ((♯‘(𝐺 NeighbVtx 𝑣)) − 1)) = (𝐾 · (𝐾 − 1))) |
| 44 | 5, 32, 43 | 3eqtrd 2781 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) ∧ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (♯‘(𝑀‘𝑣)) = (𝐾 · (𝐾 − 1))) |
| 45 | 44 | ex 412 |
. 2
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉) → (((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (♯‘(𝑀‘𝑣)) = (𝐾 · (𝐾 − 1)))) |
| 46 | 45 | ralrimiva 3146 |
1
⊢ (𝐺 ∈ FinUSGraph →
∀𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (♯‘(𝑀‘𝑣)) = (𝐾 · (𝐾 − 1)))) |