Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

### Projective Planes

by
Michal Muzalewski

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

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

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;

```