:: Projective {P}lanes
:: by Micha{\l} Muzalewski
::
:: Received July 28, 1994
:: Copyright (c) 1994-2011 Association of Mizar Users

begin

notation

let G be IncProjStr ;
let a be POINT of G;
let P be LINE of G;
antonym a |' P for a on P;

end;

definition

let G be IncProjStr ;
let a, b be POINT of G;
let P be LINE of G;
pred a,b |' P means :Def1: :: PROJPL_1:def 1
( a |' P & b |' P );

end;

:: deftheorem Def1 defines |' PROJPL_1:def 1 :
for G being IncProjStr
for a, b being POINT of G
for P being LINE of G holds
( a,b |' P iff ( a |' P & b |' P ) );

definition

let G be IncProjStr ;
let a be POINT of G;
let P, Q be LINE of G;
pred a on P,Q means :Def2: :: PROJPL_1:def 2
( a on P & a on Q );

end;

:: deftheorem Def2 defines on PROJPL_1:def 2 :
for G being IncProjStr
for a being POINT of G
for P, Q being LINE of G holds
( a on P,Q iff ( a on P & a on Q ) );

definition

let G be IncProjStr ;
let a be POINT of G;
let P, Q, R be LINE of G;
pred a on P,Q,R means :Def3: :: PROJPL_1:def 3
( a on P & a on Q & a on R );

end;

:: deftheorem Def3 defines on PROJPL_1:def 3 :
for G being IncProjStr
for a being POINT of G
for P, Q, R being LINE of G holds
( a on P,Q,R iff ( a on P & a on Q & a on R ) );

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

proof end;

definition

let IT be IncProjStr ;
attr IT is configuration means :Def4: :: PROJPL_1:def 4
for p, q being POINT of IT
for P, Q being LINE of IT st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q;

end;

:: deftheorem Def4 defines configuration PROJPL_1:def 4 :
for IT being IncProjStr holds
( IT is configuration iff for p, q being POINT of IT
for P, Q being LINE of IT st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q );

theorem Th2: :: PROJPL_1:2

for G being IncProjStr holds
( G is configuration iff for p, q being POINT of G
for P, Q being LINE of G st {p,q} on P & {p,q} on Q & not p = q holds
P = Q )

proof end;

theorem Th3: :: PROJPL_1:3

for G being IncProjStr holds
( G is configuration iff for p, q being POINT of G
for P, Q being LINE of G st p on P,Q & q on P,Q & not p = q holds
P = Q )

proof end;

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

proof end;

definition

mode IncProjectivePlane is 2-dimensional IncProjSp;

end;

definition

let G be IncProjStr ;
let a, b, c be POINT of G;
pred a,b,c is_collinear means :Def5: :: PROJPL_1:def 5
ex P being LINE of G st {a,b,c} on P;

end;

:: deftheorem Def5 defines is_collinear PROJPL_1:def 5 :
for G being IncProjStr
for a, b, c being POINT of G holds
( a,b,c is_collinear iff ex P being LINE of G st {a,b,c} on P );

notation

let G be IncProjStr ;
let a, b, c be POINT of G;
antonym a,b,c is_a_triangle for a,b,c is_collinear ;

end;

theorem Th5: :: PROJPL_1:5

for G being IncProjStr
for a, b, c being POINT of G holds
( a,b,c is_collinear iff ex P being LINE of G st
( a on P & b on P & c on P ) )

proof end;

theorem :: PROJPL_1:6

for G being IncProjStr
for a, b, c being POINT of G holds
( a,b,c is_a_triangle iff for P being LINE of G holds
( a |' P or b |' P or c |' P ) ) by Th5;

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

for G being IncProjStr st G is IncProjSp holds
ex A, B being LINE of G st A <> B

proof end;

theorem Th8: :: PROJPL_1:8

for G being IncProjStr
for a being POINT of G
for A being LINE of G st G is IncProjSp holds
ex b, c being POINT of G st
( {b,c} on A & a,b,c are_mutually_different )

proof end;

theorem Th9: :: PROJPL_1:9

for G being IncProjStr
for a being POINT of G
for A, B being LINE of G st G is IncProjSp & A <> B holds
ex b being POINT of G st
( b on A & b |' B & a <> b )

proof end;

theorem Th10: :: PROJPL_1:10

for G being IncProjStr
for a1, a2, b being POINT of G
for A being LINE of G st G is configuration & {a1,a2} on A & a1 <> a2 & b |' A holds
a1,a2,b is_a_triangle

proof end;

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 )

proof end;

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 )

proof end;

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

proof end;

theorem Th15: :: PROJPL_1:15

for G being IncProjStr st G is IncProjSp holds
ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle

proof end;

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 b₁ being Element of [: the Points of G, the Points of G, the Points of G, the Points of G:] st b₁ `1 ,b<sub>1</sub> `2 ,b₁ `3 ,b<sub>1</sub> `4 is_a_quadrangle

proof end;

end;

:: deftheorem defines Quadrangle PROJPL_1:def 7 :
for G being IncProjSp
for b₂ being Element of [: the Points of G, the Points of G, the Points of G, the Points of G:] holds
( b₂ is Quadrangle of G iff b₂ `1 ,b<sub>2</sub> `2 ,b₂ `3 ,b<sub>2</sub> `4 is_a_quadrangle );

definition

let G be IncProjSp;
let a, b be POINT of G;
assume A1: a <> b ;
func a * b -> LINE of G means :Def8: :: PROJPL_1:def 8
{a,b} on it;
existence
ex b₁ being LINE of G st {a,b} on b₁ by Th4;
uniqueness
for b₁, b₂ being LINE of G st {a,b} on b₁ & {a,b} on b₂ holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines * PROJPL_1:def 8 :
for G being IncProjSp
for a, b being POINT of G st a <> b holds
for b₄ being LINE of G holds
( b₄ = a * b iff {a,b} on b₄ );

theorem Th16: :: PROJPL_1:16

for G being IncProjSp
for a, b being POINT of G
for L being 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 ) )

