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 that

A1: ( not u is zero & not v is zero ) and

A2: not w is zero ; :: thesis: ( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep )

( [(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 that

A1: ( not u is zero & not v is zero ) and

A2: not w is zero ; :: thesis: ( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep )

now :: thesis: ( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) implies u,v,w are_LinDep )

hence
( [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) iff u,v,w are_LinDep )
by A1, A2, Def6; :: thesis: verumreconsider du = Dir u, dv = Dir v, dw = Dir w as set ;

assume [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) ; :: thesis: 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; :: thesis: verum

end;assume [(Dir u),(Dir v),(Dir w)] in the Collinearity of (ProjectiveSpace V) ; :: thesis: 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; :: thesis: verum