projpl_1.miz
begin
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;
::
PROJPL_1:def1
pred a,b
|' P means a
|' P & b
|' P;
end
definition
let G, a, P, Q;
::
PROJPL_1:def2
pred a
on P,Q means a
on P & a
on Q;
end
definition
let G, a, P, Q, R;
::
PROJPL_1:def3
pred a
on P,Q,R means a
on P & a
on Q & a
on R;
end
theorem ::
PROJPL_1:1
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;
::
PROJPL_1:def4
attr IT is
configuration means for p,q be
POINT of IT, P,Q be
LINE of IT st p
on P & q
on P & p
on Q & q
on Q holds p
= q or P
= Q;
end
theorem ::
PROJPL_1:2
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 ::
PROJPL_1:3
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 ::
PROJPL_1:4
Th4: G is
IncProjSp iff G is
configuration & (for p, q holds ex P st
{p, q}
on P) & (ex p, P st p
|' P) & (for P holds 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 holds 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 holds 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 holds ex P st
{p, q}
on P and
A17: ex p, P st p
|' P and
A18: for P holds 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 be
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,
INCPROJ:def 5,
INCPROJ:def 6,
INCPROJ:def 7,
INCPROJ:def 8;
end;
end;
definition
mode
IncProjectivePlane is
2-dimensional
IncProjSp;
end
definition
let G, a, b, c;
::
PROJPL_1:def5
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 ::
PROJPL_1:5
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 ::
PROJPL_1:6
(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;
::
PROJPL_1:def6
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 ::
PROJPL_1:7
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 ::
PROJPL_1:8
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 ::
PROJPL_1:9
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 ::
PROJPL_1:10
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 ::
PROJPL_1:11
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 ::
PROJPL_1:12
(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 ::
PROJPL_1:13
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 ::
PROJPL_1:14
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 ::
PROJPL_1:15
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;
::
PROJPL_1:def7
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 be
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,
MCART_1: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;
::
PROJPL_1:def8
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 ::
PROJPL_1:16
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
theorem ::
PROJPL_1:17
Th17: (ex a, b, c st (a,b,c)
is_a_triangle ) & (for p, q holds 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 holds 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 ::
PROJPL_1:18
(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 ::
PROJPL_1:19
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 ::
PROJPL_1:20
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 ::
PROJPL_1:21
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 ::
PROJPL_1:22
Th22: G is
configuration & (for p, q holds ex M st
{p, q}
on M) & (for P, Q holds ex a st a
on (P,Q)) & (ex a, b, c, d st (a,b,c,d)
is_a_quadrangle ) implies for P holds 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 holds ex M st
{p, q}
on M and
A3: for P, Q holds 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 ::
PROJPL_1:23
Th23: G is
IncProjectivePlane iff G is
configuration & (for p, q holds ex M st
{p, q}
on M) & (for P, Q holds 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 holds ex M st
{p, q}
on M by
A1,
Th4;
thus for P, Q holds 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 holds ex M st
{p, q}
on M and
A5: for P, Q holds 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 holds 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 be
LINE of G9 holds ex a be
POINT of G9 st a
on P & a
on Q
proof
let P,Q be
LINE of G9;
consider a be
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;
::
PROJPL_1:def9
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 ::
PROJPL_1:24
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 ::
PROJPL_1:25
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
reserve G for
IncProjSp;
reserve a,b,c,d for
POINT of G;
reserve P for
LINE of G;
theorem ::
PROJPL_1:26
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 ::
PROJPL_1:27
(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 ::
PROJPL_1:28
Th28: for a,b,c,d be
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 ::
PROJPL_1:29
for a,b,c,d be
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 ::
PROJPL_1:30
for G be
IncProjectivePlane, e,m,m9 be
POINT of G, I be
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 ::
PROJPL_1:31
for G be
IncProjectivePlane, e be
POINT of G, I,L1,L2 be
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 ::
PROJPL_1:32
for G be
IncProjSp, a,b,q,q1 be
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 ::
PROJPL_1:33
for G be
IncProjSp, a,b,c be
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 ::
PROJPL_1:34
for G be
IncProjectivePlane, q1,q2,r1,r2 be
POINT of G, H be
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 ::
PROJPL_1:35
Th35: for a,b,c be
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 ::
PROJPL_1:36
for a,b,c be
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 ::
PROJPL_1:37
for e,x1,x2,p1,p2 be
POINT of G holds for H,I be
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 be
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 be
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;