proof end;

begin

theorem Th17: :: PROJPL_1:17

for G being IncProjStr st ex a, b, c being POINT of G st a,b,c is_a_triangle & ( for p, q being POINT of G ex M being LINE of G st {p,q} on M ) holds
ex p being POINT of G ex P being LINE of G st p |' P

proof end;

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

proof end;

theorem Th19: :: PROJPL_1:19

for G being IncProjStr
for a, b, c being POINT of G
for P, Q being LINE of G st a,b,c is_a_triangle & {a,b} on P & {a,c} on Q holds
P <> Q

proof end;

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

proof end;

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

proof end;

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 )

proof end;

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

proof end;

definition

let G be IncProjectivePlane;
let A, B be LINE of G;
assume A1: A <> B ;
func A * B -> POINT of G means :Def9: :: PROJPL_1:def 9
it on A,B;
existence
ex b₁ being POINT of G st b₁ on A,B by Th23;
uniqueness
for b₁, b₂ being POINT of G st b₁ on A,B & b₂ on A,B holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines * PROJPL_1:def 9 :
for G being IncProjectivePlane
for A, B being LINE of G st A <> B holds
for b₄ being POINT of G holds
( b₄ = A * B iff b₄ on A,B );

theorem Th24: :: PROJPL_1:24

for G being IncProjectivePlane
for a being POINT of G
for A, B being LINE of G st A <> B holds
( A * B on A & A * B on B & A * B = B * A & ( a on A & a on B implies a = A * B ) )

proof end;

theorem :: PROJPL_1:25

for G being IncProjectivePlane
for a, q being POINT of G
for A, B being LINE of G st A <> B & a on A & q |' A & a <> A * B holds
( (q * a) * B on B & (q * a) * B |' A )

proof end;

begin

theorem Th26: :: PROJPL_1:26

for G being IncProjSp
for a, b, c being POINT of G st a,b,c is_a_triangle holds
a,b,c are_mutually_different

proof end;

theorem :: PROJPL_1:27

for G being IncProjSp
for a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle holds
a,b,c,d are_mutually_different

proof end;

theorem Th28: :: PROJPL_1:28

for G being IncProjectivePlane
for a, b, c, d being POINT of G holds
( not a * c = b * d or a = c or b = d or c = d or a * c = c * d )

proof end;

theorem :: PROJPL_1:29

for G being IncProjectivePlane
for a, b, c, d being POINT of G holds
( not a * c = b * d or a = c or b = d or c = d or a on c * d )

proof end;

theorem :: PROJPL_1:30

for G being IncProjectivePlane
for e, m, m9 being POINT of G
for I being LINE of G st m on I & m9 on I & m <> m9 & e |' I holds
( m * e <> m9 * e & e * m <> e * m9 )

proof end;

theorem :: PROJPL_1:31

for G being IncProjectivePlane
for e being POINT of G
for 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 )

proof end;

theorem :: PROJPL_1:32

for G being IncProjSp
for 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

proof end;

theorem :: PROJPL_1:33

for G being IncProjSp
for a, b, c being POINT of G st c on a * b & a <> c holds
b on a * c

proof end;

theorem :: PROJPL_1:34

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

proof end;

theorem Th35: :: PROJPL_1:35

for G being IncProjectivePlane
for a, b, c being POINT of G holds
( not a on b * c or a = c or b = c or b on c * a )

proof end;

theorem :: PROJPL_1:36

for G being IncProjectivePlane
for a, b, c being POINT of G holds
( not a on b * c or b = a or b = c or c on b * a )

proof end;

theorem :: PROJPL_1:37

for G being IncProjectivePlane
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 |' 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 )

proof end;