:: Incidence Projective Spaces
:: by Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski
::
:: Received October 4, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users


definition
let CPS be proper CollSp;
:: original: LINE
redefine mode LINE of CPS -> Subset of CPS;
coherence
for b1 being LINE of CPS holds b1 is Subset of CPS
proof end;
end;

definition
let CPS be proper CollSp;
func ProjectiveLines CPS -> set equals :: INCPROJ:def 1
 { B where B is Subset of CPS : B is LINE of CPS } ;
coherence
{ B where B is Subset of CPS : B is LINE of CPS } is set ;
end;

:: 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 } ;

registration
let CPS be proper CollSp;
cluster ProjectiveLines CPS -> non empty ;
coherence
not ProjectiveLines CPS is empty
proof end;
end;

theorem Th1: :: INCPROJ:1
for CPS being proper CollSp
for x being set holds
( x is LINE of CPS iff x is Element of ProjectiveLines CPS )
proof end;

definition
let CPS be proper CollSp;
func Proj_Inc CPS -> Relation of the carrier of CPS,(ProjectiveLines CPS) means :Def2: :: INCPROJ:def 2
 for x, y being object 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 object 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 ) ) )
proof end;
uniqueness
for b1, b2 being Relation of the carrier of CPS,(ProjectiveLines CPS) st ( for x, y being object 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 object 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
proof end;
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 object 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 ) ) ) );

definition
let CPS be proper CollSp;
func IncProjSp_of CPS -> IncProjStr equals :: INCPROJ:def 3
 IncProjStr(# the carrier of CPS,(ProjectiveLines CPS),(Proj_Inc CPS) #);
coherence
IncProjStr(# the carrier of CPS,(ProjectiveLines CPS),(Proj_Inc CPS) #) is IncProjStr ;
end;

:: 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) #);

registration
let CPS be proper CollSp;
cluster IncProjSp_of CPS -> strict ;
coherence
IncProjSp_of CPS is strict ;
end;

theorem :: INCPROJ:2
for CPS being proper CollSp holds
( 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 :: INCPROJ:3
for CPS being proper CollSp
for x being set holds
( x is Point of CPS iff x is POINT of (IncProjSp_of CPS) ) ;

theorem :: INCPROJ:4
for CPS being proper CollSp
for x being set holds
( x is LINE of CPS iff x is LINE of (IncProjSp_of CPS) ) by Th1;

theorem Th5: :: INCPROJ:5
for CPS being proper CollSp
for p being POINT of (IncProjSp_of CPS)
for P being LINE of (IncProjSp_of CPS)
for p9 being Point of CPS
for P9 being LINE of CPS st p = p9 & P = P9 holds
( p on P iff p9 in P9 )
proof end;

theorem Th6: :: INCPROJ:6
for CPS being proper CollSp ex a9, b9, c9 being Point of CPS st
( a9 <> b9 & b9 <> c9 & c9 <> a9 )
proof end;

theorem Th7: :: INCPROJ:7
for CPS being proper CollSp
for a9 being Point of CPS ex b9 being Point of CPS st a9 <> b9
proof end;

theorem Th8: :: INCPROJ:8
for CPS being proper CollSp
for p, q being POINT of (IncProjSp_of CPS)
for P, Q being LINE of (IncProjSp_of CPS) st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q
proof end;

theorem Th9: :: INCPROJ:9
for CPS being proper CollSp
for p, q being POINT of (IncProjSp_of CPS) ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P )
proof end;

theorem Th10: :: INCPROJ:10
for CPS being proper CollSp
for a, b, c being POINT of (IncProjSp_of CPS)
for a9, b9, c9 being Point of CPS st a = a9 & b = b9 & c = c9 holds
( a9,b9,c9 are_collinear iff ex P being LINE of (IncProjSp_of CPS) st
( a on P & b on P & c on P ) )
proof end;

theorem Th11: :: INCPROJ:11
for CPS being proper CollSp holds
not for p being POINT of (IncProjSp_of CPS)
for P being LINE of (IncProjSp_of CPS) holds p on P
proof end;

theorem Th12: :: INCPROJ:12
for CPS being CollProjectiveSpace
for P being LINE of (IncProjSp_of CPS) ex a, b, c being POINT of (IncProjSp_of CPS) st
( a <> b & b <> c & c <> a & a on P & b on P & c on P )
proof end;

theorem Th13: :: INCPROJ:13
for CPS being CollProjectiveSpace
for a, b, c, d, p being POINT of (IncProjSp_of CPS)
for P, Q, M, N being LINE of (IncProjSp_of CPS) 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 (IncProjSp_of CPS) st
( q on P & q on Q )
proof end;

theorem Th14: :: INCPROJ:14
for CPS being CollProjectiveSpace st ( for a9, b9, c9, d9 being Point of CPS ex p9 being Point of CPS st
( a9,b9,p9 are_collinear & c9,d9,p9 are_collinear ) ) holds
for M, N being LINE of (IncProjSp_of CPS) ex q being POINT of (IncProjSp_of CPS) st
( q on M & q on N )
proof end;

theorem Th15: :: INCPROJ:15
for CPS being CollProjectiveSpace st ex p, p1, r, r1 being Point of CPS st
for s being Point of CPS holds
( not p,p1,s are_collinear or not r,r1,s are_collinear ) holds
ex M, N being LINE of (IncProjSp_of CPS) st
for q being POINT of (IncProjSp_of CPS) holds
( not q on M or not q on N )
proof end;

theorem Th16: :: INCPROJ:16
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 are_collinear & p1,q1,r1 are_collinear & r2,r,r1 are_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 )
proof end;

