![]() |
Metamath
Proof Explorer Theorem List (p. 265 of 429) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-27903) |
![]() (27904-29428) |
![]() (29429-42879) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cusgrsizeindb0 26401 | Base case of the induction in cusgrsize 26406. The size of a complete simple graph with 0 vertices, actually of every null graph, is 0=((0-1)*0)/2. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 7-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ (#‘𝑉) = 0) → (#‘𝐸) = ((#‘𝑉)C2)) | ||
Theorem | cusgrsizeindb1 26402 | Base case of the induction in cusgrsize 26406. The size of a (complete) simple graph with 1 vertex is 0=((1-1)*1)/2. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 7-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ (#‘𝑉) = 1) → (#‘𝐸) = ((#‘𝑉)C2)) | ||
Theorem | cusgrsizeindslem 26403* | Lemma for cusgrsizeinds 26404. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (#‘{𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}) = ((#‘𝑉) − 1)) | ||
Theorem | cusgrsizeinds 26404* | Part 1 of induction step in cusgrsize 26406. The size of a complete simple graph with 𝑛 vertices is (𝑛 − 1) plus the size of the complete graph reduced by one vertex. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (#‘𝐸) = (((#‘𝑉) − 1) + (#‘𝐹))) | ||
Theorem | cusgrsize2inds 26405* | Induction step in cusgrsize 26406. If the size of the complete graph with 𝑛 vertices reduced by one vertex is "(𝑛 − 1) choose 2", the size of the complete graph with 𝑛 vertices is "𝑛 choose 2". (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} ⇒ ⊢ (𝑌 ∈ ℕ0 → ((𝐺 ∈ ComplUSGraph ∧ (#‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉) → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2)))) | ||
Theorem | cusgrsize 26406 | The size of a finite complete simple graph with 𝑛 vertices (𝑛 ∈ ℕ0) is (𝑛C2) ("𝑛 choose 2") resp. (((𝑛 − 1)∗𝑛) / 2), see definition in section I.1 of [Bollobas] p. 3 . (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 10-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin) → (#‘𝐸) = ((#‘𝑉)C2)) | ||
Theorem | cusgrfilem1 26407* | Lemma 1 for cusgrfi 26410. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})} ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉) → 𝑃 ⊆ (Edg‘𝐺)) | ||
Theorem | cusgrfilem2 26408* | Lemma 2 for cusgrfi 26410. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})} & ⊢ 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁}) ⇒ ⊢ (𝑁 ∈ 𝑉 → 𝐹:(𝑉 ∖ {𝑁})–1-1-onto→𝑃) | ||
Theorem | cusgrfilem3 26409* | Lemma 3 for cusgrfi 26410. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})} & ⊢ 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁}) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝑉 ∈ Fin ↔ 𝑃 ∈ Fin)) | ||
Theorem | cusgrfi 26410 | If the size of a complete simple graph is finite, then its order is also finite. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝐸 ∈ Fin) → 𝑉 ∈ Fin) | ||
Theorem | usgredgsscusgredg 26411 | A simple graph is a subgraph of a complete simple graph. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 13-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐻) & ⊢ 𝐹 = (Edg‘𝐻) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) → 𝐸 ⊆ 𝐹) | ||
Theorem | usgrsscusgr 26412* | A simple graph is a subgraph of a complete simple graph. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 13-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐻) & ⊢ 𝐹 = (Edg‘𝐻) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) → ∀𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 𝑒 = 𝑓) | ||
Theorem | sizusglecusglem1 26413 | Lemma 1 for sizusglecusg 26415. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 13-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐻) & ⊢ 𝐹 = (Edg‘𝐻) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) → ( I ↾ 𝐸):𝐸–1-1→𝐹) | ||
Theorem | sizusglecusglem2 26414 | Lemma 2 for sizusglecusg 26415. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 13-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐻) & ⊢ 𝐹 = (Edg‘𝐻) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ∧ 𝐹 ∈ Fin) → 𝐸 ∈ Fin) | ||
Theorem | sizusglecusg 26415 | The size of a simple graph with 𝑛 vertices is at most the size of a complete simple graph with 𝑛 vertices (𝑛 may be infinite). (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 13-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐻) & ⊢ 𝐹 = (Edg‘𝐻) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) → (#‘𝐸) ≤ (#‘𝐹)) | ||
Theorem | fusgrmaxsize 26416 | The maximum size of a finite simple graph with 𝑛 vertices is (((𝑛 − 1)∗𝑛) / 2). See statement in section I.1 of [Bollobas] p. 3 . (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 14-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph → (#‘𝐸) ≤ ((#‘𝑉)C2)) | ||
Syntax | cvtxdg 26417 | Extend class notation with the vertex degree function. |
class VtxDeg | ||
Definition | df-vtxdg 26418* | Define the vertex degree function for a graph. To be appropriate for arbitrary hypergraphs, we have to double-count those edges that contain 𝑢 "twice" (i.e. self-loops), this being represented as a singleton as the edge's value. Since the degree of a vertex can be (positive) infinity (if the graph containing the vertex is not of finite size), the extended addition +𝑒 is used for the summation of the number of "ordinary" edges" and the number of "loops". (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 9-Dec-2020.) |
⊢ VtxDeg = (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})))) | ||
Theorem | vtxdgfval 26419* | The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 9-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 ⇒ ⊢ (𝐺 ∈ 𝑊 → (VtxDeg‘𝐺) = (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}})))) | ||
Theorem | vtxdgval 26420* | The degree of a vertex. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 10-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 ⇒ ⊢ (𝑈 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑈) = ((#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑈}}))) | ||
Theorem | vtxdgfival 26421* | The degree of a vertex for graphs of finite size. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.) (Revised by AV, 8-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 ⇒ ⊢ ((𝐴 ∈ Fin ∧ 𝑈 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑈) = ((#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)}) + (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑈}}))) | ||
Theorem | vtxdgop 26422 | The vertex degree expressed as operation. (Contributed by AV, 12-Dec-2021.) |
⊢ (𝐺 ∈ 𝑊 → (VtxDeg‘𝐺) = ((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))) | ||
Theorem | vtxdgf 26423 | The vertex degree function is a function from vertices to extended nonnegative integers. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 10-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (VtxDeg‘𝐺):𝑉⟶ℕ0*) | ||
Theorem | vtxdgelxnn0 26424 | The degree of a vertex is either a nonnegative integer or positive infinity. (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 10-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑋) ∈ ℕ0*) | ||
Theorem | vtxdg0v 26425 | The degree of a vertex in the null graph is zero (or anything else), because there are no vertices. (Contributed by AV, 11-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 = ∅ ∧ 𝑈 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑈) = 0) | ||
Theorem | vtxdg0e 26426 | The degree of a vertex in an empty graph is zero, because there are no edges. This is the base case for the induction for calculating the degree of a vertex, for example in a Königsberg graph (see also the induction steps vdegp1ai 26488, vdegp1bi 26489 and vdegp1ci 26490). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 11-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝑈 ∈ 𝑉 ∧ 𝐼 = ∅) → ((VtxDeg‘𝐺)‘𝑈) = 0) | ||
Theorem | vtxdgfisnn0 26427 | The degree of a vertex in a graph of finite size is a nonnegative integer. (Contributed by Alexander van der Vekens, 10-Mar-2018.) (Revised by AV, 11-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 ⇒ ⊢ ((𝐴 ∈ Fin ∧ 𝑈 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑈) ∈ ℕ0) | ||
Theorem | vtxdgfisf 26428 | The vertex degree function on graphs of finite size is a function from vertices to nonnegative integers. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 11-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐴 ∈ Fin) → (VtxDeg‘𝐺):𝑉⟶ℕ0) | ||
Theorem | vtxdeqd 26429 | Equality theorem for the vertex degree: If two graphs are structurally equal, their vertex degree functions are equal. (Contributed by AV, 26-Feb-2021.) |
⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → 𝐻 ∈ 𝑌) & ⊢ (𝜑 → (Vtx‘𝐻) = (Vtx‘𝐺)) & ⊢ (𝜑 → (iEdg‘𝐻) = (iEdg‘𝐺)) ⇒ ⊢ (𝜑 → (VtxDeg‘𝐻) = (VtxDeg‘𝐺)) | ||
Theorem | vtxduhgr0e 26430 | The degree of a vertex in an empty hypergraph is zero, because there are no edges. Analogue of vtxdg0e 26426. (Contributed by AV, 15-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 = ∅) → ((VtxDeg‘𝐺)‘𝑈) = 0) | ||
Theorem | vtxdlfuhgr1v 26431* | The degree of the vertex in a loop-free hypergraph with one vertex is 0. (Contributed by AV, 2-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)} ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ (#‘𝑉) = 1 ∧ 𝐼:dom 𝐼⟶𝐸) → (𝑈 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑈) = 0)) | ||
Theorem | vdumgr0 26432 | A vertex in a multigraph has degree 0 if the graph consists of only one vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 2-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ∧ (#‘𝑉) = 1) → ((VtxDeg‘𝐺)‘𝑁) = 0) | ||
Theorem | vtxdun 26433 | The degree of a vertex in the union of two graphs on the same vertex set is the sum of the degrees of the vertex in each graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Dec-2017.) (Revised by AV, 19-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐽 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉) & ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → Fun 𝐽) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽)) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) +𝑒 ((VtxDeg‘𝐻)‘𝑁))) | ||
Theorem | vtxdfiun 26434 | The degree of a vertex in the union of two hypergraphs of finite size on the same vertex set is the sum of the degrees of the vertex in each hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.) (Revised by AV, 19-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐽 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉) & ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → Fun 𝐽) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽)) & ⊢ (𝜑 → dom 𝐼 ∈ Fin) & ⊢ (𝜑 → dom 𝐽 ∈ Fin) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) + ((VtxDeg‘𝐻)‘𝑁))) | ||
Theorem | vtxduhgrun 26435 | The degree of a vertex in the union of two hypergraphs on the same vertex set is the sum of the degrees of the vertex in each hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Dec-2017.) (Revised by AV, 12-Dec-2020.) (Proof shortened by AV, 19-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐽 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉) & ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅) & ⊢ (𝜑 → 𝐺 ∈ UHGraph) & ⊢ (𝜑 → 𝐻 ∈ UHGraph) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽)) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) +𝑒 ((VtxDeg‘𝐻)‘𝑁))) | ||
Theorem | vtxduhgrfiun 26436 | The degree of a vertex in the union of two hypergraphs of finite size on the same vertex set is the sum of the degrees of the vertex in each hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.) (Revised by AV, 7-Dec-2020.) (Proof shortened by AV, 19-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐽 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉) & ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅) & ⊢ (𝜑 → 𝐺 ∈ UHGraph) & ⊢ (𝜑 → 𝐻 ∈ UHGraph) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽)) & ⊢ (𝜑 → dom 𝐼 ∈ Fin) & ⊢ (𝜑 → dom 𝐽 ∈ Fin) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) + ((VtxDeg‘𝐻)‘𝑁))) | ||
Theorem | vtxdlfgrval 26437* | The value of the vertex degree function for a loop-free graph 𝐺. (Contributed by AV, 23-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐼:𝐴⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)} ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = (#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)})) | ||
Theorem | vtxdumgrval 26438* | The value of the vertex degree function for a multigraph. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 23-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = (#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)})) | ||
Theorem | vtxdusgrval 26439* | The value of the vertex degree function for a simple graph. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 11-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = (#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)})) | ||
Theorem | vtxd0nedgb 26440* | A vertex has degree 0 iff there is no edge incident with the vertex. (Contributed by AV, 24-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ (𝑈 ∈ 𝑉 → ((𝐷‘𝑈) = 0 ↔ ¬ ∃𝑖 ∈ dom 𝐼 𝑈 ∈ (𝐼‘𝑖))) | ||
Theorem | vtxdushgrfvedglem 26441* | Lemma for vtxdushgrfvedg 26442 and vtxdusgrfvedg 26443. (Contributed by AV, 12-Dec-2020.) (Proof shortened by AV, 5-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉) → (#‘{𝑖 ∈ dom (iEdg‘𝐺) ∣ 𝑈 ∈ ((iEdg‘𝐺)‘𝑖)}) = (#‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒})) | ||
Theorem | vtxdushgrfvedg 26442* | The value of the vertex degree function for a simple hypergraph. (Contributed by AV, 12-Dec-2020.) (Proof shortened by AV, 5-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = ((#‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒}) +𝑒 (#‘{𝑒 ∈ 𝐸 ∣ 𝑒 = {𝑈}}))) | ||
Theorem | vtxdusgrfvedg 26443* | The value of the vertex degree function for a simple graph. (Contributed by AV, 12-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = (#‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒})) | ||
Theorem | vtxduhgr0nedg 26444* | If a vertex in a hypergraph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 8-Dec-2017.) (Revised by AV, 15-Dec-2020.) (Proof shortened by AV, 24-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ∧ (𝐷‘𝑈) = 0) → ¬ ∃𝑣 ∈ 𝑉 {𝑈, 𝑣} ∈ 𝐸) | ||
Theorem | vtxdumgr0nedg 26445* | If a vertex in a multigraph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 8-Dec-2017.) (Revised by AV, 12-Dec-2020.) (Proof shortened by AV, 15-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑈 ∈ 𝑉 ∧ (𝐷‘𝑈) = 0) → ¬ ∃𝑣 ∈ 𝑉 {𝑈, 𝑣} ∈ 𝐸) | ||
Theorem | vtxduhgr0edgnel 26446* | A vertex in a hypergraph has degree 0 iff there is no edge incident with this vertex. (Contributed by AV, 24-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉) → ((𝐷‘𝑈) = 0 ↔ ¬ ∃𝑒 ∈ 𝐸 𝑈 ∈ 𝑒)) | ||
Theorem | vtxdusgr0edgnel 26447* | A vertex in a simple graph has degree 0 iff there is no edge incident with this vertex. (Contributed by AV, 17-Dec-2020.) (Proof shortened by AV, 24-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → ((𝐷‘𝑈) = 0 ↔ ¬ ∃𝑒 ∈ 𝐸 𝑈 ∈ 𝑒)) | ||
Theorem | vtxdusgr0edgnelALT 26448* | Alternate proof of vtxdusgr0edgnel 26447, not based on vtxduhgr0edgnel 26446. A vertex in a simple graph has degree 0 if there is no edge incident with this vertex. (Contributed by AV, 17-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → ((𝐷‘𝑈) = 0 ↔ ¬ ∃𝑒 ∈ 𝐸 𝑈 ∈ 𝑒)) | ||
Theorem | vtxdgfusgrf 26449 | The vertex degree function on finite simple graphs is a function from vertices to nonnegative integers. (Contributed by AV, 12-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph → (VtxDeg‘𝐺):𝑉⟶ℕ0) | ||
Theorem | vtxdgfusgr 26450* | In a finite simple graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 10-Mar-2018.) (Revised by AV, 12-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph → ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ∈ ℕ0) | ||
Theorem | fusgrn0degnn0 26451* | In a nonempty, finite graph there is a vertex having a nonnegative integer as degree. (Contributed by Alexander van der Vekens, 6-Sep-2018.) (Revised by AV, 1-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) → ∃𝑣 ∈ 𝑉 ∃𝑛 ∈ ℕ0 ((VtxDeg‘𝐺)‘𝑣) = 𝑛) | ||
Theorem | 1loopgruspgr 26452 | A graph with one edge which is a loop is a simple pseudograph (see also uspgr1v1eop 26186). (Contributed by AV, 21-Feb-2021.) |
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝑁}〉}) ⇒ ⊢ (𝜑 → 𝐺 ∈ USPGraph) | ||
Theorem | 1loopgredg 26453 | The set of edges in a graph (simple pseudograph) with one edge which is a loop is a singleton of a singleton. (Contributed by AV, 17-Dec-2020.) (Revised by AV, 21-Feb-2021.) |
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝑁}〉}) ⇒ ⊢ (𝜑 → (Edg‘𝐺) = {{𝑁}}) | ||
Theorem | 1loopgrnb0 26454 | In a graph (simple pseudograph) with one edge which is a loop, the vertex connected with itself by the loop has no neighbors. (Contributed by AV, 17-Dec-2020.) (Revised by AV, 21-Feb-2021.) |
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝑁}〉}) ⇒ ⊢ (𝜑 → (𝐺 NeighbVtx 𝑁) = ∅) | ||
Theorem | 1loopgrvd2 26455 | The vertex degree of a one-edge graph, case 4: an edge from a vertex to itself contributes two to the vertex's degree. I. e. in a graph (simple pseudograph) with one edge which is a loop, the vertex connected with itself by the loop has degree 2. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.) |
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝑁}〉}) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝑁) = 2) | ||
Theorem | 1loopgrvd0 26456 | The vertex degree of a one-edge graph, case 1 (for a loop): a loop at a vertex other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 21-Feb-2021.) |
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝑁}〉}) & ⊢ (𝜑 → 𝐾 ∈ (𝑉 ∖ {𝑁})) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐾) = 0) | ||
Theorem | 1hevtxdg0 26457 | The vertex degree of vertex 𝐷 in a graph 𝐺 with only one hyperedge 𝐸 is 0 if 𝐷 is not incident with the edge 𝐸. (Contributed by AV, 2-Mar-2021.) |
⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, 𝐸〉}) & ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝑌) & ⊢ (𝜑 → 𝐷 ∉ 𝐸) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐷) = 0) | ||
Theorem | 1hevtxdg1 26458 | The vertex degree of vertex 𝐷 in a graph 𝐺 with only one hyperedge 𝐸 (not being a loop) is 1 if 𝐷 is incident with the edge 𝐸. (Contributed by AV, 2-Mar-2021.) (Proof shortened by AV, 17-Apr-2021.) |
⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, 𝐸〉}) & ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝐸) & ⊢ (𝜑 → 2 ≤ (#‘𝐸)) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐷) = 1) | ||
Theorem | 1hegrvtxdg1 26459 | The vertex degree of a graph with one hyperedge, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 23-Feb-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, 𝐸〉}) & ⊢ (𝜑 → {𝐵, 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐵) = 1) | ||
Theorem | 1hegrvtxdg1r 26460 | The vertex degree of a graph with one hyperedge, case 3: an edge from some other vertex to the given vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 23-Feb-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, 𝐸〉}) & ⊢ (𝜑 → {𝐵, 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐶) = 1) | ||
Theorem | 1egrvtxdg1 26461 | The vertex degree of a one-edge graph, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.) |
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐵) = 1) | ||
Theorem | 1egrvtxdg1r 26462 | The vertex degree of a one-edge graph, case 3: an edge from some other vertex to the given vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.) |
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐶) = 1) | ||
Theorem | 1egrvtxdg0 26463 | The vertex degree of a one-edge graph, case 1: an edge between two vertices other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.) |
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ≠ 𝐷) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐷}〉}) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐶) = 0) | ||
Theorem | p1evtxdeqlem 26464 | Lemma for p1evtxdeq 26465 and p1evtxdp1 26466. (Contributed by AV, 3-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ∪ {〈𝐾, 𝐸〉})) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ (𝜑 → 𝐾 ∉ dom 𝐼) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝑌) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = (((VtxDeg‘𝐺)‘𝑈) +𝑒 ((VtxDeg‘〈𝑉, {〈𝐾, 𝐸〉}〉)‘𝑈))) | ||
Theorem | p1evtxdeq 26465 | If an edge 𝐸 which does not contain vertex 𝑈 is added to a graph 𝐺 (yielding a graph 𝐹), the degree of 𝑈 is the same in both graphs. (Contributed by AV, 2-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ∪ {〈𝐾, 𝐸〉})) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ (𝜑 → 𝐾 ∉ dom 𝐼) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝑌) & ⊢ (𝜑 → 𝑈 ∉ 𝐸) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = ((VtxDeg‘𝐺)‘𝑈)) | ||
Theorem | p1evtxdp1 26466 | If an edge 𝐸 (not being a loop) which contains vertex 𝑈 is added to a graph 𝐺 (yielding a graph 𝐹), the degree of 𝑈 is increased by 1. (Contributed by AV, 3-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ∪ {〈𝐾, 𝐸〉})) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ (𝜑 → 𝐾 ∉ dom 𝐼) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉) & ⊢ (𝜑 → 𝑈 ∈ 𝐸) & ⊢ (𝜑 → 2 ≤ (#‘𝐸)) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = (((VtxDeg‘𝐺)‘𝑈) +𝑒 1)) | ||
Theorem | uspgrloopvtx 26467 | The set of vertices in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 26186). (Contributed by AV, 17-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈𝐴, {𝑁}〉}〉 ⇒ ⊢ (𝑉 ∈ 𝑊 → (Vtx‘𝐺) = 𝑉) | ||
Theorem | uspgrloopvtxel 26468 | A vertex in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 26186). (Contributed by AV, 17-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈𝐴, {𝑁}〉}〉 ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) → 𝑁 ∈ (Vtx‘𝐺)) | ||
Theorem | uspgrloopiedg 26469 | The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 26186) is a singleton of a singleton. (Contributed by AV, 21-Feb-2021.) |
⊢ 𝐺 = 〈𝑉, {〈𝐴, {𝑁}〉}〉 ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) → (iEdg‘𝐺) = {〈𝐴, {𝑁}〉}) | ||
Theorem | uspgrloopedg 26470 | The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 26186) is a singleton of a singleton. (Contributed by AV, 17-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈𝐴, {𝑁}〉}〉 ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) → (Edg‘𝐺) = {{𝑁}}) | ||
Theorem | uspgrloopnb0 26471 | In a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 26186), the vertex connected with itself by the loop has no neighbors. (Contributed by AV, 17-Dec-2020.) (Proof shortened by AV, 21-Feb-2021.) |
⊢ 𝐺 = 〈𝑉, {〈𝐴, {𝑁}〉}〉 ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉) → (𝐺 NeighbVtx 𝑁) = ∅) | ||
Theorem | uspgrloopvd2 26472 | The vertex degree of a one-edge graph, case 4: an edge from a vertex to itself contributes two to the vertex's degree. I. e. in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 26186), the vertex connected with itself by the loop has degree 2. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 17-Dec-2020.) (Proof shortened by AV, 21-Feb-2021.) |
⊢ 𝐺 = 〈𝑉, {〈𝐴, {𝑁}〉}〉 ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑁) = 2) | ||
Theorem | umgr2v2evtx 26473 | The set of vertices in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 ⇒ ⊢ (𝑉 ∈ 𝑊 → (Vtx‘𝐺) = 𝑉) | ||
Theorem | umgr2v2evtxel 26474 | A vertex in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ (Vtx‘𝐺)) | ||
Theorem | umgr2v2eiedg 26475 | The edge function in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (iEdg‘𝐺) = {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}) | ||
Theorem | umgr2v2eedg 26476 | The set of edges in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (Edg‘𝐺) = {{𝐴, 𝐵}}) | ||
Theorem | umgr2v2e 26477 | A multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 ⇒ ⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ UMGraph) | ||
Theorem | umgr2v2enb1 26478 | In a multigraph with two edges connecting the same two vertices, each of the vertices has one neighbor. (Contributed by AV, 18-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 ⇒ ⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐺 NeighbVtx 𝐴) = {𝐵}) | ||
Theorem | umgr2v2evd2 26479 | In a multigraph with two edges connecting the same two vertices, each of the vertices has degree 2. (Contributed by AV, 18-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 ⇒ ⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((VtxDeg‘𝐺)‘𝐴) = 2) | ||
Theorem | hashnbusgrvd 26480 | In a simple graph, the number of neighbors of a vertex is the degree of this vertex. This theorem does not hold for (simple) pseudographs, because a vertex connected with itself only by a loop has no neighbors, see uspgrloopnb0 26471, but degree 2, see uspgrloopvd2 26472. And it does not hold for multigraphs, because a vertex connected with only one other vertex by two edges has one neighbor, see umgr2v2enb1 26478, but also degree 2, see umgr2v2evd2 26479. (Contributed by Alexander van der Vekens, 17-Dec-2017.) (Revised by AV, 15-Dec-2020.) (Proof shortened by AV, 5-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (#‘(𝐺 NeighbVtx 𝑈)) = ((VtxDeg‘𝐺)‘𝑈)) | ||
Theorem | usgruvtxvdb 26481 | In a finite simple graph with n vertices a vertex is universal iff the vertex has degree 𝑛 − 1. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 17-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → (𝑈 ∈ (UnivVtx‘𝐺) ↔ ((VtxDeg‘𝐺)‘𝑈) = ((#‘𝑉) − 1))) | ||
Theorem | vdiscusgrb 26482* | A finite simple graph with n vertices is complete iff every vertex has degree 𝑛 − 1. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 22-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph → (𝐺 ∈ ComplUSGraph ↔ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = ((#‘𝑉) − 1))) | ||
Theorem | vdiscusgr 26483* | In a finite complete simple graph with n vertices every vertex has degree 𝑛 − 1. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 17-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = ((#‘𝑉) − 1) → 𝐺 ∈ ComplUSGraph)) | ||
Theorem | vtxdusgradjvtx 26484* | The degree of a vertex in a simple graph is the number of vertices adjacent to this vertex. (Contributed by Alexander van der Vekens, 9-Jul-2018.) (Revised by AV, 23-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑈) = (#‘{𝑣 ∈ 𝑉 ∣ {𝑈, 𝑣} ∈ 𝐸})) | ||
Theorem | usgrvd0nedg 26485* | If a vertex in a simple graph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 16-Dec-2020.) (Proof shortened by AV, 23-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (((VtxDeg‘𝐺)‘𝑈) = 0 → ¬ ∃𝑣 ∈ 𝑉 {𝑈, 𝑣} ∈ 𝐸)) | ||
Theorem | uhgrvd00 26486* | If every vertex in a hypergraph has degree 0, there is no edge in the graph. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 24-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ UHGraph → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 → 𝐸 = ∅)) | ||
Theorem | usgrvd00 26487* | If every vertex in a simple graph has degree 0, there is no edge in the graph. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 17-Dec-2020.) (Proof shortened by AV, 23-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 → 𝐸 = ∅)) | ||
Theorem | vdegp1ai 26488* | The induction step for a vertex degree calculation. If the degree of 𝑈 in the edge set 𝐸 is 𝑃, then adding {𝑋, 𝑌} to the edge set, where 𝑋 ≠ 𝑈 ≠ 𝑌, yields degree 𝑃 as well. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 ∈ 𝑉 & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐼 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} & ⊢ ((VtxDeg‘𝐺)‘𝑈) = 𝑃 & ⊢ (Vtx‘𝐹) = 𝑉 & ⊢ 𝑋 ∈ 𝑉 & ⊢ 𝑋 ≠ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑌 ≠ 𝑈 & ⊢ (iEdg‘𝐹) = (𝐼 ++ 〈“{𝑋, 𝑌}”〉) ⇒ ⊢ ((VtxDeg‘𝐹)‘𝑈) = 𝑃 | ||
Theorem | vdegp1bi 26489* | The induction step for a vertex degree calculation, for example in the Königsberg graph. If the degree of 𝑈 in the edge set 𝐸 is 𝑃, then adding {𝑈, 𝑋} to the edge set, where 𝑋 ≠ 𝑈, yields degree 𝑃 + 1. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 ∈ 𝑉 & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐼 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} & ⊢ ((VtxDeg‘𝐺)‘𝑈) = 𝑃 & ⊢ (Vtx‘𝐹) = 𝑉 & ⊢ 𝑋 ∈ 𝑉 & ⊢ 𝑋 ≠ 𝑈 & ⊢ (iEdg‘𝐹) = (𝐼 ++ 〈“{𝑈, 𝑋}”〉) ⇒ ⊢ ((VtxDeg‘𝐹)‘𝑈) = (𝑃 + 1) | ||
Theorem | vdegp1ci 26490* | The induction step for a vertex degree calculation, for example in the Königsberg graph. If the degree of 𝑈 in the edge set 𝐸 is 𝑃, then adding {𝑋, 𝑈} to the edge set, where 𝑋 ≠ 𝑈, yields degree 𝑃 + 1. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 ∈ 𝑉 & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐼 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} & ⊢ ((VtxDeg‘𝐺)‘𝑈) = 𝑃 & ⊢ (Vtx‘𝐹) = 𝑉 & ⊢ 𝑋 ∈ 𝑉 & ⊢ 𝑋 ≠ 𝑈 & ⊢ (iEdg‘𝐹) = (𝐼 ++ 〈“{𝑋, 𝑈}”〉) ⇒ ⊢ ((VtxDeg‘𝐹)‘𝑈) = (𝑃 + 1) | ||
Theorem | vtxdginducedm1lem1 26491 | Lemma 1 for vtxdginducedm1 26495: the edge function in the induced subgraph 𝑆 of a pseudograph 𝐺 obtained by removing one vertex 𝑁. (Contributed by AV, 16-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 ⇒ ⊢ (iEdg‘𝑆) = 𝑃 | ||
Theorem | vtxdginducedm1lem2 26492* | Lemma 2 for vtxdginducedm1 26495: the domain of the edge function in the induced subgraph 𝑆 of a pseudograph 𝐺 obtained by removing one vertex 𝑁. (Contributed by AV, 16-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 ⇒ ⊢ dom (iEdg‘𝑆) = 𝐼 | ||
Theorem | vtxdginducedm1lem3 26493* | Lemma 3 for vtxdginducedm1 26495: an edge in the induced subgraph 𝑆 of a pseudograph 𝐺 obtained by removing one vertex 𝑁. (Contributed by AV, 16-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 ⇒ ⊢ (𝐻 ∈ 𝐼 → ((iEdg‘𝑆)‘𝐻) = (𝐸‘𝐻)) | ||
Theorem | vtxdginducedm1lem4 26494* | Lemma 4 for vtxdginducedm1 26495. (Contributed by AV, 17-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ (𝑊 ∈ (𝑉 ∖ {𝑁}) → (#‘{𝑘 ∈ 𝐽 ∣ (𝐸‘𝑘) = {𝑊}}) = 0) | ||
Theorem | vtxdginducedm1 26495* | The degree of a vertex 𝑣 in the induced subgraph 𝑆 of a pseudograph 𝐺 obtained by removing one vertex 𝑁 plus the number of edges joining the vertex 𝑣 and the vertex 𝑁 is the degree of the vertex 𝑣 in the pseudograph 𝐺. (Contributed by AV, 17-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ ∀𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) = (((VtxDeg‘𝑆)‘𝑣) +𝑒 (#‘{𝑙 ∈ 𝐽 ∣ 𝑣 ∈ (𝐸‘𝑙)})) | ||
Theorem | vtxdginducedm1fi 26496* | The degree of a vertex 𝑣 in the induced subgraph 𝑆 of a pseudograph 𝐺 of finite size obtained by removing one vertex 𝑁 plus the number of edges joining the vertex 𝑣 and the vertex 𝑁 is the degree of the vertex 𝑣 in the pseudograph 𝐺. (Contributed by AV, 18-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ (𝐸 ∈ Fin → ∀𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) = (((VtxDeg‘𝑆)‘𝑣) + (#‘{𝑙 ∈ 𝐽 ∣ 𝑣 ∈ (𝐸‘𝑙)}))) | ||
Theorem | finsumvtxdg2ssteplem1 26497* | Lemma for finsumvtxdg2sstep 26501. (Contributed by AV, 15-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (#‘𝐸) = ((#‘𝑃) + (#‘𝐽))) | ||
Theorem | finsumvtxdg2ssteplem2 26498* | Lemma for finsumvtxdg2sstep 26501. (Contributed by AV, 12-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → ((VtxDeg‘𝐺)‘𝑁) = ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}}))) | ||
Theorem | finsumvtxdg2ssteplem3 26499* | Lemma for finsumvtxdg2sstep 26501. (Contributed by AV, 19-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖 ∈ 𝐽 ∣ 𝑣 ∈ (𝐸‘𝑖)}) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}})) = (#‘𝐽)) | ||
Theorem | finsumvtxdg2ssteplem4 26500* | Lemma for finsumvtxdg2sstep 26501. (Contributed by AV, 12-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) ∧ Σ𝑣 ∈ 𝐾 ((VtxDeg‘𝑆)‘𝑣) = (2 · (#‘𝑃))) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) + ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}}))) = (2 · ((#‘𝑃) + (#‘𝐽)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |