afvect0.miz



    begin

    definition

      let IT be non empty AffinStruct;

      :: AFVECT0:def1

      attr IT is WeakAffVect-like means

      : Def1: (for a,b,c be Element of IT st (a,b) // (c,c) holds a = b) & (for a,b,c,d,p,q be Element of IT st (a,b) // (p,q) & (c,d) // (p,q) holds (a,b) // (c,d)) & (for a,b,c be Element of IT holds ex d be Element of IT st (a,b) // (c,d)) & (for a,b,c,a9,b9,c9 be Element of IT st (a,b) // (a9,b9) & (a,c) // (a9,c9) holds (b,c) // (b9,c9)) & (for a,c be Element of IT holds ex b be Element of IT st (a,b) // (b,c)) & for a,b,c,d be Element of IT st (a,b) // (c,d) holds (a,c) // (b,d);

    end

    registration

      cluster strict WeakAffVect-like for non trivial AffinStruct;

      existence

      proof

        set AFV = the strict AffVect;

        reconsider AS = AFV as non empty AffinStruct;

        

         A1: (for a,b,c be Element of AS holds ex d be Element of AS st (a,b) // (c,d)) & for a,b,c,a9,b9,c9 be Element of AS st (a,b) // (a9,b9) & (a,c) // (a9,c9) holds (b,c) // (b9,c9) by TDGROUP: 16;

        

         A2: (for a,c be Element of AS holds ex b be Element of AS st (a,b) // (b,c)) & for a,b,c,d be Element of AS st (a,b) // (c,d) holds (a,c) // (b,d) by TDGROUP: 16;

        (for a,b,c be Element of AS st (a,b) // (c,c) holds a = b) & for a,b,c,d,p,q be Element of AS st (a,b) // (p,q) & (c,d) // (p,q) holds (a,b) // (c,d) by TDGROUP: 16;

        then AS is WeakAffVect-like by A1, A2;

        hence thesis;

      end;

    end

    definition

      mode WeakAffVect is WeakAffVect-like non trivial AffinStruct;

    end

    registration

      cluster AffVect-like -> WeakAffVect-like for non empty AffinStruct;

      coherence by TDGROUP:def 5;

    end

    reserve AFV for WeakAffVect;

    reserve a,b,c,d,e,f,a9,b9,c9,d9,f9,p,q,r,o,x99 for Element of AFV;

    theorem :: AFVECT0:1

    

     Th1: (a,b) // (a,b)

    proof

      ex d st (a,b) // (b,d) by Def1;

      hence thesis by Def1;

    end;

    theorem :: AFVECT0:2

    (a,a) // (a,a) by Th1;

    theorem :: AFVECT0:3

    

     Th3: (a,b) // (c,d) implies (c,d) // (a,b)

    proof

      assume

       A1: (a,b) // (c,d);

      (c,d) // (c,d) by Th1;

      hence thesis by A1, Def1;

    end;

    theorem :: AFVECT0:4

    

     Th4: (a,b) // (a,c) implies b = c

    proof

      assume (a,b) // (a,c);

      then (a,a) // (b,c) by Def1;

      then (b,c) // (a,a) by Th3;

      hence thesis by Def1;

    end;

    theorem :: AFVECT0:5

    

     Th5: (a,b) // (c,d) & (a,b) // (c,d9) implies d = d9

    proof

      assume (a,b) // (c,d) & (a,b) // (c,d9);

      then (c,d) // (a,b) & (c,d9) // (a,b) by Th3;

      then (c,d) // (c,d9) by Def1;

      hence thesis by Th4;

    end;

    theorem :: AFVECT0:6

    

     Th6: for a, b holds (a,a) // (b,b)

    proof

      let a, b;

      consider p such that

       A1: (a,a) // (b,p) by Def1;

      (b,p) // (a,a) by A1, Th3;

      hence thesis by A1, Def1;

    end;

    theorem :: AFVECT0:7

    

     Th7: (a,b) // (c,d) implies (b,a) // (d,c)

    proof

      assume

       A1: (a,b) // (c,d);

      (a,a) // (c,c) by Th6;

      hence thesis by A1, Def1;

    end;

    theorem :: AFVECT0:8

    (a,b) // (c,d) & (a,c) // (b9,d) implies b = b9

    proof

      assume that

       A1: (a,b) // (c,d) and

       A2: (a,c) // (b9,d);

      (a,c) // (b,d) by A1, Def1;

      then (b,d) // (a,c) by Th3;

      then

       A3: (d,b) // (c,a) by Th7;

      (b9,d) // (a,c) by A2, Th3;

      then (d,b9) // (c,a) by Th7;

      then (d,b) // (d,b9) by A3, Def1;

      hence thesis by Th4;

    end;

    theorem :: AFVECT0:9

    (b,c) // (b9,c9) & (a,d) // (b,c) & (a,d9) // (b9,c9) implies d = d9

    proof

      assume that

       A1: (b,c) // (b9,c9) and

       A2: (a,d) // (b,c) and

       A3: (a,d9) // (b9,c9);

      (b9,c9) // (b,c) by A1, Th3;

      then (a,d) // (b9,c9) by A2, Def1;

      then (a,d) // (a,d9) by A3, Def1;

      hence thesis by Th4;

    end;

    theorem :: AFVECT0:10

    (a,b) // (a9,b9) & (c,d) // (b,a) & (c,d9) // (b9,a9) implies d = d9

    proof

      assume that

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

       A2: (c,d) // (b,a) and

       A3: (c,d9) // (b9,a9);

      (a9,b9) // (a,b) by A1, Th3;

      then (b9,a9) // (b,a) by Th7;

      then (c,d) // (b9,a9) by A2, Def1;

      then (c,d) // (c,d9) by A3, Def1;

      hence thesis by Th4;

    end;

    theorem :: AFVECT0:11

    (a,b) // (a9,b9) & (c,d) // (c9,d9) & (b,f) // (c,d) & (b9,f9) // (c9,d9) implies (a,f) // (a9,f9)

    proof

      assume that

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

       A2: (c,d) // (c9,d9) and

       A3: (b,f) // (c,d) and

       A4: (b9,f9) // (c9,d9);

      (b9,f9) // (c,d) by A2, A4, Def1;

      then

       A5: (b,f) // (b9,f9) by A3, Def1;

      (b,a) // (b9,a9) by A1, Th7;

      hence thesis by A5, Def1;

    end;

    theorem :: AFVECT0:12

    

     Th12: (a,b) // (a9,b9) & (a,c) // (c9,b9) implies (b,c) // (c9,a9)

    proof

      assume that

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

       A2: (a,c) // (c9,b9);

      consider d such that

       A3: (c9,b9) // (a9,d) by Def1;

      (a9,d) // (c9,b9) by A3, Th3;

      then (a,c) // (a9,d) by A2, Def1;

      then

       A4: (b,c) // (b9,d) by A1, Def1;

      (c9,a9) // (b9,d) by A3, Def1;

      hence thesis by A4, Def1;

    end;

    definition

      let AFV;

      let a, b;

      :: AFVECT0:def2

      pred MDist a,b means (a,b) // (b,a) & a <> b;

      irreflexivity ;

      symmetry by Th3;

    end

    theorem :: AFVECT0:13

    ex a, b st a <> b & not MDist (a,b)

    proof

      consider p, q such that

       A1: p <> q by STRUCT_0:def 10;

      now

        consider r such that

         A2: (p,r) // (r,q) by Def1;

         A3:

        now

           A4:

          now

            assume MDist (p,r);

            then

             A5: (p,r) // (r,p);

            (r,q) // (p,r) by A2, Th3;

            then (q,r) // (r,p) by Th7;

            then (p,r) // (q,r) by A5, Def1;

            hence thesis by A1, Th4, Th7;

          end;

          assume p <> r;

          hence thesis by A4;

        end;

        now

          assume

           A6: p = r;

          then (r,q) // (p,p) by A2, Th3;

          hence thesis by A1, A6, Def1;

        end;

        hence thesis by A3;

      end;

      hence thesis;

    end;

    theorem :: AFVECT0:14

     MDist (a,b) & MDist (a,c) implies b = c or MDist (b,c)

    proof

      assume that

       A1: MDist (a,b) and

       A2: MDist (a,c);

      

       A3: (a,b) // (b,a) by A1;

      

       A4: (a,c) // (c,a) by A2;

      consider d such that

       A5: (c,a) // (b,d) by Def1;

      (b,d) // (c,a) by A5, Th3;

      then (a,c) // (b,d) by A4, Def1;

      then

       A6: (b,c) // (a,d) by A3, Def1;

      (c,b) // (a,d) by A5, Def1;

      then (b,c) // (c,b) by A6, Def1;

      hence thesis;

    end;

    theorem :: AFVECT0:15

     MDist (a,b) & (a,b) // (c,d) implies MDist (c,d)

    proof

      assume that

       A1: MDist (a,b) and

       A2: (a,b) // (c,d);

      

       A3: (a,b) // (b,a) by A1;

      

       A4: (c,d) // (a,b) by A2, Th3;

      then (d,c) // (b,a) by Th7;

      then (d,c) // (a,b) by A3, Def1;

      then (c,d) // (d,c) by A4, Def1;

      then c <> d implies thesis;

      hence thesis by A1, A2, Def1;

    end;

    definition

      let AFV;

      let a, b, c;

      :: AFVECT0:def3

      pred Mid a,b,c means

      : Def3: (a,b) // (b,c);

    end

    theorem :: AFVECT0:16

    

     Th16: Mid (a,b,c) implies Mid (c,b,a)

    proof

      assume Mid (a,b,c);

      then (a,b) // (b,c);

      then (b,a) // (c,b) by Th7;

      then (c,b) // (b,a) by Th3;

      hence thesis;

    end;

    theorem :: AFVECT0:17

     Mid (a,b,b) iff a = b by Def1, Th6;

    theorem :: AFVECT0:18

    

     Th18: Mid (a,b,a) iff a = b or MDist (a,b) by Th6;

    theorem :: AFVECT0:19

    

     Th19: ex b st Mid (a,b,c)

    proof

      consider b such that

       A1: (a,b) // (b,c) by Def1;

       Mid (a,b,c) by A1;

      hence thesis;

    end;

    theorem :: AFVECT0:20

    

     Th20: Mid (a,b,c) & Mid (a,b9,c) implies b = b9 or MDist (b,b9)

    proof

      assume that

       A1: Mid (a,b,c) and

       A2: Mid (a,b9,c);

      

       A3: (a,b) // (b,c) by A1;

      consider d such that

       A4: (b9,c) // (b,d) by Def1;

      

       A5: (b,d) // (b9,c) by A4, Th3;

      then (b,b9) // (d,c) by Def1;

      then

       A6: (b9,b) // (c,d) by Th7;

      (a,b9) // (b9,c) by A2;

      then (a,b9) // (b,d) by A5, Def1;

      then (b,b9) // (c,d) by A3, Def1;

      then (b,b9) // (b9,b) by A6, Def1;

      hence thesis;

    end;

    theorem :: AFVECT0:21

    

     Th21: ex c st Mid (a,b,c)

    proof

      consider c such that

       A1: (a,b) // (b,c) by Def1;

       Mid (a,b,c) by A1;

      hence thesis;

    end;

    theorem :: AFVECT0:22

    

     Th22: Mid (a,b,c) & Mid (a,b,c9) implies c = c9

    proof

      assume that

       A1: Mid (a,b,c) and

       A2: Mid (a,b,c9);

      (a,b) // (b,c9) by A2;

      then

       A3: (b,c9) // (a,b) by Th3;

      (a,b) // (b,c) by A1;

      then (b,c) // (a,b) by Th3;

      then (b,c) // (b,c9) by A3, Def1;

      hence thesis by Th4;

    end;

    theorem :: AFVECT0:23

    

     Th23: Mid (a,b,c) & MDist (b,b9) implies Mid (a,b9,c)

    proof

      assume that

       A1: Mid (a,b,c) and

       A2: MDist (b,b9);

      

       A3: (b,b9) // (b9,b) by A2;

      (a,b) // (b,c) by A1;

      then

       A4: (b,a) // (c,b) by Th7;

      consider d such that

       A5: (b9,b) // (c,d) by Def1;

      (c,d) // (b9,b) by A5, Th3;

      then (b,b9) // (c,d) by A3, Def1;

      then

       A6: (a,b9) // (b,d) by A4, Def1;

      (b9,c) // (b,d) by A5, Def1;

      then (a,b9) // (b9,c) by A6, Def1;

      hence thesis;

    end;

    theorem :: AFVECT0:24

    

     Th24: Mid (a,b,c) & Mid (a,b9,c9) & MDist (b,b9) implies c = c9

    proof

      assume that

       A1: Mid (a,b,c) and

       A2: Mid (a,b9,c9) and

       A3: MDist (b,b9);

       Mid (a,b9,c) by A1, A3, Th23;

      hence thesis by A2, Th22;

    end;

    theorem :: AFVECT0:25

    

     Th25: Mid (a,p,a9) & Mid (b,p,b9) implies (a,b) // (b9,a9)

    proof

      assume that

       A1: Mid (a,p,a9) and

       A2: Mid (b,p,b9);

      consider d such that

       A3: (b9,p) // (a9,d) by Def1;

      (a,p) // (p,a9) by A1;

      then

       A4: (p,a) // (a9,p) by Th7;

      (b,p) // (p,b9) by A2;

      then

       A5: (p,b) // (b9,p) by Th7;

      (a9,d) // (b9,p) by A3, Th3;

      then (p,b) // (a9,d) by A5, Def1;

      then

       A6: (a,b) // (p,d) by A4, Def1;

      (b9,a9) // (p,d) by A3, Def1;

      hence thesis by A6, Def1;

    end;

    theorem :: AFVECT0:26

     Mid (a,p,a9) & Mid (b,q,b9) & MDist (p,q) implies (a,b) // (b9,a9)

    proof

      assume that

       A1: Mid (a,p,a9) and

       A2: Mid (b,q,b9) and

       A3: MDist (p,q);

       Mid (a,q,a9) by A1, A3, Th23;

      hence thesis by A2, Th25;

    end;

    definition

      let AFV;

      let a, b;

      :: AFVECT0:def4

      func PSym (a,b) -> Element of AFV means

      : Def4: Mid (b,a,it );

      correctness by Th21, Th22;

    end

    theorem :: AFVECT0:27

    ( PSym (p,a)) = b iff (a,p) // (p,b) by Def3, Def4;

    theorem :: AFVECT0:28

    

     Th28: ( PSym (p,a)) = a iff a = p or MDist (a,p)

    proof

       A1:

      now

        assume a = p or MDist (a,p);

        then Mid (a,p,a) by Th18;

        hence ( PSym (p,a)) = a by Def4;

      end;

      now

        assume ( PSym (p,a)) = a;

        then Mid (a,p,a) by Def4;

        hence a = p or MDist (a,p);

      end;

      hence thesis by A1;

    end;

    theorem :: AFVECT0:29

    

     Th29: ( PSym (p,( PSym (p,a)))) = a

    proof

       Mid (a,p,( PSym (p,a))) by Def4;

      then Mid (( PSym (p,a)),p,a) by Th16;

      hence thesis by Def4;

    end;

    theorem :: AFVECT0:30

    

     Th30: ( PSym (p,a)) = ( PSym (p,b)) implies a = b

    proof

      assume

       A1: ( PSym (p,a)) = ( PSym (p,b));

      ( PSym (p,( PSym (p,a)))) = a by Th29;

      hence thesis by A1, Th29;

    end;

    theorem :: AFVECT0:31

    ex a st ( PSym (p,a)) = b

    proof

      ( PSym (p,( PSym (p,b)))) = b by Th29;

      hence thesis;

    end;

    theorem :: AFVECT0:32

    

     Th32: (a,b) // (( PSym (p,b)),( PSym (p,a)))

    proof

       Mid (a,p,( PSym (p,a))) & Mid (b,p,( PSym (p,b))) by Def4;

      hence thesis by Th25;

    end;

    theorem :: AFVECT0:33

    

     Th33: (a,b) // (c,d) iff (( PSym (p,a)),( PSym (p,b))) // (( PSym (p,c)),( PSym (p,d)))

    proof

       A1:

      now

        assume

         A2: (( PSym (p,a)),( PSym (p,b))) // (( PSym (p,c)),( PSym (p,d)));

        (d,c) // (( PSym (p,c)),( PSym (p,d))) by Th32;

        then (d,c) // (( PSym (p,a)),( PSym (p,b))) by A2, Def1;

        then

         A3: (c,d) // (( PSym (p,b)),( PSym (p,a))) by Th7;

        (a,b) // (( PSym (p,b)),( PSym (p,a))) by Th32;

        hence (a,b) // (c,d) by A3, Def1;

      end;

      now

        

         A4: (( PSym (p,b)),( PSym (p,a))) // (a,b) by Th3, Th32;

        assume

         A5: (a,b) // (c,d);

        (( PSym (p,d)),( PSym (p,c))) // (c,d) by Th3, Th32;

        then (( PSym (p,d)),( PSym (p,c))) // (a,b) by A5, Def1;

        then (( PSym (p,b)),( PSym (p,a))) // (( PSym (p,d)),( PSym (p,c))) by A4, Def1;

        hence (( PSym (p,a)),( PSym (p,b))) // (( PSym (p,c)),( PSym (p,d))) by Th7;

      end;

      hence thesis by A1;

    end;

    theorem :: AFVECT0:34

     MDist (a,b) iff MDist (( PSym (p,a)),( PSym (p,b))) by Th30, Th33;

    theorem :: AFVECT0:35

    

     Th35: Mid (a,b,c) iff Mid (( PSym (p,a)),( PSym (p,b)),( PSym (p,c))) by Th33;

    theorem :: AFVECT0:36

    

     Th36: ( PSym (p,a)) = ( PSym (q,a)) iff p = q or MDist (p,q)

    proof

       A1:

      now

        assume

         A2: MDist (p,q);

         Mid (a,p,( PSym (p,a))) & Mid (a,q,( PSym (q,a))) by Def4;

        hence ( PSym (p,a)) = ( PSym (q,a)) by A2, Th24;

      end;

      now

        assume

         A3: ( PSym (p,a)) = ( PSym (q,a));

         Mid (a,p,( PSym (p,a))) & Mid (a,q,( PSym (q,a))) by Def4;

        hence p = q or MDist (p,q) by A3, Th20;

      end;

      hence thesis by A1;

    end;

    theorem :: AFVECT0:37

    

     Th37: ( PSym (q,( PSym (p,( PSym (q,a)))))) = ( PSym (( PSym (q,p)),a))

    proof

       Mid (( PSym (q,a)),p,( PSym (p,( PSym (q,a))))) by Def4;

      then Mid (( PSym (q,( PSym (q,a)))),( PSym (q,p)),( PSym (q,( PSym (p,( PSym (q,a))))))) by Th35;

      then ( PSym (q,( PSym (p,( PSym (q,a)))))) = ( PSym (( PSym (q,p)),( PSym (q,( PSym (q,a)))))) by Def4;

      hence thesis by Th29;

    end;

    theorem :: AFVECT0:38

    ( PSym (p,( PSym (q,a)))) = ( PSym (q,( PSym (p,a)))) iff p = q or MDist (p,q) or MDist (q,( PSym (p,q)))

    proof

       A1:

      now

        assume ( PSym (p,( PSym (q,a)))) = ( PSym (q,( PSym (p,a))));

        then ( PSym (p,( PSym (q,( PSym (p,a)))))) = ( PSym (q,a)) by Th29;

        then ( PSym (( PSym (p,q)),a)) = ( PSym (q,a)) by Th37;

        then q = ( PSym (p,q)) or MDist (q,( PSym (p,q))) by Th36;

        then

         A2: Mid (q,p,q) or MDist (q,( PSym (p,q))) by Def4;

        hence p = q or MDist (q,p) or MDist (q,( PSym (p,q)));

        thus p = q or MDist (p,q) or MDist (q,( PSym (p,q))) by A2, Th18;

      end;

      now

        assume p = q or MDist (p,q) or MDist (q,( PSym (p,q)));

        then Mid (q,p,q) or MDist (q,( PSym (p,q))) by Th18;

        then ( PSym (( PSym (p,q)),a)) = ( PSym (q,a)) by Def4, Th36;

        then ( PSym (p,( PSym (q,( PSym (p,a)))))) = ( PSym (q,a)) by Th37;

        hence ( PSym (p,( PSym (q,a)))) = ( PSym (q,( PSym (p,a)))) by Th29;

      end;

      hence thesis by A1;

    end;

    theorem :: AFVECT0:39

    

     Th39: ( PSym (p,( PSym (q,( PSym (r,a)))))) = ( PSym (r,( PSym (q,( PSym (p,a))))))

    proof

      (p,a) // (( PSym (r,a)),( PSym (r,p))) & (( PSym (q,( PSym (r,p)))),( PSym (q,( PSym (r,a))))) // (( PSym (r,a)),( PSym (r,p))) by Th3, Th32;

      then

       A1: (p,a) // (( PSym (q,( PSym (r,p)))),( PSym (q,( PSym (r,a))))) by Def1;

      (p,a) // (( PSym (p,a)),( PSym (p,p))) & (( PSym (q,( PSym (p,p)))),( PSym (q,( PSym (p,a))))) // (( PSym (p,a)),( PSym (p,p))) by Th3, Th32;

      then

       A2: (p,a) // (( PSym (q,( PSym (p,p)))),( PSym (q,( PSym (p,a))))) by Def1;

      (( PSym (q,p)),( PSym (r,p))) // (( PSym (r,( PSym (r,p)))),( PSym (r,( PSym (q,p))))) by Th32;

      then (( PSym (q,p)),( PSym (r,p))) // (p,( PSym (r,( PSym (q,p))))) by Th29;

      then

       A3: (p,( PSym (r,( PSym (q,p))))) // (( PSym (q,p)),( PSym (r,p))) by Th3;

      (( PSym (q,( PSym (r,p)))),p) // (( PSym (q,p)),( PSym (q,( PSym (q,( PSym (r,p))))))) by Th32;

      then (( PSym (q,( PSym (r,p)))),p) // (( PSym (q,p)),( PSym (r,p))) by Th29;

      then (( PSym (q,( PSym (r,p)))),p) // (p,( PSym (r,( PSym (q,p))))) by A3, Def1;

      then Mid (( PSym (q,( PSym (r,p)))),p,( PSym (r,( PSym (q,p)))));

      then ( PSym (p,( PSym (q,( PSym (r,p)))))) = ( PSym (r,( PSym (q,p)))) by Def4;

      then

       A4: ( PSym (p,( PSym (q,( PSym (r,p)))))) = ( PSym (r,( PSym (q,( PSym (p,p)))))) by Th28;

      (( PSym (r,( PSym (q,( PSym (p,a)))))),( PSym (r,( PSym (q,( PSym (p,p))))))) // (( PSym (q,( PSym (p,p)))),( PSym (q,( PSym (p,a))))) by Th3, Th32;

      then

       A5: (( PSym (r,( PSym (q,( PSym (p,a)))))),( PSym (r,( PSym (q,( PSym (p,p))))))) // (p,a) by A2, Def1;

      (( PSym (p,( PSym (q,( PSym (r,a)))))),( PSym (p,( PSym (q,( PSym (r,p))))))) // (( PSym (q,( PSym (r,p)))),( PSym (q,( PSym (r,a))))) by Th3, Th32;

      then (( PSym (p,( PSym (q,( PSym (r,a)))))),( PSym (p,( PSym (q,( PSym (r,p))))))) // (p,a) by A1, Def1;

      then (( PSym (p,( PSym (q,( PSym (r,a)))))),( PSym (p,( PSym (q,( PSym (r,p))))))) // (( PSym (r,( PSym (q,( PSym (p,a)))))),( PSym (p,( PSym (q,( PSym (r,p))))))) by A4, A5, Def1;

      hence thesis by Th4, Th7;

    end;

    theorem :: AFVECT0:40

    ex d st ( PSym (a,( PSym (b,( PSym (c,p)))))) = ( PSym (d,p))

    proof

      consider e such that

       A1: Mid (a,e,c) by Th19;

      consider d such that

       A2: Mid (b,e,d) by Th21;

      c = ( PSym (e,a)) by A1, Def4;

      

      then ( PSym (c,( PSym (d,p)))) = ( PSym (( PSym (e,a)),( PSym (( PSym (e,b)),p)))) by A2, Def4

      .= ( PSym (( PSym (e,a)),( PSym (e,( PSym (b,( PSym (e,p)))))))) by Th37

      .= ( PSym (e,( PSym (a,( PSym (e,( PSym (e,( PSym (b,( PSym (e,p)))))))))))) by Th37

      .= ( PSym (e,( PSym (a,( PSym (b,( PSym (e,p)))))))) by Th29

      .= ( PSym (e,( PSym (e,( PSym (b,( PSym (a,p)))))))) by Th39

      .= ( PSym (b,( PSym (a,p)))) by Th29;

      then ( PSym (d,p)) = ( PSym (c,( PSym (b,( PSym (a,p)))))) by Th29;

      hence thesis by Th39;

    end;

    theorem :: AFVECT0:41

    ex c st ( PSym (a,( PSym (c,p)))) = ( PSym (c,( PSym (b,p))))

    proof

      consider c such that

       A1: Mid (a,c,b) by Th19;

      ( PSym (b,p)) = ( PSym (( PSym (c,a)),p)) by A1, Def4

      .= ( PSym (c,( PSym (a,( PSym (c,p)))))) by Th37;

      then ( PSym (c,( PSym (b,p)))) = ( PSym (a,( PSym (c,p)))) by Th29;

      hence thesis;

    end;

    definition

      let AFV, o;

      let a, b;

      :: AFVECT0:def5

      func Padd (o,a,b) -> Element of AFV means

      : Def5: (o,a) // (b,it );

      correctness by Def1, Th5;

    end

    notation

      let AFV, o;

      let a;

      synonym Pcom (o,a) for PSym (o,a);

    end

    

     Lm1: ( Pcom (o,a)) = b iff (a,o) // (o,b) by Def4, Def3;

    definition

      let AFV, o;

      :: AFVECT0:def6

      func Padd (o) -> BinOp of the carrier of AFV means

      : Def6: for a, b holds (it . (a,b)) = ( Padd (o,a,b));

      existence

      proof

        deffunc F( Element of AFV, Element of AFV) = ( Padd (o,$1,$2));

        consider O be BinOp of the carrier of AFV such that

         A1: for a, b holds (O . (a,b)) = F(a,b) from BINOP_1:sch 4;

        take O;

        thus thesis by A1;

      end;

      uniqueness

      proof

        set X = the carrier of AFV;

        let o1,o2 be BinOp of the carrier of AFV such that

         A2: for a, b holds (o1 . (a,b)) = ( Padd (o,a,b)) and

         A3: for a, b holds (o2 . (a,b)) = ( Padd (o,a,b));

        for x be Element of [:X, X:] holds (o1 . x) = (o2 . x)

        proof

          let x be Element of [:X, X:];

          consider x1,x2 be Element of X such that

           A4: x = [x1, x2] by DOMAIN_1: 1;

          (o1 . x) = (o1 . (x1,x2)) by A4

          .= ( Padd (o,x1,x2)) by A2

          .= (o2 . (x1,x2)) by A3

          .= (o2 . x) by A4;

          hence thesis;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let AFV, o;

      :: AFVECT0:def7

      func Pcom (o) -> UnOp of the carrier of AFV means

      : Def7: for a holds (it . a) = ( Pcom (o,a));

      existence

      proof

        deffunc F( Element of AFV) = ( Pcom (o,$1));

        consider O be UnOp of the carrier of AFV such that

         A1: for a holds (O . a) = F(a) from FUNCT_2:sch 4;

        take O;

        thus thesis by A1;

      end;

      uniqueness

      proof

        set X = the carrier of AFV;

        let o1,o2 be UnOp of the carrier of AFV such that

         A2: for a holds (o1 . a) = ( Pcom (o,a)) and

         A3: for a holds (o2 . a) = ( Pcom (o,a));

        for x be Element of X holds (o1 . x) = (o2 . x)

        proof

          let x be Element of X;

          (o1 . x) = ( Pcom (o,x)) by A2

          .= (o2 . x) by A3;

          hence thesis;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let AFV, o;

      :: AFVECT0:def8

      func GroupVect (AFV,o) -> strict addLoopStr equals addLoopStr (# the carrier of AFV, ( Padd o), o #);

      correctness ;

    end

    registration

      let AFV, o;

      cluster ( GroupVect (AFV,o)) -> non empty;

      coherence ;

    end

    theorem :: AFVECT0:42

    the carrier of ( GroupVect (AFV,o)) = the carrier of AFV & the addF of ( GroupVect (AFV,o)) = ( Padd o) & ( 0. ( GroupVect (AFV,o))) = o;

    reserve a,b,c for Element of ( GroupVect (AFV,o));

    theorem :: AFVECT0:43

    for a,b be Element of ( GroupVect (AFV,o)), a9,b9 be Element of AFV st a = a9 & b = b9 holds (a + b) = (( Padd o) . (a9,b9));

    

     Lm2: (a + b) = (b + a)

    proof

      reconsider a9 = a, b9 = b as Element of AFV;

      reconsider c9 = (a + b) as Element of AFV;

      c9 = ( Padd (o,a9,b9)) by Def6;

      then (o,a9) // (b9,c9) by Def5;

      then (o,b9) // (a9,c9) by Def1;

      

      then c9 = ( Padd (o,b9,a9)) by Def5

      .= (b + a) by Def6;

      hence thesis;

    end;

    

     Lm3: ((a + b) + c) = (a + (b + c))

    proof

      reconsider a9 = a, b9 = b, c9 = c as Element of AFV;

      set p = (b + c), q = (a + b);

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

      reconsider x9 = (a + p), y9 = (q + c) as Element of AFV;

      consider x99 such that

       A1: (x9,p9) // (c9,x99) by Def1;

      x9 = ( Padd (o,a9,p9)) by Def6;

      then (o,a9) // (p9,x9) by Def5;

      then

       A2: (a9,o) // (x9,p9) by Th7;

      (c9,x99) // (x9,p9) by A1, Th3;

      then

       A3: (a9,o) // (c9,x99) by A2, Def1;

      q9 = ( Padd (o,a9,b9)) by Def6;

      then (o,a9) // (b9,q9) by Def5;

      then (o,b9) // (a9,q9) by Def1;

      then

       A4: (a9,q9) // (o,b9) by Th3;

      p9 = ( Padd (o,b9,c9)) by Def6;

      then (o,b9) // (c9,p9) by Def5;

      then (c9,p9) // (o,b9) by Th3;

      then (a9,q9) // (c9,p9) by A4, Def1;

      then

       A5: (q9,o) // (p9,x99) by A3, Def1;

      (x9,c9) // (p9,x99) by A1, Def1;

      then (q9,o) // (x9,c9) by A5, Def1;

      then (o,q9) // (c9,x9) by Th7;

      then

       A6: (c9,x9) // (o,q9) by Th3;

      y9 = ( Padd (o,q9,c9)) by Def6;

      then (o,q9) // (c9,y9) by Def5;

      then (c9,y9) // (o,q9) by Th3;

      then (c9,y9) // (c9,x9) by A6, Def1;

      hence thesis by Th4;

    end;

    

     Lm4: (a + ( 0. ( GroupVect (AFV,o)))) = a

    proof

      reconsider a9 = a as Element of AFV;

      reconsider x9 = (a + ( 0. ( GroupVect (AFV,o)))) as Element of AFV;

      x9 = ( Padd (o,a9,o)) by Def6;

      then (o,a9) // (o,x9) by Def5;

      hence thesis by Th4;

    end;

    

     Lm5: ( GroupVect (AFV,o)) is Abelian add-associative right_zeroed

    proof

      thus for a, b holds (a + b) = (b + a) by Lm2;

      thus for a, b, c holds ((a + b) + c) = (a + (b + c)) by Lm3;

      thus for a holds (a + ( 0. ( GroupVect (AFV,o)))) = a by Lm4;

    end;

    

     Lm6: ( GroupVect (AFV,o)) is right_complementable

    proof

      let s be Element of ( GroupVect (AFV,o));

      reconsider s9 = s as Element of AFV;

      reconsider t = (( Pcom o) . s9) as Element of ( GroupVect (AFV,o));

      take t;

      ( Pcom (o,o)) = o by Th28;

      then (o,s9) // (( Pcom (o,s9)),o) by Th32;

      then

       A1: ( Padd (o,s9,( Pcom (o,s9)))) = o by Def5;

      

      thus (s + t) = (( Padd o) . (s9,( Pcom (o,s9)))) by Def7

      .= ( 0. ( GroupVect (AFV,o))) by A1, Def6;

    end;

    registration

      let AFV, o;

      cluster ( GroupVect (AFV,o)) -> Abelian add-associative right_zeroed right_complementable;

      coherence by Lm5, Lm6;

    end

    theorem :: AFVECT0:44

    

     Th44: for a be Element of ( GroupVect (AFV,o)), a9 be Element of AFV st a = a9 holds ( - a) = (( Pcom o) . a9)

    proof

      let a be Element of ( GroupVect (AFV,o)), a9 be Element of AFV;

      assume

       A1: a = a9;

      reconsider aa = (( Pcom o) . a9) as Element of ( GroupVect (AFV,o));

      ( Pcom (o,o)) = o & (o,a9) // (( Pcom (o,a9)),( Pcom (o,o))) by Th28, Th32;

      then

       A2: ( Padd (o,a9,( Pcom (o,a9)))) = o by Def5;

      (a + aa) = (( Padd o) . (a,( Pcom (o,a9)))) by Def7

      .= ( 0. ( GroupVect (AFV,o))) by A1, A2, Def6;

      hence thesis by RLVECT_1:def 10;

    end;

    theorem :: AFVECT0:45

    ( 0. ( GroupVect (AFV,o))) = o;

    reserve a,b for Element of ( GroupVect (AFV,o));

    theorem :: AFVECT0:46

    

     Th46: for a holds ex b st (b + b) = a

    proof

      let a;

      reconsider a99 = a as Element of AFV;

      consider b9 be Element of AFV such that

       A1: (o,b9) // (b9,a99) by Def1;

      reconsider b = b9 as Element of ( GroupVect (AFV,o));

      a99 = ( Padd (o,b9,b9)) by A1, Def5

      .= (b + b) by Def6;

      hence thesis;

    end;

    registration

      let AFV, o;

      cluster ( GroupVect (AFV,o)) -> Two_Divisible;

      coherence

      proof

        for a holds ex b st (b + b) = a by Th46;

        hence thesis by TDGROUP:def 1;

      end;

    end

    reserve AFV for AffVect,

o for Element of AFV;

    theorem :: AFVECT0:47

    

     Th47: for a be Element of ( GroupVect (AFV,o)) st (a + a) = ( 0. ( GroupVect (AFV,o))) holds a = ( 0. ( GroupVect (AFV,o)))

    proof

      let a be Element of ( GroupVect (AFV,o)) such that

       A1: (a + a) = ( 0. ( GroupVect (AFV,o)));

      reconsider a99 = a as Element of AFV;

      o = ( Padd (o,a99,a99)) by A1, Def6;

      then

       A2: (o,a99) // (a99,o) by Def5;

      (o,o) // (o,o) by Th1;

      hence thesis by A2, TDGROUP: 16;

    end;

    registration

      let AFV, o;

      cluster ( GroupVect (AFV,o)) -> Fanoian;

      coherence

      proof

        for a be Element of ( GroupVect (AFV,o)) st (a + a) = ( 0. ( GroupVect (AFV,o))) holds a = ( 0. ( GroupVect (AFV,o))) by Th47;

        hence thesis by VECTSP_1:def 18;

      end;

    end

    registration

      cluster strict non trivial for Uniquely_Two_Divisible_Group;

      existence

      proof

        set X = G_Real ;

        X is non trivial by TDGROUP: 6;

        hence thesis;

      end;

    end

    definition

      mode Proper_Uniquely_Two_Divisible_Group is non trivial Uniquely_Two_Divisible_Group;

    end

    theorem :: AFVECT0:48

    ( GroupVect (AFV,o)) is Proper_Uniquely_Two_Divisible_Group;

    registration

      let AFV, o;

      cluster ( GroupVect (AFV,o)) -> non trivial;

      coherence ;

    end

    theorem :: AFVECT0:49

    

     Th49: for ADG be Proper_Uniquely_Two_Divisible_Group holds ( AV ADG) is AffVect

    proof

      let ADG be Proper_Uniquely_Two_Divisible_Group;

      ex a,b be Element of ADG st a <> b by STRUCT_0:def 10;

      hence thesis by TDGROUP: 17;

    end;

    registration

      let ADG be Proper_Uniquely_Two_Divisible_Group;

      cluster ( AV ADG) -> AffVect-like non trivial;

      coherence by Th49;

    end

    theorem :: AFVECT0:50

    

     Th50: for AFV be strict AffVect holds for o be Element of AFV holds AFV = ( AV ( GroupVect (AFV,o)))

    proof

      let AFV be strict AffVect;

      let o be Element of AFV;

      set X = ( GroupVect (AFV,o));

      now

        let x,y be object;

        set xy = [x, y];

         A1:

        now

          set V = the carrier of AFV;

          assume

           A2: xy in the CONGR of AFV;

          set VV = [:V, V:];

          (xy `2 ) = y;

          then

           A3: y in VV by A2, MCART_1: 10;

          then

           A4: y = [(y `1 ), (y `2 )] by MCART_1: 21;

          (xy `1 ) = x;

          then

           A5: x in VV by A2, MCART_1: 10;

          then

          reconsider x1 = (x `1 ), x2 = (x `2 ), y1 = (y `1 ), y2 = (y `2 ) as Element of AFV by A3, MCART_1: 10;

          reconsider x19 = x1, x29 = x2, y19 = y1, y29 = y2 as Element of X;

          

           A6: x = [(x `1 ), (x `2 )] by A5, MCART_1: 21;

          then

           A7: (x1,x2) // (y1,y2) by A2, A4, ANALOAF:def 2;

          (x19 # y29) = (x29 # y19)

          proof

            reconsider z1 = (x19 # y29), z2 = (x29 # y19) as Element of AFV;

            z1 = ( Padd (o,x1,y2)) by Def6;

            then (o,x1) // (y2,z1) by Def5;

            then (x1,o) // (z1,y2) by Th7;

            then

             A8: (o,x2) // (y1,z1) by A7, Th12;

            z2 = ( Padd (o,x2,y1)) by Def6;

            hence thesis by A8, Def5;

          end;

          hence [x, y] in ( CONGRD X) by A6, A4, TDGROUP:def 2;

        end;

        now

          set V = the carrier of X;

          assume

           A9: xy in ( CONGRD X);

          set VV = [:V, V:];

          (xy `2 ) = y;

          then

           A10: y in VV by A9, MCART_1: 10;

          then

           A11: y = [(y `1 ), (y `2 )] by MCART_1: 21;

          (xy `1 ) = x;

          then

           A12: x in VV by A9, MCART_1: 10;

          then

          reconsider x19 = (x `1 ), x29 = (x `2 ), y19 = (y `1 ), y29 = (y `2 ) as Element of X by A10, MCART_1: 10;

          set z19 = (x19 # y29), z29 = (x29 # y19);

          reconsider x1 = x19, x2 = x29, y1 = y19, y2 = y29 as Element of AFV;

          reconsider z1 = z19, z2 = z29 as Element of AFV;

          

           A13: z2 = ( Padd (o,x2,y1)) by Def6;

          z1 = ( Padd (o,x1,y2)) by Def6;

          then

           A14: (o,x1) // (y2,z1) by Def5;

          

           A15: x = [(x `1 ), (x `2 )] by A12, MCART_1: 21;

          then z19 = z29 by A9, A11, TDGROUP:def 2;

          then (o,x2) // (y1,z1) by A13, Def5;

          then (x1,x2) // (y1,y2) by A14, Th12;

          hence xy in the CONGR of AFV by A15, A11, ANALOAF:def 2;

        end;

        hence [x, y] in ( CONGRD X) iff [x, y] in the CONGR of AFV by A1;

      end;

      then the carrier of ( AV X) = the carrier of AFV & ( CONGRD X) = the CONGR of AFV by RELAT_1:def 2, TDGROUP: 4;

      hence thesis by TDGROUP: 4;

    end;

    theorem :: AFVECT0:51

    for AS be strict AffinStruct holds (AS is AffVect iff ex ADG be Proper_Uniquely_Two_Divisible_Group st AS = ( AV ADG))

    proof

      let AS be strict AffinStruct;

      now

        assume AS is AffVect;

        then

        reconsider AS9 = AS as AffVect;

        set o = the Element of AS9;

        take ADG = ( GroupVect (AS9,o));

        AS9 = ( AV ADG) by Th50;

        hence ex ADG be Proper_Uniquely_Two_Divisible_Group st AS = ( AV ADG);

      end;

      hence thesis;

    end;

    definition

      let X,Y be non empty addLoopStr;

      let f be Function of the carrier of X, the carrier of Y;

      :: AFVECT0:def9

      pred f is_Iso_of X,Y means f is one-to-one & ( rng f) = the carrier of Y & for a,b be Element of X holds (f . (a + b)) = ((f . a) + (f . b)) & (f . ( 0. X)) = ( 0. Y) & (f . ( - a)) = ( - (f . a));

    end

    definition

      let X,Y be non empty addLoopStr;

      :: AFVECT0:def10

      pred X,Y are_Iso means ex f be Function of the carrier of X, the carrier of Y st f is_Iso_of (X,Y);

    end

    reserve ADG for Proper_Uniquely_Two_Divisible_Group;

    reserve f for Function of the carrier of ADG, the carrier of ADG;

    theorem :: AFVECT0:52

    

     Th52: for o9 be Element of ADG, o be Element of ( AV ADG) st (for x be Element of ADG holds (f . x) = (o9 + x)) & o = o9 holds for a,b be Element of ADG holds (f . (a + b)) = (( Padd o) . ((f . a),(f . b))) & (f . ( 0. ADG)) = ( 0. ( GroupVect (( AV ADG),o))) & (f . ( - a)) = (( Pcom o) . (f . a))

    proof

      let o9 be Element of ADG, o be Element of ( AV ADG);

      assume that

       A1: for x be Element of ADG holds (f . x) = (o9 + x) and

       A2: o = o9;

      let a,b be Element of ADG;

      set a9 = (f . a), b9 = (f . b);

      

       A3: ( AV ADG) = AffinStruct (# the carrier of ADG, ( CONGRD ADG) #) by TDGROUP:def 3;

      then

      reconsider a99 = a9, b99 = b9 as Element of ( AV ADG);

      thus (f . (a + b)) = (( Padd o) . ((f . a),(f . b)))

      proof

        

         A4: (( Padd o) . ((f . a),(f . b))) = ( Padd (o,a99,b99)) by Def6;

        then

        reconsider c99 = (( Padd o) . ((f . a),(f . b))) as Element of ( AV ADG);

        reconsider c9 = c99 as Element of ADG by A3;

        (o,a99) // (b99,c99) by A4, Def5;

        then [ [o9, a9], [b9, c9]] in ( CONGRD ADG) by A2, A3, ANALOAF:def 2;

        then

         A5: (o9 + c9) = (a9 + b9) by TDGROUP:def 2;

        a9 = (o9 + a) & b9 = (o9 + b) by A1;

        

        then (o9 + c9) = (o9 + ((a + o9) + b)) by A5, RLVECT_1:def 3

        .= (o9 + (o9 + (a + b))) by RLVECT_1:def 3;

        

        then c9 = (o9 + (a + b)) by RLVECT_1: 8

        .= (f . (a + b)) by A1;

        hence thesis;

      end;

      (f . ( 0. ADG)) = (o9 + ( 0. ADG)) by A1

      .= ( 0. ( GroupVect (( AV ADG),o))) by A2, RLVECT_1: 4;

      hence (f . ( 0. ADG)) = ( 0. ( GroupVect (( AV ADG),o)));

      thus (f . ( - a)) = (( Pcom o) . (f . a))

      proof

        

         A6: (( Pcom o) . (f . a)) = ( Pcom (o,a99)) by Def7;

        then

        reconsider c99 = (( Pcom o) . (f . a)) as Element of ( AV ADG);

        reconsider c9 = c99 as Element of ADG by A3;

        (a99,o) // (o,c99) by A6, Lm1;

        then [ [a9, o9], [o9, c9]] in ( CONGRD ADG) by A2, A3, ANALOAF:def 2;

        then (a9 + c9) = (o9 + o9) by TDGROUP:def 2;

        

        then

         A7: (o9 + o9) = ((o9 + a) + c9) by A1

        .= (o9 + (a + c9)) by RLVECT_1:def 3;

        (f . ( - a)) = (o9 + ( - a)) by A1

        .= ((c9 + a) + ( - a)) by A7, RLVECT_1: 8

        .= (c9 + (a + ( - a))) by RLVECT_1:def 3

        .= (c9 + ( 0. ADG)) by RLVECT_1: 5

        .= c9 by RLVECT_1: 4;

        hence thesis;

      end;

    end;

    theorem :: AFVECT0:53

    

     Th53: for o9 be Element of ADG st (for b be Element of ADG holds (f . b) = (o9 + b)) holds f is one-to-one

    proof

      let o9 be Element of ADG such that

       A1: for b be Element of ADG holds (f . b) = (o9 + b);

      now

        let x1,x2 be object such that

         A2: x1 in ( dom f) & x2 in ( dom f) and

         A3: (f . x1) = (f . x2);

        reconsider x19 = x1, x29 = x2 as Element of ADG by A2, FUNCT_2:def 1;

        (o9 + x29) = (f . x19) by A1, A3

        .= (o9 + x19) by A1;

        hence x1 = x2 by RLVECT_1: 8;

      end;

      hence thesis by FUNCT_1:def 4;

    end;

    theorem :: AFVECT0:54

    

     Th54: for o9 be Element of ADG, o be Element of ( AV ADG) st (for b be Element of ADG holds (f . b) = (o9 + b)) holds ( rng f) = the carrier of ( GroupVect (( AV ADG),o))

    proof

      set X = the carrier of ADG;

      

       A1: X = ( dom f) by FUNCT_2:def 1;

      let o9 be Element of ADG, o be Element of ( AV ADG) such that

       A2: for b be Element of ADG holds (f . b) = (o9 + b);

      now

        let y be object;

        assume y in X;

        then

        reconsider y9 = y as Element of X;

        set x9 = (y9 - o9);

        (f . x9) = (o9 + (( - o9) + y9)) by A2

        .= ((o9 + ( - o9)) + y9) by RLVECT_1:def 3

        .= (y9 + ( 0. ADG)) by RLVECT_1: 5

        .= y by RLVECT_1: 4;

        hence y in ( rng f) by A1, FUNCT_1:def 3;

      end;

      then

       A3: X c= ( rng f) by TARSKI:def 3;

      ( rng f) c= X & X = the carrier of ( GroupVect (( AV ADG),o)) by RELAT_1:def 19, TDGROUP: 4;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: AFVECT0:55

    for ADG be Proper_Uniquely_Two_Divisible_Group, o9 be Element of ADG, o be Element of ( AV ADG) st o = o9 holds (ADG,( GroupVect (( AV ADG),o))) are_Iso

    proof

      let ADG be Proper_Uniquely_Two_Divisible_Group, o9 be Element of ADG, o be Element of ( AV ADG) such that

       A1: o = o9;

      set AS = ( AV ADG);

      set X = the carrier of ADG, Z = ( GroupVect (AS,o));

      set T = the carrier of ( GroupVect (AS,o));

      deffunc F( Element of X) = (o9 + $1);

      consider g be UnOp of X such that

       A2: for a be Element of X holds (g . a) = F(a) from FUNCT_2:sch 4;

      X = T by TDGROUP: 4;

      then

      reconsider f = g as Function of X, T;

       A3:

      now

        let a,b be Element of ADG;

        reconsider fa = (f . a) as Element of ( AV ADG);

        thus (f . (a + b)) = ((f . a) + (f . b)) by A1, A2, Th52;

        thus (f . ( 0. ADG)) = ( 0. Z) by A1, A2, Th52;

        

        thus (f . ( - a)) = (( Pcom o) . fa) by A1, A2, Th52

        .= ( - (f . a)) by Th44;

      end;

      f is one-to-one & ( rng f) = T by A2, Th53, Th54;

      then f is_Iso_of (ADG,Z) by A3;

      hence thesis;

    end;