The Mizar abstract of INCPROJ

Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users
The abstract of the Mizar article:: Incidence Projective Spaces
by
Wojciech Leonczuk, and
Krzysztof Prazmowski
Received October 4, 1990
MML identifier: INCPROJ
[ Mizar article, MML identifier index ]
environ

 vocabulary COLLSP, PRE_TOPC, INCSP_1, RELAT_1, ANPROJ_2, ANALOAF, VECTSP_1,
      AFF_2, INCPROJ;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELSET_1, STRUCT_0, PRE_TOPC,
      INCSP_1, COLLSP, ANPROJ_2;
 constructors INCSP_1, ANPROJ_2, DOMAIN_1, XBOOLE_0;
 clusters ANPROJ_2, RELSET_1, STRUCT_0, SUBSET_1, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

reserve CPS for proper CollSp,
        B for Element of bool the carrier of CPS,
        p for Point of CPS,
        x, y, z, Y for set;

definition let CPS;
  redefine mode LINE of CPS -> Element of bool the carrier of CPS;
end;

definition let CPS;
  func ProjectiveLines(CPS) -> set equals
:: INCPROJ:def 1
   {B : B is LINE of CPS};
end;

definition let CPS;
 cluster ProjectiveLines(CPS) -> non empty;
end;

canceled;

theorem :: INCPROJ:2
  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 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;

definition let CPS;
  cluster IncProjSp_of(CPS) -> strict;
end;

canceled;

theorem :: INCPROJ:4
  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:5
   x is Point of CPS iff x is POINT of IncProjSp_of(CPS);

theorem :: INCPROJ:6
  x is LINE of CPS iff x is LINE of IncProjSp_of(CPS);

reserve a,b,c,p,q,s for POINT of IncProjSp_of(CPS),
        P,Q,S for LINE of IncProjSp_of(CPS),
        a',b',c',p',q',r' for Point of CPS,
        P' for LINE of CPS;

canceled;

theorem :: INCPROJ:8
  s on S iff [s,S] in Proj_Inc(CPS);

theorem :: INCPROJ:9
  p = p' & P = P' implies (p on P iff p' in P');

theorem :: INCPROJ:10
  ex a', b', c' st a'<>b' & b'<>c' & c'<>a';

theorem :: INCPROJ:11
  ex b' st a'<>b';

theorem :: INCPROJ:12
  p on P & q on P & p on Q & q on Q implies p = q or P = Q;

theorem :: INCPROJ:13
  ex P st p on P & q on P;

theorem :: INCPROJ:14
  a = a' & b = b' & c = c'
    implies
   (a',b',c' is_collinear iff ex P st a on P & b on P & c on P);

theorem :: INCPROJ:15
  ex p, P st not p on P;

reserve CPS for CollProjectiveSpace;

reserve a,b,c,d,p,q for POINT of IncProjSp_of(CPS),
        P,Q,S,M,N for LINE of IncProjSp_of(CPS),
        a',b',c',d',p',q' for Point of CPS;

theorem :: INCPROJ:16
  ex a, b, c st a<>b & b<>c & c <>a & a on P & b on P & c on P;

theorem :: INCPROJ:17
  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:18
  (for a',b',c',d' ex p' st a', b', p' is_collinear & c', d', p' is_collinear)
    implies
   for M, N ex q st q on M & q on N;

theorem :: INCPROJ:19
  (ex p, p1, r, r1 being Point of CPS st not ex s being Point of CPS st
   (p, p1, s is_collinear & r, r1, s is_collinear))
     implies
    (ex M, N st not ex q st q on M & q on N);

theorem :: INCPROJ:20
  (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)
      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);

definition let x, y, z be set;
 canceled;

  pred x,y,z are_mutually_different means
:: INCPROJ:def 5

  x <> y & y <> z & z <> x;

  let u be set;
  pred x, y, z, u are_mutually_different means
:: INCPROJ:def 6

  x <> y & y <> z & z <> x & u <> x & u <> y & u <> z;
end;

definition
  let CS be IncProjStr, a,b be POINT of CS,
   M be LINE of CS;
  pred a,b on M means
:: INCPROJ:def 7

  a on M & b on M;

  let c be POINT of CS;
  pred a,b,c on M means
:: INCPROJ:def 8

  a on M & b on M & c on M;
end;

theorem :: INCPROJ:21
  (for p1, r2, q, r1, q1, p, r being Point of CPS holds
   (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
      implies
     (p1,r2,q1 is_collinear or p1,r2,r1 is_collinear or
      p1,r1,q1 is_collinear or r2,r1,q1 is_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 &
      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);

theorem :: INCPROJ:22
  (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)
 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_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 :: INCPROJ:23
  (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)
 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_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);

definition let IT be IncProjStr;
  attr IT is partial means
:: INCPROJ:def 9

  for p, q being POINT of IT, P, Q being LINE of IT st
   p on P & q on P & p on Q & q on Q holds
   p = q or P = Q;

  attr IT is linear means
:: INCPROJ:def 10

  for p,q being POINT of IT ex P being LINE of IT st p on P & q on P;

  attr IT is up-2-dimensional means
:: INCPROJ:def 11

  ex p being POINT of IT, P being LINE of IT st not p on P;

  attr IT is up-3-rank means
:: INCPROJ:def 12

  for P being LINE of IT ex a, b, c being POINT of IT st
   a <> b & b <> c & c <> a & a on P & b on P & c on P;

  attr IT is Vebleian means
:: INCPROJ:def 13

  for a, b, c, d, p, q being POINT of IT
  for M, N, P, Q being LINE of IT 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 IT st q on P & q on Q;
end;

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

definition
  cluster strict partial linear up-2-dimensional up-3-rank
   Vebleian IncProjStr;
end;

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

definition
  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 14

  for M,N being LINE of IT ex q being POINT of IT st q on M & q on N;
  antonym IT is up-3-dimensional;
end;

definition
  let IT be IncProjSp;
 canceled;

  attr IT is at_most-3-dimensional means
:: INCPROJ:def 16

  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 17
    IT is at_most-3-dimensional up-3-dimensional;
end;

definition let IT be IncProjSp;
  attr IT is Fanoian means
:: INCPROJ:def 18

  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 IncProjSp;
  attr IT is Desarguesian means
:: INCPROJ:def 19

  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;

definition let IT be IncProjSp;
  attr IT is Pappian means
:: INCPROJ:def 20

  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;

definition
  cluster Desarguesian Fanoian at_most-3-dimensional up-3-dimensional
    IncProjSp;
end;

definition
  cluster Pappian Fanoian at_most-3-dimensional up-3-dimensional
    IncProjSp;
end;

definition
  cluster Desarguesian Fanoian 2-dimensional IncProjSp;
end;

definition
  cluster Pappian Fanoian 2-dimensional IncProjSp;
end;
The abstract of the Mizar article:

Incidence Projective Spaces
