let AS be AffinSpace; for a, b, c, d, p being POINT of (IncProjSp_of AS)
for M, N, P, Q being LINE of (IncProjSp_of AS) 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 (IncProjSp_of AS) st
( q on P & q on Q )
let a, b, c, d, p be POINT of (IncProjSp_of AS); for M, N, P, Q being LINE of (IncProjSp_of AS) 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 (IncProjSp_of AS) st
( q on P & q on Q )
let M, N, P, Q be LINE of (IncProjSp_of AS); ( 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 (IncProjSp_of AS) st
( q on P & q on Q ) )
assume that
A1:
a on M
and
A2:
b on M
and
A3:
c on N
and
A4:
d on N
and
A5:
p on M
and
A6:
p on N
and
A7:
a on P
and
A8:
c on P
and
A9:
b on Q
and
A10:
d on Q
and
A11:
not p on P
and
A12:
not p on Q
and
A13:
M <> N
; ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
now ( p is not Element of AS implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )assume A14:
p is not
Element of
AS
;
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )now ( a is not Element of AS & b is not Element of AS & c is not Element of AS & d is not Element of AS implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )A15:
b <> d
by A2, A4, A5, A6, A9, A12, A13, Lm2;
set x = the
Element of
AS;
assume that A16:
a is not
Element of
AS
and A17:
b is not
Element of
AS
and A18:
c is not
Element of
AS
and A19:
d is not
Element of
AS
;
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )consider Xa being
Subset of
AS such that A20:
a = LDir Xa
and A21:
Xa is
being_line
by A16, Th20;
consider Xc being
Subset of
AS such that A22:
c = LDir Xc
and A23:
Xc is
being_line
by A18, Th20;
consider Xb being
Subset of
AS such that A24:
b = LDir Xb
and A25:
Xb is
being_line
by A17, Th20;
consider Xd being
Subset of
AS such that A26:
d = LDir Xd
and A27:
Xd is
being_line
by A19, Th20;
consider Xp being
Subset of
AS such that A28:
p = LDir Xp
and A29:
Xp is
being_line
by A14, Th20;
set Xa9 = the
Element of
AS * Xa;
set Xb9 = the
Element of
AS * Xb;
set Xc9 = the
Element of
AS * Xc;
set Xd9 = the
Element of
AS * Xd;
set Xp9 = the
Element of
AS * Xp;
consider y being
Element of
AS such that A30:
the
Element of
AS <> y
and A31:
y in the
Element of
AS * Xa
by A21, AFF_1:20, AFF_4:27;
A32:
Xp // the
Element of
AS * Xp
by A29, AFF_4:def 3;
consider t being
Element of
AS such that A33:
the
Element of
AS <> t
and A34:
t in the
Element of
AS * Xc
by A23, AFF_1:20, AFF_4:27;
set Y1 =
y * ( the Element of AS * Xp);
set Y2 =
t * ( the Element of AS * Xp);
A35:
the
Element of
AS * Xp is
being_line
by A29, AFF_4:27;
then A36:
y * ( the Element of AS * Xp) is
being_line
by AFF_4:27;
A37:
t * ( the Element of AS * Xp) is
being_line
by A35, AFF_4:27;
A38:
Xb // the
Element of
AS * Xb
by A25, AFF_4:def 3;
A39:
the
Element of
AS * Xd is
being_line
by A27, AFF_4:27;
A40:
Xd // the
Element of
AS * Xd
by A27, AFF_4:def 3;
A41:
the
Element of
AS in the
Element of
AS * Xc
by A23, AFF_4:def 3;
A42:
the
Element of
AS in the
Element of
AS * Xb
by A25, AFF_4:def 3;
A43:
the
Element of
AS * Xb is
being_line
by A25, AFF_4:27;
A44:
the
Element of
AS in the
Element of
AS * Xd
by A27, AFF_4:def 3;
then consider XQ being
Subset of
AS such that A45:
the
Element of
AS * Xb c= XQ
and A46:
the
Element of
AS * Xd c= XQ
and A47:
XQ is
being_plane
by A43, A39, A42, AFF_4:38;
A48:
the
Element of
AS * Xa is
being_line
by A21, AFF_4:27;
A49:
the
Element of
AS * Xp // t * ( the Element of AS * Xp)
by A35, AFF_4:def 3;
A50:
not the
Element of
AS * Xd // t * ( the Element of AS * Xp)
A51:
the
Element of
AS * Xp // y * ( the Element of AS * Xp)
by A35, AFF_4:def 3;
A52:
not the
Element of
AS * Xb // y * ( the Element of AS * Xp)
A53:
the
Element of
AS in the
Element of
AS * Xa
by A21, AFF_4:def 3;
A54:
the
Element of
AS * Xc is
being_line
by A23, AFF_4:27;
then consider XP being
Subset of
AS such that A55:
the
Element of
AS * Xa c= XP
and A56:
the
Element of
AS * Xc c= XP
and A57:
XP is
being_plane
by A48, A53, A41, AFF_4:38;
A58:
the
Element of
AS in the
Element of
AS * Xp
by A29, AFF_4:def 3;
then consider X2 being
Subset of
AS such that A59:
the
Element of
AS * Xc c= X2
and A60:
the
Element of
AS * Xp c= X2
and A61:
X2 is
being_plane
by A54, A35, A41, AFF_4:38;
A62:
Xc // the
Element of
AS * Xc
by A23, AFF_4:def 3;
N = [(PDir X2),2]
proof
reconsider N9 =
[(PDir X2),2] as
Element of the
Lines of
(IncProjSp_of AS) by A61, Th23;
A63:
c on N9
by A22, A62, A59, A61, Th32;
p on N9
by A28, A32, A60, A61, Th32;
hence
N = [(PDir X2),2]
by A3, A6, A8, A11, A63, Lm2;
verum
end; then
Xd '||' X2
by A4, A26, A27, A61, Th29;
then A64:
the
Element of
AS * Xd c= X2
by A39, A41, A44, A40, A59, A61, AFF_4:43, AFF_4:56;
consider X1 being
Subset of the
carrier of
AS such that A65:
the
Element of
AS * Xa c= X1
and A66:
the
Element of
AS * Xp c= X1
and A67:
X1 is
being_plane
by A48, A35, A53, A58, AFF_4:38;
A68:
Xa // the
Element of
AS * Xa
by A21, AFF_4:def 3;
M = [(PDir X1),2]
proof
reconsider M9 =
[(PDir X1),2] as
Element of the
Lines of
(IncProjSp_of AS) by A67, Th23;
A69:
a on M9
by A20, A68, A65, A67, Th32;
p on M9
by A28, A32, A66, A67, Th32;
hence
M = [(PDir X1),2]
by A1, A5, A7, A11, A69, Lm2;
verum
end; then
Xb '||' X1
by A2, A24, A25, A67, Th29;
then A70:
the
Element of
AS * Xb c= X1
by A43, A53, A42, A38, A65, A67, AFF_4:43, AFF_4:56;
y * ( the Element of AS * Xp) c= X1
by A29, A31, A65, A66, A67, AFF_4:27, AFF_4:28;
then consider z being
Element of
AS such that A71:
z in the
Element of
AS * Xb
and A72:
z in y * ( the Element of AS * Xp)
by A43, A36, A67, A70, A52, AFF_4:22;
t * ( the Element of AS * Xp) c= X2
by A29, A34, A59, A60, A61, AFF_4:27, AFF_4:28;
then consider u being
Element of
AS such that A73:
u in the
Element of
AS * Xd
and A74:
u in t * ( the Element of AS * Xp)
by A39, A37, A61, A64, A50, AFF_4:22;
set AC =
Line (
y,
t);
set BD =
Line (
z,
u);
A75:
y in Line (
y,
t)
by AFF_1:15;
A76:
y in y * ( the Element of AS * Xp)
by A35, AFF_4:def 3;
A77:
the
Element of
AS <> z
proof
assume A78:
not the
Element of
AS <> z
;
contradiction
a =
LDir ( the Element of AS * Xa)
by A20, A21, A48, A68, Th11
.=
LDir (y * ( the Element of AS * Xp))
by A48, A53, A30, A31, A36, A76, A72, A78, AFF_1:18
.=
LDir ( the Element of AS * Xp)
by A35, A36, A51, Th11
.=
p
by A28, A29, A35, A32, Th11
;
hence
contradiction
by A7, A11;
verum
end; A79:
z <> u
proof
assume A80:
not
z <> u
;
contradiction
b =
LDir ( the Element of AS * Xb)
by A24, A25, A43, A38, Th11
.=
LDir ( the Element of AS * Xd)
by A43, A39, A42, A44, A71, A73, A77, A80, AFF_1:18
.=
d
by A26, A27, A39, A40, Th11
;
hence
contradiction
by A2, A4, A5, A6, A9, A12, A13, Lm2;
verum
end; then A81:
Line (
z,
u) is
being_line
by AFF_1:def 3;
A82:
the
Element of
AS * Xa <> the
Element of
AS * Xc
proof
assume
the
Element of
AS * Xa = the
Element of
AS * Xc
;
contradiction
then a =
LDir ( the Element of AS * Xc)
by A20, A21, A48, A68, Th11
.=
c
by A22, A23, A54, A62, Th11
;
hence
contradiction
by A1, A3, A5, A6, A7, A11, A13, Lm2;
verum
end; then A83:
y <> t
by A48, A54, A53, A41, A30, A31, A34, AFF_1:18;
then A84:
Line (
y,
t) is
being_line
by AFF_1:def 3;
A85:
Line (
z,
u)
c= XQ
by A71, A73, A79, A45, A46, A47, AFF_4:19;
A86:
t in Line (
y,
t)
by AFF_1:15;
y * ( the Element of AS * Xp) // t * ( the Element of AS * Xp)
by A51, A49, AFF_1:44;
then consider X3 being
Subset of
AS such that A87:
y * ( the Element of AS * Xp) c= X3
and A88:
t * ( the Element of AS * Xp) c= X3
and A89:
X3 is
being_plane
by AFF_4:39;
A90:
Line (
z,
u)
c= X3
by A87, A88, A89, A72, A74, A79, AFF_4:19;
A91:
a <> c
by A1, A3, A5, A6, A7, A11, A13, Lm2;
A92:
(
P = [(PDir XP),2] &
Q = [(PDir XQ),2] )
proof
reconsider P9 =
[(PDir XP),2],
Q9 =
[(PDir XQ),2] as
LINE of
(IncProjSp_of AS) by A57, A47, Th23;
A93:
c on P9
by A22, A62, A56, A57, Th32;
A94:
b on Q9
by A24, A38, A45, A47, Th32;
A95:
d on Q9
by A26, A40, A46, A47, Th32;
a on P9
by A20, A68, A55, A57, Th32;
hence
(
P = [(PDir XP),2] &
Q = [(PDir XQ),2] )
by A7, A8, A9, A10, A91, A15, A93, A94, A95, Lm2;
verum
end; A96:
now ( Line (y,t) // Line (z,u) implies ex q being Element of the Points of (IncProjSp_of AS) st
( q on P & q on Q ) )reconsider q =
LDir (Line (y,t)),
q9 =
LDir (Line (z,u)) as
Element of the
Points of
(IncProjSp_of AS) by A84, A81, Th20;
assume A97:
Line (
y,
t)
// Line (
z,
u)
;
ex q being Element of the Points of (IncProjSp_of AS) st
( q on P & q on Q )take q =
q;
( q on P & q on Q )
q = q9
by A84, A81, A97, Th11;
hence
(
q on P &
q on Q )
by A31, A34, A71, A73, A83, A79, A84, A81, A55, A56, A57, A45, A46, A47, A92, Th31, AFF_4:19;
verum end; A98:
Line (
y,
t)
c= XP
by A31, A34, A83, A55, A56, A57, AFF_4:19;
A99:
now ( ex w being Element of AS st
( w in Line (y,t) & w in Line (z,u) ) implies ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q ) )given w being
Element of
AS such that A100:
w in Line (
y,
t)
and A101:
w in Line (
z,
u)
;
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )set R =
Line ( the
Element of
AS,
w);
A102:
the
Element of
AS <> w
proof
assume A103:
the
Element of
AS = w
;
contradiction
then
the
Element of
AS * Xa = Line (
y,
t)
by A48, A53, A30, A31, A84, A75, A100, AFF_1:18;
hence
contradiction
by A54, A41, A33, A34, A82, A84, A86, A100, A103, AFF_1:18;
verum
end; then A104:
Line ( the
Element of
AS,
w) is
being_line
by AFF_1:def 3;
then reconsider q =
LDir (Line ( the Element of AS,w)) as
POINT of
(IncProjSp_of AS) by Th20;
take q =
q;
( q on P & q on Q )thus
(
q on P &
q on Q )
by A53, A42, A55, A57, A45, A47, A92, A98, A85, A100, A101, A102, A104, Th31, AFF_4:19;
verum end;
t in t * ( the Element of AS * Xp)
by A35, AFF_4:def 3;
then
Line (
y,
t)
c= X3
by A76, A87, A88, A89, A83, AFF_4:19;
hence
ex
q being
POINT of
(IncProjSp_of AS) st
(
q on P &
q on Q )
by A89, A84, A81, A90, A96, A99, AFF_4:22;
verum end; hence
ex
q being
POINT of
(IncProjSp_of AS) st
(
q on P &
q on Q )
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, Lm11;
verum end;
hence
ex q being POINT of (IncProjSp_of AS) st
( q on P & q on Q )
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, Lm9; verum