begin
:: deftheorem defines ProjectiveLines INCPROJ:def 1 :
for CPS being proper CollSp holds ProjectiveLines CPS = { B where B is Subset of CPS : B is LINE of CPS } ;
theorem Th2:
definition
let CPS be
proper CollSp;
func Proj_Inc CPS -> Relation of the
carrier of
CPS,
(ProjectiveLines CPS) means :
Def2:
for
x,
y being
set holds
(
[x,y] in it iff (
x in the
carrier of
CPS &
y in ProjectiveLines CPS & ex
Y being
set st
(
y = Y &
x in Y ) ) );
existence
ex b1 being Relation of the carrier of CPS,(ProjectiveLines CPS) st
for x, y being set holds
( [x,y] in b1 iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) )
uniqueness
for b1, b2 being Relation of the carrier of CPS,(ProjectiveLines CPS) st ( for x, y being set holds
( [x,y] in b1 iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines Proj_Inc INCPROJ:def 2 :
for CPS being proper CollSp
for b2 being Relation of the carrier of CPS,(ProjectiveLines CPS) holds
( b2 = Proj_Inc CPS iff for x, y being set holds
( [x,y] in b2 iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st
( y = Y & x in Y ) ) ) );
:: deftheorem defines IncProjSp_of INCPROJ:def 3 :
for CPS being proper CollSp holds IncProjSp_of CPS = IncProjStr(# the carrier of CPS,(ProjectiveLines CPS),(Proj_Inc CPS) #);
theorem
theorem
theorem
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
for
CPS being
CollProjectiveSpace st ( for
p,
p1,
q,
q1,
r2 being
Point of
CPS ex
r,
r1 being
Point of
CPS st
(
p,
q,
r is_collinear &
p1,
q1,
r1 is_collinear &
r2,
r,
r1 is_collinear ) ) holds
for
a being
POINT of
(IncProjSp_of CPS) for
M,
N being
LINE of
(IncProjSp_of CPS) ex
b,
c being
POINT of
(IncProjSp_of CPS) ex
S being
LINE of
(IncProjSp_of CPS) st
(
a on S &
b on S &
c on S &
b on M &
c on N )
theorem Th21:
for
CPS being
CollProjectiveSpace st ( for
p1,
r2,
q,
r1,
q1,
p,
r being
Point of
CPS st
p1,
r2,
q is_collinear &
r1,
q1,
q is_collinear &
p1,
r1,
p is_collinear &
r2,
q1,
p is_collinear &
p1,
q1,
r is_collinear &
r2,
r1,
r is_collinear &
p,
q,
r is_collinear & not
p1,
r2,
q1 is_collinear & not
p1,
r2,
r1 is_collinear & not
p1,
r1,
q1 is_collinear holds
r2,
r1,
q1 is_collinear ) holds
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
theorem Th22:
for
CPS being
CollProjectiveSpace st ( 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 is_collinear & not
o,
p1,
p3 is_collinear & not
o,
p2,
p3 is_collinear &
p1,
p2,
r3 is_collinear &
q1,
q2,
r3 is_collinear &
p2,
p3,
r1 is_collinear &
q2,
q3,
r1 is_collinear &
p1,
p3,
r2 is_collinear &
q1,
q3,
r2 is_collinear &
o,
p1,
q1 is_collinear &
o,
p2,
q2 is_collinear &
o,
p3,
q3 is_collinear holds
r1,
r2,
r3 is_collinear ) holds
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_different &
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
theorem Th23:
for
CPS being
CollProjectiveSpace st ( 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 is_collinear &
o,
p1,
p2 is_collinear &
o,
p1,
p3 is_collinear &
o,
q1,
q2 is_collinear &
o,
q1,
q3 is_collinear &
p1,
q2,
r3 is_collinear &
q1,
p2,
r3 is_collinear &
p1,
q3,
r2 is_collinear &
p3,
q1,
r2 is_collinear &
p2,
q3,
r1 is_collinear &
p3,
q2,
r1 is_collinear holds
r1,
r2,
r3 is_collinear ) holds
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_different &
o,
b1,
b2,
b3 are_mutually_different &
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
:: deftheorem Def9 defines partial INCPROJ:def 4 :
for S being IncProjStr holds
( S is partial iff for p, q being POINT of S
for P, Q being LINE of S st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q );
:: deftheorem Def10 defines linear INCPROJ:def 5 :
for S being IncProjStr holds
( S is linear iff for p, q being POINT of S ex P being LINE of S st
( p on P & q on P ) );
definition
let S be
IncProjStr ;
attr S is
up-2-dimensional means :
Def11:
not for
p being
POINT of
S for
P being
LINE of
S holds
p on P;
attr S is
up-3-rank means :
Def12:
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 :
Def13:
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;
:: deftheorem Def11 defines up-2-dimensional INCPROJ:def 6 :
for S being IncProjStr holds
( S is up-2-dimensional iff not for p being POINT of S
for P being LINE of S holds p on P );
:: deftheorem Def12 defines up-3-rank INCPROJ:def 7 :
for S being IncProjStr holds
( S is up-3-rank iff 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 ) );
:: deftheorem Def13 defines Vebleian INCPROJ:def 8 :
for S being IncProjStr holds
( S is Vebleian iff 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 ) );
:: deftheorem Def14 defines 2-dimensional INCPROJ:def 9 :
for IT being IncProjSp holds
( IT is 2-dimensional iff for M, N being LINE of IT ex q being POINT of IT st
( q on M & q on N ) );
:: deftheorem Def16 defines at_most-3-dimensional INCPROJ:def 10 :
for IT being IncProjStr holds
( IT is at_most-3-dimensional iff for a being POINT of IT
for M, N being LINE of IT ex b, c being POINT of IT ex S being LINE of IT st
( a on S & b on S & c on S & b on M & c on N ) );
:: deftheorem defines 3-dimensional INCPROJ:def 11 :
for IT being IncProjSp holds
( IT is 3-dimensional iff ( IT is at_most-3-dimensional & not IT is 2-dimensional ) );
definition
let IT be
IncProjStr ;
attr IT is
Fanoian means :
Def18:
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;
:: deftheorem Def18 defines Fanoian INCPROJ:def 12 :
for IT being IncProjStr holds
( IT is Fanoian iff 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 );
definition
let IT be
IncProjStr ;
attr IT is
Desarguesian means :
Def19:
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_different &
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;
:: deftheorem Def19 defines Desarguesian INCPROJ:def 13 :
for IT being IncProjStr holds
( IT is Desarguesian iff 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_different & 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 );
definition
let IT be
IncProjStr ;
attr IT is
Pappian means :
Def20:
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_different &
o,
b1,
b2,
b3 are_mutually_different &
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;
:: deftheorem Def20 defines Pappian INCPROJ:def 14 :
for IT being IncProjStr holds
( IT is Pappian iff 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_different & o,b1,b2,b3 are_mutually_different & 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 );