let V be non trivial RealLinearSpace; :: thesis: ( ex u, v, w being Element of V st
( ( for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V holds
( a = 0 & b = 0 & c = 0 ) ) & ( for y being Element of V ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) ) implies ex x1, x2 being Element of (ProjectiveSpace V) st
( x1 <> x2 & ( for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st
( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) ) )
given p, q, r being Element of V such that A1: for a, b, c being Real st ((a * p) + (b * q)) + (c * r) = 0. V holds
( a = 0 & b = 0 & c = 0 ) and
A2: for y being Element of V ex a, b, c being Real st y = ((a * p) + (b * q)) + (c * r) ; :: thesis: ex x1, x2 being Element of (ProjectiveSpace V) st
( x1 <> x2 & ( for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st
( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) )
A3: ( not p is zero & not q is zero ) by A1, Th1;
then reconsider x1 = Dir p, x2 = Dir q as Element of (ProjectiveSpace V) by ANPROJ_1:26;
take x1 ; :: thesis: ex x2 being Element of (ProjectiveSpace V) st
( x1 <> x2 & ( for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st
( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) )
take x2 ; :: thesis: ( x1 <> x2 & ( for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st
( x1,x2,q are_collinear & r1,r2,q are_collinear ) ) )
not are_Prop p,q by A1, Th1;
hence x1 <> x2 by A3, ANPROJ_1:22; :: thesis: for r1, r2 being Element of (ProjectiveSpace V) ex q being Element of (ProjectiveSpace V) st
( x1,x2,q are_collinear & r1,r2,q are_collinear )
let r1, r2 be Element of (ProjectiveSpace V); :: thesis: ex q being Element of (ProjectiveSpace V) st
( x1,x2,q are_collinear & r1,r2,q are_collinear )
consider u being Element of V such that
A4: ( not u is zero & r1 = Dir u ) by ANPROJ_1:26;
consider u1 being Element of V such that
A5: ( not u1 is zero & r2 = Dir u1 ) by ANPROJ_1:26;
consider y being Element of V such that
A6: p,q,y are_LinDep and
A7: u,u1,y are_LinDep and
A8: not y is zero by A1, A2, Th3;
reconsider q = Dir y as Element of (ProjectiveSpace V) by A8, ANPROJ_1:26;
take q ; :: thesis: ( x1,x2,q are_collinear & r1,r2,q are_collinear )
thus x1,x2,q are_collinear by A3, A6, A8, Th23; :: thesis: r1,r2,q are_collinear
thus r1,r2,q are_collinear by A4, A5, A7, A8, Th23; :: thesis: verum