let V be non trivial RealLinearSpace; :: thesis: 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; :: thesis: ( 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 A1:
( not u is zero & not v is zero & not w is zero )
; :: thesis: ( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep )
now assume A2:
[(Dir u),(Dir v),(Dir w)] in the
Collinearity of
(ProjectiveSpace V)
;
:: thesis: u,v,w are_LinDep reconsider du =
Dir u,
dv =
Dir v,
dw =
Dir w as
set ;
consider p,
q,
r being
Element of
V such that A3:
(
du = Dir p &
dv = Dir q &
dw = Dir r & not
p is
zero & not
q is
zero & not
r is
zero &
p,
q,
r are_LinDep )
by A2, Def9;
(
are_Prop p,
u &
are_Prop q,
v &
are_Prop r,
w )
by A1, A3, Th35;
hence
u,
v,
w are_LinDep
by A3, Th9;
:: thesis: verum end;
hence
( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep )
by A1, Def9; :: thesis: verum