![]() |
Metamath
Proof Explorer Theorem List (p. 276 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43639) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | clwwlknon1nloop 27501 | If there is no loop at vertex 𝑋, the set of (closed) walks on 𝑋 of length 1 as words over the set of vertices is empty. (Contributed by AV, 11-Feb-2022.) (Revised by AV, 25-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐶 = (ClWWalksNOn‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ({𝑋} ∉ 𝐸 → (𝑋𝐶1) = ∅) | ||
Theorem | clwwlknon1sn 27502 | The set of (closed) walks on vertex 𝑋 of length 1 as words over the set of vertices is a singleton containing the singleton word consisting of 𝑋 iff there is a loop at 𝑋. (Contributed by AV, 11-Feb-2022.) (Revised by AV, 25-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐶 = (ClWWalksNOn‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝑉 → ((𝑋𝐶1) = {〈“𝑋”〉} ↔ {𝑋} ∈ 𝐸)) | ||
Theorem | clwwlknon1le1 27503 | There is at most one (closed) walk on vertex 𝑋 of length 1 as word over the set of vertices. (Contributed by AV, 11-Feb-2022.) (Revised by AV, 25-Mar-2022.) |
⊢ (♯‘(𝑋(ClWWalksNOn‘𝐺)1)) ≤ 1 | ||
Theorem | clwwlknon2 27504* | The set of closed walks on vertex 𝑋 of length 2 in a graph 𝐺 as words over the set of vertices. (Contributed by AV, 5-Mar-2022.) (Proof revised by AV, 25-Mar-2022.) |
⊢ 𝐶 = (ClWWalksNOn‘𝐺) ⇒ ⊢ (𝑋𝐶2) = {𝑤 ∈ (2 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} | ||
Theorem | clwwlknon2x 27505* | The set of closed walks on vertex 𝑋 of length 2 in a graph 𝐺 as words over the set of vertices, definition of ClWWalksN expanded. (Contributed by Alexander van der Vekens, 19-Sep-2018.) (Revised by AV, 25-Mar-2022.) |
⊢ 𝐶 = (ClWWalksNOn‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑋𝐶2) = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸 ∧ (𝑤‘0) = 𝑋)} | ||
Theorem | s2elclwwlknon2 27506 | Sufficient conditions of a doubleton word to represent a closed walk on vertex 𝑋 of length 2. (Contributed by AV, 11-May-2022.) |
⊢ 𝐶 = (ClWWalksNOn‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ {𝑋, 𝑌} ∈ 𝐸) → 〈“𝑋𝑌”〉 ∈ (𝑋𝐶2)) | ||
Theorem | clwwlknon2num 27507 | In a 𝐾-regular graph 𝐺, there are 𝐾 closed walks on vertex 𝑋 of length 2. (Contributed by Alexander van der Vekens, 19-Sep-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 25-Feb-2022.) (Proof shortened by AV, 25-Mar-2022.) |
⊢ ((𝐺RegUSGraph𝐾 ∧ 𝑋 ∈ (Vtx‘𝐺)) → (♯‘(𝑋(ClWWalksNOn‘𝐺)2)) = 𝐾) | ||
Theorem | clwwlknonwwlknonb 27508 | A word over vertices represents a closed walk of a fixed length 𝑁 on vertex 𝑋 iff the word concatenated with 𝑋 represents a walk of length 𝑁 on 𝑋 and 𝑋. This theorem would not hold for 𝑁 = 0 and 𝑊 = ∅, see clwwlknwwlksnb 27452. (Contributed by AV, 4-Mar-2022.) (Revised by AV, 27-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑊 ++ 〈“𝑋”〉) ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑋))) | ||
Theorem | clwwlknonex2lem1 27509 | Lemma 1 for clwwlknonex2 27511: Transformation of a special half-open integer range into a union of a smaller half-open integer range and an unordered pair. This Lemma would not hold for 𝑁 = 2, i.e., (♯‘𝑊) = 0, because (0..^(((♯‘𝑊) + 2) − 1)) = (0..^((0 + 2) − 1)) = (0..^1) = {0} ≠ {-1, 0} = (∅ ∪ {-1, 0}) = ((0..^(0 − 1)) ∪ {(0 − 1), 0}) = ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1), (♯‘𝑊)}). (Contributed by AV, 22-Sep-2018.) (Revised by AV, 26-Jan-2022.) |
⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2)) → (0..^(((♯‘𝑊) + 2) − 1)) = ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1), (♯‘𝑊)})) | ||
Theorem | clwwlknonex2lem2 27510* | Lemma 2 for clwwlknonex2 27511: Transformation of a walk and two edges into a walk extended by two vertices/edges. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 27-Jan-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → ∀𝑖 ∈ ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1), (♯‘𝑊)}){(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸) | ||
Theorem | clwwlknonex2 27511 | Extending a closed walk 𝑊 on vertex 𝑋 by an additional edge (forth and back) results in a closed walk. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 25-Feb-2022.) (Proof shortened by AV, 28-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)) ∧ {𝑋, 𝑌} ∈ 𝐸 ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺)) | ||
Theorem | clwwlknonex2e 27512 | Extending a closed walk 𝑊 on vertex 𝑋 by an additional edge (forth and back) results in a closed walk on vertex 𝑋. (Contributed by AV, 17-Apr-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)) ∧ {𝑋, 𝑌} ∈ 𝐸 ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁)) | ||
Theorem | clwwlknondisj 27513* | The sets of closed walks on different vertices are disjunct. (Contributed by Alexander van der Vekens, 7-Oct-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 3-Mar-2022.) (Proof shortened by AV, 28-Mar-2022.) |
⊢ Disj 𝑥 ∈ 𝑉 (𝑥(ClWWalksNOn‘𝐺)𝑁) | ||
Theorem | clwwlknun 27514* | The set of closed walks of fixed length 𝑁 in a simple graph 𝐺 is the union of the closed walks of the fixed length 𝑁 on each of the vertices of graph 𝐺. (Contributed by Alexander van der Vekens, 7-Oct-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 3-Mar-2022.) (Proof shortened by AV, 28-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → (𝑁 ClWWalksN 𝐺) = ∪ 𝑥 ∈ 𝑉 (𝑥(ClWWalksNOn‘𝐺)𝑁)) | ||
Theorem | clwwlkvbij 27515* | There is a bijection between the set of closed walks of a fixed length 𝑁 on a fixed vertex 𝑋 represented by walks (as word) and the set of closed walks (as words) of the fixed length 𝑁 on the fixed vertex 𝑋. The difference between these two representations is that in the first case the fixed vertex is repeated at the end of the word, and in the second case it is not. (Contributed by Alexander van der Vekens, 29-Sep-2018.) (Revised by AV, 26-Apr-2021.) (Revised by AV, 7-Jul-2022.) (Proof shortened by AV, 2-Nov-2022.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ∃𝑓 𝑓:{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}–1-1-onto→(𝑋(ClWWalksNOn‘𝐺)𝑁)) | ||
Theorem | clwwlkvbijOLD 27516* | Obsolete proof of clwwlkvbij 27515 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 29-Sep-2018.) (Revised by AV, 26-Apr-2021.) (Revised by AV, 7-Jul-2022.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ∃𝑓 𝑓:{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}–1-1-onto→(𝑋(ClWWalksNOn‘𝐺)𝑁)) | ||
Theorem | 0ewlk 27517 | The empty set (empty sequence of edges) is an s-walk of edges for all s. (Contributed by AV, 4-Jan-2021.) |
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ ℕ0*) → ∅ ∈ (𝐺 EdgWalks 𝑆)) | ||
Theorem | 1ewlk 27518 | A sequence of 1 edge is an s-walk of edges for all s. (Contributed by AV, 5-Jan-2021.) |
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ∧ 𝐼 ∈ dom (iEdg‘𝐺)) → 〈“𝐼”〉 ∈ (𝐺 EdgWalks 𝑆)) | ||
Theorem | 0wlk 27519 | A pair of an empty set (of edges) and a second set (of vertices) is a walk iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 3-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑈 → (∅(Walks‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | is0wlk 27520 | A pair of an empty set (of edges) and a sequence of one vertex is a walk (of length 0). (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃 = {〈0, 𝑁〉} ∧ 𝑁 ∈ 𝑉) → ∅(Walks‘𝐺)𝑃) | ||
Theorem | 0wlkonlem1 27521 | Lemma 1 for 0wlkon 27523 and 0trlon 27527. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → (𝑁 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) | ||
Theorem | 0wlkonlem2 27522 | Lemma 2 for 0wlkon 27523 and 0trlon 27527. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → 𝑃 ∈ (𝑉 ↑pm (0...0))) | ||
Theorem | 0wlkon 27523 | A walk of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → ∅(𝑁(WalksOn‘𝐺)𝑁)𝑃) | ||
Theorem | 0wlkons1 27524 | A walk of length 0 from a vertex to itself. (Contributed by AV, 17-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → ∅(𝑁(WalksOn‘𝐺)𝑁)〈“𝑁”〉) | ||
Theorem | 0trl 27525 | A pair of an empty set (of edges) and a second set (of vertices) is a trail iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑈 → (∅(Trails‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | is0trl 27526 | A pair of an empty set (of edges) and a sequence of one vertex is a trail (of length 0). (Contributed by AV, 7-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃 = {〈0, 𝑁〉} ∧ 𝑁 ∈ 𝑉) → ∅(Trails‘𝐺)𝑃) | ||
Theorem | 0trlon 27527 | A trail of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 8-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → ∅(𝑁(TrailsOn‘𝐺)𝑁)𝑃) | ||
Theorem | 0pth 27528 | A pair of an empty set (of edges) and a second set (of vertices) is a path iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 19-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (∅(Paths‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | 0spth 27529 | A pair of an empty set (of edges) and a second set (of vertices) is a simple path iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 18-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (∅(SPaths‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | 0pthon 27530 | A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 20-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → ∅(𝑁(PathsOn‘𝐺)𝑁)𝑃) | ||
Theorem | 0pthon1 27531 | A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 20-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → ∅(𝑁(PathsOn‘𝐺)𝑁){〈0, 𝑁〉}) | ||
Theorem | 0pthonv 27532* | For each vertex there is a path of length 0 from the vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 21-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → ∃𝑓∃𝑝 𝑓(𝑁(PathsOn‘𝐺)𝑁)𝑝) | ||
Theorem | 0clwlk 27533 | A pair of an empty set (of edges) and a second set (of vertices) is a closed walk if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 17-Feb-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑋 → (∅(ClWalks‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | 0clwlkv 27534 | Any vertex (more precisely, a pair of an empty set (of edges) and a singleton function to this vertex) determines a closed walk of length 0. (Contributed by AV, 11-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹 = ∅ ∧ 𝑃:{0}⟶{𝑋}) → 𝐹(ClWalks‘𝐺)𝑃) | ||
Theorem | 0clwlk0 27535 | There is no closed walk in the empty set (i.e. the null graph). (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.) |
⊢ (ClWalks‘∅) = ∅ | ||
Theorem | 0crct 27536 | A pair of an empty set (of edges) and a second set (of vertices) is a circuit if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ (𝐺 ∈ 𝑊 → (∅(Circuits‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶(Vtx‘𝐺))) | ||
Theorem | 0cycl 27537 | A pair of an empty set (of edges) and a second set (of vertices) is a cycle if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ (𝐺 ∈ 𝑊 → (∅(Cycles‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶(Vtx‘𝐺))) | ||
Theorem | 1pthdlem1 27538 | Lemma 1 for 1pthd 27546. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 ⇒ ⊢ Fun ◡(𝑃 ↾ (1..^(♯‘𝐹))) | ||
Theorem | 1pthdlem2 27539 | Lemma 2 for 1pthd 27546. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 ⇒ ⊢ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅ | ||
Theorem | 1wlkdlem1 27540 | Lemma 1 for 1wlkd 27544. (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶𝑉) | ||
Theorem | 1wlkdlem2 27541 | Lemma 2 for 1wlkd 27544. (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋}) & ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽)) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝐼‘𝐽)) | ||
Theorem | 1wlkdlem3 27542 | Lemma 3 for 1wlkd 27544. (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋}) & ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽)) ⇒ ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼) | ||
Theorem | 1wlkdlem4 27543* | Lemma 4 for 1wlkd 27544. (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋}) & ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) | ||
Theorem | 1wlkd 27544 | In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a walk. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋}) & ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽)) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) | ||
Theorem | 1trld 27545 | In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a trail. The two vertices need not be distinct (in the case of a loop). (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋}) & ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽)) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) | ||
Theorem | 1pthd 27546 | In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋}) & ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽)) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃) | ||
Theorem | 1pthond 27547 | In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path from one of these vertices to the other vertex. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋}) & ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽)) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝜑 → 𝐹(𝑋(PathsOn‘𝐺)𝑌)𝑃) | ||
Theorem | upgr1wlkdlem1 27548 | Lemma 1 for upgr1wlkd 27550. (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺)) & ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺)) & ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌}) ⇒ ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → ((iEdg‘𝐺)‘𝐽) = {𝑋}) | ||
Theorem | upgr1wlkdlem2 27549 | Lemma 2 for upgr1wlkd 27550. (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺)) & ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺)) & ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌}) ⇒ ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ ((iEdg‘𝐺)‘𝐽)) | ||
Theorem | upgr1wlkd 27550 | In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a walk. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺)) & ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺)) & ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌}) & ⊢ (𝜑 → 𝐺 ∈ UPGraph) ⇒ ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) | ||
Theorem | upgr1trld 27551 | In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a trail. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺)) & ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺)) & ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌}) & ⊢ (𝜑 → 𝐺 ∈ UPGraph) ⇒ ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) | ||
Theorem | upgr1pthd 27552 | In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺)) & ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺)) & ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌}) & ⊢ (𝜑 → 𝐺 ∈ UPGraph) ⇒ ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃) | ||
Theorem | upgr1pthond 27553 | In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path from one of these vertices to the other vertex. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺)) & ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺)) & ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌}) & ⊢ (𝜑 → 𝐺 ∈ UPGraph) ⇒ ⊢ (𝜑 → 𝐹(𝑋(PathsOn‘𝐺)𝑌)𝑃) | ||
Theorem | lppthon 27554 | A loop (which is an edge at index 𝐽) induces a path of length 1 from a vertex to itself in a hypergraph. (Contributed by AV, 1-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → 〈“𝐽”〉(𝐴(PathsOn‘𝐺)𝐴)〈“𝐴𝐴”〉) | ||
Theorem | lp1cycl 27555 | A loop (which is an edge at index 𝐽) induces a cycle of length 1 in a hypergraph. (Contributed by AV, 2-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → 〈“𝐽”〉(Cycles‘𝐺)〈“𝐴𝐴”〉) | ||
Theorem | 1pthon2v 27556* | For each pair of adjacent vertices there is a path of length 1 from one vertex to the other in a hypergraph. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ ∃𝑒 ∈ 𝐸 {𝐴, 𝐵} ⊆ 𝑒) → ∃𝑓∃𝑝 𝑓(𝐴(PathsOn‘𝐺)𝐵)𝑝) | ||
Theorem | 1pthon2ve 27557* | For each pair of adjacent vertices there is a path of length 1 from one vertex to the other in a hypergraph. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Proof shortened by AV, 15-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ {𝐴, 𝐵} ∈ 𝐸) → ∃𝑓∃𝑝 𝑓(𝐴(PathsOn‘𝐺)𝐵)𝑝) | ||
Theorem | wlk2v2elem1 27558 | Lemma 1 for wlk2v2e 27560: 𝐹 is a length 2 word of over {0}, the domain of the singleton word 𝐼. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 9-Jan-2021.) |
⊢ 𝐼 = 〈“{𝑋, 𝑌}”〉 & ⊢ 𝐹 = 〈“00”〉 ⇒ ⊢ 𝐹 ∈ Word dom 𝐼 | ||
Theorem | wlk2v2elem2 27559* | Lemma 2 for wlk2v2e 27560: The values of 𝐼 after 𝐹 are edges between two vertices enumerated by 𝑃. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 9-Jan-2021.) |
⊢ 𝐼 = 〈“{𝑋, 𝑌}”〉 & ⊢ 𝐹 = 〈“00”〉 & ⊢ 𝑋 ∈ V & ⊢ 𝑌 ∈ V & ⊢ 𝑃 = 〈“𝑋𝑌𝑋”〉 ⇒ ⊢ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} | ||
Theorem | wlk2v2e 27560 | In a graph with two vertices and one edge connecting these two vertices, to go from one vertex to the other and back to the first vertex via the same/only edge is a walk. Notice that 𝐺 is a simple graph (without loops) only if 𝑋 ≠ 𝑌. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 8-Jan-2021.) |
⊢ 𝐼 = 〈“{𝑋, 𝑌}”〉 & ⊢ 𝐹 = 〈“00”〉 & ⊢ 𝑋 ∈ V & ⊢ 𝑌 ∈ V & ⊢ 𝑃 = 〈“𝑋𝑌𝑋”〉 & ⊢ 𝐺 = 〈{𝑋, 𝑌}, 𝐼〉 ⇒ ⊢ 𝐹(Walks‘𝐺)𝑃 | ||
Theorem | ntrl2v2e 27561 | A walk which is not a trail: In a graph with two vertices and one edge connecting these two vertices, to go from one vertex to the other and back to the first vertex via the same/only edge is a walk, see wlk2v2e 27560, but not a trail. Notice that 𝐺 is a simple graph (without loops) only if 𝑋 ≠ 𝑌. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 8-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝐼 = 〈“{𝑋, 𝑌}”〉 & ⊢ 𝐹 = 〈“00”〉 & ⊢ 𝑋 ∈ V & ⊢ 𝑌 ∈ V & ⊢ 𝑃 = 〈“𝑋𝑌𝑋”〉 & ⊢ 𝐺 = 〈{𝑋, 𝑌}, 𝐼〉 ⇒ ⊢ ¬ 𝐹(Trails‘𝐺)𝑃 | ||
Theorem | 3wlkdlem1 27562 | Lemma 1 for 3wlkd 27573. (Contributed by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 ⇒ ⊢ (♯‘𝑃) = ((♯‘𝐹) + 1) | ||
Theorem | 3wlkdlem2 27563 | Lemma 2 for 3wlkd 27573. (Contributed by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 ⇒ ⊢ (0..^(♯‘𝐹)) = {0, 1, 2} | ||
Theorem | 3wlkdlem3 27564 | Lemma 3 for 3wlkd 27573. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) ⇒ ⊢ (𝜑 → (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷))) | ||
Theorem | 3wlkdlem4 27565* | Lemma 4 for 3wlkd 27573. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0...(♯‘𝐹))(𝑃‘𝑘) ∈ 𝑉) | ||
Theorem | 3wlkdlem5 27566* | Lemma 5 for 3wlkd 27573. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) | ||
Theorem | 3pthdlem1 27567* | Lemma 1 for 3pthd 27577. (Contributed by AV, 9-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^(♯‘𝐹))(𝑘 ≠ 𝑗 → (𝑃‘𝑘) ≠ (𝑃‘𝑗))) | ||
Theorem | 3wlkdlem6 27568 | Lemma 6 for 3wlkd 27573. (Contributed by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) ⇒ ⊢ (𝜑 → (𝐴 ∈ (𝐼‘𝐽) ∧ 𝐵 ∈ (𝐼‘𝐾) ∧ 𝐶 ∈ (𝐼‘𝐿))) | ||
Theorem | 3wlkdlem7 27569 | Lemma 7 for 3wlkd 27573. (Contributed by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) ⇒ ⊢ (𝜑 → (𝐽 ∈ V ∧ 𝐾 ∈ V ∧ 𝐿 ∈ V)) | ||
Theorem | 3wlkdlem8 27570 | Lemma 8 for 3wlkd 27573. (Contributed by Alexander van der Vekens, 12-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) ⇒ ⊢ (𝜑 → ((𝐹‘0) = 𝐽 ∧ (𝐹‘1) = 𝐾 ∧ (𝐹‘2) = 𝐿)) | ||
Theorem | 3wlkdlem9 27571 | Lemma 9 for 3wlkd 27573. (Contributed by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) ⇒ ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘(𝐹‘0)) ∧ {𝐵, 𝐶} ⊆ (𝐼‘(𝐹‘1)) ∧ {𝐶, 𝐷} ⊆ (𝐼‘(𝐹‘2)))) | ||
Theorem | 3wlkdlem10 27572* | Lemma 10 for 3wlkd 27573. (Contributed by Alexander van der Vekens, 12-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) | ||
Theorem | 3wlkd 27573 | Construction of a walk from two given edges in a graph. (Contributed by AV, 7-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) | ||
Theorem | 3wlkond 27574 | A walk of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 8-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝜑 → 𝐹(𝐴(WalksOn‘𝐺)𝐷)𝑃) | ||
Theorem | 3trld 27575 | Construction of a trail from two given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 8-Feb-2021.) (Revised by AV, 24-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → (𝐽 ≠ 𝐾 ∧ 𝐽 ≠ 𝐿 ∧ 𝐾 ≠ 𝐿)) ⇒ ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) | ||
Theorem | 3trlond 27576 | A trail of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 8-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → (𝐽 ≠ 𝐾 ∧ 𝐽 ≠ 𝐿 ∧ 𝐾 ≠ 𝐿)) ⇒ ⊢ (𝜑 → 𝐹(𝐴(TrailsOn‘𝐺)𝐷)𝑃) | ||
Theorem | 3pthd 27577 | A path of length 3 from one vertex to another vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → (𝐽 ≠ 𝐾 ∧ 𝐽 ≠ 𝐿 ∧ 𝐾 ≠ 𝐿)) ⇒ ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃) | ||
Theorem | 3pthond 27578 | A path of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → (𝐽 ≠ 𝐾 ∧ 𝐽 ≠ 𝐿 ∧ 𝐾 ≠ 𝐿)) ⇒ ⊢ (𝜑 → 𝐹(𝐴(PathsOn‘𝐺)𝐷)𝑃) | ||
Theorem | 3spthd 27579 | A simple path of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → (𝐽 ≠ 𝐾 ∧ 𝐽 ≠ 𝐿 ∧ 𝐾 ≠ 𝐿)) & ⊢ (𝜑 → 𝐴 ≠ 𝐷) ⇒ ⊢ (𝜑 → 𝐹(SPaths‘𝐺)𝑃) | ||
Theorem | 3spthond 27580 | A simple path of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → (𝐽 ≠ 𝐾 ∧ 𝐽 ≠ 𝐿 ∧ 𝐾 ≠ 𝐿)) & ⊢ (𝜑 → 𝐴 ≠ 𝐷) ⇒ ⊢ (𝜑 → 𝐹(𝐴(SPathsOn‘𝐺)𝐷)𝑃) | ||
Theorem | 3cycld 27581 | Construction of a 3-cycle from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → (𝐽 ≠ 𝐾 ∧ 𝐽 ≠ 𝐿 ∧ 𝐾 ≠ 𝐿)) & ⊢ (𝜑 → 𝐴 = 𝐷) ⇒ ⊢ (𝜑 → 𝐹(Cycles‘𝐺)𝑃) | ||
Theorem | 3cyclpd 27582 | Construction of a 3-cycle from three given edges in a graph, containing an endpoint of one of these edges. (Contributed by Alexander van der Vekens, 17-Nov-2017.) (Revised by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → (𝐽 ≠ 𝐾 ∧ 𝐽 ≠ 𝐿 ∧ 𝐾 ≠ 𝐿)) & ⊢ (𝜑 → 𝐴 = 𝐷) ⇒ ⊢ (𝜑 → (𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 3 ∧ (𝑃‘0) = 𝐴)) | ||
Theorem | upgr3v3e3cycl 27583* | If there is a cycle of length 3 in a pseudograph, there are three distinct vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.) |
⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))) | ||
Theorem | uhgr3cyclexlem 27584 | Lemma for uhgr3cyclex 27585. (Contributed by AV, 12-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ ((𝐽 ∈ dom 𝐼 ∧ {𝐵, 𝐶} = (𝐼‘𝐽)) ∧ (𝐾 ∈ dom 𝐼 ∧ {𝐶, 𝐴} = (𝐼‘𝐾)))) → 𝐽 ≠ 𝐾) | ||
Theorem | uhgr3cyclex 27585* | If there are three different vertices in a hypergraph which are mutually connected by edges, there is a 3-cycle in the graph containing one of these vertices. (Contributed by Alexander van der Vekens, 17-Nov-2017.) (Revised by AV, 12-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝐴)) | ||
Theorem | umgr3cyclex 27586* | If there are three (different) vertices in a multigraph which are mutually connected by edges, there is a 3-cycle in the graph containing one of these vertices. (Contributed by Alexander van der Vekens, 17-Nov-2017.) (Revised by AV, 12-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝐴)) | ||
Theorem | umgr3v3e3cycl 27587* | If and only if there is a 3-cycle in a multigraph, there are three (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 14-Nov-2017.) (Revised by AV, 12-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ UMGraph → (∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸))) | ||
Theorem | upgr4cycl4dv4e 27588* | If there is a cycle of length 4 in a pseudograph, there are four (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.) (Revised by AV, 13-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 4) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) | ||
Syntax | cconngr 27589 | Extend class notation with connected graphs. |
class ConnGraph | ||
Definition | df-conngr 27590* | Define the class of all connected graphs. A graph is called connected if there is a path between every pair of (distinct) vertices. The distinctness of the vertices is not necessary for the definition, because there is always a path (of length 0) from a vertex to itself, see 0pthonv 27532 and dfconngr1 27591. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
⊢ ConnGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣]∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝} | ||
Theorem | dfconngr1 27591* | Alternative definition of the class of all connected graphs, requiring paths between distinct vertices. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
⊢ ConnGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣]∀𝑘 ∈ 𝑣 ∀𝑛 ∈ (𝑣 ∖ {𝑘})∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝} | ||
Theorem | isconngr 27592* | The property of being a connected graph. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ ConnGraph ↔ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ 𝑉 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝐺)𝑛)𝑝)) | ||
Theorem | isconngr1 27593* | The property of being a connected graph. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ ConnGraph ↔ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘})∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝐺)𝑛)𝑝)) | ||
Theorem | cusconngr 27594 | A complete hypergraph is connected. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
⊢ ((𝐺 ∈ UHGraph ∧ 𝐺 ∈ ComplGraph) → 𝐺 ∈ ConnGraph) | ||
Theorem | 0conngr 27595 | A graph without vertices is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
⊢ ∅ ∈ ConnGraph | ||
Theorem | 0vconngr 27596 | A graph without vertices is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → 𝐺 ∈ ConnGraph) | ||
Theorem | 1conngr 27597 | A graph with (at most) one vertex is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = {𝑁}) → 𝐺 ∈ ConnGraph) | ||
Theorem | conngrv2edg 27598* | A vertex in a connected graph with more than one vertex is incident with at least one edge. Formerly part of proof for vdgn0frgrv2 27703. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 4-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉)) → ∃𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒) | ||
Theorem | vdn0conngrumgrv2 27599 | A vertex in a connected multigraph with more than one vertex cannot have degree 0. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 4-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (((𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph) ∧ (𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉))) → ((VtxDeg‘𝐺)‘𝑁) ≠ 0) | ||
According to Wikipedia ("Eulerian path", 9-Mar-2021, https://en.wikipedia.org/wiki/Eulerian_path): "In graph theory, an Eulerian trail (or Eulerian path) is a trail in a finite graph that visits every edge exactly once (allowing for revisiting vertices). Similarly, an Eulerian circuit or Eulerian cycle is an Eulerian trail that starts and ends on the same vertex. ... The term Eulerian graph has two common meanings in graph theory. One meaning is a graph with an Eulerian circuit, and the other is a graph with every vertex of even degree. These definitions coincide for connected graphs. ... A graph that has an Eulerian trail but not an Eulerian circuit is called semi-Eulerian." Correspondingly, an Eulerian path is defined as "a trail containing all edges" (see definition in [Bollobas] p. 16) in df-eupth 27601 resp. iseupth 27604. (EulerPaths‘𝐺) is the set of all Eulerian paths in graph 𝐺, see eupths 27603. An Eulerian circuit (called Euler tour in the definition in [Diestel] p. 22) is "a circuit in a graph containing all the edges" (see definition in [Bollobas] p. 16), or, with other words, a circuit which is an Eulerian path. The function mapping a graph to the set of its Eulerian paths is defined as EulerPaths in df-eupth 27601, whereas there is no explicit definition for Eulerian circuits (yet): The statement "〈𝐹, 𝑃〉 is an Eulerian circuit" is formally expressed by (𝐹(EulerPaths‘𝐺)𝑃 ∧ 𝐹(Circuits‘𝐺)𝑃). Each Eulerian path can be made an Eulerian circuit by adding an edge which connects the endpoints of the Eulerian path (see eupth2eucrct 27621). Vice versa, removing one edge from a graph with an Eulerian circuit results in a graph with an Eulerian path, see eucrct2eupth 27651. An Eulerian path does not have to be a path in the meaning of definition df-pths 27068, because it may traverse some vertices more than once. Therefore, "Eulerian trail" would be a more appropriate name. The main result of this section is (one direction of) Euler's Theorem: "A non-trivial connected graph has an Euler[ian] circuit iff each vertex has even degree." (see part 1 of theorem 12 in [Bollobas] p. 16 and theorem 1.8.1 in [Diestel] p. 22) or, expressed with Eulerian paths: "A connected graph has an Euler[ian] trail from a vertex x to a vertex y (not equal with x) iff x and y are the only vertices of odd degree." (see part 2 of theorem 12 in [Bollobas] p. 17). In eulerpath 27645, it is shown that a pseudograph with an Eulerian path has either zero or two vertices of odd degree, and eulercrct 27646 shows that a pseudograph with an Eulerian circuit has only vertices of even degree. | ||
Syntax | ceupth 27600 | Extend class notation with Eulerian paths. |
class EulerPaths |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |