:: Projective {P}lanes
:: by Micha{\l} Muzalewski
::
:: Received July 28, 1994
:: Copyright (c) 1994-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies INCSP_1, INCPROJ, ZFMISC_1, ANALOAF, SUBSET_1, RELAT_1, PROJPL_1,
RECDEF_2, PENCIL_1;
notations ZFMISC_1, SUBSET_1, MCART_1, DOMAIN_1, INCSP_1, INCPROJ;
constructors DOMAIN_1, INCPROJ;
registrations INCPROJ;
theorems INCPROJ, PROJRED1, MCART_1, ZFMISC_1, INCSP_1;
begin :: 1. PROJECTIVE SPACES
reserve G for IncProjStr;
reserve a,a1,a2,b,b1,b2,c,d,p,q,r for POINT of G;
reserve A,B,C,D,M,N,P,Q,R for LINE of G;
notation
let G,a,P;
antonym a|'P for a on P;
end;
definition
let G,a,b,P;
pred a,b|'P means
a|'P & b|'P;
end;
definition
let G,a,P,Q;
pred a on P,Q means
a on P & a on Q;
end;
definition
let G,a,P,Q,R;
pred a on P,Q,R means
a on P & a on Q & a on R;
end;
theorem Th1:
({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
thus {a,b} on P implies {b,a} on 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
proof
assume
A1: {a,b,c} on P;
then
A2: c on P by INCSP_1:2;
a on P & b on P by A1,INCSP_1:2;
hence thesis by A2,INCSP_1:2;
end;
thus a on P,Q implies a on Q,P;
assume
A3: a on P,Q,R;
then
A4: a on R;
a on P & a on Q by A3;
hence thesis by A4;
end;
definition
let IT be IncProjStr;
attr IT is configuration means
for p,q being POINT of IT, P,Q being
LINE of IT st p on P & q on P & p on Q & q on Q holds p = q or P = Q;
end;
theorem Th2:
G is configuration iff for p,q,P,Q st {p,q} on P & {p,q} on Q
holds p = q or P = Q
proof
hereby
assume
A1: G is configuration;
let p,q,P,Q;
assume that
A2: {p,q} on P and
A3: {p,q} on 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;
end;
hereby
assume
A5: for p,q,P,Q st {p,q} on P & {p,q} on Q holds p = q or P = Q;
now
let p,q,P,Q;
assume p on P & q on P & p on Q & q on Q;
then {p,q} on P & {p,q} on Q by INCSP_1:1;
hence p = q or P = Q by A5;
end;
hence G is configuration;
end;
end;
theorem
G is configuration iff for p,q,P,Q st p on P,Q & q on P,Q holds p
= q or P = Q
proof
thus G is configuration implies for p,q,P,Q st p on P,Q & q on P,Q holds
p = q or P = Q;
hereby
assume
A1: for p,q,P,Q st p on P,Q & q on P,Q holds p = q or P = Q;
now
let p,q,P,Q;
assume p on P & q on P & p on Q & q on Q;
then p on P,Q & q on P,Q;
hence p = q or P = Q by A1;
end;
hence G is configuration;
end;
end;
theorem Th4:
G is IncProjSp iff G is configuration & (for p,q ex P st {p,q} on
P) & (ex p,P st p|'P) & (for P ex a,b,c st a,b,c are_mutually_distinct & {a,b,
c} on P) & for a,b,c,d,p,M,N,P,Q 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 st q on P,Q
proof
hereby
assume
A1: G is IncProjSp;
then
for p,q,P,Q st p on P & q on P & p on Q & q on Q holds p = q or P = Q
by INCPROJ:def 4;
hence G is configuration;
thus for p,q ex P st {p,q} on P
proof
let p,q;
consider P such that
A2: p on P & q on P by A1,INCPROJ:def 5;
take P;
thus thesis by A2,INCSP_1:1;
end;
thus ex p,P st p|'P by A1,INCPROJ:def 6;
thus for P ex a,b,c st a,b,c are_mutually_distinct & {a,b,c} on P
proof
let P;
consider a,b,c 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,b,c;
thus a,b,c are_mutually_distinct by A3,ZFMISC_1:def 5;
thus thesis by A4,INCSP_1:2;
end;
thus for a,b,c,d,p,M,N,P,Q 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 st q on P,Q
proof
let a,b,c,d,p,M,N,P,Q such 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;
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 such that
A14: q on P & q on Q by A1,A9,A10,A12,A11,A13,INCPROJ:def 8;
take q;
thus thesis by A14;
end;
end;
hereby
assume that
A15: G is configuration and
A16: for p,q ex P st {p,q} on P and
A17: ex p,P st p|'P and
A18: for P ex a,b,c st a,b,c are_mutually_distinct & {a,b,c} on P and
A19: for a,b,c,d,p,M,N,P,Q 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 st q on P,Q;
A20: now
let p,q;
consider P such that
A21: {p,q} on P by A16;
take P;
thus p on P & q on P by A21,INCSP_1:1;
end;
A22: now
let P;
consider a,b,c such that
A23: a,b,c are_mutually_distinct 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 st a<>b & b<>c & c <>a & a on P & b on P & c on P by A25,A26;
end;
A27: for a,b,c,d,p,q,M,N,P,Q 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 st q on P & q on Q
proof
let a,b,c,d,p,q,M,N,P,Q such 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;
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;
thus thesis by A32;
end;
for p,q,P,Q st p on P & q on P & p on Q & q on Q holds p = q or P = Q
by A15;
hence G is IncProjSp by A17,A20,A22,A27,INCPROJ:def 4,def 5,def 6,def 7
,def 8;
end;
end;
definition
mode IncProjectivePlane is 2-dimensional IncProjSp;
end;
definition
let G,a,b,c;
pred a,b,c are_collinear means
ex P st {a,b,c} on P;
end;
notation
let G,a,b,c;
antonym a,b,c is_a_triangle for a,b,c are_collinear;
end;
theorem Th5:
a,b,c are_collinear iff ex P st a on P & b on P & c on P
proof
(ex P st {a,b,c} on P) iff ex P st a on P & b on P & c on P
proof
hereby
given P such that
A1: {a,b,c} on P;
take P;
thus a on P & b on P & c on P by A1,INCSP_1:2;
end;
thus (ex P st a on P & b on P & c on P) implies
ex P st {a,b,c} on P by INCSP_1:2;
end;
hence thesis;
end;
theorem
a,b,c is_a_triangle iff for P holds a|'P or b|'P or c|'P by Th5;
definition
let G,a,b,c,d;
pred a,b,c,d is_a_quadrangle means
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;
theorem Th7:
G is IncProjSp implies ex A,B st A<>B
proof
set a = the POINT of G;
assume G is IncProjSp;
then consider A,B,C such that
a on A and
a on B and
a on C and
A1: A<>B and
B<>C and
C<>A by PROJRED1:5;
take A,B;
thus thesis by A1;
end;
theorem Th8:
G is IncProjSp implies ex b,c st {b,c} on A & a,b,c are_mutually_distinct
proof
assume
A1: G is IncProjSp;
then consider b such that
A2: b on A & b<>a and
b<>a by PROJRED1:8;
consider c such that
A3: c on A & c <>a & c <>b by A1,PROJRED1:8;
take b,c;
thus thesis by A2,A3,INCSP_1:1,ZFMISC_1:def 5;
end;
theorem Th9:
G is IncProjSp & A<>B implies ex b st b on A & b|'B & a<>b
proof
assume that
A1: G is IncProjSp and
A2: A<>B;
consider b,c such that
A3: {b,c} on A and
A4: a,b,c are_mutually_distinct 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
per cases by A1,A2,A7,A8,A6,INCPROJ:def 4;
case
b|'B;
hence thesis by A9,A8;
end;
case
c|'B;
hence thesis by A5,A6;
end;
end;
hence thesis;
end;
theorem Th10:
G is configuration & {a1,a2} on A & a1<>a2 & b|'A implies a1,a2,
b is_a_triangle
proof
assume that
A1: G is configuration and
A2: {a1,a2} on A and
A3: a1<>a2 & b|'A and
A4: a1,a2,b are_collinear;
A5: a1 on A & a2 on A by A2,INCSP_1:1;
ex P st a1 on P & a2 on P & b on P by A4,Th5;
hence contradiction by A1,A3,A5;
end;
theorem Th11:
a,b,c are_collinear implies 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
assume a,b,c are_collinear;
then consider P such that
A1: {a,b,c} on P;
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 thesis by A3,A2;
end;
theorem
a,b,c is_a_triangle implies 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:
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
by Th11;
theorem Th14:
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
proof
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;
b1|'A by A5;
then
A8: a1,a2,b1 is_a_triangle by A1,A2,A6,Th10;
b2|'A by A5;
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;
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;
then b1,b2,a1 is_a_triangle by A1,A3,A7,Th10;
hence thesis by A8,A10,A9;
end;
theorem Th15:
G is IncProjSp implies ex a,b,c,d st a,b,c,d is_a_quadrangle
proof
assume
A1: G is IncProjSp;
then consider A,B such that
A2: A<>B by Th7;
consider a,b such that
A3: a on A & a|'B and
A4: b on B & b|'A by A1,A2,PROJRED1:3;
consider q 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,INCSP_1:1;
A8: G is configuration by A1,Th4;
consider p such that
A9: p on A & p|'B and
A10: a<>p by A1,A3,Th9;
take a,p,b,q;
{a,p} on A & a,p|'B by A3,A9,INCSP_1:1;
hence thesis by A10,A6,A8,A7,Th14;
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
it`1_4,it`2_4,it`3_4,it`4_4 is_a_quadrangle;
existence
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;
e`1_4 = a & e`2_4 = b by MCART_1:def 8,def 9;
hence thesis by A1,A2,MCART_1:def 11;
end;
end;
definition
let G be IncProjSp, a,b be POINT of G;
assume
A1: a <> b;
func a*b -> LINE of G means
:Def8:
{a,b} on it;
existence by Th4;
uniqueness
proof
G is configuration by Th4;
hence thesis by A1,Th2;
end;
end;
theorem Th16:
for G be IncProjSp, a,b be POINT of G, L be 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, a,b be POINT of G, L be LINE of G;
assume
A1: 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;
assume a on L & b on L;
then {a,b} on L by INCSP_1:1;
hence thesis by A1,Def8;
end;
begin :: 2. PROJECTIVE PLANES
theorem Th17:
(ex a,b,c st a,b,c is_a_triangle) & (for p,q ex M st {p,q} on M)
implies ex p,P st p|'P
proof
assume that
A1: ex a,b,c st a,b,c is_a_triangle and
A2: for p,q ex M st {p,q} on M;
consider a,b,c such that
A3: a,b,c is_a_triangle by A1;
consider P such that
A4: {a,b} on P by A2;
take c,P;
a on P & b on P by A4,INCSP_1:1;
hence thesis by A3,Th5;
end;
theorem
(ex a,b,c,d st a,b,c,d is_a_quadrangle) implies ex a,b,c st a,b,
c is_a_triangle;
theorem Th19:
a,b,c is_a_triangle & {a,b} on P & {a,c} on Q implies P<>Q
proof
assume that
A1: a,b,c is_a_triangle and
A2: {a,b} on P and
A3: {a,c} on Q;
A4: c on Q by A3,INCSP_1:1;
a on P & b on P by A2,INCSP_1:1;
hence thesis by A1,A4,Th5;
end;
theorem Th20:
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_distinct
proof
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;
c,d,a is_a_triangle by A1;
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;
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;
then P<>Q by A2,A3,Th19;
hence thesis by A5,A6,ZFMISC_1:def 5;
end;
theorem Th21:
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 implies p,q,r are_mutually_distinct
proof
assume that
A1: G is configuration and
A2: a on P,Q,R and
A3: P,Q,R are_mutually_distinct and
A4: a|'A and
A5: p on A,P and
A6: q on A,Q and
A7: r on A,R;
A8: a on R & r on R by A2,A7;
A9: a on Q & q on Q by A2,A6;
Q<>R & q on A by A3,A6,ZFMISC_1:def 5;
then
A10: q<>r by A1,A4,A9,A8;
A11: p on P by A5;
A12: a on P & p on A by A2,A5;
R<>P by A3,ZFMISC_1:def 5;
then
A13: r<>p by A1,A4,A12,A11,A8;
P<>Q by A3,ZFMISC_1:def 5;
then p<>q by A1,A4,A12,A11,A9;
hence thesis by A10,A13,ZFMISC_1:def 5;
end;
theorem Th22:
G is configuration & (for p,q ex M st {p,q} on M) & (for P,Q ex
a st a on P,Q) & (ex a,b,c,d st a,b,c,d is_a_quadrangle) implies for P ex a,b,c
st a,b,c are_mutually_distinct & {a,b,c} on P
proof
assume that
A1: G is configuration and
A2: for p,q ex M st {p,q} on M and
A3: for P,Q ex a st a on P,Q and
A4: ex a,b,c,d st a,b,c,d is_a_quadrangle;
hereby
let P;
consider a,b,c,d such that
A5: a,b,c,d is_a_quadrangle by A4;
A6: a,b,c is_a_triangle by A5;
thus ex a,b,c st a,b,c are_mutually_distinct & {a,b,c} on P
proof
now
per cases by A6,Th5;
case
A7: a|'P;
consider B such that
A8: {a,b} on B by A2;
consider D such that
A9: {a,d} on D by A2;
consider C 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;
consider p such that
A14: p on P,B by A3;
A15: B,C,D are_mutually_distinct by A5,A8,A10,A9,Th20;
consider q such that
A16: q on P,C by A3;
A17: q on P by A16;
consider r such that
A18: r on P,D by A3;
A19: r on P by A18;
p on P by A14;
then {p,q,r} on P by A17,A19,INCSP_1:2;
hence thesis by A1,A7,A13,A15,A14,A16,A18,Th21;
end;
case
A20: b|'P;
consider B such that
A21: {b,a} on B by A2;
consider D such that
A22: {b,d} on D by A2;
consider C 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;
consider q 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_distinct by A21,A23,A22,Th20;
consider p such that
A29: p on P,B by A3;
A30: q on P by A27;
consider r such that
A31: r on P,D by A3;
A32: r on P by A31;
p on P by A29;
then {p,q,r} on P by A30,A32,INCSP_1:2;
hence thesis by A1,A20,A26,A28,A29,A27,A31,Th21;
end;
case
A33: c|'P;
consider B such that
A34: {c,a} on B by A2;
consider D such that
A35: {c,d} on D by A2;
consider C 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;
consider q 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_distinct by A34,A36,A35,Th20;
consider p such that
A42: p on P,B by A3;
A43: q on P by A40;
consider r such that
A44: r on P,D by A3;
A45: r on P by A44;
p on P by A42;
then {p,q,r} on P by A43,A45,INCSP_1:2;
hence thesis by A1,A33,A39,A41,A42,A40,A44,Th21;
end;
end;
hence thesis;
end;
end;
end;
theorem Th23:
G is IncProjectivePlane iff G is configuration & (for p,q ex M
st {p,q} on M) & (for P,Q ex a st a on P,Q) & ex a,b,c,d st a,b,c,d
is_a_quadrangle
proof
hereby
assume
A1: G is IncProjectivePlane;
hence G is configuration by Th4;
thus for p,q ex M st {p,q} on M by A1,Th4;
thus for P,Q ex a st a on P,Q
proof
let P,Q;
consider a such that
A2: a on P & a on Q by A1,INCPROJ:def 9;
take a;
thus thesis by A2;
end;
thus ex a,b,c,d st a,b,c,d is_a_quadrangle by A1,Th15;
end;
hereby
assume that
A3: G is configuration and
A4: for p,q ex M st {p,q} on M and
A5: for P,Q ex a st a on P,Q and
A6: ex a,b,c,d st a,b,c,d is_a_quadrangle;
ex a,b,c st a,b,c is_a_triangle by A6;
then
A7: ex p,P st p|'P by A4,Th17;
( for P ex a,b,c st a,b,c are_mutually_distinct & {a,b,c} on P)& for
a,b,c,d, p,M,N,P,Q 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 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;
consider a being POINT of G9 such that
A8: a on P,Q by A5;
take a;
thus thesis by A8;
end;
hence G is IncProjectivePlane by INCPROJ:def 9;
end;
end;
reserve G for IncProjectivePlane;
reserve a,q for POINT of G;
reserve A,B for LINE of G;
definition
let G,A,B;
assume
A1: A <> B;
func A*B -> POINT of G means
:Def9:
it on A,B;
existence by Th23;
uniqueness
proof
G is configuration by Th4;
hence thesis by A1;
end;
end;
theorem Th24:
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)
proof
assume
A1: A <> B;
then A*B on A,B by Def9;
then A*B on B,A;
hence A*B on A & A*B on B & A*B = B*A by A1,Def9;
assume a on A & a on B;
then a on A,B;
hence thesis by A1,Def9;
end;
theorem
A<>B & a on A & q|'A & a<>A*B implies (q*a)*B on B & (q*a)*B|'A
proof
assume that
A1: A<>B and
A2: a on A and
A3: q|'A and
A4: a<>A*B;
set D=q*a;
A5: a on D & q on D by A2,A3,Th16;
set d=D*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;
assume
A9: d on A;
d on D by A8,Th24;
then a = d by A2,A3,A6,A9,A5;
hence thesis by A7,A8,Th24;
end;
begin :: 3. SOME USEFUL PROPOSITIONS
reserve G for IncProjSp;
reserve a,b,c,d for POINT of G;
reserve P for LINE of G;
theorem Th26:
a,b,c is_a_triangle implies a,b,c are_mutually_distinct
proof
assume that
A1: a,b,c is_a_triangle and
A2: not a,b,c are_mutually_distinct;
now
per cases by A2,ZFMISC_1:def 5;
case
A3: a=b;
ex P st b on P & c on P by INCPROJ:def 5;
hence contradiction by A1,A3,Th5;
end;
case
A4: b=c;
ex P st a on P & b on P by INCPROJ:def 5;
hence contradiction by A1,A4,Th5;
end;
case
A5: c =a;
ex P st b on P & c on P by INCPROJ:def 5;
hence contradiction by A1,A5,Th5;
end;
end;
hence thesis;
end;
theorem
a,b,c,d is_a_quadrangle implies a,b,c,d are_mutually_distinct
proof
assume that
A1: a,b,c,d is_a_quadrangle and
A2: not a,b,c,d are_mutually_distinct;
now
per cases by A2,ZFMISC_1:def 6;
case
a=b;
then not a,b,c are_mutually_distinct by ZFMISC_1:def 5;
then not a,b,c is_a_triangle by Th26;
hence contradiction by A1;
end;
case
b=c;
then not a,b,c are_mutually_distinct by ZFMISC_1:def 5;
then not a,b,c is_a_triangle by Th26;
hence contradiction by A1;
end;
case
c =a;
then not a,b,c are_mutually_distinct by ZFMISC_1:def 5;
then not a,b,c is_a_triangle by Th26;
hence contradiction by A1;
end;
case
d=a;
then not d,a,b are_mutually_distinct by ZFMISC_1:def 5;
then not d,a,b is_a_triangle by Th26;
hence contradiction by A1;
end;
case
d=b;
then not d,a,b are_mutually_distinct by ZFMISC_1:def 5;
then not d,a,b is_a_triangle by Th26;
hence contradiction by A1;
end;
case
d=c;
then not b,c,d are_mutually_distinct by ZFMISC_1:def 5;
then not b,c,d is_a_triangle by Th26;
hence contradiction by A1;
end;
end;
hence thesis;
end;
reserve G for IncProjectivePlane;
theorem Th28:
for a,b,c,d being POINT of G st a*c = b*d holds a = c or b = d
or c = d or a*c = c*d
proof
let a,b,c,d be POINT of G;
assume that
A1: a*c = b*d & not a = c & not b = d and
A2: not c = d;
c on a*c & d on a*c by A1,Th16;
hence thesis by A2,Th16;
end;
theorem
for a,b,c,d being POINT of G st a*c = b*d holds a = c or b = d or c =
d or a on c*d
proof
let a,b,c,d be POINT of G;
assume that
A1: a*c = b*d and
A2: not a = c and
A3: ( not b = d)& not c = d;
a*c = c*d by A1,A2,A3,Th28;
hence thesis by A2,Th16;
end;
theorem
for G being IncProjectivePlane, e,m,m9 being POINT of G, 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, e,m,m9 be POINT of G, I be LINE of G such that
A1: m on I and
A2: m9 on I and
A3: m<>m9 and
A4: e |'I;
set L1=m*e,L2=m9*e;
A5: now
m on L1 by A1,A4,Th16;
then
A6: m on I,L1 by A1;
e on L1 by A1,A4,Th16;
then
A7: m=I*L1 by A4,A6,Def9;
assume
A8: m*e=m9*e;
m9 on L2 by A2,A4,Th16;
then
A9: m9 on I,L2 by A2;
e on L2 by A2,A4,Th16;
hence contradiction by A3,A4,A8,A9,A7,Def9;
end;
now
assume
A10: e*m=e*m9;
m*e=e*m by A1,A4,Th16;
hence contradiction by A2,A4,A5,A10,Th16;
end;
hence thesis by A5;
end;
theorem
for G being IncProjectivePlane, e being POINT of G, 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, e be POINT of G, I,L1,L2 be LINE of G such that
A1: e on L1 and
A2: e on L2 and
A3: L1<>L2 and
A4: e |'I;
set p1=I*L1,p2=I*L2;
A5: now
p1 on L1 by A1,A4,Th24;
then
A6: {e,p1} on L1 by A1,INCSP_1:1;
p1 on I by A1,A4,Th24;
then
A7: L1=e*p1 by A4,A6,Def8;
assume
A8: I*L1=I*L2;
p2 on L2 by A2,A4,Th24;
then
A9: {e,p2} on L2 by A2,INCSP_1:1;
p2 on I by A2,A4,Th24;
hence contradiction by A3,A4,A8,A9,A7,Def8;
end;
now
assume
A10: L1*I=L2*I;
L1*I=I*L1 by A1,A4,Th24;
hence contradiction by A2,A4,A5,A10,Th24;
end;
hence thesis by A5;
end;
theorem
for G being IncProjSp, 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, a,b,q,q1 be POINT of G;
assume that
A1: q on a*b & q on a*q1 & q<>a and
A2: q1<>a and
A3: 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 thesis by A2,Th16;
end;
theorem
for G being IncProjSp, a,b,c being POINT of G st c on a*b & a<>c holds
b on a*c
proof
let G be IncProjSp, a,b,c be POINT of G;
assume that
A1: c on a*b and
A2: a<>c;
now
assume
A3: a<>b;
then a on a*b by Th16;
then a*b = a*c by A1,A2,Th16;
hence thesis by A3,Th16;
end;
hence thesis by A2,Th16;
end;
theorem
for G being IncProjectivePlane, q1,q2,r1,r2 being POINT of G, 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, q1,q2,r1,r2 be POINT of G, H be LINE of G such
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;
set L1=q1*r1,L2=q2*r2;
A7: q1 on L1 by A2,A4,Th16;
r2 on L2 by A3,A5,Th16;
then
A8: r2 on L2,H by A3;
r1 on L1 by A2,A4,Th16;
then r1 on L1,H by A2;
then r1=L1*H by A4,A7,Def9;
hence contradiction by A1,A4,A6,A7,A8,Def9;
end;
theorem Th35:
for a,b,c being POINT of G st a on b*c holds a=c or b=c or b on c*a
proof
let a,b,c be POINT of G;
assume that
A1: a on b*c and
A2: a<>c and
A3: b<>c;
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 thesis by A2,A4,Def8;
end;
theorem
for a,b,c being POINT of G st a on b*c holds b=a or b=c or c on b*a
proof
let a,b,c be POINT of G;
assume that
A1: a on b*c & b<>a and
A2: b<>c;
b*c = c*b by A2,Th16;
hence thesis by A1,A2,Th35;
end;
theorem
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 e,x1,x2,p1,p2 be POINT of G;
let H,I be LINE of G such 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;
set L1=e*x1,L2=e*x2,L=p1*p2;
A9: e on L1 by A1,A3,Th16;
A10: e on L2 by A2,A3,Th16;
x1 on L1 & x2 on L2 by A1,A2,A3,Th16;
then
A11: L1 <> L2 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 L by Th16;
then
A13: L<>L1 by A6,A8,A9,A10,A11,INCPROJ:def 4;
consider r being POINT of G such that
A14: r on L and
A15: r on H by INCPROJ:def 9;
p1 on L by A12,Th16;
then r<>e by A5,A7,A14,A9,A13,INCPROJ:def 4;
hence thesis by A14,A15;
end;