let R be POINT of (IncProjSp_of real_projective_plane); for L being LINE of (IncProjSp_of real_projective_plane)
for p, q being Point of real_projective_plane
for u, v, w being non zero Element of (TOP-REAL 3) st p = Dir u & q = Dir v & R = Dir w & L = Line (p,q) holds
( R on L iff |{u,v,w}| = 0 )
let L be LINE of (IncProjSp_of real_projective_plane); for p, q being Point of real_projective_plane
for u, v, w being non zero Element of (TOP-REAL 3) st p = Dir u & q = Dir v & R = Dir w & L = Line (p,q) holds
( R on L iff |{u,v,w}| = 0 )
let p, q be Point of real_projective_plane; for u, v, w being non zero Element of (TOP-REAL 3) st p = Dir u & q = Dir v & R = Dir w & L = Line (p,q) holds
( R on L iff |{u,v,w}| = 0 )
let u, v, w be non zero Element of (TOP-REAL 3); ( p = Dir u & q = Dir v & R = Dir w & L = Line (p,q) implies ( R on L iff |{u,v,w}| = 0 ) )
assume that
A1:
p = Dir u
and
A2:
q = Dir v
and
A3:
R = Dir w
and
A4:
L = Line (p,q)
; ( R on L iff |{u,v,w}| = 0 )
reconsider r = Dir w as Point of real_projective_plane by ANPROJ_1:26;
hereby ( |{u,v,w}| = 0 implies R on L )
assume
R on L
;
|{u,v,w}| = 0 then
p,
q,
r are_collinear
by A3, A4, Th61;
then consider u1,
v1,
w1 being
Element of
(TOP-REAL 3) such that A5:
p = Dir u1
and A6:
q = Dir v1
and A7:
r = Dir w1
and A8:
( not
u1 is
zero & not
v1 is
zero & not
w1 is
zero )
and A9:
(
u1 = v1 or
u1 = w1 or
v1 = w1 or
{u1,v1,w1} is
linearly-dependent )
by ANPROJ_8:10;
u1,
v1,
w1 are_LinDep
by A9, ANPROJ_8:9;
then
|{u1,v1,w1}| = 0
by ANPROJ_8:43;
then
|{u,v1,w1}| = 0
by A1, A5, A8, ANPROJ_8:58;
then
|{u,v,w1}| = 0
by A2, A6, A8, ANPROJ_8:59;
hence
|{u,v,w}| = 0
by A8, A7, ANPROJ_8:60;
verum
end;
assume
|{u,v,w}| = 0
; R on L
then
( u = v or u = w or v = w or {u,v,w} is linearly-dependent )
by ANPROJ_8:9, ANPROJ_8:43;
then
p,q,r are_collinear
by A1, A2, ANPROJ_8:10;
hence
R on L
by A3, A4, Th61; verum