let V be non trivial RealLinearSpace; for p, q, r being Element of (ProjectiveSpace V) holds
( p,q,r are_collinear iff ex u, v, w being Element of V st
( p = Dir u & q = Dir v & r = Dir w & not u is zero & not v is zero & not w is zero & ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) ) )
let p, q, r be Element of (ProjectiveSpace V); ( p,q,r are_collinear iff ex u, v, w being Element of V st
( p = Dir u & q = Dir v & r = Dir w & not u is zero & not v is zero & not w is zero & ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) ) )
hereby ( ex u, v, w being Element of V st
( p = Dir u & q = Dir v & r = Dir w & not u is zero & not v is zero & not w is zero & ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) ) implies p,q,r are_collinear )
assume
p,
q,
r are_collinear
;
ex u, v, w being Element of V st
( p = Dir u & q = Dir v & r = Dir w & not u is zero & not v is zero & not w is zero & ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) )then consider u,
v,
w being
Element of
V such that A1:
(
p = Dir u &
q = Dir v &
r = Dir w & not
u is
zero & not
v is
zero & not
w is
zero &
u,
v,
w are_LinDep )
by ANPROJ_2:23;
take u =
u;
ex v, w being Element of V st
( p = Dir u & q = Dir v & r = Dir w & not u is zero & not v is zero & not w is zero & ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) )take v =
v;
ex w being Element of V st
( p = Dir u & q = Dir v & r = Dir w & not u is zero & not v is zero & not w is zero & ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) )take w =
w;
( p = Dir u & q = Dir v & r = Dir w & not u is zero & not v is zero & not w is zero & ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) )thus
(
p = Dir u &
q = Dir v &
r = Dir w & not
u is
zero & not
v is
zero & not
w is
zero & ex
a,
b,
c being
Real st
(
((a * u) + (b * v)) + (c * w) = 0. V & (
a <> 0 or
b <> 0 or
c <> 0 ) ) )
by A1, ANPROJ_1:def 2;
verum
end;
given u, v, w being Element of V such that A2:
( p = Dir u & q = Dir v & r = Dir w & not u is zero & not v is zero & not w is zero & ex a, b, c being Real st
( ((a * u) + (b * v)) + (c * w) = 0. V & ( a <> 0 or b <> 0 or c <> 0 ) ) )
; p,q,r are_collinear
( p = Dir u & q = Dir v & r = Dir w & not u is zero & not v is zero & not w is zero & u,v,w are_LinDep )
by A2, ANPROJ_1:def 2;
hence
p,q,r are_collinear
by ANPROJ_2:23; verum