:: Axioms of Incidence
:: by Wojciech A. Trybulec
::
:: Received April 14, 1989
:: Copyright (c) 1990-2026 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;
definitions TARSKI;
expansions TARSKI;
theorems ENUMSET1, TARSKI, XBOOLE_0, XBOOLE_1, XTUPLE_0;
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
[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
[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
[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
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
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
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
ex P be PLANE of S st F on P;
end;
theorem Th1:
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
proof
let S be IncProjStr, L be LINE of S, A, B be POINT of S;
thus {A,B} on L implies A on L & B on L
proof
A1: A in {A,B} & B in {A,B} by TARSKI:def 2;
assume {A,B} on L;
hence thesis by A1;
end;
assume
A2: A on L & B on L;
let C be POINT of S;
assume C in {A,B};
hence thesis by A2,TARSKI:def 2;
end;
theorem Th2:
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
proof
let S be IncProjStr, L be LINE of S, A, B, C be POINT of S;
thus {A,B,C} on L implies A on L & B on L & C on L
proof
A1: C in {A,B,C} by ENUMSET1:def 1;
A2: A in {A,B,C} & B in {A,B,C} by ENUMSET1:def 1;
assume {A,B,C} on L;
hence thesis by A2,A1;
end;
assume
A3: A on L & B on L & C on L;
let D be POINT of S;
assume D in {A,B,C};
hence thesis by A3,ENUMSET1:def 1;
end;
theorem Th3:
{A,B} on P iff A on P & B on P
proof
thus {A,B} on P implies A on P & B on P
proof
A1: A in {A,B} & B in {A,B} by TARSKI:def 2;
assume {A,B} on P;
hence thesis by A1;
end;
assume
A2: A on P & B on P;
let C be POINT of S;
assume C in {A,B};
hence thesis by A2,TARSKI:def 2;
end;
theorem Th4:
{A,B,C} on P iff A on P & B on P & C on P
proof
thus {A,B,C} on P implies A on P & B on P & C on P
proof
A1: C in {A,B,C} by ENUMSET1:def 1;
A2: A in {A,B,C} & B in {A,B,C} by ENUMSET1:def 1;
assume {A,B,C} on P;
hence thesis by A2,A1;
end;
assume
A3: A on P & B on P & C on P;
let D be POINT of S;
assume D in {A,B,C};
hence thesis by A3,ENUMSET1:def 1;
end;
theorem Th5:
{A,B,C,D} on P iff A on P & B on P & C on P & D on P
proof
thus {A,B,C,D} on P implies A on P & B on P & C on P & D on P
proof
A1: C in {A,B,C,D} & D in {A,B,C,D} by ENUMSET1:def 2;
A2: A in {A,B,C,D} & B in {A,B,C,D} by ENUMSET1:def 2;
assume {A,B,C,D} on P;
hence thesis by A2,A1;
end;
assume
A3: A on P & B on P & C on P & D on P;
let E be POINT of S;
assume E in {A,B,C,D};
hence thesis by A3,ENUMSET1:def 2;
end;
theorem Th6:
G c= F & F on L implies G on L;
theorem Th7:
G c= F & F on P implies G on P;
theorem Th8:
F on L & A on L iff F \/ {A} on L
proof
thus F on L & A on L implies F \/ {A} on L
proof
assume
A1: F on L & A on L;
let C be POINT of S;
assume C in F \/ {A};
then C in F or C in {A} by XBOOLE_0:def 3;
hence thesis by A1,TARSKI:def 1;
end;
assume
A2: F \/ {A} on L;
hence F on L by Th6,XBOOLE_1:7;
{A} c= F \/ {A} by XBOOLE_1:7;
then {A,A} c= F \/ {A} by ENUMSET1:29;
then {A,A} on L by A2;
hence thesis by Th1;
end;
theorem Th9:
F on P & A on P iff F \/ {A} on P
proof
thus F on P & A on P implies F \/ {A} on P
proof
assume
A1: F on P & A on P;
let C be POINT of S;
assume C in F \/ {A};
then C in F or C in {A} by XBOOLE_0:def 3;
hence thesis by A1,TARSKI:def 1;
end;
assume
A2: F \/ {A} on P;
hence F on P by Th7,XBOOLE_1:7;
{A} c= F \/ {A} by XBOOLE_1:7;
then {A,A} c= F \/ {A} by ENUMSET1:29;
then {A,A} on P by A2;
hence thesis by Th3;
end;
theorem Th10:
F \/ G on L iff F on L & G on L
proof
thus F \/ G on L implies F on L & G on L by Th6,XBOOLE_1:7;
assume
A1: F on L & G on L;
let C be POINT of S;
assume C in F \/ G;
then C in F or C in G by XBOOLE_0:def 3;
hence thesis by A1;
end;
theorem Th11:
F \/ G on P iff F on P & G on P
proof
thus F \/ G on P implies F on P & G on P by Th7,XBOOLE_1:7;
assume
A1: F on P & G on P;
let C be POINT of S;
assume C in F \/ G;
then C in F or C in G by XBOOLE_0:def 3;
hence thesis by A1;
end;
theorem
G c= F & F is linear implies G is linear
proof
assume that
A1: G c= F and
A2: F is linear;
consider L such that
A3: F on L by A2;
take L;
let A be POINT of S;
assume A in G;
hence thesis by A1,A3;
end;
theorem
G c= F & F is planar implies G is planar
proof
assume that
A1: G c= F and
A2: F is planar;
consider P such that
A3: F on P by A2;
take P;
let A be POINT of S;
assume A in G;
hence thesis by A1,A3;
end;
:: Introduction of mode IncSpace
definition
let S be IncProjStr;
attr S is with_non-trivial_lines means
:Def8:
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
:Def9:
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
:Def10:
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
:Def11:
for P being PLANE of S ex A being POINT of S st A on P;
attr S is planar means
:Def12:
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
:Def13:
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
:Def14:
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
:Def15:
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
:Def16:
ex A,B,C,D being POINT of S st not {A,B,C,D} is planar;
attr S is inc-compatible means
:Def17:
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
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;
coherence;
end;
registration
cluster strict IncSpace-like for IncStruct;
existence
proof
reconsider Zero1 = 0, One = 1, Two = 2, Three = 3 as Element of {0,1,2,3}
by ENUMSET1:def 2;
{Zero1,One} in {{a,b} where a is Element of {0,1,2,3}, b is Element of
{0,1,2,3} : a <> b };
then reconsider
Li = {{a,b} where a is Element of {0,1,2,3}, b is Element of {0
,1,2,3} : a <> b } as non empty set;
{Zero1,One,Two} in {{a,b,c} where a is Element of {0,1,2,3}, b is
Element of {0,1,2,3}, c is Element of {0,1,2,3} : a <> b & a <> c & b <> c };
then reconsider
Pl = {{a,b,c} where a is Element of {0,1,2,3}, b is Element of
{0,1,2,3}, c is Element of {0,1,2,3} : a <> b & a <> c & b <> c } as non empty
set;
{[a,l] where l is Element of Li : a in l} c= [:{0,1,2,3},Li:]
proof
let x be object;
assume x in {[a,l] where l is Element of Li: a in l};
then
ex a be Element of {0,1,2,3},l be Element of Li st x = [a,l] & a in l;
hence thesis;
end;
then reconsider
i1 = {[a,l] where l is Element of Li: a in l} as Relation of {0
,1,2,3},Li;
{[a,p] where p is Element of Pl : a in p} c= [:{0,1,2,3},Pl:]
proof
let x be object;
assume x in {[a,p] where p is Element of Pl: a in p};
then ex a st ex p be Element of Pl st x =[a,p] & a in p;
hence thesis;
end;
then reconsider
i2 = {[a,p] where p is Element of Pl : a in p} as Relation of {
0,1,2,3},Pl;
{[l,p] where l is Element of Li, p is Element of Pl: l c= p} c= [:Li, Pl:]
proof
let x be object;
assume x in {[l,p] where l is Element of Li, p is Element of Pl: l c= p};
then ex l be Element of Li, p be Element of Pl st x =[l,p] & l c= p;
hence thesis;
end;
then reconsider
i3 = {[l,p] where l is Element of Li, p is Element of Pl: l c=
p} as Relation of Li,Pl;
now
set S = IncStruct (# {0,1,2,3},Li,Pl,i1,i2,i3 #);
thus S is with_non-trivial_lines
proof
let L be LINE of S;
reconsider l = L as Element of Li;
l in Li;
then consider a,b such that
A1: l = {a,b} and
A2: a <> b;
reconsider A = a, B = b as POINT of S;
take A,B;
thus A <> B by A2;
b in l by A1,TARSKI:def 2;
then [b,l] in i1;
then
A3: B on L;
a in l by A1,TARSKI:def 2;
then [a,l] in i1;
then A on L;
hence thesis by A3,Th1;
end;
thus
A4: S is linear
proof
let A,B be POINT of S;
reconsider a = A,b = B as Element of {0,1,2,3};
A5: now
for a ex c st a <> c
proof
let a;
A6: now
assume a = 1 or a = 2 or a = 3;
then a <> Zero1;
hence thesis;
end;
now
assume a = 0;
then a <> One;
hence thesis;
end;
hence thesis by A6,ENUMSET1:def 2;
end;
then consider c being Element of {0,1,2,3} such that
A7: a <> c;
{a,c} in Li by A7;
then consider l be Element of Li such that
A8: l = {a,c};
reconsider L = l as LINE of S;
a in l by A8,TARSKI:def 2;
then [a,l] in i1;
then
A9: A on L;
assume a = b;
then {A,B} on L by A9,Th1;
hence thesis;
end;
now
assume a <> b;
then {a,b} in Li;
then consider l be Element of Li such that
A10: l = {a,b};
reconsider L = l as LINE of S;
b in l by A10,TARSKI:def 2;
then [b,l] in i1;
then
A11: B on L;
a in l by A10,TARSKI:def 2;
then [a,l] in i1;
then A on L;
then {A,B} on L by A11,Th1;
hence thesis;
end;
hence thesis by A5;
end;
A12: for l being Element of Li holds [a,l] in i1 implies a in l
proof
let l be Element of Li;
assume [a,l] in i1;
then consider b be Element of {0,1,2,3}, k be Element of Li such that
A13: [a,l] = [b,k] and
A14: b in k;
a = b by A13,XTUPLE_0:1;
hence thesis by A13,A14,XTUPLE_0:1;
end;
thus S is up-2-rank
proof
let A,B be POINT of S, K,L be LINE of S;
assume that
A15: A <> B and
A16: {A,B} on K and
A17: {A,B} on L;
reconsider a = A, b = B as Element of {0,1,2,3};
reconsider k = K,l = L as Element of Li;
k in Li;
then consider x1,x2 being Element of {0,1,2,3} such that
A18: k = {x1,x2} and
x1 <> x2;
B on K by A16,Th1;
then [b,k] in i1;
then b in k by A12;
then
A19: b = x1 or b = x2 by A18,TARSKI:def 2;
l in Li;
then consider x3,x4 being Element of {0,1,2,3} such that
A20: l = {x3,x4} and
x3 <> x4;
A on L by A17,Th1;
then [a,l] in i1;
then a in l by A12;
then
A21: a = x3 or a = x4 by A20,TARSKI:def 2;
B on L by A17,Th1;
then [b,l] in i1;
then
A22: b in l by A12;
A on K by A16,Th1;
then [a,k] in i1;
then a in k by A12;
then a = x1 or a = x2 by A18,TARSKI:def 2;
hence thesis by A15,A22,A18,A19,A20,A21,TARSKI:def 2;
end;
thus S is with_non-empty_planes
proof
let P be PLANE of S;
reconsider p = P as Element of Pl;
p in Pl;
then consider a,b,c such that
A23: p = {a,b,c} and
a <> b and
a <> c and
b <> c;
reconsider A = a as POINT of S;
take A;
a in p by A23,ENUMSET1:def 1;
then [a,p] in i2;
hence thesis;
end;
thus S is planar
proof
let A,B,C be POINT of S;
reconsider a = A, b = B, c = C as Element of {0,1,2,3};
A24: now
for a ex b,c st a <> b & a <> c & b <> c
proof
let a;
A25: now
assume a = 2 or a = 3;
then a <> Zero1 & a <> One;
hence thesis;
end;
now
assume a = 0 or a = 1;
then a <> Two & a <> Three;
hence thesis;
end;
hence thesis by A25,ENUMSET1:def 2;
end;
then consider x,y being Element of {0,1,2,3} such that
A26: a <> x & a <> y & x <> y;
{a,x,y} in Pl by A26;
then consider p be Element of Pl such that
A27: p = {a,x,y};
reconsider P = p as PLANE of S;
assume that
A28: a = b & a = c and
b = c;
a in p by A27,ENUMSET1:def 1;
then [a,p] in i2;
then A on P;
then {A,B,C} on P by A28,Th4;
hence thesis;
end;
A29: now
assume
A30: a = b & a <> c or a = c & a <> b or b = c & a <> b;
then consider x,y being Element of {0,1,2,3} such that
A31: ( x = a or x = b or x = c)&( y = a or y = b or y = c) and
A32: x <> y;
for a,b ex c st a <> c & b <> c
proof
let a,b;
A33: now
assume that
A34: a = 0 and
A35: b = 3;
a <> One by A34;
hence thesis by A35;
end;
A36: now
assume that
A37: a = 1 or a = 2 or a = 3 and
A38: b = 1 or b = 2 or b = 3;
a <> Zero1 by A37;
hence thesis by A38;
end;
A39: now
assume that
A40: a=3 and
A41: b = 0;
a <> Two by A40;
hence thesis by A41;
end;
A42: now
assume that
A43: a = 1 or a = 2 and
A44: b = 0;
a <> Three by A43;
hence thesis by A44;
end;
now
assume that
A45: a = 0 and
A46: b = 0 or b = 1 or b = 2;
a <> Three by A45;
hence thesis by A46;
end;
hence thesis by A33,A36,A42,A39,ENUMSET1:def 2;
end;
then consider z being Element of {0,1,2,3} such that
A47: x <> z & y <> z;
{x,y,z} in Pl by A32,A47;
then consider p be Element of Pl such that
A48: p = {x,y,z};
reconsider P = p as PLANE of S;
b in p by A30,A31,A32,A48,ENUMSET1:def 1;
then [b,p] in i2;
then
A49: B on P;
c in p by A30,A31,A32,A48,ENUMSET1:def 1;
then [c,p] in i2;
then
A50: C on P;
a in p by A30,A31,A32,A48,ENUMSET1:def 1;
then [a,p] in i2;
then A on P;
then {A,B,C} on P by A49,A50,Th4;
hence thesis;
end;
now
assume a <> b & a <> c & b <> c;
then {a,b,c} in Pl;
then consider p be Element of Pl such that
A51: p = {a,b,c};
reconsider P = p as PLANE of S;
b in p by A51,ENUMSET1:def 1;
then [b,p] in i2;
then
A52: B on P;
c in p by A51,ENUMSET1:def 1;
then [c,p] in i2;
then
A53: C on P;
a in p by A51,ENUMSET1:def 1;
then [a,p] in i2;
then A on P;
then {A,B,C} on P by A52,A53,Th4;
hence thesis;
end;
hence thesis by A24,A29;
end;
A54: for p being Element of Pl holds [a,p] in i2 implies a in p
proof
let p be Element of Pl;
assume [a,p] in i2;
then consider b be Element of {0,1,2,3}, q be Element of Pl such that
A55: [a,p] = [b,q] and
A56: b in q;
a = b by A55,XTUPLE_0:1;
hence thesis by A55,A56,XTUPLE_0:1;
end;
thus S is with_<=1_plane_per_3_pts
proof
let A,B,C be POINT of S, P,Q be PLANE of S;
assume that
A57: not {A,B,C} is linear and
A58: {A,B,C} on P and
A59: {A,B,C} on Q;
reconsider a = A, b = B, c = C as Element of {0,1,2,3};
reconsider p = P,q = Q as Element of Pl;
p in Pl;
then consider x1,x2,x3 being Element of {0,1,2,3} such that
A60: p = {x1,x2,x3} and
x1 <> x2 and
x1 <> x3 and
x2 <> x3;
A on P by A58,Th4;
then [a,p] in i2;
then a in p by A54;
then
A61: a = x1 or a = x2 or a = x3 by A60,ENUMSET1:def 1;
C on P by A58,Th4;
then [c,p] in i2;
then c in p by A54;
then
A62: c = x1 or c = x2 or c = x3 by A60,ENUMSET1:def 1;
B on P by A58,Th4;
then [b,p] in i2;
then b in p by A54;
then
A63: b = x1 or b = x2 or b = x3 by A60,ENUMSET1:def 1;
q in Pl;
then consider x1,x2,x3 being Element of {0,1,2,3} such that
A64: q = {x1,x2,x3} and
x1 <> x2 and
x1 <> x3 and
x2 <> x3;
B on Q by A59,Th4;
then [b,q] in i2;
then b in q by A54;
then
A65: b = x1 or b = x2 or b = x3 by A64,ENUMSET1:def 1;
A66: now
consider L being LINE of S such that
A67: {A,C} on L by A4;
A68: A on L & C on L by A67,Th1;
consider K being LINE of S such that
A69: {A,B} on K by A4;
A70: ( not {A,B,C} on K)& not {A,B,C} on L by A57;
assume
A71: A = B or A = C or B = C;
A on K & B on K by A69,Th1;
hence contradiction by A71,A68,A70,Th2;
end;
C on Q by A59,Th4;
then [c,q] in i2;
then c in q by A54;
then
A72: c = x1 or c = x2 or c = x3 by A64,ENUMSET1:def 1;
A on Q by A59,Th4;
then [a,q] in i2;
then a in q by A54;
then a = x1 or a = x2 or a = x3 by A64,ENUMSET1:def 1;
hence thesis by A66,A60,A61,A63,A62,A64,A65,A72,ENUMSET1:57,58,59,60;
end;
thus S is with_lines_inside_planes
proof
let L be LINE of S, P be PLANE of S;
given A,B being POINT of S such that
A73: A <> B and
A74: {A,B} on L and
A75: {A,B} on P;
reconsider a = A, b = B as Element of {0,1,2,3};
reconsider p = P as Element of Pl;
A on P by A75,Th3;
then [a,p] in i2;
then
A76: a in p by A54;
reconsider l = L as Element of Li;
B on L by A74,Th1;
then [b,l] in i1;
then
A77: b in l by A12;
B on P by A75,Th3;
then [b,p] in i2;
then
A78: b in p by A54;
A on L by A74,Th1;
then [a,l] in i1;
then
A79: a in l by A12;
now
let x be object;
assume
A80: x in l;
l in Li;
then consider x1,x2 being Element of {0,1,2,3} such that
A81: l = {x1,x2} and
x1 <> x2;
A82: b = x1 or b = x2 by A77,A81,TARSKI:def 2;
a = x1 or a = x2 by A79,A81,TARSKI:def 2;
hence x in p by A73,A76,A78,A80,A81,A82,TARSKI:def 2;
end;
then l c= p;
then [l,p] in i3;
hence thesis;
end;
thus S is with_planes_intersecting_in_2_pts
proof
let A be POINT of S, P,Q be PLANE of S;
assume that
A83: A on P and
A84: A on Q;
reconsider p = P,q = Q as Element of Pl;
reconsider a = A as Element of {0,1,2,3};
p in Pl;
then consider x1,x2,x3 being Element of {0,1,2,3} such that
A85: p = {x1,x2,x3} and
A86: x1 <> x2 & x1 <> x3 & x2 <> x3;
A87: x1 in p & x2 in p by A85,ENUMSET1:def 1;
A88: x3 in p by A85,ENUMSET1:def 1;
q in Pl;
then consider y1,y2,y3 being Element of {0,1,2,3} such that
A89: q = {y1,y2,y3} and
A90: y1 <> y2 & y1 <> y3 & y2 <> y3;
A91: y1 in q & y2 in q by A89,ENUMSET1:def 1;
A92: y3 in q by A89,ENUMSET1:def 1;
[a,q] in i2 by A84;
then a in q by A54;
then a = y1 or a = y2 or a = y3 by A89,ENUMSET1:def 1;
then consider z3,z4 being Element of {0,1,2,3} such that
A93: z3 in q & z4 in q and
A94: z3 <> a and
A95: z4 <> a & z3 <> z4 by A90,A91,A92;
[a,p] in i2 by A83;
then a in p by A54;
then a = x1 or a = x2 or a = x3 by A85,ENUMSET1:def 1;
then consider z1,z2 being Element of {0,1,2,3} such that
A96: z1 in p & z2 in p and
A97: z1 <> a and
A98: z2 <> a and
A99: z1 <> z2 by A86,A87,A88;
now
assume
A100: z1 <> z3 & z1 <> z4 & z2 <> z3 & z2 <> z4;
per cases by ENUMSET1:def 2;
suppose
A101: a = 0;
then
A102: z3 = 1 or z3 = 2 or z3 = 3 by A94,ENUMSET1:def 2;
A103: z2 = 1 or z2 = 2 or z2 = 3 by A98,A101,ENUMSET1:def 2;
z1 = 1 or z1 = 2 or z1 = 3 by A97,A101,ENUMSET1:def 2;
hence contradiction by A99,A95,A100,A101,A103,A102,ENUMSET1:def 2;
end;
suppose
A104: a = 1;
then
A105: z3 = 0 or z3 = 2 or z3 = 3 by A94,ENUMSET1:def 2;
A106: z2 = 0 or z2 = 2 or z2 = 3 by A98,A104,ENUMSET1:def 2;
z1 = 0 or z1 = 2 or z1 = 3 by A97,A104,ENUMSET1:def 2;
hence contradiction by A99,A95,A100,A104,A106,A105,ENUMSET1:def 2;
end;
suppose
A107: a = 2;
then
A108: z3 = 0 or z3 = 1 or z3 = 3 by A94,ENUMSET1:def 2;
A109: z2 = 0 or z2 = 1 or z2 = 3 by A98,A107,ENUMSET1:def 2;
z1 = 0 or z1 = 1 or z1 = 3 by A97,A107,ENUMSET1:def 2;
hence contradiction by A99,A95,A100,A107,A109,A108,ENUMSET1:def 2;
end;
suppose
A110: a = 3;
then
A111: z3 = 0 or z3 = 1 or z3 = 2 by A94,ENUMSET1:def 2;
A112: z2 = 0 or z2 = 1 or z2 = 2 by A98,A110,ENUMSET1:def 2;
z1 = 0 or z1 = 1 or z1 = 2 by A97,A110,ENUMSET1:def 2;
hence contradiction by A99,A95,A100,A110,A112,A111,ENUMSET1:def 2;
end;
end;
then consider z being Element of {0,1,2,3} such that
A113: z in p & z in q and
A114: a <> z by A96,A97,A98,A93;
reconsider B = z as POINT of S;
take B;
thus A <> B by A114;
[z,p] in i2 & [z,q] in i2 by A113;
hence thesis;
end;
thus S is up-3-dimensional
proof
reconsider Three = 3 as Element of {0,1,2,3} by ENUMSET1:def 2;
reconsider A = Zero1, B = One, C = Two, D = Three as POINT of S;
take A,B,C,D;
assume {A,B,C,D} is planar;
then consider P being PLANE of S such that
A115: {A,B,C,D} on P;
reconsider p = P as Element of Pl;
p in Pl;
then consider a,b,c such that
A116: p = {a,b,c} and
a <> b and
a <> c and
b <> c;
D on P by A115;
then [Three,p] in i2;
then
A117: Three in p by A54;
C on P by A115;
then [Two,p] in i2;
then Two in p by A54;
then
A118: Two = a or Two = b or Two = c by A116,ENUMSET1:def 1;
B on P by A115;
then [One,p] in i2;
then One in p by A54;
then
A119: One = a or One = b or One = c by A116,ENUMSET1:def 1;
A on P by A115;
then [Zero1,p] in i2;
then Zero1 in p by A54;
then Zero1 = a or Zero1 = b or Zero1 = c by A116,ENUMSET1:def 1;
hence contradiction by A116,A117,A119,A118,ENUMSET1:def 1;
end;
A120: for p being Element of Pl, l be Element of Li holds [l,p] in i3
implies l c= p
proof
let p be Element of Pl, l be Element of Li;
assume [l,p] in i3;
then consider k be Element of Li, q be Element of Pl such that
A121: [l,p] = [k,q] and
A122: k c= q;
l = k by A121,XTUPLE_0:1;
hence thesis by A121,A122,XTUPLE_0:1;
end;
thus S is inc-compatible
proof
let A be POINT of S, L be LINE of S, P be PLANE of S;
reconsider a = A as Element of {0,1,2,3};
reconsider l = L as Element of Li;
reconsider p = P as Element of Pl;
assume that
A123: A on L and
A124: L on P;
[l,p] in i3 by A124;
then
A125: l c= p by A120;
[a,l] in i1 by A123;
then a in l by A12;
then [a,p] in i2 by A125;
hence thesis;
end;
end;
then IncStruct (# {0,1,2,3},Li,Pl,i1,i2,i3 #) is IncSpace-like;
hence thesis;
end;
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 Th14:
F on L & L on P implies F on P
by Def17;
:: Collinearity of points & coplanarity of points & lines
theorem Th15:
{A,A,B} is linear
proof
consider K such that
A1: {A,B} on K by Def9;
take K;
thus thesis by A1,ENUMSET1:30;
end;
theorem Th16:
{A,A,B,C} is planar
proof
consider P such that
A1: {A,B,C} on P by Def12;
take P;
thus thesis by A1,ENUMSET1:31;
end;
theorem Th17:
{A,B,C} is linear implies {A,B,C,D} is planar
proof
given L such that
A1: {A,B,C} on L;
{A,B} \/ {C} on L by A1,ENUMSET1:3;
then
A2: {A,B} on L by Th8;
consider P such that
A3: {A,B,D} on P by Def12;
{A,B} \/ {D} on P by A3,ENUMSET1:3;
then
A4: {A,B} on P by Th11;
assume
A5: not {A,B,C,D} is planar;
then A <> B by Th16;
then L on P by A2,A4,Def14;
then
A6: {A,B,C} on P by A1,Th14;
then
A7: C on P by Th4;
A8: D on P by A3,Th4;
A on P & B on P by A6,Th4;
then {A,B,C,D} on P by A7,A8,Th5;
hence contradiction by A5;
end;
theorem Th18:
A <> B & {A,B} on L & not C on L implies not {A,B,C} is linear
proof
assume that
A1: A <> B & {A,B} on L and
A2: not C on L;
given K such that
A3: {A,B,C} on K;
{A,B} \/ {C} on K by A3,ENUMSET1:3;
then {A,B} on K by Th10;
then L = K by A1,Def10;
hence contradiction by A2,A3,Th2;
end;
theorem Th19:
not {A,B,C} is linear & {A,B,C} on P & not D on P implies not {A
,B,C,D} is planar
proof
assume that
A1: ( not {A,B,C} is linear)& {A,B,C} on P and
A2: not D on P;
given Q such that
A3: {A,B,C,D} on Q;
{A,B,C} \/ {D} on Q by A3,ENUMSET1:6;
then {A,B,C} on Q by Th9;
then P = Q by A1,Def13;
hence contradiction by A2,A3,Th5;
end;
theorem
not(ex P st K on P & L on P) implies K <> L
proof
assume that
A1: not(ex P st K on P & L on P) and
A2: K = L;
consider A,B such that
A3: A <> B and
A4: {A,B} on K by Def8;
A5: A on K & B on K by A4,Th1;
consider C,D such that
A6: C <> D and
A7: {C,D} on L by Def8;
C on K by A2,A7,Th1;
then {A,B,C} on K by A5,Th2;
then {A,B,C} is linear;
then {A,B,C,D} is planar by Th17;
then consider Q such that
A8: {A,B,C,D} on Q;
C on Q & D on Q by A8,Th5;
then {C,D} on Q by Th3;
then
A9: L on Q by A6,A7,Def14;
A on Q & B on Q by A8,Th5;
then {A,B} on Q by Th3;
then K on Q by A3,A4,Def14;
hence contradiction by A1,A9;
end;
Lm1: ex B st A <> B & B on L
proof
consider B,C such that
A1: B <> C and
A2: {B,C} on L by Def8;
A3: A <> C or A <> B by A1;
B on L & C on L by A2,Th1;
hence thesis by A3;
end;
theorem
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
proof
assume
A1: not(ex P st L on P & L1 on P & L2 on P);
given A such that
A2: A on L and
A3: A on L1 and
A4: A on L2;
consider C such that
A5: A <> C and
A6: C on L1 by Lm1;
consider D such that
A7: A <> D and
A8: D on L2 by Lm1;
consider B such that
A9: A <> B and
A10: B on L by Lm1;
assume
A11: L = L1;
then {A,C,B} on L1 by A3,A10,A6,Th2;
then {A,C} \/ {B} on L1 by ENUMSET1:3;
then
A12: {A,C} on L1 by Th10;
{A,B,C} on L by A3,A11,A10,A6,Th2;
then {A,B,C} is linear;
then {A,B,C,D} is planar by Th17;
then consider Q such that
A13: {A,B,C,D} on Q;
A on Q & D on Q by A13,Th5;
then
A14: {A,D} on Q by Th3;
{A,D} on L2 by A4,A8,Th1;
then
A15: L2 on Q by A7,A14,Def14;
A on Q & C on Q by A13,Th5;
then {A,C} on Q by Th3;
then
A16: L1 on Q by A5,A12,Def14;
{A,B} \/ {C,D} on Q by A13,ENUMSET1:5;
then
A17: {A,B} on Q by Th11;
{A,B} on L by A2,A10,Th1;
then L on Q by A9,A17,Def14;
hence contradiction by A1,A16,A15;
end;
theorem
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)
proof
assume that
A1: L1 on P and
A2: L2 on P and
A3: not L on P and
A4: L1 <> L2;
consider A,B such that
A5: A <> B and
A6: {A,B} on L1 by Def8;
A7: {A,B} on P by A1,A6,Th14;
consider C,C1 being POINT of S such that
A8: C <> C1 and
A9: {C,C1} on L2 by Def8;
A10: now
assume C on L1 & C1 on L1;
then {C,C1} on L1 by Th1;
hence contradiction by A4,A8,A9,Def10;
end;
A11: {C,C1} on P by A2,A9,Th14;
then C on P by Th3;
then {A,B} \/ {C} on P by A7,Th9;
then
A12: {A,B,C} on P by ENUMSET1:3;
C1 on P by A11,Th3;
then {A,B} \/ {C1} on P by A7,Th9;
then
A13: {A,B,C1} on P by ENUMSET1:3;
consider D,E such that
A14: D <> E and
A15: {D,E} on L by Def8;
given Q such that
A16: L on Q and
A17: L1 on Q and
A18: L2 on Q;
A19: {A,B} on Q by A17,A6,Th14;
A20: {C,C1} on Q by A18,A9,Th14;
then
A21: C on Q by Th3;
A22: {D,E} on Q by A16,A15,Th14;
then
A23: D on Q by Th3;
then {C,D} on Q by A21,Th3;
then {A,B} \/ {C,D} on Q by A19,Th11;
then {A,B,C,D} on Q by ENUMSET1:5;
then
A24: {A,B,C,D} is planar;
A25: E on Q by A22,Th3;
then {C,E} on Q by A21,Th3;
then {A,B} \/ {C,E} on Q by A19,Th11;
then {A,B,C,E} on Q by ENUMSET1:5;
then
A26: {A,B,C,E} is planar;
A27: C1 on Q by A20,Th3;
then {C1,D} on Q by A23,Th3;
then {A,B} \/ {C1,D} on Q by A19,Th11;
then {A,B,C1,D} on Q by ENUMSET1:5;
then
A28: {A,B,C1,D} is planar;
{C1,E} on Q by A27,A25,Th3;
then {A,B} \/ {C1,E} on Q by A19,Th11;
then {A,B,C1,E} on Q by ENUMSET1:5;
then
A29: {A,B,C1,E} is planar;
not {D,E} on P by A3,A14,A15,Def14;
then not D on P or not E on P by Th3;
hence contradiction by A5,A6,A24,A26,A28,A29,A10,A12,A13,Th18,Th19;
end;
:: Lines & planes
theorem Th23:
(ex A st A on K & A on L) implies ex P st K on P & L on P
proof
given A such that
A1: A on K and
A2: A on L;
consider C such that
A3: A <> C and
A4: C on L by Lm1;
A5: {A,C} on L by A2,A4,Th1;
consider B such that
A6: A <> B and
A7: B on K by Lm1;
consider P such that
A8: {A,B,C} on P by Def12;
take P;
A9: A on P by A8,Th4;
C on P by A8,Th4;
then
A10: {A,C} on P by A9,Th3;
B on P by A8,Th4;
then
A11: {A,B} on P by A9,Th3;
{A,B} on K by A1,A7,Th1;
hence thesis by A6,A3,A5,A11,A10,Def14;
end;
theorem
A <> B implies ex L st for K holds {A,B} on K iff K = L
proof
assume
A1: A <> B;
consider L such that
A2: {A,B} on L by Def9;
take L;
thus thesis by A1,A2,Def10;
end;
theorem
not {A,B,C} is linear implies ex P st for Q holds {A,B,C} on Q iff P = Q
proof
assume
A1: not {A,B,C} is linear;
consider P such that
A2: {A,B,C} on P by Def12;
take P;
thus thesis by A1,A2,Def13;
end;
theorem Th26:
not A on L implies ex P st for Q holds A on Q & L on Q iff P = Q
proof
assume
A1: not A on L;
consider B,C such that
A2: B <> C and
A3: {B,C} on L by Def8;
consider P such that
A4: {B,C,A} on P by Def12;
take P;
let Q;
thus A on Q & L on Q implies P = Q
proof
assume that
A5: A on Q and
A6: L on Q;
{B,C} on Q by A3,A6,Th14;
then B on Q & C on Q by Th3;
then
A7: {B,C,A} on Q by A5,Th4;
not {B,C,A} is linear by A1,A2,A3,Th18;
hence thesis by A4,A7,Def13;
end;
A8: {B,C} \/ {A} on P by A4,ENUMSET1:3;
thus thesis by A2,A3,A8,Def14,Th9;
end;
theorem Th27:
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
proof
assume that
A1: K <> L and
A2: ex A st A on K & A on L;
consider A such that
A3: A on K and
A4: A on L by A2;
consider C such that
A5: A <> C and
A6: C on L by Lm1;
consider B such that
A7: A <> B and
A8: B on K by Lm1;
consider P such that
A9: {A,B,C} on P by Def12;
A10: A on P by A9,Th4;
take P;
let Q;
thus K on Q & L on Q implies P = Q
proof
{A,C} on L by A4,A6,Th1;
then not {A,C} on K by A1,A5,Def10;
then
A11: not C on K by A3,Th1;
assume that
A12: K on Q and
A13: L on Q;
A14: C on Q by A6,A13,Def17;
A on Q & B on Q by A3,A8,A12,Def17;
then
A15: {A,B,C} on Q by A14,Th4;
{A,B} on K by A3,A8,Th1;
then not {A,B,C} is linear by A7,A11,Th18;
hence thesis by A9,A15,Def13;
end;
B on P by A9,Th4;
then
A16: {A,B} on P by A10,Th3;
C on P by A9,Th4;
then
A17: {A,C} on P by A10,Th3;
A18: {A,C} on L by A4,A6,Th1;
{A,B} on K by A3,A8,Th1;
hence thesis by A7,A5,A18,A16,A17,Def14;
end;
:: Definitions of functions: Line, Plane
definition
let S;
let A,B;
assume
A1: A <> B;
func Line(A,B) -> LINE of S means
:Def19:
{A,B} on it;
correctness by A1,Def9,Def10;
end;
definition
let S;
let A,B,C;
assume
A1: not {A,B,C} is linear;
func Plane(A,B,C) -> PLANE of S means
:Def20:
{A,B,C} on it;
correctness by A1,Def12,Def13;
end;
definition
let S;
let A,L;
assume
A1: not A on L;
func Plane(A,L) -> PLANE of S means
:Def21:
A on it & L on it;
existence
proof
consider B,C such that
A2: B <> C & {B,C} on L by Def8;
consider P such that
A3: {B,C,A} on P by Def12;
take P;
thus A on P by A3,Th4;
{B,C} \/ {A} on P by A3,ENUMSET1:3;
then {B,C} on P by Th9;
hence thesis by A2,Def14;
end;
uniqueness
proof
let P,Q;
assume that
A4: A on P & L on P and
A5: A on Q & L on Q;
consider P1 such that
A6: for P2 holds A on P2 & L on P2 iff P1 = P2 by A1,Th26;
P1 = P by A4,A6;
hence thesis by A5,A6;
end;
end;
definition
let S;
let K,L;
assume that
A1: K <> L and
A2: ex A st A on K & A on L;
func Plane(K,L) -> PLANE of S means
:Def22:
K on it & L on it;
existence by A2,Th23;
uniqueness
proof
let P,Q;
assume that
A3: K on P & L on P and
A4: K on Q & L on Q;
consider P1 such that
A5: for P2 holds K on P2 & L on P2 iff P1 = P2 by A1,A2,Th27;
P = P1 by A3,A5;
hence thesis by A4,A5;
end;
end;
:: Definitional theorems of functions: Line, Plane
theorem
A <> B implies Line(A,B) = Line(B,A)
proof
assume
A1: A <> B;
then {A,B} on Line(A,B) by Def19;
hence thesis by A1,Def19;
end;
theorem Th29:
not {A,B,C} is linear implies Plane(A,B,C) = Plane(A,C,B)
proof
assume
A1: not {A,B,C} is linear;
then not {A,C,B} is linear by ENUMSET1:57;
then {A,C,B} on Plane(A,C,B) by Def20;
then {A,B,C} on Plane(A,C,B) by ENUMSET1:57;
hence thesis by A1,Def20;
end;
theorem Th30:
not {A,B,C} is linear implies Plane(A,B,C) = Plane(B,A,C)
proof
assume
A1: not {A,B,C} is linear;
then not {B,A,C} is linear by ENUMSET1:58;
then {B,A,C} on Plane(B,A,C) by Def20;
then {A,B,C} on Plane(B,A,C) by ENUMSET1:58;
hence thesis by A1,Def20;
end;
theorem
not {A,B,C} is linear implies Plane(A,B,C) = Plane(B,C,A)
proof
assume
A1: not {A,B,C} is linear;
then
A2: not {B,C,A} is linear by ENUMSET1:59;
thus Plane(A,B,C) = Plane(B,A,C) by A1,Th30
.= Plane(B,C,A) by A2,Th29;
end;
theorem Th32:
not {A,B,C} is linear implies Plane(A,B,C) = Plane(C,A,B)
proof
assume
A1: not {A,B,C} is linear;
then
A2: not {C,A,B} is linear by ENUMSET1:59;
thus Plane(A,B,C) = Plane(A,C,B) by A1,Th29
.= Plane(C,A,B) by A2,Th30;
end;
theorem
not {A,B,C} is linear implies Plane(A,B,C) = Plane(C,B,A)
proof
assume
A1: not {A,B,C} is linear;
then
A2: not {C,B,A} is linear by ENUMSET1:60;
thus Plane(A,B,C) = Plane(C,A,B) by A1,Th32
.= Plane(C,B,A) by A2,Th29;
end;
theorem
K <> L & (ex A st A on K & A on L) implies Plane(K,L) = Plane(L,K)
proof
assume
A1: K <> L;
set P2 = Plane(L,K);
set P1 = Plane(K,L);
given A such that
A2: A on K and
A3: A on L;
consider C such that
A4: A <> C and
A5: C on L by Lm1;
consider B such that
A6: A <> B and
A7: B on K by Lm1;
A8: K on P2 by A1,A2,A3,Def22;
then
A9: B on P2 by A7,Def17;
A10: K on P1 by A1,A2,A3,Def22;
then
A11: B on P1 by A7,Def17;
A12: now
assume {A,B,C} is linear;
then consider L1 such that
A13: {A,B,C} on L1;
A14: A on L1 by A13,Th2;
C on L1 by A13,Th2;
then
A15: {A,C} on L1 by A14,Th1;
A16: {A,B} on K by A2,A7,Th1;
B on L1 by A13,Th2;
then {A,B} on L1 by A14,Th1;
then
A17: K = L1 by A6,A16,Def10;
{A,C} on L by A3,A5,Th1;
hence contradiction by A1,A4,A15,A17,Def10;
end;
L on P2 by A1,A2,A3,Def22;
then
A18: C on P2 by A5,Def17;
A on P2 by A2,A8,Def17;
then
A19: {A,B,C} on P2 by A9,A18,Th4;
L on P1 by A1,A2,A3,Def22;
then
A20: C on P1 by A5,Def17;
A on P1 by A2,A10,Def17;
then {A,B,C} on P1 by A11,A20,Th4;
hence thesis by A19,A12,Def13;
end;
theorem Th35:
A <> B & C on Line(A,B) implies {A,B,C} is linear
proof
assume A <> B;
then {A,B} on Line(A,B) by Def19;
then
A1: A on Line(A,B) & B on Line(A,B) by Th1;
assume C on Line(A,B);
then {A,B,C} on Line(A,B) by A1,Th2;
hence thesis;
end;
theorem
A <> B & A <> C & {A,B,C} is linear implies Line(A,B) = Line(A,C)
proof
assume
A1: A <> B;
then
A2: {A,B} on Line(A,B) by Def19;
then
A3: A on Line(A,B) by Th1;
assume
A4: A <> C;
assume {A,B,C} is linear;
then C on Line(A,B) by A1,A2,Th18;
then {A,C} on Line(A,B) by A3,Th1;
hence thesis by A4,Def19;
end;
theorem
not {A,B,C} is linear implies Plane(A,B,C) = Plane(C,Line(A,B))
proof
assume
A1: not {A,B,C} is linear;
then A <> B by Th15;
then
A2: {A,B} on Line(A,B) by Def19;
then A on Line(A,B) & B on Line(A,B) by Th1;
then
A3: C on Line(A,B) implies {A,B,C} on Line(A,B) by Th2;
then Line(A,B) on Plane(C,Line(A,B)) by A1,Def21;
then
A4: {A,B} on Plane(C,Line(A,B)) by A2,Th14;
C on Plane(C,Line(A,B)) by A1,A3,Def21;
then {A,B} \/ {C} on Plane(C,Line(A,B)) by A4,Th9;
then {A,B,C} on Plane(C,Line(A,B)) by ENUMSET1:3;
hence thesis by A1,Def20;
end;
theorem
not {A,B,C} is linear & D on Plane(A,B,C) implies {A,B,C,D} is planar
proof
assume that
A1: not {A,B,C} is linear and
A2: D on Plane(A,B,C);
{A,B,C} on Plane(A,B,C) by A1,Def20;
then {A,B,C} \/ {D} on Plane(A,B,C) by A2,Th9;
then {A,B,C,D} on Plane(A,B,C) by ENUMSET1:6;
hence thesis;
end;
theorem
not C on L & {A,B} on L & A <> B implies Plane(C,L) = Plane(A,B,C)
proof
assume that
A1: not C on L and
A2: {A,B} on L and
A3: A <> B;
set P1 = Plane(C,L);
L on P1 by A1,Def21;
then
A4: {A,B} on P1 by A2,Th14;
C on P1 by A1,Def21;
then {A,B} \/ {C} on P1 by A4,Th9;
then
A5: {A,B,C} on P1 by ENUMSET1:3;
not {A,B,C} is linear by A1,A2,A3,Th18;
hence thesis by A5,Def20;
end;
theorem
not {A,B,C} is linear implies Plane(A,B,C) = Plane(Line(A,B),Line(A,C) )
proof
set P2 = Plane(Line(A,B),Line(A,C));
set L1 = Line(A,B);
set L2 = Line(A,C);
assume
A1: not {A,B,C} is linear;
then
A2: A <> B by Th15;
then
A3: {A,B} on L1 by Def19;
then
A4: A on L1 by Th1;
not {A,C,B} is linear by A1,ENUMSET1:57;
then
A5: A <> C by Th15;
then
A6: {A,C} on L2 by Def19;
then
A7: A on L2 by Th1;
{A,C} on L2 by A5,Def19;
then C on L2 by Th1;
then
A8: L1 <> L2 by A1,A2,Th35;
then L2 on P2 by A4,A7,Def22;
then {A,C} on P2 by A6,Th14;
then
A9: C on P2 by Th3;
L1 on P2 by A4,A7,A8,Def22;
then {A,B} on P2 by A3,Th14;
then {A,B} \/ {C} on P2 by A9,Th9;
then {A,B,C} on P2 by ENUMSET1:3;
hence thesis by A1,Def20;
end;
Lm2: ex A,B,C,D st A on P & not {A,B,C,D} is planar
proof
consider A such that
A1: A on P by Def11;
consider A1,B1,C1,D1 being POINT of S such that
A2: not {A1,B1,C1,D1} is planar by Def16;
now
assume
A3: not A1 on P;
A4: now
A5: A1 <> B1 by A2,Th16;
then
A6: {A1,B1} on Line(A1,B1) by Def19;
{A1,B1} on Line (A1,B1) by A5,Def19;
then C1 on Line(A1,B1) implies {A1,B1} \/ {C1} on Line(A1,B1) by Th8;
then
A7: C1 on Line(A1,B1) implies {A1,B1,C1} on Line(A1,B1) by ENUMSET1:3;
set Q = Plane(A1,B1,C1);
assume
A8: A on Line(A1,B1);
A9: not {A1,B1,C1} is linear by A2,Th17;
then {A1,B1,C1} on Q by Def20;
then
A10: A1 on Q & C1 on Q by Th4;
A11: {A1,B1,C1} on Q by A9,Def20;
then D1 on Q implies {A1,B1,C1} \/ {D1} on Q by Th9;
then
A12: D1 on Q implies {A1,B1,C1,D1} on Q by ENUMSET1:6;
{A1,B1} \/ {C1} on Q by A11,ENUMSET1:3;
then {A1,B1} on Q by Th11;
then Line(A1,B1) on Q by A5,A6,Def14;
then A on Q by A8,Def17;
then
A13: {A,A1,C1} on Plane(A1,B1,C1) by A10,Th4;
A1 on Line(A1,B1) by A6,Th1;
then {A,A1} on Line(A1,B1) by A8,Th1;
then not {A,A1,C1} is linear by A1,A3,A9,A7,Th18;
then not {A,A1,C1,D1} is planar by A2,A12,A13,Th19;
hence thesis by A1;
end;
now
set Q = Plane(A1,B1,A);
assume
A14: not A on Line(A1,B1);
A15: A1 <> B1 by A2,Th16;
then
A16: {A1,B1} on Line(A1,B1) by Def19;
then not {A1,B1,A} is linear by A14,A15,Th18;
then
A17: {A1,B1,A} on Q by Def20;
then {A1,B1} \/ {A} on Q by ENUMSET1:3;
then {A1,B1} on Q by Th9;
then {C1,D1} on Q implies {A1,B1} \/ {C1,D1} on Q by Th11;
then {C1,D1} on Q implies {A1,B1,C1,D1} on Q by ENUMSET1:5;
then not C1 on Q or not D1 on Q by A2,Th3;
then
not {A1,B1,A,C1} is planar or not {A1,B1,A,D1} is planar by A14,A15,A16
,A17,Th18,Th19;
then not {A,A1,B1,C1} is planar or not {A,A1,B1,D1} is planar by
ENUMSET1:67;
hence thesis by A1;
end;
hence thesis by A4;
end;
hence thesis by A2;
end;
:: The fourth axiom of incidence
theorem Th41:
ex A,B,C st {A,B,C} on P & not {A,B,C} is linear
proof
consider A1,B1,C1,D1 being POINT of S such that
A1: A1 on P and
A2: not {A1,B1,C1,D1} is planar by Lm2;
not {B1,D1,A1,C1} is planar by A2,ENUMSET1:69;
then
A3: B1 <> D1 by Th16;
not {C1,D1,A1,B1} is planar by A2,ENUMSET1:73;
then
A4: C1 <> D1 by Th16;
not {A1,B1,C1,D1} on P by A2;
then not {B1,C1,D1,A1} on P by ENUMSET1:68;
then not {B1,C1,D1} \/ {A1} on P by ENUMSET1:6;
then not {B1,C1,D1} on P by A1,Th9;
then not B1 on P or not C1 on P or not D1 on P by Th4;
then consider X being POINT of S such that
A5: X = B1 or X = C1 or X = D1 and
A6: not X on P;
not {B1,C1,A1,D1} is planar by A2,ENUMSET1:67;
then B1 <> C1 by Th16;
then consider Y,Z being POINT of S such that
A7: ( Y = B1 or Y = C1 or Y = D1)&( Z = B1 or Z = C1 or Z = D1) & Y <>
X & Z <> X & Y <> Z by A5,A3,A4;
set P1 = Plane(X,Y,A1), P2 = Plane(X,Z,A1);
A8: now
assume {A1,X,Y,Z} is planar;
then {A1,D1,B1,C1} is planar or {A1,D1,C1,B1} is planar by A2,A5,A7,
ENUMSET1:62;
hence contradiction by A2,ENUMSET1:63,64;
end;
then not {A1,X,Y} is linear by Th17;
then not {X,Y,A1} is linear by ENUMSET1:59;
then
A9: {X,Y,A1} on P1 by Def20;
then
A10: A1 on P1 by Th4;
then consider B such that
A11: A1 <> B and
A12: B on P1 and
A13: B on P by A1,Def15;
not {X,Z,A1,Y} is planar by A8,ENUMSET1:69;
then not {X,Z,A1} is linear by Th17;
then
A14: {X,Z,A1} on P2 by Def20;
then
A15: A1 on P2 by Th4;
then consider C such that
A16: A1 <> C and
A17: C on P and
A18: C on P2 by A1,Def15;
take A1,B,C;
thus {A1,B,C} on P by A1,A13,A17,Th4;
given K such that
A19: {A1,B,C} on K;
A20: {A1,C} on P2 by A15,A18,Th3;
{A1,C,B} on K by A19,ENUMSET1:57;
then {A1,C} \/ {B} on K by ENUMSET1:3;
then {A1,C} on K by Th10;
then
A21: K on P2 by A16,A20,Def14;
consider E such that
A22: B <> E and
A23: E on K by Lm1;
{A1,B} \/ {C} on K by A19,ENUMSET1:3;
then
A24: {A1,B} on K by Th10;
A25: now
{A1,B} on P by A1,A13,Th3;
then K on P by A11,A24,Def14;
then E on P by A23,Def17;
then
A26: {E,B} on P by A13,Th3;
assume {X,B,E} is linear;
then consider L such that
A27: {X,B,E} on L;
A28: X on L by A27,Th2;
{E,B,X} on L by A27,ENUMSET1:60;
then {E,B} \/ {X} on L by ENUMSET1:3;
then {E,B} on L by Th8;
then L on P by A22,A26,Def14;
hence contradiction by A6,A28,Def17;
end;
B on K by A19,Th2;
then
A29: B on P2 by A21,Def17;
A30: X on P2 by A14,Th4;
A31: X on P1 by A9,Th4;
{A1,B} on P1 by A10,A12,Th3;
then K on P1 by A11,A24,Def14;
then E on P1 by A23,Def17;
then
A32: {X,B,E} on P1 by A12,A31,Th4;
E on P2 by A23,A21,Def17;
then {X,B,E} on P2 by A29,A30,Th4;
then P1 = P2 by A25,A32,Def13;
then Z on P1 by A14,Th4;
then {X,Y,A1} \/ {Z} on P1 by A9,Th9;
then {X,Y,A1,Z} on P1 by ENUMSET1:6;
then {X,Y,A1,Z} is planar;
hence contradiction by A8,ENUMSET1:67;
end;
:: Fundamental existence theorems
theorem
ex A,B,C,D st A on P & not {A,B,C,D} is planar by Lm2;
theorem
ex B st A <> B & B on L by Lm1;
theorem Th44:
A <> B implies ex C st C on P & not {A,B,C} is linear
proof
consider L such that
A1: {A,B} on L by Def9;
consider C,D,E such that
A2: {C,D,E} on P and
A3: not {C,D,E} is linear by Th41;
A4: C on P & D on P by A2,Th4;
not {C,D,E} on L by A3;
then
A5: not C on L or not D on L or not E on L by Th2;
A6: E on P by A2,Th4;
assume A <> B;
then
not {A,B,C} is linear or not {A,B,D} is linear or not {A,B,E} is linear
by A1,A5,Th18;
hence thesis by A4,A6;
end;
theorem Th45:
not {A,B,C} is linear implies ex D st not {A,B,C,D} is planar
proof
assume
A1: not {A,B,C} is linear;
consider P such that
A2: {A,B,C} on P by Def12;
consider A1,B1,C1,D1 being POINT of S such that
A3: not {A1,B1,C1,D1} is planar by Def16;
not {A1,B1,C1,D1} on P by A3;
then not A1 on P or not B1 on P or not C1 on P or not D1 on P by Th5;
then not {A,B,C,A1} is planar or not {A,B,C,B1} is planar or not {A,B,C,C1}
is planar or not {A,B,C,D1} is planar by A1,A2,Th19;
hence thesis;
end;
theorem Th46:
ex B,C st {B,C} on P & not {A,B,C} is linear
proof
A1: now
assume
A2: not A on P;
consider B,C,D such that
A3: {B,C,D} on P and
A4: not {B,C,D} is linear by Th41;
A5: B <> C by A4,Th15;
take B, C;
{B,C} \/ {D} on P by A3,ENUMSET1:3;
hence
A6: {B,C} on P by Th9;
assume {A,B,C} is linear;
then consider K such that
A7: {A,B,C} on K;
{B,C,A} on K by A7,ENUMSET1:59;
then
A8: {B,C} \/ {A} on K by ENUMSET1:3;
then
A9: A on K by Th8;
{B,C} on K by A8,Th10;
then K on P by A6,A5,Def14;
hence contradiction by A2,A9,Def17;
end;
now
assume A on P;
then consider B such that
A10: A <> B and
A11: B on P and
B on P by Def15;
consider C such that
A12: C on P and
A13: not {A,B,C} is linear by A10,Th44;
{B,C} on P by A11,A12,Th3;
hence thesis by A13;
end;
hence thesis by A1;
end;
theorem Th47:
A <> B implies ex C,D st not {A,B,C,D} is planar
proof
set P = the PLANE of S;
assume A <> B;
then consider C such that
C on P and
A1: not {A,B,C} is linear by Th44;
ex D st not {A,B,C,D} is planar by A1,Th45;
hence thesis;
end;
theorem
ex B,C,D st not {A,B,C,D} is planar
proof
set L = the LINE of S;
consider B such that
A1: A <> B and
B on L by Lm1;
ex C,D st not {A,B,C,D} is planar by A1,Th47;
hence thesis;
end;
theorem
ex L st not A on L & L on P
proof
consider B,C such that
A1: {B,C} on P and
A2: not {A,B,C} is linear by Th46;
consider L such that
A3: {B,C} on L by Def9;
take L;
A on L implies {B,C} \/ {A} on L by A3,Th8;
then A on L implies {B,C,A} on L by ENUMSET1:3;
then A on L implies {A,B,C} on L by ENUMSET1:59;
hence not A on L by A2;
not {B,C,A} is linear by A2,ENUMSET1:59;
then B <> C by Th15;
hence thesis by A1,A3,Def14;
end;
theorem Th50:
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
proof
consider B,C such that
A1: {B,C} on P and
A2: not {A,B,C} is linear by Th46;
consider D such that
A3: not {A,B,C,D} is planar by A2,Th45;
assume A on P;
then
A4: {A} \/ {B,C} on P by A1,Th9;
then
A5: {A,B,C} on P by ENUMSET1:2;
take L3 = Line(A,D),L1 = Line(A,B),L2 = Line(A,C);
A6: A <> B by A2,Th15;
then
A7: {A,B} on L1 by Def19;
A8: not {A,C,B} is linear by A2,ENUMSET1:57;
then
A9: A <> C by Th15;
then
A10: {A,C} on L2 by Def19;
then B on L2 implies {A,C} \/ {B} on L2 by Th8;
then B on L2 implies {A,C,B} on L2 by ENUMSET1:3;
hence L1 <> L2 by A8,A7,Th1;
{A,B} \/ {C} on P by A5,ENUMSET1:3;
then {A,B} on P by Th11;
hence L1 on P by A6,A7,Def14;
{A,C,B} on P by A4,ENUMSET1:2;
then {A,C} \/ {B} on P by ENUMSET1:3;
then {A,C} on P by Th9;
hence L2 on P by A9,A10,Def14;
not {A,D,B,C} is planar by A3,ENUMSET1:63;
then A <> D by Th16;
then
A11: {A,D} on L3 by Def19;
then L3 on P implies {A,D} on P by Th14;
then L3 on P implies D on P by Th3;
then L3 on P implies {A,B,C} \/ {D} on P by A5,Th9;
then L3 on P implies {A,B,C,D} on P by ENUMSET1:6;
hence not L3 on P by A3;
thus thesis by A10,A7,A11,Th1;
end;
theorem
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)
proof
consider P such that
A1: {A,A,A} on P by Def12;
A on P by A1,Th4;
then consider L,L1,L2 such that
A2: L1 <> L2 and
A3: L1 on P and
A4: L2 on P and
A5: not L on P and
A6: A on L and
A7: A on L1 and
A8: A on L2 by Th50;
consider B such that
A9: A <> B and
A10: B on L1 by Lm1;
consider C such that
A11: A <> C and
A12: C on L2 by Lm1;
A13: C on P by A4,A12,Def17;
A14: {A,B} on L1 by A7,A10,Th1;
then {A,B} on P by A3,Th14;
then {A,B} \/ {C} on P by A13,Th9;
then
A15: {A,B,C} on P by ENUMSET1:3;
take L,L1,L2;
thus A on L & A on L1 & A on L2 by A6,A7,A8;
given Q such that
A16: L on Q and
A17: L1 on Q and
A18: L2 on Q;
A19: C on Q by A18,A12,Def17;
A20: {A,C} on L2 by A8,A12,Th1;
now
given K such that
A21: {A,B,C} on K;
{A,C,B} on K by A21,ENUMSET1:57;
then {A,C} \/ {B} on K by ENUMSET1:3;
then
A22: {A,C} on K by Th8;
{A,B} \/ {C} on K by A21,ENUMSET1:3;
then {A,B} on K by Th8;
then K = L1 by A9,A14,Def10;
hence contradiction by A2,A11,A20,A22,Def10;
end;
then
A23: not {A,B,C} is linear;
{A,B} on Q by A17,A14,Th14;
then {A,B} \/ {C} on Q by A19,Th9;
then {A,B,C} on Q by ENUMSET1:3;
hence contradiction by A5,A16,A15,A23,Def13;
end;
theorem
ex P st A on P & not L on P
proof
consider B such that
A1: A <> B and
A2: B on L by Lm1;
consider C,D such that
A3: not {A,B,C,D} is planar by A1,Th47;
take P = Plane(A,C,D);
A4: not {A,C,D,B} is planar by A3,ENUMSET1:63;
then not {A,C,D} is linear by Th17;
then
A5: {A,C,D} on P by Def20;
hence A on P by Th4;
B on P implies {A,C,D} \/ {B} on P by A5,Th9;
then B on P implies {A,C,D,B} on P by ENUMSET1:6;
hence thesis by A2,A4,Def17;
end;
theorem
ex A st A on P & not A on L
proof
consider A,B such that
A1: A <> B and
A2: {A,B} on L by Def8;
consider C such that
A3: C on P and
A4: not {A,B,C} is linear by A1,Th44;
take C;
thus C on P by A3;
C on L implies {A,B} \/ {C} on L by A2,Th8;
then C on L implies {A,B,C} on L by ENUMSET1:3;
hence thesis by A4;
end;
theorem
ex K st not(ex P st L on P & K on P)
proof
consider A,B such that
A1: A <> B and
A2: {A,B} on L by Def8;
consider C,D such that
A3: not {A,B,C,D} is planar by A1,Th47;
take K = Line(C,D);
given P such that
A4: L on P and
A5: K on P;
not {C,D,A,B} is planar by A3,ENUMSET1:73;
then C <> D by Th16;
then {C,D} on K by Def19;
then
A6: {C,D} on P by A5,Th14;
{A,B} on P by A2,A4,Th14;
then {A,B} \/ {C,D} on P by A6,Th11;
then {A,B,C,D} on P by ENUMSET1:5;
hence thesis by A3;
end;
theorem
ex P,Q st P <> Q & L on P & L on Q
proof
consider A,B such that
A1: A <> B and
A2: {A,B} on L by Def8;
consider C,D such that
A3: not {A,B,C,D} is planar by A1,Th47;
take P = Plane (A,B,C), Q = Plane(A,B,D);
not {A,B,C} is linear by A3,Th17;
then
A4: {A,B,C} on P by Def20;
not {A,B,D,C} is planar by A3,ENUMSET1:61;
then not {A,B,D} is linear by Th17;
then
A5: {A,B,D} on Q by Def20;
then {A,B} \/ {D} on Q by ENUMSET1:3;
then
A6: {A,B} on Q by Th11;
D on Q by A5,Th4;
then P = Q implies {A,B,C} \/ {D} on P by A4,Th9;
then P = Q implies {A,B,C,D} on P by ENUMSET1:6;
hence P <> Q by A3;
{A,B} \/ {C} on P by A4,ENUMSET1:3;
then {A,B} on P by Th11;
hence thesis by A1,A2,A6,Def14;
end;
:: Intersection of lines and planes
theorem
not L on P & {A,B} on L & {A,B} on P implies A = B by Def14;
theorem
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
proof
assume
A1: P <> Q;
given A such that
A2: A on P and
A3: A on Q;
consider C such that
A4: A <> C and
A5: C on P and
A6: C on Q by A2,A3,Def15;
take L = Line(A,C);
A7: {A,C} on L by A4,Def19;
{A,C} on Q by A3,A6,Th3;
then
A8: L on Q by A4,A7,Def14;
let B;
{A,C} on P by A2,A5,Th3;
then
A9: L on P by A4,A7,Def14;
thus B on P & B on Q implies B on L
proof
assume that
A10: B on P and
A11: B on Q and
A12: not B on L;
consider P1 such that
A13: for P2 holds B on P2 & L on P2 iff P1 = P2 by A12,Th26;
P = P1 by A9,A10,A13;
hence contradiction by A1,A8,A11,A13;
end;
thus thesis by A9,A8,Def17;
end;