:: Projective {P}lanes :: by Micha{\l} Muzalewski :: :: Received July 28, 1994 :: Copyright (c) 1994-2012 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; preda,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; preda 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; preda 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 ) ) ) proofend; definition let IT be IncProjStr ; attrIT 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 ) proofend; 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 ) proofend; 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 ) ) ) proofend; definition mode IncProjectivePlane is 2-dimensional IncProjSp; end; definition let G be IncProjStr ; let a, b, c be POINT of G; preda,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 ) ) proofend; 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; preda,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 proofend; 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 ) proofend; 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 ) proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 ; funca * 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 proofend; 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 ) ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 ) ) proofend; definition let G be IncProjectivePlane; let A, B be LINE of G; assume A1: A <> B ; funcA * 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 proofend; 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 ) ) proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend;