pardepap.miz



    begin

    reserve SAS for AffinPlane;

    theorem :: PARDEPAP:1

    

     Th1: SAS is Pappian implies for a1,a2,a3,b1,b2,b3 be Element of SAS holds ((a1,a2) // (a1,a3) & (b1,b2) // (b1,b3) & (a1,b2) // (a2,b1) & (a2,b3) // (a3,b2) implies (a3,b1) // (a1,b3))

    proof

      assume

       A1: SAS is Pappian;

      let a1,a2,a3,b1,b2,b3 be Element of SAS such that

       A2: (a1,a2) // (a1,a3) and

       A3: (b1,b2) // (b1,b3) and

       A4: (a1,b2) // (a2,b1) and

       A5: (a2,b3) // (a3,b2);

       LIN (a1,a2,a3) by A2, AFF_1:def 1;

      then

      consider M be Subset of SAS such that

       A6: M is being_line and

       A7: a1 in M and

       A8: a2 in M and

       A9: a3 in M by AFF_1: 21;

       LIN (b1,b2,b3) by A3, AFF_1:def 1;

      then

      consider N be Subset of SAS such that

       A10: N is being_line and

       A11: b1 in N and

       A12: b2 in N and

       A13: b3 in N by AFF_1: 21;

       A14:

      now

        assume that

         A15: M <> N and

         A16: not M // N;

        consider o be Element of SAS such that

         A17: o in M and

         A18: o in N by A6, A10, A16, AFF_1: 58;

         A19:

        now

          assume that

           A20: o <> a1 and

           A21: b1 <> o and

           A22: o = b3;

           A23:

          now

            assume a2 <> o;

            then b2 in M by A5, A6, A8, A9, A17, A22, AFF_1: 48;

            then b2 = o by A6, A10, A12, A15, A17, A18, AFF_1: 18;

            then b1 in M by A4, A6, A7, A8, A17, A20, AFF_1: 48;

            hence thesis by A6, A7, A9, A17, A22, AFF_1: 51;

          end;

          now

            assume a2 = o;

            then (o,b1) // (b2,a1) by A4, AFF_1: 4;

            then a1 in N by A10, A11, A12, A13, A21, A22, AFF_1: 48;

            hence thesis by A6, A7, A10, A15, A17, A18, A20, AFF_1: 18;

          end;

          hence thesis by A23;

        end;

         A24:

        now

          assume that o <> a1 and

           A25: b1 = o;

          

           A26: (o,a2) // (a1,b2) by A4, A25, AFF_1: 4;

           A27:

          now

            assume a2 <> o;

            then b2 in M by A6, A7, A8, A17, A26, AFF_1: 48;

            then b2 = o by A6, A10, A12, A15, A17, A18, AFF_1: 18;

            then

             A28: (o,a3) // (a2,b3) by A5, AFF_1: 4;

            now

              assume o <> a3;

              then b3 in M by A6, A8, A9, A17, A28, AFF_1: 48;

              hence thesis by A6, A7, A9, A17, A25, AFF_1: 51;

            end;

            hence thesis by A25, AFF_1: 3;

          end;

          now

            assume

             A29: a2 = o;

            now

              assume

               A30: b3 <> o;

              (o,b3) // (b2,a3) by A5, A29, AFF_1: 4;

              then a3 in N by A10, A12, A13, A18, A30, AFF_1: 48;

              then b1 = a3 by A6, A9, A10, A15, A17, A18, A25, AFF_1: 18;

              hence thesis by AFF_1: 3;

            end;

            hence thesis by A6, A7, A9, A17, A25, AFF_1: 51;

          end;

          hence thesis by A27;

        end;

         A31:

        now

          assume

           A32: o = a1;

          then

           A33: (o,b2) // (b1,a2) by A4, AFF_1: 4;

           A34:

          now

            assume b2 <> o;

            then a2 in N by A10, A11, A12, A18, A33, AFF_1: 48;

            then a2 = o by A6, A8, A10, A15, A17, A18, AFF_1: 18;

            then

             A35: (o,b3) // (b2,a3) by A5, AFF_1: 4;

            now

              assume o <> b3;

              then a3 in N by A10, A12, A13, A18, A35, AFF_1: 48;

              hence thesis by A10, A11, A13, A18, A32, AFF_1: 51;

            end;

            hence thesis by A32, AFF_1: 3;

          end;

          now

            assume

             A36: b2 = o;

            now

              assume

               A37: a3 <> o;

              (o,a3) // (a2,b3) by A5, A36, AFF_1: 4;

              then b3 in M by A6, A8, A9, A17, A37, AFF_1: 48;

              then a1 = b3 by A6, A10, A13, A15, A17, A18, A32, AFF_1: 18;

              hence thesis by AFF_1: 3;

            end;

            hence thesis by A10, A11, A13, A18, A32, AFF_1: 51;

          end;

          hence thesis by A34;

        end;

         A38:

        now

          assume that

           A39: o <> a1 and

           A40: b1 <> o and o <> b3 and

           A41: o = a3;

          

           A42: (o,b2) // (b3,a2) by A5, A41, AFF_1: 4;

           A43:

          now

            assume b2 <> o;

            then a2 in N by A10, A12, A13, A18, A42, AFF_1: 48;

            then a2 = o by A6, A8, A10, A15, A17, A18, AFF_1: 18;

            then (o,b1) // (b2,a1) by A4, AFF_1: 4;

            then a1 in N by A10, A11, A12, A18, A40, AFF_1: 48;

            hence thesis by A10, A11, A13, A18, A41, AFF_1: 51;

          end;

          now

            assume b2 = o;

            then b1 in M by A4, A6, A7, A8, A9, A39, A41, AFF_1: 48;

            hence thesis by A6, A10, A11, A15, A17, A18, A40, AFF_1: 18;

          end;

          hence thesis by A43;

        end;

        now

          assume that

           A44: o <> a1 & o <> b1 and

           A45: o <> b3 and

           A46: o <> a3;

          

           A47: o <> b2

          proof

            assume o = b2;

            then (o,a3) // (a2,b3) by A5, AFF_1: 4;

            then b3 in M by A6, A8, A9, A17, A46, AFF_1: 48;

            hence contradiction by A6, A10, A13, A15, A17, A18, A45, AFF_1: 18;

          end;

          o <> a2

          proof

            assume o = a2;

            then (o,b3) // (b2,a3) by A5, AFF_1: 4;

            then a3 in N by A10, A12, A13, A18, A45, AFF_1: 48;

            hence contradiction by A6, A9, A10, A15, A17, A18, A46, AFF_1: 18;

          end;

          then (a1,b3) // (a3,b1) by A1, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A15, A17, A18, A44, A45, A46, A47, AFF_2:def 2;

          hence thesis by AFF_1: 4;

        end;

        hence thesis by A31, A24, A19, A38;

      end;

      

       A48: SAS is satisfying_pap by A1, AFF_2: 9;

      now

        assume M <> N & M // N;

        then (a1,b3) // (a3,b1) by A48, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, AFF_2:def 13;

        hence thesis by AFF_1: 4;

      end;

      hence thesis by A6, A7, A9, A11, A13, A14, AFF_1: 51;

    end;

    theorem :: PARDEPAP:2

    

     Th2: SAS is Desarguesian implies for o,a,a9,b,b9,c,c9 be Element of SAS holds ( not (o,a) // (o,b) & not (o,a) // (o,c) & (o,a) // (o,a9) & (o,b) // (o,b9) & (o,c) // (o,c9) & (a,b) // (a9,b9) & (a,c) // (a9,c9) implies (b,c) // (b9,c9))

    proof

      assume

       A1: SAS is Desarguesian;

      let o,a,a9,b,b9,c,c9 be Element of SAS such that

       A2: not (o,a) // (o,b) and

       A3: not (o,a) // (o,c) and

       A4: (o,a) // (o,a9) and

       A5: (o,b) // (o,b9) and

       A6: (o,c) // (o,c9) and

       A7: (a,b) // (a9,b9) & (a,c) // (a9,c9);

      

       A8: o <> a & o <> b by A2, AFF_1: 3;

      

       A9: o <> c by A3, AFF_1: 3;

       LIN (o,b,b9) by A5, AFF_1:def 1;

      then

      consider P be Subset of SAS such that

       A10: P is being_line & o in P and

       A11: b in P and

       A12: b9 in P by AFF_1: 21;

       LIN (o,a,a9) by A4, AFF_1:def 1;

      then

      consider A be Subset of SAS such that

       A13: A is being_line & o in A & a in A and

       A14: a9 in A by AFF_1: 21;

       LIN (o,c,c9) by A6, AFF_1:def 1;

      then

      consider C be Subset of SAS such that

       A15: C is being_line & o in C and

       A16: c in C and

       A17: c9 in C by AFF_1: 21;

      

       A18: A <> C by A3, A13, A16, AFF_1: 51;

      A <> P by A2, A13, A11, AFF_1: 51;

      hence thesis by A1, A7, A13, A14, A10, A11, A12, A15, A16, A17, A8, A9, A18, AFF_2:def 4;

    end;

    theorem :: PARDEPAP:3

    

     Th3: SAS is translational implies for a,a9,b,b9,c,c9 be Element of SAS holds ( not (a,a9) // (a,b) & not (a,a9) // (a,c) & (a,a9) // (b,b9) & (a,a9) // (c,c9) & (a,b) // (a9,b9) & (a,c) // (a9,c9) implies (b,c) // (b9,c9))

    proof

      assume

       A1: SAS is translational;

      let a,a9,b,b9,c,c9 be Element of SAS such that

       A2: not (a,a9) // (a,b) and

       A3: not (a,a9) // (a,c) and

       A4: (a,a9) // (b,b9) and

       A5: (a,a9) // (c,c9) and

       A6: (a,b) // (a9,b9) & (a,c) // (a9,c9);

      set A = ( Line (a,a9));

      

       A7: a <> a9 by A2, AFF_1: 3;

      then

       A8: A is being_line by AFF_1:def 3;

      then

      consider C be Subset of SAS such that

       A9: c in C and

       A10: A // C by AFF_1: 49;

      

       A11: C is being_line by A10, AFF_1: 36;

      

       A12: a in A & a9 in A by AFF_1: 15;

      then

       A13: A <> C by A3, A8, A9, AFF_1: 51;

      

       A14: (a,a9) // A by A8, A12, AFF_1: 23;

      then (a,a9) // C by A10, AFF_1: 43;

      then (c,c9) // C by A5, A7, AFF_1: 32;

      then

       A15: c9 in C by A9, A11, AFF_1: 23;

      consider P be Subset of SAS such that

       A16: b in P and

       A17: A // P by A8, AFF_1: 49;

      

       A18: P is being_line by A17, AFF_1: 36;

      (a,a9) // P by A14, A17, AFF_1: 43;

      then (b,b9) // P by A4, A7, AFF_1: 32;

      then

       A19: b9 in P by A16, A18, AFF_1: 23;

      A <> P by A2, A8, A12, A16, AFF_1: 51;

      hence thesis by A1, A6, A8, A12, A16, A17, A9, A10, A18, A11, A19, A15, A13, AFF_2:def 11;

    end;

    theorem :: PARDEPAP:4

    ex SAS st (for o,a,a9,b,b9,c,c9 be Element of SAS holds ( not (o,a) // (o,b) & not (o,a) // (o,c) & (o,a) // (o,a9) & (o,b) // (o,b9) & (o,c) // (o,c9) & (a,b) // (a9,b9) & (a,c) // (a9,c9) implies (b,c) // (b9,c9))) & (for a,a9,b,b9,c,c9 be Element of SAS holds ( not (a,a9) // (a,b) & not (a,a9) // (a,c) & (a,a9) // (b,b9) & (a,a9) // (c,c9) & (a,b) // (a9,b9) & (a,c) // (a9,c9) implies (b,c) // (b9,c9))) & (for a1,a2,a3,b1,b2,b3 be Element of SAS holds ((a1,a2) // (a1,a3) & (b1,b2) // (b1,b3) & (a1,b2) // (a2,b1) & (a2,b3) // (a3,b2) implies (a3,b1) // (a1,b3))) & for a,b,c,d be Element of SAS holds ( not (a,b) // (a,c) & (a,b) // (c,d) & (a,c) // (b,d) implies not (a,d) // (b,c))

    proof

      set PAS = the Fanoian Pappian Desarguesian translational AffinPlane;

      reconsider SAS = PAS as AffinPlane;

      take SAS;

      thus thesis by Th1, Th2, Th3, PAPDESAF:def 1;

    end;

    theorem :: PARDEPAP:5

    for o,a be Element of SAS holds ex p be Element of SAS st for b,c be Element of SAS holds ((o,a) // (o,p) & ex d be Element of SAS st ((o,p) // (o,b) implies (o,c) // (o,d) & (p,c) // (b,d)))

    proof

      let o,a be Element of SAS;

      ex p be Element of SAS st o <> p & (o,a) // (o,p)

      proof

        consider x,y be Element of SAS such that

         A1: x <> y by DIRAF: 40;

        now

          assume a = o;

          then

           A2: (o,a) // (o,x) & (o,a) // (o,y) by AFF_1: 3;

          o <> x or o <> y by A1;

          hence thesis by A2;

        end;

        hence thesis by AFF_1: 2;

      end;

      then

      consider p be Element of SAS such that

       A3: o <> p and

       A4: (o,a) // (o,p);

      take p;

      thus for b,c be Element of SAS holds ((o,a) // (o,p) & ex d be Element of SAS st ((o,p) // (o,b) implies (o,c) // (o,d) & (p,c) // (b,d)))

      proof

        let b,c be Element of SAS;

        ex d be Element of SAS st ((o,p) // (o,b) implies (o,c) // (o,d) & (p,c) // (b,d))

        proof

          now

            assume (o,p) // (o,b);

            then (p,o) // (o,b) by AFF_1: 4;

            then

            consider d be Element of SAS such that

             A5: (c,o) // (o,d) & (c,p) // (b,d) by A3, DIRAF: 40;

            (o,c) // (o,d) & (p,c) // (b,d) by A5, AFF_1: 4;

            hence thesis;

          end;

          hence thesis;

        end;

        hence thesis by A4;

      end;

    end;