![]() |
Metamath
Proof Explorer Theorem List (p. 288 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eqeefv 28701* | Two points are equal iff they agree in all dimensions. (Contributed by Scott Fenton, 10-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โ (๐ด = ๐ต โ โ๐ โ (1...๐)(๐ดโ๐) = (๐ตโ๐))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eqeelen 28702* | Two points are equal iff the square of the distance between them is zero. (Contributed by Scott Fenton, 10-Jun-2013.) (Revised by Mario Carneiro, 22-May-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โ (๐ด = ๐ต โ ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2) = 0)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | brbtwn2 28703* | Alternate characterization of betweenness, with no existential quantifiers. (Contributed by Scott Fenton, 24-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (๐ด Btwn โจ๐ต, ๐ถโฉ โ (โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โง โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | colinearalglem1 28704 | Lemma for colinearalg 28708. Expand out a multiplication. (Contributed by Scott Fenton, 24-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ท โ โ โง ๐ธ โ โ โง ๐น โ โ)) โ (((๐ต โ ๐ด) ยท (๐น โ ๐ท)) = ((๐ธ โ ๐ท) ยท (๐ถ โ ๐ด)) โ ((๐ต ยท ๐น) โ ((๐ด ยท ๐น) + (๐ต ยท ๐ท))) = ((๐ถ ยท ๐ธ) โ ((๐ด ยท ๐ธ) + (๐ถ ยท ๐ท))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | colinearalglem2 28705* | Lemma for colinearalg 28708. Translate between two forms of the colinearity condition. (Contributed by Scott Fenton, 24-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))) = (((๐ถโ๐) โ (๐ตโ๐)) ยท ((๐ดโ๐) โ (๐ตโ๐))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | colinearalglem3 28706* | Lemma for colinearalg 28708. Translate between two forms of the colinearity condition. (Contributed by Scott Fenton, 24-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โ โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))) = (((๐ดโ๐) โ (๐ถโ๐)) ยท ((๐ตโ๐) โ (๐ถโ๐))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | colinearalglem4 28707* | Lemma for colinearalg 28708. Prove a disjunction that will be needed in the final proof. (Contributed by Scott Fenton, 27-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (((๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง ๐พ โ โ) โ (โ๐ โ (1...๐)((((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) โค 0 โจ โ๐ โ (1...๐)(((๐ถโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐))) ยท ((๐ดโ๐) โ ((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)))) โค 0 โจ โ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐)) ยท (((๐พ ยท ((๐ถโ๐) โ (๐ดโ๐))) + (๐ดโ๐)) โ (๐ถโ๐))) โค 0)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | colinearalg 28708* | An algebraic characterization of colinearity. Note the similarity to brbtwn2 28703. (Contributed by Scott Fenton, 24-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ ((๐ด Btwn โจ๐ต, ๐ถโฉ โจ ๐ต Btwn โจ๐ถ, ๐ดโฉ โจ ๐ถ Btwn โจ๐ด, ๐ตโฉ) โ โ๐ โ (1...๐)โ๐ โ (1...๐)(((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))) = (((๐ตโ๐) โ (๐ดโ๐)) ยท ((๐ถโ๐) โ (๐ดโ๐))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eleesub 28709* | Membership of a subtraction mapping in a Euclidean space. (Contributed by Scott Fenton, 17-Jul-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ถ = (๐ โ (1...๐) โฆ ((๐ดโ๐) โ (๐ตโ๐))) โ โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โ ๐ถ โ (๐ผโ๐)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eleesubd 28710* | Membership of a subtraction mapping in a Euclidean space. Deduction form of eleesub 28709. (Contributed by Scott Fenton, 17-Jul-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (๐ โ ๐ถ = (๐ โ (1...๐) โฆ ((๐ดโ๐) โ (๐ตโ๐)))) โ โข ((๐ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โ ๐ถ โ (๐ผโ๐)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axdimuniq 28711 | The unique dimension axiom. If a point is in ๐ dimensional space and in ๐ dimensional space, then ๐ = ๐. This axiom is not traditionally presented with Tarski's axioms, but we require it here as we are considering spaces in arbitrary dimensions. (Contributed by Scott Fenton, 24-Sep-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐)) โง (๐ โ โ โง ๐ด โ (๐ผโ๐))) โ ๐ = ๐) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axcgrrflx 28712 | ๐ด is as far from ๐ต as ๐ต is from ๐ด. Axiom A1 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โ โจ๐ด, ๐ตโฉCgrโจ๐ต, ๐ดโฉ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axcgrtr 28713 | Congruence is transitive. Axiom A2 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐) โง ๐น โ (๐ผโ๐))) โ ((โจ๐ด, ๐ตโฉCgrโจ๐ถ, ๐ทโฉ โง โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ) โ โจ๐ถ, ๐ทโฉCgrโจ๐ธ, ๐นโฉ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axcgrid 28714 | If there is no distance between ๐ด and ๐ต, then ๐ด = ๐ต. Axiom A3 of [Schwabhauser] p. 10. (Contributed by Scott Fenton, 3-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) โ (โจ๐ด, ๐ตโฉCgrโจ๐ถ, ๐ถโฉ โ ๐ด = ๐ต)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axsegconlem1 28715* | Lemma for axsegcon 28725. Handle the degenerate case. (Contributed by Scott Fenton, 7-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ด = ๐ต โง ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐)))) โ โ๐ฅ โ (๐ผโ๐)โ๐ก โ (0[,]1)(โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ฅโ๐))) โง ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ฅโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axsegconlem2 28716* | Lemma for axsegcon 28725. Show that the square of the distance between two points is a real number. (Contributed by Scott Fenton, 17-Sep-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2) โ โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โ ๐ โ โ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axsegconlem3 28717* | Lemma for axsegcon 28725. Show that the square of the distance between two points is nonnegative. (Contributed by Scott Fenton, 17-Sep-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2) โ โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โ 0 โค ๐) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axsegconlem4 28718* | Lemma for axsegcon 28725. Show that the distance between two points is a real number. (Contributed by Scott Fenton, 17-Sep-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2) โ โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โ (โโ๐) โ โ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axsegconlem5 28719* | Lemma for axsegcon 28725. Show that the distance between two points is nonnegative. (Contributed by Scott Fenton, 17-Sep-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2) โ โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โ 0 โค (โโ๐)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axsegconlem6 28720* | Lemma for axsegcon 28725. Show that the distance between two distinct points is positive. (Contributed by Scott Fenton, 17-Sep-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2) โ โข ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โ 0 < (โโ๐)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axsegconlem7 28721* | Lemma for axsegcon 28725. Show that a particular ratio of distances is in the closed unit interval. (Contributed by Scott Fenton, 18-Sep-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2) & โข ๐ = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2) โ โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ ((โโ๐) / ((โโ๐) + (โโ๐))) โ (0[,]1)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axsegconlem8 28722* | Lemma for axsegcon 28725. Show that a particular mapping generates a point. (Contributed by Scott Fenton, 18-Sep-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2) & โข ๐ = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2) & โข ๐น = (๐ โ (1...๐) โฆ (((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) / (โโ๐))) โ โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ ๐น โ (๐ผโ๐)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axsegconlem9 28723* | Lemma for axsegcon 28725. Show that ๐ต๐น is congruent to ๐ถ๐ท. (Contributed by Scott Fenton, 19-Sep-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2) & โข ๐ = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2) & โข ๐น = (๐ โ (1...๐) โฆ (((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) / (โโ๐))) โ โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐นโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axsegconlem10 28724* | Lemma for axsegcon 28725. Show that the scaling constant from axsegconlem7 28721 produces the betweenness condition for ๐ด, ๐ต and ๐น. (Contributed by Scott Fenton, 21-Sep-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2) & โข ๐ = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2) & โข ๐น = (๐ โ (1...๐) โฆ (((((โโ๐) + (โโ๐)) ยท (๐ตโ๐)) โ ((โโ๐) ยท (๐ดโ๐))) / (โโ๐))) โ โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ((โโ๐) / ((โโ๐) + (โโ๐)))) ยท (๐ดโ๐)) + (((โโ๐) / ((โโ๐) + (โโ๐))) ยท (๐นโ๐)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axsegcon 28725* | Any segment ๐ด๐ต can be extended to a point ๐ฅ such that ๐ต๐ฅ is congruent to ๐ถ๐ท. Axiom A4 of [Schwabhauser] p. 11. (Contributed by Scott Fenton, 4-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ โ๐ฅ โ (๐ผโ๐)(๐ต Btwn โจ๐ด, ๐ฅโฉ โง โจ๐ต, ๐ฅโฉCgrโจ๐ถ, ๐ทโฉ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ax5seglem1 28726* | Lemma for ax5seg 28736. Rexpress a one congruence sum given betweenness. (Contributed by Scott Fenton, 11-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) โ ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2) = ((๐โ2) ยท ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐))โ2))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ax5seglem2 28727* | Lemma for ax5seg 28736. Rexpress another congruence sum given betweenness. (Contributed by Scott Fenton, 11-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) โ ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ถโ๐))โ2) = (((1 โ ๐)โ2) ยท ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐))โ2))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ax5seglem3a 28728 | Lemma for ax5seg 28736. (Contributed by Scott Fenton, 7-May-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐) โง ๐น โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((๐ดโ๐) โ (๐ถโ๐)) โ โ โง ((๐ทโ๐) โ (๐นโ๐)) โ โ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ax5seglem3 28729* | Lemma for ax5seg 28736. Combine congruences for points on a line. (Contributed by Scott Fenton, 11-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐) โง ๐น โ (๐ผโ๐))) โง ((๐ โ (0[,]1) โง ๐ โ (0[,]1)) โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐ธโ๐) = (((1 โ ๐) ยท (๐ทโ๐)) + (๐ ยท (๐นโ๐))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ท, ๐ธโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐ธ, ๐นโฉ)) โ ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ทโ๐) โ (๐นโ๐))โ2)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ax5seglem4 28730* | Lemma for ax5seg 28736. Given two distinct points, the scaling constant in a betweenness statement is nonzero. (Contributed by Scott Fenton, 11-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))) โง ๐ด โ ๐ต) โ ๐ โ 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ax5seglem5 28731* | Lemma for ax5seg 28736. If ๐ต is between ๐ด and ๐ถ, and ๐ด is distinct from ๐ต, then ๐ด is distinct from ๐ถ. (Contributed by Scott Fenton, 11-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) โง (๐ด โ ๐ต โง ๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) โ ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐))โ2) โ 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ax5seglem6 28732* | Lemma for ax5seg 28736. Given two line segments that are divided into pieces, if the pieces are congruent, then the scaling constant is the same. (Contributed by Scott Fenton, 12-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (((๐ โ โ โง ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐) โง ๐น โ (๐ผโ๐)))) โง (๐ด โ ๐ต โง (๐ โ (0[,]1) โง ๐ โ (0[,]1)) โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐ธโ๐) = (((1 โ ๐) ยท (๐ทโ๐)) + (๐ ยท (๐นโ๐))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ท, ๐ธโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐ธ, ๐นโฉ)) โ ๐ = ๐) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ax5seglem7 28733 | Lemma for ax5seg 28736. An algebraic calculation needed further down the line. (Contributed by Scott Fenton, 12-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ด โ โ & โข ๐ โ โ & โข ๐ถ โ โ & โข ๐ท โ โ โ โข (๐ ยท ((๐ถ โ ๐ท)โ2)) = ((((((1 โ ๐) ยท ๐ด) + (๐ ยท ๐ถ)) โ ๐ท)โ2) + ((1 โ ๐) ยท ((๐ ยท ((๐ด โ ๐ถ)โ2)) โ ((๐ด โ ๐ท)โ2)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ax5seglem8 28734 | Lemma for ax5seg 28736. Use the weak deduction theorem to eliminate the hypotheses from ax5seglem7 28733. (Contributed by Scott Fenton, 11-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (((๐ด โ โ โง ๐ โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ ยท ((๐ถ โ ๐ท)โ2)) = ((((((1 โ ๐) ยท ๐ด) + (๐ ยท ๐ถ)) โ ๐ท)โ2) + ((1 โ ๐) ยท ((๐ ยท ((๐ด โ ๐ถ)โ2)) โ ((๐ด โ ๐ท)โ2))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ax5seglem9 28735* | Lemma for ax5seg 28736. Take the calculation in ax5seglem8 28734 and turn it into a series of measurements. (Contributed by Scott Fenton, 12-Jun-2013.) (Revised by Mario Carneiro, 22-May-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (((๐ โ โ โง ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐)))) โง (๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ถโ๐))))) โ (๐ ยท ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) = (ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ทโ๐))โ2) + ((1 โ ๐) ยท ((๐ ยท ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐))โ2)) โ ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ทโ๐))โ2))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ax5seg 28736 | The five segment axiom. Take two triangles ๐ด๐ท๐ถ and ๐ธ๐ป๐บ, a point ๐ต on ๐ด๐ถ, and a point ๐น on ๐ธ๐บ. If all corresponding line segments except for ๐ถ๐ท and ๐บ๐ป are congruent, then so are ๐ถ๐ท and ๐บ๐ป. Axiom A5 of [Schwabhauser] p. 11. (Contributed by Scott Fenton, 12-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ (((๐ด โ ๐ต โง ๐ต Btwn โจ๐ด, ๐ถโฉ โง ๐น Btwn โจ๐ธ, ๐บโฉ) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ)) โ โจ๐ถ, ๐ทโฉCgrโจ๐บ, ๐ปโฉ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axbtwnid 28737 | Points are indivisible. That is, if ๐ด lies between ๐ต and ๐ต, then ๐ด = ๐ต. Axiom A6 of [Schwabhauser] p. 11. (Contributed by Scott Fenton, 3-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โ (๐ด Btwn โจ๐ต, ๐ตโฉ โ ๐ด = ๐ต)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axpaschlem 28738* | Lemma for axpasch 28739. Set up coefficents used in the proof. (Contributed by Scott Fenton, 5-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ โ (0[,]1) โง ๐ โ (0[,]1)) โ โ๐ โ (0[,]1)โ๐ โ (0[,]1)(๐ = ((1 โ ๐) ยท (1 โ ๐)) โง ๐ = ((1 โ ๐) ยท (1 โ ๐)) โง ((1 โ ๐) ยท ๐) = ((1 โ ๐) ยท ๐))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axpasch 28739* | The inner Pasch axiom. Take a triangle ๐ด๐ถ๐ธ, a point ๐ท on ๐ด๐ถ, and a point ๐ต extending ๐ถ๐ธ. Then ๐ด๐ธ and ๐ท๐ต intersect at some point ๐ฅ. Axiom A7 of [Schwabhauser] p. 12. (Contributed by Scott Fenton, 3-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐))) โ ((๐ท Btwn โจ๐ด, ๐ถโฉ โง ๐ธ Btwn โจ๐ต, ๐ถโฉ) โ โ๐ฅ โ (๐ผโ๐)(๐ฅ Btwn โจ๐ท, ๐ตโฉ โง ๐ฅ Btwn โจ๐ธ, ๐ดโฉ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdimlem1 28740 | Lemma for axlowdim 28759. Establish a particular constant function as a function. (Contributed by Scott Fenton, 29-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((3...๐) ร {0}):(3...๐)โถโ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdimlem2 28741 | Lemma for axlowdim 28759. Show that two sets are disjoint. (Contributed by Scott Fenton, 29-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((1...2) โฉ (3...๐)) = โ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdimlem3 28742 | Lemma for axlowdim 28759. Set up a union property for an interval of integers. (Contributed by Scott Fenton, 29-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (๐ โ (โคโฅโ2) โ (1...๐) = ((1...2) โช (3...๐))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdimlem4 28743 | Lemma for axlowdim 28759. Set up a particular constant function. (Contributed by Scott Fenton, 17-Apr-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ด โ โ & โข ๐ต โ โ โ โข {โจ1, ๐ดโฉ, โจ2, ๐ตโฉ}:(1...2)โถโ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdimlem5 28744 | Lemma for axlowdim 28759. Show that a particular union is a point in Euclidean space. (Contributed by Scott Fenton, 29-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ด โ โ & โข ๐ต โ โ โ โข (๐ โ (โคโฅโ2) โ ({โจ1, ๐ดโฉ, โจ2, ๐ตโฉ} โช ((3...๐) ร {0})) โ (๐ผโ๐)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdimlem6 28745 | Lemma for axlowdim 28759. Show that three points are non-colinear. (Contributed by Scott Fenton, 29-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ด = ({โจ1, 0โฉ, โจ2, 0โฉ} โช ((3...๐) ร {0})) & โข ๐ต = ({โจ1, 1โฉ, โจ2, 0โฉ} โช ((3...๐) ร {0})) & โข ๐ถ = ({โจ1, 0โฉ, โจ2, 1โฉ} โช ((3...๐) ร {0})) โ โข (๐ โ (โคโฅโ2) โ ยฌ (๐ด Btwn โจ๐ต, ๐ถโฉ โจ ๐ต Btwn โจ๐ถ, ๐ดโฉ โจ ๐ถ Btwn โจ๐ด, ๐ตโฉ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdimlem7 28746 | Lemma for axlowdim 28759. Set up a point in Euclidean space. (Contributed by Scott Fenton, 29-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = ({โจ3, -1โฉ} โช (((1...๐) โ {3}) ร {0})) โ โข (๐ โ (โคโฅโ3) โ ๐ โ (๐ผโ๐)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdimlem8 28747 | Lemma for axlowdim 28759. Calculate the value of ๐ at three. (Contributed by Scott Fenton, 21-Apr-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = ({โจ3, -1โฉ} โช (((1...๐) โ {3}) ร {0})) โ โข (๐โ3) = -1 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdimlem9 28748 | Lemma for axlowdim 28759. Calculate the value of ๐ away from three. (Contributed by Scott Fenton, 21-Apr-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = ({โจ3, -1โฉ} โช (((1...๐) โ {3}) ร {0})) โ โข ((๐พ โ (1...๐) โง ๐พ โ 3) โ (๐โ๐พ) = 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdimlem10 28749 | Lemma for axlowdim 28759. Set up a family of points in Euclidean space. (Contributed by Scott Fenton, 21-Apr-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = ({โจ(๐ผ + 1), 1โฉ} โช (((1...๐) โ {(๐ผ + 1)}) ร {0})) โ โข ((๐ โ โ โง ๐ผ โ (1...(๐ โ 1))) โ ๐ โ (๐ผโ๐)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdimlem11 28750 | Lemma for axlowdim 28759. Calculate the value of ๐ at its distinguished point. (Contributed by Scott Fenton, 21-Apr-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = ({โจ(๐ผ + 1), 1โฉ} โช (((1...๐) โ {(๐ผ + 1)}) ร {0})) โ โข (๐โ(๐ผ + 1)) = 1 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdimlem12 28751 | Lemma for axlowdim 28759. Calculate the value of ๐ away from its distinguished point. (Contributed by Scott Fenton, 21-Apr-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = ({โจ(๐ผ + 1), 1โฉ} โช (((1...๐) โ {(๐ผ + 1)}) ร {0})) โ โข ((๐พ โ (1...๐) โง ๐พ โ (๐ผ + 1)) โ (๐โ๐พ) = 0) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdimlem13 28752 | Lemma for axlowdim 28759. Establish that ๐ and ๐ are different points. (Contributed by Scott Fenton, 21-Apr-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = ({โจ3, -1โฉ} โช (((1...๐) โ {3}) ร {0})) & โข ๐ = ({โจ(๐ผ + 1), 1โฉ} โช (((1...๐) โ {(๐ผ + 1)}) ร {0})) โ โข ((๐ โ โ โง ๐ผ โ (1...(๐ โ 1))) โ ๐ โ ๐) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdimlem14 28753 | Lemma for axlowdim 28759. Take two possible ๐ from axlowdimlem10 28749. They are the same iff their distinguished values are the same. (Contributed by Scott Fenton, 21-Apr-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = ({โจ(๐ผ + 1), 1โฉ} โช (((1...๐) โ {(๐ผ + 1)}) ร {0})) & โข ๐ = ({โจ(๐ฝ + 1), 1โฉ} โช (((1...๐) โ {(๐ฝ + 1)}) ร {0})) โ โข ((๐ โ โ โง ๐ผ โ (1...(๐ โ 1)) โง ๐ฝ โ (1...(๐ โ 1))) โ (๐ = ๐ โ ๐ผ = ๐ฝ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdimlem15 28754* | Lemma for axlowdim 28759. Set up a one-to-one function of points. (Contributed by Scott Fenton, 21-Apr-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐น = (๐ โ (1...(๐ โ 1)) โฆ if(๐ = 1, ({โจ3, -1โฉ} โช (((1...๐) โ {3}) ร {0})), ({โจ(๐ + 1), 1โฉ} โช (((1...๐) โ {(๐ + 1)}) ร {0})))) โ โข (๐ โ (โคโฅโ3) โ ๐น:(1...(๐ โ 1))โ1-1โ(๐ผโ๐)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdimlem16 28755* | Lemma for axlowdim 28759. Set up a summation that will help establish distance. (Contributed by Scott Fenton, 21-Apr-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = ({โจ3, -1โฉ} โช (((1...๐) โ {3}) ร {0})) & โข ๐ = ({โจ(๐ผ + 1), 1โฉ} โช (((1...๐) โ {(๐ผ + 1)}) ร {0})) โ โข ((๐ โ (โคโฅโ3) โง ๐ผ โ (2...(๐ โ 1))) โ ฮฃ๐ โ (3...๐)((๐โ๐)โ2) = ฮฃ๐ โ (3...๐)((๐โ๐)โ2)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdimlem17 28756 | Lemma for axlowdim 28759. Establish a congruence result. (Contributed by Scott Fenton, 22-Apr-2013.) (Proof shortened by Mario Carneiro, 22-May-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = ({โจ3, -1โฉ} โช (((1...๐) โ {3}) ร {0})) & โข ๐ = ({โจ(๐ผ + 1), 1โฉ} โช (((1...๐) โ {(๐ผ + 1)}) ร {0})) & โข ๐ด = ({โจ1, ๐โฉ, โจ2, ๐โฉ} โช ((3...๐) ร {0})) & โข ๐ โ โ & โข ๐ โ โ โ โข ((๐ โ (โคโฅโ3) โง ๐ผ โ (2...(๐ โ 1))) โ โจ๐, ๐ดโฉCgrโจ๐, ๐ดโฉ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdim1 28757* | The lower dimension axiom for one dimension. In any dimension, there are at least two distinct points. Theorem 3.13 of [Schwabhauser] p. 32, where it is derived from axlowdim2 28758. (Contributed by Scott Fenton, 22-Apr-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (๐ โ โ โ โ๐ฅ โ (๐ผโ๐)โ๐ฆ โ (๐ผโ๐)๐ฅ โ ๐ฆ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdim2 28758* | The lower two-dimensional axiom. In any space where the dimension is greater than one, there are three non-colinear points. Axiom A8 of [Schwabhauser] p. 12. (Contributed by Scott Fenton, 15-Apr-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (๐ โ (โคโฅโ2) โ โ๐ฅ โ (๐ผโ๐)โ๐ฆ โ (๐ผโ๐)โ๐ง โ (๐ผโ๐) ยฌ (๐ฅ Btwn โจ๐ฆ, ๐งโฉ โจ ๐ฆ Btwn โจ๐ง, ๐ฅโฉ โจ ๐ง Btwn โจ๐ฅ, ๐ฆโฉ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axlowdim 28759* | The general lower dimension axiom. Take a dimension ๐ greater than or equal to three. Then, there are three non-colinear points in ๐ dimensional space that are equidistant from ๐ โ 1 distinct points. Derived from remarks in Tarski's System of Geometry, Alfred Tarski and Steven Givant, Bulletin of Symbolic Logic, Volume 5, Number 2 (1999), 175-214. (Contributed by Scott Fenton, 22-Apr-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (๐ โ (โคโฅโ3) โ โ๐โ๐ฅ โ (๐ผโ๐)โ๐ฆ โ (๐ผโ๐)โ๐ง โ (๐ผโ๐)(๐:(1...(๐ โ 1))โ1-1โ(๐ผโ๐) โง โ๐ โ (2...(๐ โ 1))(โจ(๐โ1), ๐ฅโฉCgrโจ(๐โ๐), ๐ฅโฉ โง โจ(๐โ1), ๐ฆโฉCgrโจ(๐โ๐), ๐ฆโฉ โง โจ(๐โ1), ๐งโฉCgrโจ(๐โ๐), ๐งโฉ) โง ยฌ (๐ฅ Btwn โจ๐ฆ, ๐งโฉ โจ ๐ฆ Btwn โจ๐ง, ๐ฅโฉ โจ ๐ง Btwn โจ๐ฅ, ๐ฆโฉ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axeuclidlem 28760* | Lemma for axeuclid 28761. Handle the algebraic aspects of the theorem. (Contributed by Scott Fenton, 9-Sep-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐))) โง (๐ โ (0[,]1) โง ๐ โ (0[,]1) โง ๐ โ 0) โง โ๐ โ (1...๐)(((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐โ๐))) = (((1 โ ๐) ยท (๐ตโ๐)) + (๐ ยท (๐ถโ๐)))) โ โ๐ฅ โ (๐ผโ๐)โ๐ฆ โ (๐ผโ๐)โ๐ โ (0[,]1)โ๐ โ (0[,]1)โ๐ข โ (0[,]1)โ๐ โ (1...๐)((๐ตโ๐) = (((1 โ ๐) ยท (๐ดโ๐)) + (๐ ยท (๐ฅโ๐))) โง (๐ถโ๐) = (((1 โ ๐ ) ยท (๐ดโ๐)) + (๐ ยท (๐ฆโ๐))) โง (๐โ๐) = (((1 โ ๐ข) ยท (๐ฅโ๐)) + (๐ข ยท (๐ฆโ๐))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axeuclid 28761* | Euclid's axiom. Take an angle ๐ต๐ด๐ถ and a point ๐ท between ๐ต and ๐ถ. Now, if you extend the segment ๐ด๐ท to a point ๐, then ๐ lies between two points ๐ฅ and ๐ฆ that lie on the angle. Axiom A10 of [Schwabhauser] p. 13. (Contributed by Scott Fenton, 9-Sep-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ท โ (๐ผโ๐) โง ๐ โ (๐ผโ๐))) โ ((๐ท Btwn โจ๐ด, ๐โฉ โง ๐ท Btwn โจ๐ต, ๐ถโฉ โง ๐ด โ ๐ท) โ โ๐ฅ โ (๐ผโ๐)โ๐ฆ โ (๐ผโ๐)(๐ต Btwn โจ๐ด, ๐ฅโฉ โง ๐ถ Btwn โจ๐ด, ๐ฆโฉ โง ๐ Btwn โจ๐ฅ, ๐ฆโฉ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axcontlem1 28762* | Lemma for axcont 28774. Change bound variables for later use. (Contributed by Scott Fenton, 20-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐น = {โจ๐ฅ, ๐กโฉ โฃ (๐ฅ โ ๐ท โง (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))))} โ โข ๐น = {โจ๐ฆ, ๐ โฉ โฃ (๐ฆ โ ๐ท โง (๐ โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฆโ๐) = (((1 โ ๐ ) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))))} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axcontlem2 28763* | Lemma for axcont 28774. The idea here is to set up a mapping ๐น that will allow to transfer dedekind 11399 to two sets of points. Here, we set up ๐น and show its domain and codomain. (Contributed by Scott Fenton, 17-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ท = {๐ โ (๐ผโ๐) โฃ (๐ Btwn โจ๐, ๐โฉ โจ ๐ Btwn โจ๐, ๐โฉ)} & โข ๐น = {โจ๐ฅ, ๐กโฉ โฃ (๐ฅ โ ๐ท โง (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))))} โ โข (((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โ ๐น:๐ทโ1-1-ontoโ(0[,)+โ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axcontlem3 28764* | Lemma for axcont 28774. Given the separation assumption, ๐ต is a subset of ๐ท. (Contributed by Scott Fenton, 18-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ท = {๐ โ (๐ผโ๐) โฃ (๐ Btwn โจ๐, ๐โฉ โจ ๐ Btwn โจ๐, ๐โฉ)} โ โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง (๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ โ ๐)) โ ๐ต โ ๐ท) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axcontlem4 28765* | Lemma for axcont 28774. Given the separation assumption, ๐ด is a subset of ๐ท. (Contributed by Scott Fenton, 18-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ท = {๐ โ (๐ผโ๐) โฃ (๐ Btwn โจ๐, ๐โฉ โจ ๐ Btwn โจ๐, ๐โฉ)} โ โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ ) โง ๐ โ ๐)) โ ๐ด โ ๐ท) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axcontlem5 28766* | Lemma for axcont 28774. Compute the value of ๐น. (Contributed by Scott Fenton, 18-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ท = {๐ โ (๐ผโ๐) โฃ (๐ Btwn โจ๐, ๐โฉ โจ ๐ Btwn โจ๐, ๐โฉ)} & โข ๐น = {โจ๐ฅ, ๐กโฉ โฃ (๐ฅ โ ๐ท โง (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))))} โ โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง ๐ โ ๐ท) โ ((๐นโ๐) = ๐ โ (๐ โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐โ๐)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axcontlem6 28767* | Lemma for axcont 28774. State the defining properties of the value of ๐น. (Contributed by Scott Fenton, 19-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ท = {๐ โ (๐ผโ๐) โฃ (๐ Btwn โจ๐, ๐โฉ โจ ๐ Btwn โจ๐, ๐โฉ)} & โข ๐น = {โจ๐ฅ, ๐กโฉ โฃ (๐ฅ โ ๐ท โง (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))))} โ โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง ๐ โ ๐ท) โ ((๐นโ๐) โ (0[,)+โ) โง โ๐ โ (1...๐)(๐โ๐) = (((1 โ (๐นโ๐)) ยท (๐โ๐)) + ((๐นโ๐) ยท (๐โ๐))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axcontlem7 28768* | Lemma for axcont 28774. Given two points in ๐ท, one preceeds the other iff its scaling constant is less than the other point's. (Contributed by Scott Fenton, 18-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ท = {๐ โ (๐ผโ๐) โฃ (๐ Btwn โจ๐, ๐โฉ โจ ๐ Btwn โจ๐, ๐โฉ)} & โข ๐น = {โจ๐ฅ, ๐กโฉ โฃ (๐ฅ โ ๐ท โง (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))))} โ โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (๐ โ ๐ท โง ๐ โ ๐ท)) โ (๐ Btwn โจ๐, ๐โฉ โ (๐นโ๐) โค (๐นโ๐))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axcontlem8 28769* | Lemma for axcont 28774. A point in ๐ท is between two others if its function value falls in the middle. (Contributed by Scott Fenton, 18-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ท = {๐ โ (๐ผโ๐) โฃ (๐ Btwn โจ๐, ๐โฉ โจ ๐ Btwn โจ๐, ๐โฉ)} & โข ๐น = {โจ๐ฅ, ๐กโฉ โฃ (๐ฅ โ ๐ท โง (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))))} โ โข ((((๐ โ โ โง ๐ โ (๐ผโ๐) โง ๐ โ (๐ผโ๐)) โง ๐ โ ๐) โง (๐ โ ๐ท โง ๐ โ ๐ท โง ๐ โ ๐ท)) โ (((๐นโ๐) โค (๐นโ๐) โง (๐นโ๐) โค (๐นโ๐ )) โ ๐ Btwn โจ๐, ๐ โฉ)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axcontlem9 28770* | Lemma for axcont 28774. Given the separation assumption, all values of ๐น over ๐ด are less than or equal to all values of ๐น over ๐ต. (Contributed by Scott Fenton, 20-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ท = {๐ โ (๐ผโ๐) โฃ (๐ Btwn โจ๐, ๐โฉ โจ ๐ Btwn โจ๐, ๐โฉ)} & โข ๐น = {โจ๐ฅ, ๐กโฉ โฃ (๐ฅ โ ๐ท โง (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))))} โ โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ ) โง ๐ โ ๐)) โ โ๐ โ (๐น โ ๐ด)โ๐ โ (๐น โ ๐ต)๐ โค ๐) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axcontlem10 28771* | Lemma for axcont 28774. Given a handful of assumptions, derive the conclusion of the final theorem. (Contributed by Scott Fenton, 20-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ท = {๐ โ (๐ผโ๐) โฃ (๐ Btwn โจ๐, ๐โฉ โจ ๐ Btwn โจ๐, ๐โฉ)} & โข ๐น = {โจ๐ฅ, ๐กโฉ โฃ (๐ฅ โ ๐ท โง (๐ก โ (0[,)+โ) โง โ๐ โ (1...๐)(๐ฅโ๐) = (((1 โ ๐ก) ยท (๐โ๐)) + (๐ก ยท (๐โ๐)))))} โ โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ ) โง ๐ โ ๐)) โ โ๐ โ (๐ผโ๐)โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ Btwn โจ๐ฅ, ๐ฆโฉ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axcontlem11 28772* | Lemma for axcont 28774. Eliminate the hypotheses from axcontlem10 28771. (Contributed by Scott Fenton, 20-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ((๐ โ (๐ผโ๐) โง ๐ โ ๐ด โง ๐ต โ โ ) โง ๐ โ ๐)) โ โ๐ โ (๐ผโ๐)โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ Btwn โจ๐ฅ, ๐ฆโฉ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axcontlem12 28773* | Lemma for axcont 28774. Eliminate the trivial cases from the previous lemmas. (Contributed by Scott Fenton, 20-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โง ๐ โ (๐ผโ๐)) โ โ๐ โ (๐ผโ๐)โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ Btwn โจ๐ฅ, ๐ฆโฉ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | axcont 28774* | The axiom of continuity. Take two sets of points ๐ด and ๐ต. If all the points in ๐ด come before the points of ๐ต on a line, then there is a point separating the two. Axiom A11 of [Schwabhauser] p. 13. (Contributed by Scott Fenton, 20-Jun-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง โ๐ โ (๐ผโ๐)โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ฅ Btwn โจ๐, ๐ฆโฉ)) โ โ๐ โ (๐ผโ๐)โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ Btwn โจ๐ฅ, ๐ฆโฉ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | ceeng 28775 | Extends class notation with the Tarski geometry structure for ๐ผโ๐. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class EEG | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-eeng 28776* | Define the geometry structure for ๐ผโ๐. (Contributed by Thierry Arnoux, 24-Aug-2017.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข EEG = (๐ โ โ โฆ ({โจ(Baseโndx), (๐ผโ๐)โฉ, โจ(distโndx), (๐ฅ โ (๐ผโ๐), ๐ฆ โ (๐ผโ๐) โฆ ฮฃ๐ โ (1...๐)(((๐ฅโ๐) โ (๐ฆโ๐))โ2))โฉ} โช {โจ(Itvโndx), (๐ฅ โ (๐ผโ๐), ๐ฆ โ (๐ผโ๐) โฆ {๐ง โ (๐ผโ๐) โฃ ๐ง Btwn โจ๐ฅ, ๐ฆโฉ})โฉ, โจ(LineGโndx), (๐ฅ โ (๐ผโ๐), ๐ฆ โ ((๐ผโ๐) โ {๐ฅ}) โฆ {๐ง โ (๐ผโ๐) โฃ (๐ง Btwn โจ๐ฅ, ๐ฆโฉ โจ ๐ฅ Btwn โจ๐ง, ๐ฆโฉ โจ ๐ฆ Btwn โจ๐ฅ, ๐งโฉ)})โฉ})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eengv 28777* | The value of the Euclidean geometry for dimension ๐. (Contributed by Thierry Arnoux, 15-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (๐ โ โ โ (EEGโ๐) = ({โจ(Baseโndx), (๐ผโ๐)โฉ, โจ(distโndx), (๐ฅ โ (๐ผโ๐), ๐ฆ โ (๐ผโ๐) โฆ ฮฃ๐ โ (1...๐)(((๐ฅโ๐) โ (๐ฆโ๐))โ2))โฉ} โช {โจ(Itvโndx), (๐ฅ โ (๐ผโ๐), ๐ฆ โ (๐ผโ๐) โฆ {๐ง โ (๐ผโ๐) โฃ ๐ง Btwn โจ๐ฅ, ๐ฆโฉ})โฉ, โจ(LineGโndx), (๐ฅ โ (๐ผโ๐), ๐ฆ โ ((๐ผโ๐) โ {๐ฅ}) โฆ {๐ง โ (๐ผโ๐) โฃ (๐ง Btwn โจ๐ฅ, ๐ฆโฉ โจ ๐ฅ Btwn โจ๐ง, ๐ฆโฉ โจ ๐ฆ Btwn โจ๐ฅ, ๐งโฉ)})โฉ})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eengstr 28778 | The Euclidean geometry as a structure. (Contributed by Thierry Arnoux, 15-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (๐ โ โ โ (EEGโ๐) Struct โจ1, ;17โฉ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eengbas 28779 | The Base of the Euclidean geometry. (Contributed by Thierry Arnoux, 15-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (๐ โ โ โ (๐ผโ๐) = (Baseโ(EEGโ๐))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ebtwntg 28780 | The betweenness relation used in the Tarski structure for the Euclidean geometry is the same as Btwn. (Contributed by Thierry Arnoux, 15-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (๐ โ ๐ โ โ) & โข ๐ = (Baseโ(EEGโ๐)) & โข ๐ผ = (Itvโ(EEGโ๐)) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ โ ๐) โ โข (๐ โ (๐ Btwn โจ๐, ๐โฉ โ ๐ โ (๐๐ผ๐))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ecgrtg 28781 | The congruence relation used in the Tarski structure for the Euclidean geometry is the same as Cgr. (Contributed by Thierry Arnoux, 15-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (๐ โ ๐ โ โ) & โข ๐ = (Baseโ(EEGโ๐)) & โข โ = (distโ(EEGโ๐)) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ต โ ๐) & โข (๐ โ ๐ถ โ ๐) & โข (๐ โ ๐ท โ ๐) โ โข (๐ โ (โจ๐ด, ๐ตโฉCgrโจ๐ถ, ๐ทโฉ โ (๐ด โ ๐ต) = (๐ถ โ ๐ท))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | elntg 28782* | The line definition in the Tarski structure for the Euclidean geometry. (Contributed by Thierry Arnoux, 7-Apr-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = (Baseโ(EEGโ๐)) & โข ๐ผ = (Itvโ(EEGโ๐)) โ โข (๐ โ โ โ (LineGโ(EEGโ๐)) = (๐ฅ โ ๐, ๐ฆ โ (๐ โ {๐ฅ}) โฆ {๐ง โ ๐ โฃ (๐ง โ (๐ฅ๐ผ๐ฆ) โจ ๐ฅ โ (๐ง๐ผ๐ฆ) โจ ๐ฆ โ (๐ฅ๐ผ๐ง))})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | elntg2 28783* | The line definition in the Tarski structure for the Euclidean geometry. In contrast to elntg 28782, the betweenness can be strengthened by excluding 1 resp. 0 from the related intervals (because of ๐ฅ โ ๐ฆ). (Contributed by AV, 14-Feb-2023.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข ๐ = (Baseโ(EEGโ๐)) & โข ๐ผ = (1...๐) โ โข (๐ โ โ โ (LineGโ(EEGโ๐)) = (๐ฅ โ ๐, ๐ฆ โ (๐ โ {๐ฅ}) โฆ {๐ โ ๐ โฃ (โ๐ โ (0[,]1)โ๐ โ ๐ผ (๐โ๐) = (((1 โ ๐) ยท (๐ฅโ๐)) + (๐ ยท (๐ฆโ๐))) โจ โ๐ โ (0[,)1)โ๐ โ ๐ผ (๐ฅโ๐) = (((1 โ ๐) ยท (๐โ๐)) + (๐ ยท (๐ฆโ๐))) โจ โ๐ โ (0(,]1)โ๐ โ ๐ผ (๐ฆโ๐) = (((1 โ ๐) ยท (๐ฅโ๐)) + (๐ ยท (๐โ๐))))})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eengtrkg 28784 | The geometry structure for ๐ผโ๐ is a Tarski geometry. (Contributed by Thierry Arnoux, 15-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (๐ โ โ โ (EEGโ๐) โ TarskiG) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eengtrkge 28785 | The geometry structure for ๐ผโ๐ is a Euclidean geometry. (Contributed by Thierry Arnoux, 15-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (๐ โ โ โ (EEGโ๐) โ TarskiGE) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Basic concepts:
Basic kinds of graphs:
Terms and properties of graphs:
Special kinds of graphs:
For the terms "Path", "Walk", "Trail", "Circuit", "Cycle" see the remarks below and the definitions in Section I.1 in [Bollobas] p. 4-5. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
In the following, the vertices and (indexed) edges for an arbitrary class ๐บ (called "graph" in the following) are defined and examined. The main result of this section is to show that the set of vertices (Vtxโ๐บ) of a graph ๐บ is the first component ๐ of the graph ๐บ if it is represented by an ordered pair โจ๐, ๐ธโฉ (see opvtxfv 28804), or the base set (Baseโ๐บ) of the graph ๐บ if it is represented as extensible structure (see basvtxval 28816), and that the set of indexed edges resp. the edge function (iEdgโ๐บ) is the second component ๐ธ of the graph ๐บ if it is represented by an ordered pair โจ๐, ๐ธโฉ (see opiedgfv 28807), or the component (.efโ๐บ) of the graph ๐บ if it is represented as extensible structure (see edgfiedgval 28817). Finally, it is shown that the set of edges of a graph ๐บ is the range of its edge function: (Edgโ๐บ) = ran (iEdgโ๐บ), see edgval 28849. Usually, a graph ๐บ is a set. If ๐บ is a proper class, however, it represents the null graph (without vertices and edges), because (Vtxโ๐บ) = โ and (iEdgโ๐บ) = โ holds, see vtxvalprc 28845 and iedgvalprc 28846. Up to the end of this section, the edges need not be related to the vertices. Once undirected hypergraphs are defined (see df-uhgr 28858), the edges become nonempty sets of vertices, and by this obtain their meaning as "connectors" of vertices. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cedgf 28786 | Extend class notation with an edge function. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class .ef | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-edgf 28787 | Define the edge function (indexed edges) of a graph. (Contributed by AV, 18-Jan-2020.) Use its index-independent form edgfid 28788 instead. (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข .ef = Slot ;18 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgfid 28788 | Utility theorem: index-independent form of df-edgf 28787. (Contributed by AV, 16-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข .ef = Slot (.efโndx) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgfndx 28789 | Index value of the df-edgf 28787 slot. (Contributed by AV, 13-Oct-2024.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (.efโndx) = ;18 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgfndxnn 28790 | The index value of the edge function extractor is a positive integer. This property should be ensured for every concrete coding because otherwise it could not be used in an extensible structure (slots must be positive integers). (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 13-Oct-2024.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (.efโndx) โ โ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgfndxid 28791 | The value of the edge function extractor is the value of the corresponding slot of the structure. (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 28-Oct-2024.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (๐บ โ ๐ โ (.efโ๐บ) = (๐บโ(.efโndx))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgfndxidOLD 28792 | Obsolete version of edgfndxid 28791 as of 28-Oct-2024. The value of the edge function extractor is the value of the corresponding slot of the structure. (Contributed by AV, 21-Sep-2020.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (๐บ โ ๐ โ (.efโ๐บ) = (๐บโ(.efโndx))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | basendxltedgfndx 28793 | The index value of the Base slot is less than the index value of the .ef slot. (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 30-Oct-2024.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (Baseโndx) < (.efโndx) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | baseltedgfOLD 28794 | Obsolete proof of basendxltedgfndx 28793 as of 30-Oct-2024. The index value of the Base slot is less than the index value of the .ef slot. (Contributed by AV, 21-Sep-2020.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (Baseโndx) < (.efโndx) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | basendxnedgfndx 28795 | The slots Base and .ef are different. (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (Baseโndx) โ (.efโndx) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
The key concepts in graph theory are vertices and edges. In general, a graph "consists" (at least) of two sets: the set of vertices and the set of edges. The edges "connect" vertices. The meaning of "connect" is different for different kinds of graphs (directed/undirected graphs, hyper-/pseudo-/ multi-/simple graphs, etc.). The simplest way to represent a graph (of any kind) is to define a graph as "an ordered pair of disjoint sets (V, E)" (see section I.1 in [Bollobas] p. 1), or in the notation of Metamath: โจ๐, ๐ธโฉ. Another way is to regard a graph as a mathematical structure, which consistes at least of a set (of vertices) and a relation between the vertices (edge function), but which can be enhanced by additional features (see Wikipedia "Mathematical structure", 24-Sep-2020, https://en.wikipedia.org/wiki/Mathematical_structure): "In mathematics, a structure is a set endowed with some additional features on the set (e.g., operation, relation, metric, topology). Often, the additional features are attached or related to the set, so as to provide it with some additional meaning or significance.". Such structures are provided as "extensible structures" in Metamath, see df-struct 17107. To allow for expressing and proving most of the theorems for graphs independently from their representation, the functions Vtx and iEdg are defined (see df-vtx 28798 and df-iedg 28799), which provide the vertices resp. (indexed) edges of an arbitrary class ๐บ which represents a graph: (Vtxโ๐บ) resp. (iEdgโ๐บ). In literature, these functions are often denoted also by "V" and "E", see section I.1 in [Bollobas] p. 1 ("If G is a graph, then V = V(G) is the vertex set of G, and E = E(G) is the edge set.") or section 1.1 in [Diestel] p. 2 ("The vertex set of graph G is referred to as V(G), its edge set as E(G)."). Instead of providing edges themselves, iEdg is intended to provide a function as mapping of "indices" (the domain of the function) to the edges (therefore called "set of indexed edges"), which allows for hyper-/pseudo-/multigraphs with more than one edge between two (or more) vertices. For example, e1 = e(1) = { a, b } and e2 = e(2) = { a, b } are two different edges connecting the same two vertices a and b (in a pseudograph). In section 1.10 of [Diestel] p. 28, the edge function is defined differently: as "map E -> V u. [V]^2 assigning to every edge either one or two vertices, its end.". Here, the domain is the set of abstract edges: for two different edges e1 and e2 connecting the same two vertices a and b, we would have e(e1) = e(e2) = { a, b }. Since the set of abstract edges can be chosen as index set, these definitions are equivalent. The result of these functions are as expected: for a graph represented as ordered pair (๐บ โ (V ร V)), the set of vertices is (Vtxโ๐บ) = (1st โ๐บ) (see opvtxval 28803) and the set of (indexed) edges is (iEdgโ๐บ) = (2nd โ๐บ) (see opiedgval 28806), or if ๐บ is given as ordered pair ๐บ = โจ๐, ๐ธโฉ, the set of vertices is (Vtxโ๐บ) = ๐ (see opvtxfv 28804) and the set of (indexed) edges is (iEdgโ๐บ) = ๐ธ (see opiedgfv 28807). And for a graph represented as extensible structure (๐บ Struct โจ(Baseโndx), (.efโndx)โฉ), the set of vertices is (Vtxโ๐บ) = (Baseโ๐บ) (see funvtxval 28818) and the set of (indexed) edges is (iEdgโ๐บ) = (.efโ๐บ) (see funiedgval 28819), or if ๐บ is given in its simplest form as extensible structure with two slots (๐บ = {โจ(Baseโndx), ๐โฉ, โจ(.efโndx), ๐ธโฉ}), the set of vertices is (Vtxโ๐บ) = ๐ (see struct2grvtx 28827) and the set of (indexed) edges is (iEdgโ๐บ) = ๐ธ (see struct2griedg 28828). These two representations are convertible, see graop 28829 and grastruct 28830: If ๐บ is a graph (for example ๐บ = โจ๐, ๐ธโฉ), then ๐ป = {โจ(Baseโndx), (Vtxโ๐บ)โฉ, โจ(.efโndx), (iEdgโ๐บ)โฉ} represents essentially the same graph, and if ๐บ is a graph (for example ๐บ = {โจ(Baseโndx), ๐โฉ, โจ(.efโndx), ๐ธโฉ}), then ๐ป = โจ(Vtxโ๐บ), (iEdgโ๐บ)โฉ represents essentially the same graph. In both cases, (Vtxโ๐บ) = (Vtxโ๐ป) and (iEdgโ๐บ) = (iEdgโ๐ป) hold. Theorems gropd 28831 and gropeld 28833 show that if any representation of a graph with vertices ๐ and edges ๐ธ has a certain property, then the ordered pair โจ๐, ๐ธโฉ of the set of vertices and the set of edges (which is such a representation of a graph with vertices ๐ and edges ๐ธ) has this property. Analogously, theorems grstructd 28832 and grstructeld 28834 show that if any representation of a graph with vertices ๐ and edges ๐ธ has a certain property, then any extensible structure with base set ๐ and value ๐ธ in the slot for edge functions (which is also such a representation of a graph with vertices ๐ and edges ๐ธ) has this property. Besides the usual way to represent graphs without edges (consisting of unconnected vertices only), which would be ๐บ = โจ๐, โ โฉ or ๐บ = {โจ(Baseโndx), ๐โฉ, โจ(.efโndx), โ โฉ}, a structure without a slot for edges can be used: ๐บ = {โจ(Baseโndx), ๐โฉ}, see snstrvtxval 28837 and snstriedgval 28838. Analogously, the empty set โ can be used to represent the null graph, see vtxval0 28839 and iedgval0 28840, which can also be represented by ๐บ = โจโ , โ โฉ or ๐บ = {โจ(Baseโndx), โ โฉ, โจ(.efโndx), โ โฉ}. Even proper classes can be used to represent the null graph, see vtxvalprc 28845 and iedgvalprc 28846. Other classes should not be used to represent graphs, because there could be a degenerate behavior of the vertex set and (indexed) edge functions, see vtxvalsnop 28841 resp. iedgvalsnop 28842, and vtxval3sn 28843 resp. iedgval3sn 28844. Avoid directly depending on this detail so that theorems will not depend on the Kuratowski construction of ordered pairs, see also the comment for df-op 4631. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cvtx 28796 | Extend class notation with the vertices of "graphs". | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class Vtx | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | ciedg 28797 | Extend class notation with the indexed edges of "graphs". | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class iEdg | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-vtx 28798 | Define the function mapping a graph to the set of its vertices. This definition is very general: It defines the set of vertices for any ordered pair as its first component, and for any other class as its "base set". It is meaningful, however, only if the ordered pair represents a graph resp. the class is an extensible structure representing a graph. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 20-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข Vtx = (๐ โ V โฆ if(๐ โ (V ร V), (1st โ๐), (Baseโ๐))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-iedg 28799 | Define the function mapping a graph to its indexed edges. This definition is very general: It defines the indexed edges for any ordered pair as its second component, and for any other class as its "edge function". It is meaningful, however, only if the ordered pair represents a graph resp. the class is an extensible structure (containing a slot for "edge functions") representing a graph. (Contributed by AV, 20-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข iEdg = (๐ โ V โฆ if(๐ โ (V ร V), (2nd โ๐), (.efโ๐))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | vtxval 28800 | The set of vertices of a graph. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
โข (Vtxโ๐บ) = if(๐บ โ (V ร V), (1st โ๐บ), (Baseโ๐บ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |