:: Incidence Projective Spaces :: by Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski :: :: Received October 4, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin 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 proofend; 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 proofend; 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 ) proofend; 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 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 ) ) ) proofend; 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 proofend; 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 ) ) ) ); 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 ) proofend; theorem Th6: :: INCPROJ:6 for CPS being proper CollSp ex a9, b9, c9 being Point of CPS st ( a9 <> b9 & b9 <> c9 & c9 <> a9 ) proofend; theorem Th7: :: INCPROJ:7 for CPS being proper CollSp for a9 being Point of CPS ex b9 being Point of CPS st a9 <> b9 proofend; 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 proofend; 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 ) proofend; 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 is_collinear iff ex P being LINE of (IncProjSp_of CPS) st ( a on P & b on P & c on P ) ) proofend; 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 proofend; 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 ) proofend; theorem Th13: :: INCPROJ:13 for CPS being CollProjectiveSpace for a, b, c, d, p being POINT of (IncProjSp_of CPS) for M, N, P, Q 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 ) proofend; 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 is_collinear & c9,d9,p9 is_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 ) proofend; 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 is_collinear or not r,r1,s is_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 ) proofend; 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 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 ) proofend; 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 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 proofend; 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 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 proofend; 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 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 proofend; definition let S be IncProjStr ; attrS is partial means :Def4: :: 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 :Def5: :: 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 ) ) proofend; end; :: deftheorem Def4 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 Def5 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 ; attrS is up-2-dimensional means :Def6: :: INCPROJ:def 6 not for p being POINT of S for P being LINE of S holds p on P; attrS is up-3-rank means :Def7: :: 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 ); attrS is Vebleian means :Def8: :: 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 Def6 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 Def7 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 Def8 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 ) proofend; 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 ) proofend; 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; attrIT is 2-dimensional means :Def9: :: 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 Def9 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 ; attrIT is at_most-3-dimensional means :Def10: :: 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 Def10 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; attrIT 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 ; attrIT is Fanoian means :Def12: :: 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 Def12 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 ; attrIT is Desarguesian means :Def13: :: 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_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 Def13 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 ; attrIT is Pappian means :Def14: :: 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_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 Def14 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 ); 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; end;