let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, c, p, q, r, s being Element of FCPS st not a,b,c are_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar & a,b,c,s are_coplanar holds
p,q,r,s are_coplanar
let a, b, c, p, q, r, s be Element of FCPS; :: thesis: ( not a,b,c are_collinear & a,b,c,p are_coplanar & a,b,c,q are_coplanar & a,b,c,r are_coplanar & a,b,c,s are_coplanar implies p,q,r,s are_coplanar )
assume that
A1: not a,b,c are_collinear and
A2: a,b,c,p are_coplanar and
A3: a,b,c,q are_coplanar and
A4: a,b,c,r are_coplanar and
A5: a,b,c,s are_coplanar ; :: thesis: p,q,r,s are_coplanar
A6: a,b,p,q are_coplanar by A1, A2, A3, Lm4;
A7: a,b,q,r are_coplanar by A1, A3, A4, Lm4;
A8: a,b,p,r are_coplanar by A1, A2, A4, Lm4;
A9: a,b,q,s are_coplanar by A1, A3, A5, Lm4;
A10: now :: thesis: ( not a,b,q are_collinear implies p,q,r,s are_coplanar )
A11: q,a,b,r are_coplanar by A7, Th7;
assume A12: not a,b,q are_collinear ; :: thesis: p,q,r,s are_coplanar
then A13: not q,a,b are_collinear by Th1;
A14: q,a,b,p are_coplanar by A6, Th7;
then A15: q,a,p,r are_coplanar by A13, A11, Lm4;
A16: q,a,b,s are_coplanar by A9, Th7;
then A17: q,a,p,s are_coplanar by A13, A14, Lm4;
A18: now :: thesis: ( not q,a,p are_collinear implies p,q,r,s are_coplanar )
assume not q,a,p are_collinear ; :: thesis: p,q,r,s are_coplanar
then A19: not q,p,a are_collinear by Th1;
( q,p,a,r are_coplanar & q,p,a,s are_coplanar ) by A15, A17, Th7;
then q,p,r,s are_coplanar by A19, Lm4;
hence p,q,r,s are_coplanar by Th7; :: thesis: verum
end;
A20: q,a,r,s are_coplanar by A13, A11, A16, Lm4;
A21: now :: thesis: ( not q,a,r are_collinear implies p,q,r,s are_coplanar )
assume not q,a,r are_collinear ; :: thesis: p,q,r,s are_coplanar
then A22: not q,r,a are_collinear by Th1;
( q,r,a,p are_coplanar & q,r,a,s are_coplanar ) by A15, A20, Th7;
then q,r,p,s are_coplanar by A22, Lm4;
hence p,q,r,s are_coplanar by Th7; :: thesis: verum
end;
A23: q <> a by A12, ANPROJ_2:def 7;
now :: thesis: ( q,a,p are_collinear & q,a,r are_collinear implies p,q,r,s are_coplanar )
assume ( q,a,p are_collinear & q,a,r are_collinear ) ; :: thesis: p,q,r,s are_coplanar
then q,p,r are_collinear by A23, COLLSP:6;
then p,q,r are_collinear by Th1;
hence p,q,r,s are_coplanar by Th6; :: thesis: verum
end;
hence p,q,r,s are_coplanar by A18, A21; :: thesis: verum
end;
A24: a,b,r,s are_coplanar by A1, A4, A5, Lm4;
A25: now :: thesis: ( not a,b,r are_collinear implies p,q,r,s are_coplanar )
A26: r,a,b,q are_coplanar by A7, Th7;
assume A27: not a,b,r are_collinear ; :: thesis: p,q,r,s are_coplanar
then A28: not r,a,b are_collinear by Th1;
A29: r,a,b,p are_coplanar by A8, Th7;
then A30: r,a,p,q are_coplanar by A28, A26, Lm4;
A31: r,a,b,s are_coplanar by A24, Th7;
then A32: r,a,p,s are_coplanar by A28, A29, Lm4;
A33: now :: thesis: ( not r,a,p are_collinear implies p,q,r,s are_coplanar )
assume not r,a,p are_collinear ; :: thesis: p,q,r,s are_coplanar
then A34: not r,p,a are_collinear by Th1;
( r,p,a,q are_coplanar & r,p,a,s are_coplanar ) by A30, A32, Th7;
then r,p,q,s are_coplanar by A34, Lm4;
hence p,q,r,s are_coplanar by Th7; :: thesis: verum
end;
A35: r,a,q,s are_coplanar by A28, A26, A31, Lm4;
A36: now :: thesis: ( not r,a,q are_collinear implies p,q,r,s are_coplanar )
assume not r,a,q are_collinear ; :: thesis: p,q,r,s are_coplanar
then A37: not r,q,a are_collinear by Th1;
( r,q,a,p are_coplanar & r,q,a,s are_coplanar ) by A30, A35, Th7;
then r,q,p,s are_coplanar by A37, Lm4;
hence p,q,r,s are_coplanar by Th7; :: thesis: verum
end;
A38: r <> a by A27, ANPROJ_2:def 7;
now :: thesis: ( r,a,p are_collinear & r,a,q are_collinear implies p,q,r,s are_coplanar )
assume ( r,a,p are_collinear & r,a,q are_collinear ) ; :: thesis: p,q,r,s are_coplanar
then r,p,q are_collinear by A38, COLLSP:6;
then p,q,r are_collinear by Th1;
hence p,q,r,s are_coplanar by Th6; :: thesis: verum
end;
hence p,q,r,s are_coplanar by A33, A36; :: thesis: verum
end;
A39: a,b,p,s are_coplanar by A1, A2, A5, Lm4;
A40: now :: thesis: ( not a,b,p are_collinear implies p,q,r,s are_coplanar )
A41: p,a,b,r are_coplanar by A8, Th7;
assume A42: not a,b,p are_collinear ; :: thesis: p,q,r,s are_coplanar
then A43: not p,a,b are_collinear by Th1;
A44: p,a,b,q are_coplanar by A6, Th7;
then A45: p,a,q,r are_coplanar by A43, A41, Lm4;
A46: p,a,b,s are_coplanar by A39, Th7;
then A47: p,a,q,s are_coplanar by A43, A44, Lm4;
A48: now :: thesis: ( not p,a,q are_collinear implies p,q,r,s are_coplanar )
assume not p,a,q are_collinear ; :: thesis: p,q,r,s are_coplanar
then A49: not p,q,a are_collinear by Th1;
( p,q,a,r are_coplanar & p,q,a,s are_coplanar ) by A45, A47, Th7;
hence p,q,r,s are_coplanar by A49, Lm4; :: thesis: verum
end;
A50: p,a,r,s are_coplanar by A43, A41, A46, Lm4;
A51: now :: thesis: ( not p,a,r are_collinear implies p,q,r,s are_coplanar )
assume not p,a,r are_collinear ; :: thesis: p,q,r,s are_coplanar
then A52: not p,r,a are_collinear by Th1;
( p,r,a,q are_coplanar & p,r,a,s are_coplanar ) by A45, A50, Th7;
then p,r,q,s are_coplanar by A52, Lm4;
hence p,q,r,s are_coplanar by Th7; :: thesis: verum
end;
A53: p <> a by A42, ANPROJ_2:def 7;
now :: thesis: ( p,a,q are_collinear & p,a,r are_collinear implies p,q,r,s are_coplanar )
assume ( p,a,q are_collinear & p,a,r are_collinear ) ; :: thesis: p,q,r,s are_coplanar
then p,q,r are_collinear by A53, COLLSP:6;
hence p,q,r,s are_coplanar by Th6; :: thesis: verum
end;
hence p,q,r,s are_coplanar by A48, A51; :: thesis: verum
end;
A54: a <> b by A1, ANPROJ_2:def 7;
now :: thesis: ( a,b,p are_collinear & a,b,q are_collinear & a,b,r are_collinear implies p,q,r,s are_coplanar )
assume ( a,b,p are_collinear & a,b,q are_collinear & a,b,r are_collinear ) ; :: thesis: p,q,r,s are_coplanar
then p,q,r are_collinear by A54, ANPROJ_2:def 8;
hence p,q,r,s are_coplanar by Th6; :: thesis: verum
end;
hence p,q,r,s are_coplanar by A40, A10, A25; :: thesis: verum