The abstract of the Mizar article:

Projective Planes

by

Michal Muzalewski

Received July 28, 1994

MML identifier: PROJPL_1

[ Mizar article, MML identifier index ]

environ

 vocabulary INCSP_1, INCPROJ, ANALOAF, MCART_1, PROJPL_1;
 notation ZFMISC_1, SUBSET_1, MCART_1, DOMAIN_1, INCSP_1, INCPROJ;
 constructors DOMAIN_1, INCPROJ, MEMBERED, XBOOLE_0;
 clusters INCPROJ, MEMBERED, ZFMISC_1, XBOOLE_0;


begin

 reserve G for IncProjStr;

                       ::
                       ::    1. PROJECTIVE SPACES
                       ::

 reserve a,a1,a2,b,b1,b2,c,d,p,q,r for POINT of G;
 reserve A,B,C,D,M,N,P,Q,R for LINE of G;

definition let G,a,P;
  redefine pred a on P;
  antonym a|'P;
end;

definition let G,a,b,P;
  pred a,b|'P means
:: PROJPL_1:def 1
 a|'P & b|'P;
end;

definition let G,a,P,Q;
  pred a on P,Q means
:: PROJPL_1:def 2
 a on P & a on Q;
end;

definition let G,a,P,Q,R;
  pred a on P,Q,R means
:: PROJPL_1:def 3
 a on P & a on Q & a on R;
end;

theorem :: PROJPL_1:1
 (a,b on P implies b,a on P)
 & (a,b,c on P implies a,c,b on P & b,a,c on P & b,c,a on P & c,a,b on P &
 c,b,a on P)
 & (a on P,Q implies a on Q,P)
 & (a on P,Q,R implies a on P,R,Q & a on Q,P,R & a on Q,R,P &
    a on R,P,Q & a on R,Q,P);

definition let IT be IncProjStr;
 attr IT is configuration means
:: PROJPL_1:def 4
  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;
end;

theorem :: PROJPL_1:2
 G is configuration iff for p,q,P,Q st p,q on P & p,q on Q holds
  p = q or P = Q;

theorem :: PROJPL_1:3
 G is configuration iff
  for p,q,P,Q st p on P,Q & q on P,Q holds p = q or P = Q;

