![]() |
Metamath
Proof Explorer Theorem List (p. 298 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wlkreslem 29701 | Lemma for wlkres 29702. (Contributed by AV, 5-Mar-2021.) (Revised by AV, 30-Nov-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) ⇒ ⊢ (𝜑 → 𝑆 ∈ V) | ||
Theorem | wlkres 29702 | The restriction 〈𝐻, 𝑄〉 of a walk 〈𝐹, 𝑃〉 to an initial segment of the walk (of length 𝑁) forms a walk on the subgraph 𝑆 consisting of the edges in the initial segment. Formerly proven directly for Eulerian paths, see eupthres 30243. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 5-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ 𝐻 = (𝐹 prefix 𝑁) & ⊢ 𝑄 = (𝑃 ↾ (0...𝑁)) ⇒ ⊢ (𝜑 → 𝐻(Walks‘𝑆)𝑄) | ||
Theorem | redwlklem 29703 | Lemma for redwlk 29704. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.) |
⊢ ((𝐹 ∈ Word 𝑆 ∧ 1 ≤ (♯‘𝐹) ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) → (𝑃 ↾ (0..^(♯‘𝐹))):(0...(♯‘(𝐹 ↾ (0..^((♯‘𝐹) − 1)))))⟶𝑉) | ||
Theorem | redwlk 29704 | A walk ending at the last but one vertex of the walk is a walk. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.) |
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 1 ≤ (♯‘𝐹)) → (𝐹 ↾ (0..^((♯‘𝐹) − 1)))(Walks‘𝐺)(𝑃 ↾ (0..^(♯‘𝐹)))) | ||
Theorem | wlkp1lem1 29705 | Lemma for wlkp1 29713. (Contributed by AV, 6-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) & ⊢ 𝑁 = (♯‘𝐹) ⇒ ⊢ (𝜑 → ¬ (𝑁 + 1) ∈ dom 𝑃) | ||
Theorem | wlkp1lem2 29706 | Lemma for wlkp1 29713. (Contributed by AV, 6-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) & ⊢ 𝑁 = (♯‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) ⇒ ⊢ (𝜑 → (♯‘𝐻) = (𝑁 + 1)) | ||
Theorem | wlkp1lem3 29707 | Lemma for wlkp1 29713. (Contributed by AV, 6-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) & ⊢ 𝑁 = (♯‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) ⇒ ⊢ (𝜑 → ((iEdg‘𝑆)‘(𝐻‘𝑁)) = ((𝐼 ∪ {〈𝐵, 𝐸〉})‘𝐵)) | ||
Theorem | wlkp1lem4 29708 | Lemma for wlkp1 29713. (Contributed by AV, 6-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) & ⊢ 𝑁 = (♯‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) & ⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) ⇒ ⊢ (𝜑 → (𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V)) | ||
Theorem | wlkp1lem5 29709* | Lemma for wlkp1 29713. (Contributed by AV, 6-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) & ⊢ 𝑁 = (♯‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) & ⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0...𝑁)(𝑄‘𝑘) = (𝑃‘𝑘)) | ||
Theorem | wlkp1lem6 29710* | Lemma for wlkp1 29713. (Contributed by AV, 6-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) & ⊢ 𝑁 = (♯‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) & ⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑁)((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘)))) | ||
Theorem | wlkp1lem7 29711 | Lemma for wlkp1 29713. (Contributed by AV, 6-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) & ⊢ 𝑁 = (♯‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) & ⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) ⇒ ⊢ (𝜑 → {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁))) | ||
Theorem | wlkp1lem8 29712* | Lemma for wlkp1 29713. (Contributed by AV, 6-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) & ⊢ 𝑁 = (♯‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) & ⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) & ⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶}) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)))) | ||
Theorem | wlkp1 29713 | Append one path segment (edge) 𝐸 from vertex (𝑃‘𝑁) to a vertex 𝐶 to a walk 〈𝐹, 𝑃〉 to become a walk 〈𝐻, 𝑄〉 of the supergraph 𝑆 obtained by adding the new edge to the graph 𝐺. Formerly proven directly for Eulerian paths (for pseudographs), see eupthp1 30244. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 6-Mar-2021.) (Proof shortened by AV, 18-Apr-2021.) (Revised by AV, 8-Apr-2024.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) & ⊢ 𝑁 = (♯‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) & ⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) & ⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶}) ⇒ ⊢ (𝜑 → 𝐻(Walks‘𝑆)𝑄) | ||
Theorem | wlkdlem1 29714* | Lemma 1 for wlkd 29718. (Contributed by AV, 7-Feb-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ (𝜑 → 𝐹 ∈ Word V) & ⊢ (𝜑 → (♯‘𝑃) = ((♯‘𝐹) + 1)) & ⊢ (𝜑 → ∀𝑘 ∈ (0...(♯‘𝐹))(𝑃‘𝑘) ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶𝑉) | ||
Theorem | wlkdlem2 29715* | Lemma 2 for wlkd 29718. (Contributed by AV, 7-Feb-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ (𝜑 → 𝐹 ∈ Word V) & ⊢ (𝜑 → (♯‘𝑃) = ((♯‘𝐹) + 1)) & ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → (((♯‘𝐹) ∈ ℕ → (𝑃‘(♯‘𝐹)) ∈ (𝐼‘(𝐹‘((♯‘𝐹) − 1)))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ∈ (𝐼‘(𝐹‘𝑘)))) | ||
Theorem | wlkdlem3 29716* | Lemma 3 for wlkd 29718. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ (𝜑 → 𝐹 ∈ Word V) & ⊢ (𝜑 → (♯‘𝑃) = ((♯‘𝐹) + 1)) & ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼) | ||
Theorem | wlkdlem4 29717* | Lemma 4 for wlkd 29718. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 23-Jan-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ (𝜑 → 𝐹 ∈ Word V) & ⊢ (𝜑 → (♯‘𝑃) = ((♯‘𝐹) + 1)) & ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) & ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) | ||
Theorem | wlkd 29718* | Two words representing a walk in a graph. (Contributed by AV, 7-Feb-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ (𝜑 → 𝐹 ∈ Word V) & ⊢ (𝜑 → (♯‘𝑃) = ((♯‘𝐹) + 1)) & ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) & ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → ∀𝑘 ∈ (0...(♯‘𝐹))(𝑃‘𝑘) ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) | ||
Theorem | lfgrwlkprop 29719* | Two adjacent vertices in a walk are different in a loop-free graph. (Contributed by AV, 28-Jan-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) | ||
Theorem | lfgriswlk 29720* | Conditions for a pair of functions to be a walk in a loop-free graph. (Contributed by AV, 28-Jan-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))((𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))) | ||
Theorem | lfgrwlknloop 29721* | In a loop-free graph, each walk has no loops! (Contributed by AV, 2-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) | ||
Syntax | ctrls 29722 | Extend class notation with trails (within a graph). |
class Trails | ||
Syntax | ctrlson 29723 | Extend class notation with trails between two vertices (within a graph). |
class TrailsOn | ||
Definition | df-trls 29724* |
Define the set of all Trails (in an undirected graph).
According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A trail is a walk in which all edges are distinct. According to Bollobas: "... walk is called a trail if all its edges are distinct.", see Definition of [Bollobas] p. 5. Therefore, a trail can be represented by an injective mapping f from { 1 , ... , n } and a mapping p from { 0 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the trail is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.) |
⊢ Trails = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(Walks‘𝑔)𝑝 ∧ Fun ◡𝑓)}) | ||
Definition | df-trlson 29725* | Define the collection of trails with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.) |
⊢ TrailsOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(WalksOn‘𝑔)𝑏)𝑝 ∧ 𝑓(Trails‘𝑔)𝑝)})) | ||
Theorem | reltrls 29726 | The set (Trails‘𝐺) of all trails on 𝐺 is a set of pairs by our definition of a trail, and so is a relation. (Contributed by AV, 29-Oct-2021.) |
⊢ Rel (Trails‘𝐺) | ||
Theorem | trlsfval 29727* | The set of trails (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) (Revised by AV, 29-Oct-2021.) |
⊢ (Trails‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓(Walks‘𝐺)𝑝 ∧ Fun ◡𝑓)} | ||
Theorem | istrl 29728 | Conditions for a pair of classes/functions to be a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) (Revised by AV, 29-Oct-2021.) |
⊢ (𝐹(Trails‘𝐺)𝑃 ↔ (𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝐹)) | ||
Theorem | trliswlk 29729 | A trail is a walk. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Proof shortened by AV, 29-Oct-2021.) |
⊢ (𝐹(Trails‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) | ||
Theorem | trlf1 29730 | The enumeration 𝐹 of a trail 〈𝐹, 𝑃〉 is injective. (Contributed by AV, 20-Feb-2021.) (Proof shortened by AV, 29-Oct-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐹(Trails‘𝐺)𝑃 → 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼) | ||
Theorem | trlreslem 29731 | Lemma for trlres 29732. Formerly part of proof of eupthres 30243. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 6-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ 𝐻 = (𝐹 prefix 𝑁) ⇒ ⊢ (𝜑 → 𝐻:(0..^(♯‘𝐻))–1-1-onto→dom (𝐼 ↾ (𝐹 “ (0..^𝑁)))) | ||
Theorem | trlres 29732 | The restriction 〈𝐻, 𝑄〉 of a trail 〈𝐹, 𝑃〉 to an initial segment of the trail (of length 𝑁) forms a trail on the subgraph 𝑆 consisting of the edges in the initial segment. (Contributed by AV, 6-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ 𝐻 = (𝐹 prefix 𝑁) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ 𝑄 = (𝑃 ↾ (0...𝑁)) ⇒ ⊢ (𝜑 → 𝐻(Trails‘𝑆)𝑄) | ||
Theorem | upgrtrls 29733* | The set of trails in a pseudograph, definition of walks expanded. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UPGraph → (Trails‘𝐺) = {〈𝑓, 𝑝〉 ∣ ((𝑓 ∈ Word dom 𝐼 ∧ Fun ◡𝑓) ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) | ||
Theorem | upgristrl 29734* | Properties of a pair of functions to be a trail in a pseudograph, definition of walks expanded. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UPGraph → (𝐹(Trails‘𝐺)𝑃 ↔ ((𝐹 ∈ Word dom 𝐼 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) | ||
Theorem | upgrf1istrl 29735* | Properties of a pair of a one-to-one function into the set of indices of edges and a function into the set of vertices to be a trail in a pseudograph. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UPGraph → (𝐹(Trails‘𝐺)𝑃 ↔ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) | ||
Theorem | wksonproplem 29736* | Lemma for theorems for properties of walks between two vertices, e.g., trlsonprop 29740. (Contributed by AV, 16-Jan-2021.) Remove is-walk hypothesis. (Revised by SN, 13-Dec-2024.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝐴(𝑊‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(𝑂‘𝐺)𝐵)𝑃 ∧ 𝐹(𝑄‘𝐺)𝑃))) & ⊢ 𝑊 = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑂‘𝑔)𝑏)𝑝 ∧ 𝑓(𝑄‘𝑔)𝑝)})) ⇒ ⊢ (𝐹(𝐴(𝑊‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(𝑂‘𝐺)𝐵)𝑃 ∧ 𝐹(𝑄‘𝐺)𝑃))) | ||
Theorem | wksonproplemOLD 29737* | Obsolete version of wksonproplem 29736 as of 13-Dec-2024. (Contributed by AV, 16-Jan-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝐴(𝑊‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(𝑂‘𝐺)𝐵)𝑃 ∧ 𝐹(𝑄‘𝐺)𝑃))) & ⊢ 𝑊 = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑂‘𝑔)𝑏)𝑝 ∧ 𝑓(𝑄‘𝑔)𝑝)})) & ⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑓(𝑄‘𝐺)𝑝) → 𝑓(Walks‘𝐺)𝑝) ⇒ ⊢ (𝐹(𝐴(𝑊‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(𝑂‘𝐺)𝐵)𝑃 ∧ 𝐹(𝑄‘𝐺)𝑃))) | ||
Theorem | trlsonfval 29738* | The set of trails between two vertices. (Contributed by Alexander van der Vekens, 4-Nov-2017.) (Revised by AV, 7-Jan-2021.) (Proof shortened by AV, 15-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(TrailsOn‘𝐺)𝐵) = {〈𝑓, 𝑝〉 ∣ (𝑓(𝐴(WalksOn‘𝐺)𝐵)𝑝 ∧ 𝑓(Trails‘𝐺)𝑝)}) | ||
Theorem | istrlson 29739 | Properties of a pair of functions to be a trail between two given vertices. (Contributed by Alexander van der Vekens, 3-Nov-2017.) (Revised by AV, 7-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Trails‘𝐺)𝑃))) | ||
Theorem | trlsonprop 29740 | Properties of a trail between two vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017.) (Revised by AV, 7-Jan-2021.) (Proof shortened by AV, 16-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Trails‘𝐺)𝑃))) | ||
Theorem | trlsonistrl 29741 | A trail between two vertices is a trail. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 7-Jan-2021.) |
⊢ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 → 𝐹(Trails‘𝐺)𝑃) | ||
Theorem | trlsonwlkon 29742 | A trail between two vertices is a walk between these vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017.) (Revised by AV, 7-Jan-2021.) |
⊢ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃) | ||
Theorem | trlontrl 29743 | A trail is a trail between its endpoints. (Contributed by AV, 31-Jan-2021.) |
⊢ (𝐹(Trails‘𝐺)𝑃 → 𝐹((𝑃‘0)(TrailsOn‘𝐺)(𝑃‘(♯‘𝐹)))𝑃) | ||
Syntax | cpths 29744 | Extend class notation with paths (of a graph). |
class Paths | ||
Syntax | cspths 29745 | Extend class notation with simple paths (of a graph). |
class SPaths | ||
Syntax | cpthson 29746 | Extend class notation with paths between two vertices (within a graph). |
class PathsOn | ||
Syntax | cspthson 29747 | Extend class notation with simple paths between two vertices (within a graph). |
class SPathsOn | ||
Definition | df-pths 29748* |
Define the set of all paths (in an undirected graph).
According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A path is a trail in which all vertices (except possibly the first and last) are distinct. ... use the term simple path to refer to a path which contains no repeated vertices." According to Bollobas: "... a path is a walk with distinct vertices.", see Notation of [Bollobas] p. 5. (A walk with distinct vertices is actually a simple path, see upgrwlkdvspth 29771). Therefore, a path can be represented by an injective mapping f from { 1 , ... , n } and a mapping p from { 0 , ... , n }, which is injective restricted to the set { 1 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the path is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 9-Jan-2021.) |
⊢ Paths = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(Trails‘𝑔)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(♯‘𝑓))) ∧ ((𝑝 “ {0, (♯‘𝑓)}) ∩ (𝑝 “ (1..^(♯‘𝑓)))) = ∅)}) | ||
Definition | df-spths 29749* |
Define the set of all simple paths (in an undirected graph).
According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A path is a trail in which all vertices (except possibly the first and last) are distinct. ... use the term simple path to refer to a path which contains no repeated vertices." Therefore, a simple path can be represented by an injective mapping f from { 1 , ... , n } and an injective mapping p from { 0 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the simple path is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 9-Jan-2021.) |
⊢ SPaths = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(Trails‘𝑔)𝑝 ∧ Fun ◡𝑝)}) | ||
Definition | df-pthson 29750* | Define the collection of paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 9-Jan-2021.) |
⊢ PathsOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(TrailsOn‘𝑔)𝑏)𝑝 ∧ 𝑓(Paths‘𝑔)𝑝)})) | ||
Definition | df-spthson 29751* | Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 9-Jan-2021.) |
⊢ SPathsOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(TrailsOn‘𝑔)𝑏)𝑝 ∧ 𝑓(SPaths‘𝑔)𝑝)})) | ||
Theorem | relpths 29752 | The set (Paths‘𝐺) of all paths on 𝐺 is a set of pairs by our definition of a path, and so is a relation. (Contributed by AV, 30-Oct-2021.) |
⊢ Rel (Paths‘𝐺) | ||
Theorem | pthsfval 29753* | The set of paths (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
⊢ (Paths‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓(Trails‘𝐺)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(♯‘𝑓))) ∧ ((𝑝 “ {0, (♯‘𝑓)}) ∩ (𝑝 “ (1..^(♯‘𝑓)))) = ∅)} | ||
Theorem | spthsfval 29754* | The set of simple paths (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
⊢ (SPaths‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓(Trails‘𝐺)𝑝 ∧ Fun ◡𝑝)} | ||
Theorem | ispth 29755 | Conditions for a pair of classes/functions to be a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
⊢ (𝐹(Paths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅)) | ||
Theorem | isspth 29756 | Conditions for a pair of classes/functions to be a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
⊢ (𝐹(SPaths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡𝑃)) | ||
Theorem | pthistrl 29757 | A path is a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Trails‘𝐺)𝑃) | ||
Theorem | spthispth 29758 | A simple path is a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ (𝐹(SPaths‘𝐺)𝑃 → 𝐹(Paths‘𝐺)𝑃) | ||
Theorem | pthiswlk 29759 | A path is a walk (in an undirected graph). (Contributed by AV, 6-Feb-2021.) |
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) | ||
Theorem | spthiswlk 29760 | A simple path is a walk (in an undirected graph). (Contributed by AV, 16-May-2021.) |
⊢ (𝐹(SPaths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) | ||
Theorem | pthdivtx 29761 | The inner vertices of a path are distinct from all other vertices. (Contributed by AV, 5-Feb-2021.) (Proof shortened by AV, 31-Oct-2021.) |
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝐼 ∈ (1..^(♯‘𝐹)) ∧ 𝐽 ∈ (0...(♯‘𝐹)) ∧ 𝐼 ≠ 𝐽)) → (𝑃‘𝐼) ≠ (𝑃‘𝐽)) | ||
Theorem | pthdadjvtx 29762 | The adjacent vertices of a path of length at least 2 are distinct. (Contributed by AV, 5-Feb-2021.) |
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 𝐼 ∈ (0..^(♯‘𝐹))) → (𝑃‘𝐼) ≠ (𝑃‘(𝐼 + 1))) | ||
Theorem | 2pthnloop 29763* | A path of length at least 2 does not contain a loop. In contrast, a path of length 1 can contain/be a loop, see lppthon 30179. (Contributed by AV, 6-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹)) → ∀𝑖 ∈ (0..^(♯‘𝐹))2 ≤ (♯‘(𝐼‘(𝐹‘𝑖)))) | ||
Theorem | upgr2pthnlp 29764* | A path of length at least 2 in a pseudograph does not contain a loop. (Contributed by AV, 6-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹)) → ∀𝑖 ∈ (0..^(♯‘𝐹))(♯‘(𝐼‘(𝐹‘𝑖))) = 2) | ||
Theorem | spthdifv 29765 | The vertices of a simple path are distinct, so the vertex function is one-to-one. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Revised by AV, 5-Jun-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ (𝐹(SPaths‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))–1-1→(Vtx‘𝐺)) | ||
Theorem | spthdep 29766 | A simple path (at least of length 1) has different start and end points (in an undirected graph). (Contributed by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ ((𝐹(SPaths‘𝐺)𝑃 ∧ (♯‘𝐹) ≠ 0) → (𝑃‘0) ≠ (𝑃‘(♯‘𝐹))) | ||
Theorem | pthdepisspth 29767 | A path with different start and end points is a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 12-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹))) → 𝐹(SPaths‘𝐺)𝑃) | ||
Theorem | upgrwlkdvdelem 29768* | Lemma for upgrwlkdvde 29769. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Proof shortened by AV, 17-Jan-2021.) |
⊢ ((𝑃:(0...(♯‘𝐹))–1-1→𝑉 ∧ 𝐹 ∈ Word dom 𝐼) → (∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → Fun ◡𝐹)) | ||
Theorem | upgrwlkdvde 29769 | In a pseudograph, all edges of a walk consisting of different vertices are different. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk 29770. (Contributed by AV, 17-Jan-2021.) |
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝑃) → Fun ◡𝐹) | ||
Theorem | upgrspthswlk 29770* | The set of simple paths in a pseudograph, expressed as walk. Notice that this theorem would not hold for arbitrary hypergraphs, since a walk with distinct vertices does not need to be a trail: let E = { p0, p1, p2 } be a hyperedge, then ( p0, e, p1, e, p2 ) is walk with distinct vertices, but not with distinct edges. Therefore, E is not a trail and, by definition, also no path. (Contributed by AV, 11-Jan-2021.) (Proof shortened by AV, 17-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ (𝐺 ∈ UPGraph → (SPaths‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓(Walks‘𝐺)𝑝 ∧ Fun ◡𝑝)}) | ||
Theorem | upgrwlkdvspth 29771 | A walk consisting of different vertices is a simple path. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk 29770. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Revised by AV, 17-Jan-2021.) |
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝑃) → 𝐹(SPaths‘𝐺)𝑃) | ||
Theorem | pthsonfval 29772* | The set of paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(PathsOn‘𝐺)𝐵) = {〈𝑓, 𝑝〉 ∣ (𝑓(𝐴(TrailsOn‘𝐺)𝐵)𝑝 ∧ 𝑓(Paths‘𝐺)𝑝)}) | ||
Theorem | spthson 29773* | The set of simple paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(SPathsOn‘𝐺)𝐵) = {〈𝑓, 𝑝〉 ∣ (𝑓(𝐴(TrailsOn‘𝐺)𝐵)𝑝 ∧ 𝑓(SPaths‘𝐺)𝑝)}) | ||
Theorem | ispthson 29774 | Properties of a pair of functions to be a path between two given vertices. (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Paths‘𝐺)𝑃))) | ||
Theorem | isspthson 29775 | Properties of a pair of functions to be a simple path between two given vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(SPaths‘𝐺)𝑃))) | ||
Theorem | pthsonprop 29776 | Properties of a path between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 16-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Paths‘𝐺)𝑃))) | ||
Theorem | spthonprop 29777 | Properties of a simple path between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(SPaths‘𝐺)𝑃))) | ||
Theorem | pthonispth 29778 | A path between two vertices is a path. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 17-Jan-2021.) |
⊢ (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 → 𝐹(Paths‘𝐺)𝑃) | ||
Theorem | pthontrlon 29779 | A path between two vertices is a trail between these vertices. (Contributed by AV, 24-Jan-2021.) |
⊢ (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃) | ||
Theorem | pthonpth 29780 | A path is a path between its endpoints. (Contributed by AV, 31-Jan-2021.) |
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹((𝑃‘0)(PathsOn‘𝐺)(𝑃‘(♯‘𝐹)))𝑃) | ||
Theorem | isspthonpth 29781 | A pair of functions is a simple path between two given vertices iff it is a simple path starting and ending at the two vertices. (Contributed by Alexander van der Vekens, 9-Mar-2018.) (Revised by AV, 17-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(SPaths‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵))) | ||
Theorem | spthonisspth 29782 | A simple path between to vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 18-Jan-2021.) |
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → 𝐹(SPaths‘𝐺)𝑃) | ||
Theorem | spthonpthon 29783 | A simple path between two vertices is a path between these vertices. (Contributed by AV, 24-Jan-2021.) |
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃) | ||
Theorem | spthonepeq 29784 | The endpoints of a simple path between two vertices are equal iff the path is of length 0. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 18-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.) |
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → (𝐴 = 𝐵 ↔ (♯‘𝐹) = 0)) | ||
Theorem | uhgrwkspthlem1 29785 | Lemma 1 for uhgrwkspth 29787. (Contributed by AV, 25-Jan-2021.) |
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (♯‘𝐹) = 1) → Fun ◡𝐹) | ||
Theorem | uhgrwkspthlem2 29786 | Lemma 2 for uhgrwkspth 29787. (Contributed by AV, 25-Jan-2021.) |
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ ((♯‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵)) → Fun ◡𝑃) | ||
Theorem | uhgrwkspth 29787 | Any walk of length 1 between two different vertices is a simple path. (Contributed by AV, 25-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.) (Revised by AV, 7-Jul-2022.) |
⊢ ((𝐺 ∈ 𝑊 ∧ (♯‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ↔ 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃)) | ||
Theorem | usgr2wlkneq 29788 | The vertices and edges are pairwise different in a walk of length 2 in a simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 26-Jan-2021.) |
⊢ (((𝐺 ∈ USGraph ∧ 𝐹(Walks‘𝐺)𝑃) ∧ ((♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))) | ||
Theorem | usgr2wlkspthlem1 29789 | Lemma 1 for usgr2wlkspth 29791. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 26-Jan-2021.) |
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))) → Fun ◡𝐹) | ||
Theorem | usgr2wlkspthlem2 29790 | Lemma 2 for usgr2wlkspth 29791. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 27-Jan-2021.) |
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))) → Fun ◡𝑃) | ||
Theorem | usgr2wlkspth 29791 | In a simple graph, any walk of length 2 between two different vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 27-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.) |
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ↔ 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃)) | ||
Theorem | usgr2trlncl 29792 | In a simple graph, any trail of length 2 does not start and end at the same vertex. (Contributed by AV, 5-Jun-2021.) (Proof shortened by AV, 31-Oct-2021.) |
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝐹(Trails‘𝐺)𝑃 → (𝑃‘0) ≠ (𝑃‘2))) | ||
Theorem | usgr2trlspth 29793 | In a simple graph, any trail of length 2 is a simple path. (Contributed by AV, 5-Jun-2021.) |
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝐹(Trails‘𝐺)𝑃 ↔ 𝐹(SPaths‘𝐺)𝑃)) | ||
Theorem | usgr2pthspth 29794 | In a simple graph, any path of length 2 is a simple path. (Contributed by Alexander van der Vekens, 25-Jan-2018.) (Revised by AV, 5-Jun-2021.) |
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝐹(Paths‘𝐺)𝑃 ↔ 𝐹(SPaths‘𝐺)𝑃)) | ||
Theorem | usgr2pthlem 29795* | Lemma for usgr2pth 29796. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))) | ||
Theorem | usgr2pth 29796* | In a simple graph, there is a path of length 2 iff there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.) (Proof shortened by AV, 31-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (♯‘𝐹) = 2) ↔ (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))) | ||
Theorem | usgr2pth0 29797* | In a simply graph, there is a path of length 2 iff there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (♯‘𝐹) = 2) ↔ (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑧 ∧ (𝑃‘2) = 𝑦) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑧} ∧ (𝐼‘(𝐹‘1)) = {𝑧, 𝑦}))))) | ||
Theorem | pthdlem1 29798* | Lemma 1 for pthd 29801. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 9-Feb-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ 𝑅 = ((♯‘𝑃) − 1) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) ⇒ ⊢ (𝜑 → Fun ◡(𝑃 ↾ (1..^𝑅))) | ||
Theorem | pthdlem2lem 29799* | Lemma for pthdlem2 29800. (Contributed by AV, 10-Feb-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ 𝑅 = ((♯‘𝑃) − 1) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) ⇒ ⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → (𝑃‘𝐼) ∉ (𝑃 “ (1..^𝑅))) | ||
Theorem | pthdlem2 29800* | Lemma 2 for pthd 29801. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 10-Feb-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ 𝑅 = ((♯‘𝑃) − 1) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) ⇒ ⊢ (𝜑 → ((𝑃 “ {0, 𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |