let V be non trivial RealLinearSpace; for u, v, w being Element of V st not u is zero & not v is zero & not w is zero holds
( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep )
let u, v, w be Element of V; ( not u is zero & not v is zero & not w is zero implies ( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep ) )
assume that
A1:
( not u is zero & not v is zero )
and
A2:
not w is zero
; ( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep )
now ( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) implies u,v,w are_LinDep )reconsider du =
Dir u,
dv =
Dir v,
dw =
Dir w as
set ;
assume
[(Dir u),(Dir v),(Dir w)] in the
Collinearity of
(ProjectiveSpace V)
;
u,v,w are_LinDep then consider p,
q,
r being
Element of
V such that A3:
(
du = Dir p &
dv = Dir q )
and A4:
dw = Dir r
and A5:
( not
p is
zero & not
q is
zero )
and A6:
not
r is
zero
and A7:
p,
q,
r are_LinDep
by Def6;
A8:
are_Prop r,
w
by A2, A4, A6, Th22;
(
are_Prop p,
u &
are_Prop q,
v )
by A1, A3, A5, Th22;
hence
u,
v,
w are_LinDep
by A7, A8, Th4;
verum end;
hence
( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep )
by A1, A2, Def6; verum