let IPP be 2-dimensional Desarguesian IncProjSp; for c, p, q being POINT of IPP
for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R & c on K & c on L & c on R & K <> R holds
ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )
let c, p, q be POINT of IPP; for K, L, R being LINE of IPP st not p on K & not p on L & not q on L & not q on R & c on K & c on L & c on R & K <> R holds
ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )
let K, L, R be LINE of IPP; ( not p on K & not p on L & not q on L & not q on R & c on K & c on L & c on R & K <> R implies ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) )
assume that
A1:
not p on K
and
A2:
not p on L
and
A3:
not q on L
and
A4:
not q on R
and
A5:
c on K
and
A6:
c on L
and
A7:
c on R
and
A8:
K <> R
; ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )
defpred S1[ object ] means ex k being POINT of IPP st
( $1 = k & k on K );
consider X being set such that
A9:
for x being object holds
( x in X iff ( x in the Points of IPP & S1[x] ) )
from XBOOLE_0:sch 1();
A10:
( dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= the Points of IPP & rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= the Points of IPP )
proof
set f =
(IncProj (L,q,R)) * (IncProj (K,p,L));
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L))
by A1, A2, A3, A4, Th22;
hence
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= the
Points of
IPP
;
rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= the Points of IPP
rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R))
by A1, A2, A3, A4, Th22;
hence
rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= the
Points of
IPP
by RELAT_1:def 19;
verum
end;
A11:
now ( p <> q implies ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) )A12:
now ( L = R implies ex p, o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) )A13:
X c= dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
proof
let e be
object ;
TARSKI:def 3 ( not e in X or e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) )
assume A14:
e in X
;
e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
then reconsider e =
e as
Element of the
Points of
IPP by A9;
A15:
ex
e9 being
POINT of
IPP st
(
e = e9 &
e9 on K )
by A9, A14;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L))
by A1, A2, A3, A4, Th22;
hence
e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
by A1, A2, A15, Def1;
verum
end; assume A16:
L = R
;
ex p, o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )A17:
X c= dom (IncProj (K,p,R))
proof
let e be
object ;
TARSKI:def 3 ( not e in X or e in dom (IncProj (K,p,R)) )
assume A18:
e in X
;
e in dom (IncProj (K,p,R))
then reconsider e =
e as
POINT of
IPP by A9;
ex
e9 being
POINT of
IPP st
(
e = e9 &
e9 on K )
by A9, A18;
hence
e in dom (IncProj (K,p,R))
by A1, A2, A16, Def1;
verum
end; A19:
for
x being
POINT of
IPP st
x in X holds
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x
proof
let x be
Element of the
Points of
IPP;
( x in X implies ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x )
assume A20:
x in X
;
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x
then A21:
((IncProj (R,q,R)) * (IncProj (K,p,R))) . x = (IncProj (R,q,R)) . ((IncProj (K,p,R)) . x)
by A16, A13, FUNCT_1:12;
A22:
x on K
by A1, A2, A16, A17, A20, Def1;
then reconsider y =
(IncProj (K,p,R)) . x as
POINT of
IPP by A1, A2, A16, Th19;
y on R
by A1, A2, A16, A22, Th20;
hence
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x
by A3, A16, A21, Th18;
verum
end;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= X
proof
let e be
object ;
TARSKI:def 3 ( not e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) or e in X )
assume
e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
;
e in X
then A23:
e in dom (IncProj (K,p,L))
by A1, A2, A3, A4, Th22;
then reconsider e =
e as
POINT of
IPP ;
e on K
by A1, A2, A23, Def1;
hence
e in X
by A9;
verum
end; then A24:
X = dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
by A13, XBOOLE_0:def 10;
A25:
(IncProj (L,q,R)) * (IncProj (K,p,L)) is
PartFunc of the
Points of
IPP, the
Points of
IPP
by A10, RELSET_1:4;
take p =
p;
ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )
dom (IncProj (K,p,R)) c= X
then
X = dom (IncProj (K,p,R))
by A17, XBOOLE_0:def 10;
hence
ex
o being
POINT of
IPP st
( not
o on K & not
o on R &
(IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (
K,
o,
R) )
by A1, A2, A16, A24, A19, A25, PARTFUN1:5;
verum end; consider A being
LINE of
IPP such that A27:
p on A
and A28:
q on A
by INCPROJ:def 5;
consider c1 being
POINT of
IPP such that A29:
c1 on K
and A30:
c1 on A
by INCPROJ:def 9;
reconsider c2 =
(IncProj (K,p,L)) . c1 as
Element of the
Points of
IPP by A1, A2, A29, Th19;
A31:
c2 on L
by A1, A2, A29, Th20;
then reconsider c3 =
(IncProj (L,q,R)) . c2 as
POINT of
IPP by A3, A4, Th19;
A32:
c3 on R
by A3, A4, A31, Th20;
consider a1 being
POINT of
IPP such that A33:
a1 on K
and A34:
c1 <> a1
and A35:
c <> a1
by Th8;
reconsider a2 =
(IncProj (K,p,L)) . a1 as
POINT of
IPP by A1, A2, A33, Th19;
A36:
a2 on L
by A1, A2, A33, Th20;
then reconsider a3 =
(IncProj (L,q,R)) . a2 as
POINT of
IPP by A3, A4, Th19;
A37:
a3 on R
by A3, A4, A36, Th20;
A38:
not
a3 on K
proof
assume
a3 on K
;
contradiction
then A39:
c = a3
by A5, A7, A8, A37, INCPROJ:def 4;
ex
C being
LINE of
IPP st
(
q on C &
c on C )
by INCPROJ:def 5;
then
(IncProj (L,q,R)) . c = a3
by A3, A4, A6, A7, A39, Def1;
then A40:
c = a2
by A3, A4, A6, A36, Th23;
ex
D being
LINE of
IPP st
(
p on D &
c on D )
by INCPROJ:def 5;
then
(IncProj (K,p,L)) . c = a2
by A1, A2, A5, A6, A40, Def1;
hence
contradiction
by A1, A2, A5, A33, A35, Th23;
verum
end; consider B being
LINE of
IPP such that A41:
(
a1 on B &
a3 on B )
by INCPROJ:def 5;
consider o being
POINT of
IPP such that A42:
o on A
and A43:
o on B
by INCPROJ:def 9;
A44:
not
a1 on R
by A5, A7, A8, A33, A35, INCPROJ:def 4;
A45:
( not
o on K & not
o on R )
proof
A46:
now not o on Rassume A47:
o on R
;
contradictionthen A48:
o = a3
by A37, A41, A43, A44, INCPROJ:def 4;
consider A2 being
LINE of
IPP such that A49:
q on A2
and A50:
c2 on A2
and A51:
c3 on A2
by A3, A4, A31, A32, Def1;
ex
A1 being
LINE of
IPP st
(
p on A1 &
c1 on A1 &
c2 on A1 )
by A1, A2, A29, A31, Def1;
then
c2 on A
by A1, A27, A29, A30, INCPROJ:def 4;
then
A = A2
by A3, A28, A31, A49, A50, INCPROJ:def 4;
then
o = c3
by A4, A42, A32, A47, A49, A51, INCPROJ:def 4;
then
c2 = a2
by A3, A4, A36, A31, A48, Th23;
hence
contradiction
by A1, A2, A29, A33, A34, Th23;
verum end;
A52:
now not o on Kassume A53:
o on K
;
contradictionthen
o = c1
by A1, A27, A29, A30, A42, INCPROJ:def 4;
hence
contradiction
by A33, A34, A41, A43, A38, A53, INCPROJ:def 4;
verum end;
assume
(
o on K or
o on R )
;
contradiction
hence
contradiction
by A52, A46;
verum
end; assume A54:
p <> q
;
ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )A55:
now ( L <> R & K <> L implies ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) )assume that A56:
L <> R
and
K <> L
;
ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )A57:
X c= dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
proof
let e be
object ;
TARSKI:def 3 ( not e in X or e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) )
assume A58:
e in X
;
e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
then reconsider e =
e as
POINT of
IPP by A9;
A59:
ex
e9 being
POINT of
IPP st
(
e = e9 &
e9 on K )
by A9, A58;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L))
by A1, A2, A3, A4, Th22;
hence
e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
by A1, A2, A59, Def1;
verum
end; A60:
for
x being
POINT of
IPP st
x in X holds
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
proof
let x be
Element of the
Points of
IPP;
( x in X implies ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x )
assume A61:
x in X
;
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
A62:
now ( x = c implies ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x )assume A63:
x = c
;
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . xthen
((IncProj (L,q,R)) * (IncProj (K,p,L))) . c = (IncProj (L,q,R)) . ((IncProj (K,p,L)) . c)
by A57, A61, FUNCT_1:12;
then
((IncProj (L,q,R)) * (IncProj (K,p,L))) . c = (IncProj (L,q,R)) . c
by A1, A2, A5, A6, Th24;
then
((IncProj (L,q,R)) * (IncProj (K,p,L))) . c = c
by A3, A4, A6, A7, Th24;
hence
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
by A5, A7, A45, A63, Th24;
verum end;
A64:
now ( x <> c1 & x <> c & x <> a1 implies ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x )assume that
x <> c1
and A65:
x <> c
and
x <> a1
;
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
proof
A66:
a2 <> a3
proof
assume
a2 = a3
;
contradiction
then A67:
(IncProj (K,p,L)) . a1 = c
by A6, A7, A36, A37, A56, INCPROJ:def 4;
(IncProj (K,p,L)) . c = c
by A1, A2, A5, A6, Th24;
hence
contradiction
by A1, A2, A5, A33, A35, A67, Th23;
verum
end;
A68:
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (L,q,R)) . ((IncProj (K,p,L)) . x)
by A57, A61, FUNCT_1:12;
A69:
a2 <> c
proof
assume A70:
a2 = c
;
contradiction
(IncProj (K,p,L)) . c = c
by A1, A2, A5, A6, Th24;
hence
contradiction
by A1, A2, A5, A33, A35, A70, Th23;
verum
end;
A71:
a3 on R
by A3, A4, A36, Th20;
A72:
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L))
by A1, A2, A3, A4, Th22;
then A73:
x on K
by A1, A2, A57, A61, Def1;
then reconsider y =
(IncProj (K,p,L)) . x as
POINT of
IPP by A1, A2, Th19;
A74:
y on L
by A1, A2, A73, Th20;
then reconsider z =
(IncProj (L,q,R)) . y as
POINT of
IPP by A3, A4, Th19;
consider B3 being
LINE of
IPP such that A75:
(
p on B3 &
x on B3 &
y on B3 )
by A1, A2, A73, A74, Def1;
x on K
by A1, A2, A57, A61, A72, Def1;
then A76:
c <> y
by A1, A5, A65, A75, INCPROJ:def 4;
consider A1 being
LINE of
IPP such that A77:
q on A1
and A78:
(
a2 on A1 &
a3 on A1 )
by A3, A4, A36, A37, Def1;
A79:
{a2,a3,q} on A1
by A77, A78, INCSP_1:2;
A80:
z on R
by A3, A4, A74, Th20;
then consider B1 being
LINE of
IPP such that A81:
(
q on B1 &
y on B1 &
z on B1 )
by A3, A4, A74, Def1;
x on K
by A1, A2, A57, A61, A72, Def1;
then A82:
{x,c,a1} on K
by A5, A33, INCSP_1:2;
consider A3 being
Element of the
Lines of
IPP such that A83:
p on A3
and A84:
a1 on A3
and A85:
a2 on A3
by A1, A2, A33, A36, Def1;
A86:
{a2,p,a1} on A3
by A83, A84, A85, INCSP_1:2;
A1 <> A3
proof
assume
A1 = A3
;
contradiction
then
A = A3
by A54, A27, A28, A77, A83, INCPROJ:def 4;
hence
contradiction
by A1, A29, A30, A33, A34, A83, A84, INCPROJ:def 4;
verum
end;
then A87:
A1,
L,
A3 are_mutually_distinct
by A2, A3, A77, A83, ZFMISC_1:def 5;
A88:
{a2,y,c} on L
by A6, A36, A74, INCSP_1:2;
A89:
{p,y,x} on B3
by A75, INCSP_1:2;
z on R
by A3, A4, A74, Th20;
then A90:
{a3,z,c} on R
by A7, A71, INCSP_1:2;
A91:
(
{p,o,q} on A &
{a3,o,a1} on B )
by A27, A28, A41, A42, A43, INCSP_1:2;
A92:
a2 <> p
by A1, A2, A33, Th20;
{y,z,q} on B1
by A81, INCSP_1:2;
then consider O being
LINE of
IPP such that A93:
{o,z,x} on O
by A69, A66, A76, A88, A79, A86, A89, A91, A82, A90, A87, A92, Th12;
A94:
o on O
by A93, INCSP_1:2;
(
x on O &
z on O )
by A93, INCSP_1:2;
hence
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
by A45, A73, A80, A94, A68, Def1;
verum
end; hence
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
;
verum end;
A95:
now ( x = c1 implies ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x )assume A96:
x = c1
;
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
proof
A97:
((IncProj (L,q,R)) * (IncProj (K,p,L))) . c1 = c3
by A57, A61, A96, FUNCT_1:12;
consider A2 being
LINE of
IPP such that A98:
(
q on A2 &
c2 on A2 )
and A99:
c3 on A2
by A3, A4, A31, A32, Def1;
ex
A1 being
Element of the
Lines of
IPP st
(
p on A1 &
c1 on A1 &
c2 on A1 )
by A1, A2, A29, A31, Def1;
then
c2 on A
by A1, A27, A29, A30, INCPROJ:def 4;
then
A = A2
by A3, A28, A31, A98, INCPROJ:def 4;
hence
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
by A29, A30, A42, A32, A45, A96, A97, A99, Def1;
verum
end; hence
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
;
verum end;
now ( x = a1 implies ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x )assume A100:
x = a1
;
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . xthen
((IncProj (L,q,R)) * (IncProj (K,p,L))) . a1 = a3
by A57, A61, FUNCT_1:12;
hence
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
by A33, A37, A41, A43, A45, A100, Def1;
verum end;
hence
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x
by A62, A95, A64;
verum
end; A101:
dom (IncProj (K,o,R)) c= X
X c= dom (IncProj (K,o,R))
then A104:
X = dom (IncProj (K,o,R))
by A101, XBOOLE_0:def 10;
A105:
(IncProj (L,q,R)) * (IncProj (K,p,L)) is
PartFunc of the
Points of
IPP, the
Points of
IPP
by A10, RELSET_1:4;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= X
proof
let e be
object ;
TARSKI:def 3 ( not e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) or e in X )
assume
e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
;
e in X
then A106:
e in dom (IncProj (K,p,L))
by A1, A2, A3, A4, Th22;
then reconsider e =
e as
POINT of
IPP ;
e on K
by A1, A2, A106, Def1;
hence
e in X
by A9;
verum
end; then
X = dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
by A57, XBOOLE_0:def 10;
hence
ex
o being
POINT of
IPP st
( not
o on K & not
o on R &
(IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (
K,
o,
R) )
by A45, A60, A104, A105, PARTFUN1:5;
verum end; now ( K = L implies ex q, o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) )A107:
X c= dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
proof
let e be
object ;
TARSKI:def 3 ( not e in X or e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) )
assume A108:
e in X
;
e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
then reconsider e =
e as
Element of the
Points of
IPP by A9;
A109:
ex
e9 being
POINT of
IPP st
(
e = e9 &
e9 on K )
by A9, A108;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L))
by A1, A2, A3, A4, Th22;
hence
e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
by A1, A2, A109, Def1;
verum
end;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= X
proof
let e be
object ;
TARSKI:def 3 ( not e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) or e in X )
assume
e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
;
e in X
then A110:
e in dom (IncProj (K,p,L))
by A1, A2, A3, A4, Th22;
then reconsider e =
e as
POINT of
IPP ;
e on K
by A1, A2, A110, Def1;
hence
e in X
by A9;
verum
end; then A111:
X = dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
by A107, XBOOLE_0:def 10;
A112:
(IncProj (L,q,R)) * (IncProj (K,p,L)) is
PartFunc of the
Points of
IPP, the
Points of
IPP
by A10, RELSET_1:4;
assume A113:
K = L
;
ex q, o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )A114:
X c= dom (IncProj (K,q,R))
proof
let e be
object ;
TARSKI:def 3 ( not e in X or e in dom (IncProj (K,q,R)) )
assume A115:
e in X
;
e in dom (IncProj (K,q,R))
then reconsider e =
e as
POINT of
IPP by A9;
ex
e9 being
POINT of
IPP st
(
e = e9 &
e9 on K )
by A9, A115;
hence
e in dom (IncProj (K,q,R))
by A3, A4, A113, Def1;
verum
end; A116:
for
x being
POINT of
IPP st
x in X holds
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,q,R)) . x
proof
let x be
Element of the
Points of
IPP;
( x in X implies ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,q,R)) . x )
assume
x in X
;
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,q,R)) . x
then
(
x on K &
((IncProj (K,q,R)) * (IncProj (K,p,K))) . x = (IncProj (K,q,R)) . ((IncProj (K,p,K)) . x) )
by A3, A4, A113, A107, A114, Def1, FUNCT_1:12;
hence
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,q,R)) . x
by A1, A113, Th18;
verum
end; take q =
q;
ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )
dom (IncProj (K,q,R)) c= X
then
X = dom (IncProj (K,q,R))
by A114, XBOOLE_0:def 10;
hence
ex
o being
POINT of
IPP st
( not
o on K & not
o on R &
(IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (
K,
o,
R) )
by A3, A4, A113, A111, A116, A112, PARTFUN1:5;
verum end; hence
ex
o being
POINT of
IPP st
( not
o on K & not
o on R &
(IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (
K,
o,
R) )
by A12, A55;
verum end;
now ( p = q implies ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) ) )A118:
X c= dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
proof
let e be
object ;
TARSKI:def 3 ( not e in X or e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) )
assume A119:
e in X
;
e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
then reconsider e =
e as
POINT of
IPP by A9;
A120:
ex
e9 being
Element of the
Points of
IPP st
(
e = e9 &
e9 on K )
by A9, A119;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L))
by A1, A2, A3, A4, Th22;
hence
e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
by A1, A2, A120, Def1;
verum
end; assume A121:
p = q
;
ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )A122:
X c= dom (IncProj (K,p,R))
proof
let e be
object ;
TARSKI:def 3 ( not e in X or e in dom (IncProj (K,p,R)) )
assume A123:
e in X
;
e in dom (IncProj (K,p,R))
then reconsider e =
e as
POINT of
IPP by A9;
ex
e9 being
POINT of
IPP st
(
e = e9 &
e9 on K )
by A9, A123;
hence
e in dom (IncProj (K,p,R))
by A1, A4, A121, Def1;
verum
end; A124:
for
x being
POINT of
IPP st
x in X holds
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x
proof
let x be
POINT of
IPP;
( x in X implies ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x )
assume A125:
x in X
;
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x
then A126:
((IncProj (L,p,R)) * (IncProj (K,p,L))) . x = (IncProj (L,p,R)) . ((IncProj (K,p,L)) . x)
by A121, A118, FUNCT_1:12;
A127:
x on K
by A1, A4, A121, A122, A125, Def1;
then reconsider y =
(IncProj (K,p,L)) . x as
POINT of
IPP by A1, A2, Th19;
A128:
y on L
by A1, A2, A127, Th20;
then reconsider z =
(IncProj (L,p,R)) . y as
POINT of
IPP by A2, A4, A121, Th19;
consider A being
LINE of
IPP such that A129:
(
p on A &
y on A )
by INCPROJ:def 5;
A130:
z on R
by A2, A4, A121, A128, Th20;
then consider C being
LINE of
IPP such that A131:
(
p on C &
y on C )
and A132:
z on C
by A2, A4, A121, A128, Def1;
A133:
A = C
by A2, A128, A129, A131, INCPROJ:def 4;
consider B being
LINE of
IPP such that A134:
p on B
and A135:
x on B
and A136:
y on B
by A1, A2, A127, A128, Def1;
A = B
by A2, A128, A129, A134, A136, INCPROJ:def 4;
hence
((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x
by A1, A4, A121, A127, A126, A134, A135, A130, A132, A133, Def1;
verum
end;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= X
proof
let e be
object ;
TARSKI:def 3 ( not e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) or e in X )
assume
e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
;
e in X
then A137:
e in dom (IncProj (K,p,L))
by A1, A2, A3, A4, Th22;
then reconsider e =
e as
POINT of
IPP ;
e on K
by A1, A2, A137, Def1;
hence
e in X
by A9;
verum
end; then A138:
X = dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))
by A118, XBOOLE_0:def 10;
A139:
(IncProj (L,q,R)) * (IncProj (K,p,L)) is
PartFunc of the
Points of
IPP, the
Points of
IPP
by A10, RELSET_1:4;
dom (IncProj (K,p,R)) c= X
then
X = dom (IncProj (K,p,R))
by A122, XBOOLE_0:def 10;
hence
ex
o being
POINT of
IPP st
( not
o on K & not
o on R &
(IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (
K,
o,
R) )
by A1, A4, A121, A138, A124, A139, PARTFUN1:5;
verum end;
hence
ex o being POINT of IPP st
( not o on K & not o on R & (IncProj (L,q,R)) * (IncProj (K,p,L)) = IncProj (K,o,R) )
by A11; verum