Home | Metamath
Proof Explorer Theorem List (p. 266 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 | eupa0 26501 | There is an Eulerian path on the empty graph. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → ∅(𝑉 EulPaths ∅){〈0, 𝐴〉}) | ||
Theorem | eupares 26502 | The restriction of an Eulerian path to an initial segment of the path forms an Eulerian path on the subgraph consisting of the edges in the initial segment. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) |
⊢ (𝜑 → 𝐺(𝑉 EulPaths 𝐸)𝑃) & ⊢ (𝜑 → 𝑁 ∈ (0...(#‘𝐺))) & ⊢ 𝐹 = (𝐸 ↾ (𝐺 “ (1...𝑁))) & ⊢ 𝐻 = (𝐺 ↾ (1...𝑁)) & ⊢ 𝑄 = (𝑃 ↾ (0...𝑁)) ⇒ ⊢ (𝜑 → 𝐻(𝑉 EulPaths 𝐹)𝑄) | ||
Theorem | eupap1 26503 | Append one path segment to an Eulerian path (enlarging the graph to add the new edge). (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ (𝜑 → 𝐸 Fn 𝐴) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐺(𝑉 EulPaths 𝐸)𝑃) & ⊢ (𝜑 → 𝑁 = (#‘𝐺)) & ⊢ 𝐹 = (𝐸 ∪ {〈𝐵, {(𝑃‘𝑁), 𝐶}〉}) & ⊢ 𝐻 = (𝐺 ∪ {〈(𝑁 + 1), 𝐵〉}) & ⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) ⇒ ⊢ (𝜑 → 𝐻(𝑉 EulPaths 𝐹)𝑄) | ||
Theorem | eupath2lem1 26504 | Lemma for eupath2 26507. (Contributed by Mario Carneiro, 8-Apr-2015.) |
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}) ↔ (𝐴 ≠ 𝐵 ∧ (𝑈 = 𝐴 ∨ 𝑈 = 𝐵)))) | ||
Theorem | eupath2lem2 26505 | Lemma for eupath2 26507. (Contributed by Mario Carneiro, 8-Apr-2015.) |
⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈) → (¬ 𝑈 ∈ if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}) ↔ 𝑈 ∈ if(𝐴 = 𝐶, ∅, {𝐴, 𝐶}))) | ||
Theorem | eupath2lem3 26506* | Lemma for eupath2 26507. (Contributed by Mario Carneiro, 8-Apr-2015.) |
⊢ (𝜑 → 𝐸 Fn 𝐴) & ⊢ (𝜑 → 𝐹(𝑉 EulPaths 𝐸)𝑃) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝑁 + 1) ≤ (#‘𝐹)) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...𝑁))))‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})) ⇒ ⊢ (𝜑 → (¬ 2 ∥ ((𝑉 VDeg (𝐸 ↾ (𝐹 “ (1...(𝑁 + 1)))))‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) | ||
Theorem | eupath2 26507* | The only vertices of odd degree in a graph with an Eulerian path are the endpoints, and then only if the endpoints are distinct. (Contributed by Mario Carneiro, 8-Apr-2015.) |
⊢ (𝜑 → 𝐸 Fn 𝐴) & ⊢ (𝜑 → 𝐹(𝑉 EulPaths 𝐸)𝑃) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} = if((𝑃‘0) = (𝑃‘(#‘𝐹)), ∅, {(𝑃‘0), (𝑃‘(#‘𝐹))})) | ||
Theorem | eupath 26508* | A graph with an Eulerian path has either zero or two vertices of odd degree. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ ((𝑉 EulPaths 𝐸) ≠ ∅ → (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) ∈ {0, 2}) | ||
Theorem | vdeg0i 26509 | The base case for the induction for calculating the degree of a vertex. The degree of 𝑈 in the empty graph is 0. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ 𝑉 ∈ V & ⊢ 𝑈 ∈ 𝑉 ⇒ ⊢ ((𝑉 VDeg ∅)‘𝑈) = 0 | ||
Theorem | umgrabi 26510* | Show that an unordered pair is a valid edge in a graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) |
⊢ 𝑉 ∈ V & ⊢ 𝑋 ∈ 𝑉 & ⊢ 𝑌 ∈ 𝑉 ⇒ ⊢ (𝜑 → {𝑋, 𝑌} ∈ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) | ||
Theorem | vdegp1ai 26511* | The induction step for a vertex degree calculation. If the degree of 𝑈 in the edge set 𝐸 is 𝑃, then adding {𝑋, 𝑌} to the edge set, where 𝑋 ≠ 𝑈 ≠ 𝑌, yields degree 𝑃 as well. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) |
⊢ 𝑉 ∈ V & ⊢ (⊤ → 𝐸 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) & ⊢ 𝑈 ∈ 𝑉 & ⊢ ((𝑉 VDeg 𝐸)‘𝑈) = 𝑃 & ⊢ 𝑋 ∈ 𝑉 & ⊢ 𝑋 ≠ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑌 ≠ 𝑈 & ⊢ 𝐹 = (𝐸 ++ 〈“{𝑋, 𝑌}”〉) ⇒ ⊢ ((𝑉 VDeg 𝐹)‘𝑈) = 𝑃 | ||
Theorem | vdegp1bi 26512* | The induction step for a vertex degree calculation. If the degree of 𝑈 in the edge set 𝐸 is 𝑃, then adding {𝑈, 𝑋} to the edge set, where 𝑋 ≠ 𝑈, yields degree 𝑃 + 1. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) |
⊢ 𝑉 ∈ V & ⊢ (⊤ → 𝐸 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) & ⊢ 𝑈 ∈ 𝑉 & ⊢ ((𝑉 VDeg 𝐸)‘𝑈) = 𝑃 & ⊢ 𝑄 = (𝑃 + 1) & ⊢ 𝑋 ∈ 𝑉 & ⊢ 𝑋 ≠ 𝑈 & ⊢ 𝐹 = (𝐸 ++ 〈“{𝑈, 𝑋}”〉) ⇒ ⊢ ((𝑉 VDeg 𝐹)‘𝑈) = 𝑄 | ||
Theorem | vdegp1ci 26513* | The induction step for a vertex degree calculation. If the degree of 𝑈 in the edge set 𝐸 is 𝑃, then adding {𝑋, 𝑈} to the edge set, where 𝑋 ≠ 𝑈, yields degree 𝑃 + 1. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) |
⊢ 𝑉 ∈ V & ⊢ (⊤ → 𝐸 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) & ⊢ 𝑈 ∈ 𝑉 & ⊢ ((𝑉 VDeg 𝐸)‘𝑈) = 𝑃 & ⊢ 𝑄 = (𝑃 + 1) & ⊢ 𝑋 ∈ 𝑉 & ⊢ 𝑋 ≠ 𝑈 & ⊢ 𝐹 = (𝐸 ++ 〈“{𝑋, 𝑈}”〉) ⇒ ⊢ ((𝑉 VDeg 𝐹)‘𝑈) = 𝑄 | ||
Theorem | konigsberg 26514 | The Konigsberg Bridge problem. If 〈𝑉, 𝐸〉 is the graph on four vertices 0, 1, 2, 3, with edges {0, 1}, {0, 2}, {0, 3}, {1, 2}, {1, 2}, {2, 3}, {2, 3}, then vertices 0, 1, 3 each have degree three, and 2 has degree five, so there are four vertices of odd degree and thus by eupath 26508 the graph cannot have an Eulerian path. This is Metamath 100 proof #54. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) |
⊢ 𝑉 = (0...3) & ⊢ 𝐸 = 〈“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”〉 ⇒ ⊢ (𝑉 EulPaths 𝐸) = ∅ | ||
In this section, the basics for the friendship theorem, which is one from the "100 theorem list" (#83), are provided (subsection "Friendship graphs - basics"), including the definition of friendship graphs df-frgra 26516 as special undirected simple graphs without loops (see frisusgra 26519). In subsection "The friendship theorem for small graphs", the friendship theorem for small graphs (with up to 3 vertices) is proved, see 1to3vfriendship 26535. The general friendship theorem friendship 26649 (⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) → ∃𝑣 ∈ 𝑉∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸) is proven by following the approach of [Huneke] in subsection "Huneke's Proof of the Friendship Theorem". The case 𝑉 = ∅ (a graph without vertices) must be excluded either from the definition of a friendship graph, or from the theorem. If it is not excluded from the definition, which is the case with df-frgra 26516, a graph without vertices is a friendship graph (see frgra0 26521), but the friendship condition ∃𝑣 ∈ 𝑉∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸 does not hold (because of ¬ ∃𝑥 ∈ ∅𝜑, see rex0 3894). Further results of this sections are: Any graph with exactly one vertex is a friendship graph, see frgra1v 26525, any graph with exactly 2 (different) vertices is not a friendship graph, see frgra2v 26526, a graph with exactly 3 (different) vertices is a friendship graph if and only if it is a complete graph (every two vertices are connected by an edge), see frgra3v 26529, and every friendship graph (with 1 or 3 vertices) is a windmill graph, see 1to3vfriswmgra 26534 (The generalization of this theorem "Every friendship graph (with at least one vertex) is a windmill graph" is a stronger result than the "friendship theorem". This generalization was proven by Mertzios and Unger, see Theorem 1 of [MertziosUnger] p. 152.). In subsection "Theorems according to Mertzios and Unger", the first steps to prove the friendship theorem following the approach of Mertzios and Unger are made by 2pthfrgrarn2 26537 and n4cyclfrgra 26545 (these theorems correspond to Proposition 1 of [MertziosUnger] p. 153.). | ||
Syntax | cfrgra 26515 | Extend class notation with Friendship Graphs. |
class FriendGrph | ||
Definition | df-frgra 26516* | Define the class of all Friendship Graphs. A graph is called a friendship graph if every pair of its vertices has exactly one common neighbor. (Contributed by Alexander van der Vekens and Mario Carneiro, 2-Oct-2017.) |
⊢ FriendGrph = {〈𝑣, 𝑒〉 ∣ (𝑣 USGrph 𝑒 ∧ ∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒)} | ||
Theorem | isfrgra 26517* | The property of being a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 FriendGrph 𝐸 ↔ (𝑉 USGrph 𝐸 ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸))) | ||
Theorem | frisusgrapr 26518* | A friendship graph is an undirected simple graph without loops with special properties. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |
⊢ (𝑉 FriendGrph 𝐸 → (𝑉 USGrph 𝐸 ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝐸)) | ||
Theorem | frisusgra 26519 | A friendship graph is an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 USGrph 𝐸) | ||
Theorem | frgra0v 26520 | Any graph with no vertex is a friendship graph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |
⊢ (∅ FriendGrph 𝐸 ↔ 𝐸 = ∅) | ||
Theorem | frgra0 26521 | Any empty graph (graph without vertices) is a friendship graph. (Contributed by Alexander van der Vekens, 30-Sep-2017.) |
⊢ ∅ FriendGrph ∅ | ||
Theorem | frgraunss 26522* | Any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Dec-2017.) |
⊢ (𝑉 FriendGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ ran 𝐸)) | ||
Theorem | frgraun 26523* | Any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Dec-2017.) |
⊢ (𝑉 FriendGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → ∃!𝑏 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝐶} ∈ ran 𝐸))) | ||
Theorem | frisusgranb 26524* | In a friendship graph, the neighborhoods of two different vertices have exactly one vertex in common. (Contributed by Alexander van der Vekens, 19-Dec-2017.) |
⊢ (𝑉 FriendGrph 𝐸 → ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃𝑥 ∈ 𝑉 ((〈𝑉, 𝐸〉 Neighbors 𝑘) ∩ (〈𝑉, 𝐸〉 Neighbors 𝑙)) = {𝑥}) | ||
Theorem | frgra1v 26525 | Any graph with only one vertex is a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |
⊢ ((𝑉 ∈ 𝑋 ∧ {𝑉} USGrph 𝐸) → {𝑉} FriendGrph 𝐸) | ||
Theorem | frgra2v 26526 | Any graph with two (different) vertices is not a friendship graph. (Contributed by Alexander van der Vekens, 30-Sep-2017.) (Proof shortened by Alexander van der Vekens, 13-Sep-2018.) |
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵) → ¬ {𝐴, 𝐵} FriendGrph 𝐸) | ||
Theorem | frgra3vlem1 26527* | Lemma 1 for frgra3v 26529. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |
⊢ ((((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ∀𝑥∀𝑦(((𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸) ∧ (𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ ran 𝐸)) → 𝑥 = 𝑦)) | ||
Theorem | frgra3vlem2 26528* | Lemma 2 for frgra3v 26529. (Contributed by Alexander van der Vekens, 4-Oct-2017.) |
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ ran 𝐸 ↔ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)))) | ||
Theorem | frgra3v 26529 | Any graph with three vertices which are completely connected with each other is a friendship graph. (Contributed by Alexander van der Vekens, 5-Oct-2017.) |
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ({𝐴, 𝐵, 𝐶} USGrph 𝐸 → ({𝐴, 𝐵, 𝐶} FriendGrph 𝐸 ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)))) | ||
Theorem | 1vwmgra 26530* | Every graph with one vertex is a windmill graph. (Contributed by Alexander van der Vekens, 5-Oct-2017.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑉 = {𝐴}) → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸)) | ||
Theorem | 3vfriswmgralem 26531* | Lemma for 3vfriswmgra 26532. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵, 𝐶} USGrph 𝐸) → ({𝐴, 𝐵} ∈ ran 𝐸 → ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ ran 𝐸)) | ||
Theorem | 3vfriswmgra 26532* | Every friendship graph with three (different) vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → (𝑉 FriendGrph 𝐸 → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸))) | ||
Theorem | 1to2vfriswmgra 26533* | Every friendship graph with one or two vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |
⊢ ((𝐴 ∈ 𝑋 ∧ (𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵})) → (𝑉 FriendGrph 𝐸 → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸))) | ||
Theorem | 1to3vfriswmgra 26534* | Every friendship graph with one, two or three vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |
⊢ ((𝐴 ∈ 𝑋 ∧ (𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵} ∨ 𝑉 = {𝐴, 𝐵, 𝐶})) → (𝑉 FriendGrph 𝐸 → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ ran 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ ran 𝐸))) | ||
Theorem | 1to3vfriendship 26535* | The friendship theorem for small graphs: In every friendship graph with one, two or three vertices, there is a vertex which is adjacent to all other vertices. (Contributed by Alexander van der Vekens, 6-Oct-2017.) |
⊢ ((𝐴 ∈ 𝑋 ∧ (𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵} ∨ 𝑉 = {𝐴, 𝐵, 𝐶})) → (𝑉 FriendGrph 𝐸 → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) | ||
Theorem | 2pthfrgrarn 26536* | Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1(b) of [MertziosUnger] p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 15-Nov-2017.) |
⊢ (𝑉 FriendGrph 𝐸 → ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸)) | ||
Theorem | 2pthfrgrarn2 26537* | Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1(b) of [MertziosUnger] p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 16-Nov-2017.) |
⊢ (𝑉 FriendGrph 𝐸 → ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃𝑏 ∈ 𝑉 (({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐))) | ||
Theorem | 2pthfrgra 26538* | Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1(b) of [MertziosUnger] p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 6-Dec-2017.) |
⊢ (𝑉 FriendGrph 𝐸 → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑓∃𝑝(𝑓(𝑎(𝑉 PathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2)) | ||
Theorem | 3cyclfrgrarn1 26539* | Every vertex in a friendship graph ( with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 16-Nov-2017.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝐴} ∈ ran 𝐸)) | ||
Theorem | 3cyclfrgrarn 26540* | Every vertex in a friendship graph ( with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 16-Nov-2017.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ 1 < (#‘𝑉)) → ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸)) | ||
Theorem | 3cyclfrgrarn2 26541* | Every vertex in a friendship graph ( with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 10-Dec-2017.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ 1 < (#‘𝑉)) → ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝑐} ∈ ran 𝐸 ∧ {𝑐, 𝑎} ∈ ran 𝐸))) | ||
Theorem | 3cyclfrgra 26542* | Every vertex in a friendship graph (with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 19-Nov-2017.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ 1 < (#‘𝑉)) → ∀𝑣 ∈ 𝑉 ∃𝑓∃𝑝(𝑓(𝑉 Cycles 𝐸)𝑝 ∧ (#‘𝑓) = 3 ∧ (𝑝‘0) = 𝑣)) | ||
Theorem | 4cycl2v2nb 26543 | In a (maybe degenerated) 4-cycle, two vertices have two (maybe not different) common neighbors. (Contributed by Alexander van der Vekens, 19-Nov-2017.) |
⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) → ({{𝐴, 𝐵}, {𝐵, 𝐶}} ⊆ ran 𝐸 ∧ {{𝐴, 𝐷}, {𝐷, 𝐶}} ⊆ ran 𝐸)) | ||
Theorem | 4cycl2vnunb 26544* | In a 4-cycle, two distinct vertices have not a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Nov-2017.) |
⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸) ∧ (𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷)) → ¬ ∃!𝑥 ∈ 𝑉 {{𝐴, 𝑥}, {𝑥, 𝐶}} ⊆ ran 𝐸) | ||
Theorem | n4cyclfrgra 26545 | There is no 4-cycle in a friendship graph, see Proposition 1(a) of [MertziosUnger] p. 153 : "A friendship graph G contains no C4 as a subgraph ...". (Contributed by Alexander van der Vekens, 19-Nov-2017.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐹(𝑉 Cycles 𝐸)𝑃) → (#‘𝐹) ≠ 4) | ||
Theorem | 4cyclusnfrgra 26546 | A graph with a 4-cycle is not a friendhip graph. (Contributed by Alexander van der Vekens, 19-Dec-2017.) |
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷)) → ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐷} ∈ ran 𝐸 ∧ {𝐷, 𝐴} ∈ ran 𝐸)) → ¬ 𝑉 FriendGrph 𝐸)) | ||
Theorem | frgranbnb 26547 | If two neighbors of a specific vertex have a common neighbor in a friendship graph, then this common neighbor must be the specific vertex. (Contributed by Alexander van der Vekens, 19-Dec-2017.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ 𝐷 = (〈𝑉, 𝐸〉 Neighbors 𝑋) & ⊢ (𝜑 → 𝑉 FriendGrph 𝐸) ⇒ ⊢ ((𝜑 ∧ (𝑈 ∈ 𝐷 ∧ 𝑊 ∈ 𝐷) ∧ 𝑈 ≠ 𝑊) → (({𝑈, 𝐴} ∈ ran 𝐸 ∧ {𝑊, 𝐴} ∈ ran 𝐸) → 𝐴 = 𝑋)) | ||
Theorem | frconngra 26548 | A friendship graph is connected, see remark 1 in [MertziosUnger] p. 153 (after Proposition 1): "An arbitrary friendship graph has to be connected, ... ". (Contributed by Alexander van der Vekens, 6-Dec-2017.) |
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 ConnGrph 𝐸) | ||
Theorem | vdfrgra0 26549 | A vertex in a friendship graph has degree 0 if the graph consists of only one vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉 ∧ (#‘𝑉) = 1) → ((𝑉 VDeg 𝐸)‘𝑁) = 0) | ||
Theorem | vdn0frgrav2 26550 | A vertex in a friendship graph with more than one vertex cannot have degree 0. (Contributed by Alexander van der Vekens, 9-Dec-2017.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (1 < (#‘𝑉) → ((𝑉 VDeg 𝐸)‘𝑁) ≠ 0)) | ||
Theorem | vdgn0frgrav2 26551 | A vertex in a friendship graph with more than one vertex cannot have degree 0. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (1 < (#‘𝑉) → ((𝑉 VDeg 𝐸)‘𝑁) ≠ 0)) | ||
Theorem | vdn1frgrav2 26552 | Any vertex in a friendship graph does not have degree 1, see remark 2 in [MertziosUnger] p. 153 (after Proposition 1): "... no node v of it [a friendship graph] may have deg(v) = 1.". (Contributed by Alexander van der Vekens, 10-Dec-2017.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (1 < (#‘𝑉) → ((𝑉 VDeg 𝐸)‘𝑁) ≠ 1)) | ||
Theorem | vdgn1frgrav2 26553 | Any vertex in a friendship graph does not have degree 1, see remark 2 in [MertziosUnger] p. 153 (after Proposition 1): "... no node v of it [a friendship graph] may have deg(v) = 1.". (Contributed by Alexander van der Vekens, 21-Dec-2017.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (1 < (#‘𝑉) → ((𝑉 VDeg 𝐸)‘𝑁) ≠ 1)) | ||
Theorem | vdgfrgragt2 26554 | Any vertex in a friendship graph (with more than one vertex - then, actually, the graph must have at least three vertices, because otherwise, it would not be a friendship graph) has at least degree 2, see remark 3 in [MertziosUnger] p. 153 (after Proposition 1): "It follows that deg(v) >= 2 for every node v of a friendship graph". (Contributed by Alexander van der Vekens, 21-Dec-2017.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (1 < (#‘𝑉) → 2 ≤ ((𝑉 VDeg 𝐸)‘𝑁))) | ||
Theorem | vdgn1frgrav3 26555* | Any vertex in a friendship graph does not have degree 1, see remark 2 in [MertziosUnger] p. 153 (after Proposition 1): "... no node v of it [a friendship graph] may have deg(v) = 1.". (Contributed by Alexander van der Vekens, 4-Sep-2018.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ 1 < (#‘𝑉)) → ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 1) | ||
Theorem | usgn0fidegnn0 26556* | In a nonempty, finite graph there is a vertex having a nonnegative integer as degree. (Contributed by Alexander van der Vekens, 6-Sep-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ∃𝑣 ∈ 𝑉 ∃𝑛 ∈ ℕ0 ((𝑉 VDeg 𝐸)‘𝑣) = 𝑛) | ||
In this section, the friendship theorem friendship 26649 is proven by formalizing Huneke's proof, see [Huneke] pp. 1-2. The three claims (see frgrancvvdgeq 26570, frgraregorufr 26580 and frgregordn0 26597) and additional statements (numbered in the order of their occurence in the paper) in Huneke's proof are cited in the corresponding theorems. | ||
Theorem | frgrancvvdeqlem1 26557* | Lemma 1 for frgrancvvdeq 26569. (Contributed by Alexander van der Vekens, 22-Dec-2017.) |
⊢ 𝐷 = (〈𝑉, 𝐸〉 Neighbors 𝑋) & ⊢ 𝑁 = (〈𝑉, 𝐸〉 Neighbors 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝑉 FriendGrph 𝐸) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑌 ∈ (𝑉 ∖ {𝑥})) | ||
Theorem | frgrancvvdeqlem2 26558* | Lemma 2 for frgrancvvdeq 26569. (Contributed by Alexander van der Vekens, 23-Dec-2017.) |
⊢ 𝐷 = (〈𝑉, 𝐸〉 Neighbors 𝑋) & ⊢ 𝑁 = (〈𝑉, 𝐸〉 Neighbors 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝑉 FriendGrph 𝐸) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸)) ⇒ ⊢ (𝜑 → 𝑋 ∉ 𝑁) | ||
Theorem | frgrancvvdeqlem3 26559* | Lemma 3 for frgrancvvdeq 26569. In a friendship graph, for each neighbor of a vertex there is exacly one neighbor of another vertex so that there is an edge between these two neighbors. (Contributed by Alexander van der Vekens, 22-Dec-2017.) |
⊢ 𝐷 = (〈𝑉, 𝐸〉 Neighbors 𝑋) & ⊢ 𝑁 = (〈𝑉, 𝐸〉 Neighbors 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝑉 FriendGrph 𝐸) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃!𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸) | ||
Theorem | frgrancvvdeqlem4 26560* | Lemma 4 for frgrancvvdeq 26569. The restricted iota of a vertex is the intersection of the corresponding neighborhoods. (Contributed by Alexander van der Vekens, 18-Dec-2017.) |
⊢ 𝐷 = (〈𝑉, 𝐸〉 Neighbors 𝑋) & ⊢ 𝑁 = (〈𝑉, 𝐸〉 Neighbors 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝑉 FriendGrph 𝐸) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸)} = ((〈𝑉, 𝐸〉 Neighbors 𝑥) ∩ 𝑁)) | ||
Theorem | frgrancvvdeqlem5 26561* | Lemma 5 for frgrancvvdeq 26569. The mapping of neighbors to neighbors is a function. (Contributed by Alexander van der Vekens, 22-Dec-2017.) |
⊢ 𝐷 = (〈𝑉, 𝐸〉 Neighbors 𝑋) & ⊢ 𝑁 = (〈𝑉, 𝐸〉 Neighbors 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝑉 FriendGrph 𝐸) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸)) ⇒ ⊢ (𝜑 → 𝐴:𝐷⟶𝑁) | ||
Theorem | frgrancvvdeqlem6 26562* | Lemma 6 for frgrancvvdeq 26569. The mapping of neighbors to neighbors applied on a vertex is the intersection of the corresponding neighborhoods. (Contributed by Alexander van der Vekens, 23-Dec-2017.) |
⊢ 𝐷 = (〈𝑉, 𝐸〉 Neighbors 𝑋) & ⊢ 𝑁 = (〈𝑉, 𝐸〉 Neighbors 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝑉 FriendGrph 𝐸) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → {(𝐴‘𝑥)} = ((〈𝑉, 𝐸〉 Neighbors 𝑥) ∩ 𝑁)) | ||
Theorem | frgrancvvdeqlem7 26563* | Lemma 7 for frgrancvvdeq 26569. (Contributed by Alexander van der Vekens, 23-Dec-2017.) |
⊢ 𝐷 = (〈𝑉, 𝐸〉 Neighbors 𝑋) & ⊢ 𝑁 = (〈𝑉, 𝐸〉 Neighbors 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝑉 FriendGrph 𝐸) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → {𝑥, (𝐴‘𝑥)} ∈ ran 𝐸) | ||
Theorem | frgrancvvdeqlemA 26564* | Lemma A for frgrancvvdeq 26569. This corresponds to statement 1 in [Huneke] p. 1: "This common neighbor cannot be x, as x and y are not adjacent.". (Contributed by Alexander van der Vekens, 23-Dec-2017.) |
⊢ 𝐷 = (〈𝑉, 𝐸〉 Neighbors 𝑋) & ⊢ 𝑁 = (〈𝑉, 𝐸〉 Neighbors 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝑉 FriendGrph 𝐸) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) ≠ 𝑋) | ||
Theorem | frgrancvvdeqlemB 26565* | Lemma B for frgrancvvdeq 26569. This corresponds to statement 2 in [Huneke] p. 1: "The map is one-to-one since z in N(x) is uniquely determined as the common neighbor of x and a(x)". (Contributed by Alexander van der Vekens, 23-Dec-2017.) |
⊢ 𝐷 = (〈𝑉, 𝐸〉 Neighbors 𝑋) & ⊢ 𝑁 = (〈𝑉, 𝐸〉 Neighbors 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝑉 FriendGrph 𝐸) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸)) ⇒ ⊢ (𝜑 → 𝐴:𝐷–1-1→ran 𝐴) | ||
Theorem | frgrancvvdeqlemC 26566* | Lemma C for frgrancvvdeq 26569. This corresponds to statement 3 in [Huneke] p. 1: "By symmetry the map is onto". (Contributed by Alexander van der Vekens, 24-Dec-2017.) |
⊢ 𝐷 = (〈𝑉, 𝐸〉 Neighbors 𝑋) & ⊢ 𝑁 = (〈𝑉, 𝐸〉 Neighbors 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝑉 FriendGrph 𝐸) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸)) ⇒ ⊢ (𝜑 → 𝐴:𝐷–onto→𝑁) | ||
Theorem | frgrancvvdeqlem8 26567* | Lemma 8 for frgrancvvdeq 26569. (Contributed by Alexander van der Vekens, 24-Dec-2017.) |
⊢ 𝐷 = (〈𝑉, 𝐸〉 Neighbors 𝑋) & ⊢ 𝑁 = (〈𝑉, 𝐸〉 Neighbors 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝑉 FriendGrph 𝐸) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ ran 𝐸)) ⇒ ⊢ (𝜑 → 𝐴:𝐷–1-1-onto→𝑁) | ||
Theorem | frgrancvvdeqlem9 26568* | Lemma 9 for frgrancvvdeq 26569. (Contributed by Alexander van der Vekens, 24-Dec-2017.) |
⊢ (𝑉 FriendGrph 𝐸 → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑥)–1-1-onto→(〈𝑉, 𝐸〉 Neighbors 𝑦))) | ||
Theorem | frgrancvvdeq 26569* | In a finite friendship graph, two vertices which are not connected by an edge have the same degree. This corresponds to claim 1 in [Huneke] p. 1: "If x,y are elements of (the friendship graph) G and are not adjacent, then they have the same degree (i.e., the same number of adjacent vertices).". (Contributed by Alexander van der Vekens, 19-Dec-2017.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐸 ∈ Fin) → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦))) | ||
Theorem | frgrancvvdgeq 26570* | In a friendship graph, two vertices which are not connected by an edge have the same degree. This corresponds to claim 1 in [Huneke] p. 1: "If x,y, are elements of (the friendship graph) G and are not adjacent, then they have the same degree (i.e., the same number of adjacent vertices).". (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Proof shortened by AV, 5-May-2021.) |
⊢ (𝑉 FriendGrph 𝐸 → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (〈𝑉, 𝐸〉 Neighbors 𝑥) → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘𝑦))) | ||
Theorem | frgrawopreglem1 26571* | Lemma 1 for frgrawopreg 26576. In a friendship graph, the classes A and B are sets. The definition of A and B corresponds to definition 3 in [Huneke] p. 2: "Let A be the set of all vertices of degree k, let B be the set of all vertices of degree different from k, ..." (Contributed by Alexander van der Vekens, 31-Dec-2017.) |
⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑥) = 𝐾} & ⊢ 𝐵 = (𝑉 ∖ 𝐴) ⇒ ⊢ (𝑉 FriendGrph 𝐸 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | frgrawopreglem2 26572* | Lemma 2 for frgrawopreg 26576. In a friendship graph with at least two vertices, the degree of a vertex must be at least 2. (Contributed by Alexander van der Vekens, 30-Dec-2017.) |
⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑥) = 𝐾} & ⊢ 𝐵 = (𝑉 ∖ 𝐴) ⇒ ⊢ ((𝑉 FriendGrph 𝐸 ∧ 1 < (#‘𝑉) ∧ 𝐴 ≠ ∅) → 1 < 𝐾) | ||
Theorem | frgrawopreglem3 26573* | Lemma 3 for frgrawopreg 26576. The vertices in the sets A and B have different degrees. (Contributed by Alexander van der Vekens, 30-Dec-2017.) |
⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑥) = 𝐾} & ⊢ 𝐵 = (𝑉 ∖ 𝐴) ⇒ ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → ((𝑉 VDeg 𝐸)‘𝑋) ≠ ((𝑉 VDeg 𝐸)‘𝑌)) | ||
Theorem | frgrawopreglem4 26574* | Lemma 4 for frgrawopreg 26576. In a friendship graph each vertex with degree K is connected with a vertex with degree other than K. This corresponds to statement 4 in [Huneke] p. 2: "By the first claim, every vertex in A is adjacent to every vertex in B.". (Contributed by Alexander van der Vekens, 30-Dec-2017.) |
⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑥) = 𝐾} & ⊢ 𝐵 = (𝑉 ∖ 𝐴) ⇒ ⊢ (𝑉 FriendGrph 𝐸 → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑎, 𝑏} ∈ ran 𝐸) | ||
Theorem | frgrawopreglem5 26575* | Lemma 5 for frgrawopreg 26576. If A as well as B contain at least two vertices in a friendship graph, there is a 4-cycle in the graph. This corresponds to statement 6 in [Huneke] p. 2: "... otherwise, there are two different vertices in A, and they have two common neighbors in B, ...". (Contributed by Alexander van der Vekens, 31-Dec-2017.) |
⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑥) = 𝐾} & ⊢ 𝐵 = (𝑉 ∖ 𝐴) ⇒ ⊢ ((𝑉 FriendGrph 𝐸 ∧ 1 < (#‘𝐴) ∧ 1 < (#‘𝐵)) → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑏 ≠ 𝑦 ∧ 𝑎 ≠ 𝑥) ∧ ({𝑎, 𝑏} ∈ ran 𝐸 ∧ {𝑥, 𝑏} ∈ ran 𝐸) ∧ ({𝑎, 𝑦} ∈ ran 𝐸 ∧ {𝑥, 𝑦} ∈ ran 𝐸))) | ||
Theorem | frgrawopreg 26576* | In a friendship graph there are either no vertices or exactly one vertex having degree K, or all or all except one vertices have degree K. (Contributed by Alexander van der Vekens, 31-Dec-2017.) |
⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑥) = 𝐾} & ⊢ 𝐵 = (𝑉 ∖ 𝐴) ⇒ ⊢ (𝑉 FriendGrph 𝐸 → (((#‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((#‘𝐵) = 1 ∨ 𝐵 = ∅))) | ||
Theorem | frgrawopreg1 26577* | According to statement 5 in [Huneke] p. 2: "If A ... is a singleton, then that singleton is a universal friend". (Contributed by Alexander van der Vekens, 1-Jan-2018.) |
⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑥) = 𝐾} & ⊢ 𝐵 = (𝑉 ∖ 𝐴) ⇒ ⊢ ((𝑉 FriendGrph 𝐸 ∧ (#‘𝐴) = 1) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸) | ||
Theorem | frgrawopreg2 26578* | According to statement 5 in [Huneke] p. 2: "If ... B is a singleton, then that singleton is a universal friend". (Contributed by Alexander van der Vekens, 1-Jan-2018.) |
⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ ((𝑉 VDeg 𝐸)‘𝑥) = 𝐾} & ⊢ 𝐵 = (𝑉 ∖ 𝐴) ⇒ ⊢ ((𝑉 FriendGrph 𝐸 ∧ (#‘𝐵) = 1) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸) | ||
Theorem | frgraregorufr0 26579* | In a friendship graph there are either no vertices having degree 𝐾, or all vertices have degree 𝐾 for any (nonnegative integer) 𝐾, unless there is a universal friend. This corresponds to claim 2 in [Huneke] p. 2: "... all vertices have degree k, unless there is a universal friend." (Contributed by Alexander van der Vekens, 1-Jan-2018.) |
⊢ (𝑉 FriendGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 𝐾 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸)) | ||
Theorem | frgraregorufr 26580* | If there is a vertex having degree 𝐾 for each (nonnegative integer) 𝐾 in a friendship graph, then either all vertices have degree 𝐾 or there is a universal friend. This corresponds to claim 2 in [Huneke] p. 2: "Suppose there is a vertex of degree k > 1. ... all vertices have degree k, unless there is a universal friend. ... It follows that G is k-regular, i.e., the degree of every vertex is k". (Contributed by Alexander van der Vekens, 1-Jan-2018.) |
⊢ (𝑉 FriendGrph 𝐸 → (∃𝑎 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑎) = 𝐾 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸))) | ||
Theorem | frgraeu 26581* | Any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
⊢ (𝑉 FriendGrph 𝐸 → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → ∃!𝑏({𝐴, 𝑏} ∈ ran 𝐸 ∧ {𝑏, 𝐶} ∈ ran 𝐸))) | ||
Theorem | frg2woteu 26582* | For two different vertices in a friendship graph, there is exactly one third vertex being the middle vertex of a (simple) path/walk of length 2 between the two vertices as ordered triple. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ∃!𝑐 ∈ 𝑉 〈𝐴, 𝑐, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) | ||
Theorem | frg2wotn0 26583 | In a friendship graph, there is always a path/walk of length 2 between two different vertices as ordered triple. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ≠ ∅) | ||
Theorem | frg2wot1 26584 | In a friendship graph, there is exactly one walk of length 2 between two different vertices as ordered triple. (Contributed by Alexander van der Vekens, 19-Feb-2018.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (#‘(𝐴(𝑉 2WalksOnOt 𝐸)𝐵)) = 1) | ||
Theorem | frg2spot1 26585 | In a friendship graph, there is exactly one simple path of length 2 between two different vertices as ordered triple. (Contributed by Alexander van der Vekens, 3-Mar-2018.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (#‘(𝐴(𝑉 2SPathOnOt 𝐸)𝐵)) = 1) | ||
Theorem | frg2woteqm 26586 | There is a (simple) path of length 2 from one vertex to another vertex in a friendship graph if and only if there is a (simple) path of length 2 from the other vertex back to the first vertex. (Contributed by Alexander van der Vekens, 20-Feb-2018.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((〈𝐴, 𝑃, 𝐵〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 〈𝐵, 𝑄, 𝐴〉 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) → 𝑄 = 𝑃)) | ||
Theorem | frg2woteq 26587 | There is a (simple) path of length 2 from one vertex to another vertex in a friendship graph if and only if there is a (simple) path of length 2 from the other vertex back to the first vertex. (Contributed by Alexander van der Vekens, 14-Feb-2018.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝐴 ≠ 𝐵) → ((𝑃 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) ∧ 𝑄 ∈ (𝐵(𝑉 2WalksOnOt 𝐸)𝐴)) → ((1st ‘(1st ‘𝑃)) = (2nd ‘𝑄) ∧ (2nd ‘(1st ‘𝑃)) = (2nd ‘(1st ‘𝑃)) ∧ (1st ‘(1st ‘𝑄)) = (2nd ‘𝑃)))) | ||
Theorem | 2spotdisj 26588* | All simple paths of length 2 as ordered triple from a fixed vertex to another vertex are disjunct. (Contributed by Alexander van der Vekens, 4-Mar-2018.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝐴 ∈ 𝑉) → Disj 𝑏 ∈ (𝑉 ∖ {𝐴})(𝐴(𝑉 2SPathOnOt 𝐸)𝑏)) | ||
Theorem | 2spotiundisj 26589* | All simple paths of length 2 as ordered triple from a fixed vertex to another vertex are disjunct. (Contributed by Alexander van der Vekens, 5-Mar-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → Disj 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ (𝑉 ∖ {𝑎})(𝑎(𝑉 2SPathOnOt 𝐸)𝑏)) | ||
Theorem | frghash2spot 26590 | The number of simple paths of length 2 is n*(n-1) in a friendship graph with 𝑛 vertices. This corresponds to the proof of claim 3 in [Huneke] p. 2: "... the paths of length two in G: by assumption there are ( n 2 ) such paths.". However, the order of vertices is not respected by Huneke, so he only counts half of the paths which are existing when respecting the order as it is the case for simple paths represented by ordered triples. (Contributed by Alexander van der Vekens, 6-Mar-2018.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → (#‘(𝑉 2SPathsOt 𝐸)) = ((#‘𝑉) · ((#‘𝑉) − 1))) | ||
Theorem | 2spot0 26591 | If there are no vertices, then there are no paths (of length 2), too. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
⊢ ((𝑉 = ∅ ∧ 𝐸 ∈ 𝑋) → (𝑉 2SPathsOt 𝐸) = ∅) | ||
Theorem | usg2spot2nb 26592* | The set of paths of length 2 with a given vertex in the middle for a finite graph is the union of all paths of length 2 from one neighbor to another neighbor of this vertex via this vertex. (Contributed by Alexander van der Vekens, 9-Mar-2018.) |
⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st ‘𝑡)) = 𝑎)}) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (𝑀‘𝑁) = ∪ 𝑥 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑁)∪ 𝑦 ∈ ((〈𝑉, 𝐸〉 Neighbors 𝑁) ∖ {𝑥}){〈𝑥, 𝑁, 𝑦〉}) | ||
Theorem | usgreghash2spotv 26593* | According to statement 7 in [Huneke] p. 2: "For each vertex v, there are exactly ( k 2 ) paths with length two having v in the middle, ..." in a finite k-regular graph. For simple paths of length 2 represented by ordered triples, we have again k*(k-1) such paths. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |
⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st ‘𝑡)) = 𝑎)}) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) → ∀𝑣 ∈ 𝑉 (((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (#‘(𝑀‘𝑣)) = (𝐾 · (𝐾 − 1)))) | ||
Theorem | usgreg2spot 26594* | In a finite k-regular graph the set of all paths of length two is the union of all the paths of length 2 over the vertices which are in the middle of such a path. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |
⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st ‘𝑡)) = 𝑎)}) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (𝑉 2SPathsOt 𝐸) = ∪ 𝑥 ∈ 𝑉 (𝑀‘𝑥))) | ||
Theorem | 2spotmdisj 26595* | The sets of paths of length 2 with a given vertex in the middle are distinct for different vertices in the middle. (Contributed by Alexander van der Vekens, 11-Mar-2018.) (Revised by AV, 17-Sep-2021.) |
⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ (𝑡 ∈ (𝑉 2SPathsOt 𝐸) ∧ (2nd ‘(1st ‘𝑡)) = 𝑎)}) ⇒ ⊢ (𝑉 ∈ 𝑊 → Disj 𝑥 ∈ 𝑉 (𝑀‘𝑥)) | ||
Theorem | usgreghash2spot 26596* | In a finite k-regular graph with N vertices there are N times "𝑘 choose 2 " paths with length 2, according to statement 8 in [Huneke] p. 2: "... giving n * ( k 2 ) total paths of length two.", if the direction of traversing the path is not respected. For simple paths of length 2 represented by ordered triples, however, we have again n*k*(k-1) such paths. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (#‘(𝑉 2SPathsOt 𝐸)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1))))) | ||
Theorem | frgregordn0 26597* | If a nonempty friendship graph is k-regular, its order is k(k-1)+1. This corresponds to claim 3 in [Huneke] p. 2: "Next we claim that the number n of vertices in G is exactly k(k-1)+1.". (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) | ||
Theorem | frrusgraord 26598 | If a nonempty finite friendship graph is k-regular, its order is k(k-1)+1. This corresponds to claim 3 in [Huneke] p. 2: "Next we claim that the number n of vertices in G is exactly k(k-1)+1.". Variant of frgregordn0 26597, using the definition RegUSGrph (df-rusgra 26452). (Contributed by Alexander van der Vekens, 25-Aug-2018.) |
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) | ||
Theorem | frgraregorufrg 26599* | If there is a vertex having degree 𝑘 for each nonnegative integer 𝑘 in a friendship graph, then there is a universal friend. This corresponds to claim 2 in [Huneke] p. 2: "Suppose there is a vertex of degree k > 1. ... all vertices have degree k, unless there is a universal friend. ... It follows that G is k-regular, i.e., the degree of every vertex is k". Variant of frgraregorufr 26580 with generalization. (Contributed by Alexander van der Vekens, 6-Sep-2018.) |
⊢ (𝑉 FriendGrph 𝐸 → ∀𝑘 ∈ ℕ0 (∃𝑎 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑎) = 𝑘 → (〈𝑉, 𝐸〉 RegUSGrph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ ran 𝐸))) | ||
Theorem | numclwlk3lem3 26600 | Lemma 3 for numclwwlk3 26636. (Contributed by Alexander van der Vekens, 26-Aug-2018.) |
⊢ ((𝐾 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ 𝑁 ∈ (ℤ≥‘2)) → (((𝐾↑(𝑁 − 2)) − 𝑌) + (𝐾 · 𝑌)) = (((𝐾 − 1) · 𝑌) + (𝐾↑(𝑁 − 2)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |