let u, v, w be Element of (TOP-REAL 3); for P1, P2, P3 being Element of (ProjectiveSpace (TOP-REAL 3)) st not u is zero & not v is zero & not w is zero & P1 = Dir u & P2 = Dir v & P3 = Dir w holds
( P1,P2,P3 are_collinear iff |{u,v,w}| = 0 )
let P1, P2, P3 be Element of (ProjectiveSpace (TOP-REAL 3)); ( not u is zero & not v is zero & not w is zero & P1 = Dir u & P2 = Dir v & P3 = Dir w implies ( P1,P2,P3 are_collinear iff |{u,v,w}| = 0 ) )
assume that
A1:
not u is zero
and
A2:
not v is zero
and
A3:
not w is zero
and
A4:
P1 = Dir u
and
A5:
P2 = Dir v
and
A6:
P3 = Dir w
; ( P1,P2,P3 are_collinear iff |{u,v,w}| = 0 )
hereby ( |{u,v,w}| = 0 implies P1,P2,P3 are_collinear )
assume
P1,
P2,
P3 are_collinear
;
|{u,v,w}| = 0 then consider u9,
v9,
w9 being
Element of
(TOP-REAL 3) such that A7:
P1 = Dir u9
and A8:
P2 = Dir v9
and A9:
(
P3 = Dir w9 & not
u9 is
zero & not
v9 is
zero & not
w9 is
zero &
u9,
v9,
w9 are_LinDep )
by ANPROJ_2:23;
[(Dir u9),(Dir v9),(Dir w9)] in the
Collinearity of
(ProjectiveSpace (TOP-REAL 3))
by A9, ANPROJ_1:25;
then
u,
v,
w are_LinDep
by A7, A8, A9, A1, A2, A3, A4, A5, A6, ANPROJ_1:25;
hence
|{u,v,w}| = 0
by ANPROJ_8:43;
verum
end;
thus
( |{u,v,w}| = 0 implies P1,P2,P3 are_collinear )
by A1, A2, A3, A4, A5, A6, ANPROJ_2:23, ANPROJ_8:43; verum