mod_4.miz



    begin

    registration

      let G be non empty addMagma;

      cluster ( id G) -> bijective;

      coherence

      proof

        set f = ( id G);

        ( rng f) = the carrier of G by RELAT_1: 45;

        then f is one-to-one onto by FUNCT_2:def 3;

        hence thesis;

      end;

    end

    reserve A,B,C for non empty set,

f for Function of [:A, B:], C;

    theorem :: MOD_4:1

    for x be Element of A, y be Element of B holds (f . (x,y)) = (( ~ f) . (y,x)) by FUNCT_4:def 8;

    begin

    reserve K for non empty doubleLoopStr;

    definition

      let K;

      :: MOD_4:def1

      func opp K -> strict doubleLoopStr equals doubleLoopStr (# the carrier of K, the addF of K, ( ~ the multF of K), ( 1. K), ( 0. K) #);

      correctness ;

    end

    registration

      let K;

      cluster ( opp K) -> non empty;

      coherence ;

    end

    

     Lm1: for K be well-unital non empty doubleLoopStr holds for h,e be Element of ( opp K) st e = ( 1. K) holds (h * e) = h & (e * h) = h

    proof

      let K be well-unital non empty doubleLoopStr;

      let h,e be Element of ( opp K);

      assume

       A1: e = ( 1. K);

      reconsider a = h, b = e as Element of K;

      

      thus (h * e) = (b * a) by FUNCT_4:def 8

      .= h by A1;

      

      thus (e * h) = (a * b) by FUNCT_4:def 8

      .= h by A1;

    end;

    registration

      let K be well-unital non empty doubleLoopStr;

      cluster ( opp K) -> well-unital;

      coherence by Lm1;

    end

     Lm2:

    now

      let K be add-associative right_zeroed right_complementable non empty doubleLoopStr;

      set L = ( opp K);

      thus for x,y,z be Scalar of L holds ((x + y) + z) = (x + (y + z)) & (x + ( 0. L)) = x

      proof

        let x,y,z be Scalar of L;

        reconsider a = x, b = y, c = z as Scalar of K;

        

        thus ((x + y) + z) = ((a + b) + c)

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

        .= (x + (y + z));

        

        thus (x + ( 0. L)) = (a + ( 0. K))

        .= x by RLVECT_1:def 4;

      end;

    end;

    registration

      let K be add-associative right_complementable right_zeroed non empty doubleLoopStr;

      cluster ( opp K) -> add-associative right_zeroed right_complementable;

      coherence

      proof

        thus for x,y,z be Element of ( opp K) holds (x + (y + z)) = ((x + y) + z) by Lm2;

        thus for x be Element of ( opp K) holds (x + ( 0. ( opp K))) = x by Lm2;

        let a be Element of ( opp K);

        reconsider x = a as Element of K;

        reconsider y = ( - x) as Element of ( opp K);

        take y;

        

        thus (a + y) = (x + ( - x))

        .= ( 0. ( opp K)) by RLVECT_1: 5;

      end;

    end

    

     Lm3: for K be add-associative right_zeroed right_complementable non empty doubleLoopStr holds for x,y be Scalar of K, a,b be Scalar of ( opp K) st x = a & y = b holds (x + y) = (a + b) & (x * y) = (b * a) & ( - x) = ( - a)

    proof

      let K be add-associative right_zeroed right_complementable non empty doubleLoopStr;

      let x,y be Scalar of K, a,b be Scalar of ( opp K) such that

       A1: x = a and

       A2: y = b;

      thus (x + y) = (a + b) by A1, A2;

      thus (x * y) = (b * a) by A1, A2, FUNCT_4:def 8;

      reconsider c = ( - a) as Element of K;

      (c + x) = (( - a) + a) by A1

      .= ( 0. ( opp K)) by RLVECT_1: 5

      .= ( 0. K);

      hence thesis by RLVECT_1: 6;

    end;

    theorem :: MOD_4:2

     the addLoopStr of ( opp K) = the addLoopStr of K & (K is add-associative right_zeroed right_complementable implies ( comp ( opp K)) = ( comp K)) & for x be set holds x is Scalar of ( opp K) iff x is Scalar of K

    proof

      thus the addLoopStr of ( opp K) = the addLoopStr of K;

      hereby

        assume

         A1: K is add-associative right_zeroed right_complementable;

        

         A2: for x be object st x in the carrier of K holds (( comp ( opp K)) . x) = (( comp K) . x)

        proof

          let x be object;

          assume x in the carrier of K;

          then

          reconsider y = x as Element of K;

          reconsider z = y as Element of ( opp K);

          

           A3: ( - y) = ( - z) by A1, Lm3;

          

          thus (( comp ( opp K)) . x) = ( - z) by VECTSP_1:def 13

          .= (( comp K) . x) by A3, VECTSP_1:def 13;

        end;

        ( dom ( comp ( opp K))) = the carrier of K & ( dom ( comp K)) = the carrier of K by FUNCT_2:def 1;

        hence ( comp ( opp K)) = ( comp K) by A2, FUNCT_1: 2;

      end;

      let x be set;

      thus thesis;

    end;

    

     Lm4: for K be non empty doubleLoopStr holds for x,y,z,u be Scalar of K, a,b,c,d be Scalar of ( opp K) st x = a & y = b & z = c & u = d holds ((x + y) + z) = ((a + b) + c) & (x + (y + z)) = (a + (b + c)) & ((x * y) * z) = (c * (b * a)) & (x * (y * z)) = ((c * b) * a) & (x * (y + z)) = ((b + c) * a) & ((y + z) * x) = (a * (b + c)) & ((x * y) + (z * u)) = ((b * a) + (d * c))

    proof

      let K be non empty doubleLoopStr;

      let x,y,z,u be Scalar of K, a,b,c,d be Scalar of ( opp K);

      assume that

       A1: x = a & y = b & z = c and

       A2: u = d;

      (x * y) = (b * a) & (y * z) = (c * b) by A1, FUNCT_4:def 8;

      hence thesis by A1, A2, FUNCT_4:def 8;

    end;

    theorem :: MOD_4:3

    (for K be unital non empty doubleLoopStr holds ( 1. K) = ( 1. ( opp K))) & for K be add-associative right_zeroed right_complementable non empty doubleLoopStr holds ( 0. K) = ( 0. ( opp K)) & for x,y,z,u be Scalar of K, a,b,c,d be Scalar of ( opp K) st x = a & y = b & z = c & u = d holds (x + y) = (a + b) & (x * y) = (b * a) & ( - x) = ( - a) & ((x + y) + z) = ((a + b) + c) & (x + (y + z)) = (a + (b + c)) & ((x * y) * z) = (c * (b * a)) & (x * (y * z)) = ((c * b) * a) & (x * (y + z)) = ((b + c) * a) & ((y + z) * x) = (a * (b + c)) & ((x * y) + (z * u)) = ((b * a) + (d * c)) by Lm3, Lm4;

    registration

      let K be Abelian non empty doubleLoopStr;

      cluster ( opp K) -> Abelian;

      coherence

      proof

        let x,y be Element of ( opp K);

        reconsider a = x, b = y as Element of K;

        

        thus (x + y) = (a + b)

        .= (b + a)

        .= (y + x);

      end;

    end

    registration

      let K be add-associative non empty doubleLoopStr;

      cluster ( opp K) -> add-associative;

      coherence

      proof

        let x,y,z be Element of ( opp K);

        reconsider a = x, b = y, c = z as Element of K;

        

        thus ((x + y) + z) = ((a + b) + c)

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

        .= (x + (y + z));

      end;

    end

    registration

      let K be right_zeroed non empty doubleLoopStr;

      cluster ( opp K) -> right_zeroed;

      coherence

      proof

        let x be Element of ( opp K);

        reconsider a = x as Element of K;

        

        thus (x + ( 0. ( opp K))) = (a + ( 0. K))

        .= x by RLVECT_1:def 4;

      end;

    end

    registration

      let K be right_complementable non empty doubleLoopStr;

      cluster ( opp K) -> right_complementable;

      coherence

      proof

        let x be Element of ( opp K);

        reconsider a = x as Element of K;

        consider b be Element of K such that

         A1: (a + b) = ( 0. K) by ALGSTR_0:def 11;

        reconsider y = b as Element of ( opp K);

        take y;

        thus thesis by A1;

      end;

    end

    registration

      let K be associative non empty doubleLoopStr;

      cluster ( opp K) -> associative;

      coherence

      proof

        let x,y,z be Element of ( opp K);

        reconsider a = x, b = y, c = z as Element of K;

        

        thus ((x * y) * z) = (c * (b * a)) by Lm4

        .= ((c * b) * a) by GROUP_1:def 3

        .= (x * (y * z)) by Lm4;

      end;

    end

    registration

      let K be distributive non empty doubleLoopStr;

      cluster ( opp K) -> distributive;

      coherence

      proof

        let x,y,z be Element of ( opp K);

        reconsider a = x, b = y, c = z as Element of K;

        

        thus (x * (y + z)) = ((b + c) * a) by Lm4

        .= ((b * a) + (c * a)) by VECTSP_1:def 7

        .= ((x * y) + (x * z)) by Lm4;

        

        thus ((y + z) * x) = (a * (b + c)) by Lm4

        .= ((a * b) + (a * c)) by VECTSP_1:def 7

        .= ((y * x) + (z * x)) by Lm4;

      end;

    end

    theorem :: MOD_4:4

    for K be Ring holds ( opp K) is strict Ring;

    theorem :: MOD_4:5

    

     Th5: for K be Skew-Field holds ( opp K) is Skew-Field

    proof

      let K be Skew-Field;

      set L = ( opp K);

      for x be Scalar of L holds (x <> ( 0. L) implies ex y be Scalar of L st (y * x) = ( 1_ L)) & ( 0. L) <> ( 1_ L)

      proof

        let x be Scalar of L;

        x <> ( 0. L) implies ex y be Scalar of L st (y * x) = ( 1_ L)

        proof

          reconsider a = x as Scalar of K;

          assume x <> ( 0. L);

          then

          consider b be Scalar of K such that

           A1: (a * b) = ( 1_ K) by VECTSP_2: 6;

          reconsider y = b as Scalar of ( opp K);

          take y;

          thus thesis by A1, Lm3;

        end;

        hence thesis;

      end;

      hence thesis by STRUCT_0:def 8, VECTSP_1:def 9;

    end;

    registration

      let K be Skew-Field;

      cluster ( opp K) -> non degenerated almost_left_invertible associative Abelian add-associative right_zeroed right_complementable unital distributive;

      coherence by Th5;

    end

    

     Lm5: for F be commutative non empty doubleLoopStr, x,y be Element of F holds (x * y) = (y * x);

    theorem :: MOD_4:6

    for K be Field holds ( opp K) is strict Field

    proof

      let K be Field;

      set L = ( opp K);

      for x,y be Scalar of L holds (x * y) = (y * x)

      proof

        let x,y be Scalar of L;

        reconsider a = x, b = y as Scalar of K;

        (b * a) = (x * y) by Lm3;

        hence thesis by Lm3;

      end;

      hence thesis by GROUP_1:def 12;

    end;

    registration

      let K be Field;

      cluster ( opp K) -> almost_left_invertible;

      coherence ;

    end

    begin

    reserve V for non empty ModuleStr over K;

    definition

      let K, V;

      :: MOD_4:def2

      func opp (V) -> strict RightModStr over ( opp K) means

      : Def2: for o be Function of [:the carrier of V, the carrier of ( opp K):], the carrier of V st o = ( ~ the lmult of V) holds it = RightModStr (# the carrier of V, the addF of V, ( 0. V), o #);

      existence

      proof

        reconsider o = ( ~ the lmult of V) as Function of [:the carrier of V, the carrier of ( opp K):], the carrier of V;

        take RightModStr (# the carrier of V, the addF of V, ( 0. V), o #);

        thus thesis;

      end;

      uniqueness

      proof

        reconsider o = ( ~ the lmult of V) as Function of [:the carrier of V, the carrier of ( opp K):], the carrier of V;

        let M1,M2 be strict RightModStr over ( opp K) such that

         A1: for o be Function of [:the carrier of V, the carrier of ( opp K):], the carrier of V st o = ( ~ the lmult of V) holds M1 = RightModStr (# the carrier of V, the addF of V, ( 0. V), o #) and

         A2: for o be Function of [:the carrier of V, the carrier of ( opp K):], the carrier of V st o = ( ~ the lmult of V) holds M2 = RightModStr (# the carrier of V, the addF of V, ( 0. V), o #);

        

        thus M1 = RightModStr (# the carrier of V, the addF of V, ( 0. V), o #) by A1

        .= M2 by A2;

      end;

    end

    registration

      let K, V;

      cluster ( opp V) -> non empty;

      coherence

      proof

        reconsider o = ( ~ the lmult of V) as Function of [:the carrier of V, the carrier of ( opp K):], the carrier of V;

        ( opp V) = RightModStr (# the carrier of V, the addF of V, ( 0. V), o #) by Def2;

        hence the carrier of ( opp V) is non empty;

      end;

    end

    theorem :: MOD_4:7

    

     Th7: the addLoopStr of ( opp V) = the addLoopStr of V & for x be set holds x is Vector of V iff x is Vector of ( opp V)

    proof

      reconsider p = ( ~ the lmult of V) as Function of [:the carrier of V, the carrier of ( opp K):], the carrier of V;

      

       A1: ( opp V) = RightModStr (# the carrier of V, the addF of V, ( 0. V), p #) by Def2;

      hence the addLoopStr of ( opp V) = the addLoopStr of V;

      let x be set;

      thus thesis by A1;

    end;

    definition

      let K, V;

      let o be Function of [:the carrier of K, the carrier of V:], the carrier of V;

      :: MOD_4:def3

      func opp (o) -> Function of [:the carrier of ( opp V), the carrier of ( opp K):], the carrier of ( opp V) equals ( ~ o);

      coherence

      proof

         the addLoopStr of ( opp V) = the addLoopStr of V by Th7;

        hence thesis;

      end;

    end

    theorem :: MOD_4:8

    

     Th8: the rmult of ( opp V) = ( opp the lmult of V)

    proof

      reconsider p = ( ~ the lmult of V) as Function of [:the carrier of V, the carrier of ( opp K):], the carrier of V;

      ( opp V) = RightModStr (# the carrier of V, the addF of V, ( 0. V), p #) by Def2;

      hence thesis;

    end;

    reserve W for non empty RightModStr over K;

    definition

      let K, W;

      :: MOD_4:def4

      func opp (W) -> strict ModuleStr over ( opp K) means

      : Def4: for o be Function of [:the carrier of ( opp K), the carrier of W:], the carrier of W st o = ( ~ the rmult of W) holds it = ModuleStr (# the carrier of W, the addF of W, ( 0. W), o #);

      existence

      proof

        reconsider o = ( ~ the rmult of W) as Function of [:the carrier of ( opp K), the carrier of W:], the carrier of W;

        take ModuleStr (# the carrier of W, the addF of W, ( 0. W), o #);

        thus thesis;

      end;

      uniqueness

      proof

        reconsider o = ( ~ the rmult of W) as Function of [:the carrier of ( opp K), the carrier of W:], the carrier of W;

        let M1,M2 be strict ModuleStr over ( opp K) such that

         A1: for o be Function of [:the carrier of ( opp K), the carrier of W:], the carrier of W st o = ( ~ the rmult of W) holds M1 = ModuleStr (# the carrier of W, the addF of W, ( 0. W), o #) and

         A2: for o be Function of [:the carrier of ( opp K), the carrier of W:], the carrier of W st o = ( ~ the rmult of W) holds M2 = ModuleStr (# the carrier of W, the addF of W, ( 0. W), o #);

        

        thus M1 = ModuleStr (# the carrier of W, the addF of W, ( 0. W), o #) by A1

        .= M2 by A2;

      end;

    end

    registration

      let K, W;

      cluster ( opp W) -> non empty;

      coherence

      proof

        reconsider o = ( ~ the rmult of W) as Function of [:the carrier of ( opp K), the carrier of W:], the carrier of W;

        ( opp W) = ModuleStr (# the carrier of W, the addF of W, ( 0. W), o #) by Def4;

        hence the carrier of ( opp W) is non empty;

      end;

    end

    theorem :: MOD_4:9

    

     Th9: the addLoopStr of ( opp W) = the addLoopStr of W & for x be set holds x is Vector of W iff x is Vector of ( opp W)

    proof

      reconsider p = ( ~ the rmult of W) as Function of [:the carrier of ( opp K), the carrier of W:], the carrier of W;

      

       A1: ( opp W) = ModuleStr (# the carrier of W, the addF of W, ( 0. W), p #) by Def4;

      hence the addLoopStr of ( opp W) = the addLoopStr of W;

      let x be set;

      thus thesis by A1;

    end;

    definition

      let K, W;

      let o be Function of [:the carrier of W, the carrier of K:], the carrier of W;

      :: MOD_4:def5

      func opp (o) -> Function of [:the carrier of ( opp K), the carrier of ( opp W):], the carrier of ( opp W) equals ( ~ o);

      coherence

      proof

         the addLoopStr of ( opp W) = the addLoopStr of W by Th9;

        then

        reconsider o9 = ( ~ o) as Function of [:the carrier of ( opp K), the carrier of ( opp W):], the carrier of ( opp W);

        o9 is Function of [:the carrier of ( opp K), the carrier of ( opp W):], the carrier of ( opp W);

        hence thesis;

      end;

    end

    theorem :: MOD_4:10

    

     Th10: the lmult of ( opp W) = ( opp the rmult of W)

    proof

      reconsider p = ( ~ the rmult of W) as Function of [:the carrier of ( opp K), the carrier of W:], the carrier of W;

      ( opp W) = ModuleStr (# the carrier of W, the addF of W, ( 0. W), p #) by Def4;

      hence thesis;

    end;

    theorem :: MOD_4:11

    for o be Function of [:the carrier of K, the carrier of V:], the carrier of V, x be Scalar of K, y be Scalar of ( opp K), v be Vector of V, w be Vector of ( opp V) st x = y & v = w holds (( opp o) . (w,y)) = (o . (x,v)) by FUNCT_4:def 8;

    theorem :: MOD_4:12

    

     Th12: for K,L be Ring, V be non empty ModuleStr over K holds for W be non empty RightModStr over L holds for x be Scalar of K, y be Scalar of L, v be Vector of V, w be Vector of W st L = ( opp K) & W = ( opp V) & x = y & v = w holds (w * y) = (x * v)

    proof

      let K,L be Ring, V be non empty ModuleStr over K;

      let W be non empty RightModStr over L;

      let x be Scalar of K, y be Scalar of L, v be Vector of V, w be Vector of W such that

       A1: L = ( opp K) & W = ( opp V) and

       A2: x = y & v = w;

      set o = the lmult of V;

      ( opp o) = the rmult of ( opp V) by Th8;

      

      hence (w * y) = (( opp o) . (w,y)) by A1, VECTSP_2:def 7

      .= (x * v) by A2, FUNCT_4:def 8;

    end;

    theorem :: MOD_4:13

    

     Th13: for K,L be Ring, V be non empty ModuleStr over K holds for W be non empty RightModStr over L holds for v1,v2 be Vector of V, w1,w2 be Vector of W st W = ( opp V) & v1 = w1 & v2 = w2 holds (w1 + w2) = (v1 + v2)

    proof

      let K,L be Ring, V be non empty ModuleStr over K;

      

       A1: the addLoopStr of ( opp V) = the addLoopStr of V by Th7;

      let W be non empty RightModStr over L, v1,v2 be Vector of V, w1,w2 be Vector of W;

      assume W = ( opp V) & v1 = w1 & v2 = w2;

      hence thesis by A1;

    end;

    theorem :: MOD_4:14

    for o be Function of [:the carrier of W, the carrier of K:], the carrier of W, x be Scalar of K, y be Scalar of ( opp K), v be Vector of W, w be Vector of ( opp W) st x = y & v = w holds (( opp o) . (y,w)) = (o . (v,x)) by FUNCT_4:def 8;

    theorem :: MOD_4:15

    

     Th15: for K,L be Ring, V be non empty ModuleStr over K holds for W be non empty RightModStr over L holds for x be Scalar of K, y be Scalar of L, v be Vector of V, w be Vector of W st V = ( opp W) & x = y & v = w holds (w * y) = (x * v)

    proof

      let K,L be Ring, V be non empty ModuleStr over K;

      let W be non empty RightModStr over L;

      let x be Scalar of K, y be Scalar of L, v be Vector of V, w be Vector of W such that

       A1: V = ( opp W) & x = y & v = w;

      set o = the rmult of W;

      

       A2: ( opp o) = the lmult of ( opp W) by Th10;

      

      thus (w * y) = (o . (w,y)) by VECTSP_2:def 7

      .= (x * v) by A1, A2, FUNCT_4:def 8;

    end;

    theorem :: MOD_4:16

    

     Th16: for K,L be Ring, V be non empty ModuleStr over K holds for W be non empty RightModStr over L holds for v1,v2 be Vector of V, w1,w2 be Vector of W st V = ( opp W) & v1 = w1 & v2 = w2 holds (w1 + w2) = (v1 + v2)

    proof

      let K,L be Ring, V be non empty ModuleStr over K;

      let W be non empty RightModStr over L;

      

       A1: the addLoopStr of ( opp W) = the addLoopStr of W by Th9;

      let v1,v2 be Vector of V, w1,w2 be Vector of W;

      assume V = ( opp W) & v1 = w1 & v2 = w2;

      hence thesis by A1;

    end;

    theorem :: MOD_4:17

    for K be strict non empty doubleLoopStr, V be non empty ModuleStr over K holds ( opp ( opp V)) = the ModuleStr of V

    proof

      let K be strict non empty doubleLoopStr, V be non empty ModuleStr over K;

      set W = ( opp V);

      

       A1: ( opp ( opp K)) = K by FUNCT_4: 53;

      

       A2: ( opp the rmult of W) = ( opp ( opp the lmult of V)) by Th8

      .= the lmult of V by FUNCT_4: 53;

       the addLoopStr of ( opp W) = the addLoopStr of W by Th9

      .= the addLoopStr of V by Th7;

      hence thesis by A2, A1, Th10;

    end;

    theorem :: MOD_4:18

    for K be strict non empty doubleLoopStr, W be non empty RightModStr over K holds ( opp ( opp W)) = the RightModStr of W

    proof

      let K be strict non empty doubleLoopStr, W be non empty RightModStr over K;

      set V = ( opp W);

      

       A1: ( opp ( opp K)) = K by FUNCT_4: 53;

      

       A2: ( opp the lmult of V) = ( opp ( opp the rmult of W)) by Th10

      .= the rmult of W by FUNCT_4: 53;

       the addLoopStr of ( opp V) = the addLoopStr of V by Th7

      .= the addLoopStr of W by Th9;

      hence thesis by A2, A1, Th8;

    end;

    theorem :: MOD_4:19

    

     Th19: for K be Ring, V be LeftMod of K holds ( opp V) is strict RightMod of ( opp K)

    proof

      let K be Ring, V be LeftMod of K;

      set R = ( opp K);

      reconsider W = ( opp V) as non empty RightModStr over R;

      

       A1: the addLoopStr of ( opp V) = the addLoopStr of V by Th7;

      then

       A2: for a,b be Element of ( opp V) holds for x,y be Element of V st x = a & b = y holds (a + b) = (x + y);

      

       A3: ( opp V) is Abelian add-associative right_zeroed right_complementable

      proof

        thus ( opp V) is Abelian

        proof

          let a,b be Element of ( opp V);

          reconsider x = a, y = b as Element of V by Th7;

          

          thus (a + b) = (y + x) by A2

          .= (b + a) by A1;

        end;

        hereby

          let a,b,c be Element of ( opp V);

          reconsider x = a, y = b, z = c as Element of V by Th7;

          

          thus ((a + b) + c) = ((x + y) + z) by A1

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

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

        end;

        hereby

          let a be Element of ( opp V);

          reconsider x = a as Element of V by Th7;

          

          thus (a + ( 0. ( opp V))) = (x + ( 0. V)) by A1

          .= a by RLVECT_1: 4;

        end;

        let a be Element of ( opp V);

        reconsider x = a as Element of V by Th7;

        consider b be Element of V such that

         A4: (x + b) = ( 0. V) by ALGSTR_0:def 11;

        reconsider b9 = b as Element of ( opp V) by Th7;

        take b9;

        thus thesis by A1, A4;

      end;

      now

        let x,y be Scalar of R, v,w be Vector of W;

        reconsider p = v, q = w as Vector of V by Th7;

        reconsider a = x, b = y as Scalar of K;

        

         A5: (b * p) = (v * y) by Th12;

        

         A6: (a * q) = (w * x) by Th12;

        

         A7: (a * p) = (v * x) by Th12;

        (v + w) = (p + q) by Th13;

        

        hence ((v + w) * x) = (a * (p + q)) by Th12

        .= ((a * p) + (a * q)) by VECTSP_1:def 14

        .= ((v * x) + (w * x)) by A7, A6, Th13;

        

        thus (v * (x + y)) = ((a + b) * p) by Th12

        .= ((a * p) + (b * p)) by VECTSP_1:def 15

        .= ((v * x) + (v * y)) by A5, A7, Th13;

        

        thus (v * (y * x)) = ((a * b) * p) by Lm3, Th12

        .= (a * (b * p)) by VECTSP_1:def 16

        .= ((v * y) * x) by A5, Th12;

        

        thus (v * ( 1_ R)) = (( 1_ K) * p) by Th12

        .= v by VECTSP_1:def 17;

      end;

      hence thesis by A3, VECTSP_2:def 9;

    end;

    registration

      let K be Ring, V be LeftMod of K;

      cluster ( opp V) -> Abelian add-associative right_zeroed right_complementable RightMod-like;

      coherence by Th19;

    end

    theorem :: MOD_4:20

    

     Th20: for K be Ring, W be RightMod of K holds ( opp W) is strict LeftMod of ( opp K)

    proof

      let K be Ring, W be RightMod of K;

      set R = ( opp K);

      reconsider V = ( opp W) as non empty ModuleStr over R;

      

       A1: the addLoopStr of ( opp W) = the addLoopStr of W by Th9;

      then

       A2: for a,b be Element of ( opp W) holds for x,y be Element of W st x = a & b = y holds (a + b) = (x + y);

      

       A3: ( opp W) is Abelian add-associative right_zeroed right_complementable

      proof

        thus ( opp W) is Abelian

        proof

          let a,b be Element of ( opp W);

          reconsider x = a, y = b as Element of W by Th9;

          

          thus (a + b) = (y + x) by A2

          .= (b + a) by A1;

        end;

        hereby

          let a,b,c be Element of ( opp W);

          reconsider x = a, y = b, z = c as Element of W by Th9;

          

          thus ((a + b) + c) = ((x + y) + z) by A1

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

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

        end;

        hereby

          let a be Element of ( opp W);

          reconsider x = a as Element of W by Th9;

          

          thus (a + ( 0. ( opp W))) = (x + ( 0. W)) by A1

          .= a by RLVECT_1: 4;

        end;

        let a be Element of ( opp W);

        reconsider x = a as Element of W by Th9;

        consider b be Element of W such that

         A4: (x + b) = ( 0. W) by ALGSTR_0:def 11;

        reconsider b9 = b as Element of ( opp W) by Th9;

        take b9;

        thus thesis by A1, A4;

      end;

      now

        let x,y be Scalar of R, v,w be Vector of V;

        reconsider p = v, q = w as Vector of W by Th9;

        reconsider a = x, b = y as Scalar of K;

        

         A5: (p * b) = (y * v) by Th15;

        

         A6: (q * a) = (x * w) by Th15;

        

         A7: (p * a) = (x * v) by Th15;

        (v + w) = (p + q) by Th16;

        

        hence (x * (v + w)) = ((p + q) * a) by Th15

        .= ((p * a) + (q * a)) by VECTSP_2:def 9

        .= ((x * v) + (x * w)) by A7, A6, Th16;

        

        thus ((x + y) * v) = (p * (a + b)) by Th15

        .= ((p * a) + (p * b)) by VECTSP_2:def 9

        .= ((x * v) + (y * v)) by A5, A7, Th16;

        (x * y) = (b * a) by Lm3;

        

        hence ((x * y) * v) = (p * (b * a)) by Th15

        .= ((p * b) * a) by VECTSP_2:def 9

        .= (x * (y * v)) by A5, Th15;

        

        thus (( 1_ R) * v) = (p * ( 1_ K)) by Th15

        .= v by VECTSP_2:def 9;

      end;

      hence thesis by A3, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17;

    end;

    registration

      let K be Ring, W be RightMod of K;

      cluster ( opp W) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence by Th20;

    end

    begin

    definition

      let K,L be non empty multMagma;

      let IT be Function of K, L;

      :: MOD_4:def6

      attr IT is antimultiplicative means

      : Def6: for x,y be Scalar of K holds (IT . (x * y)) = ((IT . y) * (IT . x));

    end

    definition

      let K,L be non empty doubleLoopStr;

      let IT be Function of K, L;

      :: MOD_4:def7

      attr IT is antilinear means IT is additive antimultiplicative unity-preserving;

    end

    definition

      let K,L be non empty doubleLoopStr;

      let IT be Function of K, L;

      :: MOD_4:def8

      attr IT is monomorphism means IT is linear one-to-one;

      :: MOD_4:def9

      attr IT is antimonomorphism means IT is antilinear one-to-one;

      :: MOD_4:def10

      attr IT is epimorphism means IT is linear onto;

      :: MOD_4:def11

      attr IT is antiepimorphism means IT is antilinear onto;

    end

    definition

      let K,L be non empty doubleLoopStr;

      let IT be Function of K, L;

      :: MOD_4:def12

      attr IT is isomorphism means IT is monomorphism onto;

      :: MOD_4:def13

      attr IT is antiisomorphism means IT is antimonomorphism onto;

    end

    registration

      let K,L be non empty doubleLoopStr;

      cluster antilinear -> additive antimultiplicative unity-preserving for Function of K, L;

      coherence ;

      cluster additive antimultiplicative unity-preserving -> antilinear for Function of K, L;

      coherence ;

      cluster monomorphism -> linear one-to-one for Function of K, L;

      coherence ;

      cluster linear one-to-one -> monomorphism for Function of K, L;

      coherence ;

      cluster antimonomorphism -> antilinear one-to-one for Function of K, L;

      coherence ;

      cluster antilinear one-to-one -> antimonomorphism for Function of K, L;

      coherence ;

      cluster epimorphism -> linear onto for Function of K, L;

      coherence ;

      cluster linear onto -> epimorphism for Function of K, L;

      coherence ;

      cluster antiepimorphism -> antilinear onto for Function of K, L;

      coherence ;

      cluster antilinear onto -> antiepimorphism for Function of K, L;

      coherence ;

      cluster isomorphism -> monomorphism onto for Function of K, L;

      coherence ;

      cluster monomorphism onto -> isomorphism for Function of K, L;

      coherence ;

      cluster antiisomorphism -> antimonomorphism onto for Function of K, L;

      coherence ;

      cluster antimonomorphism onto -> antiisomorphism for Function of K, L;

      coherence ;

    end

    definition

      let K be non empty doubleLoopStr;

      let IT be Function of K, K;

      :: MOD_4:def14

      attr IT is endomorphism means IT is linear;

      :: MOD_4:def15

      attr IT is antiendomorphism means IT is antilinear;

    end

    registration

      let K be non empty doubleLoopStr;

      cluster endomorphism -> linear for Function of K, K;

      coherence ;

      cluster linear -> endomorphism for Function of K, K;

      coherence ;

      cluster antiendomorphism -> antilinear for Function of K, K;

      coherence ;

      cluster antilinear -> antiendomorphism for Function of K, K;

      coherence ;

    end

    reserve J for Function of K, K;

    theorem :: MOD_4:21

    J is isomorphism iff J is additive & (for x,y be Scalar of K holds (J . (x * y)) = ((J . x) * (J . y))) & (J . ( 1_ K)) = ( 1_ K) & J is one-to-one onto

    proof

      thus J is isomorphism implies J is additive & (for x,y be Scalar of K holds (J . (x * y)) = ((J . x) * (J . y))) & (J . ( 1_ K)) = ( 1_ K) & J is one-to-one onto by GROUP_1:def 13, GROUP_6:def 6;

      assume (J is additive & for x,y be Scalar of K holds (J . (x * y)) = ((J . x) * (J . y))) & (J . ( 1_ K)) = ( 1_ K);

      then J is additive multiplicative unity-preserving;

      hence thesis;

    end;

    theorem :: MOD_4:22

    

     Th22: J is antiisomorphism iff J is additive & (for x,y be Scalar of K holds (J . (x * y)) = ((J . y) * (J . x))) & (J . ( 1_ K)) = ( 1_ K) & J is one-to-one & J is onto

    proof

      thus J is antiisomorphism implies J is additive & (for x,y be Scalar of K holds (J . (x * y)) = ((J . y) * (J . x))) & (J . ( 1_ K)) = ( 1_ K) & J is one-to-one & J is onto by Def6, GROUP_1:def 13;

      assume (J is additive & for x,y be Scalar of K holds (J . (x * y)) = ((J . y) * (J . x))) & (J . ( 1_ K)) = ( 1_ K);

      then J is additive antimultiplicative unity-preserving;

      hence thesis;

    end;

    registration

      let K;

      cluster ( id K) -> isomorphism;

      coherence ;

    end

    reserve K,L for Ring;

    reserve J for Function of K, L;

    reserve x,y for Scalar of K;

    

     Lm6: J is additive implies (J . ( 0. K)) = ( 0. L)

    proof

      set a = ( 0. K);

      assume

       A1: J is additive;

      (a + a) = a by RLVECT_1: 4;

      

      then ((J . a) + (J . a)) = (J . a) by A1

      .= ((J . a) + ( 0. L)) by RLVECT_1: 4;

      hence thesis by RLVECT_1: 8;

    end;

    

     Lm7: J is linear implies (J . ( - x)) = ( - (J . x))

    proof

      set a = ( 0. K), b = ( 0. L), y = (J . x);

      

       A1: (x + ( - x)) = a by RLVECT_1: 5;

      

       A2: (y + ( - y)) = b by RLVECT_1: 5;

      assume

       A3: J is linear;

      

      then (y + (J . ( - x))) = (J . a) by A1, VECTSP_1:def 20

      .= b by A3, Lm6;

      hence thesis by A2, RLVECT_1: 8;

    end;

    

     Lm8: J is linear implies (J . (x - y)) = ((J . x) - (J . y))

    proof

      assume

       A1: J is linear;

      

      hence (J . (x - y)) = ((J . x) + (J . ( - y))) by VECTSP_1:def 20

      .= ((J . x) - (J . y)) by A1, Lm7;

    end;

    theorem :: MOD_4:23

    J is linear implies (J . ( 0. K)) = ( 0. L) & (J . ( - x)) = ( - (J . x)) & (J . (x - y)) = ((J . x) - (J . y)) by Lm6, Lm7, Lm8;

    

     Lm9: J is antilinear implies (J . ( 0. K)) = ( 0. L)

    proof

      set a = ( 0. K);

      

       A1: (a + a) = a by RLVECT_1: 4;

      assume J is antilinear;

      

      then ((J . a) + (J . a)) = (J . a) by A1, VECTSP_1:def 20

      .= ((J . a) + ( 0. L)) by RLVECT_1: 4;

      hence thesis by RLVECT_1: 8;

    end;

    

     Lm10: J is antilinear implies (J . ( - x)) = ( - (J . x))

    proof

      assume

       A1: J is antilinear;

      set a = ( 0. K), b = ( 0. L), y = (J . x);

      

       A2: (y + ( - y)) = b by RLVECT_1: 5;

      (x + ( - x)) = a by RLVECT_1: 5;

      

      then (y + (J . ( - x))) = (J . a) by A1, VECTSP_1:def 20

      .= b by A1, Lm9;

      hence thesis by A2, RLVECT_1: 8;

    end;

    

     Lm11: J is antilinear implies (J . (x - y)) = ((J . x) - (J . y))

    proof

      assume

       A1: J is antilinear;

      

      hence (J . (x - y)) = ((J . x) + (J . ( - y))) by VECTSP_1:def 20

      .= ((J . x) - (J . y)) by A1, Lm10;

    end;

    theorem :: MOD_4:24

    J is antilinear implies (J . ( 0. K)) = ( 0. L) & (J . ( - x)) = ( - (J . x)) & (J . (x - y)) = ((J . x) - (J . y)) by Lm9, Lm10, Lm11;

    theorem :: MOD_4:25

    for K be Ring holds ( id K) is antiisomorphism iff K is comRing

    proof

      let K be Ring;

      set J = ( id K);

       A1:

      now

        assume

         A2: K is comRing;

        

         A3: for x,y be Scalar of K holds (J . (x * y)) = ((J . y) * (J . x)) by A2, Lm5;

        (J . ( 1_ K)) = ( 1_ K);

        hence J is antiisomorphism by A3, Th22;

      end;

      now

        assume

         A4: J is antiisomorphism;

        for x,y be Element of K holds (x * y) = (y * x)

        proof

          let x,y be Element of K;

          

           A5: (J . y) = y;

          (J . (x * y)) = (x * y) & (J . x) = x;

          hence thesis by A4, A5, Th22;

        end;

        hence K is comRing by GROUP_1:def 12;

      end;

      hence thesis by A1;

    end;

    theorem :: MOD_4:26

    for K be Skew-Field holds ( id K) is antiisomorphism iff K is Field

    proof

      let K be Skew-Field;

      set J = ( id K);

       A1:

      now

        assume

         A2: K is Field;

        

         A3: for x,y be Scalar of K holds (J . (x * y)) = ((J . y) * (J . x)) by A2, GROUP_1:def 12;

        (J . ( 1_ K)) = ( 1_ K);

        hence J is antiisomorphism by A3, Th22;

      end;

      now

        assume

         A4: J is antiisomorphism;

        for x,y be Scalar of K holds (x * y) = (y * x)

        proof

          let x,y be Scalar of K;

          

           A5: (J . y) = y;

          (J . (x * y)) = (x * y) & (J . x) = x;

          hence thesis by A4, A5, Th22;

        end;

        hence K is Field by GROUP_1:def 12;

      end;

      hence thesis by A1;

    end;

    begin

    definition

      let K,L be non empty doubleLoopStr, J be Function of K, L;

      :: MOD_4:def16

      func opp (J) -> Function of K, ( opp L) equals J;

      coherence ;

    end

    reserve K,L for add-associative right_zeroed right_complementable non empty doubleLoopStr;

    reserve J for Function of K, L;

    reserve K for add-associative right_zeroed right_complementable non empty doubleLoopStr;

    reserve L for add-associative right_zeroed right_complementable well-unital non empty doubleLoopStr;

    reserve J for Function of K, L;

    

     Lm12: J is linear implies ( opp J) is additive

    proof

      set J9 = ( opp J);

      assume

       A1: J is linear;

      let x,y be Scalar of K;

      

      thus (J9 . (x + y)) = ((J . x) + (J . y)) by A1, VECTSP_1:def 20

      .= ((J9 . x) + (J9 . y));

    end;

    ::$Canceled

    theorem :: MOD_4:28

    

     Th27: J is linear iff ( opp J) is antilinear

    proof

      set J9 = ( opp J), L9 = ( opp L);

       A1:

      now

        assume

         A2: J is linear;

        

         A3: for x,y be Scalar of K holds (J9 . (x * y)) = ((J9 . y) * (J9 . x))

        proof

          let x,y be Scalar of K;

          

          thus (J9 . (x * y)) = ((J . x) * (J . y)) by A2, GROUP_6:def 6

          .= ((J9 . y) * (J9 . x)) by Lm3;

        end;

        (J9 . ( 1_ K)) = ( 1_ L) by A2, GROUP_1:def 13

        .= ( 1_ L9);

        then J9 is additive antimultiplicative unity-preserving by Lm12, A3, A2;

        hence J9 is antilinear;

      end;

      now

        assume

         A4: J9 is antilinear;

        

         A5: for x,y be Scalar of K holds (J . (x + y)) = ((J . x) + (J . y))

        proof

          let x,y be Scalar of K;

          

          thus (J . (x + y)) = ((J9 . x) + (J9 . y)) by A4, VECTSP_1:def 20

          .= ((J . x) + (J . y));

        end;

        

         A6: for x,y be Scalar of K holds (J . (x * y)) = ((J . x) * (J . y))

        proof

          let x,y be Scalar of K;

          

          thus (J . (x * y)) = ((J9 . y) * (J9 . x)) by A4, Def6

          .= ((J . x) * (J . y)) by Lm3;

        end;

        (J . ( 1_ K)) = ( 1_ L9) by A4, GROUP_1:def 13

        .= ( 1_ L);

        then J is additive multiplicative unity-preserving by A5, A6;

        hence J is linear;

      end;

      hence thesis by A1;

    end;

    theorem :: MOD_4:29

    

     Th28: J is antilinear iff ( opp J) is linear

    proof

      set J9 = ( opp J), L9 = ( opp L);

      hereby

        assume

         A1: J is antilinear;

        

         A2: J9 is additive

        proof

          let x,y be Scalar of K;

          

          thus (J9 . (x + y)) = ((J . x) + (J . y)) by A1, VECTSP_1:def 20

          .= ((J9 . x) + (J9 . y));

        end;

        

         A3: J9 is multiplicative

        proof

          let x,y be Scalar of K;

          

          thus (J9 . (x * y)) = ((J . y) * (J . x)) by A1, Def6

          .= ((J9 . x) * (J9 . y)) by Lm3;

        end;

        (J9 . ( 1_ K)) = ( 1_ L) by A1, GROUP_1:def 13

        .= ( 1_ L9);

        then J9 is unity-preserving;

        hence J9 is linear by A2, A3;

      end;

      assume

       A4: J9 is additive multiplicative unity-preserving;

      hereby

        let x,y be Scalar of K;

        

        thus (J . (x + y)) = ((J9 . x) + (J9 . y)) by A4

        .= ((J . x) + (J . y));

      end;

      hereby

        let x,y be Scalar of K;

        

        thus (J . (x * y)) = ((J9 . x) * (J9 . y)) by A4

        .= ((J . y) * (J . x)) by Lm3;

      end;

      thus (J . ( 1_ K)) = ( 1_ L) by A4;

    end;

    theorem :: MOD_4:30

    

     Th29: J is monomorphism iff ( opp J) is antimonomorphism by Th27;

    theorem :: MOD_4:31

    

     Th30: J is antimonomorphism iff ( opp J) is monomorphism by Th28;

    theorem :: MOD_4:32

    J is epimorphism iff ( opp J) is antiepimorphism by Th27;

    theorem :: MOD_4:33

    J is antiepimorphism iff ( opp J) is epimorphism by Th28;

    theorem :: MOD_4:34

    J is isomorphism iff ( opp J) is antiisomorphism by Th29;

    theorem :: MOD_4:35

    J is antiisomorphism iff ( opp J) is isomorphism by Th30;

    reserve K for add-associative right_zeroed right_complementable well-unital non empty doubleLoopStr;

    reserve J for Function of K, K;

    theorem :: MOD_4:36

    J is endomorphism iff ( opp J) is antilinear by Th27;

    theorem :: MOD_4:37

    J is antiendomorphism iff ( opp J) is linear by Th28;

    theorem :: MOD_4:38

    J is isomorphism iff ( opp J) is antiisomorphism by Th29;

    theorem :: MOD_4:39

    J is antiisomorphism iff ( opp J) is isomorphism by Th30;

    begin

    definition

      let G,H be AddGroup;

      mode Homomorphism of G,H is additive Function of G, H;

    end

    definition

      let G be AddGroup;

      mode Endomorphism of G is Homomorphism of G, G;

    end

    registration

      let G be AddGroup;

      cluster bijective for Endomorphism of G;

      existence

      proof

        take ( id G);

        thus thesis;

      end;

    end

    definition

      let G be AddGroup;

      mode Automorphism of G is bijective Endomorphism of G;

    end

    reserve G,H for AddGroup;

    reserve f for Homomorphism of G, H;

    reserve x,y for Element of G;

    

     Lm13: (f . ( 0. G)) = ( 0. H)

    proof

      set a = ( 0. G);

      (a + a) = a by RLVECT_1:def 4;

      

      then ((f . a) + (f . a)) = (f . a) by VECTSP_1:def 20

      .= ((f . a) + ( 0. H)) by RLVECT_1:def 4;

      hence thesis by RLVECT_1: 8;

    end;

    

     Lm14: (f . ( - x)) = ( - (f . x))

    proof

      set a = ( 0. G), b = ( 0. H), y = (f . x);

      (x + ( - x)) = a by RLVECT_1:def 10;

      

      then (y + (f . ( - x))) = (f . a) by VECTSP_1:def 20

      .= b by Lm13;

      hence thesis by VECTSP_1: 16;

    end;

    

     Lm15: (f . (x - y)) = ((f . x) - (f . y))

    proof

      

      thus (f . (x - y)) = ((f . x) + (f . ( - y))) by VECTSP_1:def 20

      .= ((f . x) - (f . y)) by Lm14;

    end;

    theorem :: MOD_4:40

    (f . ( 0. G)) = ( 0. H) & (f . ( - x)) = ( - (f . x)) & (f . (x - y)) = ((f . x) - (f . y)) by Lm13, Lm14, Lm15;

    begin

    reserve G,H for AbGroup;

    reserve f for Homomorphism of G, H;

    reserve x,y for Element of G;

    reserve K,L for Ring;

    reserve J for Function of K, L;

    reserve V for LeftMod of K;

    reserve W for LeftMod of L;

    

     Lm16: for x,y be Vector of V holds (( ZeroMap (V,W)) . (x + y)) = ((( ZeroMap (V,W)) . x) + (( ZeroMap (V,W)) . y))

    proof

      set f = ( ZeroMap (V,W));

      thus for x,y be Vector of V holds (f . (x + y)) = ((f . x) + (f . y))

      proof

        let x,y be Vector of V;

        

         A1: (f . y) = ( 0. W) by FUNCOP_1: 7;

        (f . (x + y)) = ( 0. W) & (f . x) = ( 0. W) by FUNCOP_1: 7;

        hence thesis by A1, RLVECT_1:def 4;

      end;

    end;

    

     Lm17: for a be Scalar of K, x be Vector of V holds (( ZeroMap (V,W)) . (a * x)) = ((J . a) * (( ZeroMap (V,W)) . x))

    proof

      let a be Scalar of K, x be Vector of V;

      set z = ( ZeroMap (V,W));

      (z . (a * x)) = ( 0. W) & (z . x) = ( 0. W) by FUNCOP_1: 7;

      hence thesis by VECTSP_1: 14;

    end;

    definition

      let K, L, J, V, W;

      :: MOD_4:def17

      mode Homomorphism of J,V,W -> Function of V, W means

      : Def17: (for x,y be Vector of V holds (it . (x + y)) = ((it . x) + (it . y))) & for a be Scalar of K, x be Vector of V holds (it . (a * x)) = ((J . a) * (it . x));

      existence

      proof

        take ( ZeroMap (V,W));

        thus thesis by Lm16, Lm17;

      end;

    end

    theorem :: MOD_4:41

    ( ZeroMap (V,W)) is Homomorphism of J, V, W

    proof

      set z = ( ZeroMap (V,W));

      (for x,y be Vector of V holds (z . (x + y)) = ((z . x) + (z . y))) & for a be Scalar of K, x be Vector of V holds (z . (a * x)) = ((J . a) * (z . x)) by Lm16, Lm17;

      hence thesis by Def17;

    end;

    reserve J for Function of K, K;

    reserve f for Homomorphism of J, V, V;

    reserve W for LeftMod of K;

    definition

      let K, J, V;

      mode Endomorphism of J,V is Homomorphism of J, V, V;

    end

    definition

      let K, V, W;

      mode Homomorphism of V,W is Homomorphism of ( id K), V, W;

    end

    theorem :: MOD_4:42

    for f be Function of V, W holds f is Homomorphism of V, W iff (for x,y be Vector of V holds (f . (x + y)) = ((f . x) + (f . y))) & for a be Scalar of K, x be Vector of V holds (f . (a * x)) = (a * (f . x))

    proof

      let f be Function of V, W;

      set J = ( id K);

      

       A1: (for a be Scalar of K, x be Vector of V holds (f . (a * x)) = (a * (f . x))) implies for a be Scalar of K, x be Vector of V holds (f . (a * x)) = ((J . a) * (f . x));

      now

        assume

         A2: for a be Scalar of K, x be Vector of V holds (f . (a * x)) = ((J . a) * (f . x));

        let a be Scalar of K, x be Vector of V;

        (J . a) = a;

        hence (f . (a * x)) = (a * (f . x)) by A2;

      end;

      hence thesis by A1, Def17;

    end;

    definition

      let K, V;

      mode Endomorphism of V is Homomorphism of V, V;

    end