Home | Metamath
Proof Explorer Theorem List (p. 265 of 424) | < 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: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | el2wlkonotot1 26401 | A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 8-Mar-2018.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝑅(𝑉 2WalksOnOt 𝐸)𝑆) ↔ (𝐴 = 𝑅 ∧ 𝐶 = 𝑆 ∧ 〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶)))) | ||
Theorem | 2wlkonot3v 26402 | If an ordered triple represents a walk of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018.) |
⊢ (𝑇 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))) | ||
Theorem | 2spthonot3v 26403 | If an ordered triple represents a simple path of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) |
⊢ (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))) | ||
Theorem | 2wlkonotv 26404 | If an ordered tripple represents a walk of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018.) |
⊢ (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) | ||
Theorem | el2wlksoton 26405* | A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 21-Feb-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑇 ∈ (𝑉 2WalksOt 𝐸) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑇 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏))) | ||
Theorem | el2spthsoton 26406* | A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 1-Mar-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑇 ∈ (𝑉 2SPathsOt 𝐸) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑇 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏))) | ||
Theorem | el2wlksot 26407* | A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 21-Feb-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑇 ∈ (𝑉 2WalksOt 𝐸) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑇 = 〈𝑎, 𝑏, 𝑐〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) | ||
Theorem | el2pthsot 26408* | A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 28-Feb-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑇 ∈ (𝑉 2SPathsOt 𝐸) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑇 = 〈𝑎, 𝑏, 𝑐〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))) | ||
Theorem | el2wlksotot 26409* | A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 26-Feb-2018.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝑉 2WalksOt 𝐸) ↔ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) | ||
Theorem | usg2wlkonot 26410 | A walk of length 2 between two vertices as ordered triple in an undirected simple graph. This theorem would also hold for undirected multigraphs, but to prove this the cases 𝐴 = 𝐵 and/or 𝐵 = 𝐶 must be considered separately. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) | ||
Theorem | usg2wotspth 26411* | A walk of length 2 between two different vertices as ordered triple corresponds to a simple path of length 2 in an undirected simple graph. (Contributed by Alexander van der Vekens, 16-Feb-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) | ||
Theorem | 2pthwlkonot 26412 | For two different vertices, a walk of length 2 between these vertices as ordered triple is a simple path of length 2 between these vertices as ordered triple in an undirected simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐴(𝑉 2SPathOnOt 𝐸)𝐵) = (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) | ||
Theorem | 2wot2wont 26413* | The set of (simple) paths of length 2 (in a graph) is the set of (simple) paths of length 2 between any two different vertices. (Contributed by Alexander van der Vekens, 27-Feb-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 2WalksOt 𝐸) = ∪ 𝑥 ∈ 𝑉 ∪ 𝑦 ∈ 𝑉 (𝑥(𝑉 2WalksOnOt 𝐸)𝑦)) | ||
Theorem | 2spontn0vne 26414 | If the set of simple paths of length 2 between two vertices (in a graph) is not empty, the two vertices must be not equal. (Contributed by Alexander van der Vekens, 3-Mar-2018.) |
⊢ ((𝑋(𝑉 2SPathOnOt 𝐸)𝑌) ≠ ∅ → 𝑋 ≠ 𝑌) | ||
Theorem | usg2spthonot 26415 | A simple path of length 2 between two vertices as ordered triple corresponds to two adjacent edges in an undirected simple graph. (Contributed by Alexander van der Vekens, 8-Mar-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) ↔ (𝐴 ≠ 𝐶 ∧ {𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) | ||
Theorem | usg2spthonot0 26416 | A simple path of length 2 between two vertices as ordered triple corresponds to two adjacent edges in an undirected simple graph. (Contributed by Alexander van der Vekens, 8-Mar-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝑆, 𝐵, 𝑇〉 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) ↔ ((𝑆 = 𝐴 ∧ 𝑇 = 𝐶 ∧ 𝐴 ≠ 𝐶) ∧ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))) | ||
Theorem | usg2spthonot1 26417* | A simple path of length 2 between two vertices as ordered triple corresponds to two adjacent edges in an undirected simple graph. (Contributed by Alexander van der Vekens, 9-Mar-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) ↔ ∃𝑏 ∈ 𝑉 ((𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ 𝐴 ≠ 𝐶) ∧ ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝐶} ∈ ran 𝐸)))) | ||
Theorem | 2spot2iun2spont 26418* | The set of simple paths of length 2 (in a graph) is the double union of the simple paths of length 2 between different vertices. (Contributed by Alexander van der Vekens, 3-Mar-2018.) |
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 2SPathsOt 𝐸) = ∪ 𝑥 ∈ 𝑉 ∪ 𝑦 ∈ (𝑉 ∖ {𝑥})(𝑥(𝑉 2SPathOnOt 𝐸)𝑦)) | ||
Theorem | 2spotfi 26419 | In a finite graph, the set of simple paths of length 2 between two vertices (as ordered triples) is finite. (Contributed by Alexander van der Vekens, 4-Mar-2018.) |
⊢ (((𝑉 ∈ Fin ∧ 𝐸 ∈ 𝑋) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉 2SPathOnOt 𝐸)𝐵) ∈ Fin) | ||
Syntax | cvdg 26420 | Extend class notation with the vertex degree function. |
class VDeg | ||
Definition | df-vdgr 26421* | Define the vertex degree function (for an undirected multigraph). To be appropriate for multigraphs, 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.) |
⊢ VDeg = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑢 ∈ 𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})))) | ||
Theorem | vdgrfval 26422* | The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) → (𝑉 VDeg 𝐸) = (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})))) | ||
Theorem | vdgrval 26423* | The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) |
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑈 ∈ 𝑉) → ((𝑉 VDeg 𝐸)‘𝑈) = ((#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}}))) | ||
Theorem | vdgrfival 26424* | The value of the vertex degree function (for graphs of finite size). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.) |
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ Fin) ∧ 𝑈 ∈ 𝑉) → ((𝑉 VDeg 𝐸)‘𝑈) = ((#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) + (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}}))) | ||
Theorem | vdgrf 26425 | The vertex degree function is a function from vertices to nonnegative integers or plus infinity. (Contributed by Alexander van der Vekens, 20-Dec-2017.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) → (𝑉 VDeg 𝐸):𝑉⟶(ℕ0 ∪ {+∞})) | ||
Theorem | vdgrfif 26426 | 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.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ Fin) → (𝑉 VDeg 𝐸):𝑉⟶ℕ0) | ||
Theorem | vdgr0 26427 | The degree of a vertex in an empty graph is zero, because there are no edges. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑈 ∈ 𝑉) → ((𝑉 VDeg ∅)‘𝑈) = 0) | ||
Theorem | vdgrun 26428 | 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.) |
⊢ (𝜑 → 𝐸 Fn 𝐴) & ⊢ (𝜑 → 𝐹 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → 𝑉 UMGrph 𝐸) & ⊢ (𝜑 → 𝑉 UMGrph 𝐹) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑉 VDeg (𝐸 ∪ 𝐹))‘𝑈) = (((𝑉 VDeg 𝐸)‘𝑈) +𝑒 ((𝑉 VDeg 𝐹)‘𝑈))) | ||
Theorem | vdgrfiun 26429 | The degree of a vertex in the union of two graphs (of finite size) 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-Jan-2018.) |
⊢ (𝜑 → 𝐸 Fn 𝐴) & ⊢ (𝜑 → 𝐹 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → 𝑉 UMGrph 𝐸) & ⊢ (𝜑 → 𝑉 UMGrph 𝐹) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑉 VDeg (𝐸 ∪ 𝐹))‘𝑈) = (((𝑉 VDeg 𝐸)‘𝑈) + ((𝑉 VDeg 𝐹)‘𝑈))) | ||
Theorem | vdgr1d 26430 | The vertex degree of a one-edge graph, case 4: an edge from a vertex to itself contributes two to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) |
⊢ (𝜑 → 𝑉 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑉 VDeg {〈𝐴, {𝑈}〉})‘𝑈) = 2) | ||
Theorem | vdgr1b 26431 | 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.) |
⊢ (𝜑 → 𝑉 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ≠ 𝑈) ⇒ ⊢ (𝜑 → ((𝑉 VDeg {〈𝐴, {𝑈, 𝐵}〉})‘𝑈) = 1) | ||
Theorem | vdgr1c 26432 | 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.) |
⊢ (𝜑 → 𝑉 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ≠ 𝑈) ⇒ ⊢ (𝜑 → ((𝑉 VDeg {〈𝐴, {𝐵, 𝑈}〉})‘𝑈) = 1) | ||
Theorem | vdgr1a 26433 | 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.) |
⊢ (𝜑 → 𝑉 ∈ V) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ≠ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ≠ 𝑈) ⇒ ⊢ (𝜑 → ((𝑉 VDeg {〈𝐴, {𝐵, 𝐶}〉})‘𝑈) = 0) | ||
Theorem | vdusgraval 26434* | The value of the vertex degree function for simple undirected graphs. (Contributed by Alexander van der Vekens, 20-Dec-2017.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ((𝑉 VDeg 𝐸)‘𝑈) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)})) | ||
Theorem | vdusgra0nedg 26435* | 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, 8-Dec-2017.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → (((𝑉 VDeg 𝐸)‘𝑈) = 0 → ¬ ∃𝑣 ∈ 𝑉 {𝑈, 𝑣} ∈ ran 𝐸)) | ||
Theorem | vdgrnn0pnf 26436 | The degree of a vertex is either a nonnegative integer or positive infinity. (Contributed by Alexander van der Vekens, 30-Dec-2017.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉) → ((𝑉 VDeg 𝐸)‘𝑋) ∈ (ℕ0 ∪ {+∞})) | ||
Theorem | usgfidegfi 26437* | In a finite graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) → ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ∈ ℕ0) | ||
Theorem | usgfiregdegfi 26438* | In a finite graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 6-Mar-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → 𝐾 ∈ ℕ0)) | ||
Theorem | hashnbgravd 26439 | The size of the set of the neighbors of a vertex is the vertex degree of this vertex. (Contributed by Alexander van der Vekens, 17-Dec-2017.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑈)) = ((𝑉 VDeg 𝐸)‘𝑈)) | ||
Theorem | hashnbgravdg 26440 | The size of the set of the neighbors of a vertex is the vertex degree of this vertex, analogous to hashnbgravd 26439. (Contributed by Alexander van der Vekens, 20-Dec-2017.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑈)) = ((𝑉 VDeg 𝐸)‘𝑈)) | ||
Theorem | nbhashnn0 26441 | The number of the neighbors of a vertex in a finite undirected simple graph is a nonnegative integer. (Contributed by Alexander van der Vekens, 14-Jul-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) ∈ ℕ0) | ||
Theorem | nbhashuvtx1 26442 | If the number of the neighbors of a vertex in a finite graph is the number of vertices of the graph minus 1, each vertex except the first mentioned vertex is a neighbor of this vertex. (Contributed by Alexander van der Vekens, 14-Jul-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) = ((#‘𝑉) − 1) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁) → 𝑀 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁)))) | ||
Theorem | nbhashuvtx 26443 | If the number of the neighbors of a vertex in a graph is the number of vertices of the graph minus 1, the vertex is universal. (Contributed by Alexander van der Vekens, 14-Jul-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) = ((#‘𝑉) − 1) → 𝑁 ∈ (𝑉 UnivVertex 𝐸))) | ||
Theorem | uvtxhashnb 26444 | A universal vertex has 𝑛 − 1 neighbors in a graph with 𝑛 vertices, a biconditional version of uvtxnm1nbgra 26022. (Contributed by Alexander van der Vekens, 14-Jul-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝑁 ∈ (𝑉 UnivVertex 𝐸) ↔ (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) = ((#‘𝑉) − 1))) | ||
Theorem | usgravd0nedg 26445* | If a vertex in a simple graph has degree 0, the vertex is not adjacent to another vertex via an edge, analogous to vdusgra0nedg 26435. (Contributed by Alexander van der Vekens, 20-Dec-2017.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (((𝑉 VDeg 𝐸)‘𝑈) = 0 → ¬ ∃𝑣 ∈ 𝑉 {𝑈, 𝑣} ∈ ran 𝐸)) | ||
Theorem | usgravd00 26446* | 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.) |
⊢ (𝑉 USGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 0 → 𝐸 = ∅)) | ||
Theorem | usgrauvtxvdbi 26447 | In a finite undirected simple graph with n vertices a vertex is universal if the vertex has degree 𝑛 − 1. (Contributed by Alexander van der Vekens, 14-Jul-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝐾 ∈ 𝑉) → (𝐾 ∈ (𝑉 UnivVertex 𝐸) ↔ ((𝑉 VDeg 𝐸)‘𝐾) = ((#‘𝑉) − 1))) | ||
Theorem | vdiscusgra 26448* | In a finite complete undirected simple graph with n vertices every vertex has degree 𝑛 − 1. (Contributed by Alexander van der Vekens, 14-Jul-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = ((#‘𝑉) − 1) → 𝑉 ComplUSGrph 𝐸)) | ||
Syntax | crgra 26449 | Extend class notation to include the class of all regular graphs. |
class RegGrph | ||
Syntax | crusgra 26450 | Extend class notation to include the class of all regular undirected simple graphs. |
class RegUSGrph | ||
Definition | df-rgra 26451* | Define the class of k-regular "graphs". (Contributed by Alexander van der Vekens, 6-Jul-2018.) |
⊢ RegGrph = {〈〈𝑣, 𝑒〉, 𝑘〉 ∣ (𝑘 ∈ ℕ0 ∧ ∀𝑝 ∈ 𝑣 ((𝑣 VDeg 𝑒)‘𝑝) = 𝑘)} | ||
Definition | df-rusgra 26452* | Define the class of k-regular undirected simple graphs. (Contributed by Alexander van der Vekens, 6-Jul-2018.) |
⊢ RegUSGrph = {〈〈𝑣, 𝑒〉, 𝑘〉 ∣ (𝑣 USGrph 𝑒 ∧ 〈𝑣, 𝑒〉 RegGrph 𝑘)} | ||
Theorem | isrgra 26453* | The property of being a k-regular graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐾 ∈ 𝑍) → (〈𝑉, 𝐸〉 RegGrph 𝐾 ↔ (𝐾 ∈ ℕ0 ∧ ∀𝑝 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑝) = 𝐾))) | ||
Theorem | isrusgra 26454* | The property of being a k-regular undirected simple graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐾 ∈ 𝑍) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 ↔ (𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧ ∀𝑝 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑝) = 𝐾))) | ||
Theorem | rgraprop 26455* | The properties of a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) |
⊢ (〈𝑉, 𝐸〉 RegGrph 𝐾 → (𝐾 ∈ ℕ0 ∧ ∀𝑝 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑝) = 𝐾)) | ||
Theorem | rusgraprop 26456* | The properties of a k-regular undirected simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) |
⊢ (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧ ∀𝑝 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑝) = 𝐾)) | ||
Theorem | rusgrargra 26457 | A k-regular undirected simple graph is a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) |
⊢ (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 〈𝑉, 𝐸〉 RegGrph 𝐾) | ||
Theorem | rusisusgra 26458 | Any k-regular undirected simple graph is an undirected simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) |
⊢ (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝑉 USGrph 𝐸) | ||
Theorem | isrusgusrg 26459 | A graph is a k-regular undirected simple graph iff it is an undirected simple graph and a k-regular graph. (Contributed by AV, 3-Jan-2020.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐾 ∈ 𝑍) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 ↔ (𝑉 USGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegGrph 𝐾))) | ||
Theorem | isrusgusrgcl 26460 | A graph represented by a class is a k-regular undirected simple graph iff it is an undirected simple graph and a k-regular graph. (Contributed by AV, 2-Jan-2020.) |
⊢ ((𝐺 ∈ (𝑋 × 𝑌) ∧ 𝐾 ∈ 𝑍) → (𝐺 RegUSGrph 𝐾 ↔ (𝐺 ∈ USGrph ∧ 𝐺 RegGrph 𝐾))) | ||
Theorem | isrgrac 26461* | The property of being a k-regular graph represented by a class. (Contributed by AV, 3-Jan-2020.) |
⊢ ((𝐺 ∈ (𝑋 × 𝑌) ∧ 𝐾 ∈ 𝑍) → (𝐺 RegGrph 𝐾 ↔ (𝐾 ∈ ℕ0 ∧ ∀𝑝 ∈ (1st ‘𝐺)(( VDeg ‘𝐺)‘𝑝) = 𝐾))) | ||
Theorem | isrusgrac 26462* | The property of being a k-regular undirected simple graph represented by a class. (Contributed by AV, 3-Jan-2020.) |
⊢ ((𝐺 ∈ (𝑋 × 𝑌) ∧ 𝐾 ∈ 𝑍) → (𝐺 RegUSGrph 𝐾 ↔ (𝐺 ∈ USGrph ∧ 𝐾 ∈ ℕ0 ∧ ∀𝑝 ∈ (1st ‘𝐺)(( VDeg ‘𝐺)‘𝑝) = 𝐾))) | ||
Theorem | 0egra0rgra 26463 | A graph is 0-regular if it has no edges. (Contributed by Alexander van der Vekens, 8-Jul-2018.) |
⊢ ∀𝑣〈𝑣, ∅〉 RegGrph 0 | ||
Theorem | 0vgrargra 26464* | A graph with no vertices is k-regular for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018.) |
⊢ (𝐸 ∈ 𝑉 → ∀𝑘 ∈ ℕ0 〈∅, 𝐸〉 RegGrph 𝑘) | ||
Theorem | cusgraisrusgra 26465 | A complete undirected simple graph with n vertices (at least one) is (n-1)-regular. (Contributed by Alexander van der Vekens, 10-Jul-2018.) |
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 〈𝑉, 𝐸〉 RegUSGrph ((#‘𝑉) − 1)) | ||
Theorem | 0eusgraiff0rgra 26466 | An undirected simple graph is 0-regular iff it has no edges. (Contributed by Alexander van der Vekens, 12-Jul-2018.) |
⊢ (𝑉 USGrph 𝐸 → (〈𝑉, 𝐸〉 RegGrph 0 ↔ 𝐸 = ∅)) | ||
Theorem | cusgraiffrusgra 26467 | A finite undirected simple graph with n vertices is complete iff it is (n-1)-regular. Hint: If the definition of RegGrph allowed for 𝑘 ∈ ℤ, then the assumption 𝑉 ≠ ∅ could be removed. Furthermore, if the definition of RegGrph also allowed for 𝑘 ∈ (ℤ ∪ {+∞}), then the theorem would also hold for inifinite graphs. (Contributed by Alexander van der Vekens, 14-Jul-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝑉 ComplUSGrph 𝐸 ↔ 〈𝑉, 𝐸〉 RegUSGrph ((#‘𝑉) − 1))) | ||
Theorem | 0eusgraiff0rgracl 26468 | An undirected simple graph represented by a class is 0-regular iff it has no edges. (Contributed by AV, 3-Jan-2020.) |
⊢ (𝐺 ∈ USGrph → (𝐺 RegGrph 0 ↔ (Edges‘𝐺) = ∅)) | ||
Theorem | rusgraprop2 26469* | The properties of a k-regular undirected simple graph expressed with neighbors. (Contributed by Alexander van der Vekens, 26-Jul-2018.) |
⊢ (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧ ∀𝑝 ∈ 𝑉 (#‘(〈𝑉, 𝐸〉 Neighbors 𝑝)) = 𝐾)) | ||
Theorem | rusgraprop3 26470* | The properties of a k-regular undirected simple graph expressed with edges. (Contributed by Alexander van der Vekens, 26-Jul-2018.) |
⊢ (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧ ∀𝑝 ∈ 𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑝, 𝑛} ∈ ran 𝐸}) = 𝐾)) | ||
Theorem | rusgraprop4 26471* | The properties of a k-regular undirected simple graph expressed with trailing edges of walks (as words). (Contributed by Alexander van der Vekens, 2-Aug-2018.) |
⊢ (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧ ∀𝑝 ∈ Word 𝑉(𝑝 ≠ ∅ → (#‘{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑝), 𝑛} ∈ ran 𝐸}) = 𝐾))) | ||
Theorem | rusgrasn 26472 | If a k-regular undirected simple graph has only one vertex, then k must be 0. (Contributed by Alexander van der Vekens, 4-Sep-2018.) |
⊢ (((#‘𝑉) = 1 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → 𝐾 = 0) | ||
Theorem | rusgranumwwlkl1 26473* | In a k-regular graph, the number of walks of length 1 represented as words (thus the number of edges) starting at a fixed vertex is k. (Contributed by Alexander van der Vekens, 28-Jul-2018.) (Proof shortened by AV, 4-May-2021.) |
⊢ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → (#‘{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ ran 𝐸)}) = 𝐾) | ||
Theorem | rusgranumwlkl1 26474* | In a k-regular graph, there are k walks (as word) of length 1 starting at each vertex. (Contributed by Alexander van der Vekens, 28-Jul-2018.) |
⊢ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘1) ∣ (𝑤‘0) = 𝑃}) = 𝐾) | ||
Theorem | rusgranumwlklem0 26475* | Lemma 0 for rusgranumwlk 26484. (Contributed by Alexander van der Vekens, 23-Aug-2018.) |
⊢ (𝑌 ∈ {𝑤 ∈ 𝑍 ∣ (𝑤‘0) = 𝑃} → {𝑤 ∈ 𝑋 ∣ (𝜑 ∧ 𝜓)} = {𝑤 ∈ 𝑋 ∣ (𝜑 ∧ (𝑌‘0) = 𝑃 ∧ 𝜓)}) | ||
Theorem | rusgranumwlklem1 26476* | Lemma 1 for rusgranumwlk 26484. (Contributed by Alexander van der Vekens, 21-Jul-2018.) |
⊢ 𝑊 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑐)) = 𝑛}) ⇒ ⊢ (𝑅 ∈ (𝑊‘𝑁) → (𝑅 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st ‘𝑅)) = 𝑁)) | ||
Theorem | rusgranumwlklem2 26477* | Lemma 2 for rusgranumwlk 26484. (Contributed by Alexander van der Vekens, 21-Jul-2018.) |
⊢ 𝑊 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑐)) = 𝑛}) & ⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ (#‘{𝑤 ∈ (𝑊‘𝑛) ∣ ((2nd ‘𝑤)‘0) = 𝑣})) ⇒ ⊢ ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑃𝐿𝑁) = (#‘{𝑤 ∈ (𝑊‘𝑁) ∣ ((2nd ‘𝑤)‘0) = 𝑃})) | ||
Theorem | rusgranumwlklem3 26478* | Lemma 3 for rusgranumwlk 26484. (Contributed by Alexander van der Vekens, 21-Jul-2018.) |
⊢ 𝑊 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑐)) = 𝑛}) & ⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ (#‘{𝑤 ∈ (𝑊‘𝑛) ∣ ((2nd ‘𝑤)‘0) = 𝑣})) ⇒ ⊢ ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑃𝐿𝑁) = (#‘{𝑤 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑃)})) | ||
Theorem | rusgranumwlklem4 26479* | Lemma 4 for rusgranumwlk 26484. (Contributed by Alexander van der Vekens, 24-Jul-2018.) (Proof shortened by AV, 5-May-2021.) |
⊢ 𝑊 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑐)) = 𝑛}) & ⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ (#‘{𝑤 ∈ (𝑊‘𝑛) ∣ ((2nd ‘𝑤)‘0) = 𝑣})) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑃𝐿𝑁) = (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃})) | ||
Theorem | rusgranumwlkb0 26480* | Induction base 0 for rusgranumwlk 26484. Here, we do not need the regularity of the graph yet. (Contributed by Alexander van der Vekens, 24-Jul-2018.) |
⊢ 𝑊 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑐)) = 𝑛}) & ⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ (#‘{𝑤 ∈ (𝑊‘𝑛) ∣ ((2nd ‘𝑤)‘0) = 𝑣})) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉) → (𝑃𝐿0) = 1) | ||
Theorem | rusgranumwlkb1 26481* | Induction base 1 for rusgranumwlk 26484. (Contributed by Alexander van der Vekens, 28-Jul-2018.) |
⊢ 𝑊 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑐)) = 𝑛}) & ⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ (#‘{𝑤 ∈ (𝑊‘𝑛) ∣ ((2nd ‘𝑤)‘0) = 𝑣})) ⇒ ⊢ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑃 ∈ 𝑉) → (𝑃𝐿1) = 𝐾) | ||
Theorem | rusgra0edg 26482* | Special case for graphs without edges: There are no walks of length greater than 0. (Contributed by Alexander van der Vekens, 26-Jul-2018.) |
⊢ 𝑊 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑐)) = 𝑛}) & ⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ (#‘{𝑤 ∈ (𝑊‘𝑛) ∣ ((2nd ‘𝑤)‘0) = 𝑣})) ⇒ ⊢ ((〈𝑉, 𝐸〉 RegUSGrph 0 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑃𝐿𝑁) = 0) | ||
Theorem | rusgranumwlks 26483* | Induction step for rusgranumwlk 26484. (Contributed by Alexander van der Vekens, 24-Aug-2018.) |
⊢ 𝑊 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑐)) = 𝑛}) & ⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ (#‘{𝑤 ∈ (𝑊‘𝑛) ∣ ((2nd ‘𝑤)‘0) = 𝑣})) ⇒ ⊢ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑃𝐿𝑁) = (𝐾↑𝑁) → (𝑃𝐿(𝑁 + 1)) = (𝐾↑(𝑁 + 1)))) | ||
Theorem | rusgranumwlk 26484* | In a k-regular graph, the number of walks of a fixed length n from a fixed vertex is k to the power of n. We denote with (𝑊‘𝑛) the set of walks with length n (in a given undirected simple graph) and with (𝑣𝐿𝑛) the number of walks with length n starting at the vertex v. This theorem corresponds to statement 11 in [Huneke] p. 2: "The total number of walks v(0) v(1) ... v(n-2) from a fixed vertex v = v(0) is k^(n-2) as G is k-regular.". Because of the k-regularity, the walk can be continued in k different ways at each vertex in the walk, therefore n times. This theorem even holds for n=0: then the walk consists only of one vertex v(0), so the number of walks of length n=0 starting with v=v(0) is 1=k^0. (Contributed by Alexander van der Vekens, 24-Aug-2018.) |
⊢ 𝑊 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑐)) = 𝑛}) & ⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ (#‘{𝑤 ∈ (𝑊‘𝑛) ∣ ((2nd ‘𝑤)‘0) = 𝑣})) ⇒ ⊢ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (𝑃𝐿𝑁) = (𝐾↑𝑁)) | ||
Theorem | rusgranumwlkg 26485* | In a k-regular graph, the number of walks of a fixed length n from a fixed vertex is k to the power of n. This theorem corresponds to statement 11 in [Huneke] p. 2: "The total number of walks v(0) v(1) ... v(n-2) from a fixed vertex v = v(0) is k^(n-2) as G is k-regular.". This theorem even holds for n=0: then the walk consists only of one vertex v(0), so the number of walks of length n=0 starting with v=v(0) is 1=k^0. Closed form of rusgranumwlk 26484. (Contributed by Alexander van der Vekens, 24-Aug-2018.) |
⊢ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (#‘{𝑤 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑃)}) = (𝐾↑𝑁)) | ||
Theorem | rusgranumwwlkg 26486* | In a k-regular graph, the number of walks (represented by words) of a fixed length n from a fixed vertex is k to the power of n. (Contributed by Alexander van der Vekens, 30-Sep-2018.) (Proof shortened by AV, 5-May-2021.) |
⊢ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) = (𝐾↑𝑁)) | ||
Theorem | clwlknclwlkdifs 26487 | The set of walks of length n starting with a fixed vertex and ending not at this vertex is the difference between the set of walks of length n starting with this vertex and the set of walks of length n starting with this vertex and ending at this vertex. (Contributed by Alexander van der Vekens, 30-Sep-2018.) |
⊢ 𝐴 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)} & ⊢ 𝐵 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)} ⇒ ⊢ 𝐴 = ({𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋} ∖ 𝐵) | ||
Theorem | clwlknclwlkdifnum 26488* | In a k-regular graph, the size of the set of walks of length n starting with a fixed vertex and ending not at this vertex is the difference between k to the power of n and the size of the set of walks of length n starting with this vertex and ending at this vertex. (Contributed by Alexander van der Vekens, 30-Sep-2018.) |
⊢ 𝐴 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)} & ⊢ 𝐵 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)} ⇒ ⊢ (((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (#‘𝐴) = ((𝐾↑𝑁) − (#‘𝐵))) | ||
Syntax | ceup 26489 | Extend class notation with Eulerian paths. |
class EulPaths | ||
Definition | df-eupa 26490* | Define the set of all Eulerian paths on an undirected multigraph. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ EulPaths = (𝑣 ∈ V, 𝑒 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑣 UMGrph 𝑒 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom 𝑒 ∧ 𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}))}) | ||
Theorem | releupa 26491 | The set (𝑉 EulPaths 𝐸) of all Eulerian paths on 〈𝑉, 𝐸〉 is a set of pairs by our definition of an Eulerian path, and so is a relation. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ Rel (𝑉 EulPaths 𝐸) | ||
Theorem | iseupa 26492* | The property "〈𝐹, 𝑃〉 is an Eulerian path on the graph 〈𝑉, 𝐸〉". An Eulerian path is defined as bijection 𝐹 from the edges to a set 1...𝑁 a function 𝑃:(0...𝑁)⟶𝑉 into the vertices such that for each 1 ≤ 𝑘 ≤ 𝑁, 𝐹(𝑘) is an edge from 𝑃(𝑘 − 1) to 𝑃(𝑘). (Since the edges are undirected and there are possibly many edges between any two given vertices, we need to list both the edges and the vertices of the path separately.) (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) |
⊢ (dom 𝐸 = 𝐴 → (𝐹(𝑉 EulPaths 𝐸)𝑃 ↔ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})))) | ||
Theorem | eupagra 26493 | If an eulerian path exists, then 〈𝑉, 𝐸〉 is a graph. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ (𝐹(𝑉 EulPaths 𝐸)𝑃 → 𝑉 UMGrph 𝐸) | ||
Theorem | eupai 26494* | Properties of an Eulerian path. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ ((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) → (((#‘𝐹) ∈ ℕ0 ∧ 𝐹:(1...(#‘𝐹))–1-1-onto→𝐴 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ ∀𝑘 ∈ (1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})) | ||
Theorem | eupatrl 26495* |
An Eulerian path is a trail.
Unfortunately, the edge function 𝐹 of an Eulerian path has the domain (1...(#‘𝐹)), whereas the edge functions of all kinds of walks defined here have the domain (0..^(#‘𝐹)) (i.e. the edge functions are "words of edge indices", see discussion and proposal of Mario Carneiro at https://groups.google.com/d/msg/metamath/KdVXdL3IH3k/2-BYcS_ACQAJ). Therefore, the arguments of the edge function of an Eulerian path must be shifted by 1 to obtain an edge function of a trail in this theorem, using the auxiliary theorems above (fargshiftlem 26162, fargshiftfv 26163, etc.). TODO: The definition of an Eulerian path and all related theorems should be modified to fit to the general definition of a trail. (Contributed by Alexander van der Vekens, 24-Nov-2017.) |
⊢ 𝐺 = (𝑥 ∈ (0..^(#‘𝐹)) ↦ (𝐹‘(𝑥 + 1))) ⇒ ⊢ (𝐹(𝑉 EulPaths 𝐸)𝑃 → 𝐺(𝑉 Trails 𝐸)𝑃) | ||
Theorem | eupacl 26496 | An Eulerian path has length #(𝐹), which is an integer. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ (𝐹(𝑉 EulPaths 𝐸)𝑃 → (#‘𝐹) ∈ ℕ0) | ||
Theorem | eupaf1o 26497 | The 𝐹 function in an Eulerian path is a bijection from a one-based sequence to the set of edges. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ ((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) → 𝐹:(1...(#‘𝐹))–1-1-onto→𝐴) | ||
Theorem | eupafi 26498 | Any graph with an Eulerian path is finite. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ ((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) → 𝐴 ∈ Fin) | ||
Theorem | eupapf 26499 | The 𝑃 function in an Eulerian path is a function from a zero-based finite sequence to the vertices. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ (𝐹(𝑉 EulPaths 𝐸)𝑃 → 𝑃:(0...(#‘𝐹))⟶𝑉) | ||
Theorem | eupaseg 26500 | The 𝑁-th edge in an eulerian path is the edge from 𝑃(𝑁 − 1) to 𝑃(𝑁). (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ ((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝑁 ∈ (1...(#‘𝐹))) → (𝐸‘(𝐹‘𝑁)) = {(𝑃‘(𝑁 − 1)), (𝑃‘𝑁)}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |