euclmetr.miz



    begin

    definition

      let IT be OrtAfSp;

      :: EUCLMETR:def1

      attr IT is Euclidean means for a,b,c,d be Element of IT st (a,b) _|_ (c,d) & (b,c) _|_ (a,d) holds (b,d) _|_ (a,c);

    end

    definition

      let IT be OrtAfSp;

      :: EUCLMETR:def2

      attr IT is Pappian means

      : Def2: the AffinStruct of IT is Pappian;

    end

    definition

      let IT be OrtAfSp;

      :: EUCLMETR:def3

      attr IT is Desarguesian means

      : Def3: the AffinStruct of IT is Desarguesian;

    end

    definition

      let IT be OrtAfSp;

      :: EUCLMETR:def4

      attr IT is Fanoian means

      : Def4: the AffinStruct of IT is Fanoian;

    end

    definition

      let IT be OrtAfSp;

      :: EUCLMETR:def5

      attr IT is Moufangian means

      : Def5: the AffinStruct of IT is Moufangian;

    end

    definition

      let IT be OrtAfSp;

      :: EUCLMETR:def6

      attr IT is translation means

      : Def6: the AffinStruct of IT is translational;

    end

    definition

      let IT be OrtAfSp;

      :: EUCLMETR:def7

      attr IT is Homogeneous means for o,a,a1,b,b1,c,c1 be Element of IT st (o,a) _|_ (o,a1) & (o,b) _|_ (o,b1) & (o,c) _|_ (o,c1) & (a,b) _|_ (a1,b1) & (a,c) _|_ (a1,c1) & not (o,c) // (o,a) & not (o,a) // (o,b) holds (b,c) _|_ (b1,c1);

    end

    reserve MS for OrtAfPl;

    reserve MP for OrtAfSp;

    theorem :: EUCLMETR:1

    

     Th1: for a,b,c be Element of MP st not LIN (a,b,c) holds a <> b & b <> c & a <> c

    proof

      let a,b,c be Element of MP such that

       A1: not LIN (a,b,c);

      reconsider b9 = b, a9 = a, c9 = c as Element of the AffinStruct of MP;

      assume not thesis;

      then LIN (a9,b9,c9) by AFF_1: 7;

      hence contradiction by A1, ANALMETR: 40;

    end;

    theorem :: EUCLMETR:2

    

     Th2: for a,b,c,d be Element of MS, K be Subset of the carrier of MS st (a,b) _|_ K & (c,d) _|_ K holds (a,b) // (c,d) & (a,b) // (d,c)

    proof

      let a,b,c,d be Element of MS, K be Subset of MS such that

       A1: (a,b) _|_ K and

       A2: (c,d) _|_ K;

      reconsider K9 = K as Subset of the AffinStruct of MS;

      K is being_line by A1, ANALMETR: 44;

      then K9 is being_line by ANALMETR: 43;

      then

      consider p9,q9 be Element of the AffinStruct of MS such that

       A3: p9 in K9 & q9 in K9 and

       A4: p9 <> q9 by AFF_1: 19;

      reconsider p = p9, q = q9 as Element of MS;

      (a,b) _|_ (p,q) & (c,d) _|_ (p,q) by A1, A2, A3, ANALMETR: 53;

      hence (a,b) // (c,d) by A4, ANALMETR: 63;

      hence thesis by ANALMETR: 59;

    end;

    theorem :: EUCLMETR:3

    for a,b be Element of MS, A,K be Subset of the carrier of MS st a <> b & ((a,b) _|_ K or (b,a) _|_ K) & (a,b) _|_ A holds K // A

    proof

      let a,b be Element of MS, A,K be Subset of MS such that

       A1: a <> b and

       A2: (a,b) _|_ K or (b,a) _|_ K and

       A3: (a,b) _|_ A;

      (a,b) _|_ K by A2, ANALMETR: 49;

      then

      consider p,q be Element of MS such that

       A4: p <> q & K = ( Line (p,q)) and

       A5: (a,b) _|_ (p,q) by ANALMETR:def 13;

      consider r,s be Element of MS such that

       A6: r <> s & A = ( Line (r,s)) and

       A7: (a,b) _|_ (r,s) by A3, ANALMETR:def 13;

      (p,q) // (r,s) by A1, A5, A7, ANALMETR: 63;

      hence thesis by A4, A6, ANALMETR:def 15;

    end;

    theorem :: EUCLMETR:4

    

     Th4: for x,y,z be Element of MP st LIN (x,y,z) holds LIN (x,z,y) & LIN (y,x,z) & LIN (y,z,x) & LIN (z,x,y) & LIN (z,y,x)

    proof

      let x,y,z be Element of MP such that

       A1: LIN (x,y,z);

      reconsider x9 = x, y9 = y, z9 = z as Element of the AffinStruct of MP;

      

       A2: LIN (x9,y9,z9) by A1, ANALMETR: 40;

      then

       A3: LIN (y9,z9,x9) & LIN (z9,x9,y9) by AFF_1: 6;

      

       A4: LIN (z9,y9,x9) by A2, AFF_1: 6;

       LIN (x9,z9,y9) & LIN (y9,x9,z9) by A2, AFF_1: 6;

      hence thesis by A3, A4, ANALMETR: 40;

    end;

    theorem :: EUCLMETR:5

    

     Th5: for a,b,c be Element of MS st not LIN (a,b,c) holds ex d be Element of MS st (d,a) _|_ (b,c) & (d,b) _|_ (a,c)

    proof

      let a,b,c be Element of MS;

      set A = ( Line (a,c)), K = ( Line (b,c));

      reconsider A9 = A, K9 = K as Subset of the AffinStruct of MS;

      reconsider a9 = a, b9 = b, c9 = c as Element of the AffinStruct of MS;

      K9 = ( Line (b9,c9)) by ANALMETR: 41;

      then

       A1: b9 in K9 & c9 in K9 by AFF_1: 15;

      assume

       A2: not LIN (a,b,c);

      then a <> c by Th1;

      then A is being_line by ANALMETR:def 12;

      then

      consider P be Subset of MS such that

       A3: b in P and

       A4: A _|_ P by CONMETR: 3;

      b <> c by A2, Th1;

      then K is being_line by ANALMETR:def 12;

      then

      consider Q be Subset of MS such that

       A5: a in Q and

       A6: K _|_ Q by CONMETR: 3;

      reconsider P9 = P, Q9 = Q as Subset of the AffinStruct of MS;

      Q is being_line by A6, ANALMETR: 44;

      then

       A7: Q9 is being_line by ANALMETR: 43;

      

       A8: A9 = ( Line (a9,c9)) by ANALMETR: 41;

      then

       A9: c9 in A9 by AFF_1: 15;

      

       A10: not P9 // Q9

      proof

        assume not thesis;

        then P // Q by ANALMETR: 46;

        then A _|_ Q by A4, ANALMETR: 52;

        then A // K by A6, ANALMETR: 65;

        then A9 // K9 by ANALMETR: 46;

        then b9 in A9 by A9, A1, AFF_1: 45;

        then LIN (a9,c9,b9) by A8, AFF_1:def 2;

        then LIN (a9,b9,c9) by AFF_1: 6;

        hence contradiction by A2, ANALMETR: 40;

      end;

      P is being_line by A4, ANALMETR: 44;

      then P9 is being_line by ANALMETR: 43;

      then

      consider d9 be Element of the AffinStruct of MS such that

       A11: d9 in P9 & d9 in Q9 by A7, A10, AFF_1: 58;

      reconsider d = d9 as Element of MS;

      take d;

      a9 in A9 by A8, AFF_1: 15;

      hence thesis by A3, A4, A5, A6, A9, A1, A11, ANALMETR: 56;

    end;

    theorem :: EUCLMETR:6

    

     Th6: for a,b,c,d1,d2 be Element of MS st not LIN (a,b,c) & (d1,a) _|_ (b,c) & (d1,b) _|_ (a,c) & (d2,a) _|_ (b,c) & (d2,b) _|_ (a,c) holds d1 = d2

    proof

      let a,b,c,d1,d2 be Element of MS such that

       A1: not LIN (a,b,c) and

       A2: (d1,a) _|_ (b,c) and

       A3: (d1,b) _|_ (a,c) and

       A4: (d2,a) _|_ (b,c) and

       A5: (d2,b) _|_ (a,c);

      reconsider a9 = a, b9 = b, c9 = c, d19 = d1, d29 = d2 as Element of the AffinStruct of MS;

      assume

       A6: d1 <> d2;

      b <> c by A1, Th1;

      then (d1,a) // (d2,a) by A2, A4, ANALMETR: 63;

      then (d19,a9) // (d29,a9) by ANALMETR: 36;

      then (a9,d19) // (a9,d29) by AFF_1: 4;

      then LIN (a9,d19,d29) by AFF_1:def 1;

      then

       A7: LIN (d19,d29,a9) by AFF_1: 6;

      a <> c by A1, Th1;

      then (d1,b) // (d2,b) by A3, A5, ANALMETR: 63;

      then (d19,b9) // (d29,b9) by ANALMETR: 36;

      then (b9,d19) // (b9,d29) by AFF_1: 4;

      then LIN (b9,d19,d29) by AFF_1:def 1;

      then

       A8: LIN (d19,d29,b9) by AFF_1: 6;

      set X9 = ( Line (a9,b9));

      reconsider X = X9 as Subset of MS;

      

       A9: b <> a by A1, Th1;

      then

       A10: X9 is being_line by AFF_1:def 3;

      then

       A11: X is being_line by ANALMETR: 43;

      

       A12: a9 in X9 by AFF_1: 15;

      

       A13: b9 in X9 by AFF_1: 15;

       LIN (d19,d29,d29) by AFF_1: 7;

      then

       A14: d2 in X by A6, A9, A7, A8, A10, A12, A13, AFF_1: 8, AFF_1: 25;

       LIN (d19,d29,d19) by AFF_1: 7;

      then

       A15: d1 in X by A6, A9, A7, A8, A10, A12, A13, AFF_1: 8, AFF_1: 25;

      a <> d1 or a <> d2 by A6;

      then

       A16: (b,c) _|_ X by A2, A4, A12, A15, A14, A11, ANALMETR: 55;

      b <> d1 or b <> d2 by A6;

      then (a,c) _|_ X by A3, A5, A13, A15, A14, A11, ANALMETR: 55;

      then (a,c) // (b,c) by A16, Th2;

      then (a9,c9) // (b9,c9) by ANALMETR: 36;

      then (c9,b9) // (c9,a9) by AFF_1: 4;

      then LIN (c9,b9,a9) by AFF_1:def 1;

      then LIN (a9,b9,c9) by AFF_1: 6;

      hence contradiction by A1, ANALMETR: 40;

    end;

    theorem :: EUCLMETR:7

    

     Th7: for a,b,c,d be Element of MS st (a,b) _|_ (c,d) & (b,c) _|_ (a,d) & LIN (a,b,c) holds (a = c or a = b or b = c)

    proof

      let a,b,c,d be Element of MS such that

       A1: (a,b) _|_ (c,d) and

       A2: (b,c) _|_ (a,d) and

       A3: LIN (a,b,c);

      assume

       A4: not thesis;

       LIN (c,b,a) by A3, Th4;

      then (c,b) // (c,a) by ANALMETR:def 10;

      then (a,c) // (b,c) by ANALMETR: 59;

      then

       A5: (a,c) _|_ (a,d) by A2, A4, ANALMETR: 62;

      reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of the AffinStruct of MS;

       LIN (a9,b9,c9) by A3, ANALMETR: 40;

      then

      consider A9 be Subset of the AffinStruct of MS such that

       A6: A9 is being_line and

       A7: a9 in A9 and

       A8: b9 in A9 and

       A9: c9 in A9 by AFF_1: 21;

      reconsider A = A9 as Subset of MS;

      

       A10: A is being_line by A6, ANALMETR: 43;

      then

       A11: (c,d) _|_ A by A1, A4, A7, A8, ANALMETR: 55;

      (a,b) // (a,c) by A3, ANALMETR:def 10;

      then (a,c) _|_ (c,d) by A1, A4, ANALMETR: 62;

      then (c,d) // (a,d) by A4, A5, ANALMETR: 63;

      then (d,c) // (d,a) by ANALMETR: 59;

      then LIN (d,c,a) by ANALMETR:def 10;

      then LIN (a,c,d) by Th4;

      then LIN (a9,c9,d9) by ANALMETR: 40;

      then d in A by A4, A6, A7, A9, AFF_1: 25;

      then

       A12: c = d by A9, A11, ANALMETR: 51;

      (a,d) _|_ A by A2, A4, A8, A9, A10, ANALMETR: 55;

      hence contradiction by A4, A7, A9, A12, ANALMETR: 51;

    end;

    theorem :: EUCLMETR:8

    

     Th8: MS is Euclidean iff MS is satisfying_3H

    proof

       A1:

      now

        assume

         A2: MS is satisfying_3H;

        now

          let a,b,c,d be Element of MS such that

           A3: (a,b) _|_ (c,d) and

           A4: (b,c) _|_ (a,d);

           A5:

          now

            

             A6: (d,a) _|_ (c,b) & (d,c) _|_ (a,b) by A3, A4, ANALMETR: 61;

            assume

             A7: not LIN (a,b,c);

            then

            consider d1 be Element of MS such that

             A8: (d1,a) _|_ (b,c) and

             A9: (d1,b) _|_ (a,c) & (d1,c) _|_ (a,b) by A2, CONAFFM:def 3;

            

             A10: not LIN (a,c,b) by A7, Th4;

            (d1,a) _|_ (c,b) by A8, ANALMETR: 61;

            then (d,b) _|_ (a,c) by A9, A6, A10, Th6;

            hence (b,d) _|_ (a,c) by ANALMETR: 61;

          end;

          now

            

             A11: a = c implies (b,d) _|_ (a,c) by ANALMETR: 58;

            

             A12: b = c implies (b,d) _|_ (a,c) by A3, ANALMETR: 61;

            assume

             A13: LIN (a,b,c);

            a = b implies (b,d) _|_ (a,c) by A4, ANALMETR: 61;

            hence (b,d) _|_ (a,c) by A3, A4, A13, A11, A12, Th7;

          end;

          hence (b,d) _|_ (a,c) by A5;

        end;

        hence MS is Euclidean;

      end;

      now

        assume

         A14: MS is Euclidean;

        now

          let a,b,c be Element of MS;

          assume not LIN (a,b,c);

          then

          consider d be Element of MS such that

           A15: (d,a) _|_ (b,c) & (d,b) _|_ (a,c) by Th5;

          take d;

          (b,c) _|_ (a,d) & (c,a) _|_ (b,d) by A15, ANALMETR: 61;

          then (c,d) _|_ (b,a) by A14;

          hence (d,a) _|_ (b,c) & (d,b) _|_ (a,c) & (d,c) _|_ (a,b) by A15, ANALMETR: 61;

        end;

        hence MS is satisfying_3H by CONAFFM:def 3;

      end;

      hence thesis by A1;

    end;

    theorem :: EUCLMETR:9

    

     Th9: MS is Homogeneous iff MS is satisfying_ODES by CONAFFM:def 4;

    

     Lm1: MS is satisfying_PAP iff the AffinStruct of MS is Pappian

    proof

      set AS = the AffinStruct of MS;

       A1:

      now

        assume

         A2: MS is satisfying_PAP;

        now

          let M,N be Subset of AS, o,a,b,c,a9,b9,c9 be Element of AS such that

           A3: M is being_line & N is being_line and

           A4: M <> N and

           A5: o in M & o in N and

           A6: o <> a and

           A7: o <> a9 & o <> b and

           A8: o <> b9 & o <> c & o <> c9 & a in M and

           A9: b in M and

           A10: c in M and

           A11: a9 in N and

           A12: b9 in N & c9 in N and

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

           A14: (b,c9) // (c,b9);

          reconsider M9 = M, N9 = N as Subset of MS;

          reconsider a1 = a, b1 = b, c1 = c, a19 = a9, b19 = b9, c19 = c9 as Element of MS;

          

           A15: (b1,c19) // (c1,b19) by A14, ANALMETR: 36;

          (a1,b19) // (b1,a19) by A13, ANALMETR: 36;

          then

           A16: (b1,a19) // (a1,b19) by ANALMETR: 59;

          

           A17: M9 is being_line & N9 is being_line by A3, ANALMETR: 43;

          then ( not a19 in M9) & not b1 in N9 by A4, A5, A7, A9, A11, CONMETR: 5;

          then (c1,a19) // (a1,c19) by A2, A5, A6, A8, A9, A10, A11, A12, A17, A16, A15, CONMETR:def 2;

          then (a1,c19) // (c1,a19) by ANALMETR: 59;

          hence (a,c9) // (c,a9) by ANALMETR: 36;

        end;

        hence the AffinStruct of MS is Pappian by AFF_2:def 2;

      end;

      now

        assume

         A18: the AffinStruct of MS is Pappian;

        now

          let o,a1,a2,a3,b1,b2,b3 be Element of MS, M,N be Subset of the carrier of MS such that

           A19: M is being_line & N is being_line and

           A20: o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & ( not b2 in M) & not a3 in N & o <> a1 & o <> a2 and o <> a3 and

           A21: o <> b1 and o <> b2 and

           A22: o <> b3 and

           A23: (a3,b2) // (a2,b1) and

           A24: (a3,b3) // (a1,b1);

          reconsider M9 = M, N9 = N as Subset of AS;

          reconsider a = a1, b = a2, c = a3, a9 = b1, b9 = b2, c9 = b3 as Element of AS;

          

           A25: (c,c9) // (a,a9) by A24, ANALMETR: 36;

          (a2,b1) // (a3,b2) by A23, ANALMETR: 59;

          then

           A26: (b,a9) // (c,b9) by ANALMETR: 36;

          M9 is being_line & N9 is being_line by A19, ANALMETR: 43;

          then (b,c9) // (a,b9) by A18, A20, A21, A22, A26, A25, AFF_2:def 2;

          then (a2,b3) // (a1,b2) by ANALMETR: 36;

          hence (a1,b2) // (a2,b3) by ANALMETR: 59;

        end;

        hence MS is satisfying_PAP by CONMETR:def 2;

      end;

      hence thesis by A1;

    end;

    theorem :: EUCLMETR:10

    

     Th10: MS is Pappian iff MS is satisfying_PAP by Lm1;

    

     Lm2: MS is satisfying_DES iff the AffinStruct of MS is Desarguesian

    proof

      set AS = the AffinStruct of MS;

       A1:

      now

        assume

         A2: MS is satisfying_DES;

        now

          let A,P,C be Subset of AS, o,a,b,c,a9,b9,c9 be Element of AS such that

           A3: o in A and

           A4: o in P and

           A5: o in C and

           A6: o <> a and

           A7: o <> b and

           A8: o <> c and

           A9: a in A and

           A10: a9 in A and

           A11: b in P and

           A12: b9 in P and

           A13: c in C and

           A14: c9 in C and

           A15: A is being_line and

           A16: P is being_line and

           A17: C is being_line and

           A18: A <> P and

           A19: A <> C and

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

           A21: (a,c) // (a9,c9);

          now

            reconsider o1 = o, a1 = a, b1 = b, c1 = c, a19 = a9, b19 = b9, c19 = c9 as Element of MS;

            assume that

             A22: o <> a9 and

             A23: a <> a9;

            

             A24: (a1,b1) // (a19,b19) & (a1,c1) // (a19,c19) by A20, A21, ANALMETR: 36;

            

             A25: b <> b9 by A3, A4, A6, A7, A9, A10, A11, A15, A16, A18, A20, A23, AFF_4: 9;

            now

              assume LIN (b,b9,a);

              then a in P by A11, A12, A16, A25, AFF_1: 25;

              hence contradiction by A3, A4, A6, A9, A15, A16, A18, AFF_1: 18;

            end;

            then

             A26: not LIN (b1,b19,a1) by ANALMETR: 40;

             LIN (o,a,a9) by A3, A9, A10, A15, AFF_1: 21;

            then

             A27: LIN (o1,a1,a19) by ANALMETR: 40;

            now

              assume LIN (a,a9,c);

              then c in A by A9, A10, A15, A23, AFF_1: 25;

              hence contradiction by A3, A5, A8, A13, A15, A17, A19, AFF_1: 18;

            end;

            then

             A28: not LIN (a1,a19,c1) by ANALMETR: 40;

             LIN (o,b,b9) by A4, A11, A12, A16, AFF_1: 21;

            then

             A29: LIN (o1,b1,b19) by ANALMETR: 40;

             LIN (o,c,c9) by A5, A13, A14, A17, AFF_1: 21;

            then

             A30: LIN (o1,c1,c19) by ANALMETR: 40;

            o1 <> b19 & o1 <> c19 by A3, A4, A5, A6, A7, A8, A9, A10, A11, A13, A15, A16, A17, A18, A19, A20, A21, A22, AFF_4: 8;

            then (b1,c1) // (b19,c19) by A2, A6, A7, A8, A22, A27, A29, A30, A24, A26, A28, CONAFFM:def 1;

            hence (b,c) // (b9,c9) by ANALMETR: 36;

          end;

          hence (b,c) // (b9,c9) by A3, A4, A5, A6, A7, A8, A9, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, AFPROJ: 50;

        end;

        hence AS is Desarguesian by AFF_2:def 4;

      end;

      now

        assume

         A31: AS is Desarguesian;

        now

          let o,a,a1,b,b1,c,c1 be Element of MS such that

           A32: o <> a and o <> a1 and

           A33: o <> b and o <> b1 and

           A34: o <> c and o <> c1 and

           A35: not LIN (b,b1,a) and

           A36: not LIN (a,a1,c) and

           A37: LIN (o,a,a1) and

           A38: LIN (o,b,b1) and

           A39: LIN (o,c,c1) and

           A40: (a,b) // (a1,b1) & (a,c) // (a1,c1);

          reconsider o9 = o, a9 = a, b9 = b, c9 = c, a19 = a1, b19 = b1, c19 = c1 as Element of AS;

           LIN (o9,a9,a19) by A37, ANALMETR: 40;

          then

          consider A be Subset of AS such that

           A41: A is being_line and

           A42: o9 in A and

           A43: a9 in A and

           A44: a19 in A by AFF_1: 21;

           LIN (o9,c9,c19) by A39, ANALMETR: 40;

          then

          consider C be Subset of AS such that

           A45: C is being_line & o9 in C and

           A46: c9 in C and

           A47: c19 in C by AFF_1: 21;

          

           A48: A <> C

          proof

            assume A = C;

            then LIN (a9,a19,c9) by A41, A43, A44, A46, AFF_1: 21;

            hence contradiction by A36, ANALMETR: 40;

          end;

           LIN (o9,b9,b19) by A38, ANALMETR: 40;

          then

          consider P be Subset of AS such that

           A49: P is being_line and

           A50: o9 in P and

           A51: b9 in P & b19 in P by AFF_1: 21;

          

           A52: A <> P

          proof

            assume A = P;

            then LIN (b9,b19,a9) by A43, A49, A51, AFF_1: 21;

            hence contradiction by A35, ANALMETR: 40;

          end;

          (a9,b9) // (a19,b19) & (a9,c9) // (a19,c19) by A40, ANALMETR: 36;

          then (b9,c9) // (b19,c19) by A31, A32, A33, A34, A41, A42, A43, A44, A49, A50, A51, A45, A46, A47, A52, A48, AFF_2:def 4;

          hence (b,c) // (b1,c1) by ANALMETR: 36;

        end;

        hence MS is satisfying_DES by CONAFFM:def 1;

      end;

      hence thesis by A1;

    end;

    theorem :: EUCLMETR:11

    

     Th11: MS is Desarguesian iff MS is satisfying_DES by Lm2;

    theorem :: EUCLMETR:12

    MS is Moufangian iff MS is satisfying_TDES

    proof

      set AS = the AffinStruct of MS;

       A1:

      now

        assume

         A2: MS is satisfying_TDES;

        now

          let K be Subset of AS, o,a,b,c,a9,b9,c9 be Element of AS such that

           A3: K is being_line and

           A4: o in K and

           A5: c in K and

           A6: c9 in K and

           A7: not a in K and

           A8: o <> c and

           A9: a <> b and

           A10: LIN (o,a,a9) and

           A11: LIN (o,b,b9) and

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

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

           A14: (a,b) // K;

          reconsider o1 = o, a1 = a, b1 = b, c1 = c, a19 = a9, b19 = b9, c19 = c9 as Element of MS;

          

           A15: o1 <> b1 & (a1,c1) // (a19,c19) by A4, A7, A13, A14, AFF_1: 35, ANALMETR: 36;

          

           A16: not LIN (o,a,c)

          proof

            assume not thesis;

            then LIN (o,c,a) by AFF_1: 6;

            hence contradiction by A3, A4, A5, A7, A8, AFF_1: 25;

          end;

          

           A17: not LIN (o,a,b)

          proof

            set M = ( Line (a,b));

            assume not thesis;

            then LIN (a,b,o) by AFF_1: 6;

            then

             A18: o in M by AFF_1:def 2;

            a in M & M // K by A9, A14, AFF_1: 15, AFF_1:def 5;

            then a in K by A4, A18, AFF_1: 45;

            hence contradiction by A3, A4, A5, A16, AFF_1: 21;

          end;

          (a,b) // (o,c) by A3, A4, A5, A8, A14, AFF_1: 27;

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

          then

           A19: (b1,a1) // (o1,c1) by ANALMETR: 36;

          

           A20: LIN (o1,a1,a19) & LIN (o1,b1,b19) by A10, A11, ANALMETR: 40;

          (a1,b1) // (a19,b19) by A12, ANALMETR: 36;

          then

           A21: (b1,a1) // (b19,a19) by ANALMETR: 59;

          

           A22: LIN (o,c,c9) by A3, A4, A5, A6, AFF_1: 21;

          then

           A23: LIN (o1,c1,c19) by ANALMETR: 40;

           A24:

          now

            assume

             A25: a9 <> o;

             A26:

            now

              assume

               A27: a <> a9;

              

               A28: not LIN (a1,a19,c1)

              proof

                assume not thesis;

                then

                 A29: LIN (a,a9,c) by ANALMETR: 40;

                 LIN (a,a9,o) & LIN (a,a9,a) by A10, AFF_1: 6, AFF_1: 7;

                hence contradiction by A16, A27, A29, AFF_1: 8;

              end;

              

               A30: not LIN (a1,a19,b1)

              proof

                assume not thesis;

                then

                 A31: LIN (a,a9,b) by ANALMETR: 40;

                 LIN (a,a9,o) & LIN (a,a9,a) by A10, AFF_1: 6, AFF_1: 7;

                hence contradiction by A17, A27, A31, AFF_1: 8;

              end;

              (c,a) // (c9,a9) & not LIN (o,c,a) by A13, A16, AFF_1: 4, AFF_1: 6;

              then

               A32: o1 <> c19 by A10, A25, AFF_1: 55;

              (b,a) // (b9,a9) & not LIN (o,b,a) by A12, A17, AFF_1: 4, AFF_1: 6;

              then o1 <> b19 by A10, A25, AFF_1: 55;

              then (b1,c1) // (b19,c19) by A2, A4, A7, A8, A20, A23, A21, A19, A15, A25, A32, A28, A30, CONMETR:def 5;

              hence (b,c) // (b9,c9) by ANALMETR: 36;

            end;

            now

              

               A33: LIN (o,c,c) by AFF_1: 7;

              assume

               A34: a = a9;

              then (a,c) // (a9,c) by AFF_1: 2;

              then

               A35: c = c9 by A10, A13, A22, A16, A33, AFF_1: 56;

              

               A36: LIN (o,b,b) by AFF_1: 7;

              (a,b) // (a9,b) by A34, AFF_1: 2;

              then b = b9 by A10, A11, A12, A17, A36, AFF_1: 56;

              hence (b,c) // (b9,c9) by A35, AFF_1: 2;

            end;

            hence (b,c) // (b9,c9) by A26;

          end;

          now

            assume a9 = o;

            then b9 = o & c9 = o by A11, A12, A13, A22, A16, A17, AFF_1: 55;

            hence (b,c) // (b9,c9) by AFF_1: 3;

          end;

          hence (b,c) // (b9,c9) by A24;

        end;

        then AS is Moufangian by AFF_2:def 7;

        hence MS is Moufangian;

      end;

      now

        assume MS is Moufangian;

        then

         A37: AS is Moufangian;

        now

          let o,a,a1,b,b1,c,c1 be Element of MS such that o <> a and o <> a1 and

           A38: o <> b and o <> b1 and

           A39: o <> c and o <> c1 and

           A40: not LIN (b,b1,a) and

           A41: not LIN (b,b1,c) and

           A42: LIN (o,a,a1) and

           A43: LIN (o,b,b1) and

           A44: LIN (o,c,c1) and

           A45: (a,b) // (a1,b1) and

           A46: (a,b) // (o,c) and

           A47: (b,c) // (b1,c1);

          reconsider o9 = o, a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1 as Element of AS;

          set K = ( Line (o9,c9));

          

           A48: K is being_line by A39, AFF_1:def 3;

          (a9,b9) // (o9,c9) by A46, ANALMETR: 36;

          then (a9,b9) // K by A39, AFF_1:def 4;

          then

           A49: (b9,a9) // K by AFF_1: 34;

          (a9,b9) // (a19,b19) by A45, ANALMETR: 36;

          then

           A50: (b9,a9) // (b19,a19) by AFF_1: 4;

          

           A51: c9 in K by AFF_1: 15;

          

           A52: LIN (o9,a9,a19) & (b9,c9) // (b19,c19) by A42, A47, ANALMETR: 36, ANALMETR: 40;

          

           A53: b9 <> a9 by A40, Th1;

          

           A54: o9 in K by AFF_1: 15;

          

           A55: LIN (o9,b9,b19) by A43, ANALMETR: 40;

          

           A56: not b9 in K

          proof

            assume

             A57: b9 in K;

            then b19 in K by A38, A48, A54, A55, AFF_1: 25;

            then LIN (b9,b19,c9) by A48, A51, A57, AFF_1: 21;

            hence contradiction by A41, ANALMETR: 40;

          end;

           LIN (o9,c9,c19) by A44, ANALMETR: 40;

          then c19 in K by A39, A48, A54, A51, AFF_1: 25;

          then (a9,c9) // (a19,c19) by A37, A39, A48, A54, A51, A55, A56, A49, A50, A52, A53, AFF_2:def 7;

          hence (a,c) // (a1,c1) by ANALMETR: 36;

        end;

        hence MS is satisfying_TDES by CONMETR:def 5;

      end;

      hence thesis by A1;

    end;

    

     Lm3: MS is satisfying_des iff the AffinStruct of MS is translational

    proof

      set AS = the AffinStruct of MS;

       A1:

      now

        assume

         A2: MS is satisfying_des;

        now

          let A,P,C be Subset of AS, a,b,c,a9,b9,c9 be Element of AS such that

           A3: A // P and

           A4: A // C and

           A5: a in A and

           A6: a9 in A and

           A7: b in P and

           A8: b9 in P and

           A9: c in C and

           A10: c9 in C and

           A11: A is being_line and

           A12: P is being_line and

           A13: C is being_line and

           A14: A <> P and

           A15: A <> C and

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

           A17: (a,c) // (a9,c9);

          

           A18: not a in C by A4, A5, A15, AFF_1: 45;

           A19:

          now

            reconsider aa = a, a1 = a9, bb = b, b1 = b9, cc = c, c1 = c9 as Element of MS;

            (a,a9) // (b,b9) by A3, A5, A6, A7, A8, AFF_1: 39;

            then

             A20: (aa,a1) // (bb,b1) by ANALMETR: 36;

            (a,a9) // (c,c9) by A4, A5, A6, A9, A10, AFF_1: 39;

            then

             A21: (aa,a1) // (cc,c1) by ANALMETR: 36;

            assume

             A22: a <> a9;

            

             A23: not LIN (aa,a1,bb)

            proof

              assume not thesis;

              then LIN (a,a9,b) by ANALMETR: 40;

              then b in A by A5, A6, A11, A22, AFF_1: 25;

              hence contradiction by A3, A7, A14, AFF_1: 45;

            end;

            

             A24: not LIN (aa,a1,cc)

            proof

              assume not thesis;

              then LIN (a,a9,c) by ANALMETR: 40;

              then c in A by A5, A6, A11, A22, AFF_1: 25;

              hence contradiction by A4, A9, A15, AFF_1: 45;

            end;

            (aa,bb) // (a1,b1) & (aa,cc) // (a1,c1) by A16, A17, ANALMETR: 36;

            then (bb,cc) // (b1,c1) by A2, A23, A24, A20, A21, CONMETR:def 8;

            hence (b,c) // (b9,c9) by ANALMETR: 36;

          end;

          

           A25: not a in P by A3, A5, A14, AFF_1: 45;

          now

            assume

             A26: a = a9;

            then LIN (a,c,c9) by A17, AFF_1:def 1;

            then LIN (c,c9,a) by AFF_1: 6;

            then

             A27: c = c9 by A9, A10, A13, A18, AFF_1: 25;

             LIN (a,b,b9) by A16, A26, AFF_1:def 1;

            then LIN (b,b9,a) by AFF_1: 6;

            then b = b9 by A7, A8, A12, A25, AFF_1: 25;

            hence (b,c) // (b9,c9) by A27, AFF_1: 2;

          end;

          hence (b,c) // (b9,c9) by A19;

        end;

        hence AS is translational by AFF_2:def 11;

      end;

      now

        assume

         A28: AS is translational;

        now

          let a,a1,b,b1,c,c1 be Element of MS such that

           A29: ( not LIN (a,a1,b)) & not LIN (a,a1,c) and

           A30: (a,a1) // (b,b1) and

           A31: (a,a1) // (c,c1) and

           A32: (a,b) // (a1,b1) & (a,c) // (a1,c1);

          reconsider a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1 as Element of AS;

          

           A33: (a9,a19) // (b9,b19) by A30, ANALMETR: 36;

          

           A34: (a9,b9) // (a19,b19) & (a9,c9) // (a19,c19) by A32, ANALMETR: 36;

          

           A35: (a9,a19) // (c9,c19) by A31, ANALMETR: 36;

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

          

           A36: not (a9,a19) // (a9,b9) & not (a9,a19) // (a9,c9)

          proof

            assume not thesis;

            then (a,a1) // (a,b) or (a,a1) // (a,c) by ANALMETR: 36;

            hence contradiction by A29, ANALMETR:def 10;

          end;

          then

           A37: a9 <> a19 by AFF_1: 3;

          then

           A38: A is being_line by AFF_1:def 3;

          then

          consider C be Subset of AS such that

           A39: c9 in C and

           A40: A // C by AFF_1: 49;

          

           A41: C is being_line by A40, AFF_1: 36;

          

           A42: a9 in A & a19 in A by AFF_1: 15;

          then

           A43: A <> C by A36, A38, A39, AFF_1: 51;

          

           A44: (a9,a19) // A by A38, A42, AFF_1: 23;

          then (a9,a19) // C by A40, AFF_1: 43;

          then (c9,c19) // C by A35, A37, AFF_1: 32;

          then

           A45: c19 in C by A39, A41, AFF_1: 23;

          consider P be Subset of AS such that

           A46: b9 in P and

           A47: A // P by A38, AFF_1: 49;

          

           A48: P is being_line by A47, AFF_1: 36;

          (a9,a19) // P by A44, A47, AFF_1: 43;

          then (b9,b19) // P by A33, A37, AFF_1: 32;

          then

           A49: b19 in P by A46, A48, AFF_1: 23;

          A <> P by A36, A38, A42, A46, AFF_1: 51;

          then (b9,c9) // (b19,c19) by A28, A34, A38, A42, A46, A47, A39, A40, A48, A41, A49, A45, A43, AFF_2:def 11;

          hence (b,c) // (b1,c1) by ANALMETR: 36;

        end;

        hence MS is satisfying_des by CONMETR:def 8;

      end;

      hence thesis by A1;

    end;

    theorem :: EUCLMETR:13

    MS is translation iff MS is satisfying_des by Lm3;

    theorem :: EUCLMETR:14

    

     Th14: MS is Homogeneous implies MS is Desarguesian

    proof

      assume MS is Homogeneous;

      then MS is satisfying_ODES by Th9;

      then MS is satisfying_DES by CONAFFM: 1;

      hence thesis by Th11;

    end;

    theorem :: EUCLMETR:15

    

     Th15: MS is Euclidean Desarguesian implies MS is Pappian

    proof

      assume MS is Euclidean Desarguesian;

      then MS is satisfying_3H & MS is satisfying_DES by Th8, Th11;

      then MS is satisfying_PAP by CONMETR: 13, CONMETR: 15;

      hence thesis by Th10;

    end;

    reserve V for RealLinearSpace;

    reserve w,y,u,v for VECTOR of V;

    theorem :: EUCLMETR:16

    

     Th16: for o,c,c1,a,a1,a2 be Element of MS st not LIN (o,c,a) & o <> c1 & (o,c) _|_ (o,c1) & (o,a) _|_ (o,a1) & (o,a) _|_ (o,a2) & (c,a) _|_ (c1,a1) & (c,a) _|_ (c1,a2) holds a1 = a2

    proof

      let o,c,c1,a,a1,a2 be Element of MS such that

       A1: not LIN (o,c,a) and

       A2: o <> c1 & (o,c) _|_ (o,c1) and

       A3: (o,a) _|_ (o,a1) & (o,a) _|_ (o,a2) and

       A4: (c,a) _|_ (c1,a1) & (c,a) _|_ (c1,a2);

      reconsider o9 = o, a19 = a1, a29 = a2, c19 = c1 as Element of the AffinStruct of MS;

      assume

       A5: a1 <> a2;

      o <> a by A1, Th1;

      then (o,a1) // (o,a2) by A3, ANALMETR: 63;

      then (o9,a19) // (o9,a29) by ANALMETR: 36;

      then LIN (o9,a19,a29) by AFF_1:def 1;

      then

       A6: LIN (a19,a29,o9) by AFF_1: 6;

      a <> c by A1, Th1;

      then (c1,a1) // (c1,a2) by A4, ANALMETR: 63;

      then (c19,a19) // (c19,a29) by ANALMETR: 36;

      then LIN (c19,a19,a29) by AFF_1:def 1;

      then

       A7: LIN (a19,a29,c19) by AFF_1: 6;

       LIN (a19,a29,a29) by AFF_1: 7;

      then LIN (o9,c19,a29) by A5, A6, A7, AFF_1: 8;

      then (o9,c19) // (o9,a29) by AFF_1:def 1;

      then (o,c1) // (o,a2) by ANALMETR: 36;

      then

       A8: (o,c) _|_ (o,a2) by A2, ANALMETR: 62;

       LIN (a19,a29,a19) by AFF_1: 7;

      then LIN (o9,c19,a19) by A5, A6, A7, AFF_1: 8;

      then (o9,c19) // (o9,a19) by AFF_1:def 1;

      then (o,c1) // (o,a1) by ANALMETR: 36;

      then

       A9: (o,c) _|_ (o,a1) by A2, ANALMETR: 62;

      o <> a1 or o <> a2 by A5;

      then (o,c) // (o,a) by A3, A9, A8, ANALMETR: 63;

      hence contradiction by A1, ANALMETR:def 10;

    end;

    theorem :: EUCLMETR:17

    for o,c,c1,a be Element of MS st not LIN (o,c,a) holds ex a1 be Element of MS st (o,a) _|_ (o,a1) & (c,a) _|_ (c1,a1)

    proof

      let o,c,c1,a be Element of MS such that

       A1: not LIN (o,c,a);

      set X = ( Line (c,a)), Y = ( Line (o,a));

      c <> a by A1, Th1;

      then

       A2: X is being_line by ANALMETR:def 12;

      then

      consider X9 be Subset of MS such that

       A3: c1 in X9 and

       A4: X _|_ X9 by CONMETR: 3;

      o <> a by A1, Th1;

      then Y is being_line by ANALMETR:def 12;

      then

      consider Y9 be Subset of MS such that

       A5: o in Y9 and

       A6: Y _|_ Y9 by CONMETR: 3;

      reconsider X1 = X9, Y1 = Y9 as Subset of the AffinStruct of MS;

      Y9 is being_line by A6, ANALMETR: 44;

      then

       A7: Y1 is being_line by ANALMETR: 43;

      reconsider o9 = o, c9 = c, a9 = a as Element of the AffinStruct of MS;

      

       A8: X = ( Line (c9,a9)) by ANALMETR: 41;

      then

       A9: a in X by AFF_1: 15;

      Y = ( Line (o9,a9)) by ANALMETR: 41;

      then

       A10: o in Y & a in Y by AFF_1: 15;

      

       A11: c in X by A8, AFF_1: 15;

       not X9 // Y9

      proof

        reconsider X1 = X, Y1 = Y as Subset of the carrier of the AffinStruct of MS;

        assume not thesis;

        then X9 _|_ Y by A6, ANALMETR: 52;

        then X // Y by A4, ANALMETR: 65;

        then X1 // Y1 by ANALMETR: 46;

        then

         A12: o in X by A9, A10, AFF_1: 45;

        a in X by A8, AFF_1: 15;

        hence contradiction by A1, A2, A11, A12, CONMETR: 4;

      end;

      then

       A13: not X1 // Y1 by ANALMETR: 46;

      X9 is being_line by A4, ANALMETR: 44;

      then X1 is being_line by ANALMETR: 43;

      then

      consider a19 be Element of the AffinStruct of MS such that

       A14: a19 in X1 & a19 in Y1 by A7, A13, AFF_1: 58;

      reconsider a1 = a19 as Element of MS;

      take a1;

      thus thesis by A3, A4, A5, A6, A11, A9, A10, A14, ANALMETR: 56;

    end;

    

     Lm4: for u,v,y be VECTOR of V holds ((u - y) - (v - y)) = (u - v) & ((u + y) - (v + y)) = (u - v)

    proof

      let u,v,y be VECTOR of V;

      

      thus ((u - y) - (v - y)) = ((u - y) + (y - v)) by RLVECT_1: 33

      .= (u - v) by ANALOAF: 1;

      

      thus ((u + y) - (v + y)) = ((u - ( - y)) - (v + y)) by RLVECT_1: 17

      .= ((u - ( - y)) - (v - ( - y))) by RLVECT_1: 17

      .= ((u - ( - y)) + (( - y) - v)) by RLVECT_1: 33

      .= (u - v) by ANALOAF: 1;

    end;

    

     Lm5: Gen (w,y) implies for a,b,c be Real holds ( PProJ (w,y,((a * w) + (b * y)),(((c * b) * w) + (( - (c * a)) * y)))) = 0 & (((a * w) + (b * y)),(((c * b) * w) + (( - (c * a)) * y))) are_Ort_wrt (w,y)

    proof

      assume

       A1: Gen (w,y);

      let a,b,c be Real;

      reconsider a, b, c as Real;

      

       A2: ( pr2 (w,y,((a * w) + (b * y)))) = b & ( pr2 (w,y,(((c * b) * w) + (( - (c * a)) * y)))) = ( - (c * a)) by A1, GEOMTRAP:def 5;

      ( pr1 (w,y,((a * w) + (b * y)))) = a & ( pr1 (w,y,(((c * b) * w) + (( - (c * a)) * y)))) = (c * b) by A1, GEOMTRAP:def 4;

      

      then ( PProJ (w,y,((a * w) + (b * y)),(((c * b) * w) + (( - (c * a)) * y)))) = ((a * (b * c)) + (b * ( - (c * a)))) by A2, GEOMTRAP:def 6

      .= 0 ;

      hence thesis by A1, GEOMTRAP: 32;

    end;

    theorem :: EUCLMETR:18

    

     Th18: for a,b be Real st Gen (w,y) & ( 0. V) <> u & ( 0. V) <> v & (u,v) are_Ort_wrt (w,y) & u = ((a * w) + (b * y)) holds ex c be Real st c <> 0 & v = (((c * b) * w) + (( - (c * a)) * y))

    proof

      let a,b be Real such that

       A1: Gen (w,y) and

       A2: ( 0. V) <> u and

       A3: ( 0. V) <> v and

       A4: (u,v) are_Ort_wrt (w,y) and

       A5: u = ((a * w) + (b * y));

      set v9 = ((b * w) + (( - a) * y));

      v9 = (((1 * b) * w) + (( - (1 * a)) * y));

      then (u,v9) are_Ort_wrt (w,y) by A1, A5, Lm5;

      then

      consider a1,b1 be Real such that

       A6: (a1 * v) = (b1 * v9) and

       A7: a1 <> 0 or b1 <> 0 by A1, A2, A4, ANALMETR: 9;

       A8:

      now

        assume

         A9: a1 = 0 ;

        then ( 0. V) = (b1 * v9) by A6, RLVECT_1: 10;

        then v9 = ( 0. V) by A7, A9, RLVECT_1: 11;

        then b = 0 & ( - a) = 0 by A1, ANALMETR:def 1;

        

        then u = (( 0. V) + ( 0 * y)) by A5, RLVECT_1: 10

        .= (( 0. V) + ( 0. V)) by RLVECT_1: 10

        .= ( 0. V) by RLVECT_1: 4;

        hence contradiction by A2;

      end;

      take c = ((a1 " ) * b1);

       A10:

      now

        assume

         A11: b1 = 0 ;

        then ( 0. V) = (a1 * v) by A6, RLVECT_1: 10;

        hence contradiction by A3, A7, A11, RLVECT_1: 11;

      end;

      now

        assume c = 0 ;

        then (a1 " ) = 0 by A10, XCMPLX_1: 6;

        hence contradiction by A8, XCMPLX_1: 202;

      end;

      hence c <> 0 ;

      

      thus v = ((a1 " ) * (b1 * v9)) by A6, A8, ANALOAF: 5

      .= (c * v9) by RLVECT_1:def 7

      .= ((c * (b * w)) + (c * (( - a) * y))) by RLVECT_1:def 5

      .= (((c * b) * w) + (c * (( - a) * y))) by RLVECT_1:def 7

      .= (((c * b) * w) + ((c * ( - a)) * y)) by RLVECT_1:def 7

      .= (((c * b) * w) + (( - (c * a)) * y));

    end;

    theorem :: EUCLMETR:19

    

     Th19: Gen (w,y) & ( 0. V) <> u & ( 0. V) <> v & (u,v) are_Ort_wrt (w,y) implies ex c be Real st for a,b be Real holds (((a * w) + (b * y)),(((c * b) * w) + (( - (c * a)) * y))) are_Ort_wrt (w,y) & ((((a * w) + (b * y)) - u),((((c * b) * w) + (( - (c * a)) * y)) - v)) are_Ort_wrt (w,y)

    proof

      assume that

       A1: Gen (w,y) and

       A2: ( 0. V) <> u & ( 0. V) <> v and

       A3: (u,v) are_Ort_wrt (w,y);

      consider a1,a2 be Real such that

       A4: u = ((a1 * w) + (a2 * y)) by A1, ANALMETR:def 1;

      reconsider a1, a2 as Real;

      consider c be Real such that c <> 0 and

       A5: v = (((c * a2) * w) + (( - (c * a1)) * y)) by A1, A2, A3, A4, Th18;

      reconsider c as Real;

      take c;

      let a,b be Real;

      set u9 = ((a * w) + (b * y)), v9 = (((c * b) * w) + (( - (c * a)) * y));

      

       A6: ( pr1 (w,y,u9)) = a & ( pr2 (w,y,u9)) = b by A1, GEOMTRAP:def 4, GEOMTRAP:def 5;

      

       A7: ( pr1 (w,y,v9)) = (c * b) & ( pr2 (w,y,v9)) = ( - (c * a)) by A1, GEOMTRAP:def 4, GEOMTRAP:def 5;

      ( pr1 (w,y,u)) = a1 & ( pr2 (w,y,u)) = a2 by A1, A4, GEOMTRAP:def 4, GEOMTRAP:def 5;

      then

       A8: ( PProJ (w,y,u,v9)) = ((a1 * (c * b)) + (a2 * ( - (c * a)))) by A7, GEOMTRAP:def 6;

      ( pr1 (w,y,v)) = (c * a2) & ( pr2 (w,y,v)) = ( - (c * a1)) by A1, A5, GEOMTRAP:def 4, GEOMTRAP:def 5;

      then

       A9: ( PProJ (w,y,u9,v)) = (((c * a2) * a) + (( - (c * a1)) * b)) by A6, GEOMTRAP:def 6;

      thus (((a * w) + (b * y)),(((c * b) * w) + (( - (c * a)) * y))) are_Ort_wrt (w,y) by A1, Lm5;

      ( PProJ (w,y,(((a * w) + (b * y)) - u),((((c * b) * w) + (( - (c * a)) * y)) - v))) = (( PProJ (w,y,(u9 - u),v9)) - ( PProJ (w,y,(u9 - u),v))) by A1, GEOMTRAP: 30

      .= ((( PProJ (w,y,u9,v9)) - ( PProJ (w,y,u,v9))) - ( PProJ (w,y,(u9 - u),v))) by A1, GEOMTRAP: 30

      .= (( 0 - ( PProJ (w,y,u,v9))) - ( PProJ (w,y,(u9 - u),v))) by A1, Lm5

      .= (( - ( PProJ (w,y,u,v9))) - (( PProJ (w,y,u9,v)) - ( PProJ (w,y,u,v)))) by A1, GEOMTRAP: 30

      .= (( - ( PProJ (w,y,u,v9))) - (( PProJ (w,y,u9,v)) - 0 )) by A1, A3, GEOMTRAP: 32

      .= (( - 1) * (( PProJ (w,y,u,v9)) + ( PProJ (w,y,u9,v))));

      hence thesis by A1, A8, A9, GEOMTRAP: 32;

    end;

    

     Lm6: for w,y be VECTOR of V, a,b,c,d be Real holds (((a * w) + (b * y)) - ((c * w) + (d * y))) = (((a - c) * w) + ((b - d) * y))

    proof

      let w,y be VECTOR of V, a,b,c,d be Real;

      

      thus (((a * w) + (b * y)) - ((c * w) + (d * y))) = ((b * y) + ((a * w) - ((c * w) + (d * y)))) by RLVECT_1:def 3

      .= ((b * y) + (((a * w) - (c * w)) - (d * y))) by RLVECT_1: 27

      .= ((b * y) + (((a - c) * w) - (d * y))) by RLVECT_1: 35

      .= ((((a - c) * w) + (b * y)) - (d * y)) by RLVECT_1:def 3

      .= (((a - c) * w) + ((b * y) - (d * y))) by RLVECT_1:def 3

      .= (((a - c) * w) + ((b - d) * y)) by RLVECT_1: 35;

    end;

    

     Lm7: Gen (w,y) implies for a,b,c,d be Real st ((a * w) + (c * y)) = ((b * w) + (d * y)) holds a = b & c = d

    proof

      assume

       A1: Gen (w,y);

      let a,b,c,d be Real;

      assume ((a * w) + (c * y)) = ((b * w) + (d * y));

      

      then ( 0. V) = (((a * w) + (c * y)) - ((b * w) + (d * y))) by RLVECT_1: 15

      .= (((a - b) * w) + ((c - d) * y)) by Lm6;

      then (( - b) + a) = 0 & (( - d) + c) = 0 by A1, ANALMETR:def 1;

      hence thesis;

    end;

    theorem :: EUCLMETR:20

    

     Th20: Gen (w,y) & MS = ( AMSpace (V,w,y)) implies MS is satisfying_LIN

    proof

      assume that

       A1: Gen (w,y) and

       A2: MS = ( AMSpace (V,w,y));

      now

        let o,a,a1,b,b1,c,c1 be Element of MS such that

         A3: o <> a and o <> a1 and

         A4: o <> b and o <> b1 and

         A5: o <> c and

         A6: o <> c1 and a <> b and

         A7: (o,c) _|_ (o,c1) and

         A8: (o,a) _|_ (o,a1) and

         A9: (o,b) _|_ (o,b1) and

         A10: not LIN (o,c,a) and

         A11: LIN (o,a,b) and LIN (o,a1,b1) and

         A12: (a,c) _|_ (a1,c1) and

         A13: (b,c) _|_ (b1,c1);

        reconsider q = o, u1 = a, u2 = b, u3 = c, v3 = c1 as VECTOR of V by A2, ANALMETR: 19;

        consider A1,A2 be Real such that

         A14: (u1 - q) = ((A1 * w) + (A2 * y)) by A1, ANALMETR:def 1;

        reconsider A1, A2 as Real;

        

         A15: not LIN (o,c,b)

        proof

          reconsider o9 = o, a9 = a, b9 = b, c9 = c as Element of the AffinStruct of MS;

          assume LIN (o,c,b);

          then LIN (o9,c9,b9) by ANALMETR: 40;

          then

           A16: LIN (o9,b9,c9) by AFF_1: 6;

           LIN (o9,a9,b9) by A11, ANALMETR: 40;

          then

           A17: LIN (o9,b9,a9) by AFF_1: 6;

           LIN (o9,b9,o9) by AFF_1: 7;

          then LIN (o9,c9,a9) by A4, A16, A17, AFF_1: 8;

          hence contradiction by A10, ANALMETR: 40;

        end;

        (q,u3,q,v3) are_Ort_wrt (w,y) by A2, A7, ANALMETR: 21;

        then

         A18: ((u3 - q),(v3 - q)) are_Ort_wrt (w,y) by ANALMETR:def 3;

        (u3 - q) <> ( 0. V) & (v3 - q) <> ( 0. V) by A5, A6, RLVECT_1: 21;

        then

        consider r be Real such that

         A19: for a9,b9 be Real holds (((a9 * w) + (b9 * y)),(((r * b9) * w) + (( - (r * a9)) * y))) are_Ort_wrt (w,y) & ((((a9 * w) + (b9 * y)) - (u3 - q)),((((r * b9) * w) + (( - (r * a9)) * y)) - (v3 - q))) are_Ort_wrt (w,y) by A1, A18, Th19;

        (o,a) // (o,b) by A11, ANALMETR:def 10;

        then (q,u1) '||' (q,u2) by A2, GEOMTRAP: 4;

        then (q,u1) // (q,u2) or (q,u1) // (u2,q) by GEOMTRAP:def 1;

        then

        consider a9,b9 be Real such that

         A20: (a9 * (u1 - q)) = (b9 * (u2 - q)) and

         A21: a9 <> 0 or b9 <> 0 by ANALMETR: 14;

        consider B1,B2 be Real such that

         A22: (u2 - q) = ((B1 * w) + (B2 * y)) by A1, ANALMETR:def 1;

        reconsider a9, b9, B1, B2 as Real;

        set s = ((b9 " ) * a9);

        

         A23: (u1 - q) <> ( 0. V) by A3, RLVECT_1: 21;

        now

          assume

           A24: b9 = 0 ;

          then ( 0. V) = (a9 * (u1 - q)) by A20, RLVECT_1: 10;

          hence contradiction by A23, A21, A24, RLVECT_1: 11;

        end;

        

        then

         A25: (u2 - q) = ((b9 " ) * (a9 * (u1 - q))) by A20, ANALOAF: 5

        .= (s * (u1 - q)) by RLVECT_1:def 7;

        

        then ((B1 * w) + (B2 * y)) = ((s * (A1 * w)) + (s * (A2 * y))) by A14, A22, RLVECT_1:def 5

        .= (((s * A1) * w) + (s * (A2 * y))) by RLVECT_1:def 7

        .= (((s * A1) * w) + ((s * A2) * y)) by RLVECT_1:def 7;

        then

         A26: B1 = (s * A1) & B2 = (s * A2) by A1, Lm7;

        set v19 = ((((r * A2) * w) + (( - (r * A1)) * y)) + q), v29 = ((((r * B2) * w) + (( - (r * B1)) * y)) + q);

        reconsider a19 = v19, b19 = v29 as Element of MS by A2, ANALMETR: 19;

        

         A27: (v29 - q) = (((r * B2) * w) + (( - (r * B1)) * y)) by RLSUB_2: 61

        .= (((r * B2) * w) + ((r * B1) * ( - y))) by RLVECT_1: 24

        .= (((r * (s * A2)) * w) - ((r * (s * A1)) * y)) by A26, RLVECT_1: 25

        .= ((r * ((s * A2) * w)) - ((r * (s * A1)) * y)) by RLVECT_1:def 7

        .= ((r * ((s * A2) * w)) - (r * ((s * A1) * y))) by RLVECT_1:def 7

        .= (r * (((s * A2) * w) - ((s * A1) * y))) by RLVECT_1: 34

        .= (r * ((s * (A2 * w)) - ((s * A1) * y))) by RLVECT_1:def 7

        .= (r * ((s * (A2 * w)) - (s * (A1 * y)))) by RLVECT_1:def 7

        .= (r * (s * ((A2 * w) - (A1 * y)))) by RLVECT_1: 34

        .= ((s * r) * ((A2 * w) - (A1 * y))) by RLVECT_1:def 7

        .= (s * (r * ((A2 * w) - (A1 * y)))) by RLVECT_1:def 7

        .= (s * ((r * (A2 * w)) - (r * (A1 * y)))) by RLVECT_1: 34

        .= (s * (((r * A2) * w) - (r * (A1 * y)))) by RLVECT_1:def 7

        .= (s * (((r * A2) * w) + ( - ((r * A1) * y)))) by RLVECT_1:def 7

        .= (s * (((r * A2) * w) + ((r * A1) * ( - y)))) by RLVECT_1: 25

        .= (s * (((r * A2) * w) + (( - (r * A1)) * y))) by RLVECT_1: 24

        .= (s * (v19 - q)) by RLSUB_2: 61;

        

         A28: (v29 - q) = (((r * B2) * w) + (( - (r * B1)) * y)) by RLSUB_2: 61;

        then ((u2 - q),(v29 - q)) are_Ort_wrt (w,y) by A19, A22;

        then (q,u2,q,v29) are_Ort_wrt (w,y) by ANALMETR:def 3;

        then

         A29: (o,b) _|_ (o,b19) by A2, ANALMETR: 21;

        (1 * (u2 - v29)) = (u2 - v29) by RLVECT_1:def 8

        .= ((s * (u1 - q)) - (s * (v19 - q))) by A25, A27, Lm4

        .= (s * ((u1 - q) - (v19 - q))) by RLVECT_1: 34

        .= (s * (u1 - v19)) by Lm4;

        then (v19,u1) // (v29,u2) or (v19,u1) // (u2,v29) by ANALMETR: 14;

        then (v19,u1) '||' (v29,u2) by GEOMTRAP:def 1;

        then

         A30: (a19,a) // (b19,b) by A2, GEOMTRAP: 4;

        

         A31: (v19 - q) = (((r * A2) * w) + (( - (r * A1)) * y)) by RLSUB_2: 61;

        then ((u1 - q),(v19 - q)) are_Ort_wrt (w,y) by A19, A14;

        then (q,u1,q,v19) are_Ort_wrt (w,y) by ANALMETR:def 3;

        then

         A32: (o,a) _|_ (o,a19) by A2, ANALMETR: 21;

        ((u2 - q) - (u3 - q)) = (u2 - u3) & ((v29 - q) - (v3 - q)) = (v29 - v3) by Lm4;

        then ((u2 - u3),(v29 - v3)) are_Ort_wrt (w,y) by A19, A22, A28;

        then (u3,u2,v3,v29) are_Ort_wrt (w,y) by ANALMETR:def 3;

        then

         A33: (c,b) _|_ (c1,b19) by A2, ANALMETR: 21;

        (c,b) _|_ (c1,b1) by A13, ANALMETR: 61;

        then

         A34: b1 = b19 by A6, A7, A9, A15, A29, A33, Th16;

        ((u1 - q) - (u3 - q)) = (u1 - u3) & ((v19 - q) - (v3 - q)) = (v19 - v3) by Lm4;

        then ((u1 - u3),(v19 - v3)) are_Ort_wrt (w,y) by A19, A14, A31;

        then (u3,u1,v3,v19) are_Ort_wrt (w,y) by ANALMETR:def 3;

        then

         A35: (c,a) _|_ (c1,a19) by A2, ANALMETR: 21;

        (c,a) _|_ (c1,a1) by A12, ANALMETR: 61;

        then a1 = a19 by A6, A7, A8, A10, A32, A35, Th16;

        hence (a,a1) // (b,b1) by A34, A30, ANALMETR: 59;

      end;

      hence thesis by CONAFFM:def 5;

    end;

    theorem :: EUCLMETR:21

    

     Th21: for o,a,a1,b,b1,c,c1 be Element of MS st (o,b) _|_ (o,b1) & (o,c) _|_ (o,c1) & (a,b) _|_ (a1,b1) & (a,c) _|_ (a1,c1) & not (o,c) // (o,a) & not (o,a) // (o,b) & o = a1 holds (b,c) _|_ (b1,c1)

    proof

      let o,a,a1,b,b1,c,c1 be Element of MS such that

       A1: (o,b) _|_ (o,b1) and

       A2: (o,c) _|_ (o,c1) and

       A3: (a,b) _|_ (a1,b1) and

       A4: (a,c) _|_ (a1,c1) and

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

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

       A7: o = a1;

      

       A8: o = c1

      proof

        assume o <> c1;

        then (a,c) // (o,c) by A2, A4, A7, ANALMETR: 63;

        then (c,a) // (c,o) by ANALMETR: 59;

        then LIN (c,a,o) by ANALMETR:def 10;

        then LIN (o,c,a) by Th4;

        hence contradiction by A5, ANALMETR:def 10;

      end;

      o = b1

      proof

        assume o <> b1;

        then (a,b) // (o,b) by A1, A3, A7, ANALMETR: 63;

        then (b,a) // (b,o) by ANALMETR: 59;

        then LIN (b,a,o) by ANALMETR:def 10;

        then LIN (o,a,b) by Th4;

        hence contradiction by A6, ANALMETR:def 10;

      end;

      hence thesis by A8, ANALMETR: 58;

    end;

    theorem :: EUCLMETR:22

    

     Th22: Gen (w,y) & MS = ( AMSpace (V,w,y)) implies MS is Homogeneous

    proof

      assume that

       A1: Gen (w,y) and

       A2: MS = ( AMSpace (V,w,y));

      now

        let o,a,a1,b,b1,c,c1 be Element of MS such that

         A3: (o,a) _|_ (o,a1) and

         A4: (o,b) _|_ (o,b1) and

         A5: (o,c) _|_ (o,c1) and

         A6: (a,b) _|_ (a1,b1) and

         A7: (a,c) _|_ (a1,c1) and

         A8: ( not (o,c) // (o,a)) & not (o,a) // (o,b);

        reconsider q = o, u1 = a, u2 = b, u3 = c, v1 = a1 as VECTOR of V by A2, ANALMETR: 19;

        

         A9: not LIN (o,a,b) & not LIN (o,a,c)

        proof

          assume not thesis;

          then (o,a) // (o,b) or (o,a) // (o,c) by ANALMETR:def 10;

          hence contradiction by A8, ANALMETR: 59;

        end;

        then

         A10: o <> a by Th1;

        now

          (q,u1,q,v1) are_Ort_wrt (w,y) by A2, A3, ANALMETR: 21;

          then

           A11: ((u1 - q),(v1 - q)) are_Ort_wrt (w,y) by ANALMETR:def 3;

          

           A12: (u1 - q) <> ( 0. V) by A10, RLVECT_1: 21;

          assume

           A13: o <> a1;

          then (v1 - q) <> ( 0. V) by RLVECT_1: 21;

          then

          consider r be Real such that

           A14: for a9,b9 be Real holds (((a9 * w) + (b9 * y)),(((r * b9) * w) + (( - (r * a9)) * y))) are_Ort_wrt (w,y) & ((((a9 * w) + (b9 * y)) - (u1 - q)),((((r * b9) * w) + (( - (r * a9)) * y)) - (v1 - q))) are_Ort_wrt (w,y) by A1, A11, A12, Th19;

          consider B1,B2 be Real such that

           A15: (u2 - q) = ((B1 * w) + (B2 * y)) by A1, ANALMETR:def 1;

          consider A1,A2 be Real such that

           A16: (u3 - q) = ((A1 * w) + (A2 * y)) by A1, ANALMETR:def 1;

          reconsider B1, B2, A1, A2 as Real;

          set v39 = ((((r * A2) * w) + (( - (r * A1)) * y)) + q), v29 = ((((r * B2) * w) + (( - (r * B1)) * y)) + q);

          reconsider c19 = v39, b19 = v29 as Element of MS by A2, ANALMETR: 19;

          

           A17: (v29 - q) = (((r * B2) * w) + (( - (r * B1)) * y)) by RLSUB_2: 61;

          ((u2 - q) - (u1 - q)) = (u2 - u1) & ((v29 - q) - (v1 - q)) = (v29 - v1) by Lm4;

          then ((u2 - u1),(v29 - v1)) are_Ort_wrt (w,y) by A14, A15, A17;

          then (u1,u2,v1,v29) are_Ort_wrt (w,y) by ANALMETR:def 3;

          then

           A18: (a,b) _|_ (a1,b19) by A2, ANALMETR: 21;

          ((u2 - q),(v29 - q)) are_Ort_wrt (w,y) by A14, A15, A17;

          then (q,u2,q,v29) are_Ort_wrt (w,y) by ANALMETR:def 3;

          then (o,b) _|_ (o,b19) by A2, ANALMETR: 21;

          then

           A19: b1 = b19 by A3, A4, A6, A9, A13, A18, Th16;

          

           A20: (v39 - q) = (((r * A2) * w) + (( - (r * A1)) * y)) by RLSUB_2: 61;

          (u3 - u2) = (((A1 * w) + (A2 * y)) - ((B1 * w) + (B2 * y))) by A16, A15, Lm4

          .= (((A1 - B1) * w) + ((A2 - B2) * y)) by Lm6;

          then

           A21: ( pr1 (w,y,(u3 - u2))) = (A1 - B1) & ( pr2 (w,y,(u3 - u2))) = (A2 - B2) by A1, GEOMTRAP:def 4, GEOMTRAP:def 5;

          (v39 - v29) = ((((r * A2) * w) + ((r * ( - A1)) * y)) - (((r * B2) * w) + (( - (r * B1)) * y))) by Lm4

          .= ((((r * A2) - (r * B2)) * w) + (((r * ( - A1)) - (r * ( - B1))) * y)) by Lm6

          .= (((r * (A2 - B2)) * w) + ((r * (B1 - A1)) * y));

          then ( pr1 (w,y,(v39 - v29))) = (r * (A2 - B2)) & ( pr2 (w,y,(v39 - v29))) = (r * (B1 - A1)) by A1, GEOMTRAP:def 4, GEOMTRAP:def 5;

          

          then ( PProJ (w,y,(u3 - u2),(v39 - v29))) = (((A1 - B1) * (r * (A2 - B2))) + ((A2 - B2) * (r * (B1 - A1)))) by A21, GEOMTRAP:def 6

          .= 0 ;

          then ((u3 - u2),(v39 - v29)) are_Ort_wrt (w,y) by A1, GEOMTRAP: 32;

          then

           A22: (u2,u3,v29,v39) are_Ort_wrt (w,y) by ANALMETR:def 3;

          ((u3 - q) - (u1 - q)) = (u3 - u1) & ((v39 - q) - (v1 - q)) = (v39 - v1) by Lm4;

          then ((u3 - u1),(v39 - v1)) are_Ort_wrt (w,y) by A14, A16, A20;

          then (u1,u3,v1,v39) are_Ort_wrt (w,y) by ANALMETR:def 3;

          then

           A23: (a,c) _|_ (a1,c19) by A2, ANALMETR: 21;

          ((u3 - q),(v39 - q)) are_Ort_wrt (w,y) by A14, A16, A20;

          then (q,u3,q,v39) are_Ort_wrt (w,y) by ANALMETR:def 3;

          then (o,c) _|_ (o,c19) by A2, ANALMETR: 21;

          then c1 = c19 by A3, A5, A7, A9, A13, A23, Th16;

          hence (b,c) _|_ (b1,c1) by A2, A19, A22, ANALMETR: 21;

        end;

        hence (b,c) _|_ (b1,c1) by A4, A5, A6, A7, A8, Th21;

      end;

      hence thesis;

    end;

    registration

      cluster Euclidean Pappian Desarguesian Homogeneous translation Fanoian Moufangian for OrtAfPl;

      existence

      proof

        consider V such that

         A1: ex w, y st Gen (w,y) by ANALMETR: 3;

        consider w, y such that

         A2: Gen (w,y) by A1;

        reconsider MS = ( AMSpace (V,w,y)) as OrtAfPl by A2, ANALMETR: 34;

        

         A3: MS is satisfying_3H by A2, Th20, CONAFFM: 6;

        for a,b be Real st ((a * w) + (b * y)) = ( 0. V) holds a = 0 & b = 0 by A2, ANALMETR:def 1;

        then

        reconsider OAS = ( OASpace V) as OAffinSpace by ANALOAF: 26;

        take MS;

        

         A4: the AffinStruct of MS = ( Lambda OAS) by ANALMETR: 20;

        then

         A5: the AffinStruct of MS is Moufangian & the AffinStruct of MS is translational by PAPDESAF: 16, PAPDESAF: 17;

         the AffinStruct of MS is Pappian & the AffinStruct of MS is Desarguesian by A4, PAPDESAF: 13, PAPDESAF: 14;

        hence thesis by A2, A3, A4, A5, Th8, Th22;

      end;

    end

    registration

      cluster Euclidean Pappian Desarguesian Homogeneous translation Fanoian Moufangian for OrtAfSp;

      existence

      proof

        set MS = the Euclidean Pappian Desarguesian Homogeneous translation Fanoian Moufangian OrtAfPl;

        MS is Euclidean Pappian Desarguesian Homogeneous translation Fanoian Moufangian;

        hence thesis;

      end;

    end

    theorem :: EUCLMETR:23

     Gen (w,y) & MS = ( AMSpace (V,w,y)) implies MS is Euclidean Pappian Desarguesian Homogeneous translation Fanoian Moufangian OrtAfPl

    proof

      assume that

       A1: Gen (w,y) and

       A2: MS = ( AMSpace (V,w,y));

      reconsider MS9 = ( AMSpace (V,w,y)) as OrtAfPl by A2;

      

       A3: MS9 is satisfying_3H by A1, Th20, CONAFFM: 6;

      for a,b be Real st ((a * w) + (b * y)) = ( 0. V) holds a = 0 & b = 0 by A1, ANALMETR:def 1;

      then

      reconsider OAS = ( OASpace V) as OAffinSpace by ANALOAF: 26;

      

       A4: the AffinStruct of MS9 = ( Lambda OAS) by ANALMETR: 20;

      then

       A5: the AffinStruct of MS9 is Moufangian & the AffinStruct of MS9 is translational by PAPDESAF: 16, PAPDESAF: 17;

       the AffinStruct of MS9 is Pappian & the AffinStruct of MS9 is Desarguesian by A4, PAPDESAF: 13, PAPDESAF: 14;

      hence thesis by A1, A2, A3, A4, A5, Def2, Def3, Def4, Def5, Def6, Th8, Th22;

    end;

    registration

      let MS be Pappian OrtAfPl;

      cluster the AffinStruct of MS -> Pappian;

      correctness by Def2;

    end

    registration

      let MS be Desarguesian OrtAfPl;

      cluster the AffinStruct of MS -> Desarguesian;

      correctness by Def3;

    end

    registration

      let MS be Moufangian OrtAfPl;

      cluster the AffinStruct of MS -> Moufangian;

      correctness by Def5;

    end

    registration

      let MS be translation OrtAfPl;

      cluster the AffinStruct of MS -> translational;

      correctness by Def6;

    end

    registration

      let MS be Fanoian OrtAfPl;

      cluster the AffinStruct of MS -> Fanoian;

      correctness by Def4;

    end

    registration

      let MS be Homogeneous OrtAfPl;

      cluster the AffinStruct of MS -> Desarguesian;

      correctness

      proof

        MS is Desarguesian by Th14;

        hence thesis;

      end;

    end

    registration

      let MS be Euclidean Desarguesian OrtAfPl;

      cluster the AffinStruct of MS -> Pappian;

      correctness

      proof

        MS is Pappian by Th15;

        hence thesis;

      end;

    end

    registration

      let MS be Pappian OrtAfSp;

      cluster the AffinStruct of MS -> Pappian;

      correctness by Def2;

    end

    registration

      let MS be Desarguesian OrtAfSp;

      cluster the AffinStruct of MS -> Desarguesian;

      correctness by Def3;

    end

    registration

      let MS be Moufangian OrtAfSp;

      cluster the AffinStruct of MS -> Moufangian;

      correctness by Def5;

    end

    registration

      let MS be translation OrtAfSp;

      cluster the AffinStruct of MS -> translational;

      correctness by Def6;

    end

    registration

      let MS be Fanoian OrtAfSp;

      cluster the AffinStruct of MS -> Fanoian;

      correctness by Def4;

    end