theorem :: PROJPL_1:4
 G is IncProjSp iff
   G is configuration
 & (for p,q ex P st p,q on P)
 & (ex p,P st p|'P)
 & (for P ex a,b,c st a,b,c are_mutually_different & a,b,c on P)
 & (for a,b,c,d,p,M,N,P,Q st a,b,p on M & c,d,p on N & a,c on P & b,d on Q &
 p|'P & p|'Q
    & M<>N holds ex q st q on P,Q);

definition
  mode IncProjectivePlane is 2-dimensional IncProjSp;
end;

definition let G,a,b,c;
  pred a,b,c is_collinear means
:: PROJPL_1:def 5
 ex P st a,b,c on P;
  antonym a,b,c is_a_triangle;
end;

theorem :: PROJPL_1:5
  a,b,c is_collinear iff ex P st a on P & b on P & c on P;

theorem :: PROJPL_1:6
   a,b,c is_a_triangle iff for P holds a|'P or b|'P or c|'P;

definition let G,a,b,c,d;
  pred a,b,c,d is_a_quadrangle means
:: PROJPL_1:def 6
 a,b,c is_a_triangle
   & b,c,d is_a_triangle
   & c,d,a is_a_triangle
   & d,a,b is_a_triangle;
end;

theorem :: PROJPL_1:7
  G is IncProjSp implies ex A,B st A<>B;

theorem :: PROJPL_1:8
  G is IncProjSp & a on A implies
        ex b,c st b,c on A & a,b,c are_mutually_different;

theorem :: PROJPL_1:9
  G is IncProjSp & a on A & A<>B implies
        ex b st b on A & b|'B & a<>b;

theorem :: PROJPL_1:10
  G is configuration & a1,a2 on A & a1<>a2 & b|'A
         implies a1,a2,b is_a_triangle;

theorem :: PROJPL_1:11
  a,b,c is_collinear implies
          a,c,b is_collinear
        & b,a,c is_collinear
        & b,c,a is_collinear
        & c,a,b is_collinear
        & c,b,a is_collinear;

theorem :: PROJPL_1:12
   a,b,c is_a_triangle implies
          a,c,b is_a_triangle
        & b,a,c is_a_triangle
        & b,c,a is_a_triangle
        & c,a,b is_a_triangle
        & c,b,a is_a_triangle;

theorem :: PROJPL_1:13
 a,b,c,d is_a_quadrangle implies
          a,c,b,d is_a_quadrangle & b,a,c,d is_a_quadrangle
        & b,c,a,d is_a_quadrangle & c,a,b,d is_a_quadrangle
        & c,b,a,d is_a_quadrangle & a,b,d,c is_a_quadrangle
        & a,c,d,b is_a_quadrangle & b,a,d,c is_a_quadrangle
        & b,c,d,a is_a_quadrangle & c,a,d,b is_a_quadrangle
        & c,b,d,a is_a_quadrangle & a,d,b,c is_a_quadrangle
        & a,d,c,b is_a_quadrangle & b,d,a,c is_a_quadrangle
        & b,d,c,a is_a_quadrangle & c,d,a,b is_a_quadrangle
        & c,d,b,a is_a_quadrangle & d,a,b,c is_a_quadrangle
        & d,a,c,b is_a_quadrangle & d,b,a,c is_a_quadrangle
        & d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle
        & d,c,b,a is_a_quadrangle;

theorem :: PROJPL_1:14
  G is configuration & a1,a2 on A & b1,b2 on B & a1,a2|'B & b1,b2|'A
        & a1<>a2 & b1<>b2 implies a1,a2,b1,b2 is_a_quadrangle;

theorem :: PROJPL_1:15
  G is IncProjSp implies ex a,b,c,d st a,b,c,d is_a_quadrangle;

definition let G be IncProjSp;
  mode Quadrangle of G -> Element of
   [:the Points of G,the Points of G,the Points of G,the Points of G:] means
:: PROJPL_1:def 7
   it`1,it`2,it`3,it`4 is_a_quadrangle;
end;

definition let G be IncProjSp, a,b be POINT of G;
  assume  a <> b;
  func a*b -> LINE of G means
:: PROJPL_1:def 8
 a,b on it;
end;

theorem :: PROJPL_1:16
for G be IncProjSp, a,b be POINT of G, L be LINE of G
 st a <> b holds a on a*b & b on a*b & a*b = b*a &
 (a on L & b on L implies L = a*b);

                       ::
                       ::    2. PROJECTIVE PLANES
                       ::
begin

theorem :: PROJPL_1:17
 (ex a,b,c st a,b,c is_a_triangle) & (for p,q ex M st p,q on M)
 implies ex p,P st p|'P;

theorem :: PROJPL_1:18
 (ex a,b,c,d st a,b,c,d is_a_quadrangle)
 implies (ex a,b,c st a,b,c is_a_triangle);

theorem :: PROJPL_1:19
 a,b,c is_a_triangle & a,b on P & a,c on Q implies P<>Q;

theorem :: PROJPL_1:20
 a,b,c,d is_a_quadrangle & a,b on P & a,c on Q & a,d on R
       implies P,Q,R are_mutually_different;

theorem :: PROJPL_1:21
 G is configuration
    & a on P,Q,R & P,Q,R are_mutually_different &
     a|'A & p on A,P & q on A,Q & r on A,R
     implies p,q,r are_mutually_different;

theorem :: PROJPL_1:22
 G is configuration
    & (for p,q ex M st p,q on M)
    & (for P,Q ex a st a on P,Q)
    & (ex a,b,c,d st a,b,c,d is_a_quadrangle)
     implies for P ex a,b,c st a,b,c are_mutually_different & a,b,c on P;

theorem :: PROJPL_1:23
  G is IncProjectivePlane iff
   G is configuration
 & (for p,q ex M st p,q on M)
 & (for P,Q ex a st a on P,Q)
 & (ex a,b,c,d st a,b,c,d is_a_quadrangle);

reserve G for IncProjectivePlane;

reserve a,q for POINT of G;
reserve A,B for LINE of G;

definition let G,A,B;
  assume  A <> B;
  func A*B -> POINT of G means
:: PROJPL_1:def 9
 it on A,B;
end;

theorem :: PROJPL_1:24
A <> B implies A*B on A & A*B on B & A*B = B*A
                            & (a on A & a on B implies a=A*B);

theorem :: PROJPL_1:25
A<>B & a on A & q|'A & a<>A*B implies (q*a)*B on B & (q*a)*B|'A;

                       ::
                       ::    3. SOME USEFUL PROPOSITIONS
                       ::

begin

reserve G for IncProjSp;

reserve a,b,c,d for POINT of G;
reserve P for LINE of G;

theorem :: PROJPL_1:26
 a,b,c is_a_triangle implies a,b,c are_mutually_different;

theorem :: PROJPL_1:27
   a,b,c,d is_a_quadrangle implies a,b,c,d are_mutually_different;

reserve G for IncProjectivePlane;




theorem :: PROJPL_1:28
for a,b,c,d being POINT of G st a*c = b*d
 holds a = c or b = d or c = d or a*c = c*d;

theorem :: PROJPL_1:29
for a,b,c,d being POINT of G st a*c = b*d
 holds a = c or b = d or c = d or a on c*d;

theorem :: PROJPL_1:30
   for G being IncProjectivePlane, e,m,m' being POINT of G,
I being LINE of G st m on I & m' on I & m<>m' & e|'I holds
  m*e<>m'*e & e*m<>e*m';

theorem :: PROJPL_1:31
   for G being IncProjectivePlane, e being POINT of G,
I,L1,L2 being LINE of G st e on L1 & e on L2 & L1<>L2 & e|'I
holds I*L1<>I*L2 & L1*I<>L2*I;

theorem :: PROJPL_1:32
  for G being IncProjSp, a,b,q,q1 being POINT of G
  st q on a*b & q on a*q1 & q<>a & q1<>a & a<>b holds q1 on a*b;

theorem :: PROJPL_1:33
  for G being IncProjSp, a,b,c being POINT of G
  st c on a*b & a<>c holds b on a*c;

theorem :: PROJPL_1:34
  for G being IncProjectivePlane, q1,q2,r1,r2 being POINT of G,
 H being LINE of G st r1<>r2 & r1 on H & r2 on H & q1|'H & q2|'H
  holds q1*r1<>q2*r2;

theorem :: PROJPL_1:35
 for a,b,c being POINT of G st a on b*c holds a=c or b=c or b on c*a;

theorem :: PROJPL_1:36
   for a,b,c being POINT of G st a on b*c holds b=a or b=c or c on b*a;

theorem :: PROJPL_1:37
for e,x1,x2,p1,p2 being POINT of G for H,I being LINE of G
 st x1 on I & x2 on I & e on H & e |'I & x1<>x2 & p1<>e & p2 <>e &
   p1 on e*x1 & p2 on e*x2
 holds ex r being POINT of G st r on p1*p2 & r on H & r<>e;