algstr_2.miz



    begin

    reserve L for non empty doubleLoopStr;

    

     Lm1: 0 = ( 0. F_Real ) by STRUCT_0:def 6, VECTSP_1:def 5;

    

     Lm2: for a,b be Element of F_Real st a <> ( 0. F_Real ) holds ex x be Element of F_Real st (a * x) = b

    proof

      let a,b be Element of F_Real such that

       A1: a <> ( 0. F_Real );

      reconsider p = a, q = b as Element of REAL by VECTSP_1:def 5;

      reconsider x = (q / p) as Element of F_Real by VECTSP_1:def 5;

      (p * (q / p)) = q by A1, Lm1, XCMPLX_1: 87;

      then (a * x) = b;

      hence thesis;

    end;

    

     Lm3: for a,b be Element of F_Real st a <> ( 0. F_Real ) holds ex x be Element of F_Real st (x * a) = b

    proof

      let a,b be Element of F_Real ;

      assume a <> ( 0. F_Real );

      then ex x be Element of F_Real st (a * x) = b by Lm2;

      hence thesis;

    end;

    

     Lm4: (for a,x,y be Element of F_Real st a <> ( 0. F_Real ) holds (a * x) = (a * y) implies x = y) & for a,x,y be Element of F_Real st a <> ( 0. F_Real ) holds (x * a) = (y * a) implies x = y by VECTSP_1: 5;

    

     Lm5: (for a be Element of F_Real holds (a * ( 0. F_Real )) = ( 0. F_Real )) & for a be Element of F_Real holds (( 0. F_Real ) * a) = ( 0. F_Real ) by VECTSP_1: 12;

    registration

      cluster F_Real -> multLoop_0-like;

      coherence by Lm2, Lm3, Lm4, Lm5, ALGSTR_1: 16;

    end

    definition

      let L be left_add-cancelable add-right-invertible non empty addLoopStr;

      let a be Element of L;

      :: ALGSTR_2:def1

      func - a -> Element of L means

      : Def1: (a + it ) = ( 0. L);

      existence by ALGSTR_1:def 4;

      uniqueness by ALGSTR_0:def 3;

    end

    definition

      let L be left_add-cancelable add-right-invertible non empty addLoopStr;

      let a,b be Element of L;

      :: ALGSTR_2:def2

      func a - b -> Element of L equals (a + ( - b));

      correctness ;

    end

    registration

      cluster strict Abelian add-associative commutative associative distributive non degenerated left_zeroed right_zeroed Loop-like well-unital multLoop_0-like for non empty doubleLoopStr;

      existence

      proof

        take F_Real ;

        thus thesis;

      end;

    end

    definition

      mode doubleLoop is left_zeroed right_zeroed Loop-like well-unital multLoop_0-like non empty doubleLoopStr;

    end

    definition

      mode leftQuasi-Field is Abelian add-associative right-distributive non degenerated doubleLoop;

    end

    reserve a,b,c,x,y,z for Element of L;

    theorem :: ALGSTR_2:1

    L is leftQuasi-Field iff (for a holds (a + ( 0. L)) = a) & (for a holds ex x st (a + x) = ( 0. L)) & (for a, b, c holds ((a + b) + c) = (a + (b + c))) & (for a, b holds (a + b) = (b + a)) & ( 0. L) <> ( 1. L) & (for a holds (a * ( 1. L)) = a) & (for a holds (( 1. L) * a) = a) & (for a, b st a <> ( 0. L) holds ex x st (a * x) = b) & (for a, b st a <> ( 0. L) holds ex x st (x * a) = b) & (for a, x, y st a <> ( 0. L) holds (a * x) = (a * y) implies x = y) & (for a, x, y st a <> ( 0. L) holds (x * a) = (y * a) implies x = y) & (for a holds (a * ( 0. L)) = ( 0. L)) & (for a holds (( 0. L) * a) = ( 0. L)) & for a, b, c holds (a * (b + c)) = ((a * b) + (a * c))

    proof

      thus L is leftQuasi-Field implies (for a holds (a + ( 0. L)) = a) & (for a holds ex x st (a + x) = ( 0. L)) & (for a, b, c holds ((a + b) + c) = (a + (b + c))) & (for a, b holds (a + b) = (b + a)) & ( 0. L) <> ( 1. L) & (for a holds (a * ( 1. L)) = a) & (for a holds (( 1. L) * a) = a) & (for a, b st a <> ( 0. L) holds ex x st (a * x) = b) & (for a, b st a <> ( 0. L) holds ex x st (x * a) = b) & (for a, x, y st a <> ( 0. L) holds (a * x) = (a * y) implies x = y) & (for a, x, y st a <> ( 0. L) holds (x * a) = (y * a) implies x = y) & (for a holds (a * ( 0. L)) = ( 0. L)) & (for a holds (( 0. L) * a) = ( 0. L)) & for a, b, c holds (a * (b + c)) = ((a * b) + (a * c)) by ALGSTR_1: 6, ALGSTR_1: 16, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, STRUCT_0:def 8, VECTSP_1:def 2;

      assume that

       A1: for a holds (a + ( 0. L)) = a and

       A2: for a holds ex x st (a + x) = ( 0. L) and

       A3: for a, b, c holds ((a + b) + c) = (a + (b + c)) and

       A4: for a, b holds (a + b) = (b + a) and

       A5: (( 0. L) <> ( 1. L) & for a holds (a * ( 1. L)) = a) & ((for a holds (( 1. L) * a) = a) & for a, b st a <> ( 0. L) holds ex x st (a * x) = b) & ((for a, b st a <> ( 0. L) holds ex x st (x * a) = b) & for a, x, y st a <> ( 0. L) holds (a * x) = (a * y) implies x = y) & ((for a, x, y st a <> ( 0. L) holds (x * a) = (y * a) implies x = y) & for a holds (a * ( 0. L)) = ( 0. L)) & ((for a holds (( 0. L) * a) = ( 0. L)) & for a, b, c holds (a * (b + c)) = ((a * b) + (a * c)));

      

       A6: for a holds (( 0. L) + a) = a

      proof

        let a;

        

        thus (( 0. L) + a) = (a + ( 0. L)) by A4

        .= a by A1;

      end;

      

       A7: for a, b holds ex x st (a + x) = b

      proof

        let a, b;

        consider y such that

         A8: (a + y) = ( 0. L) by A2;

        take x = (y + b);

        

        thus (a + x) = (( 0. L) + b) by A3, A8

        .= b by A6;

      end;

      

       A9: for a, b holds ex x st (x + a) = b

      proof

        let a, b;

        consider x such that

         A10: (a + x) = b by A7;

        take x;

        thus thesis by A4, A10;

      end;

      

       A11: for a, x, y holds (a + x) = (a + y) implies x = y

      proof

        let a, x, y;

        consider z such that

         A12: (z + a) = ( 0. L) by A1, A2, A3, ALGSTR_1: 3;

        assume (a + x) = (a + y);

        

        then ((z + a) + x) = (z + (a + y)) by A3

        .= ((z + a) + y) by A3;

        

        hence x = (( 0. L) + y) by A6, A12

        .= y by A6;

      end;

      for a, x, y holds (x + a) = (y + a) implies x = y

      proof

        let a, x, y;

        assume (x + a) = (y + a);

        

        then (a + x) = (y + a) by A4

        .= (a + y) by A4;

        hence thesis by A11;

      end;

      hence thesis by A1, A3, A4, A5, A6, A7, A9, A11, ALGSTR_1: 6, ALGSTR_1: 16, ALGSTR_1:def 2, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, STRUCT_0:def 8, VECTSP_1:def 2, VECTSP_1:def 6;

    end;

    theorem :: ALGSTR_2:2

    

     Th2: for G be Abelian right-distributive doubleLoop, a,b be Element of G holds (a * ( - b)) = ( - (a * b))

    proof

      let G be Abelian right-distributive doubleLoop, a,b be Element of G;

      ((a * b) + (a * ( - b))) = (a * (b + ( - b))) by VECTSP_1:def 2

      .= (a * ( 0. G)) by Def1

      .= ( 0. G) by ALGSTR_1: 16;

      hence thesis by Def1;

    end;

    theorem :: ALGSTR_2:3

    

     Th3: for G be Abelian left_add-cancelable add-right-invertible non empty addLoopStr, a be Element of G holds ( - ( - a)) = a

    proof

      let G be Abelian left_add-cancelable add-right-invertible non empty addLoopStr, a be Element of G;

      (( - a) + a) = ( 0. G) by Def1;

      hence thesis by Def1;

    end;

    theorem :: ALGSTR_2:4

    for G be Abelian right-distributive doubleLoop holds (( - ( 1. G)) * ( - ( 1. G))) = ( 1. G)

    proof

      let G be Abelian right-distributive doubleLoop;

      

      thus (( - ( 1. G)) * ( - ( 1. G))) = ( - (( - ( 1. G)) * ( 1_ G))) by Th2

      .= ( - ( - ( 1. G)))

      .= ( 1. G) by Th3;

    end;

    theorem :: ALGSTR_2:5

    for G be Abelian right-distributive doubleLoop, a,x,y be Element of G holds (a * (x - y)) = ((a * x) - (a * y))

    proof

      let G be Abelian right-distributive doubleLoop, a,x,y be Element of G;

      

      thus (a * (x - y)) = ((a * x) + (a * ( - y))) by VECTSP_1:def 2

      .= ((a * x) - (a * y)) by Th2;

    end;

    definition

      mode rightQuasi-Field is Abelian add-associative left-distributive non degenerated doubleLoop;

    end

    theorem :: ALGSTR_2:6

    L is rightQuasi-Field iff (for a holds (a + ( 0. L)) = a) & (for a holds ex x st (a + x) = ( 0. L)) & (for a, b, c holds ((a + b) + c) = (a + (b + c))) & (for a, b holds (a + b) = (b + a)) & ( 0. L) <> ( 1. L) & (for a holds (a * ( 1. L)) = a) & (for a holds (( 1. L) * a) = a) & (for a, b st a <> ( 0. L) holds ex x st (a * x) = b) & (for a, b st a <> ( 0. L) holds ex x st (x * a) = b) & (for a, x, y st a <> ( 0. L) holds (a * x) = (a * y) implies x = y) & (for a, x, y st a <> ( 0. L) holds (x * a) = (y * a) implies x = y) & (for a holds (a * ( 0. L)) = ( 0. L)) & (for a holds (( 0. L) * a) = ( 0. L)) & for a, b, c holds ((b + c) * a) = ((b * a) + (c * a))

    proof

      thus L is rightQuasi-Field implies (for a holds (a + ( 0. L)) = a) & (for a holds ex x st (a + x) = ( 0. L)) & (for a, b, c holds ((a + b) + c) = (a + (b + c))) & (for a, b holds (a + b) = (b + a)) & ( 0. L) <> ( 1. L) & (for a holds (a * ( 1. L)) = a) & (for a holds (( 1. L) * a) = a) & (for a, b st a <> ( 0. L) holds ex x st (a * x) = b) & (for a, b st a <> ( 0. L) holds ex x st (x * a) = b) & (for a, x, y st a <> ( 0. L) holds (a * x) = (a * y) implies x = y) & (for a, x, y st a <> ( 0. L) holds (x * a) = (y * a) implies x = y) & (for a holds (a * ( 0. L)) = ( 0. L)) & (for a holds (( 0. L) * a) = ( 0. L)) & for a, b, c holds ((b + c) * a) = ((b * a) + (c * a)) by ALGSTR_1: 6, ALGSTR_1: 16, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, STRUCT_0:def 8, VECTSP_1:def 3;

      assume that

       A1: for a holds (a + ( 0. L)) = a and

       A2: for a holds ex x st (a + x) = ( 0. L) and

       A3: for a, b, c holds ((a + b) + c) = (a + (b + c)) and

       A4: for a, b holds (a + b) = (b + a) and

       A5: (( 0. L) <> ( 1. L) & for a holds (a * ( 1. L)) = a) & ((for a holds (( 1. L) * a) = a) & for a, b st a <> ( 0. L) holds ex x st (a * x) = b) & ((for a, b st a <> ( 0. L) holds ex x st (x * a) = b) & for a, x, y st a <> ( 0. L) holds (a * x) = (a * y) implies x = y) & ((for a, x, y st a <> ( 0. L) holds (x * a) = (y * a) implies x = y) & for a holds (a * ( 0. L)) = ( 0. L)) & ((for a holds (( 0. L) * a) = ( 0. L)) & for a, b, c holds ((b + c) * a) = ((b * a) + (c * a)));

      

       A6: for a, b holds ex x st (x + a) = b

      proof

        let a, b;

        consider y such that

         A7: (y + a) = ( 0. L) by A1, A2, A3, ALGSTR_1: 3;

        take x = (b + y);

        

        thus (x + a) = (b + ( 0. L)) by A3, A7

        .= b by A1;

      end;

      

       A8: for a holds (( 0. L) + a) = a

      proof

        let a;

        

        thus (( 0. L) + a) = (a + ( 0. L)) by A4

        .= a by A1;

      end;

      

       A9: for a, x, y holds (a + x) = (a + y) implies x = y

      proof

        let a, x, y;

        consider z such that

         A10: (z + a) = ( 0. L) by A1, A2, A3, ALGSTR_1: 3;

        assume (a + x) = (a + y);

        

        then ((z + a) + x) = (z + (a + y)) by A3

        .= ((z + a) + y) by A3;

        

        hence x = (( 0. L) + y) by A8, A10

        .= y by A8;

      end;

      

       A11: for a, x, y holds (x + a) = (y + a) implies x = y

      proof

        let a, x, y;

        consider z such that

         A12: (a + z) = ( 0. L) by A2;

        assume (x + a) = (y + a);

        

        then (x + (a + z)) = ((y + a) + z) by A3

        .= (y + (a + z)) by A3;

        

        hence x = (y + ( 0. L)) by A1, A12

        .= y by A1;

      end;

      for a, b holds ex x st (a + x) = b

      proof

        let a, b;

        consider y such that

         A13: (a + y) = ( 0. L) by A2;

        take x = (y + b);

        

        thus (a + x) = (( 0. L) + b) by A3, A13

        .= b by A8;

      end;

      hence thesis by A1, A3, A4, A5, A8, A6, A9, A11, ALGSTR_1: 6, ALGSTR_1: 16, ALGSTR_1:def 2, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, STRUCT_0:def 8, VECTSP_1:def 3, VECTSP_1:def 6;

    end;

    reserve G for left-distributive doubleLoop,

