let SAS be Semi_Affine_Space; :: thesis: for a, b, c, d, o being Element of SAS holds
( o, diff (b,a,o), diff (d,c,o) are_collinear iff a,b // c,d )
let a, b, c, d, o be Element of SAS; :: thesis: ( o, diff (b,a,o), diff (d,c,o) are_collinear iff a,b // c,d )
A1: ( a,b // c,d implies o, diff (b,a,o), diff (d,c,o) are_collinear )
proof
assume A2: a,b // c,d ; :: thesis: o, diff (b,a,o), diff (d,c,o) are_collinear
A3: now :: thesis: ( a <> b & c <> d implies o, diff (b,a,o), diff (d,c,o) are_collinear )
o, diff (d,c,o) // c,d by Th88;
then A4: c,d // o, diff (d,c,o) by Th6;
assume that
A5: a <> b and
A6: c <> d ; :: thesis: o, diff (b,a,o), diff (d,c,o) are_collinear
o, diff (b,a,o) // a,b by Th88;
then a,b // o, diff (b,a,o) by Th6;
then o, diff (b,a,o) // c,d by A2, A5, Def1;
then o, diff (b,a,o) // o, diff (d,c,o) by A6, A4, Th8;
hence o, diff (b,a,o), diff (d,c,o) are_collinear ; :: thesis: verum
end;
now :: thesis: ( ( a = b or c = d ) implies o, diff (b,a,o), diff (d,c,o) are_collinear )
assume ( a = b or c = d ) ; :: thesis: o, diff (b,a,o), diff (d,c,o) are_collinear
then ( o = diff (b,a,o) or o = diff (d,c,o) ) by Th87;
then o, diff (b,a,o) // o, diff (d,c,o) by Def1, Th3;
hence o, diff (b,a,o), diff (d,c,o) are_collinear ; :: thesis: verum
end;
hence o, diff (b,a,o), diff (d,c,o) are_collinear by A3; :: thesis: verum
end;
( o, diff (b,a,o), diff (d,c,o) are_collinear implies a,b // c,d )
proof
assume A7: o, diff (b,a,o), diff (d,c,o) are_collinear ; :: thesis: a,b // c,d
A8: now :: thesis: ( o <> diff (b,a,o) & o <> diff (d,c,o) implies a,b // c,d )
A9: o, diff (d,c,o) // c,d by Th88;
assume that
A10: o <> diff (b,a,o) and
A11: o <> diff (d,c,o) ; :: thesis: a,b // c,d
( o, diff (b,a,o) // o, diff (d,c,o) & o, diff (b,a,o) // a,b ) by A7, Th88;
then o, diff (d,c,o) // a,b by A10, Def1;
hence a,b // c,d by A11, A9, Def1; :: thesis: verum
end;
now :: thesis: ( ( o = diff (b,a,o) or o = diff (d,c,o) ) implies a,b // c,d )
assume ( o = diff (b,a,o) or o = diff (d,c,o) ) ; :: thesis: a,b // c,d
then ( a = b or c = d ) by Th87;
hence a,b // c,d by Def1, Th3; :: thesis: verum
end;
hence a,b // c,d by A8; :: thesis: verum
end;
hence ( o, diff (b,a,o), diff (d,c,o) are_collinear iff a,b // c,d ) by A1; :: thesis: verum