midsp_2.miz



    begin

    reserve G for non empty addLoopStr;

    reserve x for Element of G;

    reserve M for non empty MidStr;

    reserve p,q,r for Point of M;

    reserve w for Function of [:the carrier of M, the carrier of M:], the carrier of G;

    definition

      let G, x;

      :: MIDSP_2:def1

      func Double x -> Element of G equals (x + x);

      coherence ;

    end

    definition

      let M, G, w;

      :: MIDSP_2:def2

      attr w is associating means (p @ q) = r iff (w . (p,r)) = (w . (r,q));

    end

    theorem :: MIDSP_2:1

    

     Th1: w is associating implies (p @ p) = p

    proof

      

       A1: (w . (p,p)) = (w . (p,p));

      assume w is associating;

      hence thesis by A1;

    end;

    reserve S for non empty set;

    reserve a,b,b9,c,c9,d for Element of S;

    reserve w for Function of [:S, S:], the carrier of G;

    definition

      let S, G, w;

      :: MIDSP_2:def3

      pred w is_atlas_of S,G means (for a, x holds ex b st (w . (a,b)) = x) & (for a, b, c holds (w . (a,b)) = (w . (a,c)) implies b = c) & for a, b, c holds ((w . (a,b)) + (w . (b,c))) = (w . (a,c));

    end

    definition

      let S, G, w, a, x;

      assume

       A1: w is_atlas_of (S,G);

      :: MIDSP_2:def4

      func (a,x) . w -> Element of S means

      : Def4: (w . (a,it )) = x;

      existence by A1;

      uniqueness by A1;

    end

    reserve G for add-associative right_zeroed right_complementable non empty addLoopStr;

    reserve x for Element of G;

    reserve w for Function of [:S, S:], the carrier of G;

    theorem :: MIDSP_2:2

    

     Th2: w is_atlas_of (S,G) implies (w . (a,a)) = ( 0. G)

    proof

      assume w is_atlas_of (S,G);

      then ((w . (a,a)) + (w . (a,a))) = (w . (a,a));

      hence thesis by RLVECT_1: 9;

    end;

    theorem :: MIDSP_2:3

    

     Th3: w is_atlas_of (S,G) & (w . (a,b)) = ( 0. G) implies a = b

    proof

      assume that

       A1: w is_atlas_of (S,G) and

       A2: (w . (a,b)) = ( 0. G);

      (w . (a,b)) = (w . (a,a)) by A1, A2, Th2;

      hence thesis by A1;

    end;

    theorem :: MIDSP_2:4

    

     Th4: w is_atlas_of (S,G) implies (w . (a,b)) = ( - (w . (b,a)))

    proof

      assume

       A1: w is_atlas_of (S,G);

      

      then ((w . (b,a)) + (w . (a,b))) = (w . (b,b))

      .= ( 0. G) by A1, Th2;

      then ( - (w . (b,a))) = ( - ( - (w . (a,b)))) by RLVECT_1: 6;

      hence thesis by RLVECT_1: 17;

    end;

    theorem :: MIDSP_2:5

    

     Th5: w is_atlas_of (S,G) & (w . (a,b)) = (w . (c,d)) implies (w . (b,a)) = (w . (d,c))

    proof

      assume that

       A1: w is_atlas_of (S,G) and

       A2: (w . (a,b)) = (w . (c,d));

      

      thus (w . (b,a)) = ( - (w . (c,d))) by A1, A2, Th4

      .= (w . (d,c)) by A1, Th4;

    end;

    theorem :: MIDSP_2:6

    

     Th6: w is_atlas_of (S,G) implies for b, x holds ex a st (w . (a,b)) = x

    proof

      assume

       A1: w is_atlas_of (S,G);

      let b, x;

      consider a such that

       A2: (w . (b,a)) = ( - x) by A1;

      take a;

      (w . (a,b)) = ( - ( - x)) by A1, A2, Th4

      .= x by RLVECT_1: 17;

      hence thesis;

    end;

    theorem :: MIDSP_2:7

    

     Th7: w is_atlas_of (S,G) & (w . (b,a)) = (w . (c,a)) implies b = c

    proof

      assume that

       A1: w is_atlas_of (S,G) and

       A2: (w . (b,a)) = (w . (c,a));

      (w . (a,b)) = (w . (a,c)) by A1, A2, Th5;

      hence thesis by A1;

    end;

    theorem :: MIDSP_2:8

    

     Th8: for w be Function of [:the carrier of M, the carrier of M:], the carrier of G holds w is_atlas_of (the carrier of M,G) & w is associating implies (p @ q) = (q @ p)

    proof

      let w be Function of [:the carrier of M, the carrier of M:], the carrier of G;

      assume that

       A1: w is_atlas_of (the carrier of M,G) and

       A2: w is associating;

      set r = (p @ q);

      (w . (p,r)) = (w . (r,q)) by A2;

      then (w . (r,p)) = (w . (q,r)) by A1, Th5;

      hence thesis by A2;

    end;

    theorem :: MIDSP_2:9

    

     Th9: for w be Function of [:the carrier of M, the carrier of M:], the carrier of G holds w is_atlas_of (the carrier of M,G) & w is associating implies ex r st (r @ p) = q

    proof

      let w be Function of [:the carrier of M, the carrier of M:], the carrier of G;

      assume that

       A1: w is_atlas_of (the carrier of M,G) and

       A2: w is associating;

      consider r such that

       A3: (w . (r,q)) = (w . (q,p)) by A1, Th6;

      take r;

      thus thesis by A2, A3;

    end;

    reserve G for add-associative right_zeroed right_complementable Abelian non empty addLoopStr;

    reserve x for Element of G;

    theorem :: MIDSP_2:10

    

     Th10: for G be add-associative Abelian non empty addLoopStr, x,y,z,t be Element of G holds ((x + y) + (z + t)) = ((x + z) + (y + t))

    proof

      let G be add-associative Abelian non empty addLoopStr, x,y,z,t be Element of G;

      

      thus ((x + y) + (z + t)) = (x + (y + (z + t))) by RLVECT_1:def 3

      .= (x + (z + (y + t))) by RLVECT_1:def 3

      .= ((x + z) + (y + t)) by RLVECT_1:def 3;

    end;

    theorem :: MIDSP_2:11

    for G be add-associative Abelian non empty addLoopStr, x,y be Element of G holds ( Double (x + y)) = (( Double x) + ( Double y)) by Th10;

    theorem :: MIDSP_2:12

    

     Th12: ( Double ( - x)) = ( - ( Double x))

    proof

      ( 0. G) = ( Double ( 0. G)) by RLVECT_1:def 4

      .= ( Double (x + ( - x))) by RLVECT_1:def 10

      .= (( Double x) + ( Double ( - x))) by Th10;

      hence thesis by RLVECT_1: 6;

    end;

    theorem :: MIDSP_2:13

    

     Th13: for w be Function of [:the carrier of M, the carrier of M:], the carrier of G holds w is_atlas_of (the carrier of M,G) & w is associating implies for a,b,c,d be Point of M holds ((a @ b) = (c @ d) iff (w . (a,d)) = (w . (c,b)))

    proof

      let w be Function of [:the carrier of M, the carrier of M:], the carrier of G;

      assume that

       A1: w is_atlas_of (the carrier of M,G) and

       A2: w is associating;

      let a,b,c,d be Point of M;

      thus (a @ b) = (c @ d) implies (w . (a,d)) = (w . (c,b))

      proof

        set p = (a @ b);

        assume (a @ b) = (c @ d);

        then

         A3: (w . (c,p)) = (w . (p,d)) by A2;

        (w . (a,p)) = (w . (p,b)) by A2;

        

        hence (w . (a,d)) = ((w . (c,p)) + (w . (p,b))) by A1, A3

        .= (w . (c,b)) by A1;

      end;

      thus (w . (a,d)) = (w . (c,b)) implies (a @ b) = (c @ d)

      proof

        set p = (a @ b);

        assume

         A4: (w . (a,d)) = (w . (c,b));

        ((w . (p,b)) + (w . (p,d))) = ((w . (a,p)) + (w . (p,d))) by A2

        .= (w . (a,d)) by A1

        .= ((w . (p,b)) + (w . (c,p))) by A1, A4;

        then (w . (p,d)) = (w . (c,p)) by RLVECT_1: 8;

        hence thesis by A2;

      end;

    end;

    reserve w for Function of [:S, S:], the carrier of G;

    theorem :: MIDSP_2:14

    

     Th14: w is_atlas_of (S,G) implies for a, b, b9, c, c9 holds (w . (a,b)) = (w . (b,c)) & (w . (a,b9)) = (w . (b9,c9)) implies (w . (c,c9)) = ( Double (w . (b,b9)))

    proof

      assume

       A1: w is_atlas_of (S,G);

      let a, b, b9, c, c9;

      assume

       A2: (w . (a,b)) = (w . (b,c)) & (w . (a,b9)) = (w . (b9,c9));

      

      thus (w . (c,c9)) = ((w . (c,b9)) + (w . (b9,c9))) by A1

      .= (((w . (c,a)) + (w . (a,b9))) + (w . (b9,c9))) by A1

      .= ((((w . (c,b)) + (w . (b,a))) + (w . (a,b9))) + (w . (b9,c9))) by A1

      .= ((( Double (w . (b,a))) + (w . (a,b9))) + (w . (a,b9))) by A1, A2, Th5

      .= (( Double (w . (b,a))) + ( Double (w . (a,b9)))) by RLVECT_1:def 3

      .= ( Double ((w . (b,a)) + (w . (a,b9)))) by Th10

      .= ( Double (w . (b,b9))) by A1;

    end;

    reserve M for MidSp;

    reserve p,q,r,s for Point of M;

    registration

      let M;

      cluster ( vectgroup M) -> Abelian add-associative right_zeroed right_complementable;

      coherence by MIDSP_1: 56;

    end

    theorem :: MIDSP_2:15

    

     Th15: (for a be set holds a is Element of ( vectgroup M) iff a is Vector of M) & ( 0. ( vectgroup M)) = ( ID M) & for a,b be Element of ( vectgroup M), x,y be Vector of M st a = x & b = y holds (a + b) = (x + y)

    proof

      set G = ( vectgroup M);

      thus for a be set holds a is Element of G iff a is Vector of M

      proof

        let a be set;

        a is Element of G iff a is Element of ( setvect M) by MIDSP_1: 53;

        hence thesis by MIDSP_1: 48;

      end;

      

      thus ( 0. G) = ( zerovect M) by MIDSP_1: 55

      .= ( ID M) by MIDSP_1:def 16;

      thus for a,b be Element of G, x,y be Vector of M st a = x & b = y holds (a + b) = (x + y)

      proof

        let a,b be Element of G, x,y be Vector of M such that

         A1: a = x & b = y;

        reconsider xx = x, yy = y as Element of ( setvect M) by MIDSP_1: 48;

        

        thus (a + b) = (the addF of G . (a,b)) by RLVECT_1: 2

        .= (( addvect M) . (xx,yy)) by A1, MIDSP_1: 54

        .= (xx + yy) by MIDSP_1:def 14

        .= (x + y) by MIDSP_1:def 13;

      end;

    end;

    

     Lm1: (for a be Element of ( vectgroup M) holds ex x be Element of ( vectgroup M) st ( Double x) = a) & for a be Element of ( vectgroup M) holds ( Double a) = ( 0. ( vectgroup M)) implies a = ( 0. ( vectgroup M))

    proof

      set G = ( vectgroup M);

      set p = the Point of M;

      thus for a be Element of G holds ex x be Element of G st ( Double x) = a

      proof

        set p = the Point of M;

        let a be Element of G;

        reconsider aa = a as Vector of M by Th15;

        consider q be Point of M such that

         A1: aa = ( vect (p,q)) by MIDSP_1: 35;

        set xx = ( vect (p,(p @ q)));

        reconsider x = xx as Element of G by Th15;

        take x;

        (xx + xx) = aa by A1, MIDSP_1: 42;

        hence thesis by Th15;

      end;

      let a be Element of G;

      reconsider aa = a as Vector of M by Th15;

      consider q be Point of M such that

       A2: aa = ( vect (p,q)) by MIDSP_1: 35;

      consider r be Point of M such that

       A3: aa = ( vect (q,r)) by MIDSP_1: 35;

      assume ( Double a) = ( 0. G);

      

      then (aa + aa) = ( 0. G) by Th15

      .= ( ID M) by Th15;

      then (( vect (p,q)) + ( vect (q,r))) = ( vect (p,p)) by A2, A3, MIDSP_1: 38;

      then ( vect (p,r)) = ( vect (p,p)) by MIDSP_1: 40;

      then ( vect (p,q)) = ( vect (q,p)) by A2, A3, MIDSP_1: 39;

      then

       A4: (p @ p) = (q @ q) by MIDSP_1: 37;

      p = (p @ p) by MIDSP_1:def 3

      .= q by A4, MIDSP_1:def 3;

      

      hence a = ( ID M) by A2, MIDSP_1: 38

      .= ( 0. G) by Th15;

    end;

    definition

      let IT be non empty addLoopStr;

      :: MIDSP_2:def5

      attr IT is midpoint_operator means

      : Def5: (for a be Element of IT holds ex x be Element of IT st ( Double x) = a) & for a be Element of IT holds ( Double a) = ( 0. IT) implies a = ( 0. IT);

    end

    registration

      cluster midpoint_operator -> Fanoian for non empty addLoopStr;

      coherence

      proof

        let L be non empty addLoopStr;

        assume

         A1: L is midpoint_operator;

        let a be Element of L;

        assume (a + a) = ( 0. L);

        then ( Double a) = ( 0. L);

        hence thesis by A1;

      end;

    end

    registration

      cluster strict midpoint_operator add-associative right_zeroed right_complementable Abelian for non empty addLoopStr;

      existence

      proof

        set M = the MidSp;

        set G = ( vectgroup M);

        (for a be Element of G holds ex x be Element of G st ( Double x) = a) & for a be Element of G holds ( Double a) = ( 0. G) implies a = ( 0. G) by Lm1;

        then G is midpoint_operator;

        hence thesis;

      end;

    end

    reserve G for midpoint_operator add-associative right_zeroed right_complementable Abelian non empty addLoopStr;

    reserve x,y for Element of G;

    theorem :: MIDSP_2:16

    

     Th16: for G be Fanoian add-associative right_zeroed right_complementable non empty addLoopStr, x be Element of G holds x = ( - x) implies x = ( 0. G)

    proof

      let G be Fanoian add-associative right_zeroed right_complementable non empty addLoopStr, x be Element of G;

      

       A1: (( - x) + x) = ( 0. G) by RLVECT_1: 5;

      assume x = ( - x);

      hence thesis by A1, VECTSP_1:def 18;

    end;

    theorem :: MIDSP_2:17

    

     Th17: for G be Fanoian add-associative right_zeroed right_complementable Abelian non empty addLoopStr, x,y be Element of G holds ( Double x) = ( Double y) implies x = y

    proof

      let G be Fanoian add-associative right_zeroed right_complementable Abelian non empty addLoopStr, x,y be Element of G;

      assume ( Double x) = ( Double y);

      

      then ( 0. G) = ((x + x) + ( - (y + y))) by RLVECT_1:def 10

      .= ((x + x) + (( - y) + ( - y))) by RLVECT_1: 31

      .= (x + (x + (( - y) + ( - y)))) by RLVECT_1:def 3

      .= (x + ((x + ( - y)) + ( - y))) by RLVECT_1:def 3

      .= ((x + ( - y)) + (x + ( - y))) by RLVECT_1:def 3;

      then (( - y) + x) = ( 0. G) by VECTSP_1:def 18;

      

      hence x = ( - ( - y)) by RLVECT_1: 6

      .= y by RLVECT_1: 17;

    end;

    definition

      let G be midpoint_operator add-associative right_zeroed right_complementable Abelian non empty addLoopStr, x be Element of G;

      :: MIDSP_2:def6

      func Half x -> Element of G means

      : Def6: ( Double it ) = x;

      existence by Def5;

      uniqueness by Th17;

    end

    theorem :: MIDSP_2:18

    ( Half ( 0. G)) = ( 0. G) & ( Half (x + y)) = (( Half x) + ( Half y)) & (( Half x) = ( Half y) implies x = y) & ( Half ( Double x)) = x

    proof

      ( Double ( 0. G)) = ( 0. G) by RLVECT_1:def 4;

      hence ( Half ( 0. G)) = ( 0. G) by Def6;

      ( Double (( Half x) + ( Half y))) = (( Double ( Half x)) + ( Double ( Half y))) by Th10

      .= (x + ( Double ( Half y))) by Def6

      .= (x + y) by Def6;

      hence ( Half (x + y)) = (( Half x) + ( Half y)) by Def6;

      thus ( Half x) = ( Half y) implies x = y

      proof

        assume ( Half x) = ( Half y);

        

        hence x = ( Double ( Half y)) by Def6

        .= y by Def6;

      end;

      thus thesis by Def6;

    end;

    theorem :: MIDSP_2:19

    

     Th19: for M be non empty MidStr, w be Function of [:the carrier of M, the carrier of M:], the carrier of G holds w is_atlas_of (the carrier of M,G) & w is associating implies for a,b,c,d be Point of M holds ((a @ b) @ (c @ d)) = ((a @ c) @ (b @ d))

    proof

      let M be non empty MidStr, w be Function of [:the carrier of M, the carrier of M:], the carrier of G;

      assume that

       A1: w is_atlas_of (the carrier of M,G) and

       A2: w is associating;

      let a,b,c,d be Point of M;

      

       A3: (w . (b,(a @ b))) = (w . (b,(b @ a))) by A1, A2, Th8

      .= (w . ((b @ a),a)) by A2

      .= (w . ((a @ b),a)) by A1, A2, Th8;

      set p = ((a @ b) @ (c @ d));

      

       A4: (w . (c,(c @ d))) = (w . ((c @ d),d)) by A2;

      

       A5: (w . (b,(b @ d))) = (w . ((b @ d),d)) by A2;

      (w . (c,(a @ c))) = (w . (c,(c @ a))) by A1, A2, Th8

      .= (w . ((c @ a),a)) by A2

      .= (w . ((a @ c),a)) by A1, A2, Th8;

      

      then ( Double (w . ((a @ c),(c @ d)))) = (w . (a,d)) by A1, A4, Th14

      .= ( - (w . (d,a))) by A1, Th4

      .= ( - ( Double (w . ((b @ d),(a @ b))))) by A1, A5, A3, Th14

      .= ( Double ( - (w . ((b @ d),(a @ b))))) by Th12

      .= ( Double (w . ((a @ b),(b @ d)))) by A1, Th4;

      then (w . ((a @ c),(c @ d))) = (w . ((a @ b),(b @ d))) by Th17;

      

      then

       A6: ((w . ((a @ c),p)) + (w . (p,(c @ d)))) = (w . ((a @ b),(b @ d))) by A1

      .= ((w . (p,(b @ d))) + (w . ((a @ b),p))) by A1;

      (w . ((a @ b),p)) = (w . (p,(c @ d))) by A2;

      then (w . ((a @ c),p)) = (w . (p,(b @ d))) by A6, RLVECT_1: 8;

      hence thesis by A2;

    end;

    theorem :: MIDSP_2:20

    

     Th20: for M be non empty MidStr, w be Function of [:the carrier of M, the carrier of M:], the carrier of G holds w is_atlas_of (the carrier of M,G) & w is associating implies M is MidSp

    proof

      let M be non empty MidStr, w be Function of [:the carrier of M, the carrier of M:], the carrier of G;

      assume w is_atlas_of (the carrier of M,G) & w is associating;

      then for a,b,c,d be Point of M holds (a @ a) = a & (a @ b) = (b @ a) & ((a @ b) @ (c @ d)) = ((a @ c) @ (b @ d)) & ex x be Point of M st (x @ a) = b by Th1, Th8, Th9, Th19;

      hence thesis by MIDSP_1:def 3;

    end;

    reserve x,y for Element of ( vectgroup M);

    registration

      let M;

      cluster ( vectgroup M) -> midpoint_operator;

      coherence by Lm1;

    end

    definition

      let M, p, q;

      :: MIDSP_2:def7

      func vector (p,q) -> Element of ( vectgroup M) equals ( vect (p,q));

      coherence by Th15;

    end

    definition

      let M;

      :: MIDSP_2:def8

      func vect (M) -> Function of [:the carrier of M, the carrier of M:], the carrier of ( vectgroup M) means

      : Def8: (it . (p,q)) = ( vect (p,q));

      existence

      proof

        deffunc F( Point of M, Point of M) = ( vector ($1,$2));

        consider f be Function of [:the carrier of M, the carrier of M:], the carrier of ( vectgroup M) such that

         A1: (f . (p,q)) = F(p,q) from BINOP_1:sch 4;

        take f;

        (f . (p,q)) = ( vect (p,q))

        proof

          

          thus (f . (p,q)) = ( vector (p,q)) by A1

          .= ( vect (p,q));

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Function of [:the carrier of M, the carrier of M:], the carrier of ( vectgroup M);

        assume that

         A2: (f . (p,q)) = ( vect (p,q)) and

         A3: (g . (p,q)) = ( vect (p,q));

        (f . (p,q)) = (g . (p,q))

        proof

          

          thus (f . (p,q)) = ( vect (p,q)) by A2

          .= (g . (p,q)) by A3;

        end;

        hence f = g by BINOP_1: 2;

      end;

    end

    theorem :: MIDSP_2:21

    

     Th21: ( vect M) is_atlas_of (the carrier of M,( vectgroup M))

    proof

      set w = ( vect M);

      

       A1: ex q st (w . (p,q)) = x

      proof

        reconsider xx = x as Vector of M by Th15;

        consider q such that

         A2: xx = ( vect (p,q)) by MIDSP_1: 35;

        take q;

        thus thesis by A2, Def8;

      end;

      

       A3: (w . (p,q)) = (w . (p,r)) implies q = r

      proof

        assume (w . (p,q)) = (w . (p,r));

        

        then ( vect (p,q)) = (w . (p,r)) by Def8

        .= ( vect (p,r)) by Def8;

        hence thesis by MIDSP_1: 39;

      end;

      ((w . (p,q)) + (w . (q,r))) = (w . (p,r))

      proof

        (w . (p,q)) = ( vect (p,q)) & (w . (q,r)) = ( vect (q,r)) by Def8;

        

        hence ((w . (p,q)) + (w . (q,r))) = (( vect (p,q)) + ( vect (q,r))) by Th15

        .= ( vect (p,r)) by MIDSP_1: 40

        .= (w . (p,r)) by Def8;

      end;

      hence thesis by A1, A3;

    end;

    theorem :: MIDSP_2:22

    

     Th22: ( vect (p,q)) = ( vect (r,s)) iff (p @ s) = (q @ r)

    proof

      thus ( vect (p,q)) = ( vect (r,s)) implies (p @ s) = (q @ r) by MIDSP_1: 37;

      thus (p @ s) = (q @ r) implies ( vect (p,q)) = ( vect (r,s))

      proof

        assume (p @ s) = (q @ r);

        then (p,q) @@ (r,s) by MIDSP_1:def 4;

        then [p, q] ## [r, s] by MIDSP_1: 19;

        hence thesis by MIDSP_1: 36;

      end;

    end;

    theorem :: MIDSP_2:23

    

     Th23: (p @ q) = r iff ( vect (p,r)) = ( vect (r,q))

    proof

      (p @ q) = r iff (p @ q) = (r @ r) by MIDSP_1:def 3;

      hence thesis by Th22;

    end;

    ::$Canceled

    

     Lm2: ( vect M) is associating

    proof

      let p, q, r;

      set w = ( vect M);

      (w . (p,r)) = ( vect (p,r)) & (w . (r,q)) = ( vect (r,q)) by Def8;

      hence thesis by Th23;

    end;

    registration

      let M;

      cluster ( vect M) -> associating;

      coherence by Lm2;

    end

    reserve w for Function of [:S, S:], the carrier of G;

    definition

      let S, G, w;

      assume

       A1: w is_atlas_of (S,G);

      :: MIDSP_2:def9

      func @ (w) -> BinOp of S means

      : Def9: (w . (a,(it . (a,b)))) = (w . ((it . (a,b)),b));

      existence

      proof

        defpred P[ Element of S, Element of S, Element of S] means (w . ($1,$3)) = (w . ($3,$2));

        

         A2: for a, b holds ex c st P[a, b, c]

        proof

          let a, b;

          set x = ( Half (w . (a,b)));

          consider c such that

           A3: (w . (a,c)) = x by A1;

          take c;

          (x + x) = ( Double x)

          .= (w . (a,b)) by Def6

          .= (x + (w . (c,b))) by A1, A3;

          hence thesis by A3, RLVECT_1: 8;

        end;

        consider o be BinOp of S such that

         A4: for a, b holds P[a, b, (o . (a,b))] from BINOP_1:sch 3( A2);

        take o;

        thus thesis by A4;

      end;

      uniqueness

      proof

        defpred P[ Element of S, Element of S, Element of S] means (w . ($1,$3)) = (w . ($3,$2));

        

         A5: for a, b, c, c9 st P[a, b, c] & P[a, b, c9] holds c = c9

        proof

          let a, b, c, c9 such that

           A6: P[a, b, c] & P[a, b, c9];

          (w . (c,c9)) = ((w . (c,a)) + (w . (a,c9))) by A1

          .= ((w . (c9,b)) + (w . (b,c))) by A1, A6, Th5

          .= (w . (c9,c)) by A1

          .= ( - (w . (c,c9))) by A1, Th4;

          then (w . (c,c9)) = ( 0. G) by Th16;

          hence thesis by A1, Th3;

        end;

        let f,g be BinOp of S such that

         A7: (for a, b holds (w . (a,(f . (a,b)))) = (w . ((f . (a,b)),b))) & for a, b holds (w . (a,(g . (a,b)))) = (w . ((g . (a,b)),b));

        for a, b holds (f . (a,b)) = (g . (a,b))

        proof

          let a, b;

          (w . (a,(f . (a,b)))) = (w . ((f . (a,b)),b)) & (w . (a,(g . (a,b)))) = (w . ((g . (a,b)),b)) by A7;

          hence thesis by A5;

        end;

        hence f = g by BINOP_1: 2;

      end;

    end

    theorem :: MIDSP_2:25

    

     Th24: w is_atlas_of (S,G) implies for a, b, c holds (( @ w) . (a,b)) = c iff (w . (a,c)) = (w . (c,b))

    proof

      assume

       A1: w is_atlas_of (S,G);

      let a, b, c;

      thus (( @ w) . (a,b)) = c implies (w . (a,c)) = (w . (c,b)) by A1, Def9;

      thus (w . (a,c)) = (w . (c,b)) implies (( @ w) . (a,b)) = c

      proof

        defpred P[ Element of S, Element of S, Element of S] means (w . ($1,$3)) = (w . ($3,$2));

        assume

         A2: (w . (a,c)) = (w . (c,b));

        

         A3: for a, b, c, c9 st P[a, b, c] & P[a, b, c9] holds c = c9

        proof

          let a, b, c, c9 such that

           A4: P[a, b, c] & P[a, b, c9];

          (w . (c,c9)) = ((w . (c,a)) + (w . (a,c9))) by A1

          .= ((w . (c9,b)) + (w . (b,c))) by A1, A4, Th5

          .= (w . (c9,c)) by A1

          .= ( - (w . (c,c9))) by A1, Th4;

          then (w . (c,c9)) = ( 0. G) by Th16;

          hence thesis by A1, Th3;

        end;

        set c9 = (( @ w) . (a,b));

         P[a, b, c9] by A1, Def9;

        hence thesis by A2, A3;

      end;

    end;

    registration

      let D be non empty set, M be BinOp of D;

      cluster MidStr (# D, M #) -> non empty;

      coherence ;

    end

    reserve a,b,c for Point of MidStr (# S, ( @ w) #);

    definition

      let S, G, w;

      :: MIDSP_2:def10

      func Atlas (w) -> Function of [:the carrier of MidStr (# S, ( @ w) #), the carrier of MidStr (# S, ( @ w) #):], the carrier of G equals w;

      coherence ;

    end

    theorem :: MIDSP_2:26

    

     Th25: w is_atlas_of (S,G) implies ( Atlas w) is associating

    proof

      assume

       A1: w is_atlas_of (S,G);

      for a, b, c holds (a @ b) = c iff (( Atlas w) . (a,c)) = (( Atlas w) . (c,b))

      proof

        let a, b, c;

        (( @ w) . (a,b)) = c iff (w . (a,c)) = (w . (c,b)) by A1, Th24;

        hence thesis by MIDSP_1:def 1;

      end;

      hence thesis;

    end;

    definition

      let S, G, w;

      assume

       A1: w is_atlas_of (S,G);

      :: MIDSP_2:def11

      func MidSp. w -> strict MidSp equals MidStr (# S, ( @ w) #);

      coherence

      proof

        set M = MidStr (# S, ( @ w) #), W = ( Atlas w);

        W is associating by A1, Th25;

        hence thesis by A1, Th20;

      end;

    end

    reserve M for non empty MidStr;

    reserve w for Function of [:the carrier of M, the carrier of M:], the carrier of G;

    reserve a,b,b1,b2,c for Point of M;

    theorem :: MIDSP_2:27

    

     Th26: M is MidSp iff ex G st ex w st w is_atlas_of (the carrier of M,G) & w is associating

    proof

      hereby

        assume

         A1: M is MidSp;

        thus ex G st ex w st w is_atlas_of (the carrier of M,G) & w is associating

        proof

          reconsider M as MidSp by A1;

          set G = ( vectgroup M);

          take G;

          ex w be Function of [:the carrier of M, the carrier of M:], the carrier of G st w is_atlas_of (the carrier of M,G) & w is associating

          proof

            take ( vect M);

            thus thesis by Th21;

          end;

          hence thesis;

        end;

      end;

      given G be midpoint_operator add-associative right_zeroed right_complementable Abelian non empty addLoopStr, w be Function of [:the carrier of M, the carrier of M:], the carrier of G such that

       A2: w is_atlas_of (the carrier of M,G) & w is associating;

      thus thesis by A2, Th20;

    end;

    definition

      let M be non empty MidStr;

      struct AtlasStr over M (# the algebra -> non empty addLoopStr,

the function -> Function of [:the carrier of M, the carrier of M:], the carrier of the algebra #)

       attr strict strict;

    end

    definition

      let M be non empty MidStr;

      let IT be AtlasStr over M;

      :: MIDSP_2:def12

      attr IT is ATLAS-like means

      : Def12: the algebra of IT is midpoint_operator add-associative right_zeroed right_complementable Abelian & the function of IT is associating & the function of IT is_atlas_of (the carrier of M,the algebra of IT);

    end

    registration

      let M be MidSp;

      cluster ATLAS-like for AtlasStr over M;

      existence

      proof

        consider G be midpoint_operator add-associative right_zeroed right_complementable Abelian non empty addLoopStr, w be Function of [:the carrier of M, the carrier of M:], the carrier of G such that

         A1: w is_atlas_of (the carrier of M,G) & w is associating by Th26;

        take AtlasStr (# G, w #);

        thus thesis by A1;

      end;

    end

    definition

      let M be non empty MidSp;

      mode ATLAS of M is ATLAS-like AtlasStr over M;

    end

    definition

      let M be non empty MidStr, W be AtlasStr over M;

      mode Vector of W is Element of the algebra of W;

    end

    definition

      let M be MidSp;

      let W be AtlasStr over M;

      let a,b be Point of M;

      :: MIDSP_2:def13

      func W . (a,b) -> Element of the algebra of W equals (the function of W . (a,b));

      coherence ;

    end

    definition

      let M be MidSp;

      let W be AtlasStr over M;

      let a be Point of M;

      let x be Vector of W;

      :: MIDSP_2:def14

      func (a,x) . W -> Point of M equals ((a,x) . the function of W);

      coherence ;

    end

    definition

      let M be MidSp, W be ATLAS of M;

      :: MIDSP_2:def15

      func 0. W -> Vector of W equals ( 0. the algebra of W);

      coherence ;

    end

    theorem :: MIDSP_2:28

    

     Th27: w is_atlas_of (the carrier of M,G) & w is associating implies ((a @ c) = (b1 @ b2) iff (w . (a,c)) = ((w . (a,b1)) + (w . (a,b2))))

    proof

      assume that

       A1: w is_atlas_of (the carrier of M,G) and

       A2: w is associating;

      

       A3: (a @ c) = (b1 @ b2) iff (w . (a,b2)) = (w . (b1,c)) by A1, A2, Th13;

      hence (a @ c) = (b1 @ b2) implies (w . (a,c)) = ((w . (a,b1)) + (w . (a,b2))) by A1;

      (w . (a,c)) = ((w . (a,b1)) + (w . (b1,c))) by A1;

      hence thesis by A3, RLVECT_1: 8;

    end;

    theorem :: MIDSP_2:29

    

     Th28: w is_atlas_of (the carrier of M,G) & w is associating implies ((a @ c) = b iff (w . (a,c)) = ( Double (w . (a,b))))

    proof

      assume

       A1: w is_atlas_of (the carrier of M,G) & w is associating;

      then

      reconsider MM = M as MidSp by Th20;

      reconsider bb = b as Point of MM;

      (bb @ bb) = bb by MIDSP_1:def 3;

      hence thesis by A1, Th27;

    end;

    reserve M for MidSp;

    reserve W for ATLAS of M;

    reserve a,b,b1,b2,c,d for Point of M;

    reserve x for Vector of W;

    theorem :: MIDSP_2:30

    (a @ c) = (b1 @ b2) iff (W . (a,c)) = ((W . (a,b1)) + (W . (a,b2)))

    proof

      set w = the function of W, G = the algebra of W;

      

       A1: G is midpoint_operator add-associative right_zeroed right_complementable Abelian by Def12;

      w is_atlas_of (the carrier of M,G) & w is associating by Def12;

      hence thesis by A1, Th27;

    end;

    theorem :: MIDSP_2:31

    (a @ c) = b iff (W . (a,c)) = ( Double (W . (a,b)))

    proof

      set w = the function of W, G = the algebra of W;

      

       A1: G is midpoint_operator add-associative right_zeroed right_complementable Abelian by Def12;

      w is_atlas_of (the carrier of M,G) & w is associating by Def12;

      hence thesis by A1, Th28;

    end;

    theorem :: MIDSP_2:32

    (for a, x holds ex b st (W . (a,b)) = x) & (for a, b, c holds (W . (a,b)) = (W . (a,c)) implies b = c) & for a, b, c holds ((W . (a,b)) + (W . (b,c))) = (W . (a,c))

    proof

      set w = the function of W;

      thus for a, x holds ex b st (W . (a,b)) = x

      proof

        set w = the function of W;

        let a, x;

        w is_atlas_of (the carrier of M,the algebra of W) by Def12;

        then

        consider b such that

         A1: (w . (a,b)) = x;

        take b;

        thus thesis by A1;

      end;

      thus for a, b, c holds (W . (a,b)) = (W . (a,c)) implies b = c

      proof

        set w = the function of W;

        

         A2: w is_atlas_of (the carrier of M,the algebra of W) by Def12;

        let a, b, c;

        assume (W . (a,b)) = (W . (a,c));

        hence thesis by A2;

      end;

      let a, b, c;

      w is_atlas_of (the carrier of M,the algebra of W) by Def12;

      hence thesis;

    end;

    theorem :: MIDSP_2:33

    

     Th32: (W . (a,a)) = ( 0. W) & ((W . (a,b)) = ( 0. W) implies a = b) & (W . (a,b)) = ( - (W . (b,a))) & ((W . (a,b)) = (W . (c,d)) implies (W . (b,a)) = (W . (d,c))) & (for b, x holds ex a st (W . (a,b)) = x) & ((W . (b,a)) = (W . (c,a)) implies b = c) & ((a @ b) = c iff (W . (a,c)) = (W . (c,b))) & ((a @ b) = (c @ d) iff (W . (a,d)) = (W . (c,b))) & ((W . (a,b)) = x iff ((a,x) . W) = b)

    proof

      set w = the function of W, G = the algebra of W;

      

       A1: w is_atlas_of (the carrier of M,G) by Def12;

      

       A2: G is midpoint_operator add-associative right_zeroed right_complementable Abelian by Def12;

      hence (W . (a,a)) = ( 0. W) by A1, Th2;

      thus (W . (a,b)) = ( 0. W) implies a = b by A2, A1, Th3;

      thus (W . (a,b)) = ( - (W . (b,a))) by A2, A1, Th4;

      thus (W . (a,b)) = (W . (c,d)) implies (W . (b,a)) = (W . (d,c)) by A2, A1, Th5;

      thus for b, x holds ex a st (W . (a,b)) = x

      proof

        let b, x;

        consider a such that

         A3: (w . (a,b)) = x by A2, A1, Th6;

        take a;

        thus thesis by A3;

      end;

      thus (W . (b,a)) = (W . (c,a)) implies b = c by A2, A1, Th7;

      

       A4: w is associating by Def12;

      hence (a @ b) = c iff (W . (a,c)) = (W . (c,b));

      thus (a @ b) = (c @ d) iff (W . (a,d)) = (W . (c,b)) by A2, A4, A1, Th13;

      thus thesis by A1, Def4;

    end;

    theorem :: MIDSP_2:34

    ((a,( 0. W)) . W) = a

    proof

      (W . (a,a)) = ( 0. W) by Th32;

      hence thesis by Th32;

    end;