let V be non trivial RealLinearSpace; :: thesis: ( ex u, v being Element of V st
for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) implies ProjectiveSpace V is at_least_3rank )
given u, v being Element of V such that A1: for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ; :: thesis: ProjectiveSpace V is at_least_3rank
A2: not are_Prop u,v by A1, Lm1;
let p be Element of (ProjectiveSpace V); :: according to ANPROJ_2:def 10 :: thesis: for q being Element of (ProjectiveSpace V) ex r being Element of (ProjectiveSpace V) st
( p <> r & q <> r & p,q,r are_collinear )
let q be Element of (ProjectiveSpace V); :: thesis: ex r being Element of (ProjectiveSpace V) st
( p <> r & q <> r & p,q,r are_collinear )
consider y being Element of V such that
A3: ( not y is zero & p = Dir y ) by ANPROJ_1:26;
consider w being Element of V such that
A4: ( not w is zero & q = Dir w ) by ANPROJ_1:26;
( not u is zero & not v is zero ) by A1, Lm1;
then consider z being Element of V such that
A5: not z is zero and
A6: y,w,z are_LinDep and
A7: not are_Prop y,z and
A8: not are_Prop w,z by A2, ANPROJ_1:16;
reconsider r = Dir z as Element of (ProjectiveSpace V) by A5, ANPROJ_1:26;
take r ; :: thesis: ( p <> r & q <> r & p,q,r are_collinear )
thus p <> r by A3, A5, A7, ANPROJ_1:22; :: thesis: ( q <> r & p,q,r are_collinear )
thus q <> r by A4, A5, A8, ANPROJ_1:22; :: thesis: p,q,r are_collinear
thus p,q,r are_collinear by A3, A4, A5, A6, Th23; :: thesis: verum