:: by Micha{\l} Muzalewski

::

:: Received July 28, 1994

:: Copyright (c) 1994-2021 Association of Mizar Users

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

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

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

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

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

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

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;

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

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 )

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

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

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

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

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;
let a, b, c be POINT of G;

antonym a,b,c is_a_triangle for a,b,c are_collinear ;

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

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;

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;

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

( a,b,c is_a_triangle & b,c,d is_a_triangle & c,d,a is_a_triangle & d,a,b is_a_triangle );

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

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

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 )

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

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 )

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;

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;

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

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

ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle

proof end;

definition

let G be IncProjSp;

ex b_{1} being Element of [: the Points of G, the Points of G, the Points of G, the Points of G:] st b_{1} `1_4 ,b_{1} `2_4 ,b_{1} `3_4 ,b_{1} `4_4 is_a_quadrangle

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

ex b

proof end;

:: deftheorem defines Quadrangle PROJPL_1:def 7 :

for G being IncProjSp

for b_{2} being Element of [: the Points of G, the Points of G, the Points of G, the Points of G:] holds

( b_{2} is Quadrangle of G iff b_{2} `1_4 ,b_{2} `2_4 ,b_{2} `3_4 ,b_{2} `4_4 is_a_quadrangle );

for G being IncProjSp

for b

( b

definition

let G be IncProjSp;

let a, b be POINT of G;

assume A1: a <> b ;

existence

ex b_{1} being LINE of G st {a,b} on b_{1}
by Th4;

uniqueness

for b_{1}, b_{2} being LINE of G st {a,b} on b_{1} & {a,b} on b_{2} holds

b_{1} = b_{2}

end;
let a, b be POINT of G;

assume A1: a <> b ;

existence

ex b

uniqueness

for b

b

proof 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_{4} being LINE of G holds

( b_{4} = a * b iff {a,b} on b_{4} );

for G being IncProjSp

for a, b being POINT of G st a <> b holds

for b

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

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

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 ;

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

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

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

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 )

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

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

existence

ex b_{1} being POINT of G st b_{1} on A,B
by Th23;

uniqueness

for b_{1}, b_{2} being POINT of G st b_{1} on A,B & b_{2} on A,B holds

b_{1} = b_{2}

end;
let A, B be LINE of G;

assume A1: A <> B ;

existence

ex b

uniqueness

for b

b

proof 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_{4} being POINT of G holds

( b_{4} = A * B iff b_{4} on A,B );

for G being IncProjectivePlane

for A, B being LINE of G st A <> B holds

for b

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

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 )

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

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

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 )

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 )

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 )

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 )

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

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

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 )

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 )

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 )

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;