:: PROJPL_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being IncProjStr
for a being POINT of G
for A being LINE of G st G is IncProjSp & a on A 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being IncProjStr
for a being POINT of G
for A, B being LINE of G st G is IncProjSp & a on A & A <> B holds
ex b being POINT of G st
( b on A & b |' B & a <> b )
proof end;

theorem Th10: :: PROJPL_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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
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 ,b2 `2 ,b2 `3 ,b2 `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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being IncProjectivePlane
for e, m, m' being POINT of G
for I being LINE of G st m on I & m' on I & m <> m' & e |' I holds
( m * e <> m' * e & e * m <> e * m' )
proof end;

theorem :: PROJPL_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 on H & 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;