let V be non trivial RealLinearSpace; ( 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 )
; ProjectiveSpace V is at_least_3rank
A2:
not are_Prop u,v
by A1, Lm1;
let p be Element of (ProjectiveSpace V); ANPROJ_2:def 10 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); 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
; ( p <> r & q <> r & p,q,r are_collinear )
thus
p <> r
by A3, A5, A7, ANPROJ_1:22; ( q <> r & p,q,r are_collinear )
thus
q <> r
by A4, A5, A8, ANPROJ_1:22; p,q,r are_collinear
thus
p,q,r are_collinear
by A3, A4, A5, A6, Th23; verum