let V be RealLinearSpace; :: thesis: for P, Q, R, S being Element of V st P,Q,R,S are_collinear & R <> Q & S <> Q & S <> P holds
( R = P iff cross-ratio (P,Q,R,S) = 0 )
let P, Q, R, S be Element of V; :: thesis: ( P,Q,R,S are_collinear & R <> Q & S <> Q & S <> P implies ( R = P iff cross-ratio (P,Q,R,S) = 0 ) )
assume that
A1: P,Q,R,S are_collinear and
A2: R <> Q and
A3: S <> Q and
A4: S <> P ; :: thesis: ( R = P iff cross-ratio (P,Q,R,S) = 0 )
consider L being line of V such that
A5: ( P in L & Q in L & R in L & S in L ) by A1;
A6: ( R,P,Q are_collinear & S,P,Q are_collinear ) by A5;
hereby :: thesis: ( cross-ratio (P,Q,R,S) = 0 implies R = P )
assume R = P ; :: thesis: cross-ratio (P,Q,R,S) = 0
then affine-ratio (R,P,Q) = 0 by A6, A2, Th06;
hence cross-ratio (P,Q,R,S) = 0 ; :: thesis: verum
end;
assume A7: cross-ratio (P,Q,R,S) = 0 ; :: thesis: R = P
per cases ( affine-ratio (S,P,Q) = 0 or affine-ratio (S,P,Q) <> 0 ) ;
suppose affine-ratio (S,P,Q) = 0 ; :: thesis: R = P
hence R = P by A3, A4, A6, Th06; :: thesis: verum
end;
suppose affine-ratio (S,P,Q) <> 0 ; :: thesis: R = P
then affine-ratio (R,P,Q) = 0 by A7;
hence R = P by A2, A6, Th06; :: thesis: verum
end;
end;