Home | Metamath
Proof Explorer Theorem List (p. 281 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | trlsegvdeglem3 28001 | Lemma for trlsegvdeg 28006. (Contributed by AV, 20-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → Fun (iEdg‘𝑌)) | ||
Theorem | trlsegvdeglem4 28002 | Lemma for trlsegvdeg 28006. (Contributed by AV, 21-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → dom (iEdg‘𝑋) = ((𝐹 “ (0..^𝑁)) ∩ dom 𝐼)) | ||
Theorem | trlsegvdeglem5 28003 | Lemma for trlsegvdeg 28006. (Contributed by AV, 21-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → dom (iEdg‘𝑌) = {(𝐹‘𝑁)}) | ||
Theorem | trlsegvdeglem6 28004 | Lemma for trlsegvdeg 28006. (Contributed by AV, 21-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → dom (iEdg‘𝑋) ∈ Fin) | ||
Theorem | trlsegvdeglem7 28005 | Lemma for trlsegvdeg 28006. (Contributed by AV, 21-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → dom (iEdg‘𝑌) ∈ Fin) | ||
Theorem | trlsegvdeg 28006 | Formerly part of proof of eupth2lem3 28015: If a trail in a graph 𝐺 induces a subgraph 𝑍 with the vertices 𝑉 of 𝐺 and the edges being the edges of the walk, and a subgraph 𝑋 with the vertices 𝑉 of 𝐺 and the edges being the edges of the walk except the last one, and a subgraph 𝑌 with the vertices 𝑉 of 𝐺 and one edges being the last edge of the walk, then the vertex degree of any vertex 𝑈 of 𝐺 within 𝑍 is the sum of the vertex degree of 𝑈 within 𝑋 and the vertex degree of 𝑈 within 𝑌. Note that this theorem would not hold for arbitrary walks (if the last edge was identical with a previous edge, the degree of the vertices incident with this edge would not be increased because of this edge). (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 20-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝑍)‘𝑈) = (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈))) | ||
Theorem | eupth2lem3lem1 28007 | Lemma for eupth2lem3 28015. (Contributed by AV, 21-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℕ0) | ||
Theorem | eupth2lem3lem2 28008 | Lemma for eupth2lem3 28015. (Contributed by AV, 21-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝑌)‘𝑈) ∈ ℕ0) | ||
Theorem | eupth2lem3lem3 28009* | Lemma for eupth2lem3 28015, formerly part of proof of eupth2lem3 28015: If a loop {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} is added to a trail, the degree of the vertices with odd degree remains odd (regarding the subgraphs induced by the involved trails). (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 21-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) & ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})) & ⊢ (𝜑 → if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) ⇒ ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) | ||
Theorem | eupth2lem3lem4 28010* | Lemma for eupth2lem3 28015, formerly part of proof of eupth2lem3 28015: If an edge (not a loop) is added to a trail, the degree of the end vertices of this edge remains odd if it was odd before (regarding the subgraphs induced by the involved trails). (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 25-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) & ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})) & ⊢ (𝜑 → if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))) & ⊢ (𝜑 → (𝐼‘(𝐹‘𝑁)) ∈ 𝒫 𝑉) ⇒ ⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑈 = (𝑃‘𝑁) ∨ 𝑈 = (𝑃‘(𝑁 + 1)))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) | ||
Theorem | eupth2lem3lem5 28011* | Lemma for eupth2 28018. (Contributed by AV, 25-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) & ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})) & ⊢ (𝜑 → (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}) ⇒ ⊢ (𝜑 → (𝐼‘(𝐹‘𝑁)) ∈ 𝒫 𝑉) | ||
Theorem | eupth2lem3lem6 28012* | Formerly part of proof of eupth2lem3 28015: If an edge (not a loop) is added to a trail, the degree of vertices not being end vertices of this edge remains odd if it was odd before (regarding the subgraphs induced by the involved trails). Remark: This seems to be not valid for hyperedges joining more vertices than (𝑃‘0) and (𝑃‘𝑁): if there is a third vertex in the edge, and this vertex is already contained in the trail, then the degree of this vertex could be affected by this edge! (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 25-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) & ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})) & ⊢ (𝜑 → (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}) ⇒ ⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑈 ≠ (𝑃‘𝑁) ∧ 𝑈 ≠ (𝑃‘(𝑁 + 1)))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) | ||
Theorem | eupth2lem3lem7 28013* | Lemma for eupth2lem3 28015: Combining trlsegvdeg 28006, eupth2lem3lem3 28009, eupth2lem3lem4 28010 and eupth2lem3lem6 28012. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 27-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) & ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})) & ⊢ (𝜑 → (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))}) ⇒ ⊢ (𝜑 → (¬ 2 ∥ ((VtxDeg‘𝑍)‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) | ||
Theorem | eupthvdres 28014 | Formerly part of proof of eupth2 28018: The vertex degree remains the same for all vertices if the edges are restricted to the edges of an Eulerian path. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) & ⊢ 𝐻 = 〈𝑉, (𝐼 ↾ (𝐹 “ (0..^(♯‘𝐹))))〉 ⇒ ⊢ (𝜑 → (VtxDeg‘𝐻) = (VtxDeg‘𝐺)) | ||
Theorem | eupth2lem3 28015* | Lemma for eupth2 28018. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ UPGraph) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) & ⊢ 𝐻 = 〈𝑉, (𝐼 ↾ (𝐹 “ (0..^𝑁)))〉 & ⊢ 𝑋 = 〈𝑉, (𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1))))〉 & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝑁 + 1) ≤ (♯‘𝐹)) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐻)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)})) ⇒ ⊢ (𝜑 → (¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))}))) | ||
Theorem | eupth2lemb 28016* | Lemma for eupth2 28018 (induction basis): There are no vertices of odd degree in an Eulerian path of length 0, having no edge and identical endpoints (the single vertex of the Eulerian path). Formerly part of proof for eupth2 28018. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ UPGraph) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘〈𝑉, (𝐼 ↾ (𝐹 “ (0..^0)))〉)‘𝑥)} = ∅) | ||
Theorem | eupth2lems 28017* | Lemma for eupth2 28018 (induction step): The only vertices of odd degree in a graph with an Eulerian path are the endpoints, and then only if the endpoints are distinct, if the Eulerian path shortened by one edge has this property. Formerly part of proof for eupth2 28018. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ UPGraph) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) ⇒ ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ≤ (♯‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘〈𝑉, (𝐼 ↾ (𝐹 “ (0..^𝑛)))〉)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)})) → ((𝑛 + 1) ≤ (♯‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘〈𝑉, (𝐼 ↾ (𝐹 “ (0..^(𝑛 + 1))))〉)‘𝑥)} = if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))})))) | ||
Theorem | eupth2 28018* | 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.) (Revised by AV, 26-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ UPGraph) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)} = if((𝑃‘0) = (𝑃‘(♯‘𝐹)), ∅, {(𝑃‘0), (𝑃‘(♯‘𝐹))})) | ||
Theorem | eulerpathpr 28019* | A graph with an Eulerian path has either zero or two vertices of odd degree. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 26-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(EulerPaths‘𝐺)𝑃) → (♯‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)}) ∈ {0, 2}) | ||
Theorem | eulerpath 28020* | A pseudograph with an Eulerian path has either zero or two vertices of odd degree. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 26-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ (EulerPaths‘𝐺) ≠ ∅) → (♯‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)}) ∈ {0, 2}) | ||
Theorem | eulercrct 28021* | A pseudograph with an Eulerian circuit 〈𝐹, 𝑃〉 (an "Eulerian pseudograph") has only vertices of even degree. (Contributed by AV, 12-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(EulerPaths‘𝐺)𝑃 ∧ 𝐹(Circuits‘𝐺)𝑃) → ∀𝑥 ∈ 𝑉 2 ∥ ((VtxDeg‘𝐺)‘𝑥)) | ||
Theorem | eucrctshift 28022* | Cyclically shifting the indices of an Eulerian circuit 〈𝐹, 𝑃〉 results in an Eulerian circuit 〈𝐻, 𝑄〉. (Contributed by AV, 15-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃) & ⊢ 𝑁 = (♯‘𝐹) & ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁)) & ⊢ 𝐻 = (𝐹 cyclShift 𝑆) & ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) & ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) ⇒ ⊢ (𝜑 → (𝐻(EulerPaths‘𝐺)𝑄 ∧ 𝐻(Circuits‘𝐺)𝑄)) | ||
Theorem | eucrct2eupth1 28023 | Removing one edge (𝐼‘(𝐹‘𝑁)) from a nonempty graph 𝐺 with an Eulerian circuit 〈𝐹, 𝑃〉 results in a graph 𝑆 with an Eulerian path 〈𝐻, 𝑄〉. This is the special case of eucrct2eupth 28024 (with 𝐽 = (𝑁 − 1)) where the last segment/edge of the circuit is removed. (Contributed by AV, 11-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) & ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃) & ⊢ (Vtx‘𝑆) = 𝑉 & ⊢ (𝜑 → 0 < (♯‘𝐹)) & ⊢ (𝜑 → 𝑁 = ((♯‘𝐹) − 1)) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ 𝐻 = (𝐹 prefix 𝑁) & ⊢ 𝑄 = (𝑃 ↾ (0...𝑁)) ⇒ ⊢ (𝜑 → 𝐻(EulerPaths‘𝑆)𝑄) | ||
Theorem | eucrct2eupth 28024* | Removing one edge (𝐼‘(𝐹‘𝐽)) from a graph 𝐺 with an Eulerian circuit 〈𝐹, 𝑃〉 results in a graph 𝑆 with an Eulerian path 〈𝐻, 𝑄〉. (Contributed by AV, 17-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) & ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃) & ⊢ (Vtx‘𝑆) = 𝑉 & ⊢ (𝜑 → 𝑁 = (♯‘𝐹)) & ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁)) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽})))) & ⊢ 𝐾 = (𝐽 + 1) & ⊢ 𝐻 = ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1)) & ⊢ 𝑄 = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ⇒ ⊢ (𝜑 → 𝐻(EulerPaths‘𝑆)𝑄) | ||
According to Wikipedia ("Seven Bridges of Königsberg", 9-Mar-2021, https://en.wikipedia.org/wiki/Seven_Bridges_of_Koenigsberg): "The Seven Bridges of Königsberg is a historically notable problem in mathematics. Its negative resolution by Leonhard Euler in 1736 laid the foundations of graph theory and prefigured the idea of topology. The city of Königsberg in [East] Prussia (now Kaliningrad, Russia) was set on both sides of the Pregel River, and included two large islands - Kneiphof and Lomse - which were connected to each other, or to the two mainland portions of the city, by seven bridges. The problem was to devise a walk through the city that would cross each of those bridges once and only once.". Euler proved that the problem has no solution by applying Euler's theorem to the Königsberg graph, which is obtained by replacing each land mass with an abstract "vertex" or node, and each bridge with an abstract connection, an "edge", which connects two land masses/vertices. The Königsberg graph 𝐺 is a multigraph consisting of 4 vertices and 7 edges, represented by the following ordered pair: 𝐺 = 〈(0...3), 〈“{0, 1}{0, 2} {0, 3}{1, 2}{1, 2}{2, 3}{2, 3}”〉〉, see konigsbergumgr 28030. konigsberg 28036 shows that the Königsberg graph has no Eulerian path, thus the Königsberg Bridge problem has no solution. | ||
Theorem | konigsbergvtx 28025 | The set of vertices of the Königsberg graph 𝐺. (Contributed by AV, 28-Feb-2021.) |
⊢ 𝑉 = (0...3) & ⊢ 𝐸 = 〈“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ (Vtx‘𝐺) = (0...3) | ||
Theorem | konigsbergiedg 28026 | The indexed edges of the Königsberg graph 𝐺. (Contributed by AV, 28-Feb-2021.) |
⊢ 𝑉 = (0...3) & ⊢ 𝐸 = 〈“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ (iEdg‘𝐺) = 〈“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”〉 | ||
Theorem | konigsbergiedgw 28027* | The indexed edges of the Königsberg graph 𝐺 is a word over the pairs of vertices. (Contributed by AV, 28-Feb-2021.) |
⊢ 𝑉 = (0...3) & ⊢ 𝐸 = 〈“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ 𝐸 ∈ Word {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} | ||
Theorem | konigsbergssiedgwpr 28028* | Each subset of the indexed edges of the Königsberg graph 𝐺 is a word over the pairs of vertices. (Contributed by AV, 28-Feb-2021.) |
⊢ 𝑉 = (0...3) & ⊢ 𝐸 = 〈“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ∧ 𝐸 = (𝐴 ++ 𝐵)) → 𝐴 ∈ Word {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) | ||
Theorem | konigsbergssiedgw 28029* | Each subset of the indexed edges of the Königsberg graph 𝐺 is a word over the pairs of vertices. (Contributed by AV, 28-Feb-2021.) |
⊢ 𝑉 = (0...3) & ⊢ 𝐸 = 〈“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ∧ 𝐸 = (𝐴 ++ 𝐵)) → 𝐴 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}) | ||
Theorem | konigsbergumgr 28030 | The Königsberg graph 𝐺 is a multigraph. (Contributed by AV, 28-Feb-2021.) (Revised by AV, 9-Mar-2021.) |
⊢ 𝑉 = (0...3) & ⊢ 𝐸 = 〈“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ 𝐺 ∈ UMGraph | ||
Theorem | konigsberglem1 28031 | Lemma 1 for konigsberg 28036: Vertex 0 has degree three. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 4-Mar-2021.) |
⊢ 𝑉 = (0...3) & ⊢ 𝐸 = 〈“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ ((VtxDeg‘𝐺)‘0) = 3 | ||
Theorem | konigsberglem2 28032 | Lemma 2 for konigsberg 28036: Vertex 1 has degree three. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 4-Mar-2021.) |
⊢ 𝑉 = (0...3) & ⊢ 𝐸 = 〈“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ ((VtxDeg‘𝐺)‘1) = 3 | ||
Theorem | konigsberglem3 28033 | Lemma 3 for konigsberg 28036: Vertex 3 has degree three. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 4-Mar-2021.) |
⊢ 𝑉 = (0...3) & ⊢ 𝐸 = 〈“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ ((VtxDeg‘𝐺)‘3) = 3 | ||
Theorem | konigsberglem4 28034* | Lemma 4 for konigsberg 28036: Vertices 0, 1, 3 are vertices of odd degree. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 28-Feb-2021.) |
⊢ 𝑉 = (0...3) & ⊢ 𝐸 = 〈“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ {0, 1, 3} ⊆ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)} | ||
Theorem | konigsberglem5 28035* | Lemma 5 for konigsberg 28036: The set of vertices of odd degree is greater than 2. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 28-Feb-2021.) |
⊢ 𝑉 = (0...3) & ⊢ 𝐸 = 〈“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ 2 < (♯‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)}) | ||
Theorem | konigsberg 28036 | The Königsberg Bridge problem. If 𝐺 is the Königsberg graph, i.e. a 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 eulerpath 28020 the graph cannot have an Eulerian path. It is sufficient to show that there are 3 vertices of odd degree, since a graph having an Eulerian path can only have 0 or 2 vertices of odd degree. This is Metamath 100 proof #54. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 9-Mar-2021.) |
⊢ 𝑉 = (0...3) & ⊢ 𝐸 = 〈“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”〉 & ⊢ 𝐺 = 〈𝑉, 𝐸〉 ⇒ ⊢ (EulerPaths‘𝐺) = ∅ | ||
Syntax | cfrgr 28037 | Extend class notation with friendship graphs. |
class FriendGraph | ||
Definition | df-frgr 28038* | Define the class of all friendship graphs: a simple graph is called a friendship graph if every pair of its vertices has exactly one common neighbor. This condition is called the friendship condition , see definition in [MertziosUnger] p. 152. (Contributed by Alexander van der Vekens and Mario Carneiro, 2-Oct-2017.) (Revised by AV, 29-Mar-2021.) (Revised by AV, 3-Jan-2024.) |
⊢ FriendGraph = {𝑔 ∈ USGraph ∣ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒} | ||
Theorem | isfrgr 28039* | The property of being a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) (Revised by AV, 3-Jan-2024.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ FriendGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸)) | ||
Theorem | frgrusgr 28040 | A friendship graph is a simple graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) |
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph) | ||
Theorem | frgr0v 28041 | Any null graph (set with no vertices) is a friendship graph iff its edge function is empty. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) |
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → (𝐺 ∈ FriendGraph ↔ (iEdg‘𝐺) = ∅)) | ||
Theorem | frgr0vb 28042 | Any null graph (without vertices and edges) is a friendship graph. (Contributed by Alexander van der Vekens, 30-Sep-2017.) (Revised by AV, 29-Mar-2021.) |
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅ ∧ (iEdg‘𝐺) = ∅) → 𝐺 ∈ FriendGraph ) | ||
Theorem | frgruhgr0v 28043 | Any null graph (without vertices) represented as hypergraph is a friendship graph. (Contributed by AV, 29-Mar-2021.) |
⊢ ((𝐺 ∈ UHGraph ∧ (Vtx‘𝐺) = ∅) → 𝐺 ∈ FriendGraph ) | ||
Theorem | frgr0 28044 | The null graph (graph without vertices) is a friendship graph. (Contributed by AV, 29-Mar-2021.) |
⊢ ∅ ∈ FriendGraph | ||
Theorem | frcond1 28045* | The friendship condition: any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 29-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ FriendGraph → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ 𝐸)) | ||
Theorem | frcond2 28046* | The friendship condition: any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 29-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ FriendGraph → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → ∃!𝑏 ∈ 𝑉 ({𝐴, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝐶} ∈ 𝐸))) | ||
Theorem | frgreu 28047* | Variant of frcond2 28046: Any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 12-May-2021.) (Proof shortened by AV, 4-Jan-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ FriendGraph → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → ∃!𝑏({𝐴, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝐶} ∈ 𝐸))) | ||
Theorem | frcond3 28048* | The friendship condition, expressed by neighborhoods: in a friendship graph, the neighborhood of a vertex and the neighborhood of a second, different vertex have exactly one vertex in common. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 30-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ FriendGraph → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → ∃𝑥 ∈ 𝑉 ((𝐺 NeighbVtx 𝐴) ∩ (𝐺 NeighbVtx 𝐶)) = {𝑥})) | ||
Theorem | frcond4 28049* | The friendship condition, alternatively expressed by neighborhoods: 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.) (Revised by AV, 29-Mar-2021.) (Proof shortened by AV, 30-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ FriendGraph → ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃𝑥 ∈ 𝑉 ((𝐺 NeighbVtx 𝑘) ∩ (𝐺 NeighbVtx 𝑙)) = {𝑥}) | ||
Theorem | frgr1v 28050 | Any graph with (at most) one vertex is a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) |
⊢ ((𝐺 ∈ USGraph ∧ (Vtx‘𝐺) = {𝑁}) → 𝐺 ∈ FriendGraph ) | ||
Theorem | nfrgr2v 28051 | 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.) (Revised by AV, 29-Mar-2021.) |
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵) ∧ (Vtx‘𝐺) = {𝐴, 𝐵}) → 𝐺 ∉ FriendGraph ) | ||
Theorem | frgr3vlem1 28052* | Lemma 1 for frgr3v 28054. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ∀𝑥∀𝑦(((𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸) ∧ (𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ 𝐸)) → 𝑥 = 𝑦)) | ||
Theorem | frgr3vlem2 28053* | Lemma 2 for frgr3v 28054. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)))) | ||
Theorem | frgr3v 28054 | 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.) (Revised by AV, 29-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝐺 ∈ FriendGraph ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)))) | ||
Theorem | 1vwmgr 28055* | Every graph with one vertex (which may be connect with itself by (multiple) loops!) is a windmill graph. (Contributed by Alexander van der Vekens, 5-Oct-2017.) (Revised by AV, 31-Mar-2021.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑉 = {𝐴}) → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)) | ||
Theorem | 3vfriswmgrlem 28056* | Lemma for 3vfriswmgr 28057. (Contributed by Alexander van der Vekens, 6-Oct-2017.) (Revised by AV, 31-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ({𝐴, 𝐵} ∈ 𝐸 → ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ 𝐸)) | ||
Theorem | 3vfriswmgr 28057* | Every friendship graph with three (different) vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.) (Revised by AV, 31-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))) | ||
Theorem | 1to2vfriswmgr 28058* | Every friendship graph with one or two vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.) (Revised by AV, 31-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ (𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵})) → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))) | ||
Theorem | 1to3vfriswmgr 28059* | Every friendship graph with one, two or three vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.) (Revised by AV, 31-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ (𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵} ∨ 𝑉 = {𝐴, 𝐵, 𝐶})) → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))) | ||
Theorem | 1to3vfriendship 28060* | 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.) (Revised by AV, 31-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ (𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵} ∨ 𝑉 = {𝐴, 𝐵, 𝐶})) → (𝐺 ∈ FriendGraph → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ 𝐸)) | ||
Theorem | 2pthfrgrrn 28061* | 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.) (Revised by AV, 1-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ FriendGraph → ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸)) | ||
Theorem | 2pthfrgrrn2 28062* | 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.) (Revised by AV, 1-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ FriendGraph → ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃𝑏 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐))) | ||
Theorem | 2pthfrgr 28063* | Between any two (different) vertices in a friendship graph, tere is a 2-path (simple 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.) (Revised by AV, 1-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ FriendGraph → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑓∃𝑝(𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑝 ∧ (♯‘𝑓) = 2)) | ||
Theorem | 3cyclfrgrrn1 28064* | 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.) (Revised by AV, 2-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝐴} ∈ 𝐸)) | ||
Theorem | 3cyclfrgrrn 28065* | 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.) (Revised by AV, 2-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ FriendGraph ∧ 1 < (♯‘𝑉)) → ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) | ||
Theorem | 3cyclfrgrrn2 28066* | 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.) (Revised by AV, 2-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ FriendGraph ∧ 1 < (♯‘𝑉)) → ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸))) | ||
Theorem | 3cyclfrgr 28067* | 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.) (Revised by AV, 2-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FriendGraph ∧ 1 < (♯‘𝑉)) → ∀𝑣 ∈ 𝑉 ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝑣)) | ||
Theorem | 4cycl2v2nb 28068 | In a (maybe degenerate) 4-cycle, two vertice have two (maybe not different) common neighbors. (Contributed by Alexander van der Vekens, 19-Nov-2017.) (Revised by AV, 2-Apr-2021.) |
⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐷} ∈ 𝐸 ∧ {𝐷, 𝐴} ∈ 𝐸)) → ({{𝐴, 𝐵}, {𝐵, 𝐶}} ⊆ 𝐸 ∧ {{𝐴, 𝐷}, {𝐷, 𝐶}} ⊆ 𝐸)) | ||
Theorem | 4cycl2vnunb 28069* | In a 4-cycle, two distinct vertices have not a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Nov-2017.) (Revised by AV, 2-Apr-2021.) |
⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐷} ∈ 𝐸 ∧ {𝐷, 𝐴} ∈ 𝐸) ∧ (𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷)) → ¬ ∃!𝑥 ∈ 𝑉 {{𝐴, 𝑥}, {𝑥, 𝐶}} ⊆ 𝐸) | ||
Theorem | n4cyclfrgr 28070 | 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.) (Revised by AV, 2-Apr-2021.) |
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐹(Cycles‘𝐺)𝑃) → (♯‘𝐹) ≠ 4) | ||
Theorem | 4cyclusnfrgr 28071 | A graph with a 4-cycle is not a friendhip graph. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 2-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷)) → ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐷} ∈ 𝐸 ∧ {𝐷, 𝐴} ∈ 𝐸)) → 𝐺 ∉ FriendGraph )) | ||
Theorem | frgrnbnb 28072 | If two neighbors 𝑈 and 𝑊 of a vertex 𝑋 have a common neighbor 𝐴 in a friendship graph, then this common neighbor 𝐴 must be the vertex 𝑋. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 2-Apr-2021.) (Proof shortened by AV, 13-Feb-2022.) |
⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋) ⇒ ⊢ ((𝐺 ∈ FriendGraph ∧ (𝑈 ∈ 𝐷 ∧ 𝑊 ∈ 𝐷) ∧ 𝑈 ≠ 𝑊) → (({𝑈, 𝐴} ∈ 𝐸 ∧ {𝑊, 𝐴} ∈ 𝐸) → 𝐴 = 𝑋)) | ||
Theorem | frgrconngr 28073 | 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.) (Revised by AV, 1-Apr-2021.) |
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ ConnGraph) | ||
Theorem | vdgn0frgrv2 28074 | A vertex in a friendship graph 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‘𝐺) ⇒ ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉) → (1 < (♯‘𝑉) → ((VtxDeg‘𝐺)‘𝑁) ≠ 0)) | ||
Theorem | vdgn1frgrv2 28075 | 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.) (Revised by AV, 4-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉) → (1 < (♯‘𝑉) → ((VtxDeg‘𝐺)‘𝑁) ≠ 1)) | ||
Theorem | vdgn1frgrv3 28076* | 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.) (Revised by AV, 4-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FriendGraph ∧ 1 < (♯‘𝑉)) → ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 1) | ||
Theorem | vdgfrgrgt2 28077 | 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.) (Revised by AV, 5-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉) → (1 < (♯‘𝑉) → 2 ≤ ((VtxDeg‘𝐺)‘𝑁))) | ||
In this section, the friendship theorem friendship 28178 is proven by formalizing Huneke's proof, see [Huneke] pp. 1-2. The three claims (see frgrncvvdeq 28088, frgrregorufr 28104 and frrusgrord0 28119) and additional statements (numbered in the order of their occurrence in the paper) in Huneke's proof are cited in the corresponding theorems. | ||
Theorem | frgrncvvdeqlem1 28078 | Lemma 1 for frgrncvvdeq 28088. (Contributed by Alexander van der Vekens, 23-Dec-2017.) (Revised by AV, 8-May-2021.) (Proof shortened by AV, 12-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝐺 ∈ FriendGraph ) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) ⇒ ⊢ (𝜑 → 𝑋 ∉ 𝑁) | ||
Theorem | frgrncvvdeqlem2 28079* | Lemma 2 for frgrncvvdeq 28088. In a friendship graph, for each neighbor of a vertex there is exactly one neighbor of another vertex so that there is an edge between these two neighbors. (Contributed by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 12-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝐺 ∈ FriendGraph ) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃!𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸) | ||
Theorem | frgrncvvdeqlem3 28080* | Lemma 3 for frgrncvvdeq 28088. The unique neighbor of a vertex (expressed by a restricted iota) is the intersection of the corresponding neighborhoods. (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 12-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝐺 ∈ FriendGraph ) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)} = ((𝐺 NeighbVtx 𝑥) ∩ 𝑁)) | ||
Theorem | frgrncvvdeqlem4 28081* | Lemma 4 for frgrncvvdeq 28088. The mapping of neighbors to neighbors is a function. (Contributed by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 10-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝐺 ∈ FriendGraph ) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) ⇒ ⊢ (𝜑 → 𝐴:𝐷⟶𝑁) | ||
Theorem | frgrncvvdeqlem5 28082* | Lemma 5 for frgrncvvdeq 28088. 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.) (Revised by AV, 10-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝐺 ∈ FriendGraph ) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → {(𝐴‘𝑥)} = ((𝐺 NeighbVtx 𝑥) ∩ 𝑁)) | ||
Theorem | frgrncvvdeqlem6 28083* | Lemma 6 for frgrncvvdeq 28088. (Contributed by Alexander van der Vekens, 23-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 30-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝐺 ∈ FriendGraph ) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → {𝑥, (𝐴‘𝑥)} ∈ 𝐸) | ||
Theorem | frgrncvvdeqlem7 28084* | Lemma 7 for frgrncvvdeq 28088. This corresponds to statement 1 in [Huneke] p. 1: "This common neighbor cannot be x, as x and y are not adjacent.". This is only an observation, which is not required to proof the friendship theorem. (Contributed by Alexander van der Vekens, 23-Dec-2017.) (Revised by AV, 10-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝐺 ∈ FriendGraph ) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) ≠ 𝑋) | ||
Theorem | frgrncvvdeqlem8 28085* | Lemma 8 for frgrncvvdeq 28088. 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.) (Revised by AV, 10-May-2021.) (Revised by AV, 30-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝐺 ∈ FriendGraph ) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) ⇒ ⊢ (𝜑 → 𝐴:𝐷–1-1→𝑁) | ||
Theorem | frgrncvvdeqlem9 28086* | Lemma 9 for frgrncvvdeq 28088. This corresponds to statement 3 in [Huneke] p. 1: "By symmetry the map is onto". (Contributed by Alexander van der Vekens, 24-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 12-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝐺 ∈ FriendGraph ) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) ⇒ ⊢ (𝜑 → 𝐴:𝐷–onto→𝑁) | ||
Theorem | frgrncvvdeqlem10 28087* | Lemma 10 for frgrncvvdeq 28088. (Contributed by Alexander van der Vekens, 24-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 30-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋) & ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑌 ∉ 𝐷) & ⊢ (𝜑 → 𝐺 ∈ FriendGraph ) & ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)) ⇒ ⊢ (𝜑 → 𝐴:𝐷–1-1-onto→𝑁) | ||
Theorem | frgrncvvdeq 28088* | 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.) (Revised by AV, 10-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ (𝐺 ∈ FriendGraph → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (𝐺 NeighbVtx 𝑥) → (𝐷‘𝑥) = (𝐷‘𝑦))) | ||
Theorem | frgrwopreglem4a 28089 | In a friendship graph any two vertices with different degrees are connected. Alternate version of frgrwopreglem4 28094 without a fixed degree and without using the sets 𝐴 and 𝐵. (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 4-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ FriendGraph ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ≠ (𝐷‘𝑌)) → {𝑋, 𝑌} ∈ 𝐸) | ||
Theorem | frgrwopreglem5a 28090 | If a friendship graph has two vertices with the same degree and two other vertices with different degrees, then there is a 4-cycle in the graph. Alternate version of frgrwopreglem5 28100 without a fixed degree and without using the sets 𝐴 and 𝐵. (Contributed by Alexander van der Vekens, 31-Dec-2017.) (Revised by AV, 4-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ FriendGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ ((𝐷‘𝐴) = (𝐷‘𝑋) ∧ (𝐷‘𝐴) ≠ (𝐷‘𝐵) ∧ (𝐷‘𝑋) ≠ (𝐷‘𝑌))) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝑋} ∈ 𝐸) ∧ ({𝑋, 𝑌} ∈ 𝐸 ∧ {𝑌, 𝐴} ∈ 𝐸))) | ||
Theorem | frgrwopreglem1 28091* | Lemma 1 for frgrwopreg 28102: the classes 𝐴 and 𝐵 are sets. The definition of 𝐴 and 𝐵 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.) (Revised by AV, 10-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) & ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} & ⊢ 𝐵 = (𝑉 ∖ 𝐴) ⇒ ⊢ (𝐴 ∈ V ∧ 𝐵 ∈ V) | ||
Theorem | frgrwopreglem2 28092* | Lemma 2 for frgrwopreg 28102. If the set 𝐴 of vertices of degree 𝐾 is not empty in a friendship graph with at least two vertices, then 𝐾 must be greater than 1 . This is only an observation, which is not required for the proof the friendship theorem. (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 2-Jan-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) & ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} & ⊢ 𝐵 = (𝑉 ∖ 𝐴) ⇒ ⊢ ((𝐺 ∈ FriendGraph ∧ 1 < (♯‘𝑉) ∧ 𝐴 ≠ ∅) → 2 ≤ 𝐾) | ||
Theorem | frgrwopreglem3 28093* | Lemma 3 for frgrwopreg 28102. The vertices in the sets 𝐴 and 𝐵 have different degrees. (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 2-Jan-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) & ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} & ⊢ 𝐵 = (𝑉 ∖ 𝐴) ⇒ ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝐷‘𝑋) ≠ (𝐷‘𝑌)) | ||
Theorem | frgrwopreglem4 28094* | Lemma 4 for frgrwopreg 28102. In a friendship graph each vertex with degree 𝐾 is connected with any vertex with degree other than 𝐾. 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.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 4-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) & ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} & ⊢ 𝐵 = (𝑉 ∖ 𝐴) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ FriendGraph → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑎, 𝑏} ∈ 𝐸) | ||
Theorem | frgrwopregasn 28095* | According to statement 5 in [Huneke] p. 2: "If A ... is a singleton, then that singleton is a universal friend". This version of frgrwopreg1 28097 is stricter (claiming that the singleton itself is a universal friend instead of claiming the existence of a universal friend only) and therefore closer to Huneke's statement. This strict variant, however, is not required for the proof of the friendship theorem. (Contributed by Alexander van der Vekens, 1-Jan-2018.) (Revised by AV, 4-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) & ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} & ⊢ 𝐵 = (𝑉 ∖ 𝐴) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝐴 = {𝑋}) → ∀𝑤 ∈ (𝑉 ∖ {𝑋}){𝑋, 𝑤} ∈ 𝐸) | ||
Theorem | frgrwopregbsn 28096* | According to statement 5 in [Huneke] p. 2: "If ... B is a singleton, then that singleton is a universal friend". This version of frgrwopreg2 28098 is stricter (claiming that the singleton itself is a universal friend instead of claiming the existence of a universal friend only) and therefore closer to Huneke's statement. This strict variant, however, is not required for the proof of the friendship theorem. (Contributed by AV, 4-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) & ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} & ⊢ 𝐵 = (𝑉 ∖ 𝐴) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝐵 = {𝑋}) → ∀𝑤 ∈ (𝑉 ∖ {𝑋}){𝑋, 𝑤} ∈ 𝐸) | ||
Theorem | frgrwopreg1 28097* | 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.) (Proof shortened by AV, 4-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) & ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} & ⊢ 𝐵 = (𝑉 ∖ 𝐴) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ FriendGraph ∧ (♯‘𝐴) = 1) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ 𝐸) | ||
Theorem | frgrwopreg2 28098* | 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.) (Proof shortened by AV, 4-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) & ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} & ⊢ 𝐵 = (𝑉 ∖ 𝐴) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ FriendGraph ∧ (♯‘𝐵) = 1) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ 𝐸) | ||
Theorem | frgrwopreglem5lem 28099* | Lemma for frgrwopreglem5 28100. (Contributed by AV, 5-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) & ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} & ⊢ 𝐵 = (𝑉 ∖ 𝐴) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐷‘𝑎) = (𝐷‘𝑥) ∧ (𝐷‘𝑎) ≠ (𝐷‘𝑏) ∧ (𝐷‘𝑥) ≠ (𝐷‘𝑦))) | ||
Theorem | frgrwopreglem5 28100* | Lemma 5 for frgrwopreg 28102. If 𝐴 as well as 𝐵 contain at least two vertices, there is a 4-cycle in a friendship 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.) (Proof shortened by AV, 5-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) & ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} & ⊢ 𝐵 = (𝑉 ∖ 𝐴) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ FriendGraph ∧ 1 < (♯‘𝐴) ∧ 1 < (♯‘𝐵)) → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |