:: Incidence Projective Spaces
:: by Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski
::
:: Received October 4, 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 SUBSET_1, COLLSP, PRE_TOPC, INCSP_1, TARSKI, STRUCT_0, XBOOLE_0,
RELAT_1, ANPROJ_2, ZFMISC_1, FDIFF_1, ANALOAF, VECTSP_1, AFF_2, INCPROJ,
PENCIL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELSET_1, STRUCT_0,
PRE_TOPC, INCSP_1, COLLSP, ANPROJ_2;
constructors DOMAIN_1, INCSP_1, ANPROJ_2;
registrations RELSET_1, STRUCT_0, ANPROJ_2;
requirements SUBSET, BOOLE;
definitions TARSKI, INCSP_1;
expansions INCSP_1;
theorems COLLSP, ANPROJ_2, RELAT_1, INCSP_1, ZFMISC_1;
schemes RELSET_1;
begin
reserve CPS for proper CollSp,
B for Subset of CPS,
p for Point of CPS,
x, y, z, Y for set;
definition
let CPS;
redefine mode LINE of CPS -> Subset of CPS; :: redefines LINE (COLLSP, definition)
coherence
proof
let x be LINE of CPS;
x c= the carrier of CPS
proof
consider a,b being Point of CPS such that
a <> b and
A1: x = Line(a,b) by COLLSP:def 7;
let z be object;
assume z in x;
then z in {p: a,b,p are_collinear} by A1,COLLSP:def 5;
then ex p being Point of CPS st z = p & a, b, p are_collinear;
hence z in the carrier of CPS;
end;
hence thesis;
end;
end;
definition
let CPS;
func ProjectiveLines(CPS) -> set equals
{B : B is LINE of CPS};
coherence;
end;
registration
let CPS;
cluster ProjectiveLines(CPS) -> non empty;
coherence
proof
set x = the LINE of CPS;
x in ProjectiveLines(CPS);
hence thesis;
end;
end;
theorem Th1:
x is LINE of CPS iff x is Element of ProjectiveLines(CPS)
proof
hereby
assume x is LINE of CPS;
then x in {B : B is LINE of CPS};
hence x is Element of ProjectiveLines(CPS);
end;
assume x is Element of ProjectiveLines(CPS);
then x in ProjectiveLines(CPS);
then ex B st x=B & B is LINE of CPS;
hence thesis;
end;
definition
let CPS;
func Proj_Inc(CPS) -> Relation of the carrier of CPS, ProjectiveLines(CPS)
means
:Def2:
for x,y being object holds [x,y] in it iff x in the carrier of CPS & y in
ProjectiveLines(CPS) & ex Y st y=Y & x in Y;
existence
proof
defpred P[object,object] means ex Y st $2=Y & $1 in Y;
ex IT being Relation of the carrier of CPS, ProjectiveLines(CPS) st
for x,y being object
holds [x,y] in IT iff x in the carrier of CPS & y in ProjectiveLines(
CPS) & P[x,y] from RELSET_1:sch 1;
hence thesis;
end;
uniqueness
proof
let R1,R2 be Relation of the carrier of CPS,ProjectiveLines(CPS) such that
A1: for x,y being object holds [x,y] in R1 iff x in the carrier of CPS & y in
ProjectiveLines(CPS) & ex Y st y=Y & x in Y and
A2: for x,y being object holds [x,y] in R2 iff x in the carrier of CPS & y in
ProjectiveLines(CPS) & ex Y st y=Y & x in Y;
now
let x,y be object;
A3: now
assume
A4: [x,y] in R2;
then
A5: ex Y st y=Y & x in Y by A2;
x in the carrier of CPS & y in ProjectiveLines(CPS) by A2,A4;
hence [x,y] in R1 by A1,A5;
end;
now
assume
A6: [x,y] in R1;
then
A7: ex Y st y=Y & x in Y by A1;
x in the carrier of CPS & y in ProjectiveLines(CPS) by A1,A6;
hence [x,y] in R2 by A2,A7;
end;
hence [x,y] in R1 iff [x,y] in R2 by A3;
end;
hence R1 = R2 by RELAT_1:def 2;
end;
end;
definition
let CPS;
func IncProjSp_of(CPS) -> IncProjStr equals
IncProjStr (# the carrier of CPS
, ProjectiveLines(CPS), Proj_Inc(CPS) #);
coherence;
end;
registration
let CPS;
cluster IncProjSp_of(CPS) -> strict;
coherence;
end;
theorem
the Points of IncProjSp_of(CPS) = the carrier of CPS & the Lines of
IncProjSp_of(CPS) = ProjectiveLines(CPS) & the Inc of IncProjSp_of(CPS) =
Proj_Inc(CPS);
theorem
x is Point of CPS iff x is POINT of IncProjSp_of(CPS);
theorem
x is LINE of CPS iff x is LINE of IncProjSp_of(CPS) by Th1;
reserve a,b,c,p,q for POINT of IncProjSp_of(CPS),
P,Q for LINE of IncProjSp_of(CPS),
a9,b9,c9,p9,q9,r9 for Point of CPS,
P9 for LINE of CPS;
theorem Th5:
p = p9 & P = P9 implies (p on P iff p9 in P9)
proof
reconsider P99= P9 as LINE of IncProjSp_of(CPS) by Th1;
reconsider P999= P99 as Element of ProjectiveLines(CPS);
assume
A1: p = p9 & P = P9;
hereby
assume p on P;
then [p9,P9] in Proj_Inc(CPS) by A1;
then ex Y st P9= Y & p9 in Y by Def2;
hence p9 in P9;
end;
assume p9 in P9;
then [p9,P999] in Proj_Inc(CPS) by Def2;
hence thesis by A1;
end;
theorem Th6:
ex a9, b9, c9 st a9<>b9 & b9<>c9 & c9<>a9
proof
consider a99, b99, c99 being Point of CPS such that
A1: not a99,b99,c99 are_collinear by COLLSP:def 6;
A2: c99<>a99 by A1,COLLSP:2;
a99<>b99 & b99<>c99 by A1,COLLSP:2;
hence thesis by A2;
end;
theorem Th7:
ex b9 st a9<>b9
proof
consider p9,q9,r9 such that
A1: p9<>q9 and
q9<>r9 and
r9<>p9 by Th6;
a9<>p9 or a9<>q9 by A1;
hence thesis;
end;
theorem Th8:
p on P & q on P & p on Q & q on Q implies p = q or P = Q
proof
reconsider p9= p, q9= q as Point of CPS;
reconsider P9= P, Q9= Q as LINE of CPS by Th1;
assume that
A1: p on P & q on P and
A2: p on Q & q on Q and
A3: p<>q;
A4: p9 in Q9 & q9 in Q9 by A2,Th5;
p9 in P9 & q9 in P9 by A1,Th5;
hence thesis by A3,A4,COLLSP:20;
end;
theorem Th9:
ex P st p on P & q on P
proof
reconsider p9= p,q9= q as Point of CPS;
A1: now
consider r9 such that
A2: p9<>r9 by Th7;
consider P9 being LINE of CPS such that
A3: p9 in P9 and
r9 in P9 by A2,COLLSP:15;
reconsider P = P9 as LINE of IncProjSp_of(CPS) by Th1;
assume
A4: p9=q9;
p on P by A3,Th5;
hence thesis by A4;
end;
now
assume p9<>q9;
then consider P9 being LINE of CPS such that
A5: p9 in P9 & q9 in P9 by COLLSP:15;
reconsider P = P9 as LINE of IncProjSp_of(CPS) by Th1;
p on P & q on P by A5,Th5;
hence thesis;
end;
hence thesis by A1;
end;
theorem Th10:
a = a9 & b = b9 & c = c9 implies (a9,b9,c9 are_collinear iff ex P
st a on P & b on P & c on P)
proof
assume that
A1: a = a9 and
A2: b = b9 and
A3: c = c9;
hereby
assume
A4: a9,b9,c9 are_collinear;
A5: now
set X = Line(a9,b9);
assume a9<>b9;
then reconsider P9= X as LINE of CPS by COLLSP:def 7;
reconsider P = P9 as LINE of IncProjSp_of(CPS) by Th1;
a9 in X by COLLSP:10;
then
A6: a on P by A1,Th5;
b9 in X by COLLSP:10;
then
A7: b on P by A2,Th5;
c9 in X by A4,COLLSP:11;
then c on P by A3,Th5;
hence ex P st a on P & b on P & c on P by A6,A7;
end;
now
assume
A8: a9=b9;
ex P st b on P & c on P by Th9;
hence ex P st a on P & b on P & c on P by A1,A2,A8;
end;
hence ex P st a on P & b on P & c on P by A5;
end;
given P such that
A9: a on P & b on P and
A10: c on P;
reconsider P9=P as LINE of CPS by Th1;
A11: c9 in P9 by A3,A10,Th5;
a9 in P9 & b9 in P9 by A1,A2,A9,Th5;
hence thesis by A11,COLLSP:16;
end;
theorem Th11:
ex p, P st not p on P
proof
consider p9,q9,r9 such that
A1: not p9,q9,r9 are_collinear by COLLSP:def 6;
set X = Line(p9,q9);
p9 <> q9 by A1,COLLSP:2;
then reconsider P9= X as LINE of CPS by COLLSP:def 7;
reconsider P = P9 as LINE of IncProjSp_of(CPS) by Th1;
reconsider r = r9 as POINT of IncProjSp_of(CPS);
not r on P
proof
assume not thesis;
then r9 in X by Th5;
hence contradiction by A1,COLLSP:11;
end;
hence thesis;
end;
reserve CPS for CollProjectiveSpace,
a,b,c,d,p,q for POINT of IncProjSp_of(CPS ),
P,Q,S,M,N for LINE of IncProjSp_of(CPS),
a9,b9,c9,d9,p9,q9 for Point of CPS;
theorem Th12:
ex a, b, c st a<>b & b<>c & c <>a & a on P & b on P & c on P
proof
reconsider P9= P as LINE of CPS by Th1;
consider a99, b99 being Point of CPS such that
A1: a99<>b99 and
A2: P9 = Line(a99,b99) by COLLSP:def 7;
consider c9 such that
A3: a99<>c9 & b99<>c9 and
A4: a99, b99, c9 are_collinear by ANPROJ_2:def 10;
reconsider a=a99, b=b99, c =c9 as POINT of IncProjSp_of(CPS);
take a,b,c;
thus a<>b & b<>c & c <>a by A1,A3;
a99 in P9 by A2,COLLSP:10;
then
A5: a on P by Th5;
b99 in P9 by A2,COLLSP:10;
then
A6: b on P by Th5;
ex Q st a on Q & b on Q & c on Q by A4,Th10;
hence thesis by A1,A5,A6,Th8;
end;
theorem Th13:
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 & p on N and
A6: a on P and
A7: c on P and
A8: b on Q and
A9: d on Q and
A10: not p on P and
A11: not p on Q and
A12: M<>N;
reconsider a9=a,b9=b,c9=c,d9=d,p9=p as Point of CPS;
b9,p9,a9 are_collinear & p9,d9,c9 are_collinear by A1,A2,A3,A4,A5,Th10;
then consider q9 such that
A13: b9,d9,q9 are_collinear and
A14: a9,c9,q9 are_collinear by ANPROJ_2:def 9;
reconsider q = q9 as POINT of IncProjSp_of(CPS);
A15: ex P2 being LINE of IncProjSp_of(CPS) st b on P2 & d on P2 & q on P2 by
A13,Th10;
b<>d by A2,A4,A5,A8,A11,A12,Th8;
then
A16: q on Q by A8,A9,A15,Th8;
A17: ex P1 being LINE of IncProjSp_of(CPS) st a on P1 & c on P1 & q on P1 by
A14,Th10;
a<>c by A1,A3,A5,A6,A10,A12,Th8;
then q on P by A6,A7,A17,Th8;
hence thesis by A16;
end;
theorem Th14:
(for a9,b9,c9,d9 ex p9 st a9, b9, p9 are_collinear & c9, d9, p9
are_collinear) implies for M, N ex q st q on M & q on N
proof
assume
A1: for a9,b9,c9,d9 ex p9 st a9, b9, p9 are_collinear &
c9, d9, p9 are_collinear;
let M, N;
reconsider M9= M, N9= N as LINE of CPS by Th1;
consider a9, b9 such that
a9<>b9 and
A2: M9= Line(a9,b9) by COLLSP:def 7;
consider c9, d9 such that
c9<>d9 and
A3: N9= Line(c9,d9) by COLLSP:def 7;
consider p9 such that
A4: a9, b9, p9 are_collinear and
A5: c9, d9, p9 are_collinear by A1;
reconsider q = p9 as POINT of IncProjSp_of(CPS);
p9 in N9 by A3,A5,COLLSP:11;
then
A6: q on N by Th5;
p9 in M9 by A2,A4,COLLSP:11;
then q on M by Th5;
hence thesis by A6;
end;
theorem Th15:
(ex p, p1, r, r1 being Point of CPS st not ex s being Point of
CPS st (p, p1, s are_collinear & r, r1, s are_collinear)) implies
ex M, N st not
ex q st q on M & q on N
proof
given p, p1, r, r1 being Point of CPS such that
A1: not ex s being Point of CPS st
(p,p1,s are_collinear & r,r1,s are_collinear);
set M99= Line(p,p1), N99= Line(r,r1);
p<>p1 & r<>r1
proof
A2: now
assume p = p1;
then
A3: p,p1,r1 are_collinear by COLLSP:2;
r,r1,r1 are_collinear by COLLSP:2;
hence contradiction by A1,A3;
end;
A4: now
assume r = r1;
then p,p1,p1 are_collinear & r,r1,p1 are_collinear by COLLSP:2;
hence contradiction by A1;
end;
assume not thesis;
hence contradiction by A2,A4;
end;
then reconsider M9= M99, N9= N99 as LINE of CPS by COLLSP:def 7;
reconsider M = M9, N = N9 as LINE of IncProjSp_of(CPS) by Th1;
take M, N;
thus not ex q st q on M & q on N
proof
assume not thesis;
then consider q such that
A5: q on M and
A6: q on N;
reconsider q9=q as Point of CPS;
q9 in N99 by A6,Th5;
then
A7: r,r1,q9 are_collinear by COLLSP:11;
q9 in M99 by A5,Th5;
then p,p1,q9 are_collinear by COLLSP:11;
hence contradiction by A1,A7;
end;
end;
theorem Th16:
(for p, p1, q, q1, r2 being Point of CPS ex r, r1 being Point of
CPS st p,q,r are_collinear & p1,q1,r1 are_collinear & r2,r,r1 are_collinear)
implies for a, M, N ex b, c, S st a on S & b on S & c on S & b on M & c on N
proof
assume
A1: for p, p1, q, q1, r2 being Point of CPS ex r, r1 being Point of CPS
st p,q,r are_collinear & p1,q1,r1 are_collinear & r2,r,r1 are_collinear;
let a, M, N;
reconsider M9= M, N9= N as LINE of CPS by Th1;
reconsider a9= a as Point of CPS;
consider p, q being Point of CPS such that
p<>q and
A2: M9= Line(p,q) by COLLSP:def 7;
consider p1, q1 being Point of CPS such that
p1<>q1 and
A3: N9 = Line(p1,q1) by COLLSP:def 7;
consider b9, c9 such that
A4: p,q,b9 are_collinear and
A5: p1,q1,c9 are_collinear and
A6: a9,b9,c9 are_collinear by A1;
reconsider b = b9, c = c9 as POINT of IncProjSp_of(CPS);
b9 in M9 by A2,A4,COLLSP:11;
then
A7: b on M by Th5;
c9 in N9 by A3,A5,COLLSP:11;
then
A8: c on N by Th5;
ex S st a on S & b on S & c on S by A6,Th10;
hence thesis by A7,A8;
end;
theorem Th17:
(for p1, r2, q, r1, q1, p, r being Point of CPS holds (p1,r2,q
are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p
are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear &
p,q,r are_collinear
implies (p1,r2,q1 are_collinear or p1,r2,r1 are_collinear or p1,r1,q1
are_collinear or r2,r1,q1 are_collinear))) implies
for p, q, r, s, a, b, c being
POINT of IncProjSp_of(CPS) for L, Q, R, S, A, B, C being LINE of IncProjSp_of(
CPS) st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r
on R & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A
& {c,r,s} on B & {a,b} on C holds not c on C
proof
assume
A1: for p1, r2, q, r1, q1, p, r being Element of CPS holds (p1,r2,q
are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p
are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear &
p,q,r are_collinear
implies (p1,r2,q1 are_collinear or p1,r2,r1 are_collinear or p1,r1,q1
are_collinear or r2,r1,q1 are_collinear));
let p, q, r, s, a, b, c be POINT of IncProjSp_of(CPS);
let L, Q, R, S, A, B, C be LINE of IncProjSp_of(CPS) such that
A2: not q on L and
A3: not r on L and
A4: not p on Q and
A5: not s on Q and
A6: not p on R and
A7: not r on R and
A8: {a,p,s} on L and
A9: {a,q,r} on Q and
A10: {b,q,s} on R and
A11: {b,p,r} on S and
A12: {c,p,q} on A and
A13: {c,r,s} on B and
A14: {a,b} on C;
reconsider p9=p, q9=q, r9=r, s9=s, a9=a, b9=b, c9=c as Point of CPS;
A15: p on L & s on L by A8,INCSP_1:2;
A16: s on R by A10,INCSP_1:2;
A17: now
assume p9,r9,s9 are_collinear;
then
A18: ex K being LINE of IncProjSp_of(CPS) st p on K & r on K & s on K by Th10;
hence s on S by A3,A6,A15,A16,Th8;
thus contradiction by A3,A6,A15,A16,A18,Th8;
end;
A19: now
assume p9,s9,q9 are_collinear;
then
A20: ex K being LINE of IncProjSp_of(CPS) st p on K & s on K & q on K by Th10;
hence p on R by A2,A15,A16,Th8;
thus contradiction by A2,A6,A15,A16,A20,Th8;
end;
a on L by A8,INCSP_1:2;
then
A21: p9,s9,a9 are_collinear by A15,Th10;
assume
A22: not thesis;
a on C & b on C by A14,INCSP_1:1;
then
A23: a9,b9,c9 are_collinear by A22,Th10;
A24: q on Q & r on Q by A9,INCSP_1:2;
A25: q on R by A10,INCSP_1:2;
A26: now
assume p9,r9,q9 are_collinear;
then
A27: ex K being LINE of IncProjSp_of(CPS) st p on K & r on K & q on K by Th10;
hence q on S by A4,A7,A24,A25,Th8;
thus contradiction by A4,A7,A24,A25,A27,Th8;
end;
A28: now
assume r9,s9,q9 are_collinear;
then
A29: ex K being LINE of IncProjSp_of(CPS) st r on K & s on K & q on K by Th10;
hence r on R by A5,A24,A25,Th8;
thus contradiction by A5,A7,A24,A25,A29,Th8;
end;
a on Q by A9,INCSP_1:2;
then
A30: r9,q9,a9 are_collinear by A24,Th10;
A31: r on S by A11,INCSP_1:2;
b on S & p on S by A11,INCSP_1:2;
then
A32: p9,r9,b9 are_collinear by A31,Th10;
A33: s on B by A13,INCSP_1:2;
c on B & r on B by A13,INCSP_1:2;
then
A34: r9,s9,c9 are_collinear by A33,Th10;
A35: q on A by A12,INCSP_1:2;
c on A & p on A by A12,INCSP_1:2;
then
A36: p9,q9,c9 are_collinear by A35,Th10;
b on R by A10,INCSP_1:2;
then s9,q9,b9 are_collinear by A25,A16,Th10;
hence contradiction by A1,A23,A32,A21,A30,A36,A34,A26,A17,A19,A28;
end;
theorem Th18:
(for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 being Point of CPS st o<>q1 &
p1<>q1 & o<>q2 & p2<>q2 & o<>q3 & p3<>q3 & not o,p1,p2 are_collinear &
not o,p1,
p3 are_collinear & not o,p2,p3 are_collinear & p1,p2,r3 are_collinear &
q1,q2,r3
are_collinear & p2,p3,r1 are_collinear & q2,q3,r1 are_collinear & p1,p3,r2
are_collinear & q1,q3,r2 are_collinear & o,p1,q1 are_collinear & o,p2,q2
are_collinear & o,p3,q3 are_collinear holds r1,r2,r3 are_collinear) implies
for o,
b1,a1,b2,a2,b3,a3,r,s,t being POINT of IncProjSp_of(CPS) for C1,C2,C3,A1,A2,A3,
B1,B2,B3 being LINE of IncProjSp_of(CPS) st {o,b1,a1} on C1 & {o,a2,b2} on C2 &
{o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,
b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_distinct
& o<>a1 & o<>a2 & o<>a3 & o<>b1 & o<>b2 & o<>b3 & a1<>b1 & a2<>b2 & a3<>b3
holds ex O being LINE of IncProjSp_of(CPS) st {r,s,t} on O
proof
assume
A1: for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 being Element of CPS st o<>q1 & p1
<>q1 & o<>q2 & p2<>q2 & o<>q3 & p3<>q3 & not o,p1,p2 are_collinear &
not o,p1,p3
are_collinear & not o,p2,p3 are_collinear & p1,p2,r3 are_collinear & q1,q2,r3
are_collinear & p2,p3,r1 are_collinear & q2,q3,r1 are_collinear & p1,p3,r2
are_collinear & q1,q3,r2 are_collinear & o,p1,q1 are_collinear & o,p2,q2
are_collinear & o,p3,q3 are_collinear holds r1,r2,r3 are_collinear;
let o,b1,a1,b2,a2,b3,a3,r,s,t be POINT of IncProjSp_of(CPS);
let C1,C2,C3,A1,A2,A3,B1,B2,B3 be LINE of IncProjSp_of(CPS) such that
A2: {o,b1,a1} on C1 and
A3: {o,a2,b2} on C2 and
A4: {o,a3,b3} on C3 and
A5: {a3,a2,t} on A1 and
A6: {a3,r,a1} on A2 and
A7: {a2,s,a1} on A3 and
A8: {t,b2,b3} on B1 and
A9: {b1,r,b3} on B2 and
A10: {b1,s,b2} on B3 and
A11: C1,C2,C3 are_mutually_distinct and
A12: o<>a1 & o<>a2 & o<>a3 and
A13: o<>b1 and
A14: o<>b2 and
A15: o<>b3 and
A16: a1<>b1 & a2<>b2 & a3<>b3;
reconsider o9=o,b19=b1,a19=a1,b29=b2,a29=a2,b39=b3,a39=a3,r9=r,s9=s,t9=t as
Element of CPS;
A17: o on C2 & b2 on C2 by A3,INCSP_1:2;
A18: s on B3 by A10,INCSP_1:2;
b2 on B3 & b1 on B3 by A10,INCSP_1:2;
then
A19: b19,b29,s9 are_collinear by A18,Th10;
A20: r on B2 by A9,INCSP_1:2;
b3 on B2 & b1 on B2 by A9,INCSP_1:2;
then
A21: b19,b39,r9 are_collinear by A20,Th10;
A22: t on B1 by A8,INCSP_1:2;
b3 on B1 & b2 on B1 by A8,INCSP_1:2;
then
A23: b29,b39,t9 are_collinear by A22,Th10;
A24: s on A3 by A7,INCSP_1:2;
a2 on A3 & a1 on A3 by A7,INCSP_1:2;
then
A25: a19,a29,s9 are_collinear by A24,Th10;
A26: o on C3 & b3 on C3 by A4,INCSP_1:2;
a3 on C3 by A4,INCSP_1:2;
then
A27: o9,b39,a39 are_collinear by A26,Th10;
a2 on C2 by A3,INCSP_1:2;
then
A28: o9,b29,a29 are_collinear by A17,Th10;
A29: r on A2 by A6,INCSP_1:2;
a3 on A2 & a1 on A2 by A6,INCSP_1:2;
then
A30: a19,a39,r9 are_collinear by A29,Th10;
A31: t on A1 by A5,INCSP_1:2;
a3 on A1 & a2 on A1 by A5,INCSP_1:2;
then
A32: a29,a39,t9 are_collinear by A31,Th10;
A33: o on C1 & b1 on C1 by A2,INCSP_1:2;
A34: not o9,b19,b29 are_collinear & not o9,b19,b39 are_collinear & not o9,b29,
b39 are_collinear
proof
A35: now
assume o9,b19,b39 are_collinear;
then consider K being LINE of IncProjSp_of(CPS) such that
A36: o on K & b1 on K & b3 on K by Th10;
K = C1 & K = C3 by A13,A15,A33,A26,A36,Th8;
hence contradiction by A11,ZFMISC_1:def 5;
end;
A37: now
assume o9,b19,b29 are_collinear;
then consider K being LINE of IncProjSp_of(CPS) such that
A38: o on K & b1 on K & b2 on K by Th10;
K = C1 & K = C2 by A13,A14,A33,A17,A38,Th8;
hence contradiction by A11,ZFMISC_1:def 5;
end;
A39: now
assume o9,b29,b39 are_collinear;
then consider K being LINE of IncProjSp_of(CPS) such that
A40: o on K & b2 on K & b3 on K by Th10;
K = C2 & K = C3 by A14,A15,A17,A26,A40,Th8;
hence contradiction by A11,ZFMISC_1:def 5;
end;
assume not thesis;
hence contradiction by A37,A35,A39;
end;
a1 on C1 by A2,INCSP_1:2;
then o9,b19,a19 are_collinear by A33,Th10;
then t9,r9,s9 are_collinear
by A1,A12,A16,A19,A25,A21,A30,A23,A32,A28,A27,A34;
then consider O being LINE of IncProjSp_of(CPS) such that
A41: t on O & r on O & s on O by Th10;
{r,s,t} on O by A41,INCSP_1:2;
hence thesis;
end;
theorem Th19:
(for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 being Point of CPS st o<>p2 &
o<>p3 & p2<>p3 & p1<>p2 & p1<>p3 & o<>q2 & o<>q3 & q2<>q3 & q1<>q2 & q1<>q3 &
not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear &
o,q1,
q2 are_collinear & o,q1,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3
are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1
are_collinear & p3,q2,r1 are_collinear holds r1,r2,r3 are_collinear) implies
for o
,a1,a2,a3,b1,b2,b3,c1,c2,c3 being POINT of IncProjSp_of(CPS) for A1,A2,A3,B1,B2
,B3,C1,C2,C3 being LINE of IncProjSp_of(CPS) st o,a1,a2,a3
are_mutually_distinct & o,b1,b2,b3 are_mutually_distinct & A3<>B3 & o on A3 &
o on B3 & {a2,b3,c1} on A1 & {a3,b1,c2} on B1 & {a1,b2,c3} on C1 & {a1,b3,c2}
on A2 & {a3,b2,c1} on B2 & {a2,b1,c3} on C2 & {b1,b2,b3} on A3 & {a1,a2,a3} on
B3 & {c1,c2} on C3 holds c3 on C3
proof
assume
A1: for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 being Point of CPS st o<>p2 & o<>p3
& p2<>p3 & p1<>p2 & p1<>p3 & o<>q2 & o<>q3 & q2<>q3 & q1<>q2 & q1<>q3 & not o,
p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2
are_collinear & o,q1,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3
are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1
are_collinear & p3,q2,r1 are_collinear holds r1,r2,r3 are_collinear;
let o,a1,a2,a3,b1,b2,b3,c1,c2,c3 be POINT of IncProjSp_of(CPS);
let A1,A2,A3,B1,B2,B3,C1,C2,C3 be LINE of IncProjSp_of(CPS) such that
A2: o,a1,a2,a3 are_mutually_distinct and
A3: o,b1,b2,b3 are_mutually_distinct and
A4: A3<>B3 and
A5: o on A3 and
A6: o on B3 and
A7: {a2,b3,c1} on A1 and
A8: {a3,b1,c2} on B1 and
A9: {a1,b2,c3} on C1 and
A10: {a1,b3,c2} on A2 and
A11: {a3,b2,c1} on B2 and
A12: {a2,b1,c3} on C2 and
A13: {b1,b2,b3} on A3 and
A14: {a1,a2,a3} on B3 and
A15: {c1,c2} on C3;
reconsider o9= o, a19= a1, a29= a2, a39= a3, b19= b1, b29= b2, b39= b3, c19=
c1, c29= c2, c39= c3 as Point of CPS;
A16: b1 on A3 by A13,INCSP_1:2;
A17: c3 on C1 by A9,INCSP_1:2;
a1 on C1 & b2 on C1 by A9,INCSP_1:2;
then
A18: a19,b29,c39 are_collinear by A17,Th10;
A19: c1 on A1 by A7,INCSP_1:2;
A20: o9<>b39 & b29<>b39 by A3,ZFMISC_1:def 6;
A21: a29<>a39 & a19<>a29 by A2,ZFMISC_1:def 6;
A22: b3 on A2 & c2 on A2 by A10,INCSP_1:2;
A23: a1 on A2 by A10,INCSP_1:2;
then
A24: a19,b39,c29 are_collinear by A22,Th10;
A25: b19<>b29 & b19<>b39 by A3,ZFMISC_1:def 6;
A26: b3 on A1 by A7,INCSP_1:2;
A27: a1 on B3 by A14,INCSP_1:2;
A28: not o9,a19,b19 are_collinear
proof
A29: o<>a1 by A2,ZFMISC_1:def 6;
assume not thesis;
then consider K being LINE of IncProjSp_of(CPS) such that
A30: o on K and
A31: a1 on K and
A32: b1 on K by Th10;
o<>b1 by A3,ZFMISC_1:def 6;
then K = A3 by A5,A16,A30,A32,Th8;
hence contradiction by A4,A6,A27,A30,A31,A29,Th8;
end;
A33: c3 on C2 by A12,INCSP_1:2;
a2 on C2 & b1 on C2 by A12,INCSP_1:2;
then
A34: b19,a29,c39 are_collinear by A33,Th10;
A35: a3 on B1 by A8,INCSP_1:2;
A36: b2 on A3 by A13,INCSP_1:2;
then
A37: o9,b19,b29 are_collinear by A5,A16,Th10;
A38: a3 on B2 & c1 on B2 by A11,INCSP_1:2;
A39: b2 on B2 by A11,INCSP_1:2;
then
A40: a39,b29,c19 are_collinear by A38,Th10;
A41: b3 on A3 by A13,INCSP_1:2;
then
A42: o9,b19,b39 are_collinear by A5,A16,Th10;
A43: a19<>a39 & o9<>b29 by A2,A3,ZFMISC_1:def 6;
A44: o9<>a29 & o9<>a39 by A2,ZFMISC_1:def 6;
A45: c2 on B1 by A8,INCSP_1:2;
A46: a2 on A1 by A7,INCSP_1:2;
then
A47: a29,b39,c19 are_collinear by A26,A19,Th10;
A48: b1<>b2 by A3,ZFMISC_1:def 6;
A49: a1<>a2 by A2,ZFMISC_1:def 6;
A50: o<>b3 by A3,ZFMISC_1:def 6;
A51: b1 on B1 by A8,INCSP_1:2;
then
A52: a39,b19,c29 are_collinear by A35,A45,Th10;
A53: a3 on B3 by A14,INCSP_1:2;
then
A54: o9,a19,a39 are_collinear by A6,A27,Th10;
A55: a2 on B3 by A14,INCSP_1:2;
then o9,a19,a29 are_collinear by A6,A27,Th10;
then c19,c29,c39 are_collinear by A1,A44,A21,A43,A20,A25,A28,A54,A37,A42,A18
,A34,A24,A52,A47,A40;
then
A56: ex K being LINE of IncProjSp_of(CPS) st c1 on K & c2 on K & c3 on K by
Th10;
A57: o<>a3 by A2,ZFMISC_1:def 6;
A58: c1<>c2
proof
assume
A59: not thesis;
not a3 on A3 by A4,A5,A6,A57,A53,Th8;
then B1<>B2 by A48,A35,A51,A39,A16,A36,Th8;
then
A60: c1 = a3 by A35,A45,A38,A59,Th8;
not b3 on B3 by A4,A5,A6,A50,A41,Th8;
then A1<>A2 by A49,A46,A26,A23,A27,A55,Th8;
then c1 = b3 by A26,A19,A22,A59,Th8;
hence contradiction by A4,A5,A6,A50,A41,A53,A60,Th8;
end;
c1 on C3 & c2 on C3 by A15,INCSP_1:1;
hence thesis by A58,A56,Th8;
end;
definition
let S be IncProjStr;
attr S is partial means
for p, q being POINT of S, P, Q being LINE of
S st p on P & q on P & p on Q & q on Q holds p = q or P = Q;
redefine attr S is linear means :: redefines linear (INCSP_1, definition)
for p,q being POINT of S ex P being LINE of S st p on P & q on P;
compatibility
proof
hereby
assume
A1: S is linear;
let p,q be POINT of S;
consider P being LINE of S such that
A2: {p,q} on P by A1;
take P;
thus p on P & q on P by A2,INCSP_1:1;
end;
assume
A3: for p,q being POINT of S ex P being LINE of S st p on P & q on P;
let p,q be POINT of S;
consider L being LINE of S such that
A4: p on L & q on L by A3;
{p,q} on L by A4,INCSP_1:1;
hence thesis;
end;
end;
definition
let S be IncProjStr;
attr S is up-2-dimensional means
ex p being POINT of S, P being LINE of S st not p on P;
attr S is up-3-rank means
for P being LINE of S ex a, b, c being
POINT of S st a <> b & b <> c & c <> a & a on P & b on P & c on P;
attr S is Vebleian means
for a, b, c, d, p, q being POINT of S for M
, N, P, Q being LINE of S 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 S st q on P & q on Q;
end;
registration
let CPS be CollProjectiveSpace;
cluster IncProjSp_of(CPS) -> partial linear up-2-dimensional up-3-rank
Vebleian;
coherence
by Th13,Th11,Th12,Th8,Th9;
end;
registration
cluster strict partial linear up-2-dimensional up-3-rank Vebleian for
IncProjStr;
existence
proof
set CPS = the CollProjectiveSpace;
IncProjSp_of(CPS) is strict partial linear up-2-dimensional up-3-rank
Vebleian;
hence thesis;
end;
end;
definition
mode IncProjSp is partial linear up-2-dimensional up-3-rank Vebleian
IncProjStr;
end;
registration
let CPS be CollProjectiveSpace;
cluster IncProjSp_of(CPS) -> partial linear up-2-dimensional up-3-rank
Vebleian;
coherence;
end;
definition
let IT be IncProjSp;
attr IT is 2-dimensional means
for M,N being LINE of IT ex q being POINT of IT st q on M & q on N;
end;
notation
let IT be IncProjSp;
antonym IT is up-3-dimensional for IT is 2-dimensional;
end;
definition
let IT be IncProjStr;
attr IT is at_most-3-dimensional means
for a being POINT of IT, M, N
being LINE of IT ex b,c being POINT of IT, S being LINE of IT st a on S & b on
S & c on S & b on M & c on N;
end;
definition
let IT be IncProjSp;
attr IT is 3-dimensional means
IT is at_most-3-dimensional up-3-dimensional;
end;
definition
let IT be IncProjStr;
attr IT is Fanoian means
for p,q,r,s,a,b,c being POINT of IT for L,Q
,R,S,A,B,C being LINE of IT st not q on L & not r on L & not p on Q & not s on
Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r}
on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C
holds not c on C;
end;
definition
let IT be IncProjStr;
attr IT is Desarguesian means
for o,b1,a1,b2,a2,b3,a3,r,s,t being
POINT of IT for C1,C2,C3,A1,A2,A3,B1,B2,B3 being LINE of IT st {o,b1,a1} on C1
& {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s
,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3
are_mutually_distinct & o<>a1 & o<>a2 & o<>a3 & o<>b1 & o<>b2 & o<>b3 & a1<>b1
& a2<>b2 & a3<>b3 holds ex O being LINE of IT st {r,s,t} on O;
end;
definition
let IT be IncProjStr;
attr IT is Pappian means
for o,a1,a2,a3,b1,b2,b3,c1,c2,c3 being
POINT of IT for A1,A2,A3,B1,B2,B3,C1,C2,C3 being LINE of IT st o,a1,a2,a3
are_mutually_distinct & o,b1,b2,b3 are_mutually_distinct & A3<>B3 & o on A3 &
o on B3 & {a2,b3,c1} on A1 & {a3,b1,c2} on B1 & {a1,b2,c3} on C1 & {a1,b3,c2}
on A2 & {a3,b2,c1} on B2 & {a2,b1,c3} on C2 & {b1,b2,b3} on A3 & {a1,a2,a3} on
B3 & {c1,c2} on C3 holds c3 on C3;
end;
registration
cluster Desarguesian Fanoian at_most-3-dimensional up-3-dimensional
for IncProjSp;
existence
proof
set CPS = the Fanoian Desarguesian at_most-3-dimensional up-3-dimensional
CollProjectiveSpace;
reconsider CPS9 = CPS as CollProjectiveSpace;
take X = IncProjSp_of(CPS9);
for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 being Point of CPS9 st o<>q1 & p1<>q1
& o<>q2 & p2<>q2 & o<>q3 & p3<>q3 & not o,p1,p2 are_collinear & not o,p1,p3
are_collinear & not o,p2,p3 are_collinear & p1,p2,r3 are_collinear &
q1,q2,r3
are_collinear & p2,p3,r1 are_collinear & q2,q3,r1 are_collinear & p1,p3,r2
are_collinear & q1,q3,r2 are_collinear & o,p1,q1 are_collinear & o,p2,q2
are_collinear & o,p3,q3 are_collinear holds r1,r2,r3 are_collinear by
ANPROJ_2:def 12;
then
A1: for o,b1,a1,b2,a2,b3,a3,r,s,t being POINT of X for C1,C2,C3,A1,A2,A3,
B1,B2,B3 being LINE of X st {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3
& {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r
,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_distinct & o<>a1 & o<>a2
& o<>a3 & o<>b1 & o<>b2 & o<>b3 & a1<>b1 & a2<>b2 & a3<>b3 holds ex O being
LINE of X st {r,s,t} on O by Th18;
ex p,p1,r,r1 being Point of CPS9 st not ex s being Point of CPS9 st (p
,p1,s are_collinear & r,r1,s are_collinear) by ANPROJ_2:def 14;
then
A2: ex M,N being LINE of X st not ex q being POINT of X st q on M & q on N
by Th15;
for p,p1,q,q1,r2 being Point of CPS9 ex r,r1 being Point of CPS9 st p,
q,r are_collinear & p1,q1,r1 are_collinear & r2,r,r1 are_collinear by
ANPROJ_2:def 15;
then
A3: for a being POINT of X, M,N being LINE of X ex b,c being POINT of X, S
being LINE of X st a on S & b on S & c on S & b on M & c on N by Th16;
for p1,r2,q,r1,q1,p,r being Point of CPS9 holds (p1,r2,q are_collinear
& r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear &
p1,q1,r
are_collinear & r2,r1,r are_collinear & p,q,r are_collinear implies
(p1,r2,q1
are_collinear or p1,r2,r1 are_collinear or p1,r1,q1 are_collinear or
r2,r1,q1
are_collinear)) by ANPROJ_2:def 11;
then for p,q,r,s,a,b,c being POINT of X for L,Q,R,S,A,B,C being LINE of X
st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R
& not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r
} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C holds not c on C by Th17;
hence thesis by A1,A2,A3;
end;
end;
registration
cluster Pappian Fanoian at_most-3-dimensional up-3-dimensional for IncProjSp;
existence
proof
set CPS = the Fanoian Pappian at_most-3-dimensional up-3-dimensional
CollProjectiveSpace;
reconsider CPS9 = CPS as CollProjectiveSpace;
take X = IncProjSp_of(CPS9);
for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 being Point of CPS9 st o<>p2 & o<>p3
& p2<>p3 & p1<>p2 & p1<>p3 & o<>q2 & o<>q3 & q2<>q3 & q1<>q2 & q1<>q3 & not o,
p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear &
o,q1,q2
are_collinear & o,q1,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3
are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1
are_collinear & p3,q2,r1 are_collinear holds r1,r2,r3 are_collinear by
ANPROJ_2:def 13;
then
A1: for o,a1,a2,a3,b1,b2,b3,c1,c2,c3 being POINT of X for A1,A2,A3,B1,B2,
B3,C1,C2,C3 being LINE of X st o,a1,a2,a3 are_mutually_distinct & o,b1,b2,b3
are_mutually_distinct & A3<>B3 & o on A3 & o on B3 & {a2,b3,c1} on A1 & {a3,b1
,c2} on B1 & {a1,b2,c3} on C1 & {a1,b3,c2} on A2 & {a3,b2,c1} on B2 & {a2,b1,c3
} on C2 & {b1,b2,b3} on A3 & {a1,a2,a3} on B3 & {c1,c2} on C3 holds c3 on C3
by Th19;
ex p,p1,r,r1 being Point of CPS9 st not ex s being Point of CPS9 st (p
,p1,s are_collinear & r,r1,s are_collinear) by ANPROJ_2:def 14;
then
A2: ex M,N being LINE of X st not ex q being POINT of X st q on M & q on N
by Th15;
for p,p1,q,q1,r2 being Point of CPS9 ex r,r1 being Point of CPS9 st p,
q,r are_collinear & p1,q1,r1 are_collinear & r2,r,r1 are_collinear by
ANPROJ_2:def 15;
then
A3: for a being POINT of X, M,N being LINE of X ex b,c being POINT of X, S
being LINE of X st a on S & b on S & c on S & b on M & c on N by Th16;
for p1,r2,q,r1,q1,p,r being Point of CPS9 holds (p1,r2,q are_collinear
& r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear &
p1,q1,r
are_collinear & r2,r1,r are_collinear & p,q,r are_collinear
implies (p1,r2,q1
are_collinear or p1,r2,r1 are_collinear or p1,r1,q1 are_collinear
or r2,r1,q1
are_collinear)) by ANPROJ_2:def 11;
then for p,q,r,s,a,b,c being POINT of X for L,Q,R,S,A,B,C being LINE of X
st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R
& not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r
} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C holds not c on C by Th17;
hence thesis by A1,A2,A3;
end;
end;
registration
cluster Desarguesian Fanoian 2-dimensional for IncProjSp;
existence
proof
set CPS = the Fanoian Desarguesian CollProjectivePlane;
reconsider CPS9 = CPS as CollProjectiveSpace;
take X = IncProjSp_of(CPS9);
for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 being Point of CPS9 st o<>q1 & p1<>q1
& o<>q2 & p2<>q2 & o<>q3 & p3<>q3 & not o,p1,p2 are_collinear & not o,p1,p3
are_collinear & not o,p2,p3 are_collinear & p1,p2,r3 are_collinear &
q1,q2,r3
are_collinear & p2,p3,r1 are_collinear & q2,q3,r1 are_collinear & p1,p3,r2
are_collinear & q1,q3,r2 are_collinear & o,p1,q1 are_collinear & o,p2,q2
are_collinear & o,p3,q3 are_collinear holds r1,r2,r3 are_collinear by
ANPROJ_2:def 12;
then
A1: for o,b1,a1,b2,a2,b3,a3,r,s,t being POINT of X for C1,C2,C3,A1,A2,A3,
B1,B2,B3 being LINE of X st {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3
& {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r
,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_distinct & o<>a1 & o<>a2
& o<>a3 & o<>b1 & o<>b2 & o<>b3 & a1<>b1 & a2<>b2 & a3<>b3 holds ex O being
LINE of X st {r,s,t} on O by Th18;
for a,b,c,d being Point of CPS9 ex p being Point of CPS9 st a,b,p
are_collinear & c,d,p are_collinear by ANPROJ_2:def 14;
then
A2: for M,N being LINE of X ex q being POINT of X st q on M & q on N by Th14;
for p1,r2,q,r1,q1,p,r being Point of CPS9 holds (p1,r2,q are_collinear
& r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear &
p1,q1,r
are_collinear & r2,r1,r are_collinear & p,q,r are_collinear implies
(p1,r2,q1
are_collinear or p1,r2,r1 are_collinear or p1,r1,q1 are_collinear
or r2,r1,q1
are_collinear)) by ANPROJ_2:def 11;
then for p,q,r,s,a,b,c being POINT of X for L,Q,R,S,A,B,C being LINE of X
st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R
& not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r
} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C holds not c on C by Th17;
hence thesis by A1,A2;
end;
end;
registration
cluster Pappian Fanoian 2-dimensional for IncProjSp;
existence
proof
set CPS = the Fanoian Pappian CollProjectivePlane;
reconsider CPS9 = CPS as CollProjectiveSpace;
take X = IncProjSp_of(CPS9);
for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 being Point of CPS9 st o<>p2 & o<>p3
& p2<>p3 & p1<>p2 & p1<>p3 & o<>q2 & o<>q3 & q2<>q3 & q1<>q2 & q1<>q3 & not o,
p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear &
o,q1,q2
are_collinear & o,q1,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3
are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1
are_collinear & p3,q2,r1 are_collinear holds r1,r2,r3 are_collinear by
ANPROJ_2:def 13;
then
A1: for o,a1,a2,a3,b1,b2,b3,c1,c2,c3 being POINT of X for A1,A2,A3,B1,B2,
B3,C1,C2,C3 being LINE of X st o,a1,a2,a3 are_mutually_distinct & o,b1,b2,b3
are_mutually_distinct & A3<>B3 & o on A3 & o on B3 & {a2,b3,c1} on A1 & {a3,b1
,c2} on B1 & {a1,b2,c3} on C1 & {a1,b3,c2} on A2 & {a3,b2,c1} on B2 & {a2,b1,c3
} on C2 & {b1,b2,b3} on A3 & {a1,a2,a3} on B3 & {c1,c2} on C3 holds c3 on C3
by Th19;
for a,b,c,d being Point of CPS9 ex p being Point of CPS9 st a,b,p
are_collinear & c,d,p are_collinear by ANPROJ_2:def 14;
then
A2: for M,N being LINE of X ex q being POINT of X st q on M & q on N by Th14;
for p1,r2,q,r1,q1,p,r being Point of CPS9 holds (p1,r2,q are_collinear
& r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear &
p1,q1,r
are_collinear & r2,r1,r are_collinear & p,q,r are_collinear
implies (p1,r2,q1
are_collinear or p1,r2,r1 are_collinear or p1,r1,q1 are_collinear
or r2,r1,q1
are_collinear)) by ANPROJ_2:def 11;
then for p,q,r,s,a,b,c being POINT of X for L,Q,R,S,A,B,C being LINE of X
st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R
& not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r
} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C holds not c on C by Th17;
hence thesis by A1,A2;
end;
end;