theorem Th17: :: INCPROJ:17
for CPS being CollProjectiveSpace st ( for p1, r2, q, r1, q1, p, r being Point of CPS st 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 & not p1,r2,q1 are_collinear & not p1,r2,r1 are_collinear & not p1,r1,q1 are_collinear holds
r2,r1,q1 are_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
proof end;

theorem Th18: :: INCPROJ:18
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 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 ) 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_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 end;

theorem Th19: :: INCPROJ:19
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 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 ) 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_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 end;

definition
let S be IncProjStr ;
attr S is partial means :: INCPROJ:def 4
 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;
redefine attr S is linear means :: INCPROJ:def 5
 for p, q being POINT of S ex P being LINE of S st
( p on P & q on P );
compatibility
( S is linear iff for p, q being POINT of S ex P being LINE of S st
( p on P & q on P ) )
proof end;
end;

:: deftheorem 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 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 :: INCPROJ:def 6
 not for p being POINT of S
for P being LINE of S holds p on P;
attr S is up-3-rank means :: INCPROJ:def 7
 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 :: INCPROJ:def 8
 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 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 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 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 ) );

registration
let CPS be CollProjectiveSpace;
cluster IncProjSp_of CPS -> linear partial up-2-dimensional up-3-rank Vebleian ;
coherence
( IncProjSp_of CPS is partial & IncProjSp_of CPS is linear & IncProjSp_of CPS is up-2-dimensional & IncProjSp_of CPS is up-3-rank & IncProjSp_of CPS is Vebleian ) by Th13, Th11, Th12, Th8, Th9;
end;

registration
cluster strict linear partial up-2-dimensional up-3-rank Vebleian for IncProjStr ;
existence
ex b1 being IncProjStr st
( b1 is strict & b1 is partial & b1 is linear & b1 is up-2-dimensional & b1 is up-3-rank & b1 is Vebleian )
proof end;
end;

definition
mode IncProjSp is linear partial up-2-dimensional up-3-rank Vebleian IncProjStr ;
end;

registration
let CPS be CollProjectiveSpace;
cluster IncProjSp_of CPS -> linear partial up-2-dimensional up-3-rank Vebleian ;
coherence
( IncProjSp_of CPS is partial & IncProjSp_of CPS is linear & IncProjSp_of CPS is up-2-dimensional & IncProjSp_of CPS is up-3-rank & IncProjSp_of CPS is Vebleian ) ;
end;

definition
let IT be IncProjSp;
attr IT is 2-dimensional means :: INCPROJ:def 9
 for M, N being LINE of IT ex q being POINT of IT st
( q on M & q on N );
end;

:: deftheorem 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 ) );

notation
let IT be IncProjSp;
antonym up-3-dimensional IT for 2-dimensional ;
end;

definition
let IT be IncProjStr ;
attr IT is at_most-3-dimensional means :: INCPROJ:def 10
 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 );
end;

:: deftheorem 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 ) );

definition
let IT be IncProjSp;
attr IT is 3-dimensional means :: INCPROJ:def 11
( IT is at_most-3-dimensional & IT is up-3-dimensional );
end;

:: deftheorem defines 3-dimensional INCPROJ:def 11 :
for IT being IncProjSp holds
( IT is 3-dimensional iff ( IT is at_most-3-dimensional & IT is up-3-dimensional ) );

definition
let IT be IncProjStr ;
attr IT is Fanoian means :: INCPROJ:def 12
 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 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 :: INCPROJ:def 13
 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;

:: deftheorem 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_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 );

definition
let IT be IncProjStr ;
attr IT is Pappian means :: INCPROJ:def 14
 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;

:: deftheorem 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_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 );

registration
cluster linear partial up-2-dimensional up-3-rank Vebleian up-3-dimensional at_most-3-dimensional Fanoian Desarguesian for IncProjStr ;
existence
ex b1 being IncProjSp st
( b1 is Desarguesian & b1 is Fanoian & b1 is at_most-3-dimensional & b1 is up-3-dimensional )
proof end;
end;

registration
cluster linear partial up-2-dimensional up-3-rank Vebleian up-3-dimensional at_most-3-dimensional Fanoian Pappian for IncProjStr ;
existence
ex b1 being IncProjSp st
( b1 is Pappian & b1 is Fanoian & b1 is at_most-3-dimensional & b1 is up-3-dimensional )
proof end;
end;

registration
cluster linear partial up-2-dimensional up-3-rank Vebleian 2-dimensional Fanoian Desarguesian for IncProjStr ;
existence
ex b1 being IncProjSp st
( b1 is Desarguesian & b1 is Fanoian & b1 is 2-dimensional )
proof end;
end;

registration
cluster linear partial up-2-dimensional up-3-rank Vebleian 2-dimensional Fanoian Pappian for IncProjStr ;
existence
ex b1 being IncProjSp st
( b1 is Pappian & b1 is Fanoian & b1 is 2-dimensional )
proof end;
end;