:: PROJPL_1 semantic presentation
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 ) ) )
proof
let G be IncProjStr ; ::_thesis: 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 ) ) )
let a, b, c be POINT of G; ::_thesis: 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 ) ) )
let P, Q, R be LINE of G; ::_thesis: ( ( {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 ) ) )
thus ( {a,b} on P implies {b,a} on P ) ; ::_thesis: ( ( {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 ) ) )
thus ( {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 ) ) ::_thesis: ( ( 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
assume A1: {a,b,c} on P ; ::_thesis: ( {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 )
then A2: c on P by INCSP_1:2;
( a on P & b on P ) by A1, INCSP_1:2;
hence ( {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 ) by A2, INCSP_1:2; ::_thesis: verum
end;
thus ( a on P,Q implies a on Q,P ) ::_thesis: ( 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
assume a on P,Q ; ::_thesis: a on Q,P
then ( a on P & a on Q ) by Def2;
hence a on Q,P by Def2; ::_thesis: verum
end;
assume A3: a on P,Q,R ; ::_thesis: ( 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 )
then A4: a on R by Def3;
( a on P & a on Q ) by A3, Def3;
hence ( 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 ) by A4, Def3; ::_thesis: verum
end;
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 )
proof
let G be IncProjStr ; ::_thesis: ( 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 )
hereby ::_thesis: ( ( 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 ) implies G is configuration )
assume A1: G is configuration ; ::_thesis: 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
let p, q be POINT of G; ::_thesis: for P, Q being LINE of G st {p,q} on P & {p,q} on Q & not p = q holds
P = Q
let P, Q be LINE of G; ::_thesis: ( {p,q} on P & {p,q} on Q & not p = q implies P = Q )
assume that
A2: {p,q} on P and
A3: {p,q} on Q ; ::_thesis: ( p = q or P = Q )
A4: ( p on Q & q on Q ) by A3, INCSP_1:1;
( p on P & q on P ) by A2, INCSP_1:1;
hence ( p = q or P = Q ) by A1, A4, Def4; ::_thesis: verum
end;
hereby ::_thesis: verum
assume A5: 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 ; ::_thesis: G is configuration
now__::_thesis:_for_p,_q_being_POINT_of_G
for_P,_Q_being_LINE_of_G_st_p_on_P_&_q_on_P_&_p_on_Q_&_q_on_Q_&_not_p_=_q_holds_
P_=_Q
let p, q be POINT of G; ::_thesis: for P, Q being LINE of G st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q
let P, Q be LINE of G; ::_thesis: ( p on P & q on P & p on Q & q on Q & not p = q implies P = Q )
assume ( p on P & q on P & p on Q & q on Q ) ; ::_thesis: ( p = q or P = Q )
then ( {p,q} on P & {p,q} on Q ) by INCSP_1:1;
hence ( p = q or P = Q ) by A5; ::_thesis: verum
end;
hence G is configuration by Def4; ::_thesis: verum
end;
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
let G be IncProjStr ; ::_thesis: ( 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 )
hereby ::_thesis: ( ( 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 ) implies G is configuration )
assume A1: G is configuration ; ::_thesis: 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
let p, q be POINT of G; ::_thesis: for P, Q being LINE of G st p on P,Q & q on P,Q & not p = q holds
P = Q
let P, Q be LINE of G; ::_thesis: ( p on P,Q & q on P,Q & not p = q implies P = Q )
assume A2: ( p on P,Q & q on P,Q ) ; ::_thesis: ( p = q or P = Q )
then A3: ( p on Q & q on Q ) by Def2;
( p on P & q on P ) by A2, Def2;
hence ( p = q or P = Q ) by A1, A3, Def4; ::_thesis: verum
end;
hereby ::_thesis: verum
assume A4: 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 ; ::_thesis: G is configuration
now__::_thesis:_for_p,_q_being_POINT_of_G
for_P,_Q_being_LINE_of_G_st_p_on_P_&_q_on_P_&_p_on_Q_&_q_on_Q_&_not_p_=_q_holds_
P_=_Q
let p, q be POINT of G; ::_thesis: for P, Q being LINE of G st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q
let P, Q be LINE of G; ::_thesis: ( p on P & q on P & p on Q & q on Q & not p = q implies P = Q )
assume ( p on P & q on P & p on Q & q on Q ) ; ::_thesis: ( p = q or P = Q )
then ( p on P,Q & q on P,Q ) by Def2;
hence ( p = q or P = Q ) by A4; ::_thesis: verum
end;
hence G is configuration by Def4; ::_thesis: verum
end;
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
let G be IncProjStr ; ::_thesis: ( 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 ) ) )
hereby ::_thesis: ( 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 ) implies G is IncProjSp )
assume A1: G is IncProjSp ; ::_thesis: ( 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 ) )
then for p, q being POINT of G
for P, Q being LINE of G st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q by INCPROJ:def_4;
hence G is configuration by Def4; ::_thesis: ( ( 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 ) )
thus for p, q being POINT of G ex P being LINE of G st {p,q} on P ::_thesis: ( 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
let p, q be POINT of G; ::_thesis: ex P being LINE of G st {p,q} on P
consider P being LINE of G such that
A2: ( p on P & q on P ) by A1, INCPROJ:def_5;
take P ; ::_thesis: {p,q} on P
thus {p,q} on P by A2, INCSP_1:1; ::_thesis: verum
end;
thus ex p being POINT of G ex P being LINE of G st p |' P by A1, INCPROJ:def_6; ::_thesis: ( ( 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 ) )
thus 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 ) ::_thesis: 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
let P be LINE of G; ::_thesis: ex a, b, c being POINT of G st
( a,b,c are_mutually_different & {a,b,c} on P )
consider a, b, c being POINT of G such that
A3: ( a <> b & b <> c & c <> a ) and
A4: ( a on P & b on P & c on P ) by A1, INCPROJ:def_7;
take a ; ::_thesis: ex b, c being POINT of G st
( a,b,c are_mutually_different & {a,b,c} on P )
take b ; ::_thesis: ex c being POINT of G st
( a,b,c are_mutually_different & {a,b,c} on P )
take c ; ::_thesis: ( a,b,c are_mutually_different & {a,b,c} on P )
thus a,b,c are_mutually_different by A3, ZFMISC_1:def_5; ::_thesis: {a,b,c} on P
thus {a,b,c} on P by A4, INCSP_1:2; ::_thesis: verum
end;
thus 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 ::_thesis: verum
proof
let a, b, c, d, p be POINT of G; ::_thesis: 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
let M, N, P, Q be LINE of G; ::_thesis: ( {a,b,p} on M & {c,d,p} on N & {a,c} on P & {b,d} on Q & p |' P & p |' Q & M <> N implies ex q being POINT of G st q on P,Q )
assume that
A5: {a,b,p} on M and
A6: {c,d,p} on N and
A7: {a,c} on P and
A8: {b,d} on Q and
A9: ( p |' P & p |' Q & M <> N ) ; ::_thesis: ex q being POINT of G st q on P,Q
A10: ( a on M & b on M ) by A5, INCSP_1:2;
A11: ( a on P & c on P ) by A7, INCSP_1:1;
A12: ( d on N & p on N ) by A6, INCSP_1:2;
A13: ( b on Q & d on Q ) by A8, INCSP_1:1;
( p on M & c on N ) by A5, A6, INCSP_1:2;
then consider q being POINT of G such that
A14: ( q on P & q on Q ) by A1, A9, A10, A12, A11, A13, INCPROJ:def_8;
take q ; ::_thesis: q on P,Q
thus q on P,Q by A14, Def2; ::_thesis: verum
end;
end;
hereby ::_thesis: verum
assume that
A15: G is configuration and
A16: for p, q being POINT of G ex P being LINE of G st {p,q} on P and
A17: ex p being POINT of G ex P being LINE of G st p |' P and
A18: 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 ) and
A19: 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 ; ::_thesis: G is IncProjSp
A20: now__::_thesis:_for_p,_q_being_POINT_of_G_ex_P_being_LINE_of_G_st_
(_p_on_P_&_q_on_P_)
let p, q be POINT of G; ::_thesis: ex P being LINE of G st
( p on P & q on P )
consider P being LINE of G such that
A21: {p,q} on P by A16;
take P = P; ::_thesis: ( p on P & q on P )
thus ( p on P & q on P ) by A21, INCSP_1:1; ::_thesis: verum
end;
A22: now__::_thesis:_for_P_being_LINE_of_G_ex_a,_b,_c_being_POINT_of_G_st_
(_a_<>_b_&_b_<>_c_&_c_<>_a_&_a_on_P_&_b_on_P_&_c_on_P_)
let P be LINE of G; ::_thesis: ex a, b, c being POINT of G st
( a <> b & b <> c & c <> a & a on P & b on P & c on P )
consider a, b, c being POINT of G such that
A23: a,b,c are_mutually_different and
A24: {a,b,c} on P by A18;
A25: ( a <> b & b <> c ) by A23, ZFMISC_1:def_5;
A26: ( b on P & c on P ) by A24, INCSP_1:2;
( c <> a & a on P ) by A23, A24, INCSP_1:2, ZFMISC_1:def_5;
hence ex a, b, c being POINT of G st
( a <> b & b <> c & c <> a & a on P & b on P & c on P ) by A25, A26; ::_thesis: verum
end;
A27: for a, b, c, d, p, q being POINT of G
for M, N, P, Q being LINE of G st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being POINT of G st
( q on P & q on Q )
proof
let a, b, c, d, p, q be POINT of G; ::_thesis: for M, N, P, Q being LINE of G st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being POINT of G st
( q on P & q on Q )
let M, N, P, Q be LINE of G; ::_thesis: ( a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N implies ex q being POINT of G st
( q on P & q on Q ) )
assume that
A28: ( a on M & b on M & c on N & d on N & p on M & p on N ) and
A29: ( a on P & c on P & b on Q & d on Q ) and
A30: ( not p on P & not p on Q & M <> N ) ; ::_thesis: ex q being POINT of G st
( q on P & q on Q )
A31: ( {a,c} on P & {b,d} on Q ) by A29, INCSP_1:1;
( {a,b,p} on M & {c,d,p} on N ) by A28, INCSP_1:2;
then consider q1 being POINT of G such that
A32: q1 on P,Q by A19, A30, A31;
take q1 ; ::_thesis: ( q1 on P & q1 on Q )
thus ( q1 on P & q1 on Q ) by A32, Def2; ::_thesis: verum
end;
for p, q being POINT of G
for P, Q being LINE of G st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q by A15, Def4;
hence G is IncProjSp by A17, A20, A22, A27, INCPROJ:def_4, INCPROJ:def_5, INCPROJ:def_6, INCPROJ:def_7, INCPROJ:def_8; ::_thesis: verum
end;
end;
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 ) )
proof
let G be IncProjStr ; ::_thesis: 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 ) )
let a, b, c be POINT of G; ::_thesis: ( a,b,c is_collinear iff ex P being LINE of G st
( a on P & b on P & c on P ) )
( ex P being LINE of G st {a,b,c} on P iff ex P being LINE of G st
( a on P & b on P & c on P ) )
proof
hereby ::_thesis: ( ex P being LINE of G st
( a on P & b on P & c on P ) implies ex P being LINE of G st {a,b,c} on P )
given P being LINE of G such that A1: {a,b,c} on P ; ::_thesis: ex P being LINE of G st
( a on P & b on P & c on P )
take P = P; ::_thesis: ( a on P & b on P & c on P )
thus ( a on P & b on P & c on P ) by A1, INCSP_1:2; ::_thesis: verum
end;
hereby ::_thesis: verum
given P being LINE of G such that A2: ( a on P & b on P & c on P ) ; ::_thesis: ex P being LINE of G st {a,b,c} on P
take P = P; ::_thesis: {a,b,c} on P
thus {a,b,c} on P by A2, INCSP_1:2; ::_thesis: verum
end;
end;
hence ( a,b,c is_collinear iff ex P being LINE of G st
( a on P & b on P & c on P ) ) by Def5; ::_thesis: verum
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;
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
proof
let G be IncProjStr ; ::_thesis: ( G is IncProjSp implies ex A, B being LINE of G st A <> B )
set a = the POINT of G;
assume G is IncProjSp ; ::_thesis: ex A, B being LINE of G st A <> B
then consider A, B, C being LINE of G such that
the POINT of G on A and
the POINT of G on B and
the POINT of G on C and
A1: A <> B and
B <> C and
C <> A by PROJRED1:5;
take A ; ::_thesis: ex B being LINE of G st A <> B
take B ; ::_thesis: A <> B
thus A <> B by A1; ::_thesis: verum
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
let G be IncProjStr ; ::_thesis: 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 )
let a be POINT of G; ::_thesis: 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 )
let A be LINE of G; ::_thesis: ( G is IncProjSp implies ex b, c being POINT of G st
( {b,c} on A & a,b,c are_mutually_different ) )
assume A1: G is IncProjSp ; ::_thesis: ex b, c being POINT of G st
( {b,c} on A & a,b,c are_mutually_different )
then consider b being POINT of G such that
A2: ( b on A & b <> a ) and
b <> a by PROJRED1:8;
consider c being POINT of G such that
A3: ( c on A & c <> a & c <> b ) by A1, PROJRED1:8;
take b ; ::_thesis: ex c being POINT of G st
( {b,c} on A & a,b,c are_mutually_different )
take c ; ::_thesis: ( {b,c} on A & a,b,c are_mutually_different )
thus ( {b,c} on A & a,b,c are_mutually_different ) by A2, A3, INCSP_1:1, ZFMISC_1:def_5; ::_thesis: verum
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
let G be IncProjStr ; ::_thesis: 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 )
let a be POINT of G; ::_thesis: 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 )
let A, B be LINE of G; ::_thesis: ( G is IncProjSp & A <> B implies ex b being POINT of G st
( b on A & b |' B & a <> b ) )
assume that
A1: G is IncProjSp and
A2: A <> B ; ::_thesis: ex b being POINT of G st
( b on A & b |' B & a <> b )
consider b, c being POINT of G such that
A3: {b,c} on A and
A4: a,b,c are_mutually_different by A1, Th8;
A5: a <> c by A4, ZFMISC_1:def_5;
A6: c on A by A3, INCSP_1:1;
A7: b <> c by A4, ZFMISC_1:def_5;
A8: b on A by A3, INCSP_1:1;
A9: a <> b by A4, ZFMISC_1:def_5;
now__::_thesis:_(_(_b_|'_B_&_ex_b_being_POINT_of_G_st_
(_b_on_A_&_b_|'_B_&_a_<>_b_)_)_or_(_c_|'_B_&_ex_b_being_POINT_of_G_st_
(_b_on_A_&_b_|'_B_&_a_<>_b_)_)_)
percases ( b |' B or c |' B ) by A1, A2, A7, A8, A6, INCPROJ:def_4;
case b |' B ; ::_thesis: ex b being POINT of G st
( b on A & b |' B & a <> b )
hence ex b being POINT of G st
( b on A & b |' B & a <> b ) by A9, A8; ::_thesis: verum
end;
case c |' B ; ::_thesis: ex b being POINT of G st
( b on A & b |' B & a <> b )
hence ex b being POINT of G st
( b on A & b |' B & a <> b ) by A5, A6; ::_thesis: verum
end;
end;
end;
hence ex b being POINT of G st
( b on A & b |' B & a <> b ) ; ::_thesis: verum
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
let G be IncProjStr ; ::_thesis: 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
let a1, a2, b be POINT of G; ::_thesis: 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
let A be LINE of G; ::_thesis: ( G is configuration & {a1,a2} on A & a1 <> a2 & b |' A implies a1,a2,b is_a_triangle )
assume that
A1: G is configuration and
A2: {a1,a2} on A and
A3: ( a1 <> a2 & b |' A ) and
A4: a1,a2,b is_collinear ; ::_thesis: contradiction
A5: ( a1 on A & a2 on A ) by A2, INCSP_1:1;
ex P being LINE of G st
( a1 on P & a2 on P & b on P ) by A4, Th5;
hence contradiction by A1, A3, A5, Def4; ::_thesis: verum
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
let G be IncProjStr ; ::_thesis: 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 )
let a, b, c be POINT of G; ::_thesis: ( a,b,c is_collinear implies ( 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 ) )
assume a,b,c is_collinear ; ::_thesis: ( 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 )
then consider P being LINE of G such that
A1: {a,b,c} on P by Def5;
A2: {c,b,a} on P by A1, Th1;
A3: ( {b,c,a} on P & {c,a,b} on P ) by A1, Th1;
( {a,c,b} on P & {b,a,c} on P ) by A1, Th1;
hence ( 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 ) by A3, A2, Def5; ::_thesis: verum
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
let G be IncProjStr ; ::_thesis: 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 )
let a, b, c, d be POINT of G; ::_thesis: ( a,b,c,d is_a_quadrangle implies ( 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 ) )
assume A1: a,b,c,d is_a_quadrangle ; ::_thesis: ( 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 )
then A2: a,b,c is_a_triangle by Def6;
then A3: a,c,b is_a_triangle by Th11;
A4: c,b,a is_a_triangle by A2, Th11;
A5: b,c,a is_a_triangle by A2, Th11;
A6: c,a,b is_a_triangle by A2, Th11;
A7: b,a,c is_a_triangle by A2, Th11;
A8: c,d,a is_a_triangle by A1, Def6;
then A9: c,a,d is_a_triangle by Th11;
A10: a,d,c is_a_triangle by A8, Th11;
A11: d,a,c is_a_triangle by A8, Th11;
A12: d,a,b is_a_triangle by A1, Def6;
then A13: d,b,a is_a_triangle by Th11;
A14: b,a,d is_a_triangle by A12, Th11;
A15: a,b,d is_a_triangle by A12, Th11;
A16: b,d,a is_a_triangle by A12, Th11;
A17: a,d,b is_a_triangle by A12, Th11;
A18: b,c,d is_a_triangle by A1, Def6;
then A19: c,b,d is_a_triangle by Th11;
hence a,c,b,d is_a_quadrangle by A3, A11, A16, Def6; ::_thesis: ( 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 )
A20: a,c,d is_a_triangle by A8, Th11;
A21: c,d,b is_a_triangle by A18, Th11;
hence b,a,c,d is_a_quadrangle by A7, A20, A13, Def6; ::_thesis: ( 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 )
A22: d,b,c is_a_triangle by A18, Th11;
hence b,c,a,d is_a_quadrangle by A5, A9, A17, Def6; ::_thesis: ( 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 )
A23: d,c,a is_a_triangle by A8, Th11;
A24: b,d,c is_a_triangle by A18, Th11;
hence c,a,b,d is_a_quadrangle by A6, A23, A15, Def6; ::_thesis: ( 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 )
A25: d,c,b is_a_triangle by A18, Th11;
hence c,b,a,d is_a_quadrangle by A4, A10, A14, Def6; ::_thesis: ( 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 )
thus a,b,d,c is_a_quadrangle by A6, A24, A23, A15, Def6; ::_thesis: ( 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 )
thus a,c,d,b is_a_quadrangle by A7, A21, A20, A13, Def6; ::_thesis: ( 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 )
thus b,a,d,c is_a_quadrangle by A4, A25, A10, A14, Def6; ::_thesis: ( 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 )
thus b,c,d,a is_a_quadrangle by A2, A18, A8, A12, Def6; ::_thesis: ( 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 )
thus c,a,d,b is_a_quadrangle by A5, A22, A9, A17, Def6; ::_thesis: ( 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 )
thus c,b,d,a is_a_quadrangle by A3, A19, A11, A16, Def6; ::_thesis: ( 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 )
thus a,d,b,c is_a_quadrangle by A5, A22, A9, A17, Def6; ::_thesis: ( 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 )
thus a,d,c,b is_a_quadrangle by A4, A25, A10, A14, Def6; ::_thesis: ( 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 )
thus b,d,a,c is_a_quadrangle by A3, A19, A11, A16, Def6; ::_thesis: ( 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 )
thus b,d,c,a is_a_quadrangle by A6, A24, A23, A15, Def6; ::_thesis: ( 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 )
thus c,d,a,b is_a_quadrangle by A2, A18, A8, A12, Def6; ::_thesis: ( 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 )
thus c,d,b,a is_a_quadrangle by A7, A21, A20, A13, Def6; ::_thesis: ( 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 )
thus d,a,b,c is_a_quadrangle by A2, A18, A8, A12, Def6; ::_thesis: ( 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 )
thus d,a,c,b is_a_quadrangle by A3, A19, A11, A16, Def6; ::_thesis: ( 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 )
thus d,b,a,c is_a_quadrangle by A7, A21, A20, A13, Def6; ::_thesis: ( d,b,c,a is_a_quadrangle & d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle )
thus d,b,c,a is_a_quadrangle by A5, A22, A9, A17, Def6; ::_thesis: ( d,c,a,b is_a_quadrangle & d,c,b,a is_a_quadrangle )
thus d,c,a,b is_a_quadrangle by A6, A24, A23, A15, Def6; ::_thesis: d,c,b,a is_a_quadrangle
thus d,c,b,a is_a_quadrangle by A4, A25, A10, A14, Def6; ::_thesis: verum
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
let G be IncProjStr ; ::_thesis: 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
let a1, a2, b1, b2 be POINT of G; ::_thesis: 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
let A, B be LINE of G; ::_thesis: ( G is configuration & {a1,a2} on A & {b1,b2} on B & a1,a2 |' B & b1,b2 |' A & a1 <> a2 & b1 <> b2 implies a1,a2,b1,b2 is_a_quadrangle )
assume that
A1: G is configuration and
A2: {a1,a2} on A and
A3: {b1,b2} on B and
A4: a1,a2 |' B and
A5: b1,b2 |' A and
A6: a1 <> a2 and
A7: b1 <> b2 ; ::_thesis: a1,a2,b1,b2 is_a_quadrangle
b1 |' A by A5, Def1;
then A8: a1,a2,b1 is_a_triangle by A1, A2, A6, Th10;
b2 |' A by A5, Def1;
then a1,a2,b2 is_a_triangle by A1, A2, A6, Th10;
then A9: b2,a1,a2 is_a_triangle by Th11;
a2 |' B by A4, Def1;
then b1,b2,a2 is_a_triangle by A1, A3, A7, Th10;
then A10: a2,b1,b2 is_a_triangle by Th11;
a1 |' B by A4, Def1;
then b1,b2,a1 is_a_triangle by A1, A3, A7, Th10;
hence a1,a2,b1,b2 is_a_quadrangle by A8, A10, A9, Def6; ::_thesis: verum
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
let G be IncProjStr ; ::_thesis: ( G is IncProjSp implies ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle )
assume A1: G is IncProjSp ; ::_thesis: ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle
then consider A, B being LINE of G such that
A2: A <> B by Th7;
consider a, b being POINT of G such that
A3: ( a on A & a |' B ) and
A4: ( b on B & b |' A ) by A1, A2, PROJRED1:3;
consider q being POINT of G such that
A5: ( q on B & q |' A ) and
A6: b <> q by A1, A3, Th9;
A7: ( {b,q} on B & b,q |' A ) by A4, A5, Def1, INCSP_1:1;
A8: G is configuration by A1, Th4;
consider p being POINT of G such that
A9: ( p on A & p |' B ) and
A10: a <> p by A1, A3, Th9;
take a ; ::_thesis: ex b, c, d being POINT of G st a,b,c,d is_a_quadrangle
take p ; ::_thesis: ex c, d being POINT of G st a,p,c,d is_a_quadrangle
take b ; ::_thesis: ex d being POINT of G st a,p,b,d is_a_quadrangle
take q ; ::_thesis: a,p,b,q is_a_quadrangle
( {a,p} on A & a,p |' B ) by A3, A9, Def1, INCSP_1:1;
hence a,p,b,q is_a_quadrangle by A10, A6, A8, A7, Th14; ::_thesis: verum
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
consider a, b, c, d being POINT of G such that
A1: a,b,c,d is_a_quadrangle by Th15;
reconsider e = [a,b,c,d] as Element of [: the Points of G, the Points of G, the Points of G, the Points of G:] ;
A2: e `3_4 = c by MCART_1:def_10;
take e ; ::_thesis: e `1_4 ,e `2_4 ,e `3_4 ,e `4_4 is_a_quadrangle
( e `1_4 = a & e `2_4 = b ) by MCART_1:def_8, MCART_1:def_9;
hence e `1_4 ,e `2_4 ,e `3_4 ,e `4_4 is_a_quadrangle by A1, A2, MCART_1:def_11; ::_thesis: verum
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 ;
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
proof
G is configuration by Th4;
hence for b1, b2 being LINE of G st {a,b} on b1 & {a,b} on b2 holds
b1 = b2 by A1, Th2; ::_thesis: verum
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
let G be IncProjSp; ::_thesis: 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 ) )
let a, b be POINT of G; ::_thesis: 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 ) )
let L be LINE of G; ::_thesis: ( a <> b implies ( a on a * b & b on a * b & a * b = b * a & ( a on L & b on L implies L = a * b ) ) )
assume A1: a <> b ; ::_thesis: ( a on a * b & b on a * b & a * b = b * a & ( a on L & b on L implies L = a * b ) )
then {a,b} on a * b by Def8;
hence ( a on a * b & b on a * b & a * b = b * a ) by A1, Def8, INCSP_1:1; ::_thesis: ( a on L & b on L implies L = a * b )
assume ( a on L & b on L ) ; ::_thesis: L = a * b
then {a,b} on L by INCSP_1:1;
hence L = a * b by A1, Def8; ::_thesis: verum
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
let G be IncProjStr ; ::_thesis: ( 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 ) implies ex p being POINT of G ex P being LINE of G st p |' P )
assume that
A1: ex a, b, c being POINT of G st a,b,c is_a_triangle and
A2: for p, q being POINT of G ex M being LINE of G st {p,q} on M ; ::_thesis: ex p being POINT of G ex P being LINE of G st p |' P
consider a, b, c being POINT of G such that
A3: a,b,c is_a_triangle by A1;
consider P being LINE of G such that
A4: {a,b} on P by A2;
take c ; ::_thesis: ex P being LINE of G st c |' P
take P ; ::_thesis: c |' P
( a on P & b on P ) by A4, INCSP_1:1;
hence c |' P by A3, Th5; ::_thesis: verum
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
let G be IncProjStr ; ::_thesis: ( ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle implies ex a, b, c being POINT of G st a,b,c is_a_triangle )
given a, b, c, d being POINT of G such that A1: a,b,c,d is_a_quadrangle ; ::_thesis: ex a, b, c being POINT of G st a,b,c is_a_triangle
take a ; ::_thesis: ex b, c being POINT of G st a,b,c is_a_triangle
take b ; ::_thesis: ex c being POINT of G st a,b,c is_a_triangle
take c ; ::_thesis: a,b,c is_a_triangle
thus a,b,c is_a_triangle by A1, Def6; ::_thesis: verum
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
let G be IncProjStr ; ::_thesis: 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
let a, b, c be POINT of G; ::_thesis: 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
let P, Q be LINE of G; ::_thesis: ( a,b,c is_a_triangle & {a,b} on P & {a,c} on Q implies P <> Q )
assume that
A1: a,b,c is_a_triangle and
A2: {a,b} on P and
A3: {a,c} on Q ; ::_thesis: P <> Q
A4: c on Q by A3, INCSP_1:1;
( a on P & b on P ) by A2, INCSP_1:1;
hence P <> Q by A1, A4, Th5; ::_thesis: verum
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
let G be IncProjStr ; ::_thesis: 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
let a, b, c, d be POINT of G; ::_thesis: 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
let P, Q, R be LINE of G; ::_thesis: ( a,b,c,d is_a_quadrangle & {a,b} on P & {a,c} on Q & {a,d} on R implies P,Q,R are_mutually_different )
assume that
A1: a,b,c,d is_a_quadrangle and
A2: {a,b} on P and
A3: {a,c} on Q and
A4: {a,d} on R ; ::_thesis: P,Q,R are_mutually_different
c,d,a is_a_triangle by A1, Def6;
then a,c,d is_a_triangle by Th11;
then A5: Q <> R by A3, A4, Th19;
d,a,b is_a_triangle by A1, Def6;
then a,d,b is_a_triangle by Th11;
then A6: R <> P by A2, A4, Th19;
a,b,c is_a_triangle by A1, Def6;
then P <> Q by A2, A3, Th19;
hence P,Q,R are_mutually_different by A5, A6, ZFMISC_1:def_5; ::_thesis: verum
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
let G be IncProjStr ; ::_thesis: 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
let a, p, q, r be POINT of G; ::_thesis: 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
let P, Q, R, A be LINE of G; ::_thesis: ( 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 implies p,q,r are_mutually_different )
assume that
A1: G is configuration and
A2: a on P,Q,R and
A3: P,Q,R are_mutually_different and
A4: a |' A and
A5: p on A,P and
A6: q on A,Q and
A7: r on A,R ; ::_thesis: p,q,r are_mutually_different
A8: ( a on R & r on R ) by A2, A7, Def2, Def3;
A9: ( a on Q & q on Q ) by A2, A6, Def2, Def3;
( Q <> R & q on A ) by A3, A6, Def2, ZFMISC_1:def_5;
then A10: q <> r by A1, A4, A9, A8, Def4;
A11: p on P by A5, Def2;
A12: ( a on P & p on A ) by A2, A5, Def2, Def3;
R <> P by A3, ZFMISC_1:def_5;
then A13: r <> p by A1, A4, A12, A11, A8, Def4;
P <> Q by A3, ZFMISC_1:def_5;
then p <> q by A1, A4, A12, A11, A9, Def4;
hence p,q,r are_mutually_different by A10, A13, ZFMISC_1:def_5; ::_thesis: verum
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
let G be IncProjStr ; ::_thesis: ( 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 implies 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 ) )
assume that
A1: G is configuration and
A2: for p, q being POINT of G ex M being LINE of G st {p,q} on M and
A3: for P, Q being LINE of G ex a being POINT of G st a on P,Q and
A4: ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle ; ::_thesis: 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 )
hereby ::_thesis: verum
let P be LINE of G; ::_thesis: ex a, b, c being POINT of G st
( a,b,c are_mutually_different & {a,b,c} on P )
consider a, b, c, d being POINT of G such that
A5: a,b,c,d is_a_quadrangle by A4;
A6: a,b,c is_a_triangle by A5, Def6;
thus ex a, b, c being POINT of G st
( a,b,c are_mutually_different & {a,b,c} on P ) ::_thesis: verum
proof
now__::_thesis:_(_(_a_|'_P_&_ex_a,_b,_c_being_POINT_of_G_st_
(_a,b,c_are_mutually_different_&_{a,b,c}_on_P_)_)_or_(_b_|'_P_&_ex_a,_b,_c_being_POINT_of_G_st_
(_a,b,c_are_mutually_different_&_{a,b,c}_on_P_)_)_or_(_c_|'_P_&_ex_a,_b,_c_being_POINT_of_G_st_
(_a,b,c_are_mutually_different_&_{a,b,c}_on_P_)_)_)
percases ( a |' P or b |' P or c |' P ) by A6, Th5;
caseA7: a |' P ; ::_thesis: ex a, b, c being POINT of G st
( a,b,c are_mutually_different & {a,b,c} on P )
consider B being LINE of G such that
A8: {a,b} on B by A2;
consider D being LINE of G such that
A9: {a,d} on D by A2;
consider C being LINE of G such that
A10: {a,c} on C by A2;
A11: a on D by A9, INCSP_1:1;
A12: a on C by A10, INCSP_1:1;
a on B by A8, INCSP_1:1;
then A13: a on B,C,D by A12, A11, Def3;
consider p being POINT of G such that
A14: p on P,B by A3;
A15: B,C,D are_mutually_different by A5, A8, A10, A9, Th20;
consider q being POINT of G such that
A16: q on P,C by A3;
A17: q on P by A16, Def2;
consider r being POINT of G such that
A18: r on P,D by A3;
A19: r on P by A18, Def2;
p on P by A14, Def2;
then {p,q,r} on P by A17, A19, INCSP_1:2;
hence ex a, b, c being POINT of G st
( a,b,c are_mutually_different & {a,b,c} on P ) by A1, A7, A13, A15, A14, A16, A18, Th21; ::_thesis: verum
end;
caseA20: b |' P ; ::_thesis: ex a, b, c being POINT of G st
( a,b,c are_mutually_different & {a,b,c} on P )
consider B being LINE of G such that
A21: {b,a} on B by A2;
consider D being LINE of G such that
A22: {b,d} on D by A2;
consider C being LINE of G such that
A23: {b,c} on C by A2;
A24: b on D by A22, INCSP_1:1;
A25: b on C by A23, INCSP_1:1;
b on B by A21, INCSP_1:1;
then A26: b on B,C,D by A25, A24, Def3;
consider q being POINT of G such that
A27: q on P,C by A3;
b,a,c,d is_a_quadrangle by A5, Th13;
then A28: B,C,D are_mutually_different by A21, A23, A22, Th20;
consider p being POINT of G such that
A29: p on P,B by A3;
A30: q on P by A27, Def2;
consider r being POINT of G such that
A31: r on P,D by A3;
A32: r on P by A31, Def2;
p on P by A29, Def2;
then {p,q,r} on P by A30, A32, INCSP_1:2;
hence ex a, b, c being POINT of G st
( a,b,c are_mutually_different & {a,b,c} on P ) by A1, A20, A26, A28, A29, A27, A31, Th21; ::_thesis: verum
end;
caseA33: c |' P ; ::_thesis: ex a, b, c being POINT of G st
( a,b,c are_mutually_different & {a,b,c} on P )
consider B being LINE of G such that
A34: {c,a} on B by A2;
consider D being LINE of G such that
A35: {c,d} on D by A2;
consider C being LINE of G such that
A36: {c,b} on C by A2;
A37: c on D by A35, INCSP_1:1;
A38: c on C by A36, INCSP_1:1;
c on B by A34, INCSP_1:1;
then A39: c on B,C,D by A38, A37, Def3;
consider q being POINT of G such that
A40: q on P,C by A3;
c,a,b,d is_a_quadrangle by A5, Th13;
then A41: B,C,D are_mutually_different by A34, A36, A35, Th20;
consider p being POINT of G such that
A42: p on P,B by A3;
A43: q on P by A40, Def2;
consider r being POINT of G such that
A44: r on P,D by A3;
A45: r on P by A44, Def2;
p on P by A42, Def2;
then {p,q,r} on P by A43, A45, INCSP_1:2;
hence ex a, b, c being POINT of G st
( a,b,c are_mutually_different & {a,b,c} on P ) by A1, A33, A39, A41, A42, A40, A44, Th21; ::_thesis: verum
end;
end;
end;
hence ex a, b, c being POINT of G st
( a,b,c are_mutually_different & {a,b,c} on P ) ; ::_thesis: verum
end;
end;
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
let G be IncProjStr ; ::_thesis: ( 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 ) )
hereby ::_thesis: ( 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 implies G is IncProjectivePlane )
assume A1: G is IncProjectivePlane ; ::_thesis: ( 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 )
hence G is configuration by Th4; ::_thesis: ( ( 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 )
thus for p, q being POINT of G ex M being LINE of G st {p,q} on M by A1, Th4; ::_thesis: ( ( 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 )
thus for P, Q being LINE of G ex a being POINT of G st a on P,Q ::_thesis: ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle
proof
let P, Q be LINE of G; ::_thesis: ex a being POINT of G st a on P,Q
consider a being POINT of G such that
A2: ( a on P & a on Q ) by A1, INCPROJ:def_9;
take a ; ::_thesis: a on P,Q
thus a on P,Q by A2, Def2; ::_thesis: verum
end;
thus ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle by A1, Th15; ::_thesis: verum
end;
hereby ::_thesis: verum
assume that
A3: G is configuration and
A4: for p, q being POINT of G ex M being LINE of G st {p,q} on M and
A5: for P, Q being LINE of G ex a being POINT of G st a on P,Q and
A6: ex a, b, c, d being POINT of G st a,b,c,d is_a_quadrangle ; ::_thesis: G is IncProjectivePlane
ex a, b, c being POINT of G st a,b,c is_a_triangle by A6, Th18;
then A7: ex p being POINT of G ex P being LINE of G st p |' P by A4, Th17;
( ( 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 ) ) by A3, A4, A5, A6, Th22;
then reconsider G9 = G as IncProjSp by A3, A4, A7, Th4;
for P, Q being LINE of G9 ex a being POINT of G9 st
( a on P & a on Q )
proof
let P, Q be LINE of G9; ::_thesis: ex a being POINT of G9 st
( a on P & a on Q )
consider a being POINT of G9 such that
A8: a on P,Q by A5;
take a ; ::_thesis: ( a on P & a on Q )
thus ( a on P & a on Q ) by A8, Def2; ::_thesis: verum
end;
hence G is IncProjectivePlane by INCPROJ:def_9; ::_thesis: verum
end;
end;
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
proof
G is configuration by Th4;
hence for b1, b2 being POINT of G st b1 on A,B & b2 on A,B holds
b1 = b2 by A1, Th3; ::_thesis: verum
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
let G be IncProjectivePlane; ::_thesis: 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 ) )
let a be POINT of G; ::_thesis: 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 ) )
let A, B be LINE of G; ::_thesis: ( A <> B implies ( A * B on A & A * B on B & A * B = B * A & ( a on A & a on B implies a = A * B ) ) )
assume A1: A <> B ; ::_thesis: ( A * B on A & A * B on B & A * B = B * A & ( a on A & a on B implies a = A * B ) )
then A * B on A,B by Def9;
then A * B on B,A by Th1;
hence ( A * B on A & A * B on B & A * B = B * A ) by A1, Def2, Def9; ::_thesis: ( a on A & a on B implies a = A * B )
assume ( a on A & a on B ) ; ::_thesis: a = A * B
then a on A,B by Def2;
hence a = A * B by A1, Def9; ::_thesis: verum
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
let G be IncProjectivePlane; ::_thesis: 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 )
let a, q be POINT of G; ::_thesis: 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 )
let A, B be LINE of G; ::_thesis: ( A <> B & a on A & q |' A & a <> A * B implies ( (q * a) * B on B & (q * a) * B |' A ) )
assume that
A1: A <> B and
A2: a on A and
A3: q |' A and
A4: a <> A * B ; ::_thesis: ( (q * a) * B on B & (q * a) * B |' A )
set D = q * a;
A5: ( a on q * a & q on q * a ) by A2, A3, Th16;
set d = (q * a) * B;
A6: G is configuration by Th23;
A7: a |' B by A1, A2, A4, Th24;
then A8: q * a <> B by A2, A3, Th16;
hence (q * a) * B on B by Th24; ::_thesis: (q * a) * B |' A
assume A9: (q * a) * B on A ; ::_thesis: contradiction
(q * a) * B on q * a by A8, Th24;
then a = (q * a) * B by A2, A3, A6, A9, A5, Def4;
hence contradiction by A7, A8, Th24; ::_thesis: verum
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
let G be IncProjSp; ::_thesis: for a, b, c being POINT of G st a,b,c is_a_triangle holds
a,b,c are_mutually_different
let a, b, c be POINT of G; ::_thesis: ( a,b,c is_a_triangle implies a,b,c are_mutually_different )
assume that
A1: a,b,c is_a_triangle and
A2: not a,b,c are_mutually_different ; ::_thesis: contradiction
now__::_thesis:_(_(_a_=_b_&_contradiction_)_or_(_b_=_c_&_contradiction_)_or_(_c_=_a_&_contradiction_)_)
percases ( a = b or b = c or c = a ) by A2, ZFMISC_1:def_5;
caseA3: a = b ; ::_thesis: contradiction
ex P being LINE of G st
( b on P & c on P ) by INCPROJ:def_5;
hence contradiction by A1, A3, Th5; ::_thesis: verum
end;
caseA4: b = c ; ::_thesis: contradiction
ex P being LINE of G st
( a on P & b on P ) by INCPROJ:def_5;
hence contradiction by A1, A4, Th5; ::_thesis: verum
end;
caseA5: c = a ; ::_thesis: contradiction
ex P being LINE of G st
( b on P & c on P ) by INCPROJ:def_5;
hence contradiction by A1, A5, Th5; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
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
let G be IncProjSp; ::_thesis: 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
let a, b, c, d be POINT of G; ::_thesis: ( a,b,c,d is_a_quadrangle implies a,b,c,d are_mutually_different )
assume that
A1: a,b,c,d is_a_quadrangle and
A2: not a,b,c,d are_mutually_different ; ::_thesis: contradiction
now__::_thesis:_(_(_a_=_b_&_contradiction_)_or_(_b_=_c_&_contradiction_)_or_(_c_=_a_&_contradiction_)_or_(_d_=_a_&_contradiction_)_or_(_d_=_b_&_contradiction_)_or_(_d_=_c_&_contradiction_)_)
percases ( a = b or b = c or c = a or d = a or d = b or d = c ) by A2, ZFMISC_1:def_6;
case a = b ; ::_thesis: contradiction
then not a,b,c are_mutually_different by ZFMISC_1:def_5;
then not a,b,c is_a_triangle by Th26;
hence contradiction by A1, Def6; ::_thesis: verum
end;
case b = c ; ::_thesis: contradiction
then not a,b,c are_mutually_different by ZFMISC_1:def_5;
then not a,b,c is_a_triangle by Th26;
hence contradiction by A1, Def6; ::_thesis: verum
end;
case c = a ; ::_thesis: contradiction
then not a,b,c are_mutually_different by ZFMISC_1:def_5;
then not a,b,c is_a_triangle by Th26;
hence contradiction by A1, Def6; ::_thesis: verum
end;
case d = a ; ::_thesis: contradiction
then not d,a,b are_mutually_different by ZFMISC_1:def_5;
then not d,a,b is_a_triangle by Th26;
hence contradiction by A1, Def6; ::_thesis: verum
end;
case d = b ; ::_thesis: contradiction
then not d,a,b are_mutually_different by ZFMISC_1:def_5;
then not d,a,b is_a_triangle by Th26;
hence contradiction by A1, Def6; ::_thesis: verum
end;
case d = c ; ::_thesis: contradiction
then not b,c,d are_mutually_different by ZFMISC_1:def_5;
then not b,c,d is_a_triangle by Th26;
hence contradiction by A1, Def6; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
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
let G be IncProjectivePlane; ::_thesis: 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 )
let a, b, c, d be POINT of G; ::_thesis: ( not a * c = b * d or a = c or b = d or c = d or a * c = c * d )
assume that
A1: ( a * c = b * d & not a = c & not b = d ) and
A2: not c = d ; ::_thesis: a * c = c * d
( c on a * c & d on a * c ) by A1, Th16;
hence a * c = c * d by A2, Th16; ::_thesis: verum
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
let G be IncProjectivePlane; ::_thesis: 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 )
let a, b, c, d be POINT of G; ::_thesis: ( not a * c = b * d or a = c or b = d or c = d or a on c * d )
assume that
A1: a * c = b * d and
A2: not a = c and
A3: ( not b = d & not c = d ) ; ::_thesis: a on c * d
a * c = c * d by A1, A2, A3, Th28;
hence a on c * d by A2, Th16; ::_thesis: verum
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
let G be IncProjectivePlane; ::_thesis: 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 )
let e, m, m9 be POINT of G; ::_thesis: 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 )
let I be LINE of G; ::_thesis: ( m on I & m9 on I & m <> m9 & e |' I implies ( m * e <> m9 * e & e * m <> e * m9 ) )
assume that
A1: m on I and
A2: m9 on I and
A3: m <> m9 and
A4: e |' I ; ::_thesis: ( m * e <> m9 * e & e * m <> e * m9 )
set L1 = m * e;
set L2 = m9 * e;
A5: now__::_thesis:_not_m_*_e_=_m9_*_e
m on m * e by A1, A4, Th16;
then A6: m on I,m * e by A1, Def2;
e on m * e by A1, A4, Th16;
then A7: m = I * (m * e) by A4, A6, Def9;
assume A8: m * e = m9 * e ; ::_thesis: contradiction
m9 on m9 * e by A2, A4, Th16;
then A9: m9 on I,m9 * e by A2, Def2;
e on m9 * e by A2, A4, Th16;
hence contradiction by A3, A4, A8, A9, A7, Def9; ::_thesis: verum
end;
now__::_thesis:_not_e_*_m_=_e_*_m9
assume A10: e * m = e * m9 ; ::_thesis: contradiction
m * e = e * m by A1, A4, Th16;
hence contradiction by A2, A4, A5, A10, Th16; ::_thesis: verum
end;
hence ( m * e <> m9 * e & e * m <> e * m9 ) by A5; ::_thesis: verum
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
let G be IncProjectivePlane; ::_thesis: 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 )
let e be POINT of G; ::_thesis: 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 )
let I, L1, L2 be LINE of G; ::_thesis: ( e on L1 & e on L2 & L1 <> L2 & e |' I implies ( I * L1 <> I * L2 & L1 * I <> L2 * I ) )
assume that
A1: e on L1 and
A2: e on L2 and
A3: L1 <> L2 and
A4: e |' I ; ::_thesis: ( I * L1 <> I * L2 & L1 * I <> L2 * I )
set p1 = I * L1;
set p2 = I * L2;
A5: now__::_thesis:_not_I_*_L1_=_I_*_L2
I * L1 on L1 by A1, A4, Th24;
then A6: {e,(I * L1)} on L1 by A1, INCSP_1:1;
I * L1 on I by A1, A4, Th24;
then A7: L1 = e * (I * L1) by A4, A6, Def8;
assume A8: I * L1 = I * L2 ; ::_thesis: contradiction
I * L2 on L2 by A2, A4, Th24;
then A9: {e,(I * L2)} on L2 by A2, INCSP_1:1;
I * L2 on I by A2, A4, Th24;
hence contradiction by A3, A4, A8, A9, A7, Def8; ::_thesis: verum
end;
now__::_thesis:_not_L1_*_I_=_L2_*_I
assume A10: L1 * I = L2 * I ; ::_thesis: contradiction
L1 * I = I * L1 by A1, A4, Th24;
hence contradiction by A2, A4, A5, A10, Th24; ::_thesis: verum
end;
hence ( I * L1 <> I * L2 & L1 * I <> L2 * I ) by A5; ::_thesis: verum
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
let G be IncProjSp; ::_thesis: 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
let a, b, q, q1 be POINT of G; ::_thesis: ( q on a * b & q on a * q1 & q <> a & q1 <> a & a <> b implies q1 on a * b )
assume that
A1: ( q on a * b & q on a * q1 & q <> a ) and
A2: q1 <> a and
A3: a <> b ; ::_thesis: q1 on a * b
( a on a * b & a on a * q1 ) by A2, A3, Th16;
then a * b = a * q1 by A1, INCPROJ:def_4;
hence q1 on a * b by A2, Th16; ::_thesis: verum
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
let G be IncProjSp; ::_thesis: for a, b, c being POINT of G st c on a * b & a <> c holds
b on a * c
let a, b, c be POINT of G; ::_thesis: ( c on a * b & a <> c implies b on a * c )
assume that
A1: c on a * b and
A2: a <> c ; ::_thesis: b on a * c
now__::_thesis:_(_a_<>_b_implies_b_on_a_*_c_)
assume A3: a <> b ; ::_thesis: b on a * c
then a on a * b by Th16;
then a * b = a * c by A1, A2, Th16;
hence b on a * c by A3, Th16; ::_thesis: verum
end;
hence b on a * c by A2, Th16; ::_thesis: verum
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
let G be IncProjectivePlane; ::_thesis: 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
let q1, q2, r1, r2 be POINT of G; ::_thesis: for H being LINE of G st r1 <> r2 & r1 on H & r2 on H & q1 |' H & q2 |' H holds
q1 * r1 <> q2 * r2
let H be LINE of G; ::_thesis: ( r1 <> r2 & r1 on H & r2 on H & q1 |' H & q2 |' H implies q1 * r1 <> q2 * r2 )
assume that
A1: r1 <> r2 and
A2: r1 on H and
A3: r2 on H and
A4: q1 |' H and
A5: q2 |' H and
A6: q1 * r1 = q2 * r2 ; ::_thesis: contradiction
set L1 = q1 * r1;
set L2 = q2 * r2;
A7: q1 on q1 * r1 by A2, A4, Th16;
r2 on q2 * r2 by A3, A5, Th16;
then A8: r2 on q2 * r2,H by A3, Def2;
r1 on q1 * r1 by A2, A4, Th16;
then r1 on q1 * r1,H by A2, Def2;
then r1 = (q1 * r1) * H by A4, A7, Def9;
hence contradiction by A1, A4, A6, A7, A8, Def9; ::_thesis: verum
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
let G be IncProjectivePlane; ::_thesis: 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 )
let a, b, c be POINT of G; ::_thesis: ( not a on b * c or a = c or b = c or b on c * a )
assume that
A1: a on b * c and
A2: a <> c and
A3: b <> c ; ::_thesis: b on c * a
c on b * c by A3, Th16;
then A4: {c,a} on b * c by A1, INCSP_1:1;
b on b * c by A3, Th16;
hence b on c * a by A2, A4, Def8; ::_thesis: verum
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
let G be IncProjectivePlane; ::_thesis: 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 )
let a, b, c be POINT of G; ::_thesis: ( not a on b * c or b = a or b = c or c on b * a )
assume that
A1: ( a on b * c & b <> a ) and
A2: b <> c ; ::_thesis: c on b * a
b * c = c * b by A2, Th16;
hence c on b * a by A1, A2, Th35; ::_thesis: verum
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
let G be IncProjectivePlane; ::_thesis: 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 )
let e, x1, x2, p1, p2 be POINT of G; ::_thesis: 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 )
let H, I be LINE of G; ::_thesis: ( x1 on I & x2 on I & e |' I & x1 <> x2 & p1 <> e & p2 <> e & p1 on e * x1 & p2 on e * x2 implies ex r being POINT of G st
( r on p1 * p2 & r on H & r <> e ) )
assume that
A1: x1 on I and
A2: x2 on I and
A3: e |' I and
A4: x1 <> x2 and
A5: p1 <> e and
A6: p2 <> e and
A7: p1 on e * x1 and
A8: p2 on e * x2 ; ::_thesis: ex r being POINT of G st
( r on p1 * p2 & r on H & r <> e )
set L1 = e * x1;
set L2 = e * x2;
set L = p1 * p2;
A9: e on e * x1 by A1, A3, Th16;
A10: e on e * x2 by A2, A3, Th16;
( x1 on e * x1 & x2 on e * x2 ) by A1, A2, A3, Th16;
then A11: e * x1 <> e * x2 by A1, A2, A3, A4, A9, INCPROJ:def_4;
then A12: p1 <> p2 by A5, A7, A8, A9, A10, INCPROJ:def_4;
then p2 on p1 * p2 by Th16;
then A13: p1 * p2 <> e * x1 by A6, A8, A9, A10, A11, INCPROJ:def_4;
consider r being POINT of G such that
A14: r on p1 * p2 and
A15: r on H by INCPROJ:def_9;
p1 on p1 * p2 by A12, Th16;
then r <> e by A5, A7, A14, A9, A13, INCPROJ:def_4;
hence ex r being POINT of G st
( r on p1 * p2 & r on H & r <> e ) by A14, A15; ::_thesis: verum
end;