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
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 is_collinear )
let q be Element of (ProjectiveSpace V); :: thesis: ex r being Element of (ProjectiveSpace V) st
( p <> r & q <> r & p,q,r is_collinear )
consider y being Element of V such that
A2: ( not y is zero & p = Dir y ) by ANPROJ_1:42;
consider w being Element of V such that
A3: ( not w is zero & q = Dir w ) by ANPROJ_1:42;
A4: ( not u is zero & not v is zero ) by A1, Lm1;
not are_Prop u,v by A1, Lm1;
then consider z being Element of V such that
A5: ( not z is zero & y,w,z are_LinDep & not are_Prop y,z & not are_Prop w,z ) by A4, ANPROJ_1:21;
reconsider r = Dir z as Element of (ProjectiveSpace V) by A5, ANPROJ_1:42;
take r ; :: thesis: ( p <> r & q <> r & p,q,r is_collinear )
thus p <> r by A2, A5, ANPROJ_1:35; :: thesis: ( q <> r & p,q,r is_collinear )
thus q <> r by A3, A5, ANPROJ_1:35; :: thesis: p,q,r is_collinear
thus p,q,r is_collinear by A2, A3, A5, Th24; :: thesis: verum