:: A Projective Closure and Projective Horizon of an Affine Space
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received December 17, 1990
:: 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 DIRAF, SUBSET_1, STRUCT_0, AFF_4, INCSP_1, AFF_1, ANALOAF,
RELAT_1, TARSKI, PARSP_1, XBOOLE_0, ARYTM_3, SETFAM_1, ZFMISC_1, EQREL_1,
RELAT_2, ANPROJ_1, INCPROJ, MCART_1, FDIFF_1, ANPROJ_2, AFF_2, VECTSP_1,
AFPROJ;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, EQREL_1, RELSET_1,
RELAT_1, RELAT_2, XTUPLE_0, MCART_1, STRUCT_0, ANALOAF, DIRAF, AFF_1,
AFF_4, AFF_2, PAPDESAF, INCSP_1, INCPROJ;
constructors DOMAIN_1, EQREL_1, AFF_1, AFF_2, TRANSLAC, INCPROJ, AFF_4,
RELSET_1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, INCPROJ, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI;
equalities TARSKI;
expansions TARSKI;
theorems RELAT_1, RELAT_2, TARSKI, ZFMISC_1, EQREL_1, AFF_1, AFF_4, INCPROJ,
PAPDESAF, AFF_2, DIRAF, INCSP_1, XBOOLE_0, PARTFUN1, ORDERS_1, XTUPLE_0;
schemes RELSET_1;
begin
reserve AS for AffinSpace;
reserve A,K,M,X,Y,Z,X9,Y9 for Subset of AS;
reserve zz for Element of AS;
reserve x,y for set;
:: The aim of this article is to formalize the well known construction of
:: the projective closure of an affine space. We begin with some evident
:: properties of planes in affine planes.
theorem Th1:
AS is AffinPlane & X=the carrier of AS implies X is being_plane
proof
assume that
A1: AS is AffinPlane and
A2: X=the carrier of AS;
consider a,b,c being Element of AS such that
A3: not LIN a,b,c by AFF_1:12;
set P=Line(a,b),K=Line(a,c);
A4: b in P by AFF_1:15;
A5: c in K by AFF_1:15;
a<>b by A3,AFF_1:7;
then
A6: P is being_line by AFF_1:def 3;
set Y=Plane(K,P);
A7: a in P by AFF_1:15;
a<>c by A3,AFF_1:7;
then
A8: K is being_line by AFF_1:def 3;
A9: a in K by AFF_1:15;
A10: not K // P
proof
assume K // P;
then c in P by A7,A9,A5,AFF_1:45;
hence contradiction by A3,A7,A4,A6,AFF_1:21;
end;
now
let x be object;
assume x in X;
then reconsider a=x as Element of AS;
set K9=a*K;
A11: K9 is being_line by A8,AFF_4:27;
A12: K // K9 by A8,AFF_4:def 3;
then not K9 // P by A10,AFF_1:44;
then consider b being Element of AS such that
A13: b in K9 and
A14: b in P by A1,A6,A11,AFF_1:58;
a in K9 by A8,AFF_4:def 3;
then a,b // K by A12,A13,AFF_1:40;
then a in {zz: ex b being Element of AS st zz,b // K & b in P} by A14;
hence x in Y by AFF_4:def 1;
end;
then
A15: X c= Y;
Y is being_plane by A6,A8,A10,AFF_4:def 2;
hence thesis by A2,A15,XBOOLE_0:def 10;
end;
theorem Th2:
AS is AffinPlane & X is being_plane implies X = the carrier of AS
proof
assume that
A1: AS is AffinPlane and
A2: X is being_plane;
the carrier of AS c= the carrier of AS;
then reconsider Z=the carrier of AS as Subset of AS;
Z is being_plane by A1,Th1;
hence thesis by A2,AFF_4:33;
end;
theorem Th3:
AS is AffinPlane & X is being_plane & Y is being_plane implies X= Y
proof
assume that
A1: AS is AffinPlane and
A2: X is being_plane and
A3: Y is being_plane;
X=the carrier of AS by A1,A2,Th2;
hence thesis by A1,A3,Th2;
end;
theorem
X=the carrier of AS & X is being_plane implies AS is AffinPlane
proof
assume that
A1: X=the carrier of AS and
A2: X is being_plane;
assume AS is not AffinPlane;
then ex zz st not zz in X by A2,AFF_4:48;
hence contradiction by A1;
end;
theorem Th5:
not A // K & A '||' X & A '||' Y & K '||' X & K '||' Y & A is
being_line & K is being_line & X is being_plane & Y is being_plane implies X
'||' Y
proof
assume that
A1: not A // K and
A2: A '||' X and
A3: A '||' Y and
A4: K '||' X and
A5: K '||' Y and
A6: A is being_line and
A7: K is being_line and
A8: X is being_plane and
A9: Y is being_plane;
set y = the Element of Y;
set x = the Element of X;
A10: Y <> {} by A9,AFF_4:59;
A11: X <> {} by A8,AFF_4:59;
then reconsider a=x,b=y as Element of AS by A10,TARSKI:def 3;
A12: K // a*K by A7,AFF_4:def 3;
A13: A // a*A by A6,AFF_4:def 3;
A14: not a*A // a*K
proof
assume not thesis;
then a*A // K by A12,AFF_1:44;
hence contradiction by A1,A13,AFF_1:44;
end;
a*K c= a+X by A4,A7,A8,AFF_4:68;
then
A15: a*K c= X by A8,A11,AFF_4:66;
K // b*K by A7,AFF_4:def 3;
then
A16: a*K // b*K by A12,AFF_1:44;
b*A c= b+Y by A3,A6,A9,AFF_4:68;
then
A17: b*A c= Y by A9,A10,AFF_4:66;
A // b*A by A6,AFF_4:def 3;
then
A18: a*A // b*A by A13,AFF_1:44;
b*K c= b+Y by A5,A7,A9,AFF_4:68;
then
A19: b*K c= Y by A9,A10,AFF_4:66;
a*A c= a+X by A2,A6,A8,AFF_4:68;
then a*A c= X by A8,A11,AFF_4:66;
hence thesis by A8,A9,A15,A17,A19,A14,A18,A16,AFF_4:55;
end;
theorem
X is being_plane & A '||' X & X '||' Y implies A '||' Y by AFF_4:59,60;
:: Next we distinguish two sets, one consisting of the lines, the second
:: consisting of the planes of a given affine space and we consider two
:: equivalence relations defined on each of these sets; theses relations
:: are in fact the relation of parallelity restricted to suitable area.
:: Their equivalence classes are called directions (of lines and planes,
:: respectively); they are intended to be considered as new objects which
:: extend the given affine space to a projective space.
definition
let AS;
func AfLines(AS) -> Subset-Family of AS equals
{A: A is being_line};
coherence
proof
set X={A: A is being_line};
X c= bool the carrier of AS
proof
let x be object;
assume x in X;
then ex A st x=A & A is being_line;
hence thesis;
end;
hence thesis;
end;
end;
definition
let AS;
func AfPlanes(AS) -> Subset-Family of AS equals
{A: A is being_plane};
coherence
proof
set X={A: A is being_plane};
X c= bool the carrier of AS
proof
let x be object;
assume x in X;
then ex A st x=A & A is being_plane;
hence thesis;
end;
hence thesis;
end;
end;
theorem
for x holds (x in AfLines(AS) iff ex X st x=X & X is being_line);
theorem
for x holds (x in AfPlanes(AS) iff ex X st x=X & X is being_plane);
definition
let AS;
func LinesParallelity(AS) -> Equivalence_Relation of AfLines(AS) equals
{[K,
M]: K is being_line & M is being_line & K '||' M};
coherence
proof
set AFL=AfLines(AS),AFL2=[:AfLines(AS),AfLines(AS):];
set R1={[X,Y]: X is being_line & Y is being_line & X '||' Y};
now
let x be object;
assume x in R1;
then consider X,Y such that
A1: x=[X,Y] and
A2: X is being_line and
A3: Y is being_line and
X '||' Y;
A4: Y in AFL by A3;
X in AFL by A2;
hence x in AFL2 by A1,A4,ZFMISC_1:def 2;
end;
then reconsider R2=R1 as Relation of AFL,AFL by TARSKI:def 3;
now
let x be object;
assume x in AFL;
then consider X such that
A5: x=X and
A6: X is being_line;
X // X by A6,AFF_1:41;
then X '||' X by A6,AFF_4:40;
hence [x,x] in R2 by A5,A6;
end;
then
A7: R2 is_reflexive_in AFL by RELAT_2:def 1;
then
A8: field R2 = AFL by ORDERS_1:13;
A9: X is being_line & Y is being_line implies ([X,Y] in R1 iff X '||' Y)
proof
assume that
A10: X is being_line and
A11: Y is being_line;
now
assume [X,Y] in R1;
then consider X9,Y9 such that
A12: [X,Y]=[X9,Y9] and
X9 is being_line and
Y9 is being_line and
A13: X9 '||' Y9;
X=X9 by A12,XTUPLE_0:1;
hence X '||' Y by A12,A13,XTUPLE_0:1;
end;
hence thesis by A10,A11;
end;
now
let x,y,z be object;
assume that
A14: x in AFL and
A15: y in AFL and
A16: z in AFL and
A17: [x,y] in R2 and
A18: [y,z] in R2;
consider Y such that
A19: y=Y and
A20: Y is being_line by A15;
consider Z such that
A21: z=Z and
A22: Z is being_line by A16;
Y '||' Z by A9,A18,A19,A20,A21,A22;
then
A23: Y // Z by A20,A22,AFF_4:40;
consider X such that
A24: x=X and
A25: X is being_line by A14;
X '||' Y by A9,A17,A24,A25,A19,A20;
then X // Y by A25,A20,AFF_4:40;
then X // Z by A23,AFF_1:44;
then X '||' Z by A25,A22,AFF_4:40;
hence [x,z] in R2 by A24,A25,A21,A22;
end;
then
A26: R2 is_transitive_in AFL by RELAT_2:def 8;
now
let x,y be object;
assume that
A27: x in AFL and
A28: y in AFL and
A29: [x,y] in R2;
consider X such that
A30: x=X and
A31: X is being_line by A27;
consider Y such that
A32: y=Y and
A33: Y is being_line by A28;
X '||' Y by A9,A29,A30,A31,A32,A33;
then X // Y by A31,A33,AFF_4:40;
then Y '||' X by A31,A33,AFF_4:40;
hence [y,x] in R2 by A30,A31,A32,A33;
end;
then
A34: R2 is_symmetric_in AFL by RELAT_2:def 3;
dom R2 = AFL by A7,ORDERS_1:13;
hence thesis by A8,A34,A26,PARTFUN1:def 2,RELAT_2:def 11,def 16;
end;
end;
definition
let AS;
func PlanesParallelity(AS) -> Equivalence_Relation of AfPlanes(AS) equals
{[
X,Y]: X is being_plane & Y is being_plane & X '||' Y};
coherence
proof
set AFP=AfPlanes(AS),AFP2=[:AfPlanes(AS),AfPlanes(AS):];
set R1={[X,Y]: X is being_plane & Y is being_plane & X '||' Y};
now
let x be object;
assume x in R1;
then consider X,Y such that
A1: x=[X,Y] and
A2: X is being_plane and
A3: Y is being_plane and
X '||' Y;
A4: Y in AFP by A3;
X in AFP by A2;
hence x in AFP2 by A1,A4,ZFMISC_1:def 2;
end;
then reconsider R2=R1 as Relation of AFP,AFP by TARSKI:def 3;
now
let x be object;
assume x in AFP;
then consider X such that
A5: x=X and
A6: X is being_plane;
X '||' X by A6,AFF_4:57;
hence [x,x] in R2 by A5,A6;
end;
then
A7: R2 is_reflexive_in AFP by RELAT_2:def 1;
then
A8: field R2 = AFP by ORDERS_1:13;
A9: X is being_plane & Y is being_plane implies ([X,Y] in R1 iff X '||' Y)
proof
assume that
A10: X is being_plane and
A11: Y is being_plane;
now
assume [X,Y] in R1;
then consider X9,Y9 such that
A12: [X,Y]=[X9,Y9] and
X9 is being_plane and
Y9 is being_plane and
A13: X9 '||' Y9;
X=X9 by A12,XTUPLE_0:1;
hence X '||' Y by A12,A13,XTUPLE_0:1;
end;
hence thesis by A10,A11;
end;
now
let x,y,z be object;
assume that
A14: x in AFP and
A15: y in AFP and
A16: z in AFP and
A17: [x,y] in R2 and
A18: [y,z] in R2;
consider X such that
A19: x=X and
A20: X is being_plane by A14;
consider Y such that
A21: y=Y and
A22: Y is being_plane by A15;
consider Z such that
A23: z=Z and
A24: Z is being_plane by A16;
A25: Y '||' Z by A9,A18,A21,A22,A23,A24;
X '||' Y by A9,A17,A19,A20,A21,A22;
then X '||' Z by A20,A22,A24,A25,AFF_4:61;
hence [x,z] in R2 by A19,A20,A23,A24;
end;
then
A26: R2 is_transitive_in AFP by RELAT_2:def 8;
now
let x,y be object;
assume that
A27: x in AFP and
A28: y in AFP and
A29: [x,y] in R2;
consider X such that
A30: x=X and
A31: X is being_plane by A27;
consider Y such that
A32: y=Y and
A33: Y is being_plane by A28;
X '||' Y by A9,A29,A30,A31,A32,A33;
then Y '||' X by A31,A33,AFF_4:58;
hence [y,x] in R2 by A30,A31,A32,A33;
end;
then
A34: R2 is_symmetric_in AFP by RELAT_2:def 3;
dom R2 = AFP by A7,ORDERS_1:13;
hence thesis by A8,A34,A26,PARTFUN1:def 2,RELAT_2:def 11,def 16;
end;
end;
definition
let AS,X;
func LDir(X) -> Subset of AfLines(AS) equals
Class(LinesParallelity(AS),X);
correctness;
end;
definition
let AS,X;
func PDir(X) -> Subset of AfPlanes(AS) equals
Class(PlanesParallelity(AS),X);
correctness;
end;
theorem Th9:
X is being_line implies for x holds x in LDir(X) iff ex Y st x=Y
& Y is being_line & X '||' Y
proof
assume
A1: X is being_line;
let x;
A2: now
assume x in LDir(X);
then [x,X] in LinesParallelity(AS) by EQREL_1:19;
then consider K,M such that
A3: [x,X]=[K,M] and
A4: K is being_line and
A5: M is being_line and
A6: K '||' M;
take Y=K;
A7: X=M by A3,XTUPLE_0:1;
K // M by A4,A5,A6,AFF_4:40;
hence x=Y & Y is being_line & X '||' Y by A3,A4,A5,A7,AFF_4:40,XTUPLE_0:1;
end;
now
given Y such that
A8: x=Y and
A9: Y is being_line and
A10: X '||' Y;
X // Y by A1,A9,A10,AFF_4:40;
then Y '||' X by A1,A9,AFF_4:40;
then
[Y,X] in {[K,M]: K is being_line & M is being_line & K '||' M} by A1,A9;
hence x in LDir(X) by A8,EQREL_1:19;
end;
hence thesis by A2;
end;
theorem Th10:
X is being_plane implies for x holds x in PDir(X) iff ex Y st x=
Y & Y is being_plane & X '||' Y
proof
assume
A1: X is being_plane;
let x;
A2: now
assume x in PDir(X);
then [x,X] in PlanesParallelity(AS) by EQREL_1:19;
then consider K,M such that
A3: [x,X]=[K,M] and
A4: K is being_plane and
A5: M is being_plane and
A6: K '||' M;
take Y=K;
X=M by A3,XTUPLE_0:1;
hence x=Y & Y is being_plane & X '||' Y by A3,A4,A5,A6,AFF_4:58,XTUPLE_0:1;
end;
now
given Y such that
A7: x=Y and
A8: Y is being_plane and
A9: X '||' Y;
Y '||' X by A1,A8,A9,AFF_4:58;
then [Y,X] in { [K,M]: K is being_plane & M is being_plane & K '||' M} by
A1,A8;
hence x in PDir(X) by A7,EQREL_1:19;
end;
hence thesis by A2;
end;
theorem Th11:
X is being_line & Y is being_line implies (LDir(X)=LDir(Y) iff X // Y)
proof
assume that
A1: X is being_line and
A2: Y is being_line;
A3: LDir(Y)= Class(LinesParallelity(AS),Y);
A4: Y in AfLines(AS) by A2;
A5: now
assume LDir(X)=LDir(Y);
then X in Class(LinesParallelity(AS),Y) by A4,EQREL_1:23;
then ex Y9 st X=Y9 & Y9 is being_line & Y '||' Y9 by A2,A3,Th9;
hence X // Y by A2,AFF_4:40;
end;
A6: LDir(X)=Class(LinesParallelity(AS),X);
A7: X in AfLines(AS) by A1;
now
assume X // Y;
then X '||' Y by A1,A2,AFF_4:40;
then Y in Class(LinesParallelity(AS),X) by A1,A2,A6,Th9;
hence LDir(X)=LDir(Y) by A7,EQREL_1:23;
end;
hence thesis by A5;
end;
theorem Th12:
X is being_line & Y is being_line implies (LDir(X)=LDir(Y) iff X '||' Y)
proof
assume that
A1: X is being_line and
A2: Y is being_line;
LDir(X)=LDir(Y) iff X // Y by A1,A2,Th11;
hence thesis by A1,A2,AFF_4:40;
end;
theorem Th13:
X is being_plane & Y is being_plane implies (PDir(X)=PDir(Y) iff X '||' Y)
proof
assume that
A1: X is being_plane and
A2: Y is being_plane;
A3: PDir(Y)= Class(PlanesParallelity(AS),Y);
A4: Y in AfPlanes(AS) by A2;
A5: now
assume PDir(X)=PDir(Y);
then X in Class(PlanesParallelity(AS),Y) by A4,EQREL_1:23;
then ex Y9 st X=Y9 & Y9 is being_plane & Y '||' Y9 by A2,A3,Th10;
hence X '||' Y by A2,AFF_4:58;
end;
A6: PDir(X)=Class(PlanesParallelity(AS),X);
A7: X in AfPlanes(AS) by A1;
now
assume X '||' Y;
then Y in Class(PlanesParallelity(AS),X) by A1,A2,A6,Th10;
hence PDir(X)=PDir(Y) by A7,EQREL_1:23;
end;
hence thesis by A5;
end;
definition
let AS;
func Dir_of_Lines(AS) -> non empty set equals
Class LinesParallelity(AS);
coherence
proof
consider a,b being Element of AS such that
A1: a<>b by DIRAF:40;
set A=Line(a,b);
A is being_line by A1,AFF_1:def 3;
then A in AfLines(AS);
then (Class(LinesParallelity(AS),A)) in Class LinesParallelity(AS) by
EQREL_1:def 3;
hence thesis;
end;
end;
definition
let AS;
func Dir_of_Planes(AS) -> non empty set equals
Class PlanesParallelity(AS);
coherence
proof
set a = the Element of AS;
consider A such that
a in A and
a in A and
a in A and
A1: A is being_plane by AFF_4:37;
A in AfPlanes(AS) by A1;
then (Class(PlanesParallelity(AS),A)) in Class PlanesParallelity(AS) by
EQREL_1:def 3;
hence thesis;
end;
end;
theorem Th14:
for x holds x in Dir_of_Lines(AS) iff ex X st x=LDir(X) & X is being_line
proof
let x;
A1: now
assume
A2: x in Dir_of_Lines(AS);
then reconsider x99=x as Subset of AfLines(AS);
consider x9 being object such that
A3: x9 in AfLines(AS) and
A4: x99=Class(LinesParallelity(AS),x9) by A2,EQREL_1:def 3;
consider X such that
A5: x9=X and
A6: X is being_line by A3;
take X;
thus x=LDir(X) by A4,A5;
thus X is being_line by A6;
end;
now
given X such that
A7: x=LDir(X) and
A8: X is being_line;
X in AfLines(AS) by A8;
hence x in Dir_of_Lines(AS) by A7,EQREL_1:def 3;
end;
hence thesis by A1;
end;
theorem Th15:
for x holds x in Dir_of_Planes(AS) iff ex X st x=PDir(X) & X is being_plane
proof
let x;
A1: now
assume
A2: x in Dir_of_Planes(AS);
then reconsider x99= x as Subset of AfPlanes(AS);
consider x9 being object such that
A3: x9 in AfPlanes(AS) and
A4: x99=Class(PlanesParallelity(AS),x9) by A2,EQREL_1:def 3;
consider X such that
A5: x9=X and
A6: X is being_plane by A3;
take X;
thus x=PDir(X) by A4,A5;
thus X is being_plane by A6;
end;
now
given X such that
A7: x=PDir(X) and
A8: X is being_plane;
X in AfPlanes(AS) by A8;
hence x in Dir_of_Planes(AS) by A7,EQREL_1:def 3;
end;
hence thesis by A1;
end;
:: The point is to guarantee that the classes of new objects consist of really
:: new objects. Clearly the set of directions of lines and the set of affine
:: points do not intersect. However we cannot claim, in general, that the set
:: of affine lines and the set of directions of planes do not intersect; this
:: is evidently true only in the case of affine planes. Therefore we have to
:: modify (slightly) a construction of the set of lines of the projective
:: closure of affine space, when compared with (naive) intuitions.
theorem Th16:
the carrier of AS misses Dir_of_Lines(AS)
proof
assume not thesis;
then consider x being object such that
A1: x in (the carrier of AS) and
A2: x in Dir_of_Lines(AS) by XBOOLE_0:3;
reconsider a=x as Element of AS by A1;
consider X such that
A3: x=LDir(X) and
A4: X is being_line by A2,Th14;
set A=a*X;
A5: A is being_line by A4,AFF_4:27;
X // A by A4,AFF_4:def 3;
then X '||' A by A4,A5,AFF_4:40;
then A in a by A3,A4,A5,Th9;
hence contradiction by A4,AFF_4:def 3;
end;
theorem
AS is AffinPlane implies AfLines(AS) misses Dir_of_Planes(AS)
proof
the carrier of AS c= the carrier of AS;
then reconsider X9=the carrier of AS as Subset of AS;
assume AS is AffinPlane;
then
A1: X9 is being_plane by Th1;
assume not thesis;
then consider x being object such that
A2: x in AfLines(AS) and
A3: x in Dir_of_Planes(AS) by XBOOLE_0:3;
consider Y such that
A4: x=Y and
A5: Y is being_line by A2;
consider X such that
A6: x=PDir(X) and
A7: X is being_plane by A3,Th15;
consider a,b being Element of AS such that
A8: a in Y and
b in Y and
a<>b by A5,AFF_1:19;
consider Y9 such that
A9: a = Y9 and
A10: Y9 is being_plane and
X '||' Y9 by A6,A7,A4,A8,Th10;
A11: not Y9 in Y9;
Y9 = X9 by A1,A10,AFF_4:33;
hence contradiction by A9,A11;
end;
theorem Th18:
for x holds (x in [:AfLines(AS),{1}:] iff ex X st x=[X,1] & X is being_line)
proof
let x;
A1: now
assume x in [:AfLines(AS),{1}:];
then consider x1,x2 being object such that
A2: x1 in AfLines(AS) and
A3: x2 in {1} and
A4: x=[x1,x2] by ZFMISC_1:def 2;
consider X such that
A5: x1=X and
A6: X is being_line by A2;
take X;
thus x=[X,1] by A3,A4,A5,TARSKI:def 1;
thus X is being_line by A6;
end;
now
given X such that
A7: x=[X,1] and
A8: X is being_line;
X in AfLines(AS ) by A8;
hence x in [:AfLines(AS),{1}:] by A7,ZFMISC_1:106;
end;
hence thesis by A1;
end;
theorem Th19:
for x holds (x in [:Dir_of_Planes(AS),{2}:] iff ex X st x=[PDir(
X),2] & X is being_plane)
proof
let x;
A1: now
assume x in [:Dir_of_Planes(AS),{2}:];
then consider x1,x2 being object such that
A2: x1 in Dir_of_Planes(AS) and
A3: x2 in {2} and
A4: x=[x1,x2] by ZFMISC_1:def 2;
consider X such that
A5: x1=PDir(X) and
A6: X is being_plane by A2,Th15;
take X;
thus x=[PDir(X),2] by A3,A4,A5,TARSKI:def 1;
thus X is being_plane by A6;
end;
(ex X st x=[PDir(X),2] & X is being_plane)
implies x in [:Dir_of_Planes(AS),{2}:] by Th15,ZFMISC_1:106;
hence thesis by A1;
end;
definition
let AS;
func ProjectivePoints(AS) -> non empty set equals
(the carrier of AS) \/
Dir_of_Lines(AS);
correctness;
end;
definition
let AS;
func ProjectiveLines(AS) -> non empty set equals
[:AfLines(AS),{1}:] \/ [:
Dir_of_Planes(AS),{2}:];
coherence;
end;
definition
let AS;
func Proj_Inc(AS) -> Relation of ProjectivePoints(AS),ProjectiveLines(AS)
means
:Def11:
for x,y being object
holds [x,y] in it iff (ex K st K is being_line & y=[K,1]
& (x in the carrier of AS & x in K or x = LDir(K))) or ex K,X st K is
being_line & X is being_plane & x=LDir(K) & y=[PDir(X),2] & K '||' X;
existence
proof
defpred P[object,object] means
((ex K st K is being_line & $2=[K,1] & ($1 in the
carrier of AS & $1 in K or $1 = LDir(K))) or (ex K,X st K is being_line & X is
being_plane & $1=LDir(K) & $2=[PDir(X),2] & K '||' X));
set VV1 = ProjectivePoints(AS), VV2 = ProjectiveLines(AS);
consider P being Relation of VV1,VV2 such that
A1: for x,y being object holds [x,y] in P iff x in VV1 & y in VV2 & P[x,y]
from RELSET_1:sch 1;
take P;
let x,y be object;
thus [x,y] in P implies (ex K st K is being_line & y=[K,1] & (x in the
carrier of AS & x in K or x = LDir(K))) or ex K,X st K is being_line & X is
being_plane & x=LDir(K) & y=[PDir(X),2] & K '||' X by A1;
assume
A2: (ex K st K is being_line & y=[K,1] & (x in the carrier of AS & x
in K or x = LDir(K))) or ex K,X st K is being_line & X is being_plane & x=LDir(
K) & y=[PDir(X),2] & K '||' X;
x in VV1 & y in VV2
proof
A3: now
given K such that
A4: K is being_line and
A5: y=[K,1] and
A6: x in the carrier of AS & x in K or x = LDir(K);
A7: now
assume x=LDir(K);
then x in Dir_of_Lines(AS) by A4,Th14;
hence x in VV1 by XBOOLE_0:def 3;
end;
y in [:AfLines(AS),{1}:] by A4,A5,Th18;
hence thesis by A6,A7,XBOOLE_0:def 3;
end;
now
given K,X such that
A8: K is being_line and
A9: X is being_plane and
A10: x=LDir(K) and
A11: y=[PDir(X),2] and
K '||' X;
x in Dir_of_Lines(AS) by A8,A10,Th14;
hence x in VV1 by XBOOLE_0:def 3;
y in [:Dir_of_Planes(AS),{2}:] by A9,A11,Th19;
hence y in VV2 by XBOOLE_0:def 3;
end;
hence thesis by A2,A3;
end;
hence thesis by A1,A2;
end;
uniqueness
proof
let P,Q be Relation of ProjectivePoints(AS),ProjectiveLines(AS) such that
A12: for x,y being object holds
[x,y] in P iff (ex K st K is being_line & y=[K,1] & (x in the
carrier of AS & x in K or x = LDir(K))) or ex K,X st K is being_line & X is
being_plane & x=LDir(K) & y=[PDir(X),2] & K '||' X and
A13: for x,y being object holds
[x,y] in Q iff (ex K st K is being_line & y=[K,1] & (x in the
carrier of AS & x in K or x = LDir(K))) or ex K,X st K is being_line & X is
being_plane & x=LDir(K) & y=[PDir(X),2] & K '||' X;
for x,y being object holds [x,y] in P iff [x,y] in Q
proof
let x,y be object;
[x,y] in P iff (ex K st K is being_line & y=[K,1] & (x in the
carrier of AS & x in K or x = LDir(K))) or ex K,X st K is being_line & X is
being_plane & x=LDir(K) & y=[PDir(X),2] & K '||' X by A12;
hence thesis by A13;
end;
hence thesis by RELAT_1:def 2;
end;
end;
definition
let AS;
func Inc_of_Dir(AS) -> Relation of Dir_of_Lines(AS),Dir_of_Planes(AS) means
:Def12:
for x,y being object
holds [x,y] in it iff ex A,X st x=LDir(A) & y=PDir(X) & A is
being_line & X is being_plane & A '||' X;
existence
proof
defpred P[object,object] means ex A,X st $1=LDir(A) & $2=PDir(X) & A is
being_line & X is being_plane & A '||' X;
set VV1 = Dir_of_Lines(AS), VV2 = Dir_of_Planes(AS);
consider P being Relation of VV1,VV2 such that
A1: for x,y being object holds [x,y] in P iff x in VV1 & y in VV2 & P[x,y]
from RELSET_1:sch 1;
take P;
let x,y be object;
thus [x,y] in P implies ex A,X st x=LDir(A) & y=PDir(X) & A is being_line
& X is being_plane & A '||' X by A1;
assume
A2: ex A,X st x=LDir(A) & y=PDir(X) & A is being_line & X is
being_plane & A '||' X;
then
A3: y in VV2 by Th15;
x in VV1 by A2,Th14;
hence thesis by A1,A2,A3;
end;
uniqueness
proof
let P,Q be Relation of Dir_of_Lines(AS),Dir_of_Planes(AS) such that
A4: for x,y being object holds
[x,y] in P iff ex A,X st x=LDir(A) & y=PDir(X) & A is being_line &
X is being_plane & A '||' X and
A5: for x,y being object holds
[x,y] in Q iff ex A,X st x=LDir(A) & y=PDir(X) & A is being_line &
X is being_plane & A '||' X;
for x,y being object holds [x,y] in P iff [x,y] in Q
proof
let x,y be object;
[x,y] in P iff ex A,X st x=LDir(A) & y=PDir(X) & A is being_line &
X is being_plane & A '||' X by A4;
hence thesis by A5;
end;
hence thesis by RELAT_1:def 2;
end;
end;
definition
let AS;
func IncProjSp_of(AS) -> strict IncProjStr equals
IncProjStr (#
ProjectivePoints(AS), ProjectiveLines(AS), Proj_Inc(AS) #);
correctness;
end;
definition
let AS;
func ProjHorizon(AS) -> strict IncProjStr equals
IncProjStr (#Dir_of_Lines(
AS), Dir_of_Planes(AS), Inc_of_Dir(AS) #);
correctness;
end;
theorem Th20:
for x holds (x is POINT of IncProjSp_of(AS) iff (x is Element of
AS or ex X st x=LDir(X) & X is being_line))
proof
let x;
A1: now
A2: now
given X such that
A3: x=LDir(X) and
A4: X is being_line;
x in Dir_of_Lines( AS ) by A3,A4,Th14;
hence x is POINT of IncProjSp_of(AS) by XBOOLE_0:def 3;
end;
assume x is Element of AS or ex X st x=LDir(X) & X is being_line;
hence x is POINT of IncProjSp_of(AS) by A2,XBOOLE_0:def 3;
end;
now
assume
A5: x is POINT of IncProjSp_of(AS);
x in Dir_of_Lines(AS) implies ex X st x=LDir(X) & X is being_line by Th14;
hence x is Element of AS or ex X st x=LDir(X) & X is being_line by A5,
XBOOLE_0:def 3;
end;
hence thesis by A1;
end;
theorem
x is Element of the Points of ProjHorizon(AS) iff ex X st x=LDir(X) &
X is being_line by Th14;
theorem Th22:
x is Element of the Points of ProjHorizon(AS) implies x is POINT
of IncProjSp_of(AS)
proof
assume x is Element of the Points of ProjHorizon(AS);
then ex X st x=LDir(X) & X is being_line by Th14;
hence thesis by Th20;
end;
theorem Th23:
for x holds (x is LINE of IncProjSp_of(AS) iff ex X st (x=[X,1]
& X is being_line or x=[PDir(X),2] & X is being_plane))
proof
let x;
A1: now
given X such that
A2: x=[X,1] & X is being_line or x=[PDir(X),2] & X is being_plane;
A3: now
assume that
A4: x=[PDir(X),2] and
A5: X is being_plane;
x in [:Dir_of_Planes(AS),{2}:] by A4,A5,Th19;
hence x is LINE of IncProjSp_of(AS) by XBOOLE_0:def 3;
end;
now
assume that
A6: x=[X,1] and
A7: X is being_line;
x in [:AfLines(AS),{1}:] by A6,A7,Th18;
hence x is LINE of IncProjSp_of(AS) by XBOOLE_0:def 3;
end;
hence x is LINE of IncProjSp_of(AS) by A2,A3;
end;
now
A8: x in [:Dir_of_Planes(AS),{2}:] implies ex X st x=[X,1] & X is
being_line or x=[PDir(X),2] & X is being_plane by Th19;
assume
A9: x is LINE of IncProjSp_of(AS);
x in [:AfLines(AS),{1}:] implies ex X st x=[X,1] & X is being_line or
x=[PDir(X),2] & X is being_plane by Th18;
hence
ex X st x=[X,1] & X is being_line or x=[PDir(X),2] & X is being_plane
by A9,A8,XBOOLE_0:def 3;
end;
hence thesis by A1;
end;
theorem
x is Element of the Lines of ProjHorizon(AS) iff ex X st x=PDir(X) & X
is being_plane by Th15;
theorem Th25:
x is Element of the Lines of ProjHorizon(AS) implies [x,2] is
LINE of IncProjSp_of(AS)
proof
assume x is Element of the Lines of ProjHorizon(AS);
then ex X st x=PDir(X) & X is being_plane by Th15;
hence thesis by Th23;
end;
reserve x,y,z,t,u,w for Element of AS;
reserve K,X,Y,Z,X9,Y9 for Subset of AS;
reserve a,b,c,d,p,q,r,p9 for POINT of IncProjSp_of(AS);
reserve A for LINE of IncProjSp_of(AS);
theorem Th26:
x=a & [X,1]=A implies (a on A iff X is being_line & x in X)
proof
assume that
A1: x=a and
A2: [X,1]=A;
A3: now
A4: now
given K such that
A5: K is being_line and
A6: [X,1]=[K,1] and
A7: x in the carrier of AS & x in K or x = LDir(K);
A8: now
assume x=LDir(K);
then x in Dir_of_Lines(AS) by A5,Th14;
then (the carrier of AS) /\ Dir_of_Lines(AS) <> {} by XBOOLE_0:def 4;
then (the carrier of AS) meets Dir_of_Lines(AS) by XBOOLE_0:def 7;
hence contradiction by Th16;
end;
X=[K,1]`1 by A6
.= K;
hence X is being_line & x in X by A5,A7,A8;
end;
assume a on A;
then
A9: [a,A] in the Inc of IncProjSp_of(AS) by INCSP_1:def 1;
not ex K,X9 st K is being_line & X9 is being_plane & x=LDir(K) & [X,1
]=[PDir(X9),2] & K '||' X9 by XTUPLE_0:1;
hence X is being_line & x in X by A1,A2,A9,A4,Def11;
end;
now
assume that
A10: X is being_line and
A11: x in X;
[x,[X,1]] in Proj_Inc(AS) by A10,A11,Def11;
hence a on A by A1,A2,INCSP_1:def 1;
end;
hence thesis by A3;
end;
theorem Th27:
x=a & [PDir(X),2]=A implies not a on A
proof
assume that
A1: x=a and
A2: [PDir(X),2]=A;
A3: now
given K such that
K is being_line and
A4: [PDir(X),2]=[K,1] and
x in the carrier of AS & x in K or x = LDir(K);
2 = [K,1]`2 by A4
.= 1;
hence contradiction;
end;
A5: now
given K,X9 such that
A6: K is being_line and
X9 is being_plane and
A7: x=LDir(K) and
[PDir(X),2]=[PDir(X9),2] and
K '||' X9;
x in Dir_of_Lines(AS) by A6,A7,Th14;
then (the carrier of AS) /\ Dir_of_Lines(AS) <> {} by XBOOLE_0:def 4;
then (the carrier of AS) meets Dir_of_Lines(AS) by XBOOLE_0:def 7;
hence contradiction by Th16;
end;
assume a on A;
then [a,A] in the Inc of IncProjSp_of(AS) by INCSP_1:def 1;
hence contradiction by A1,A2,A3,A5,Def11;
end;
theorem Th28:
a=LDir(Y) & [X,1]=A & Y is being_line & X is being_line implies
(a on A iff Y '||' X)
proof
assume that
A1: a=LDir(Y) and
A2: [X,1]=A and
A3: Y is being_line and
A4: X is being_line;
A5: now
A6: now
given K such that
A7: K is being_line and
A8: [X,1]=[K,1] and
A9: LDir(Y) in the carrier of AS & LDir(Y) in K or LDir(Y) = LDir(K );
A10: K in AfLines(AS) by A7;
A11: X=K by A8,XTUPLE_0:1;
A12: now
assume LDir(Y)=LDir(K);
then
A13: Y in Class(LinesParallelity(AS),K) by A10,EQREL_1:23;
LDir(K)=Class(LinesParallelity(AS),K);
then consider K9 being Subset of AS such that
A14: Y=K9 and
A15: K9 is being_line and
A16: K '||' K9 by A7,A13,Th9;
K // K9 by A7,A15,A16,AFF_4:40;
hence Y '||' X by A7,A11,A14,A15,AFF_4:40;
end;
now
assume that
A17: LDir(Y) in the carrier of AS and
LDir(Y) in K;
a in Dir_of_Lines(AS) by A1,A3,Th14;
then (the carrier of AS) /\ Dir_of_Lines(AS) <> {} by A1,A17,
XBOOLE_0:def 4;
then (the carrier of AS) meets Dir_of_Lines(AS) by XBOOLE_0:def 7;
hence contradiction by Th16;
end;
hence Y '||' X by A9,A12;
end;
assume a on A;
then
A18: [a,A] in the Inc of IncProjSp_of(AS) by INCSP_1:def 1;
not ex K,X9 st K is being_line & X9 is being_plane & LDir(Y)=LDir(K)
& [X,1]=[PDir(X9),2] & K '||' X9 by XTUPLE_0:1;
hence Y '||' X by A1,A2,A18,A6,Def11;
end;
now
assume Y '||' X;
then
A19: X in LDir(Y) by A3,A4,Th9;
A20: LDir(X)=Class(LinesParallelity(AS),X);
Y in AfLines(AS) by A3;
then Class(LinesParallelity(AS),X)=Class(LinesParallelity(AS),Y) by A19,
EQREL_1:23;
then [a,A] in Proj_Inc(AS) by A1,A2,A4,A20,Def11;
hence a on A by INCSP_1:def 1;
end;
hence thesis by A5;
end;
theorem Th29:
a=LDir(Y) & A=[PDir(X),2] & Y is being_line & X is being_plane
implies (a on A iff Y '||' X)
proof
assume that
A1: a=LDir(Y) and
A2: A=[PDir(X),2] and
A3: Y is being_line and
A4: X is being_plane;
A5: now
A6: now
given K,X9 such that
A7: K is being_line and
A8: X9 is being_plane and
A9: LDir(Y)=LDir(K) and
A10: [PDir(X),2]=[PDir(X9),2] and
A11: K '||' X9;
A12: X9 in AfPlanes(AS) by A8;
A13: Class(PlanesParallelity(AS),X9)= PDir(X9);
PDir(X)=PDir(X9) by A10,XTUPLE_0:1;
then X in Class(PlanesParallelity(AS),X9) by A12,EQREL_1:23;
then
A14: ex X99 being Subset of AS st X=X99 & X99 is being_plane & X9 '||'
X99 by A8,A13,Th10;
K in AfLines(AS) by A7;
then
A15: Y in Class(LinesParallelity(AS),K) by A9,EQREL_1:23;
Class(LinesParallelity(AS),K)= LDir(K);
then consider K9 being Subset of AS such that
A16: Y=K9 and
A17: K9 is being_line and
A18: K '||' K9 by A7,A15,Th9;
K // K9 by A7,A17,A18,AFF_4:40;
then K9 '||' X9 by A11,AFF_4:56;
hence Y '||' X by A8,A16,A14,AFF_4:59,60;
end;
assume a on A;
then
A19: [a,A] in the Inc of IncProjSp_of(AS) by INCSP_1:def 1;
(ex K st K is being_line & [PDir(X),2]=[K,1] & (LDir(Y) in the carrier
of AS & LDir(Y) in K or LDir(Y) = LDir(K))) implies contradiction by XTUPLE_0:1
;
hence Y '||' X by A1,A2,A19,A6,Def11;
end;
now
assume Y '||' X;
then [LDir(Y),[PDir(X),2]] in Proj_Inc(AS) by A3,A4,Def11;
hence a on A by A1,A2,INCSP_1:def 1;
end;
hence thesis by A5;
end;
theorem Th30:
X is being_line & a=LDir(X) & A=[X,1] implies a on A
proof
assume that
A1: X is being_line and
A2: a=LDir(X) and
A3: A=[X,1];
X // X by A1,AFF_1:41;
then X '||' X by A1,AFF_4:40;
hence thesis by A1,A2,A3,Th28;
end;
theorem Th31:
X is being_line & Y is being_plane & X c= Y & a=LDir(X) & A=[
PDir(Y),2] implies a on A
proof
assume that
A1: X is being_line and
A2: Y is being_plane and
A3: X c= Y and
A4: a=LDir(X) and
A5: A=[PDir(Y),2];
X '||' Y by A1,A2,A3,AFF_4:42;
hence thesis by A1,A2,A4,A5,Th29;
end;
theorem Th32:
Y is being_plane & X c= Y & X9 // X & a=LDir(X9) & A=[PDir(Y),2]
implies a on A
proof
assume that
A1: Y is being_plane and
A2: X c= Y and
A3: X9 // X and
A4: a=LDir(X9) and
A5: A=[PDir(Y),2];
X is being_line by A3,AFF_1:36;
then
A6: X9 '||' Y by A1,A2,A3,AFF_4:42,56;
X9 is being_line by A3,AFF_1:36;
hence thesis by A1,A4,A5,A6,Th29;
end;
theorem
A=[PDir(X),2] & X is being_plane & a on A implies a is not Element of
AS by Th27;
theorem Th34:
A=[X,1] & X is being_line & p on A & p is not Element of AS implies p=LDir(X)
proof
assume that
A1: A=[X,1] and
A2: X is being_line and
A3: p on A and
A4: not p is Element of AS;
consider Xp being Subset of AS such that
A5: p=LDir(Xp) and
A6: Xp is being_line by A4,Th20;
Xp '||' X by A1,A2,A3,A5,A6,Th28;
hence thesis by A2,A5,A6,Th12;
end;
theorem Th35:
A=[X,1] & X is being_line & p on A & a on A & a<>p & not p is
Element of AS implies a is Element of AS
proof
assume that
A1: A=[X,1] and
A2: X is being_line and
A3: p on A and
A4: a on A and
A5: a<>p and
A6: not p is Element of AS;
assume not thesis;
then a=LDir(X) by A1,A2,A4,Th34;
hence contradiction by A1,A2,A3,A5,A6,Th34;
end;
theorem Th36:
for a being Element of the Points of ProjHorizon(AS),A being
Element of the Lines of ProjHorizon(AS) st a=LDir(X) & A=PDir(Y) & X is
being_line & Y is being_plane holds (a on A iff X '||' Y)
proof
let a be Element of the Points of ProjHorizon(AS),A be Element of the Lines
of ProjHorizon(AS) such that
A1: a=LDir(X) and
A2: A=PDir(Y) and
A3: X is being_line and
A4: Y is being_plane;
A5: now
assume a on A;
then [a,A] in the Inc of ProjHorizon(AS) by INCSP_1:def 1;
then consider X9,Y9 such that
A6: a=LDir(X9) and
A7: A=PDir(Y9) and
A8: X9 is being_line and
A9: Y9 is being_plane and
A10: X9 '||' Y9 by Def12;
X // X9 by A1,A3,A6,A8,Th11;
then
A11: X '||' Y9 by A10,AFF_4:56;
Y9 '||' Y by A2,A4,A7,A9,Th13;
hence X '||' Y by A9,A11,AFF_4:59,60;
end;
now
assume X '||' Y;
then [a,A] in Inc_of_Dir(AS) by A1,A2,A3,A4,Def12;
hence a on A by INCSP_1:def 1;
end;
hence thesis by A5;
end;
theorem Th37:
for a being Element of the Points of ProjHorizon(AS),a9 being
Element of the Points of IncProjSp_of(AS),A being Element of the Lines of
ProjHorizon(AS),A9 being LINE of IncProjSp_of(AS) st a9=a & A9=[A,2] holds (a
on A iff a9 on A9)
proof
let a be Element of the Points of ProjHorizon(AS),a9 be Element of the
Points of IncProjSp_of(AS),A be Element of the Lines of ProjHorizon(AS),A9 be
LINE of IncProjSp_of(AS) such that
A1: a9=a and
A2: A9=[A,2];
consider X such that
A3: a=LDir(X) and
A4: X is being_line by Th14;
consider Y such that
A5: A=PDir(Y) and
A6: Y is being_plane by Th15;
A7: now
assume a9 on A9;
then X '||' Y by A1,A2,A3,A4,A5,A6,Th29;
hence a on A by A3,A4,A5,A6,Th36;
end;
now
assume a on A;
then X '||' Y by A3,A4,A5,A6,Th36;
hence a9 on A9 by A1,A2,A3,A4,A5,A6,Th29;
end;
hence thesis by A7;
end;
reserve A,K,M,N,P,Q for LINE of IncProjSp_of(AS);
theorem Th38:
for a,b being Element of the Points of ProjHorizon(AS), A,K
being Element of the Lines of ProjHorizon(AS) st a on A & a on K & b on A & b
on K holds a=b or A=K
proof
let a,b be Element of the Points of ProjHorizon(AS), A,K be Element of the
Lines of ProjHorizon(AS) such that
A1: a on A and
A2: a on K and
A3: b on A and
A4: b on K;
consider Y9 such that
A5: b=LDir(Y9) and
A6: Y9 is being_line by Th14;
consider X9 such that
A7: K=PDir(X9) and
A8: X9 is being_plane by Th15;
A9: Y9 '||' X9 by A4,A5,A6,A7,A8,Th36;
consider Y such that
A10: a=LDir(Y) and
A11: Y is being_line by Th14;
assume a<>b;
then
A12: not Y // Y9 by A10,A11,A5,A6,Th11;
consider X such that
A13: A=PDir(X) and
A14: X is being_plane by Th15;
A15: Y9 '||' X by A3,A5,A6,A13,A14,Th36;
A16: Y '||' X9 by A2,A10,A11,A7,A8,Th36;
Y '||' X by A1,A10,A11,A13,A14,Th36;
then X '||' X9 by A11,A6,A14,A8,A12,A16,A15,A9,Th5;
hence thesis by A13,A14,A7,A8,Th13;
end;
theorem Th39:
for A being Element of the Lines of ProjHorizon(AS) ex a,b,c
being Element of the Points of ProjHorizon(AS) st a on A & b on A & c on A & a
<>b & b<>c & c <>a
proof
let A be Element of the Lines of ProjHorizon(AS);
consider X such that
A1: A=PDir(X) and
A2: X is being_plane by Th15;
consider x,y,z such that
A3: x in X and
A4: y in X and
A5: z in X and
A6: not LIN x,y,z by A2,AFF_4:34;
A7: y<>z by A6,AFF_1:7;
then
A8: Line(y,z) is being_line by AFF_1:def 3;
then
A9: Line(y,z) '||' X by A2,A4,A5,A7,AFF_4:19,42;
A10: z<>x by A6,AFF_1:7;
then
A11: Line(x,z) is being_line by AFF_1:def 3;
then
A12: Line(x,z) '||' X by A2,A3,A5,A10,AFF_4:19,42;
A13: x<>y by A6,AFF_1:7;
then
A14: Line(x,y) is being_line by AFF_1:def 3;
then reconsider
a=LDir(Line(x,y)),b=LDir(Line(y,z)),c =LDir(Line(x,z)) as Element
of the Points of ProjHorizon(AS) by A8,A11,Th14;
take a,b,c;
Line(x,y) '||' X by A2,A3,A4,A13,A14,AFF_4:19,42;
hence a on A & b on A & c on A by A1,A2,A14,A8,A11,A9,A12,Th36;
A15: x in Line(x,y) by AFF_1:15;
A16: z in Line(y,z) by AFF_1:15;
A17: y in Line(x,y) by AFF_1:15;
A18: y in Line(y,z) by AFF_1:15;
thus a<>b
proof
assume not thesis;
then Line(x,y) // Line(y,z) by A14,A8,Th11;
then z in Line(x,y) by A17,A18,A16,AFF_1:45;
hence contradiction by A6,A14,A15,A17,AFF_1:21;
end;
A19: z in Line(x,z) by AFF_1:15;
A20: x in Line(x,z) by AFF_1:15;
thus b<>c
proof
assume not thesis;
then Line(y,z) // Line(x,z) by A8,A11,Th11;
then x in Line(y,z) by A16,A20,A19,AFF_1:45;
hence contradiction by A6,A8,A18,A16,AFF_1:21;
end;
thus c <>a
proof
assume not thesis;
then Line(x,y) // Line(x,z) by A14,A11,Th11;
then z in Line(x,y) by A15,A20,A19,AFF_1:45;
hence contradiction by A6,A14,A15,A17,AFF_1:21;
end;
end;
theorem Th40:
for a,b being Element of the Points of ProjHorizon(AS) ex A
being Element of the Lines of ProjHorizon(AS) st a on A & b on A
proof
let a,b be Element of the Points of ProjHorizon(AS);
consider X such that
A1: a=LDir(X) and
A2: X is being_line by Th14;
consider X9 such that
A3: b=LDir(X9) and
A4: X9 is being_line by Th14;
consider x,y being Element of AS such that
A5: x in X9 and
y in X9 and
x<>y by A4,AFF_1:19;
A6: x in x*X by A2,AFF_4:def 3;
x*X is being_line by A2,AFF_4:27;
then consider Z such that
A7: X9 c= Z and
A8: x*X c= Z and
A9: Z is being_plane by A4,A5,A6,AFF_4:38;
A10: X9 '||' Z by A4,A7,A9,AFF_4:42;
reconsider A=PDir(Z) as Element of the Lines of ProjHorizon(AS) by A9,Th15;
take A;
X // x*X by A2,AFF_4:def 3;
then X '||' Z by A2,A8,A9,AFF_4:41;
hence thesis by A1,A2,A3,A4,A9,A10,Th36;
end;
Lm1: AS is not AffinPlane implies ex a being Element of the Points of
ProjHorizon(AS),A being Element of the Lines of ProjHorizon(AS) st not a on A
proof
set x = the Element of AS;
consider X such that
A1: x in X and
x in X and
x in X and
A2: X is being_plane by AFF_4:37;
reconsider A=PDir(X) as Element of the Lines of ProjHorizon(AS) by A2,Th15;
assume AS is not AffinPlane;
then consider t such that
A3: not t in X by A2,AFF_4:48;
set Y=Line(x,t);
A4: Y is being_line by A1,A3,AFF_1:def 3;
then reconsider a=LDir(Y) as Element of the Points of ProjHorizon(AS) by Th14
;
take a,A;
A5: t in Y by AFF_1:15;
A6: x in Y by AFF_1:15;
thus not a on A
proof
assume not thesis;
then Y '||' X by A2,A4,Th36;
then Y c= X by A1,A2,A4,A6,AFF_4:43;
hence contradiction by A3,A5;
end;
end;
Lm2: a on A & a on K & b on A & b on K implies a=b or A=K
proof
assume that
A1: a on A and
A2: a on K and
A3: b on A and
A4: b on K;
consider X such that
A5: A=[X,1] & X is being_line or A=[PDir(X),2] & X is being_plane by Th23;
consider X9 such that
A6: K=[X9,1] & X9 is being_line or K=[PDir(X9),2] & X9 is being_plane by Th23;
assume
A7: a<>b;
A8: now
given Y such that
A9: a=LDir(Y) and
A10: Y is being_line;
A11: now
given Y9 such that
A12: b=LDir(Y9) and
A13: Y9 is being_line;
A14: not Y // Y9 by A7,A9,A10,A12,A13,Th11;
A15: M=[Z,1] & Z is being_line implies not (a on M & b on M)
proof
assume that
A16: M=[Z,1] and
A17: Z is being_line;
assume
A18: not thesis;
then Y9 '||' Z by A12,A13,A16,A17,Th28;
then
A19: Y9 // Z by A13,A17,AFF_4:40;
Y '||' Z by A9,A10,A16,A17,A18,Th28;
then Y // Z by A10,A17,AFF_4:40;
then Y // Y9 by A19,AFF_1:44;
hence contradiction by A7,A9,A10,A12,A13,Th11;
end;
then
A20: Y9 '||' X by A1,A3,A5,A12,A13,Th29;
A21: Y9 '||' X9 by A2,A4,A6,A12,A13,A15,Th29;
A22: Y '||' X9 by A2,A4,A6,A9,A10,A15,Th29;
Y '||' X by A1,A3,A5,A9,A10,A15,Th29;
then X '||' X9 by A1,A2,A3,A4,A5,A6,A10,A13,A15,A14,A22,A20,A21,Th5;
hence thesis by A1,A2,A3,A4,A5,A6,A15,Th13;
end;
now
assume b is Element of AS;
then reconsider y=b as Element of AS;
A23: y in X9 by A4,A6,Th26,Th27;
A24: y=b;
then Y '||' X9 by A2,A4,A6,A9,A10,Th27,Th28;
then
A25: Y // X9 by A4,A6,A10,A24,Th27,AFF_4:40;
Y '||' X by A1,A3,A5,A9,A10,A24,Th27,Th28;
then Y // X by A3,A5,A10,A24,Th27,AFF_4:40;
then
A26: X // X9 by A25,AFF_1:44;
y in X by A3,A5,Th26,Th27;
hence thesis by A3,A4,A5,A6,A23,A26,Th27,AFF_1:45;
end;
hence thesis by A11,Th20;
end;
now
assume a is Element of AS;
then reconsider x=a as Element of AS;
A27: x=a;
A28: x in X9 by A2,A6,Th26,Th27;
A29: x in X by A1,A5,Th26,Th27;
A30: now
given Y such that
A31: b=LDir(Y) and
A32: Y is being_line;
Y '||' X9 by A2,A4,A6,A27,A31,A32,Th27,Th28;
then
A33: Y // X9 by A2,A6,A27,A32,Th27,AFF_4:40;
Y '||' X by A1,A3,A5,A27,A31,A32,Th27,Th28;
then Y // X by A1,A5,A27,A32,Th27,AFF_4:40;
then X // X9 by A33,AFF_1:44;
hence thesis by A1,A2,A5,A6,A29,A28,Th27,AFF_1:45;
end;
now
assume b is Element of AS;
then reconsider y=b as Element of AS;
A34: y in X9 by A4,A6,Th26,Th27;
y in X by A3,A5,Th26,Th27;
hence thesis by A1,A2,A7,A5,A6,A29,A28,A34,Th27,AFF_1:18;
end;
hence thesis by A30,Th20;
end;
hence thesis by A8,Th20;
end;
Lm3: ex a,b,c st a on A & b on A & c on A & a<>b & b<>c & c <>a
proof
consider X such that
A1: A=[X,1] & X is being_line or A=[PDir(X),2] & X is being_plane by Th23;
A2: now
assume that
A3: A=[PDir(X),2] and
A4: X is being_plane;
consider x,y,z such that
A5: x in X and
A6: y in X and
A7: z in X and
A8: not LIN x,y,z by A4,AFF_4:34;
A9: y<>z by A8,AFF_1:7;
then
A10: Line(y,z) is being_line by AFF_1:def 3;
then
A11: Line(y,z) '||' X by A4,A6,A7,A9,AFF_4:19,42;
A12: z<>x by A8,AFF_1:7;
then
A13: Line(x,z) is being_line by AFF_1:def 3;
then
A14: Line(x,z) '||' X by A4,A5,A7,A12,AFF_4:19,42;
A15: x<>y by A8,AFF_1:7;
then
A16: Line(x,y) is being_line by AFF_1:def 3;
then reconsider
a=LDir(Line(x,y)),b=LDir(Line(y,z)),c =LDir(Line(x,z)) as POINT
of IncProjSp_of(AS) by A10,A13,Th20;
take a,b,c;
Line(x,y) '||' X by A4,A5,A6,A15,A16,AFF_4:19,42;
hence a on A & b on A & c on A by A3,A4,A16,A10,A13,A11,A14,Th29;
A17: x in Line(x,y) by AFF_1:15;
A18: z in Line(y,z) by AFF_1:15;
A19: y in Line(x,y) by AFF_1:15;
A20: y in Line(y,z) by AFF_1:15;
thus a<>b
proof
assume not thesis;
then Line(x,y) // Line(y,z) by A16,A10,Th11;
then z in Line(x,y) by A19,A20,A18,AFF_1:45;
hence contradiction by A8,A16,A17,A19,AFF_1:21;
end;
A21: z in Line(x,z) by AFF_1:15;
A22: x in Line(x,z) by AFF_1:15;
thus b<>c
proof
assume not thesis;
then Line(y,z) // Line(x,z) by A10,A13,Th11;
then x in Line(y,z) by A18,A22,A21,AFF_1:45;
hence contradiction by A8,A10,A20,A18,AFF_1:21;
end;
thus c <>a
proof
assume not thesis;
then Line(x,y) // Line(x,z) by A16,A13,Th11;
then z in Line(x,y) by A17,A22,A21,AFF_1:45;
hence contradiction by A8,A16,A17,A19,AFF_1:21;
end;
end;
now
assume that
A23: A=[X,1] and
A24: X is being_line;
reconsider c =LDir(X) as POINT of IncProjSp_of(AS) by A24,Th20;
consider x,y such that
A25: x in X and
A26: y in X and
A27: x<>y by A24,AFF_1:19;
reconsider a=x,b=y as Element of the Points of IncProjSp_of(AS) by Th20;
take a,b,c;
X // X by A24,AFF_1:41;
then X '||' X by A24,AFF_4:40;
hence a on A & b on A & c on A by A23,A24,A25,A26,Th26,Th28;
thus a<>b by A27;
thus b<>c & c <>a
proof
assume
A28: not thesis;
c in Dir_of_Lines(AS) by A24,Th14;
then (the carrier of AS) /\ Dir_of_Lines(AS) <> {} by A28,XBOOLE_0:def 4;
then (the carrier of AS) meets Dir_of_Lines(AS) by XBOOLE_0:def 7;
hence contradiction by Th16;
end;
end;
hence thesis by A1,A2;
end;
Lm4: ex A st a on A & b on A
proof
A1: now
given X such that
A2: a=LDir(X) and
A3: X is being_line;
A4: now
given X9 such that
A5: b=LDir(X9) and
A6: X9 is being_line;
consider x,y being Element of AS such that
A7: x in X9 and
y in X9 and
x<>y by A6,AFF_1:19;
A8: x in x*X by A3,AFF_4:def 3;
x*X is being_line by A3,AFF_4:27;
then consider Z such that
A9: X9 c= Z and
A10: x*X c= Z and
A11: Z is being_plane by A6,A7,A8,AFF_4:38;
A12: X9 '||' Z by A6,A9,A11,AFF_4:42;
reconsider A=[PDir(Z),2] as LINE of IncProjSp_of(AS) by A11,Th23;
take A;
X // x*X by A3,AFF_4:def 3;
then X '||' Z by A3,A10,A11,AFF_4:41;
hence a on A & b on A by A2,A3,A5,A6,A11,A12,Th29;
end;
now
assume b is Element of AS;
then reconsider y=b as Element of AS;
A13: y*X is being_line by A3,AFF_4:27;
then reconsider A=[y*X,1] as LINE of IncProjSp_of(AS) by Th23;
take A;
X // y*X by A3,AFF_4:def 3;
then X '||' y*X by A3,A13,AFF_4:40;
hence a on A by A2,A3,A13,Th28;
y in y*X by A3,AFF_4:def 3;
hence b on A by A13,Th26;
end;
hence thesis by A4,Th20;
end;
now
assume a is Element of AS;
then reconsider x=a as Element of AS;
A14: now
given X9 such that
A15: b=LDir(X9) and
A16: X9 is being_line;
A17: x*X9 is being_line by A16,AFF_4:27;
then reconsider A=[x*X9,1] as LINE of IncProjSp_of(AS) by Th23;
take A;
x in x*X9 by A16,AFF_4:def 3;
hence a on A by A17,Th26;
X9 // x*X9 by A16,AFF_4:def 3;
then X9 '||' x*X9 by A16,A17,AFF_4:40;
hence b on A by A15,A16,A17,Th28;
end;
now
assume b is Element of AS;
then reconsider y=b as Element of AS;
consider Y such that
A18: x in Y and
A19: y in Y and
A20: Y is being_line by AFF_4:11;
reconsider A=[Y,1] as LINE of IncProjSp_of(AS) by A20,Th23;
take A;
thus a on A & b on A by A18,A19,A20,Th26;
end;
hence thesis by A14,Th20;
end;
hence thesis by A1,Th20;
end;
Lm5: AS is AffinPlane implies ex a st a on A & a on K
proof
consider X such that
A1: A=[X,1] & X is being_line or A=[PDir(X),2] & X is being_plane by Th23;
consider X9 such that
A2: K=[X9,1] & X9 is being_line or K=[PDir(X9),2] & X9 is being_plane by Th23;
assume
A3: AS is AffinPlane;
A4: now
assume that
A5: A=[X,1] and
A6: X is being_line;
A7: now
assume that
A8: K=[X9,1] and
A9: X9 is being_line;
A10: now
reconsider a=LDir(X),b=LDir(X9) as Element of the Points of
IncProjSp_of(AS) by A6,A9,Th20;
X9 // X9 by A9,AFF_1:41;
then
A11: X9 '||' X9 by A9,AFF_4:40;
assume X // X9;
then
A12: a=b by A6,A9,Th11;
take a;
X // X by A6,AFF_1:41;
then X '||' X by A6,AFF_4:40;
hence a on A & a on K by A5,A6,A8,A9,A12,A11,Th28;
end;
now
assume not X // X9;
then consider x such that
A13: x in X and
A14: x in X9 by A3,A6,A9,AFF_1:58;
reconsider a=x as Element of the Points of IncProjSp_of(AS) by Th20;
take a;
thus a on A & a on K by A5,A6,A8,A9,A13,A14,Th26;
end;
hence thesis by A10;
end;
now
X // X by A6,AFF_1:41;
then
A15: X '||' X by A6,AFF_4:40;
reconsider a=LDir(X) as Element of the Points of IncProjSp_of(AS) by A6
,Th20;
assume that
A16: K=[PDir(X9),2] and
A17: X9 is being_plane;
take a;
X9=the carrier of AS by A3,A17,Th2;
then X '||' X9 by A6,A17,AFF_4:42;
hence a on A & a on K by A5,A6,A16,A17,A15,Th28,Th29;
end;
hence thesis by A2,A7;
end;
now
assume that
A18: A=[PDir(X),2] and
A19: X is being_plane;
A20: X=the carrier of AS by A3,A19,Th2;
A21: now
assume that
A22: K=[X9,1] and
A23: X9 is being_line;
X9 // X9 by A23,AFF_1:41;
then
A24: X9 '||' X9 by A23,AFF_4:40;
reconsider a=LDir(X9) as POINT of IncProjSp_of(AS) by A23,Th20;
take a;
X9 '||' X by A19,A20,A23,AFF_4:42;
hence a on A & a on K by A18,A19,A22,A23,A24,Th28,Th29;
end;
now
consider a,b,c such that
A25: a on A and
b on A and
c on A and
a<>b and
b<>c and
c <>a by Lm3;
assume that
A26: K=[PDir(X9),2] and
A27: X9 is being_plane;
take a;
thus a on A & a on K by A3,A18,A19,A26,A27,A25,Th3;
end;
hence thesis by A2,A21;
end;
hence thesis by A1,A4;
end;
Lm6: ex a,A st not a on A
proof
consider x,y,z such that
A1: not LIN x,y,z by AFF_1:12;
y<>z by A1,AFF_1:7;
then
A2: Line(y,z) is being_line by AFF_1:def 3;
then reconsider A=[Line(y,z),1] as LINE of IncProjSp_of(AS) by Th23;
reconsider a=x as POINT of IncProjSp_of(AS) by Th20;
take a,A;
thus not a on A
proof
assume not thesis;
then
A3: x in Line(y,z) by Th26;
A4: z in Line(y,z) by AFF_1:15;
y in Line(y,z) by AFF_1:15;
hence contradiction by A1,A2,A3,A4,AFF_1:21;
end;
end;
theorem Th41:
for x,y being Element of the Points of ProjHorizon(AS), X being
Element of the Lines of IncProjSp_of(AS) st x<>y & [x,X] in the Inc of
IncProjSp_of(AS) & [y,X] in the Inc of IncProjSp_of(AS) ex Y being Element of
the Lines of ProjHorizon(AS) st X=[Y,2]
proof
let x,y be Element of the Points of ProjHorizon(AS), X be Element of the
Lines of IncProjSp_of(AS);
reconsider a=x,b=y as POINT of IncProjSp_of(AS) by Th22;
assume that
A1: x<>y and
A2: [x,X] in the Inc of IncProjSp_of(AS) and
A3: [y,X] in the Inc of IncProjSp_of(AS);
A4: b on X by A3,INCSP_1:def 1;
consider Y being Element of the Lines of ProjHorizon(AS) such that
A5: x on Y and
A6: y on Y by Th40;
reconsider A=[Y,2] as LINE of IncProjSp_of(AS) by Th25;
consider Z being Subset of AS such that
A7: Y=PDir(Z) and
A8: Z is being_plane by Th15;
consider X2 being Subset of AS such that
A9: y=LDir(X2) and
A10: X2 is being_line by Th14;
X2 '||' Z by A9,A10,A6,A7,A8,Th36;
then
A11: b on A by A9,A10,A7,A8,Th29;
take Y;
consider X1 being Subset of AS such that
A12: x=LDir(X1) and
A13: X1 is being_line by Th14;
X1 '||' Z by A12,A13,A5,A7,A8,Th36;
then
A14: a on A by A12,A13,A7,A8,Th29;
a on X by A2,INCSP_1:def 1;
hence thesis by A1,A4,A14,A11,Lm2;
end;
theorem Th42:
for x being POINT of IncProjSp_of(AS),X being Element of the
Lines of ProjHorizon(AS) st [x,[X,2]] in the Inc of IncProjSp_of(AS) holds x is
Element of the Points of ProjHorizon(AS)
proof
let x be POINT of IncProjSp_of(AS), X be Element of the Lines of ProjHorizon
(AS) such that
A1: [x,[X,2]] in the Inc of IncProjSp_of(AS);
reconsider A=[X,2] as LINE of IncProjSp_of(AS) by Th25;
A2: ex Y st X=PDir(Y) & Y is being_plane by Th15;
not x is Element of AS
proof
assume not thesis;
then reconsider a=x as Element of AS;
A3: a=x;
x on A by A1,INCSP_1:def 1;
hence contradiction by A2,A3,Th27;
end;
then ex Y9 st x=LDir(Y9) & Y9 is being_line by Th20;
hence thesis by Th14;
end;
Lm7: X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y
& A=[X,1] & K=[X9,1] & b on A & c on K & b on M & c on M & b<>c & M=[Y9,1] & Y9
is being_line implies Y9 c= Y
proof
assume that
A1: X is being_line and
A2: X9 is being_line and
A3: Y is being_plane and
A4: X c= Y and
A5: X9 c= Y and
A6: A=[X,1] and
A7: K=[X9,1] and
A8: b on A and
A9: c on K and
A10: b on M and
A11: c on M and
A12: b<>c and
A13: M=[Y9,1] and
A14: Y9 is being_line;
A15: now
assume b is Element of AS;
then reconsider y=b as Element of AS;
A16: now
given Xc being Subset of AS such that
A17: c =LDir(Xc) and
A18: Xc is being_line;
Xc '||' X9 by A2,A7,A9,A17,A18,Th28;
then
A19: Xc // X9 by A2,A18,AFF_4:40;
Xc '||' Y9 by A11,A13,A14,A17,A18,Th28;
then Xc // Y9 by A14,A18,AFF_4:40;
then
A20: X9 // Y9 by A19,AFF_1:44;
y in Y9 by A10,A13,Th26;
then
A21: Y9= y*X9 by A2,A20,AFF_4:def 3;
y in X by A6,A8,Th26;
hence thesis by A2,A3,A4,A5,A21,AFF_4:28;
end;
now
assume c is Element of AS;
then reconsider z=c as Element of AS;
A22: z in Y9 by A11,A13,Th26;
y in Y9 by A10,A13,Th26;
then
A23: Y9=Line(y,z) by A12,A14,A22,AFF_1:57;
A24: z in X9 by A7,A9,Th26;
y in X by A6,A8,Th26;
hence thesis by A3,A4,A5,A12,A24,A23,AFF_4:19;
end;
hence thesis by A16,Th20;
end;
now
given Xb being Subset of AS such that
A25: b=LDir(Xb) and
A26: Xb is being_line;
A27: now
assume c is Element of AS;
then reconsider y=c as Element of AS;
Xb '||' X by A1,A6,A8,A25,A26,Th28;
then
A28: Xb // X by A1,A26,AFF_4:40;
Xb '||' Y9 by A10,A13,A14,A25,A26,Th28;
then Xb // Y9 by A14,A26,AFF_4:40;
then
A29: X // Y9 by A28,AFF_1:44;
y in Y9 by A11,A13,Th26;
then
A30: Y9=y*X by A1,A29,AFF_4:def 3;
y in X9 by A7,A9,Th26;
hence thesis by A1,A3,A4,A5,A30,AFF_4:28;
end;
now
Xb '||' Y9 by A10,A13,A14,A25,A26,Th28;
then
A31: Xb // Y9 by A14,A26,AFF_4:40;
given Xc being Subset of AS such that
A32: c =LDir(Xc) and
A33: Xc is being_line;
Xc '||' Y9 by A11,A13,A14,A32,A33,Th28;
then Xc // Y9 by A14,A33,AFF_4:40;
then Xc // Xb by A31,AFF_1:44;
hence contradiction by A12,A25,A26,A32,A33,Th11;
end;
hence thesis by A27,Th20;
end;
hence thesis by A15,Th20;
end;
Lm8: X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y
& A=[X,1] & K=[X9,1] & b on A & c on K & b on M & c on M & b<>c & M=[PDir(Y9),2
] & Y9 is being_plane implies Y9 '||' Y & Y '||' Y9
proof
assume that
A1: X is being_line and
A2: X9 is being_line and
A3: Y is being_plane and
A4: X c= Y and
A5: X9 c= Y and
A6: A=[X,1] and
A7: K=[X9,1] and
A8: b on A and
A9: c on K and
A10: b on M and
A11: c on M and
A12: b<>c and
A13: M=[PDir(Y9),2] and
A14: Y9 is being_plane;
b is Element of AS or ex Xb being Subset of AS st b=LDir(Xb) & Xb is
being_line by Th20;
then consider Xb being Subset of AS such that
A15: b=LDir(Xb) and
A16: Xb is being_line by A10,A13,Th27;
A17: Xb '||' Y9 by A10,A13,A14,A15,A16,Th29;
Xb '||' X by A1,A6,A8,A15,A16,Th28;
then Xb // X by A1,A16,AFF_4:40;
then
A18: Xb '||' Y by A1,A3,A4,AFF_4:42,56;
c is Element of AS or ex Xc being Subset of AS st c =LDir(Xc) & Xc is
being_line by Th20;
then consider Xc being Subset of AS such that
A19: c =LDir(Xc) and
A20: Xc is being_line by A11,A13,Th27;
A21: Xc '||' Y9 by A11,A13,A14,A19,A20,Th29;
Xc '||' X9 by A2,A7,A9,A19,A20,Th28;
then Xc // X9 by A2,A20,AFF_4:40;
then
A22: Xc '||' Y by A2,A3,A5,AFF_4:42,56;
not Xb // Xc by A12,A15,A16,A19,A20,Th11;
hence thesis by A3,A14,A16,A20,A17,A21,A18,A22,Th5;
end;
theorem Th43:
Y is being_plane & X is being_line & X9 is being_line & X c= Y &
X9 c= Y & P=[X,1] & Q=[X9,1] implies ex q st q on P & q on Q
proof
assume that
A1: Y is being_plane and
A2: X is being_line and
A3: X9 is being_line and
A4: X c= Y and
A5: X9 c= Y and
A6: P=[X,1] and
A7: Q=[X9,1];
A8: now
reconsider q=LDir(X) as POINT of IncProjSp_of(AS) by A2,Th20;
assume
A9: X // X9;
take q;
LDir(X)=LDir(X9) by A2,A3,A9,Th11;
hence q on P & q on Q by A2,A3,A6,A7,Th30;
end;
now
given y such that
A10: y in X and
A11: y in X9;
reconsider q=y as Element of the Points of IncProjSp_of(AS) by Th20;
take q;
thus q on P & q on Q by A2,A3,A6,A7,A10,A11,Th26;
end;
hence thesis by A1,A2,A3,A4,A5,A8,AFF_4:22;
end;
Lm9: a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b
on Q & d on Q & not p on P & not p on Q & M<>N & p is Element of AS implies ex
q st q on P & q on Q
proof
assume that
A1: a on M and
A2: b on M and
A3: c on N and
A4: d on N and
A5: p on M and
A6: p on N and
A7: a on P and
A8: c on P and
A9: b on Q and
A10: d on Q and
A11: not p on P and
A12: not p on Q and
A13: M<>N and
A14: p is Element of AS;
A15: b<>d by A2,A4,A5,A6,A9,A12,A13,Lm2;
reconsider x=p as Element of AS by A14;
consider XM being Subset of AS such that
A16: M=[XM,1] & XM is being_line or M=[PDir(XM),2] & XM is being_plane by Th23;
consider XQ being Subset of AS such that
A17: Q=[XQ,1] & XQ is being_line or Q=[PDir(XQ),2] & XQ is being_plane by Th23;
consider XP being Subset of AS such that
A18: P=[XP,1] & XP is being_line or P=[PDir(XP),2] & XP is being_plane by Th23;
consider XN being Subset of AS such that
A19: N=[XN,1] & XN is being_line or N=[PDir(XN),2] & XN is being_plane by Th23;
A20: x in XM by A5,A16,Th26,Th27;
x in XN by A6,A19,Th26,Th27;
then consider Y such that
A21: XM c= Y and
A22: XN c= Y and
A23: Y is being_plane by A5,A6,A16,A19,A20,Th27,AFF_4:38;
A24: a<>c by A1,A3,A5,A6,A7,A11,A13,Lm2;
A25: now
assume that
A26: P=[PDir(XP),2] and
A27: XP is being_plane;
A28: Y '||' XP by A1,A3,A5,A6,A7,A8,A24,A16,A19,A20,A21,A22,A23,A26,A27,Lm8
,Th27;
A29: now
assume that
A30: Q=[XQ,1] and
A31: XQ is being_line;
reconsider q=LDir(XQ) as POINT of IncProjSp_of(AS) by A31,Th20;
take q;
XQ c= Y by A2,A4,A5,A6,A9,A10,A15,A16,A19,A20,A21,A22,A23,A30,A31,Lm7
,Th27;
then XQ '||' Y by A23,A31,AFF_4:42;
then XQ '||' XP by A23,A28,AFF_4:59,60;
hence q on P by A26,A27,A31,Th29;
thus q on Q by A30,A31,Th30;
end;
now
consider q,r,p9 such that
A32: q on P and
r on P and
p9 on P and
q<>r and
r<>p9 and
p9<>q by Lm3;
assume that
A33: Q=[PDir(XQ),2] and
A34: XQ is being_plane;
take q;
thus q on P by A32;
Y '||' XQ by A2,A4,A5,A6,A9,A10,A15,A16,A19,A20,A21,A22,A23,A33,A34,Lm8
,Th27;
then XP '||' XQ by A23,A27,A28,A34,AFF_4:61;
hence q on Q by A26,A27,A33,A34,A32,Th13;
end;
hence thesis by A17,A29;
end;
now
assume that
A35: P=[XP,1] and
A36: XP is being_line;
A37: XP c= Y by A1,A3,A5,A6,A7,A8,A24,A16,A19,A20,A21,A22,A23,A35,A36,Lm7,Th27;
A38: now
A39: XP '||' Y by A23,A36,A37,AFF_4:42;
reconsider q=LDir(XP) as POINT of IncProjSp_of(AS) by A36,Th20;
assume that
A40: Q=[PDir(XQ),2] and
A41: XQ is being_plane;
take q;
thus q on P by A35,A36,Th30;
Y '||' XQ by A2,A4,A5,A6,A9,A10,A15,A16,A19,A20,A21,A22,A23,A40,A41,Lm8
,Th27;
then XP '||' XQ by A23,A39,AFF_4:59,60;
hence q on Q by A36,A40,A41,Th29;
end;
now
assume that
A42: Q=[XQ,1] and
A43: XQ is being_line;
XQ c= Y by A2,A4,A5,A6,A9,A10,A15,A16,A19,A20,A21,A22,A23,A42,A43,Lm7
,Th27;
hence thesis by A23,A35,A36,A37,A42,A43,Th43;
end;
hence thesis by A17,A38;
end;
hence thesis by A18,A25;
end;
Lm10: a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P &
b on Q & d on Q & not p on P & not p on Q & M<>N & not p is Element of AS & a
is Element of AS implies ex q st q on P & q on Q
proof
assume that
A1: a on M and
A2: b on M and
A3: c on N and
A4: d on N and
A5: p on M and
A6: p on N and
A7: a on P and
A8: c on P and
A9: b on Q and
A10: d on Q and
A11: not p on P and
A12: not p on Q and
A13: M<>N and
A14: not p is Element of AS and
A15: a is Element of AS;
reconsider x=a as Element of AS by A15;
consider XM being Subset of AS such that
A16: M=[XM,1] & XM is being_line or M=[PDir(XM),2] & XM is being_plane by Th23;
A17: x in XM by A1,A16,Th26,Th27;
A18: b<>d by A2,A4,A5,A6,A9,A12,A13,Lm2;
consider XN being Subset of AS such that
A19: N=[XN,1] & XN is being_line or N=[PDir(XN),2] & XN is being_plane by Th23;
consider XP being Subset of AS such that
A20: P=[XP,1] & XP is being_line or P=[PDir(XP),2] & XP is being_plane by Th23;
A21: x=a;
then reconsider y=b as Element of AS by A1,A2,A5,A9,A12,A14,A16,Th27,Th35;
A22: y in XM by A2,A16,Th26,Th27;
consider X such that
A23: p=LDir(X) and
A24: X is being_line by A14,Th20;
consider XQ being Subset of AS such that
A25: Q=[XQ,1] & XQ is being_line or Q=[PDir(XQ),2] & XQ is being_plane by Th23;
A26: x in XP by A7,A20,Th26,Th27;
then consider Y such that
A27: XM c= Y and
A28: XP c= Y and
A29: Y is being_plane by A1,A7,A16,A20,A17,Th27,AFF_4:38;
A30: y=b;
A31: X '||' XM by A1,A5,A23,A24,A16,A21,Th27,Th28;
then
A32: X // XM by A1,A24,A16,A21,Th27,AFF_4:40;
A33: y in XQ by A9,A25,Th26,Th27;
A34: not XM // XP by A1,A5,A7,A11,A16,A20,A17,A26,Th27,AFF_1:45;
A35: now
A36: X // XM by A1,A24,A16,A21,A31,Th27,AFF_4:40;
assume that
A37: N=[XN,1] and
A38: XN is being_line;
X '||' XN by A6,A23,A24,A37,A38,Th28;
then X // XN by A24,A38,AFF_4:40;
then
A39: XM // XN by A36,AFF_1:44;
c is Element of AS
proof
assume not thesis;
then c =LDir( XN ) by A3,A37,A38,Th34;
then XN '||' XP by A7,A8,A20,A21,A38,Th27,Th28;
then XN // XP by A7,A20,A21,A38,Th27,AFF_4:40;
hence contradiction by A34,A39,AFF_1:44;
end;
then reconsider z=c as Element of AS;
z in XN by A3,A37,Th26;
then
A40: XN=z*XM by A1,A16,A21,A39,Th27,AFF_4:def 3;
A41: not XN // XQ
proof
assume XN // XQ;
then XM // XQ by A39,AFF_1:44;
hence contradiction by A2,A5,A9,A12,A16,A25,A33,A22,Th27,AFF_1:45;
end;
now
assume not d is Element of AS;
then consider Xd being Subset of AS such that
A42: d=LDir(Xd) and
A43: Xd is being_line by Th20;
Xd '||' XN by A4,A37,A38,A42,A43,Th28;
then
A44: Xd // XN by A38,A43,AFF_4:40;
Xd '||' XQ by A9,A10,A25,A30,A42,A43,Th27,Th28;
then Xd // XQ by A9,A25,A30,A43,Th27,AFF_4:40;
hence contradiction by A41,A44,AFF_1:44;
end;
then reconsider w=d as Element of AS;
w in XQ by A10,A25,Th26,Th27;
then
A45: XQ=Line(y,w) by A9,A18,A25,A33,Th27,AFF_1:57;
z in XP by A8,A20,Th26,Th27;
then
A46: XN c= Y by A1,A16,A21,A27,A28,A29,A40,Th27,AFF_4:28;
w in XN by A4,A37,Th26;
then XQ c= Y by A18,A27,A29,A22,A46,A45,AFF_4:19;
hence thesis by A7,A9,A20,A25,A21,A28,A29,A30,Th27,Th43;
end;
A47: XP '||' Y by A7,A20,A21,A28,A29,Th27,AFF_4:42;
A48: XM '||' Y by A1,A16,A21,A27,A29,Th27,AFF_4:42;
now
assume that
A49: N=[PDir(XN),2] and
A50: XN is being_plane;
c is not Element of AS by A3,A49,Th27;
then c =LDir(XP) by A7,A8,A20,A21,Th27,Th34;
then
A51: XP '||' XN by A3,A7,A20,A21,A49,A50,Th27,Th29;
d is not Element of AS by A4,A49,Th27;
then d=LDir(XQ) by A9,A10,A25,A30,Th27,Th34;
then
A52: XQ '||' XN by A4,A9,A25,A30,A49,A50,Th27,Th29;
X '||' XN by A6,A23,A24,A49,A50,Th29;
then XM '||' XN by A32,AFF_4:56;
then XN '||' Y by A1,A5,A7,A11,A16,A20,A17,A26,A29,A48,A47,A50,A51,Th5,Th27
,AFF_1:45;
then XQ '||' Y by A50,A52,AFF_4:59,60;
then XQ c= Y by A9,A25,A27,A29,A33,A22,Th27,AFF_4:43;
hence thesis by A7,A9,A20,A25,A21,A28,A29,A30,Th27,Th43;
end;
hence thesis by A19,A35;
end;
Lm11: a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P &
b on Q & d on Q & not p on P & not p on Q & M<>N & not p is Element of AS & (a
is Element of AS or b is Element of AS or c is Element of AS or d is Element of
AS) implies ex q st q on P & q on Q
proof
assume that
A1: a on M and
A2: b on M and
A3: c on N and
A4: d on N and
A5: p on M and
A6: p on N and
A7: a on P and
A8: c on P and
A9: b on Q and
A10: d on Q and
A11: not p on P and
A12: not p on Q and
A13: M<>N and
A14: not p is Element of AS and
A15: a is Element of AS or b is Element of AS or c is Element of AS or d
is Element of AS;
now
assume b is Element of AS or d is Element of AS;
then
ex q st q on Q & q on P by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14
,Lm10;
hence thesis;
end;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,A15,Lm10;
end;
Lm12: a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P &
b on Q & d on Q & not p on P & not p on Q & M<>N implies ex q st q on P & q on
Q
proof
assume that
A1: a on M and
A2: b on M and
A3: c on N and
A4: d on N and
A5: p on M and
A6: p on N and
A7: a on P and
A8: c on P and
A9: b on Q and
A10: d on Q and
A11: not p on P and
A12: not p on Q and
A13: M<>N;
now
assume
A14: not p is Element of AS;
now
A15: b<>d by A2,A4,A5,A6,A9,A12,A13,Lm2;
set x = the Element of AS;
assume that
A16: not a is Element of AS and
A17: not b is Element of AS and
A18: not c is Element of AS and
A19: not d is Element of AS;
consider Xa being Subset of AS such that
A20: a=LDir(Xa) and
A21: Xa is being_line by A16,Th20;
consider Xc being Subset of AS such that
A22: c =LDir(Xc) and
A23: Xc is being_line by A18,Th20;
consider Xb being Subset of AS such that
A24: b=LDir(Xb) and
A25: Xb is being_line by A17,Th20;
consider Xd being Subset of AS such that
A26: d=LDir(Xd) and
A27: Xd is being_line by A19,Th20;
consider Xp being Subset of AS such that
A28: p=LDir(Xp) and
A29: Xp is being_line by A14,Th20;
set Xa9=x*Xa,Xb9=x*Xb,Xc9=x*Xc,Xd9=x*Xd,Xp9=x*Xp;
consider y such that
A30: x<>y and
A31: y in Xa9 by A21,AFF_1:20,AFF_4:27;
A32: Xp // Xp9 by A29,AFF_4:def 3;
consider t such that
A33: x<>t and
A34: t in Xc9 by A23,AFF_1:20,AFF_4:27;
set Y1=y*Xp9,Y2=t*Xp9;
A35: Xp9 is being_line by A29,AFF_4:27;
then
A36: Y1 is being_line by AFF_4:27;
A37: Y2 is being_line by A35,AFF_4:27;
A38: Xb // Xb9 by A25,AFF_4:def 3;
A39: Xd9 is being_line by A27,AFF_4:27;
A40: Xd // Xd9 by A27,AFF_4:def 3;
A41: x in Xc9 by A23,AFF_4:def 3;
A42: x in Xb9 by A25,AFF_4:def 3;
A43: Xb9 is being_line by A25,AFF_4:27;
A44: x in Xd9 by A27,AFF_4:def 3;
then consider XQ being Subset of AS such that
A45: Xb9 c= XQ and
A46: Xd9 c= XQ and
A47: XQ is being_plane by A43,A39,A42,AFF_4:38;
A48: Xa9 is being_line by A21,AFF_4:27;
A49: Xp9 // Y2 by A35,AFF_4:def 3;
A50: not Xd9 // Y2
proof
assume Xd9 // Y2;
then Xd // Y2 by A40,AFF_1:44;
then Xd // Xp9 by A49,AFF_1:44;
then Xd // Xp by A32,AFF_1:44;
hence contradiction by A10,A12,A28,A29,A26,A27,Th11;
end;
A51: Xp9 // Y1 by A35,AFF_4:def 3;
A52: not Xb9 // Y1
proof
assume Xb9 // Y1;
then Xb // Y1 by A38,AFF_1:44;
then Xb // Xp9 by A51,AFF_1:44;
then Xb // Xp by A32,AFF_1:44;
hence contradiction by A9,A12,A28,A29,A24,A25,Th11;
end;
A53: x in Xa9 by A21,AFF_4:def 3;
A54: Xc9 is being_line by A23,AFF_4:27;
then consider XP being Subset of AS such that
A55: Xa9 c= XP and
A56: Xc9 c= XP and
A57: XP is being_plane by A48,A53,A41,AFF_4:38;
A58: x in Xp9 by A29,AFF_4:def 3;
then consider X2 being Subset of AS such that
A59: Xc9 c= X2 and
A60: Xp9 c= X2 and
A61: X2 is being_plane by A54,A35,A41,AFF_4:38;
A62: Xc // Xc9 by A23,AFF_4:def 3;
N=[PDir(X2),2]
proof
reconsider N9=[PDir(X2),2] as Element of the Lines of IncProjSp_of(AS)
by A61,Th23;
A63: c on N9 by A22,A62,A59,A61,Th32;
p on N9 by A28,A32,A60,A61,Th32;
hence thesis by A3,A6,A8,A11,A63,Lm2;
end;
then Xd '||' X2 by A4,A26,A27,A61,Th29;
then
A64: Xd9 c= X2 by A39,A41,A44,A40,A59,A61,AFF_4:43,56;
consider X1 being Subset of the carrier of AS such that
A65: Xa9 c= X1 and
A66: Xp9 c= X1 and
A67: X1 is being_plane by A48,A35,A53,A58,AFF_4:38;
A68: Xa // Xa9 by A21,AFF_4:def 3;
M=[PDir(X1),2]
proof
reconsider M9=[PDir(X1),2] as Element of the Lines of IncProjSp_of(AS)
by A67,Th23;
A69: a on M9 by A20,A68,A65,A67,Th32;
p on M9 by A28,A32,A66,A67,Th32;
hence thesis by A1,A5,A7,A11,A69,Lm2;
end;
then Xb '||' X1 by A2,A24,A25,A67,Th29;
then
A70: Xb9 c= X1 by A43,A53,A42,A38,A65,A67,AFF_4:43,56;
Y1 c= X1 by A29,A31,A65,A66,A67,AFF_4:27,28;
then consider z such that
A71: z in Xb9 and
A72: z in Y1 by A43,A36,A67,A70,A52,AFF_4:22;
Y2 c= X2 by A29,A34,A59,A60,A61,AFF_4:27,28;
then consider u such that
A73: u in Xd9 and
A74: u in Y2 by A39,A37,A61,A64,A50,AFF_4:22;
set AC=Line(y,t),BD=Line(z,u);
A75: y in AC by AFF_1:15;
A76: y in Y1 by A35,AFF_4:def 3;
A77: x<>z
proof
assume
A78: not thesis;
a = LDir(Xa9) by A20,A21,A48,A68,Th11
.= LDir(Y1) by A48,A53,A30,A31,A36,A76,A72,A78,AFF_1:18
.= LDir(Xp9) by A35,A36,A51,Th11
.= p by A28,A29,A35,A32,Th11;
hence contradiction by A7,A11;
end;
A79: z<>u
proof
assume
A80: not thesis;
b= LDir(Xb9) by A24,A25,A43,A38,Th11
.= LDir(Xd9) by A43,A39,A42,A44,A71,A73,A77,A80,AFF_1:18
.= d by A26,A27,A39,A40,Th11;
hence contradiction by A2,A4,A5,A6,A9,A12,A13,Lm2;
end;
then
A81: BD is being_line by AFF_1:def 3;
A82: Xa9<>Xc9
proof
assume Xa9=Xc9;
then a=LDir(Xc9) by A20,A21,A48,A68,Th11
.= c by A22,A23,A54,A62,Th11;
hence contradiction by A1,A3,A5,A6,A7,A11,A13,Lm2;
end;
then
A83: y<>t by A48,A54,A53,A41,A30,A31,A34,AFF_1:18;
then
A84: AC is being_line by AFF_1:def 3;
A85: BD c= XQ by A71,A73,A79,A45,A46,A47,AFF_4:19;
A86: t in AC by AFF_1:15;
Y1 // Y2 by A51,A49,AFF_1:44;
then consider X3 being Subset of AS such that
A87: Y1 c= X3 and
A88: Y2 c= X3 and
A89: X3 is being_plane by AFF_4:39;
A90: BD c= X3 by A87,A88,A89,A72,A74,A79,AFF_4:19;
A91: a<>c by A1,A3,A5,A6,A7,A11,A13,Lm2;
A92: P=[PDir(XP),2] & Q=[PDir(XQ),2]
proof
reconsider P9=[PDir(XP),2], Q9=[PDir(XQ),2] as LINE of IncProjSp_of(AS
) by A57,A47,Th23;
A93: c on P9 by A22,A62,A56,A57,Th32;
A94: b on Q9 by A24,A38,A45,A47,Th32;
A95: d on Q9 by A26,A40,A46,A47,Th32;
a on P9 by A20,A68,A55,A57,Th32;
hence thesis by A7,A8,A9,A10,A91,A15,A93,A94,A95,Lm2;
end;
A96: now
reconsider q=LDir(AC),q9=LDir(BD) as Element of the Points of
IncProjSp_of(AS) by A84,A81,Th20;
assume
A97: AC // BD;
take q;
q=q9 by A84,A81,A97,Th11;
hence q on P & q on Q by A31,A34,A71,A73,A83,A79,A84,A81,A55,A56,A57
,A45,A46,A47,A92,Th31,AFF_4:19;
end;
A98: AC c= XP by A31,A34,A83,A55,A56,A57,AFF_4:19;
A99: now
given w such that
A100: w in AC and
A101: w in BD;
set R=Line(x,w);
A102: x<>w
proof
assume
A103: x=w;
then Xa9=AC by A48,A53,A30,A31,A84,A75,A100,AFF_1:18;
hence contradiction by A54,A41,A33,A34,A82,A84,A86,A100,A103,AFF_1:18
;
end;
then
A104: R is being_line by AFF_1:def 3;
then reconsider q=LDir(R) as POINT of IncProjSp_of(AS) by Th20;
take q;
thus q on P & q on Q by A53,A42,A55,A57,A45,A47,A92,A98,A85,A100,A101
,A102,A104,Th31,AFF_4:19;
end;
t in Y2 by A35,AFF_4:def 3;
then AC c= X3 by A76,A87,A88,A89,A83,AFF_4:19;
hence thesis by A89,A84,A81,A90,A96,A99,AFF_4:22;
end;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,Lm11;
end;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,Lm9;
end;
theorem Th44:
for a,b,c,d,p being Element of the Points of ProjHorizon(AS),M,N
,P,Q being Element of the Lines of ProjHorizon(AS) st a on M & b on M & c on N
& d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P &
not p on Q & M<>N ex q being Element of the Points of ProjHorizon(AS) st q on P
& q on Q
proof
let a,b,c,d,p be Element of the Points of ProjHorizon(AS),M,N,P,Q be Element
of the Lines of ProjHorizon(AS) such that
A1: a on M and
A2: b on M and
A3: c on N and
A4: d on N and
A5: p on M and
A6: p on N and
A7: a on P and
A8: c on P and
A9: b on Q and
A10: d on Q and
A11: not p on P and
A12: not p on Q and
A13: M<>N;
reconsider M9=[M,2],N9=[N,2],P9=[P,2],Q9=[Q,2] as LINE of IncProjSp_of(AS)
by Th25;
reconsider a9=a,b9=b,c9=c,d9=d,p9=p as POINT of IncProjSp_of(AS) by Th22;
A14: b9 on M9 by A2,Th37;
A15: M9<>N9
proof
assume M9=N9;
then M = [N,2]`1
.= N;
hence contradiction by A13;
end;
A16: d9 on N9 by A4,Th37;
A17: c9 on N9 by A3,Th37;
A18: c9 on P9 by A8,Th37;
A19: a9 on P9 by A7,Th37;
A20: p9 on N9 by A6,Th37;
A21: p9 on M9 by A5,Th37;
A22: not p9 on Q9 by A12,Th37;
A23: not p9 on P9 by A11,Th37;
A24: d9 on Q9 by A10,Th37;
A25: b9 on Q9 by A9,Th37;
a9 on M9 by A1,Th37;
then consider q9 being POINT of IncProjSp_of(AS) such that
A26: q9 on P9 and
A27: q9 on Q9 by A14,A17,A16,A21,A20,A19,A18,A25,A24,A23,A22,A15,Lm12;
[q9,[P,2]] in the Inc of IncProjSp_of(AS) by A26,INCSP_1:def 1;
then reconsider q=q9 as Element of the Points of ProjHorizon(AS) by Th42;
take q;
thus thesis by A26,A27,Th37;
end;
registration
let AS;
cluster IncProjSp_of(AS) -> partial linear up-2-dimensional up-3-rank
Vebleian;
correctness
proof
set XX = IncProjSp_of(AS);
A1: for a,b being POINT of XX ex A being LINE of XX st a on A & b on A by Lm4;
A2: ex a being POINT of XX, A being LINE of XX st not a on A by Lm6;
A3: for A being LINE of XX ex a,b,c being POINT of XX st a<>b & b<>c & c
<>a & a on A & b on A & c on A
proof
let A be LINE of XX;
consider a,b,c being POINT of XX such that
A4: a on A and
A5: b on A and
A6: c on A and
A7: a<>b and
A8: b<>c and
A9: c <>a by Lm3;
take a,b,c;
thus thesis by A4,A5,A6,A7,A8,A9;
end;
A10: for a,b,c,d,p,q being POINT of XX, M,N,P,Q being LINE of XX st a on M
& b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on
Q & not p on P & not p on Q & M<>N holds ex q being POINT of XX st q on P & q
on Q by Lm12;
for a,b being POINT of XX, A,K being LINE of XX st a on A & b on A & a
on K & b on K holds a=b or A=K by Lm2;
hence thesis by A1,A2,A3,A10,INCPROJ:def 4,def 5,def 6,def 7,def 8;
end;
end;
registration
cluster strict 2-dimensional for IncProjSp;
existence
proof
set AS = the AffinPlane;
set XX=IncProjSp_of(AS);
for A,K being LINE of XX ex a being POINT of XX st a on A & a on K by Lm5;
then XX is 2-dimensional IncProjSp by INCPROJ:def 9;
hence thesis;
end;
end;
registration
let AS be AffinPlane;
cluster IncProjSp_of(AS) -> 2-dimensional;
correctness
proof
set XX=IncProjSp_of(AS);
for A,K being LINE of XX ex a being Element of the Points of XX st a
on A & a on K by Lm5;
hence thesis by INCPROJ:def 9;
end;
end;
theorem
IncProjSp_of(AS) is 2-dimensional implies AS is AffinPlane
proof
set x = the Element of AS;
assume
A1: IncProjSp_of(AS) is 2-dimensional;
consider X such that
A2: x in X and
x in X and
x in X and
A3: X is being_plane by AFF_4:37;
assume AS is not AffinPlane;
then consider z such that
A4: not z in X by A3,AFF_4:48;
set Y=Line(x,z);
A5: Y is being_line by A2,A4,AFF_1:def 3;
then reconsider A=[PDir(X),2],K=[Y,1] as LINE of IncProjSp_of(AS) by A3,Th23;
consider a being POINT of IncProjSp_of(AS) such that
A6: a on A and
A7: a on K by A1,INCPROJ:def 9;
not a is Element of AS by A6,Th27;
then consider Y9 such that
A8: a=LDir(Y9) and
A9: Y9 is being_line by Th20;
Y9 '||' Y by A5,A7,A8,A9,Th28;
then
A10: Y9 // Y by A5,A9,AFF_4:40;
A11: z in Y by AFF_1:15;
A12: x in Y by AFF_1:15;
Y9 '||' X by A3,A6,A8,A9,Th29;
then Y c= X by A2,A3,A5,A12,A10,AFF_4:43,56;
hence contradiction by A4,A11;
end;
theorem
AS is not AffinPlane implies ProjHorizon(AS) is IncProjSp
proof
set XX = ProjHorizon(AS);
A1: for a,b being Element of the Points of XX ex A being Element of the
Lines of XX st a on A & b on A by Th40;
A2: for A being Element of the Lines of XX ex a,b,c being Element of the
Points of XX st a<>b & b<>c & c <>a & a on A & b on A & c on A
proof
let A be Element of the Lines of XX;
consider a,b,c being Element of the Points of XX such that
A3: a on A and
A4: b on A and
A5: c on A and
A6: a<>b and
A7: b<>c and
A8: c <>a by Th39;
take a,b,c;
thus thesis by A3,A4,A5,A6,A7,A8;
end;
assume AS is not AffinPlane;
then
A9: ex a being Element of the Points of XX, A being Element of the Lines of
XX st not a on A by Lm1;
A10: for a,b,c,d,p,q being Element of the Points of XX, M,N,P,Q being
Element of the Lines of XX st a on M & b on M & c on N & d on N & p on M & p on
N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M<>N holds ex
q being Element of the Points of XX st q on P & q on Q by Th44;
for a,b being Element of the Points of XX, A,K being Element of the
Lines of XX st a on A & b on A & a on K & b on K holds a=b or A=K by Th38;
hence thesis by A1,A9,A2,A10,INCPROJ:def 4,def 5,def 6,def 7,def 8;
end;
theorem
ProjHorizon(AS) is IncProjSp implies AS is not AffinPlane
proof
set XX=ProjHorizon(AS);
assume ProjHorizon(AS) is IncProjSp;
then consider
a being Element of the Points of XX, A being Element of the Lines
of XX such that
A1: not a on A by INCPROJ:def 6;
consider X such that
A2: a=LDir(X) and
A3: X is being_line by Th14;
consider Y such that
A4: A=PDir(Y) and
A5: Y is being_plane by Th15;
assume AS is AffinPlane;
then Y = the carrier of AS by A5,Th2;
then X '||' Y by A3,A5,AFF_4:42;
hence contradiction by A1,A2,A3,A4,A5,Th36;
end;
theorem Th48:
for M,N being Subset of AS, o,a,b,c,a9,b9,c9 being Element
of AS st M is being_line & N is being_line & M<>N & o in M & o in N
& o<>b & o<>b9 & o<>c9 & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9
// b,a9 & b,c9 // c,b9 & (a=b or b=c or a=c) holds a,c9 // c,a9
proof
let M,N be Subset of AS, o,a,b,c,a9,b9,c9 be Element of AS
such that
A1: M is being_line and
A2: N is being_line and
A3: M<>N and
A4: o in M and
A5: o in N and
A6: o<>b and
A7: o<>b9 and
A8: o<>c9 and
A9: b in M and
A10: c in M and
A11: a9 in N and
A12: b9 in N and
A13: c9 in N and
A14: a,b9 // b,a9 and
A15: b,c9 // c,b9 and
A16: a=b or b=c or a=c;
A17: c <>b9 by A1,A2,A3,A4,A5,A7,A10,A12,AFF_1:18;
now
assume
A18: a=c;
then b,c9 // b,a9 by A14,A15,A17,AFF_1:5;
then a9=c9 by A1,A2,A3,A4,A5,A6,A8,A9,A11,A13,AFF_4:9;
hence thesis by A18,AFF_1:2;
end;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A11,A12,A13,A14,A15,A16,AFF_4:9;
end;
theorem
IncProjSp_of(AS) is Pappian implies AS is Pappian
proof
set XX = IncProjSp_of(AS);
assume
A1: IncProjSp_of(AS) is Pappian;
for M,N being Subset of AS, o,a,b,c,a9,b9,c9 being Element
of AS st M is being_line & N is being_line & M<>N & o in M & o in N & o
<>a & o<>a9 & o<>b & o<>b9 & o<>c & o<>c9 & a in M & b in M & c in M & a9 in N
& b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds a,c9 // c,a9
proof
let M,N be Subset of AS, o,a,b,c,a9,b9,c9 be Element of AS
such that
A2: M is being_line and
A3: N is being_line and
A4: M<>N and
A5: o in M and
A6: o in N and
A7: o<>a and
A8: o<>a9 and
A9: o<>b and
A10: o<>b9 and
A11: o<>c and
A12: o<>c9 and
A13: a in M and
A14: b in M and
A15: c in M and
A16: a9 in N and
A17: b9 in N and
A18: c9 in N and
A19: a,b9 // b,a9 and
A20: b,c9 // c,b9;
A21: b<>c9 by A2,A3,A4,A5,A6,A9,A14,A18,AFF_1:18;
then
A22: Line(b,c9) is being_line by AFF_1:def 3;
c <>a9 by A2,A3,A4,A5,A6,A8,A15,A16,AFF_1:18;
then
A23: Line(c,a9) is being_line by AFF_1:def 3;
A24: b<>a9 by A2,A3,A4,A5,A6,A8,A14,A16,AFF_1:18;
then
A25: Line(b,a9) is being_line by AFF_1:def 3;
A26: c <>b9 by A2,A3,A4,A5,A6,A10,A15,A17,AFF_1:18;
then
A27: Line(c,b9) is being_line by AFF_1:def 3;
reconsider A3=[M,1],B3=[N,1] as Element of the Lines of XX by A2,A3,Th23;
reconsider p=o,a1=a9,a2=c9,a3=b9,b1=a,b2=c,b3=b as Element of the Points
of XX by Th20;
A28: p on A3 by A2,A5,Th26;
A29: a<>b9 by A2,A3,A4,A5,A6,A7,A13,A17,AFF_1:18;
then
A30: Line(a,b9) is being_line by AFF_1:def 3;
then reconsider c1=LDir(Line(b,c9)),c2=LDir(Line(a,b9)) as Element of the
Points of XX by A22,Th20;
A31: b1 on A3 by A2,A13,Th26;
a<>c9 by A2,A3,A4,A5,A6,A7,A13,A18,AFF_1:18;
then
A32: Line(a,c9) is being_line by AFF_1:def 3;
then reconsider
A1=[Line(b,c9),1],A2=[Line(b,a9),1],B1=[Line(a,b9),1], B2=[Line
(c,b9),1],C1=[Line(c,a9),1],C2=[Line(a,c9),1] as Element of the Lines of XX by
A30,A25,A22,A27,A23,Th23;
A33: c2 on B1 by A30,Th30;
A34: b3 on A3 by A2,A14,Th26;
A35: b2 on A3 by A2,A15,Th26;
consider Y such that
A36: M c= Y and
A37: N c= Y and
A38: Y is being_plane by A2,A3,A5,A6,AFF_4:38;
reconsider C39=[PDir(Y),2] as Element of the Lines of XX by A38,Th23;
A39: c1 on C39 by A14,A18,A36,A37,A38,A21,A22,Th31,AFF_4:19;
A40: c2 on C39 by A13,A17,A36,A37,A38,A29,A30,Th31,AFF_4:19;
A41: a1 on B3 by A3,A16,Th26;
A42: a3 on B3 by A3,A17,Th26;
A43: p on B3 by A3,A6,Th26;
b9 in Line(a,b9) by AFF_1:15;
then
A44: a3 on B1 by A30,Th26;
a in Line(a,b9) by AFF_1:15;
then
A45: b1 on B1 by A30,Th26;
A46: c in Line(c,a9) by AFF_1:15;
then
A47: b2 on C1 by A23,Th26;
Line(b,c9) // Line(c,b9) by A20,A21,A26,AFF_1:37;
then Line(b,c9) '||' Line(c,b9) by A22,A27,AFF_4:40;
then
A48: c1 on B2 by A22,A27,Th28;
A49: c9 in Line(a,c9) by AFF_1:15;
then
A50: a2 on C2 by A32,Th26;
b9 in Line(c,b9) by AFF_1:15;
then
A51: a3 on B2 by A27,Th26;
c in Line(c,b9) by AFF_1:15;
then
A52: b2 on B2 by A27,Th26;
c9 in Line(b,c9) by AFF_1:15;
then
A53: a2 on A1 by A22,Th26;
b in Line(b,c9) by AFF_1:15;
then
A54: b3 on A1 by A22,Th26;
A55: a2 on B3 by A3,A18,Th26;
Line(a,b9) // Line(b,a9) by A19,A29,A24,AFF_1:37;
then Line(a,b9) '||' Line(b,a9) by A30,A25,AFF_4:40;
then
A56: c2 on A2 by A30,A25,Th28;
A57: a in Line(a,c9) by AFF_1:15;
then
A58: b1 on C2 by A32,Th26;
a9 in Line(b,a9) by AFF_1:15;
then
A59: a1 on A2 by A25,Th26;
b in Line(b,a9) by AFF_1:15;
then
A60: b3 on A2 by A25,Th26;
A61: a9 in Line(c,a9) by AFF_1:15;
then
A62: a1 on C1 by A23,Th26;
A63: c1 on A1 by A22,Th30;
now
A64: A3<>B3
proof
assume A3=B3;
then M=[N,1]`1
.= N;
hence contradiction by A4;
end;
not p on C1 & not p on C2
proof
assume p on C1 or p on C2;
then a1 on A3 or a2 on A3 by A7,A11,A28,A31,A35,A58,A50,A47,A62,Lm2;
hence contradiction by A8,A12,A28,A43,A41,A55,A64,INCPROJ:def 4;
end;
then consider c3 being Element of the Points of XX such that
A65: c3 on C1 and
A66: c3 on C2 by A28,A31,A35,A43,A41,A55,A58,A50,A47,A62,A64,INCPROJ:def 8;
A67: {a2,b1,c3} on C2 by A58,A50,A66,INCSP_1:2;
A68: {a1,b3,c2} on A2 by A60,A59,A56,INCSP_1:2;
A69: {a3,b1,c2} on B1 by A45,A44,A33,INCSP_1:2;
assume that
A70: b1<>b2 and
A71: b2<>b3 and
A72: b3<>b1;
A73: p,b1,b2,b3 are_mutually_distinct by A7,A9,A11,A70,A71,A72,ZFMISC_1:def 6
;
a1<>a2 & a2<>a3 & a1<>a3
proof
A74: now
assume a9=c9;
then a,b9 // c,b9 by A19,A20,A24,AFF_1:5;
hence contradiction by A2,A3,A4,A5,A6,A7,A10,A13,A15,A17,A70,AFF_4:9;
end;
assume not thesis;
hence contradiction by A2,A3,A4,A5,A6,A7,A9,A10,A13,A14,A15,A17,A19,A20
,A71,A72,A74,AFF_4:9;
end;
then
A75: p,a1,a2,a3 are_mutually_distinct by A8,A10,A12,ZFMISC_1:def 6;
A76: {a1,a2,a3} on B3 by A41,A55,A42,INCSP_1:2;
A77: {b1,b2,b3} on A3 by A31,A35,A34,INCSP_1:2;
A78: {a3,b2,c1} on B2 by A51,A52,A48,INCSP_1:2;
A79: {a2,b3,c1} on A1 by A53,A54,A63,INCSP_1:2;
A80: p on B3 by A3,A6,Th26;
A81: p on A3 by A2,A5,Th26;
A82: {c1,c2} on C39 by A39,A40,INCSP_1:1;
{a1,b2,c3} on C1 by A47,A62,A65,INCSP_1:2;
then c3 on C39 by A1,A75,A73,A64,A81,A80,A79,A69,A68,A78,A67,A77,A76,A82,
INCPROJ:def 14;
then not c3 is Element of AS by Th27;
then consider Y such that
A83: c3=LDir(Y) and
A84: Y is being_line by Th20;
Y '||' Line(c,a9) by A23,A65,A83,A84,Th28;
then
A85: Y // Line(c,a9) by A23,A84,AFF_4:40;
Y '||' Line(a,c9) by A32,A66,A83,A84,Th28;
then Y // Line(a,c9) by A32,A84,AFF_4:40;
then Line(a,c9) // Line(c,a9) by A85,AFF_1:44;
hence thesis by A57,A49,A46,A61,AFF_1:39;
end;
hence thesis by A2,A3,A4,A5,A6,A9,A10,A12,A14,A15,A16,A17,A18,A19,A20,Th48;
end;
hence thesis by AFF_2:def 2;
end;
theorem Th50:
for A,P,C being Subset of AS, o,a,b,c,a9,b9,c9 being Element
of AS st o in A & o in P & o in C & o<>a & o<>b & o<>c & a in A & b
in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is
being_line & A<>P & A<>C & a,b // a9,b9 & a,c // a9,c9 & (o=a9 or a=a9) holds b
,c // b9,c9
proof
let A,P,C be Subset of AS, o,a,b,c,a9,b9,c9 be Element of AS
such that
A1: o in A and
A2: o in P and
A3: o in C and
A4: o<>a and
A5: o<>b and
A6: o<>c and
A7: a in A and
A8: b in P and
A9: b9 in P and
A10: c in C and
A11: c9 in C and
A12: A is being_line and
A13: P is being_line and
A14: C is being_line and
A15: A<>P and
A16: A<>C and
A17: a,b // a9,b9 and
A18: a,c // a9,c9 and
A19: o=a9 or a=a9;
A20: now
assume
A21: a=a9;
then
A22: c =c9 by A1,A3,A4,A6,A7,A10,A11,A12,A14,A16,A18,AFF_4:9;
b=b9 by A1,A2,A4,A5,A7,A8,A9,A12,A13,A15,A17,A21,AFF_4:9;
hence thesis by A22,AFF_1:2;
end;
now
assume
A23: o=a9;
then
A24: o=c9 by A1,A3,A4,A6,A7,A10,A11,A12,A14,A16,A18,AFF_4:8;
o=b9 by A1,A2,A4,A5,A7,A8,A9,A12,A13,A15,A17,A23,AFF_4:8;
hence thesis by A24,AFF_1:3;
end;
hence thesis by A19,A20;
end;
theorem
IncProjSp_of(AS) is Desarguesian implies AS is Desarguesian
proof
set XX= IncProjSp_of(AS);
assume
A1: IncProjSp_of(AS) is Desarguesian;
for A,P,C being Subset of AS, o,a,b,c,a9,b9,c9 being Element
of AS st o in A & o in P & o in C & o<>a & o<>b & o<>c & a in A & a9 in
A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C
is being_line & A<>P & A<>C & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9
proof
let A,P,C be Subset of AS, o,a,b,c,a9,b9,c9 be Element of
AS such that
A2: o in A and
A3: o in P and
A4: o in C and
A5: o<>a and
A6: o<>b and
A7: o<>c and
A8: a in A and
A9: a9 in A and
A10: b in P and
A11: b9 in P and
A12: c in C and
A13: c9 in C and
A14: A is being_line and
A15: P is being_line and
A16: C is being_line and
A17: A<>P and
A18: A<>C and
A19: a,b // a9,b9 and
A20: a,c // a9,c9;
now
assume
A21: P<>C;
now
reconsider p=o,a1=a,b1=a9,a2=b,b2=b9,a3=c,b3=c9 as Element of the
Points of XX by Th20;
reconsider C1=[A,1],C2=[P,1],C39=[C,1] as Element of the Lines of XX
by A14,A15,A16,Th23;
assume that
A22: a<>a9 and
A23: o<>a9;
A24: o<>c9 by A2,A4,A5,A7,A8,A9,A12,A14,A16,A18,A20,A23,AFF_4:8;
A25: a9<>c9 by A2,A4,A9,A13,A14,A16,A18,A23,AFF_1:18;
then
A26: Line(a9,c9) is being_line by AFF_1:def 3;
A27: o<>b9 by A2,A3,A5,A6,A8,A9,A10,A14,A15,A17,A19,A23,AFF_4:8;
then b9<>c9 by A3,A4,A11,A13,A15,A16,A21,AFF_1:18;
then
A28: Line(b9,c9) is being_line by AFF_1:def 3;
b<>c by A3,A4,A6,A10,A12,A15,A16,A21,AFF_1:18;
then
A29: Line(b,c) is being_line by AFF_1:def 3;
A30: a<>c by A2,A4,A5,A8,A12,A14,A16,A18,AFF_1:18;
then
A31: Line(a,c) is being_line by AFF_1:def 3;
A32: a<>b by A2,A3,A5,A8,A10,A14,A15,A17,AFF_1:18;
then
A33: Line(a,b) is being_line by AFF_1:def 3;
then reconsider s=LDir(Line(a,b)),r=LDir(Line(a,c)) as Element of the
Points of XX by A31,Th20;
A34: p on C2 by A3,A15,Th26;
A35: a9<>b9 by A2,A3,A9,A11,A14,A15,A17,A23,AFF_1:18;
then
A36: Line(a9,b9) is being_line by AFF_1:def 3;
then reconsider
A1=[Line(b,c),1],A2=[Line(a,c),1],A3=[Line(a,b),1], B1=[
Line(b9,c9),1],B2=[Line(a9,c9),1],B3=[Line(a9,b9),1] as Element of the Lines of
XX by A33,A29,A31,A28,A26,Th23;
A37: r on A2 by A31,Th30;
A38: c in Line(b,c) by AFF_1:15;
then
A39: a3 on A1 by A29,Th26;
A40: a3 on A1 by A29,A38,Th26;
A41: c9 in Line(a9,c9) by AFF_1:15;
then
A42: b3 on B2 by A26,Th26;
A43: a9 in Line(a9,c9) by AFF_1:15;
then
A44: b1 on B2 by A26,Th26;
A45: Line(a,c) // Line(a9,c9) by A20,A30,A25,AFF_1:37;
then Line(a,c) '||' Line(a9,c9) by A31,A26,AFF_4:40;
then r on B2 by A31,A26,Th28;
then
A46: {b1,r,b3} on B2 by A44,A42,INCSP_1:2;
A47: c <>c9 by A2,A4,A5,A7,A8,A9,A12,A14,A16,A18,A20,A22,AFF_4:9;
A48: b1 on C1 by A9,A14,Th26;
A49: a3 on C39 by A12,A16,Th26;
A50: b9 in Line(a9,b9) by AFF_1:15;
then
A51: b2 on B3 by A36,Th26;
A52: a9 in Line(a9,b9) by AFF_1:15;
then
A53: b1 on B3 by A36,Th26;
A54: Line(a,b) // Line(a9,b9) by A19,A32,A35,AFF_1:37;
then Line(a,b) '||' Line(a9,b9) by A33,A36,AFF_4:40;
then s on B3 by A33,A36,Th28;
then
A55: {b1,s,b2} on B3 by A53,A51,INCSP_1:2;
A56: now
assume C2=C39;
then P=[C,1]`1
.=C;
hence contradiction by A21;
end;
A57: now
assume C1=C39;
then A=[C,1]`1
.=C;
hence contradiction by A18;
end;
now
assume C1=C2;
then A=[P,1]`1
.=P;
hence contradiction by A17;
end;
then
A58: C1,C2,C39 are_mutually_distinct by A56,A57,ZFMISC_1:def 5;
A59: a1 on C1 by A8,A14,Th26;
A60: b3 on C39 by A13,A16,Th26;
A61: p on C39 by A4,A16,Th26;
then
A62: {p,a3,b3} on C39 by A49,A60,INCSP_1:2;
p on C1 by A2,A14,Th26;
then
A63: {p,b1,a1} on C1 by A48,A59,INCSP_1:2;
A64: b2 on C2 by A11,A15,Th26;
A65: a in Line(a,c) by AFF_1:15;
then
A66: a1 on A2 by A31,Th26;
A67: c in Line(a,c) by AFF_1:15;
then a3 on A2 by A31,Th26;
then
A68: {a3,r,a1} on A2 by A37,A66,INCSP_1:2;
A69: b9 in Line(b9,c9) by AFF_1:15;
then
A70: b2 on B1 by A28,Th26;
A71: c9 in Line(b9,c9) by AFF_1:15;
then
A72: b3 on B1 by A28,Th26;
A73: b3 on B1 by A28,A71,Th26;
A74: a2 on C2 by A10,A15,Th26;
then
A75: {p,a2,b2} on C2 by A34,A64,INCSP_1:2;
A76: b in Line(b,c) by AFF_1:15;
then
A77: a2 on A1 by A29,Th26;
not p on A1 & not p on B1
proof
assume p on A1 or p on B1;
then a3 on C2 or b3 on C2 by A6,A27,A34,A74,A64,A77,A40,A70,A73,
INCPROJ:def 4;
hence contradiction by A7,A24,A34,A61,A49,A60,A56,INCPROJ:def 4;
end;
then consider t being Element of the Points of XX such that
A78: t on A1 and
A79: t on B1 by A34,A61,A74,A64,A49,A60,A77,A40,A70,A73,A56,INCPROJ:def 8;
a2 on A1 by A29,A76,Th26;
then
A80: {a3,a2,t} on A1 by A78,A39,INCSP_1:2;
b2 on B1 by A28,A69,Th26;
then
A81: {t,b2,b3} on B1 by A79,A72,INCSP_1:2;
A82: a in Line(a,b) by AFF_1:15;
then
A83: a1 on A3 by A33,Th26;
A84: s on A3 by A33,Th30;
A85: b in Line(a,b) by AFF_1:15;
then a2 on A3 by A33,Th26;
then
A86: {a2,s,a1} on A3 by A84,A83,INCSP_1:2;
b<>b9 by A2,A3,A5,A6,A8,A9,A10,A14,A15,A17,A19,A22,AFF_4:9;
then consider O being Element of the Lines of XX such that
A87: {r,s,t} on O by A1,A5,A6,A7,A22,A23,A27,A24,A47,A63,A75,A62,A80,A68,A86
,A81,A46,A55,A58,INCPROJ:def 13;
A88: t on O by A87,INCSP_1:2;
A89: s on O by A87,INCSP_1:2;
A90: r on O by A87,INCSP_1:2;
A91: now
assume
A92: r<>s;
ex X st O=[PDir(X),2] & X is being_plane
proof
reconsider x=LDir(Line(a,b)),y=LDir(Line(a,c)) as Element of the
Points of ProjHorizon(AS) by A33,A31,Th14;
A93: [y,O] in the Inc of IncProjSp_of(AS) by A90,INCSP_1:def 1;
[x,O] in the Inc of IncProjSp_of(AS) by A89,INCSP_1:def 1;
then consider
Z9 being Element of the Lines of ProjHorizon(AS) such
that
A94: O=[Z9,2] by A92,A93,Th41;
consider X such that
A95: Z9=PDir(X) and
A96: X is being_plane by Th15;
take X;
thus thesis by A94,A95,A96;
end;
then not t is Element of AS by A88,Th27;
then consider Y such that
A97: t=LDir(Y) and
A98: Y is being_line by Th20;
Y '||' Line(b9,c9) by A28,A79,A97,A98,Th28;
then
A99: Y // Line(b9,c9) by A28,A98,AFF_4:40;
Y '||' Line(b,c) by A29,A78,A97,A98,Th28;
then Y // Line(b,c) by A29,A98,AFF_4:40;
then Line(b,c) // Line(b9,c9) by A99,AFF_1:44;
hence thesis by A76,A38,A69,A71,AFF_1:39;
end;
now
assume r=s;
then
A100: Line(a,b) // Line(a,c) by A33,A31,Th11;
then Line(a,b) // Line(a9,c9) by A45,AFF_1:44;
then Line(a9,b9) // Line(a9, c9) by A54,AFF_1:44;
then
A101: c9 in Line(a9,b9) by A52,A43,A41,AFF_1:45;
c in Line(a,b) by A82,A65,A67,A100,AFF_1:45;
hence thesis by A85,A50,A54,A101,AFF_1:39;
end;
hence thesis by A91;
end;
hence
thesis by A2,A3,A4,A5,A6,A7,A8,A10,A11,A12,A13,A14,A15,A16,A17,A18,A19
,A20,Th50;
end;
hence thesis by A10,A11,A12,A13,A15,AFF_1:51;
end;
hence thesis by AFF_2:def 4;
end;
theorem
IncProjSp_of(AS) is Fanoian implies AS is Fanoian
proof
set XX=IncProjSp_of(AS);
assume
A1: IncProjSp_of(AS) is Fanoian;
for a,b,c,d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c
holds a,b // a,c
proof
let a,b,c,d be Element of AS such that
A2: a,b // c,d and
A3: a,c // b,d and
A4: a,d // b,c;
assume
A5: not a,b // a,c;
then
A6: a<>d by A2,AFF_1:4;
then
A7: Line(a,d) is being_line by AFF_1:def 3;
A8: now
assume b=d;
then b,a // b,c by A2,AFF_1:4;
then LIN b,a,c by AFF_1:def 1;
then LIN a,b,c by AFF_1:6;
hence contradiction by A5,AFF_1:def 1;
end;
then
A9: Line(b,d) is being_line by AFF_1:def 3;
A10: now
assume c =d;
then c,a // c,b by A3,AFF_1:4;
then LIN c,a,b by AFF_1:def 1;
then LIN a,b,c by AFF_1:6;
hence contradiction by A5,AFF_1:def 1;
end;
then
A11: Line(c,d) is being_line by AFF_1:def 3;
A12: a<>c by A5,AFF_1:3;
then
A13: Line(a,c) is being_line by AFF_1:def 3;
A14: a<>b by A5,AFF_1:3;
then
A15: Line(a,b) is being_line by AFF_1:def 3;
then reconsider
a9=LDir(Line(a,b)),b9=LDir(Line(a,c)),c9=LDir(Line(a,d)) as
Element of the Points of XX by A13,A7,Th20;
A16: b<>c by A5,AFF_1:2;
then
A17: Line(b,c) is being_line by AFF_1:def 3;
then reconsider
L1=[Line(a,b),1],Q1=[Line(c,d),1],R1=[Line(b,d),1],S1=[Line(a,c
),1], A1=[Line(a,d),1],B1=[Line(b,c),1] as Element of the Lines of XX by A15
,A11,A9,A13,A7,Th23;
reconsider p=a,q=d,r=c,s=b as Element of the Points of XX by Th20;
A18: a9 on L1 by A15,Th30;
c in Line(b,c) by AFF_1:15;
then
A19: r on B1 by A17,Th26;
b in Line(b,c) by AFF_1:15;
then
A20: s on B1 by A17,Th26;
Line(a,d) // Line(b,c) by A4,A16,A6,AFF_1:37;
then Line(a,d) '||' Line(b,c) by A7,A17,AFF_4:40;
then c9 on B1 by A7,A17,Th28;
then
A21: {c9,r,s} on B1 by A19,A20,INCSP_1:2;
A22: d in Line(b,d) by AFF_1:15;
then
A23: q on R1 by A9,Th26;
A24: c in Line(a,c) by AFF_1:15;
then
A25: r on S1 by A13,Th26;
A26: b9 on S1 by A13,Th30;
A27: a in Line(a,c) by AFF_1:15;
then p on S1 by A13,Th26;
then
A28: {b9,p,r} on S1 by A25,A26,INCSP_1:2;
A29: Line(a,c) // Line(b,d) by A3,A12,A8,AFF_1:37;
then Line(a,c) '||' Line(b,d) by A9,A13,AFF_4:40;
then
A30: b9 on R1 by A9,A13,Th28;
A31: b in Line(b,d) by AFF_1:15;
then s on R1 by A9,Th26;
then
A32: {b9,q,s} on R1 by A23,A30,INCSP_1:2;
A33: now
assume Line(a,c)=Line(b,d);
then LIN a,c,b by A31,AFF_1:def 2;
then LIN a,b,c by AFF_1:6;
hence contradiction by A5,AFF_1:def 1;
end;
A34: now
assume q on S1 or s on S1;
then d in Line(a,c) or b in Line(a,c) by Th26;
hence contradiction by A31,A22,A33,A29,AFF_1:45;
end;
A35: now
assume p on R1 or r on R1;
then a in Line(b,d) or c in Line(b,d) by Th26;
hence contradiction by A27,A24,A33,A29,AFF_1:45;
end;
A36: a in Line(a,b) by AFF_1:15;
then consider Y such that
A37: Line(a,b) c= Y and
A38: Line(a,c) c= Y and
A39: Y is being_plane by A27,A15,A13,AFF_4:38;
reconsider C1=[PDir(Y),2] as Element of the Lines of XX by A39,Th23;
A40: b9 on C1 by A13,A38,A39,Th31;
A41: Line(a,b) // Line(c,d) by A2,A14,A10,AFF_1:37;
then Line(a,b) '||' Line(c,d) by A15,A11,AFF_4:40;
then
A42: a9 on Q1 by A15,A11,Th28;
d in Line(a,d) by AFF_1:15;
then
A43: q on A1 by A7,Th26;
a in Line(a,d) by AFF_1:15;
then
A44: p on A1 by A7,Th26;
c9 on A1 by A7,Th30;
then
A45: {c9,p,q} on A1 by A44,A43,INCSP_1:2;
A46: b in Line(a,b) by AFF_1:15;
then
A47: s on L1 by A15,Th26;
a9 on C1 by A15,A37,A39,Th31;
then
A48: {a9,b9} on C1 by A40,INCSP_1:1;
A49: d in Line(c,d) by AFF_1:15;
then
A50: q on Q1 by A11,Th26;
A51: c in Line(c,d) by AFF_1:15;
then r on Q1 by A11,Th26;
then
A52: {a9,q,r} on Q1 by A50,A42,INCSP_1:2;
A53: now
assume Line(a,b)=Line(c,d);
then LIN a,b,c by A51,AFF_1:def 2;
hence contradiction by A5,AFF_1:def 1;
end;
A54: now
assume q on L1 or r on L1;
then d in Line(a,b) or c in Line(a,b) by Th26;
hence contradiction by A51,A49,A53,A41,AFF_1:45;
end;
A55: now
assume p on Q1 or s on Q1;
then a in Line(c,d) or b in Line(c,d) by Th26;
hence contradiction by A36,A46,A53,A41,AFF_1:45;
end;
Line(b,d)=b*Line(a,c) by A31,A13,A29,AFF_4:def 3;
then Line(b,d) c= Y by A46,A13,A37,A38,A39,AFF_4:28;
then
A56: c9 on C1 by A36,A22,A6,A7,A37,A39,Th31,AFF_4:19;
p on L1 by A36,A15,Th26;
then {a9,p,s} on L1 by A47,A18,INCSP_1:2;
hence contradiction by A1,A56,A54,A34,A55,A35,A52,A32,A28,A45,A21,A48,
INCPROJ:def 12;
end;
hence thesis by PAPDESAF:def 1;
end;