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


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 :: PROJPL_1:def 1
( a |' P & b |' P );
end;

:: deftheorem 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 :: PROJPL_1:def 2
( a on P & a on Q );
end;

:: deftheorem 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 :: PROJPL_1:def 3
( a on P & a on Q & a on R );
end;

:: deftheorem 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 :: 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 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 :: 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_distinct & {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 are_collinear means :: PROJPL_1:def 5
 ex P being LINE of G st {a,b,c} on P;
end;

:: deftheorem defines are_collinear PROJPL_1:def 5 :
for G being IncProjStr
for a, b, c being POINT of G holds
( a,b,c are_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 are_collinear ;
end;

theorem Th5: :: PROJPL_1:5
for G being IncProjStr
for a, b, c being POINT of G holds
( a,b,c are_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 :: 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 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_distinct )
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 are_collinear holds
( a,c,b are_collinear & b,a,c are_collinear & b,c,a are_collinear & c,a,b are_collinear & c,b,a are_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 ) by Th11;

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_4 ,it `2_4 ,it `3_4 ,it `4_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_4 ,b1 `2_4 ,b1 `3_4 ,b1 `4_4 is_a_quadrangle
proof end;
end;

:: deftheorem defines Quadrangle PROJPL_1:def 7 :
for G being IncProjSp
for b2 being Element of [: the Points of G, the Points of G, the Points of G, the Points of G:] holds
( b2 is Quadrangle of G iff b2 `1_4 ,b2 `2_4 ,b2 `3_4 ,b2 `4_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 b1 being LINE of G st {a,b} on b1 by Th4;
uniqueness
for b1, b2 being LINE of G st {a,b} on b1 & {a,b} on b2 holds
b1 = b2
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 b4 being LINE of G holds
( b4 = a * b iff {a,b} on b4 );

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;

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 :: 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
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_distinct
proof end;

theorem Th21: :: PROJPL_1:21
for G being IncProjStr
for a, p, q, r being POINT of G
for A, P, Q, R being LINE of G st G is configuration & a on P,Q,R & P,Q,R are_mutually_distinct & a |' A & p on A,P & q on A,Q & r on A,R holds
p,q,r are_mutually_distinct
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_distinct & {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 b1 being POINT of G st b1 on A,B by Th23;
uniqueness
for b1, b2 being POINT of G st b1 on A,B & b2 on A,B holds
b1 = b2
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 b4 being POINT of G holds
( b4 = A * B iff b4 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;

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