![]() |
Metamath
Proof Explorer Theorem List (p. 281 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eupthp1 28001 | Append one path segment to an Eulerian path 〈𝐹, 𝑃〉 to become an Eulerian path 〈𝐻, 𝑄〉 of the supergraph 𝑆 obtained by adding the new edge to the graph 𝐺. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 7-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) (Revised by AV, 8-Apr-2024.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) & ⊢ 𝑁 = (♯‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉}) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) & ⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) & ⊢ (Vtx‘𝑆) = 𝑉 & ⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶}) ⇒ ⊢ (𝜑 → 𝐻(EulerPaths‘𝑆)𝑄) | ||
Theorem | eupth2eucrct 28002 | Append one path segment to an Eulerian path 〈𝐹, 𝑃〉 which may not be an (Eulerian) circuit to become an Eulerian circuit 〈𝐻, 𝑄〉 of the supergraph 𝑆 obtained by adding the new edge to the graph 𝐺. (Contributed by AV, 11-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) (Revised by AV, 8-Apr-2024.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) & ⊢ 𝑁 = (♯‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉}) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) & ⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) & ⊢ (Vtx‘𝑆) = 𝑉 & ⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶}) & ⊢ (𝜑 → 𝐶 = (𝑃‘0)) ⇒ ⊢ (𝜑 → (𝐻(EulerPaths‘𝑆)𝑄 ∧ 𝐻(Circuits‘𝑆)𝑄)) | ||
Theorem | eupth2lem1 28003 | Lemma for eupth2 28024. (Contributed by Mario Carneiro, 8-Apr-2015.) |
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}) ↔ (𝐴 ≠ 𝐵 ∧ (𝑈 = 𝐴 ∨ 𝑈 = 𝐵)))) | ||
Theorem | eupth2lem2 28004 | Lemma for eupth2 28024. (Contributed by Mario Carneiro, 8-Apr-2015.) |
⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈) → (¬ 𝑈 ∈ if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}) ↔ 𝑈 ∈ if(𝐴 = 𝐶, ∅, {𝐴, 𝐶}))) | ||
Theorem | trlsegvdeglem1 28005 | Lemma for trlsegvdeg 28012. (Contributed by AV, 20-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) ⇒ ⊢ (𝜑 → ((𝑃‘𝑁) ∈ 𝑉 ∧ (𝑃‘(𝑁 + 1)) ∈ 𝑉)) | ||
Theorem | trlsegvdeglem2 28006 | Lemma for trlsegvdeg 28012. (Contributed by AV, 20-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → Fun (iEdg‘𝑋)) | ||
Theorem | trlsegvdeglem3 28007 | Lemma for trlsegvdeg 28012. (Contributed by AV, 20-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → Fun (iEdg‘𝑌)) | ||
Theorem | trlsegvdeglem4 28008 | Lemma for trlsegvdeg 28012. (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 28009 | Lemma for trlsegvdeg 28012. (Contributed by AV, 21-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → dom (iEdg‘𝑌) = {(𝐹‘𝑁)}) | ||
Theorem | trlsegvdeglem6 28010 | Lemma for trlsegvdeg 28012. (Contributed by AV, 21-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → dom (iEdg‘𝑋) ∈ Fin) | ||
Theorem | trlsegvdeglem7 28011 | Lemma for trlsegvdeg 28012. (Contributed by AV, 21-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → dom (iEdg‘𝑌) ∈ Fin) | ||
Theorem | trlsegvdeg 28012 | Formerly part of proof of eupth2lem3 28021: 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 28013 | Lemma for eupth2lem3 28021. (Contributed by AV, 21-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℕ0) | ||
Theorem | eupth2lem3lem2 28014 | Lemma for eupth2lem3 28021. (Contributed by AV, 21-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝑌)‘𝑈) ∈ ℕ0) | ||
Theorem | eupth2lem3lem3 28015* | Lemma for eupth2lem3 28021, formerly part of proof of eupth2lem3 28021: 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 28016* | Lemma for eupth2lem3 28021, formerly part of proof of eupth2lem3 28021: 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 28017* | Lemma for eupth2 28024. (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 28018* | Formerly part of proof of eupth2lem3 28021: 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 28019* | Lemma for eupth2lem3 28021: Combining trlsegvdeg 28012, eupth2lem3lem3 28015, eupth2lem3lem4 28016 and eupth2lem3lem6 28018. (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 28020 | Formerly part of proof of eupth2 28024: 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 28021* | Lemma for eupth2 28024. (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 28022* | Lemma for eupth2 28024 (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 28024. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ UPGraph) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘〈𝑉, (𝐼 ↾ (𝐹 “ (0..^0)))〉)‘𝑥)} = ∅) | ||
Theorem | eupth2lems 28023* | Lemma for eupth2 28024 (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 28024. (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 28024* | 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 28025* | 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 28026* | 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 28027* | 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 28028* | 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 28029 | 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 28030 (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 28030* | 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 28036. konigsberg 28042 shows that the Königsberg graph has no Eulerian path, thus the Königsberg Bridge problem has no solution. | ||
Theorem | konigsbergvtx 28031 | 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 28032 | 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 28033* | 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 28034* | 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 28035* | 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 28036 | 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 28037 | Lemma 1 for konigsberg 28042: 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 28038 | Lemma 2 for konigsberg 28042: 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 28039 | Lemma 3 for konigsberg 28042: 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 28040* | Lemma 4 for konigsberg 28042: 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 28041* | Lemma 5 for konigsberg 28042: 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 28042 | 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 28026 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 28043 | Extend class notation with friendship graphs. |
class FriendGraph | ||
Definition | df-frgr 28044* | 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 28045* | 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 28046 | 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 28047 | 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 28048 | 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 28049 | Any null graph (without vertices) represented as hypergraph is a friendship graph. (Contributed by AV, 29-Mar-2021.) |
⊢ ((𝐺 ∈ UHGraph ∧ (Vtx‘𝐺) = ∅) → 𝐺 ∈ FriendGraph ) | ||
Theorem | frgr0 28050 | The null graph (graph without vertices) is a friendship graph. (Contributed by AV, 29-Mar-2021.) |
⊢ ∅ ∈ FriendGraph | ||
Theorem | frcond1 28051* | 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 28052* | 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 28053* | Variant of frcond2 28052: 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 28054* | 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 28055* | 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 28056 | 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 28057 | 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 28058* | Lemma 1 for frgr3v 28060. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ∀𝑥∀𝑦(((𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸) ∧ (𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ 𝐸)) → 𝑥 = 𝑦)) | ||
Theorem | frgr3vlem2 28059* | Lemma 2 for frgr3v 28060. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸)))) | ||
Theorem | frgr3v 28060 | 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 28061* | 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 28062* | Lemma for 3vfriswmgr 28063. (Contributed by Alexander van der Vekens, 6-Oct-2017.) (Revised by AV, 31-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ({𝐴, 𝐵} ∈ 𝐸 → ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ 𝐸)) | ||
Theorem | 3vfriswmgr 28063* | 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 28064* | 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 28065* | 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 28066* | 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 28067* | 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 28068* | 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 28069* | 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 28070* | 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 28071* | 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 28072* | 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 28073* | 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 28074 | 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 28075* | 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 28076 | 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 28077 | 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 28078 | 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 28079 | 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 28080 | 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 28081 | 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 28082* | 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 28083 | 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 28184 is proven by formalizing Huneke's proof, see [Huneke] pp. 1-2. The three claims (see frgrncvvdeq 28094, frgrregorufr 28110 and frrusgrord0 28125) 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 28084 | Lemma 1 for frgrncvvdeq 28094. (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 28085* | Lemma 2 for frgrncvvdeq 28094. 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 28086* | Lemma 3 for frgrncvvdeq 28094. 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 28087* | Lemma 4 for frgrncvvdeq 28094. 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 28088* | Lemma 5 for frgrncvvdeq 28094. 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 28089* | Lemma 6 for frgrncvvdeq 28094. (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 28090* | Lemma 7 for frgrncvvdeq 28094. 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 28091* | Lemma 8 for frgrncvvdeq 28094. 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 28092* | Lemma 9 for frgrncvvdeq 28094. 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 28093* | Lemma 10 for frgrncvvdeq 28094. (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 28094* | 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 28095 | In a friendship graph any two vertices with different degrees are connected. Alternate version of frgrwopreglem4 28100 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 28096 | 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 28106 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 28097* | Lemma 1 for frgrwopreg 28108: 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 28098* | Lemma 2 for frgrwopreg 28108. 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 28099* | Lemma 3 for frgrwopreg 28108. 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 28100* | Lemma 4 for frgrwopreg 28108. 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 → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑎, 𝑏} ∈ 𝐸) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |