tdgroup.miz



    begin

    theorem :: TDGROUP:1

    

     Th1: for a be Element of G_Real holds ex b be Element of G_Real st (b + b) = a

    proof

      set G = G_Real ;

      let a be Element of G;

      reconsider a as Element of REAL ;

      reconsider b9 = (a / 2) as Element of REAL by XREAL_0:def 1;

      consider b be Element of G such that

       A1: b = b9;

      (b + b) = a by A1;

      hence thesis;

    end;

    theorem :: TDGROUP:2

    for a be Element of G_Real st (a + a) = ( 0. G_Real ) holds a = ( 0. G_Real );

    definition

      let IT be non empty addLoopStr;

      :: TDGROUP:def1

      attr IT is Two_Divisible means

      : Def1: for a be Element of IT holds ex b be Element of IT st (b + b) = a;

    end

    

     Lm1: G_Real is Fanoian;

    registration

      cluster G_Real -> Fanoian Two_Divisible;

      coherence by Th1;

    end

    registration

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

      existence by Lm1;

    end

    definition

      mode Two_Divisible_Group is Two_Divisible add-associative right_zeroed right_complementable Abelian non empty addLoopStr;

    end

    definition

      mode Uniquely_Two_Divisible_Group is Fanoian Two_Divisible add-associative right_zeroed right_complementable Abelian non empty addLoopStr;

    end

    theorem :: TDGROUP:3

    for AG be add-associative right_zeroed right_complementable Abelian non empty addLoopStr holds (AG is Uniquely_Two_Divisible_Group iff (for a be Element of AG holds (ex b be Element of AG st (b + b) = a)) & (for a be Element of AG st (a + a) = ( 0. AG) holds a = ( 0. AG))) by Def1, VECTSP_1:def 18;

    reserve ADG for Uniquely_Two_Divisible_Group;

    reserve a,b,c,d,a9,b9,c9,p,q for Element of ADG;

    reserve x,y for set;

    notation

      let ADG be non empty addLoopStr;

      let a,b be Element of ADG;

      synonym a # b for a + b;

    end

    definition

      let ADG be non empty addLoopStr;

      :: TDGROUP:def2

      func CONGRD (ADG) -> Relation of [:the carrier of ADG, the carrier of ADG:] means

      : Def2: for a,b,c,d be Element of ADG holds [ [a, b], [c, d]] in it iff (a # d) = (b # c);

      existence

      proof

        set X = the carrier of ADG;

        set XX = [:X, X:];

        defpred X[ object, object] means ex a,b,c,d be Element of X st $1 = [a, b] & $2 = [c, d] & (a # d) = (b # c);

        consider P be Relation of XX, XX such that

         A1: for x,y be object holds [x, y] in P iff x in XX & y in XX & X[x, y] from RELSET_1:sch 1;

        take P;

        let a,b,c,d be Element of X;

        

         A2: [ [a, b], [c, d]] in P implies (a # d) = (b # c)

        proof

          assume [ [a, b], [c, d]] in P;

          then

          consider a9,b9,c9,d9 be Element of X such that

           A3: [a, b] = [a9, b9] and

           A4: [c, d] = [c9, d9] and

           A5: (a9 # d9) = (b9 # c9) by A1;

          

           A6: c = c9 by A4, XTUPLE_0: 1;

          a = a9 & b = b9 by A3, XTUPLE_0: 1;

          hence thesis by A4, A5, A6, XTUPLE_0: 1;

        end;

         [a, b] in XX & [c, d] in XX by ZFMISC_1:def 2;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        set X = the carrier of ADG;

        set XX = [:X, X:];

        let P,Q be Relation of [:X, X:] such that

         A7: for a,b,c,d be Element of X holds [ [a, b], [c, d]] in P iff (a # d) = (b # c) and

         A8: for a,b,c,d be Element of X holds [ [a, b], [c, d]] in Q iff (a # d) = (b # c);

        for x,y be object holds [x, y] in P iff [x, y] in Q

        proof

          let x,y be object;

           A9:

          now

            assume

             A10: [x, y] in Q;

            then x in XX by ZFMISC_1: 87;

            then

            consider a,b be Element of ADG such that

             A11: x = [a, b] by DOMAIN_1: 1;

            y in XX by A10, ZFMISC_1: 87;

            then

            consider c,d be Element of ADG such that

             A12: y = [c, d] by DOMAIN_1: 1;

             [x, y] in Q iff (a # d) = (b # c) by A8, A11, A12;

            hence [x, y] in P by A7, A10, A11, A12;

          end;

          now

            assume

             A13: [x, y] in P;

            then x in XX by ZFMISC_1: 87;

            then

            consider a,b be Element of ADG such that

             A14: x = [a, b] by DOMAIN_1: 1;

            y in XX by A13, ZFMISC_1: 87;

            then

            consider c,d be Element of ADG such that

             A15: y = [c, d] by DOMAIN_1: 1;

             [x, y] in P iff (a # d) = (b # c) by A7, A14, A15;

            hence [x, y] in Q by A8, A13, A14, A15;

          end;

          hence thesis by A9;

        end;

        hence thesis by RELAT_1:def 2;

      end;

    end

    definition

      let ADG be non empty addLoopStr;

      :: TDGROUP:def3

      func AV (ADG) -> strict AffinStruct equals AffinStruct (# the carrier of ADG, ( CONGRD ADG) #);

      coherence ;

    end

    registration

      let ADG be non empty addLoopStr;

      cluster ( AV ADG) -> non empty;

      coherence ;

    end

    theorem :: TDGROUP:4

    the carrier of ( AV ADG) = the carrier of ADG & the CONGR of ( AV ADG) = ( CONGRD ADG);

    definition

      let ADG;

      let a, b, c, d;

      :: TDGROUP:def4

      pred a,b ==> c,d means [ [a, b], [c, d]] in the CONGR of ( AV ADG);

    end

    theorem :: TDGROUP:5

    

     Th5: (a,b) ==> (c,d) iff (a # d) = (b # c) by Def2;

    theorem :: TDGROUP:6

    

     Th6: ex a,b be Element of G_Real st a <> b

    proof

      

       A1: 0 in REAL & 1 in REAL by XREAL_0:def 1;

      thus thesis by A1;

    end;

    theorem :: TDGROUP:7

    ex ADG st ex a, b st a <> b by Th6;

    theorem :: TDGROUP:8

    

     Th8: (a,b) ==> (c,c) implies a = b

    proof

      assume (a,b) ==> (c,c);

      then (a # c) = (b # c) by Th5;

      hence thesis by RLVECT_1: 8;

    end;

    theorem :: TDGROUP:9

    

     Th9: (a,b) ==> (p,q) & (c,d) ==> (p,q) implies (a,b) ==> (c,d)

    proof

      assume that

       A1: (a,b) ==> (p,q) and

       A2: (c,d) ==> (p,q);

      (a # q) = (b # p) by A1, Th5;

      

      then (a + (q + d)) = ((b + p) + d) by RLVECT_1:def 3

      .= (b + (p + d)) by RLVECT_1:def 3

      .= (b + (c + q)) by A2, Th5;

      

      then ((a + d) + q) = (b + (c + q)) by RLVECT_1:def 3

      .= ((b + c) + q) by RLVECT_1:def 3;

      then (a + d) = (b + c) by RLVECT_1: 8;

      hence thesis by Th5;

    end;

    theorem :: TDGROUP:10

    

     Th10: ex d st (a,b) ==> (c,d)

    proof

      set d9 = (( - a) + (b + c));

      take d9;

      (a + d9) = ((a + ( - a)) + (b + c)) by RLVECT_1:def 3

      .= (( 0. ADG) + (b + c)) by RLVECT_1: 5

      .= (b + c) by RLVECT_1: 4;

      hence thesis by Th5;

    end;

    theorem :: TDGROUP:11

    

     Th11: (a,b) ==> (a9,b9) & (a,c) ==> (a9,c9) implies (b,c) ==> (b9,c9)

    proof

      assume (a,b) ==> (a9,b9) & (a,c) ==> (a9,c9);

      then (a + b9) = (b + a9) & (a + c9) = (c + a9) by Th5;

      

      then (b + (a9 + (a + c9))) = ((c + a9) + (a + b9)) by RLVECT_1:def 3

      .= (c + (a9 + (a + b9))) by RLVECT_1:def 3;

      

      then (b + ((a9 + a) + c9)) = (c + (a9 + (a + b9))) by RLVECT_1:def 3

      .= (c + ((a9 + a) + b9)) by RLVECT_1:def 3;

      

      then ((b + c9) + (a9 + a)) = (c + (b9 + (a9 + a))) by RLVECT_1:def 3

      .= ((c + b9) + (a9 + a)) by RLVECT_1:def 3;

      then (b + c9) = (c + b9) by RLVECT_1: 8;

      hence thesis by Th5;

    end;

    theorem :: TDGROUP:12

    

     Th12: ex b st (a,b) ==> (b,c)

    proof

      consider b be Element of ADG such that

       A1: (b + b) = (a + c) by Def1;

      take b;

      thus thesis by A1, Th5;

    end;

    theorem :: TDGROUP:13

    

     Th13: (a,b) ==> (b,c) & (a,b9) ==> (b9,c) implies b = b9

    proof

      assume (a,b) ==> (b,c) & (a,b9) ==> (b9,c);

      then (a + c) = (b + b) & (a + c) = (b9 + b9) by Th5;

      

      then ((b + ( - b9)) + b) = ((b9 + b9) + ( - b9)) by RLVECT_1:def 3

      .= (b9 + (b9 + ( - b9))) by RLVECT_1:def 3

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

      .= b9 by RLVECT_1: 4;

      

      then

       A1: ((b + ( - b9)) + (b + ( - b9))) = (b9 + ( - b9)) by RLVECT_1:def 3

      .= ( 0. ADG) by RLVECT_1: 5;

      b9 = (( 0. ADG) + b9) by RLVECT_1: 4

      .= ((b + ( - b9)) + b9) by A1, VECTSP_1:def 18

      .= (b + (( - b9) + b9)) by RLVECT_1:def 3

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

      .= b by RLVECT_1: 4;

      hence thesis;

    end;

    theorem :: TDGROUP:14

    

     Th14: (a,b) ==> (c,d) implies (a,c) ==> (b,d)

    proof

      assume (a,b) ==> (c,d);

      then (a + d) = (b + c) by Th5;

      hence thesis by Th5;

    end;

    reserve AS for non empty AffinStruct;

    theorem :: TDGROUP:15

    

     Th15: (ex a,b be Element of ADG st a <> b) implies (ex a,b be Element of ( AV ADG) st a <> b) & (for a,b,c be Element of ( AV ADG) st (a,b) // (c,c) holds a = b) & (for a,b,c,d,p,q be Element of ( AV ADG) st (a,b) // (p,q) & (c,d) // (p,q) holds (a,b) // (c,d)) & (for a,b,c be Element of ( AV ADG) holds ex d be Element of ( AV ADG) st (a,b) // (c,d)) & (for a,b,c,a9,b9,c9 be Element of ( AV ADG) st (a,b) // (a9,b9) & (a,c) // (a9,c9) holds (b,c) // (b9,c9)) & (for a,c be Element of ( AV ADG) holds ex b be Element of ( AV ADG) st (a,b) // (b,c)) & (for a,b,c,b9 be Element of ( AV ADG) st (a,b) // (b,c) & (a,b9) // (b9,c) holds b = b9) & for a,b,c,d be Element of ( AV ADG) st (a,b) // (c,d) holds (a,c) // (b,d)

    proof

      set A = ( AV ADG);

      assume ex a,b be Element of ADG st a <> b;

      hence ex a,b be Element of A st a <> b;

      

       A1: for a9,b9,c9,d9 be Element of A holds for a, b, c, d st a = a9 & b = b9 & c = c9 & d = d9 holds ((a,b) ==> (c,d) iff (a9,b9) // (c9,d9)) by ANALOAF:def 2;

      thus for a,b,c be Element of A st (a,b) // (c,c) holds a = b

      proof

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

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

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

        (a9,b9) ==> (c9,c9) by A1, A2;

        hence thesis by Th8;

      end;

      thus for a,b,c,d,p,q be Element of A st (a,b) // (p,q) & (c,d) // (p,q) holds (a,b) // (c,d)

      proof

        let a,b,c,d,p,q be Element of A;

        reconsider a9 = a, b9 = b, c9 = c, d9 = d, p9 = p, q9 = q as Element of ADG;

        assume (a,b) // (p,q) & (c,d) // (p,q);

        then (a9,b9) ==> (p9,q9) & (c9,d9) ==> (p9,q9) by A1;

        then (a9,b9) ==> (c9,d9) by Th9;

        hence thesis by A1;

      end;

      thus for a,b,c be Element of A holds ex d be Element of A st (a,b) // (c,d)

      proof

        let a,b,c be Element of A;

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

        consider d9 be Element of ADG such that

         A3: (a9,b9) ==> (c9,d9) by Th10;

        reconsider d = d9 as Element of A;

        take d;

        thus thesis by A1, A3;

      end;

      thus for a,b,c,a9,b9,c9 be Element of A st (a,b) // (a9,b9) & (a,c) // (a9,c9) holds (b,c) // (b9,c9)

      proof

        let a,b,c,a9,b9,c9 be Element of A;

        reconsider p = a, q = b, r = c, p9 = a9, q9 = b9, r9 = c9 as Element of ADG;

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

        then (p,q) ==> (p9,q9) & (p,r) ==> (p9,r9) by A1;

        then (q,r) ==> (q9,r9) by Th11;

        hence thesis by A1;

      end;

      thus for a,c be Element of A holds ex b be Element of A st (a,b) // (b,c)

      proof

        let a,c be Element of A;

        reconsider a9 = a, c9 = c as Element of ADG;

        consider b9 be Element of ADG such that

         A4: (a9,b9) ==> (b9,c9) by Th12;

        reconsider b = b9 as Element of A;

        take b;

        thus thesis by A1, A4;

      end;

      thus for a,b,c,b9 be Element of A st (a,b) // (b,c) & (a,b9) // (b9,c) holds b = b9

      proof

        let a,b,c,b9 be Element of A;

        reconsider a9 = a, p = b, c9 = c, p9 = b9 as Element of ADG;

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

        then (a9,p) ==> (p,c9) & (a9,p9) ==> (p9,c9) by A1;

        hence thesis by Th13;

      end;

      thus for a,b,c,d be Element of A st (a,b) // (c,d) holds (a,c) // (b,d)

      proof

        let a,b,c,d be Element of A;

        reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of ADG;

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

        then (a9,b9) ==> (c9,d9) by A1;

        then (a9,c9) ==> (b9,d9) by Th14;

        hence thesis by A1;

      end;

    end;

    definition

      let IT be non empty AffinStruct;

      :: TDGROUP:def5

      attr IT is AffVect-like means

      : Def5: (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,b9 be Element of IT st (a,b) // (b,c) & (a,b9) // (b9,c) holds b = b9) & for a,b,c,d be Element of IT st (a,b) // (c,d) holds (a,c) // (b,d);

    end

    registration

      cluster strict AffVect-like for non trivial AffinStruct;

      existence

      proof

        consider ADG such that

         A1: ex a, b st a <> b by Th6;

        

         A2: (for a,b,c,a9,b9,c9 be Element of ( AV ADG) st (a,b) // (a9,b9) & (a,c) // (a9,c9) holds (b,c) // (b9,c9)) & for a,c be Element of ( AV ADG) holds ex b be Element of ( AV ADG) st (a,b) // (b,c) by A1, Th15;

        

         A3: (for a,b,c be Element of ( AV ADG) st (a,b) // (c,c) holds a = b) & for a,b,c,b9 be Element of ( AV ADG) st (a,b) // (b,c) & (a,b9) // (b9,c) holds b = b9 by Th15;

        

         A4: for a,b,c,d be Element of ( AV ADG) st (a,b) // (c,d) holds (a,c) // (b,d) by A1, Th15;

        (for a,b,c,d,p,q be Element of ( AV ADG) st (a,b) // (p,q) & (c,d) // (p,q) holds (a,b) // (c,d)) & for a,b,c be Element of ( AV ADG) holds ex d be Element of ( AV ADG) st (a,b) // (c,d) by A1, Th15;

        then ( AV ADG) is non trivial AffVect-like by A1, A2, A3, A4;

        hence thesis;

      end;

    end

    definition

      mode AffVect is AffVect-like non trivial AffinStruct;

    end

    theorem :: TDGROUP:16

    for AS holds (ex a,b be Element of AS st a <> b) & (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)) & (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)) & (for a,c be Element of AS holds ex b be Element of AS st (a,b) // (b,c)) & (for a,b,c,b9 be Element of AS st (a,b) // (b,c) & (a,b9) // (b9,c) holds b = b9) & (for a,b,c,d be Element of AS st (a,b) // (c,d) holds (a,c) // (b,d)) iff AS is AffVect by Def5, STRUCT_0:def 10;

    theorem :: TDGROUP:17

    (ex a,b be Element of ADG st a <> b) implies ( AV ADG) is AffVect

    proof

      

       A1: (for a,b,c be Element of ( AV ADG) st (a,b) // (c,c) holds a = b) & for a,b,c,b9 be Element of ( AV ADG) st (a,b) // (b,c) & (a,b9) // (b9,c) holds b = b9 by Th15;

      assume

       A2: ex a,b be Element of ADG st a <> b;

      then

       A3: (for a,b,c,a9,b9,c9 be Element of ( AV ADG) st (a,b) // (a9,b9) & (a,c) // (a9,c9) holds (b,c) // (b9,c9)) & for a,c be Element of ( AV ADG) holds ex b be Element of ( AV ADG) st (a,b) // (b,c) by Th15;

      

       A4: for a,b,c,d be Element of ( AV ADG) st (a,b) // (c,d) holds (a,c) // (b,d) by A2, Th15;

      (for a,b,c,d,p,q be Element of ( AV ADG) st (a,b) // (p,q) & (c,d) // (p,q) holds (a,b) // (c,d)) & for a,b,c be Element of ( AV ADG) holds ex d be Element of ( AV ADG) st (a,b) // (c,d) by A2, Th15;

      hence thesis by A2, A3, A1, A4, Def5, STRUCT_0:def 10;

    end;