let V be non trivial RealLinearSpace; :: thesis:
given y, u, v, w being Element of V such that A1: for w1 being Element of V ex a, b, a1, b1 being Real st w1 = (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) and
A2: for a, b, a1, b1 being Real st (((a * y) + (b * u)) + (a1 * v)) + (b1 * w) = 0. V holds
( a = 0 & b = 0 & a1 = 0 & b1 = 0 ) ; :: thesis:
A3: ( not u is zero & not v is zero ) by A2, Th2;
A4: not y is zero by A2, Th2;
then reconsider p = Dir y, q1 = Dir u, q2 = Dir v as Element of (ProjectiveSpace V) by A3, ANPROJ_1:26;
take p ; :: thesis:
take q1 ; :: thesis:
take q2 ; :: thesis:
not y,u,v are_LinDep by A2, Th2;
then not p,q1,q2 are_collinear by A4, A3, ANPROJ_1:25;
hence not p,q1,q2 are_collinear ; :: thesis:
let r1, r2 be Element of (ProjectiveSpace V); :: thesis:
consider u1 being Element of V such that
A5: not u1 is zero and
A6: r1 = Dir u1 by ANPROJ_1:26;
consider u2 being Element of V such that
A7: not u2 is zero and
A8: r2 = Dir u2 by ANPROJ_1:26;
consider w1, w2 being Element of V such that
A9: u1,u2,w2 are_LinDep and
A10: u,v,w1 are_LinDep and
A11: y,w2,w1 are_LinDep and
A12: not w1 is zero and
A13: not w2 is zero by A1, A2, A5, A7, Th4;
reconsider q3 = Dir w1, r3 = Dir w2 as Element of (ProjectiveSpace V) by A12, A13, ANPROJ_1:26;
take q3 ; :: thesis:
take r3 ; :: thesis:
thus r1,r2,r3 are_collinear by A5, A6, A7, A8, A9, A13, Th23; :: thesis:
thus q1,q2,q3 are_collinear by A3, A10, A12, Th23; :: thesis:
thus p,r3,q3 are_collinear by A4, A11, A12, A13, Th23; :: thesis: