:: Axioms of Incidence :: by Wojciech A. Trybulec :: :: Received April 14, 1989 :: Copyright (c) 1990-2016 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, RELAT_1, SUBSET_1, FDIFF_1, TARSKI, CARD_1, ZFMISC_1, INCSP_1; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, DOMAIN_1, RELSET_1, ORDINAL1; constructors RELSET_1, DOMAIN_1, ORDINAL1; registrations XBOOLE_0, SUBSET_1; requirements SUBSET, BOOLE, NUMERALS; begin definition struct IncProjStr (# Points, Lines -> non empty set, Inc -> Relation of the Points, the Lines #); end; definition struct (IncProjStr) IncStruct (# Points, Lines, Planes -> non empty set, Inc -> Relation of the Points,the Lines, Inc2 -> Relation of the Points,the Planes, Inc3 -> Relation of the Lines,the Planes #); end; definition let S be IncProjStr; mode POINT of S is Element of the Points of S; mode LINE of S is Element of the Lines of S; end; definition let S be IncStruct; mode PLANE of S is Element of the Planes of S; end; reserve S for IncStruct; reserve A,B,C,D for POINT of S; reserve L for LINE of S; reserve P for PLANE of S; reserve F,G for Subset of the Points of S; :: Definitions of predicates 'on' and attributes 'linear', 'planar' definition let S be IncProjStr; let A be POINT of S, L be LINE of S; pred A on L means :: INCSP_1:def 1 [A,L] in the Inc of S; end; definition let S; let A be POINT of S, P be PLANE of S; pred A on P means :: INCSP_1:def 2 [A,P] in the Inc2 of S; end; definition let S; let L be LINE of S, P be PLANE of S; pred L on P means :: INCSP_1:def 3 [L,P] in the Inc3 of S; end; definition let S be IncProjStr; let F be Subset of the Points of S, L be LINE of S; pred F on L means :: INCSP_1:def 4 for A being POINT of S st A in F holds A on L; end; definition let S; let F be Subset of the Points of S, P be PLANE of S; pred F on P means :: INCSP_1:def 5 for A st A in F holds A on P; end; definition let S be IncProjStr; let F be Subset of the Points of S; attr F is linear means :: INCSP_1:def 6 ex L being LINE of S st F on L; end; definition let S be IncStruct; let F be Subset of the Points of S; attr F is planar means :: INCSP_1:def 7 ex P be PLANE of S st F on P; end; theorem :: INCSP_1:1 for S being IncProjStr, L being LINE of S, A, B being POINT of S holds {A,B} on L iff A on L & B on L; theorem :: INCSP_1:2 for S being IncProjStr, L being LINE of S, A, B, C being POINT of S holds {A,B,C} on L iff A on L & B on L & C on L; theorem :: INCSP_1:3 {A,B} on P iff A on P & B on P; theorem :: INCSP_1:4 {A,B,C} on P iff A on P & B on P & C on P; theorem :: INCSP_1:5 {A,B,C,D} on P iff A on P & B on P & C on P & D on P; theorem :: INCSP_1:6 G c= F & F on L implies G on L; theorem :: INCSP_1:7 G c= F & F on P implies G on P; theorem :: INCSP_1:8 F on L & A on L iff F \/ {A} on L; theorem :: INCSP_1:9 F on P & A on P iff F \/ {A} on P; theorem :: INCSP_1:10 F \/ G on L iff F on L & G on L; theorem :: INCSP_1:11 F \/ G on P iff F on P & G on P; theorem :: INCSP_1:12 G c= F & F is linear implies G is linear; theorem :: INCSP_1:13 G c= F & F is planar implies G is planar; :: Introduction of mode IncSpace definition let S be IncProjStr; attr S is with_non-trivial_lines means :: INCSP_1:def 8 for L being LINE of S ex A,B being POINT of S st A <> B & {A,B} on L; attr S is linear means :: INCSP_1:def 9 for A,B being POINT of S ex L being LINE of S st {A,B} on L; attr S is up-2-rank means :: INCSP_1:def 10 for A,B being POINT of S, K,L being LINE of S st A <> B & {A,B} on K & {A,B} on L holds K = L; end; definition let S be IncStruct; attr S is with_non-empty_planes means :: INCSP_1:def 11 for P being PLANE of S ex A being POINT of S st A on P; attr S is planar means :: INCSP_1:def 12 for A,B,C being POINT of S ex P being PLANE of S st {A,B,C} on P; attr S is with_<=1_plane_per_3_pts means :: INCSP_1:def 13 for A,B,C being POINT of S, P,Q being PLANE of S st not {A,B,C} is linear & {A,B,C} on P & {A,B,C} on Q holds P = Q; attr S is with_lines_inside_planes means :: INCSP_1:def 14 for L being LINE of S, P being PLANE of S st ex A,B being POINT of S st A <> B & {A,B} on L & {A,B} on P holds L on P; attr S is with_planes_intersecting_in_2_pts means :: INCSP_1:def 15 for A being POINT of S, P,Q being PLANE of S st A on P & A on Q ex B being POINT of S st A <> B & B on P & B on Q; attr S is up-3-dimensional means :: INCSP_1:def 16 ex A,B,C,D being POINT of S st not {A,B,C,D} is planar; attr S is inc-compatible means :: INCSP_1:def 17 for A being POINT of S, L being LINE of S, P being PLANE of S st A on L & L on P holds A on P; end; definition let IT be IncStruct; attr IT is IncSpace-like means :: INCSP_1:def 18 IT is with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible; end; reserve a,b,c for Element of {0,1,2,3}; registration cluster IncSpace-like -> with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible for IncStruct; end; registration cluster strict IncSpace-like for IncStruct; end; definition mode IncSpace is IncSpace-like IncStruct; end; reserve S for IncSpace; reserve A,B,C,D,E for POINT of S; reserve K,L,L1,L2 for LINE of S; reserve P,P1,P2,Q for PLANE of S; reserve F for Subset of the Points of S; :: Axioms of Incidence theorem :: INCSP_1:14 F on L & L on P implies F on P; :: Collinearity of points & coplanarity of points & lines theorem :: INCSP_1:15 {A,A,B} is linear; theorem :: INCSP_1:16 {A,A,B,C} is planar; theorem :: INCSP_1:17 {A,B,C} is linear implies {A,B,C,D} is planar; theorem :: INCSP_1:18 A <> B & {A,B} on L & not C on L implies not {A,B,C} is linear; theorem :: INCSP_1:19 not {A,B,C} is linear & {A,B,C} on P & not D on P implies not {A ,B,C,D} is planar; theorem :: INCSP_1:20 not(ex P st K on P & L on P) implies K <> L; theorem :: INCSP_1:21 not(ex P st L on P & L1 on P & L2 on P) & (ex A st A on L & A on L1 & A on L2) implies L <> L1; theorem :: INCSP_1:22 L1 on P & L2 on P & not L on P & L1 <> L2 implies not(ex Q st L on Q & L1 on Q & L2 on Q); :: Lines & planes theorem :: INCSP_1:23 (ex A st A on K & A on L) implies ex P st K on P & L on P; theorem :: INCSP_1:24 A <> B implies ex L st for K holds {A,B} on K iff K = L; theorem :: INCSP_1:25 not {A,B,C} is linear implies ex P st for Q holds {A,B,C} on Q iff P = Q; theorem :: INCSP_1:26 not A on L implies ex P st for Q holds A on Q & L on Q iff P = Q; theorem :: INCSP_1:27 K <>L & (ex A st A on K & A on L) implies ex P st for Q holds K on Q & L on Q iff P = Q; :: Definitions of functions: Line, Plane definition let S; let A,B; assume A <> B; func Line(A,B) -> LINE of S means :: INCSP_1:def 19 {A,B} on it; end; definition let S; let A,B,C; assume not {A,B,C} is linear; func Plane(A,B,C) -> PLANE of S means :: INCSP_1:def 20 {A,B,C} on it; end; definition let S; let A,L; assume not A on L; func Plane(A,L) -> PLANE of S means :: INCSP_1:def 21 A on it & L on it; end; definition let S; let K,L; assume that K <> L and ex A st A on K & A on L; func Plane(K,L) -> PLANE of S means :: INCSP_1:def 22 K on it & L on it; end; :: Definitional theorems of functions: Line, Plane theorem :: INCSP_1:28 A <> B implies Line(A,B) = Line(B,A); theorem :: INCSP_1:29 not {A,B,C} is linear implies Plane(A,B,C) = Plane(A,C,B); theorem :: INCSP_1:30 not {A,B,C} is linear implies Plane(A,B,C) = Plane(B,A,C); theorem :: INCSP_1:31 not {A,B,C} is linear implies Plane(A,B,C) = Plane(B,C,A); theorem :: INCSP_1:32 not {A,B,C} is linear implies Plane(A,B,C) = Plane(C,A,B); theorem :: INCSP_1:33 not {A,B,C} is linear implies Plane(A,B,C) = Plane(C,B,A); theorem :: INCSP_1:34 K <> L & (ex A st A on K & A on L) implies Plane(K,L) = Plane(L,K); theorem :: INCSP_1:35 A <> B & C on Line(A,B) implies {A,B,C} is linear; theorem :: INCSP_1:36 A <> B & A <> C & {A,B,C} is linear implies Line(A,B) = Line(A,C); theorem :: INCSP_1:37 not {A,B,C} is linear implies Plane(A,B,C) = Plane(C,Line(A,B)); theorem :: INCSP_1:38 not {A,B,C} is linear & D on Plane(A,B,C) implies {A,B,C,D} is planar; theorem :: INCSP_1:39 not C on L & {A,B} on L & A <> B implies Plane(C,L) = Plane(A,B,C); theorem :: INCSP_1:40 not {A,B,C} is linear implies Plane(A,B,C) = Plane(Line(A,B),Line(A,C) ); :: The fourth axiom of incidence theorem :: INCSP_1:41 ex A,B,C st {A,B,C} on P & not {A,B,C} is linear; :: Fundamental existence theorems theorem :: INCSP_1:42 ex A,B,C,D st A on P & not {A,B,C,D} is planar; theorem :: INCSP_1:43 ex B st A <> B & B on L; theorem :: INCSP_1:44 A <> B implies ex C st C on P & not {A,B,C} is linear; theorem :: INCSP_1:45 not {A,B,C} is linear implies ex D st not {A,B,C,D} is planar; theorem :: INCSP_1:46 ex B,C st {B,C} on P & not {A,B,C} is linear; theorem :: INCSP_1:47 A <> B implies ex C,D st not {A,B,C,D} is planar; theorem :: INCSP_1:48 ex B,C,D st not {A,B,C,D} is planar; theorem :: INCSP_1:49 ex L st not A on L & L on P; theorem :: INCSP_1:50 A on P implies ex L,L1,L2 st L1 <> L2 & L1 on P & L2 on P & not L on P & A on L & A on L1 & A on L2; theorem :: INCSP_1:51 ex L,L1,L2 st A on L & A on L1 & A on L2 & not(ex P st L on P & L1 on P & L2 on P); theorem :: INCSP_1:52 ex P st A on P & not L on P; theorem :: INCSP_1:53 ex A st A on P & not A on L; theorem :: INCSP_1:54 ex K st not(ex P st L on P & K on P); theorem :: INCSP_1:55 ex P,Q st P <> Q & L on P & L on Q; :: Intersection of lines and planes theorem :: INCSP_1:56 not L on P & {A,B} on L & {A,B} on P implies A = B; theorem :: INCSP_1:57 P <> Q implies not(ex A st A on P & A on Q) or ex L st for B holds B on P & B on Q iff B on L;