collsp.miz

    begin

    reserve X for set;

    definition

      let X;

      :: COLLSP:def1

      mode Relation3 of X -> set means

      : Def1: it c= [:X, X, X:];

      existence ;

    end

    theorem :: COLLSP:1



     Th1: X = {} or ex a be set st {a} = X or ex a,b be set st a <> b & a in X & b in X

    proof

      now

        set p = the Element of X;

        assume X <> {} & not ex a,b be set st a <> b & a in X & b in X;

        then for z be object holds z in X iff z = p;

        then X = {p} by TARSKI:def 1;

        hence ex a be set st {a} = X;

      end;

      hence thesis;

    end;

    definition

      struct ( 1-sorted) CollStr (# the carrier -> set,

the Collinearity -> Relation3 of the carrier #)

       attr strict strict;

    end

    registration

      cluster non empty strict for CollStr;

      existence

      proof

        set A = the non empty set, r = the Relation3 of A;

        take CollStr (# A, r #);

        thus the carrier of CollStr (# A, r #) is non empty;

        thus thesis;

      end;

    end

    reserve CS for non empty CollStr;

    reserve a,b,c for Point of CS;

    definition

      let CS, a, b, c;

      :: COLLSP:def2

      pred a,b,c are_collinear means [a, b, c] in the Collinearity of CS;

    end

    set Z = {1};



     Lm1: 1 in Z by TARSKI:def 1;



     Lm2: { [1, 1, 1]} c= [: {1}, {1}, {1}:]

    proof

      let x be object;

      assume x in { [1, 1, 1]};

      then x = [1, 1, 1] by TARSKI:def 1;

      hence x in [: {1}, {1}, {1}:] by Lm1, MCART_1: 69;

    end;

    reconsider Z as non empty set;

    reconsider RR = { [1, 1, 1]} as Relation3 of Z by Def1, Lm2;

    reconsider CLS = CollStr (# Z, RR #) as non empty CollStr;

     Lm3:

    now

      let a,b,c,p,q,r be Point of CLS;



       A1: for z1,z2,z3 be Point of CLS holds [z1, z2, z3] in the Collinearity of CLS

      proof

        let z1,z2,z3 be Point of CLS;



         A2: z3 = 1 by TARSKI:def 1;

        z1 = 1 & z2 = 1 by TARSKI:def 1;

        hence thesis by A2, TARSKI:def 1;

      end;

      hence a = b or a = c or b = c implies [a, b, c] in the Collinearity of CLS;

      thus a <> b & [a, b, p] in the Collinearity of CLS & [a, b, q] in the Collinearity of CLS & [a, b, r] in the Collinearity of CLS implies [p, q, r] in the Collinearity of CLS by A1;

    end;

    definition

      let IT be non empty CollStr;

      :: COLLSP:def3

      attr IT is reflexive means

      : Def3: for a,b,c be Point of IT st a = b or a = c or b = c holds [a, b, c] in the Collinearity of IT;

    end

    definition

      let IT be non empty CollStr;

      :: COLLSP:def4

      attr IT is transitive means

      : Def4: for a,b,p,q,r be Point of IT st a <> b & [a, b, p] in the Collinearity of IT & [a, b, q] in the Collinearity of IT & [a, b, r] in the Collinearity of IT holds [p, q, r] in the Collinearity of IT;

    end

    registration

      cluster strict reflexive transitive for non empty CollStr;

      existence

      proof

        take CLS;

        thus thesis by Lm3;

      end;

    end

    definition

      mode CollSp is reflexive transitive non empty CollStr;

    end

    reserve CLSP for CollSp;

    reserve a,b,c,d,p,q,r for Point of CLSP;

    theorem :: COLLSP:2



     Th2: (a = b or a = c or b = c) implies (a,b,c) are_collinear by Def3;

    theorem :: COLLSP:3



     Th3: a <> b & (a,b,p) are_collinear & (a,b,q) are_collinear & (a,b,r) are_collinear implies (p,q,r) are_collinear by Def4;

    theorem :: COLLSP:4



     Th4: (a,b,c) are_collinear implies (b,a,c) are_collinear & (a,c,b) are_collinear

    proof

      assume

       A1: (a,b,c) are_collinear ;

      then a = b or a <> b & (a,b,b) are_collinear & (a,b,a) are_collinear & (a,b,c) are_collinear by Th2;

      hence (b,a,c) are_collinear by Th2, Th3;

      a = b or a <> b & (a,b,a) are_collinear & (a,b,c) are_collinear & (a,b,b) are_collinear by A1, Th2;

      hence (a,c,b) are_collinear by Th2, Th3;

    end;

    theorem :: COLLSP:5

    (a,b,a) are_collinear by Th2;

    theorem :: COLLSP:6



     Th6: a <> b & (a,b,c) are_collinear & (a,b,d) are_collinear implies (a,c,d) are_collinear

    proof

      assume

       A1: a <> b & (a,b,c) are_collinear & (a,b,d) are_collinear ;

      (a,b,a) are_collinear by Th2;

      hence thesis by A1, Th3;

    end;

    theorem :: COLLSP:7

    (a,b,c) are_collinear implies (b,a,c) are_collinear by Th4;

    theorem :: COLLSP:8



     Th8: (a,b,c) are_collinear implies (b,c,a) are_collinear

    proof

      assume (a,b,c) are_collinear ;

      then (b,a,c) are_collinear by Th4;

      hence thesis by Th4;

    end;

    theorem :: COLLSP:9



     Th9: p <> q & (a,b,p) are_collinear & (a,b,q) are_collinear & (p,q,r) are_collinear implies (a,b,r) are_collinear

    proof

      assume that

       A1: p <> q and

       A2: (a,b,p) are_collinear & (a,b,q) are_collinear and

       A3: (p,q,r) are_collinear ;

      now

        assume

         A4: a <> b;

        then (a,p,q) are_collinear by A2, Th6;

        then

         A5: (p,q,a) are_collinear by Th8;

        (a,b,b) are_collinear by Th2;

        then (p,q,b) are_collinear by A2, A4, Th3;

        hence thesis by A1, A3, A5, Th3;

      end;

      hence thesis by Th2;

    end;

    definition

      let CLSP, a, b;

      :: COLLSP:def5

      func Line (a,b) -> set equals { p : (a,b,p) are_collinear };

      correctness ;

    end

    theorem :: COLLSP:10



     Th10: a in ( Line (a,b)) & b in ( Line (a,b))

    proof

      (a,b,a) are_collinear by Th2;

      hence a in ( Line (a,b));

      (a,b,b) are_collinear by Th2;

      hence b in ( Line (a,b));

    end;

    theorem :: COLLSP:11



     Th11: (a,b,r) are_collinear iff r in ( Line (a,b))

    proof

      thus (a,b,r) are_collinear implies r in ( Line (a,b));

      thus r in ( Line (a,b)) implies (a,b,r) are_collinear

      proof

        assume r in ( Line (a,b));

        then ex p st r = p & (a,b,p) are_collinear ;

        hence thesis;

      end;

    end;

    reserve i,j,k for Element of NAT ;

    set Z = {1, 2, 3};

    set RR = { [i, j, k] : (i = j or j = k or k = i) & i in Z & j in Z & k in Z };



     Lm4: RR c= [:Z, Z, Z:]

    proof

      let x be object;

      assume x in RR;

      then ex i, j, k st x = [i, j, k] & (i = j or j = k or k = i) & i in Z & j in Z & k in Z;

      hence x in [:Z, Z, Z:] by MCART_1: 69;

    end;

    reconsider Z as non empty set by ENUMSET1:def 1;

    reconsider RR as Relation3 of Z by Def1, Lm4;

    reconsider CLS = CollStr (# Z, RR #) as non empty CollStr;



     Lm5: for a,b,c be Point of CLS holds [a, b, c] in RR iff (a = b or b = c or c = a) & a in Z & b in Z & c in Z

    proof

      let a,b,c be Point of CLS;

      thus [a, b, c] in RR implies (a = b or b = c or c = a) & a in Z & b in Z & c in Z

      proof

        assume [a, b, c] in RR;

        then

        consider i, j, k such that

         A1: [a, b, c] = [i, j, k] and

         A2: i = j or j = k or k = i and i in Z and j in Z and k in Z;

        a = i & b = j by A1, XTUPLE_0: 3;

        hence thesis by A1, A2, XTUPLE_0: 3;

      end;

      thus thesis;

    end;



     Lm6: for a,b,c,p,q,r be Point of CLS holds (a <> b & [a, b, p] in the Collinearity of CLS & [a, b, q] in the Collinearity of CLS & [a, b, r] in the Collinearity of CLS implies [p, q, r] in the Collinearity of CLS)

    proof

      let a,b,c,p,q,r be Point of CLS;

      assume that

       A1: a <> b and

       A2: [a, b, p] in the Collinearity of CLS and

       A3: [a, b, q] in the Collinearity of CLS and

       A4: [a, b, r] in the Collinearity of CLS;



       A5: a = q or b = q by A1, A3, Lm5;



       A6: a = r or b = r by A1, A4, Lm5;



       A7: p in Z & q in Z;



       A8: r in Z;

      a = p or b = p by A1, A2, Lm5;

      hence [p, q, r] in the Collinearity of CLS by A5, A6, A7, A8;

    end;



     Lm7: ex a,b,c be Point of CLS st not (a,b,c) are_collinear

    proof

      reconsider a = 1, b = 2, c = 3 as Point of CLS by ENUMSET1:def 1;

      take a, b, c;

       not [a, b, c] in the Collinearity of CLS by Lm5;

      hence thesis;

    end;



     Lm8: CLS is CollSp

    proof

      for a,b,c,p,q,r be Point of CLS holds (a = b or a = c or b = c implies [a, b, c] in the Collinearity of CLS) & (a <> b & [a, b, p] in the Collinearity of CLS & [a, b, q] in the Collinearity of CLS & [a, b, r] in the Collinearity of CLS implies [p, q, r] in the Collinearity of CLS) by Lm5, Lm6;

      hence thesis by Def3, Def4;

    end;

    definition

      let IT be non empty CollStr;

      :: COLLSP:def6

      attr IT is proper means

      : Def6: ex a,b,c be Point of IT st not (a,b,c) are_collinear ;

    end

    registration

      cluster strict proper for CollSp;

      existence

      proof

        reconsider CLS as CollSp by Lm8;

        CLS is proper by Lm7;

        hence thesis;

      end;

    end

    reserve CLSP for proper CollSp;

    reserve a,b,c,p,q,r for Point of CLSP;

    theorem :: COLLSP:12



     Th12: for p, q holds p <> q implies ex r st not (p,q,r) are_collinear

    proof

      let p, q;

      consider a, b, c such that

       A1: not (a,b,c) are_collinear by Def6;

      assume p <> q;

      then not (p,q,a) are_collinear or not (p,q,b) are_collinear or not (p,q,c) are_collinear by A1, Th3;

      hence thesis;

    end;

    definition

      let CLSP;

      :: COLLSP:def7

      mode LINE of CLSP -> set means

      : Def7: ex a, b st a <> b & it = ( Line (a,b));

      existence

      proof

        consider a, b, c such that

         A1: not (a,b,c) are_collinear by Def6;

        take ( Line (a,b));

        a <> b by A1, Th2;

        hence thesis;

      end;

    end

    reserve P,Q for LINE of CLSP;

    theorem :: COLLSP:13

    a = b implies ( Line (a,b)) = the carrier of CLSP

    proof

      assume

       A1: a = b;

      for x be object holds x in ( Line (a,b)) iff x in the carrier of CLSP

      proof

        let x be object;

        thus x in ( Line (a,b)) implies x in the carrier of CLSP

        proof

          assume x in ( Line (a,b));

          then ex p st x = p & (a,b,p) are_collinear ;

          then

          reconsider x as Point of CLSP;

          x is Element of CLSP;

          hence thesis;

        end;

        thus x in the carrier of CLSP implies x in ( Line (a,b))

        proof

          assume x in the carrier of CLSP;

          then

          reconsider x as Point of CLSP;

          (a,b,x) are_collinear by A1, Th2;

          hence thesis;

        end;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: COLLSP:14

    for P holds ex a, b st a <> b & a in P & b in P

    proof

      let P;

      consider a, b such that

       A1: a <> b & P = ( Line (a,b)) by Def7;

      take a, b;

      thus thesis by A1, Th10;

    end;

    theorem :: COLLSP:15

    a <> b implies ex P st a in P & b in P

    proof

      assume a <> b;

      then

      reconsider P = ( Line (a,b)) as LINE of CLSP by Def7;

      take P;

      thus thesis by Th10;

    end;

    theorem :: COLLSP:16



     Th16: p in P & q in P & r in P implies (p,q,r) are_collinear

    proof

      assume that

       A1: p in P & q in P and

       A2: r in P;

      consider a, b such that

       A3: a <> b and

       A4: P = ( Line (a,b)) by Def7;



       A5: ex z be Point of CLSP st z = r & (a,b,z) are_collinear by A2, A4;

      (ex x be Point of CLSP st x = p & (a,b,x) are_collinear ) & ex y be Point of CLSP st y = q & (a,b,y) are_collinear by A1, A4;

      hence thesis by A3, A5, Th3;

    end;



     Lm9: for x be set holds x in P implies x is Point of CLSP

    proof

      let x be set;

      consider a, b such that a <> b and

       A1: P = ( Line (a,b)) by Def7;

      assume x in P;

      then ex r be Point of CLSP st r = x & (a,b,r) are_collinear by A1;

      hence thesis;

    end;

    theorem :: COLLSP:17



     Th17: P c= Q implies P = Q

    proof

      assume

       A1: P c= Q;

      Q c= P

      proof

        let r be object;

        consider p, q such that p <> q and

         A2: P = ( Line (p,q)) by Def7;

        assume

         A3: r in Q;

        then

        reconsider r as Point of CLSP by Lm9;

        p in P & q in P by A2, Th10;

        then (p,q,r) are_collinear by A1, A3, Th16;

        hence thesis by A2;

      end;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: COLLSP:18



     Th18: p <> q & p in P & q in P implies ( Line (p,q)) c= P

    proof

      assume that

       A1: p <> q and

       A2: p in P & q in P;

      let x be object;

      consider a, b such that a <> b and

       A3: P = ( Line (a,b)) by Def7;

      assume x in ( Line (p,q));

      then

      consider r be Point of CLSP such that

       A4: r = x and

       A5: (p,q,r) are_collinear ;

      (a,b,p) are_collinear & (a,b,q) are_collinear by A2, A3, Th11;

      then (a,b,r) are_collinear by A1, A5, Th9;

      hence thesis by A3, A4;

    end;

    theorem :: COLLSP:19



     Th19: p <> q & p in P & q in P implies ( Line (p,q)) = P

    proof

      assume that

       A1: p <> q and

       A2: p in P & q in P;

      reconsider Q = ( Line (p,q)) as LINE of CLSP by A1, Def7;

      Q c= P by A1, A2, Th18;

      hence thesis by Th17;

    end;

    theorem :: COLLSP:20



     Th20: p <> q & p in P & q in P & p in Q & q in Q implies P = Q

    proof

      assume that

       A1: p <> q and

       A2: p in P & q in P and

       A3: p in Q & q in Q;

      ( Line (p,q)) = P by A1, A2, Th19;

      hence thesis by A1, A3, Th19;

    end;

    theorem :: COLLSP:21

    P = Q or P misses Q or ex p st (P /\ Q) = {p}

    proof



       A1: (ex a be set st {a} = (P /\ Q)) implies ex p st (P /\ Q) = {p}

      proof

        given a be set such that

         A2: {a} = (P /\ Q);

        a in (P /\ Q) by A2, TARSKI:def 1;

        then a in P by XBOOLE_0:def 4;

        then

        reconsider p = a as Point of CLSP by Lm9;

        (P /\ Q) = {p} by A2;

        hence thesis;

      end;



       A3: (ex a,b be set st a <> b & a in (P /\ Q) & b in (P /\ Q)) implies P = Q

      proof

        given a,b be set such that

         A4: a <> b and

         A5: a in (P /\ Q) & b in (P /\ Q);

        a in P & b in P by A5, XBOOLE_0:def 4;

        then

        reconsider p = a, q = b as Point of CLSP by Lm9;



         A6: p in Q & q in Q by A5, XBOOLE_0:def 4;

        p in P & q in P by A5, XBOOLE_0:def 4;

        hence thesis by A4, A6, Th20;

      end;

      (P /\ Q) = {} or ex a be set st {a} = (P /\ Q) or ex a,b be set st a <> b & a in (P /\ Q) & b in (P /\ Q) by Th1;

      hence thesis by A1, A3, XBOOLE_0:def 7;

    end;

    theorem :: COLLSP:22

    a <> b implies ( Line (a,b)) <> the carrier of CLSP

    proof

      assume a <> b;

      then ex r st not (a,b,r) are_collinear by Th12;

      hence thesis by Th11;

    end;