a,b,x,y for Element of G;

    theorem :: ALGSTR_2:7

    

     Th7: (( - b) * a) = ( - (b * a))

    proof

      ((b * a) + (( - b) * a)) = ((b + ( - b)) * a) by VECTSP_1:def 3

      .= (( 0. G) * a) by Def1

      .= ( 0. G) by ALGSTR_1: 16;

      hence thesis by Def1;

    end;

    theorem :: ALGSTR_2:8

    for G be Abelian left-distributive doubleLoop holds (( - ( 1. G)) * ( - ( 1. G))) = ( 1. G)

    proof

      let G be Abelian left-distributive doubleLoop;

      

      thus (( - ( 1. G)) * ( - ( 1. G))) = ( - (( 1_ G) * ( - ( 1. G)))) by Th7

      .= ( - ( - ( 1. G)))

      .= ( 1. G) by Th3;

    end;

    theorem :: ALGSTR_2:9

    ((x - y) * a) = ((x * a) - (y * a))

    proof

      

      thus ((x - y) * a) = ((x * a) + (( - y) * a)) by VECTSP_1:def 3

      .= ((x * a) - (y * a)) by Th7;

    end;

    definition

      mode doublesidedQuasi-Field is Abelian add-associative distributive non degenerated doubleLoop;

    end

    reserve a,b,c,x,y,z for Element of L;

    theorem :: ALGSTR_2:10

    L is doublesidedQuasi-Field iff (for a holds (a + ( 0. L)) = a) & (for a holds ex x st (a + x) = ( 0. L)) & (for a, b, c holds ((a + b) + c) = (a + (b + c))) & (for a, b holds (a + b) = (b + a)) & ( 0. L) <> ( 1. L) & (for a holds (a * ( 1. L)) = a) & (for a holds (( 1. L) * a) = a) & (for a, b st a <> ( 0. L) holds ex x st (a * x) = b) & (for a, b st a <> ( 0. L) holds ex x st (x * a) = b) & (for a, x, y st a <> ( 0. L) holds (a * x) = (a * y) implies x = y) & (for a, x, y st a <> ( 0. L) holds (x * a) = (y * a) implies x = y) & (for a holds (a * ( 0. L)) = ( 0. L)) & (for a holds (( 0. L) * a) = ( 0. L)) & (for a, b, c holds (a * (b + c)) = ((a * b) + (a * c))) & for a, b, c holds ((b + c) * a) = ((b * a) + (c * a))

    proof

      thus L is doublesidedQuasi-Field implies (for a holds (a + ( 0. L)) = a) & (for a holds ex x st (a + x) = ( 0. L)) & (for a, b, c holds ((a + b) + c) = (a + (b + c))) & (for a, b holds (a + b) = (b + a)) & ( 0. L) <> ( 1. L) & (for a holds (a * ( 1. L)) = a) & (for a holds (( 1. L) * a) = a) & (for a, b st a <> ( 0. L) holds ex x st (a * x) = b) & (for a, b st a <> ( 0. L) holds ex x st (x * a) = b) & (for a, x, y st a <> ( 0. L) holds (a * x) = (a * y) implies x = y) & (for a, x, y st a <> ( 0. L) holds (x * a) = (y * a) implies x = y) & (for a holds (a * ( 0. L)) = ( 0. L)) & (for a holds (( 0. L) * a) = ( 0. L)) & (for a, b, c holds (a * (b + c)) = ((a * b) + (a * c))) & for a, b, c holds ((b + c) * a) = ((b * a) + (c * a)) by ALGSTR_1: 6, ALGSTR_1: 16, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, STRUCT_0:def 8, VECTSP_1:def 7;

      assume that

       A1: for a holds (a + ( 0. L)) = a and

       A2: for a holds ex x st (a + x) = ( 0. L) and

       A3: for a, b, c holds ((a + b) + c) = (a + (b + c)) and

       A4: for a, b holds (a + b) = (b + a) and

       A5: (( 0. L) <> ( 1. L) & for a holds (a * ( 1. L)) = a) & ((for a holds (( 1. L) * a) = a) & for a, b st a <> ( 0. L) holds ex x st (a * x) = b) & ((for a, b st a <> ( 0. L) holds ex x st (x * a) = b) & for a, x, y st a <> ( 0. L) holds (a * x) = (a * y) implies x = y) & ((for a, x, y st a <> ( 0. L) holds (x * a) = (y * a) implies x = y) & for a holds (a * ( 0. L)) = ( 0. L)) & (((for a holds (( 0. L) * a) = ( 0. L)) & for a, b, c holds (a * (b + c)) = ((a * b) + (a * c))) & for a, b, c holds ((b + c) * a) = ((b * a) + (c * a)));

      

       A6: for a, b holds ex x st (x + a) = b

      proof

        let a, b;

        consider y such that

         A7: (y + a) = ( 0. L) by A1, A2, A3, ALGSTR_1: 3;

        take x = (b + y);

        

        thus (x + a) = (b + ( 0. L)) by A3, A7

        .= b by A1;

      end;

      

       A8: for a holds (( 0. L) + a) = a

      proof

        let a;

        

        thus (( 0. L) + a) = (a + ( 0. L)) by A4

        .= a by A1;

      end;

      

       A9: for a, x, y holds (a + x) = (a + y) implies x = y

      proof

        let a, x, y;

        consider z such that

         A10: (z + a) = ( 0. L) by A1, A2, A3, ALGSTR_1: 3;

        assume (a + x) = (a + y);

        

        then ((z + a) + x) = (z + (a + y)) by A3

        .= ((z + a) + y) by A3;

        

        hence x = (( 0. L) + y) by A8, A10

        .= y by A8;

      end;

      

       A11: for a, x, y holds (x + a) = (y + a) implies x = y

      proof

        let a, x, y;

        consider z such that

         A12: (a + z) = ( 0. L) by A2;

        assume (x + a) = (y + a);

        

        then (x + (a + z)) = ((y + a) + z) by A3

        .= (y + (a + z)) by A3;

        

        hence x = (y + ( 0. L)) by A1, A12

        .= y by A1;

      end;

      for a, b holds ex x st (a + x) = b

      proof

        let a, b;

        consider y such that

         A13: (a + y) = ( 0. L) by A2;

        take x = (y + b);

        

        thus (a + x) = (( 0. L) + b) by A3, A13

        .= b by A8;

      end;

      hence thesis by A1, A3, A4, A5, A8, A6, A9, A11, ALGSTR_1: 6, ALGSTR_1: 16, ALGSTR_1:def 2, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, STRUCT_0:def 8, VECTSP_1:def 6, VECTSP_1:def 7;

    end;

    definition

      mode _Skew-Field is associative doublesidedQuasi-Field;

    end

    

     Lm6: ( 0. L) <> ( 1. L) & (for a holds (a * ( 1. L)) = a) & (for a st a <> ( 0. L) holds ex x st (a * x) = ( 1. L)) & (for a, b, c holds ((a * b) * c) = (a * (b * c))) & (for a holds (a * ( 0. L)) = ( 0. L)) implies ((a * b) = ( 1. L) implies (b * a) = ( 1. L))

    proof

      assume that

       A1: ( 0. L) <> ( 1. L) and

       A2: for a holds (a * ( 1. L)) = a and

       A3: for a st a <> ( 0. L) holds ex x st (a * x) = ( 1. L) and

       A4: for a, b, c holds ((a * b) * c) = (a * (b * c)) and

       A5: for a holds (a * ( 0. L)) = ( 0. L);

      thus (a * b) = ( 1. L) implies (b * a) = ( 1. L)

      proof

        assume

         A6: (a * b) = ( 1. L);

        then b <> ( 0. L) by A1, A5;

        then

        consider x such that

         A7: (b * x) = ( 1. L) by A3;

        

        thus (b * a) = ((b * a) * (b * x)) by A2, A7

        .= (((b * a) * b) * x) by A4

        .= ((b * ( 1. L)) * x) by A4, A6

        .= ( 1. L) by A2, A7;

      end;

    end;

    

     Lm7: ( 0. L) <> ( 1. L) & (for a holds (a * ( 1. L)) = a) & (for a st a <> ( 0. L) holds ex x st (a * x) = ( 1. L)) & (for a, b, c holds ((a * b) * c) = (a * (b * c))) & (for a holds (a * ( 0. L)) = ( 0. L)) implies (( 1. L) * a) = (a * ( 1. L))

    proof

      assume that

       A1: ( 0. L) <> ( 1. L) and

       A2: for a holds (a * ( 1. L)) = a and

       A3: for a st a <> ( 0. L) holds ex x st (a * x) = ( 1. L) and

       A4: for a, b, c holds ((a * b) * c) = (a * (b * c)) and

       A5: for a holds (a * ( 0. L)) = ( 0. L);

      

       A6: a <> ( 0. L) implies (( 1. L) * a) = (a * ( 1. L))

      proof

        assume a <> ( 0. L);

        then

        consider x such that

         A7: (a * x) = ( 1. L) by A3;

        

        thus (( 1. L) * a) = (a * (x * a)) by A4, A7

        .= (a * ( 1. L)) by A1, A2, A3, A4, A5, A7, Lm6;

      end;

      a = ( 0. L) implies (( 1. L) * a) = (a * ( 1. L))

      proof

        assume

         A8: a = ( 0. L);

        

        hence (( 1. L) * a) = ( 0. L) by A5

        .= (a * ( 1. L)) by A2, A8;

      end;

      hence thesis by A6;

    end;

    

     Lm8: ( 0. L) <> ( 1. L) & (for a holds (a * ( 1. L)) = a) & (for a st a <> ( 0. L) holds ex x st (a * x) = ( 1. L)) & (for a, b, c holds ((a * b) * c) = (a * (b * c))) & (for a holds (a * ( 0. L)) = ( 0. L)) implies for a st a <> ( 0. L) holds ex x st (x * a) = ( 1. L)

    proof

      assume that

       A1: ( 0. L) <> ( 1. L) & for a holds (a * ( 1. L)) = a and

       A2: for a st a <> ( 0. L) holds ex x st (a * x) = ( 1. L) and

       A3: (for a, b, c holds ((a * b) * c) = (a * (b * c))) & for a holds (a * ( 0. L)) = ( 0. L);

      let a;

      assume a <> ( 0. L);

      then

      consider x such that

       A4: (a * x) = ( 1. L) by A2;

      (x * a) = ( 1. L) by A1, A2, A3, A4, Lm6;

      hence thesis;

    end;

    theorem :: ALGSTR_2:11

    

     Th11: L is _Skew-Field iff (for a holds (a + ( 0. L)) = a) & (for a holds ex x st (a + x) = ( 0. L)) & (for a, b, c holds ((a + b) + c) = (a + (b + c))) & (for a, b holds (a + b) = (b + a)) & ( 0. L) <> ( 1. L) & (for a holds (a * ( 1. L)) = a) & (for a st a <> ( 0. L) holds ex x st (a * x) = ( 1. L)) & (for a holds (a * ( 0. L)) = ( 0. L)) & (for a holds (( 0. L) * a) = ( 0. L)) & (for a, b, c holds ((a * b) * c) = (a * (b * c))) & (for a, b, c holds (a * (b + c)) = ((a * b) + (a * c))) & (for a, b, c holds ((b + c) * a) = ((b * a) + (c * a)))

    proof

      thus L is _Skew-Field implies (for a holds (a + ( 0. L)) = a) & (for a holds ex x st (a + x) = ( 0. L)) & (for a, b, c holds ((a + b) + c) = (a + (b + c))) & (for a, b holds (a + b) = (b + a)) & ( 0. L) <> ( 1. L) & (for a holds (a * ( 1. L)) = a) & (for a st a <> ( 0. L) holds ex x st (a * x) = ( 1. L)) & (for a holds (a * ( 0. L)) = ( 0. L)) & (for a holds (( 0. L) * a) = ( 0. L)) & (for a, b, c holds ((a * b) * c) = (a * (b * c))) & (for a, b, c holds (a * (b + c)) = ((a * b) + (a * c))) & (for a, b, c holds ((b + c) * a) = ((b * a) + (c * a))) by ALGSTR_1: 6, ALGSTR_1: 16, GROUP_1:def 3, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, STRUCT_0:def 8, VECTSP_1:def 7;

      assume

       A1: (for a holds (a + ( 0. L)) = a) & (for a holds ex x st (a + x) = ( 0. L)) & (for a, b, c holds ((a + b) + c) = (a + (b + c))) & (for a, b holds (a + b) = (b + a)) & ( 0. L) <> ( 1. L) & (for a holds (a * ( 1. L)) = a) & (for a st a <> ( 0. L) holds ex x st (a * x) = ( 1. L)) & (for a holds (a * ( 0. L)) = ( 0. L)) & (for a holds (( 0. L) * a) = ( 0. L)) & (for a, b, c holds ((a * b) * c) = (a * (b * c))) & (for a, b, c holds (a * (b + c)) = ((a * b) + (a * c))) & (for a, b, c holds ((b + c) * a) = ((b * a) + (c * a)));

      now

        thus

         A2: for a holds (( 0. L) + a) = a

        proof

          let a;

          

          thus (( 0. L) + a) = (a + ( 0. L)) by A1

          .= a by A1;

        end;

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

        proof

          let a, b;

          consider y such that

           A3: (a + y) = ( 0. L) by A1;

          take x = (y + b);

          

          thus (a + x) = (( 0. L) + b) by A1, A3

          .= b by A2;

        end;

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

        proof

          let a, b;

          consider y such that

           A4: (y + a) = ( 0. L) by A1, ALGSTR_1: 3;

          take x = (b + y);

          

          thus (x + a) = (b + ( 0. L)) by A1, A4

          .= b by A1;

        end;

        thus for a, x, y holds (a + x) = (a + y) implies x = y

        proof

          let a, x, y;

          consider z such that

           A5: (z + a) = ( 0. L) by A1, ALGSTR_1: 3;

          assume (a + x) = (a + y);

          

          then ((z + a) + x) = (z + (a + y)) by A1

          .= ((z + a) + y) by A1;

          

          hence x = (( 0. L) + y) by A2, A5

          .= y by A2;

        end;

        thus for a, x, y holds (x + a) = (y + a) implies x = y

        proof

          let a, x, y;

          consider z such that

           A6: (a + z) = ( 0. L) by A1;

          assume (x + a) = (y + a);

          

          then (x + (a + z)) = ((y + a) + z) by A1

          .= (y + (a + z)) by A1;

          

          hence x = (y + ( 0. L)) by A1, A6

          .= y by A1;

        end;

        thus

         A7: for a holds (( 1. L) * a) = a

        proof

          let a;

          

          thus (( 1. L) * a) = (a * ( 1. L)) by A1, Lm7

          .= a by A1;

        end;

        thus for a, b st a <> ( 0. L) holds ex x st (a * x) = b

        proof

          let a, b;

          assume a <> ( 0. L);

          then

          consider y such that

           A8: (a * y) = ( 1. L) by A1;

          take x = (y * b);

          

          thus (a * x) = (( 1. L) * b) by A1, A8

          .= b by A7;

        end;

        thus for a, b st a <> ( 0. L) holds ex x st (x * a) = b

        proof

          let a, b;

          assume a <> ( 0. L);

          then

          consider y such that

           A9: (y * a) = ( 1. L) by A1, Lm8;

          take x = (b * y);

          

          thus (x * a) = (b * ( 1. L)) by A1, A9

          .= b by A1;

        end;

        thus for a, x, y st a <> ( 0. L) holds (a * x) = (a * y) implies x = y

        proof

          let a, x, y;

          assume a <> ( 0. L);

          then

          consider z such that

           A10: (z * a) = ( 1. L) by A1, Lm8;

          assume (a * x) = (a * y);

          

          then ((z * a) * x) = (z * (a * y)) by A1

          .= ((z * a) * y) by A1;

          

          hence x = (( 1. L) * y) by A7, A10

          .= y by A7;

        end;

        thus for a, x, y st a <> ( 0. L) holds (x * a) = (y * a) implies x = y

        proof

          let a, x, y;

          assume a <> ( 0. L);

          then

          consider z such that

           A11: (a * z) = ( 1. L) by A1;

          assume (x * a) = (y * a);

          

          then (x * (a * z)) = ((y * a) * z) by A1

          .= (y * (a * z)) by A1;

          

          hence x = (y * ( 1. L)) by A1, A11

          .= y by A1;

        end;

      end;

      hence thesis by A1, ALGSTR_1: 6, ALGSTR_1: 16, ALGSTR_1:def 2, GROUP_1:def 3, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, STRUCT_0:def 8, VECTSP_1:def 6, VECTSP_1:def 7;

    end;

    definition

      mode _Field is commutative _Skew-Field;

    end

    theorem :: ALGSTR_2:12

    L is _Field iff (for a holds (a + ( 0. L)) = a) & (for a holds ex x st (a + x) = ( 0. L)) & (for a, b, c holds ((a + b) + c) = (a + (b + c))) & (for a, b holds (a + b) = (b + a)) & ( 0. L) <> ( 1. L) & (for a holds (a * ( 1. L)) = a) & (for a st a <> ( 0. L) holds ex x st (a * x) = ( 1. L)) & (for a holds (a * ( 0. L)) = ( 0. L)) & (for a, b, c holds ((a * b) * c) = (a * (b * c))) & (for a, b, c holds (a * (b + c)) = ((a * b) + (a * c))) & for a, b holds (a * b) = (b * a)

    proof

      thus L is _Field implies (for a holds (a + ( 0. L)) = a) & (for a holds ex x st (a + x) = ( 0. L)) & (for a, b, c holds ((a + b) + c) = (a + (b + c))) & (for a, b holds (a + b) = (b + a)) & ( 0. L) <> ( 1. L) & (for a holds (a * ( 1. L)) = a) & (for a st a <> ( 0. L) holds ex x st (a * x) = ( 1. L)) & (for a holds (a * ( 0. L)) = ( 0. L)) & (for a, b, c holds ((a * b) * c) = (a * (b * c))) & (for a, b, c holds (a * (b + c)) = ((a * b) + (a * c))) & for a, b holds (a * b) = (b * a) by Th11, GROUP_1:def 12;

      assume that

       A1: ((for a holds (a + ( 0. L)) = a) & for a holds ex x st (a + x) = ( 0. L)) & ((for a, b, c holds ((a + b) + c) = (a + (b + c))) & for a, b holds (a + b) = (b + a)) & ((( 0. L) <> ( 1. L) & for a holds (a * ( 1. L)) = a) & for a st a <> ( 0. L) holds ex x st (a * x) = ( 1. L)) and

       A2: for a holds (a * ( 0. L)) = ( 0. L) and

       A3: for a, b, c holds ((a * b) * c) = (a * (b * c)) and

       A4: for a, b, c holds (a * (b + c)) = ((a * b) + (a * c)) and

       A5: for a, b holds (a * b) = (b * a);

      

       A6: for a holds (( 0. L) * a) = ( 0. L)

      proof

        let a;

        

        thus (( 0. L) * a) = (a * ( 0. L)) by A5

        .= ( 0. L) by A2;

      end;

      for a, b, c holds ((b + c) * a) = ((b * a) + (c * a))

      proof

        let a, b, c;

        

        thus ((b + c) * a) = (a * (b + c)) by A5

        .= ((a * b) + (a * c)) by A4

        .= ((b * a) + (a * c)) by A5

        .= ((b * a) + (c * a)) by A5;

      end;

      hence thesis by A1, A2, A3, A4, A5, A6, Th11, GROUP_1:def 12;

    end;