:: Incidence Projective Spaces :: by Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski :: :: Received October 4, 1990 :: Copyright (c) 1990-2021 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; 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; end; definition let CPS; func ProjectiveLines(CPS) -> set equals :: INCPROJ:def 1 {B : B is LINE of CPS}; end; registration let CPS; cluster ProjectiveLines(CPS) -> non empty; end; theorem :: INCPROJ:1 x is LINE of CPS iff x is Element of ProjectiveLines(CPS); definition let CPS; func Proj_Inc(CPS) -> Relation of the carrier of CPS, ProjectiveLines(CPS) means :: 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 st y=Y & x in Y; end; definition let CPS; func IncProjSp_of(CPS) -> IncProjStr equals :: INCPROJ:def 3 IncProjStr (# the carrier of CPS , ProjectiveLines(CPS), Proj_Inc(CPS) #); end; registration let CPS; cluster IncProjSp_of(CPS) -> strict; end; theorem :: INCPROJ:2 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 x is Point of CPS iff x is POINT of IncProjSp_of(CPS); theorem :: INCPROJ:4 x is LINE of CPS iff x is LINE of IncProjSp_of(CPS); 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 :: INCPROJ:5 p = p9 & P = P9 implies (p on P iff p9 in P9); theorem :: INCPROJ:6 ex a9, b9, c9 st a9<>b9 & b9<>c9 & c9<>a9; theorem :: INCPROJ:7 ex b9 st a9<>b9; theorem :: INCPROJ:8 p on P & q on P & p on Q & q on Q implies p = q or P = Q; theorem :: INCPROJ:9 ex P st p on P & q on P; theorem :: INCPROJ:10 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); theorem :: INCPROJ:11 ex p, P st not p on P; 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 :: INCPROJ:12 ex a, b, c st a<>b & b<>c & c <>a & a on P & b on P & c on P; theorem :: INCPROJ:13 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; theorem :: INCPROJ:14 (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; theorem :: INCPROJ:15 (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; theorem :: INCPROJ:16 (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; theorem :: INCPROJ:17 (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; theorem :: INCPROJ:18 (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; theorem :: INCPROJ:19 (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; definition let S be IncProjStr; attr S is partial means :: INCPROJ:def 4 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 :: INCPROJ:def 5 for p,q being POINT of S ex P being LINE of S st p on P & q on P; end; definition let S be IncProjStr; attr S is up-2-dimensional means :: INCPROJ:def 6 ex p being POINT of S, P being LINE of S st not 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; registration let CPS be CollProjectiveSpace; cluster IncProjSp_of(CPS) -> partial linear up-2-dimensional up-3-rank Vebleian; end; registration cluster strict partial linear up-2-dimensional up-3-rank Vebleian for IncProjStr; 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; 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; 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 :: INCPROJ:def 10 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 :: INCPROJ:def 11 IT is at_most-3-dimensional up-3-dimensional; end; 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; 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; 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; registration cluster Desarguesian Fanoian at_most-3-dimensional up-3-dimensional for IncProjSp; end; registration cluster Pappian Fanoian at_most-3-dimensional up-3-dimensional for IncProjSp; end; registration cluster Desarguesian Fanoian 2-dimensional for IncProjSp; end; registration cluster Pappian Fanoian 2-dimensional for IncProjSp; end;