:: Projective {P}lanes
:: by Micha{\l} Muzalewski
::
:: Received July 28, 1994
:: Copyright (c) 1994 Association of Mizar Users
:: deftheorem Def1 defines |' PROJPL_1:def 1 :
:: deftheorem Def2 defines on PROJPL_1:def 2 :
:: deftheorem Def3 defines on PROJPL_1:def 3 :
theorem Th1: :: PROJPL_1:1
for
G being
IncProjStr for
a,
b,
c being
POINT of
G for
P,
Q,
R being
LINE of
G holds
( (
{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 ) ) )
:: deftheorem Def4 defines configuration PROJPL_1:def 4 :
theorem Th2: :: PROJPL_1:2
theorem Th3: :: PROJPL_1:3
theorem Th4: :: PROJPL_1:4
for
G being
IncProjStr holds
(
G is
IncProjSp iff (
G is
configuration & ( for
p,
q being
POINT of
G ex
P being
LINE of
G st
{p,q} on P ) & ex
p being
POINT of
G ex
P being
LINE of
G st
p |' P & ( for
P being
LINE of
G ex
a,
b,
c being
POINT of
G st
(
a,
b,
c are_mutually_different &
{a,b,c} on P ) ) & ( for
a,
b,
c,
d,
p being
POINT of
G for
M,
N,
P,
Q being
LINE of
G 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 being
POINT of
G st
q on P,
Q ) ) )
:: deftheorem Def5 defines is_collinear PROJPL_1:def 5 :
theorem Th5: :: PROJPL_1:5
theorem :: PROJPL_1:6
definition
let G be
IncProjStr ;
let a,
b,
c,
d be
POINT of
G;
pred a,
b,
c,
d is_a_quadrangle means :
Def6:
:: 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;
:: deftheorem Def6 defines is_a_quadrangle PROJPL_1:def 6 :
for
G being
IncProjStr for
a,
b,
c,
d being
POINT of
G holds
(
a,
b,
c,
d is_a_quadrangle iff (
a,
b,
c is_a_triangle &
b,
c,
d is_a_triangle &
c,
d,
a is_a_triangle &
d,
a,
b is_a_triangle ) );
theorem Th7: :: PROJPL_1:7
theorem Th8: :: PROJPL_1:8
theorem Th9: :: PROJPL_1:9
theorem Th10: :: PROJPL_1:10
theorem Th11: :: PROJPL_1:11
for
G being
IncProjStr for
a,
b,
c being
POINT of
G st
a,
b,
c is_collinear holds
(
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
for
G being
IncProjStr for
a,
b,
c being
POINT of
G st
a,
b,
c is_a_triangle holds
(
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 )
by Th11;
theorem Th13: :: PROJPL_1:13
for
G being
IncProjStr for
a,
b,
c,
d being
POINT of
G st
a,
b,
c,
d is_a_quadrangle holds
(
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 Th14: :: PROJPL_1:14
for
G being
IncProjStr for
a1,
a2,
b1,
b2 being
POINT of
G for
A,
B being
LINE of
G st
G is
configuration &
{a1,a2} on A &
{b1,b2} on B &
a1,
a2 |' B &
b1,
b2 |' A &
a1 <> a2 &
b1 <> b2 holds
a1,
a2,
b1,
b2 is_a_quadrangle
theorem Th15: :: PROJPL_1:15
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 ;
existence
ex b1 being Element of [:the Points of G,the Points of G,the Points of G,the Points of G:] st b1 `1 ,b1 `2 ,b1 `3 ,b1 `4 is_a_quadrangle
end;
:: deftheorem defines Quadrangle PROJPL_1:def 7 :
:: deftheorem Def8 defines * PROJPL_1:def 8 :
theorem Th16: :: PROJPL_1:16
theorem Th17: :: PROJPL_1:17
theorem Th18: :: PROJPL_1:18
for
G being
IncProjStr st ex
a,
b,
c,
d being
POINT of
G st
a,
b,
c,
d is_a_quadrangle holds
ex
a,
b,
c being
POINT of
G st
a,
b,
c is_a_triangle
theorem Th19: :: PROJPL_1:19
theorem Th20: :: PROJPL_1:20
for
G being
IncProjStr for
a,
b,
c,
d being
POINT of
G for
P,
Q,
R being
LINE of
G st
a,
b,
c,
d is_a_quadrangle &
{a,b} on P &
{a,c} on Q &
{a,d} on R holds
P,
Q,
R are_mutually_different
theorem Th21: :: PROJPL_1:21
for
G being
IncProjStr for
a,
p,
q,
r being
POINT of
G for
P,
Q,
R,
A being
LINE of
G st
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 holds
p,
q,
r are_mutually_different
theorem Th22: :: PROJPL_1:22
for
G being
IncProjStr st
G is
configuration & ( for
p,
q being
POINT of
G ex
M being
LINE of
G st
{p,q} on M ) & ( for
P,
Q being
LINE of
G ex
a being
POINT of
G st
a on P,
Q ) & ex
a,
b,
c,
d being
POINT of
G st
a,
b,
c,
d is_a_quadrangle holds
for
P being
LINE of
G ex
a,
b,
c being
POINT of
G st
(
a,
b,
c are_mutually_different &
{a,b,c} on P )
theorem Th23: :: PROJPL_1:23
for
G being
IncProjStr holds
(
G is
IncProjectivePlane iff (
G is
configuration & ( for
p,
q being
POINT of
G ex
M being
LINE of
G st
{p,q} on M ) & ( for
P,
Q being
LINE of
G ex
a being
POINT of
G st
a on P,
Q ) & ex
a,
b,
c,
d being
POINT of
G st
a,
b,
c,
d is_a_quadrangle ) )
:: deftheorem Def9 defines * PROJPL_1:def 9 :
theorem Th24: :: PROJPL_1:24
theorem :: PROJPL_1:25
theorem Th26: :: PROJPL_1:26
theorem :: PROJPL_1:27
theorem Th28: :: PROJPL_1:28
theorem :: PROJPL_1:29
theorem :: PROJPL_1:30
theorem :: PROJPL_1:31
theorem :: PROJPL_1:32
theorem :: PROJPL_1:33
theorem :: PROJPL_1:34
theorem Th35: :: PROJPL_1:35
theorem :: PROJPL_1:36
theorem :: PROJPL_1:37