:: Opposite Rings, Modules and their Morphisms
::  by Micha{\l} Muzalewski
::
:: Received June 22, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, FUNCT_1, ZFMISC_1, RELAT_1, SUBSET_1, ALGSTR_0,
      ARYTM_0, STRUCT_0, MESFUNC1, SUPINF_2, VECTSP_1, RLVECT_1, ARYTM_3,
      ARYTM_1, GROUP_1, BINOP_1, LATTICES, FUNCSDOM, VECTSP_2, MSSUBFAM,
      FDIFF_1, GRCAT_1, GROUP_6, FUNCT_2, MOD_4;
 notations XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, DOMAIN_1,
      STRUCT_0, ALGSTR_0, BINOP_1, RLVECT_1, GROUP_1, VECTSP_1, FUNCSDOM,
      VECTSP_2, GRCAT_1, FUNCT_4, GROUP_6, RINGCAT1;
 constructors DOMAIN_1, VECTSP_2, GRCAT_1, GROUP_6, RINGCAT1, FUNCOP_1,
      RELSET_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, VECTSP_1, VECTSP_2,
      ALGSTR_0, GRCAT_1, FUNCT_2, RINGCAT1, FUNCT_1;
 requirements SUBSET, BOOLE;
 definitions RLVECT_1, STRUCT_0, GROUP_1, GROUP_6, GRCAT_1, RINGCAT1, VECTSP_1,
      ALGSTR_0;
 theorems FUNCT_1, FUNCT_2, VECTSP_1, VECTSP_2, FUNCT_4, RLVECT_1, RELAT_1,
      GROUP_1, FUNCOP_1, GROUP_6, ALGSTR_0, STRUCT_0;

begin :: Opposite Functions

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;

definition
  let A,B,C,f;
  redefine func ~f -> Function of [:B,A:],C;
  coherence by FUNCT_4:50;
end;

theorem Th1:
  for x being Element of A, y being Element of B holds f.(x,y) = ~f .(y,x)
proof
  let x be Element of A, y be Element of B;
  dom f = [:A,B:] by FUNCT_2:def 1;
  then [x,y] in dom f;
  then [y,x] in dom ~f by FUNCT_4:42;
  hence thesis by FUNCT_4:43;
end;

begin :: Opposite Rings

reserve K for non empty doubleLoopStr;

definition let K;
  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 being well-unital non empty doubleLoopStr for h, e being 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 Th1
    .= h by A1,VECTSP_1:def 6;
  thus e * h = a * b by Th1
    .= h by A1,VECTSP_1:def 6;
end;

registration
  let K be well-unital non empty doubleLoopStr;
  cluster opp(K) -> well-unital;
  coherence
  proof
    let x be Element of opp K;
    thus thesis by Lm1;
  end;
end;

Lm2: now
  let K be add-associative right_zeroed right_complementable non empty
  doubleLoopStr;
  set L = opp(K);
  thus for x,y,z being 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 being add-associative right_zeroed right_complementable non empty
doubleLoopStr for x,y being Scalar of K, a,b being 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,Th1;
  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
  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 being
  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 set st x in the carrier of K holds (comp opp K).x = (comp K). x
    proof
      let x be set;
      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 being non empty doubleLoopStr for x,y,z,u being Scalar of K, a,b,c,
d being 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,Th1;
  hence thesis by A1,A2,Th1;
end;

theorem
  (for K being unital non empty doubleLoopStr holds 1.K = 1.opp(K)) &
  for K being add-associative right_zeroed right_complementable non empty
doubleLoopStr holds 0.K = 0.opp(K) & for x,y,z,u being (Scalar of K), a,b,c,d
being 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 being 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
  for K being Ring holds opp(K) is strict Ring;

theorem Th5:
  for K being Skew-Field holds opp(K) is Skew-Field
proof
  let K be Skew-Field;
  set L = opp(K);
  for x being 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 being 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 being commutative non empty doubleLoopStr, x,y being Element of F
holds x*y = y*x;

theorem
  for K being Field holds opp(K) is strict Field
proof
  let K be Field;
  set L = opp(K);
  for x,y being 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 :: Opposite Modules

reserve V for non empty VectSpStr over K;

definition let K,V;
  func opp(V) -> strict RightModStr over opp(K) means
  :Def2:
  for o being
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 being 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 being 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 Th7:
  the addLoopStr of opp(V) = the addLoopStr of V & for x being 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;
  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 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;
  func opp(W) -> strict VectSpStr over opp(K) means :Def4:
  for o being
Function of [:the carrier of opp(K), the carrier of W:], the carrier of W st o
= ~(the rmult of W) holds it = VectSpStr (# 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 VectSpStr (#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 VectSpStr over opp(K) such that
A1: for o being Function of [:the carrier of opp(K), the carrier of W
    :], the carrier of W st o = ~(the rmult of W) holds M1 = VectSpStr (# the
      carrier of W, the addF of W, 0.W, o #) and
A2: for o being Function of [:the carrier of opp(K), the carrier of W
    :], the carrier of W st o = ~(the rmult of W) holds M2 = VectSpStr (# the
      carrier of W, the addF of W, 0.W, o #);
    thus M1 = VectSpStr (# 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 = VectSpStr (#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 Th9:
  the addLoopStr of opp(W) = the addLoopStr of W & for x being 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) = VectSpStr (# 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;
  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 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) = VectSpStr (# the carrier of W, the addF of W, 0.W, p #) by Def4;
  hence thesis;
end;

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

theorem Th12:
  for K,L being Ring, V being non empty VectSpStr over K for W
being non empty RightModStr over L for x being Scalar of K, y being Scalar of L
  , v being Vector of V, w being 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 VectSpStr 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,Th1;
end;

theorem Th13:
  for K,L being Ring, V being non empty VectSpStr over K for W
  being non empty RightModStr over L for v1,v2 being Vector of V, w1,w2 being
  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 VectSpStr 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
  for o being Function of [:the carrier of W, the carrier of K:], the
carrier of W, x being Scalar of K, y being Scalar of opp(K), v being Vector of
W, w being Vector of opp(W) st x=y & v=w holds (opp(o)).(y,w) = o.(v,x) by Th1;

theorem Th15:
  for K,L being Ring, V being non empty VectSpStr over K for W
being non empty RightModStr over L for x being Scalar of K, y being Scalar of L
, v being Vector of V, w being 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 VectSpStr 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,Th1;
end;

theorem Th16:
  for K,L being Ring, V being non empty VectSpStr over K for W
  being non empty RightModStr over L for v1,v2 being Vector of V, w1,w2 being
  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 VectSpStr 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
  for K being strict non empty doubleLoopStr, V being non empty
  VectSpStr over K holds opp(opp(V)) = the VectSpStr of V
proof
  let K be strict non empty doubleLoopStr, V be non empty VectSpStr 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
  for K being strict non empty doubleLoopStr, W being 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 Th19:
  for K being Ring, V being 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 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 being 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 Th20:
  for K being Ring, W being 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 VectSpStr over R;
A1: the addLoopStr of opp W = the addLoopStr of W by Th9;
  then
A2: for a,b be Element of opp W 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 being 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,def 15,def 16,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 :: Ring Morphisms

definition
  let K,L be non empty multMagma;
  let IT be Function of K,L;
  attr IT is antimultiplicative means  :Def6:
  for x,y being 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;
  attr IT is antilinear means  :Def7:
  IT is additive antimultiplicative unity-preserving;
end;

registration
  let K,L be non empty doubleLoopStr;
  cluster antilinear -> additive antimultiplicative unity-preserving for
Function
    of K,L;
  coherence by Def7;
  cluster additive antimultiplicative unity-preserving -> antilinear for
Function
    of K,L;
  coherence by Def7;
end;

definition
  let K,L be non empty doubleLoopStr;
  let IT be Function of K,L;
  attr IT is monomorphism means  :Def8:
  IT is linear one-to-one;
  attr IT is antimonomorphism means  :Def9:
  IT is antilinear one-to-one;
end;

definition
  let K,L be non empty doubleLoopStr;
  let IT be Function of K,L;
  attr IT is epimorphism means  :Def10:
  IT is linear onto;
  attr IT is antiepimorphism means  :Def11:
  IT is antilinear onto;
end;

definition
  let K,L be non empty doubleLoopStr;
  let IT be Function of K,L;
  attr IT is isomorphism means  :Def12:
  IT is monomorphism onto;
  attr IT is antiisomorphism means  :Def13:
  IT is antimonomorphism onto;
end;

reserve J for Function of K,K;

definition
  let K be non empty doubleLoopStr;
  let IT be Function of K,K;
  attr IT is endomorphism means  :Def14:
  IT is linear;
  attr IT is antiendomorphism means  :Def15:
  IT is antilinear;

end;

theorem
  J is isomorphism iff J is additive &
  (for x,y being Scalar of K holds J.(x*y) = J.x*J.y) & J.(1_K) = 1_K & J
  is one-to-one onto
proof
A1: now
    assume A2: J is isomorphism; then
A3: J is monomorphism by Def12;
    then J is linear by Def8;
    hence J is additive & for x,y being
    Scalar of K holds J.(x*y) = J.x*J.y & J.(1_K) = 1_K by GROUP_1:def 13
,GROUP_6:def 6;
    thus J is one-to-one by A3,Def8;
    thus J is onto by A2,Def12;
  end;
  now
    assume that
A4: ( J is additive & for x,y
    being Scalar of K holds J.(x*y) = J.x*J.y )& J.(1_K) = 1_K and
A5: J is one-to-one and
A6: J is onto;
    J is multiplicative unity-preserving by A4,GROUP_1:def 13,GROUP_6:def 6;
    then J is monomorphism by A5,Def8,A4;
    hence J is isomorphism by A6,Def12;
  end;
  hence thesis by A1;
end;

theorem Th22:
  J is antiisomorphism iff J is additive
  & (for x,y being 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
A1: now
    assume A2: J is antiisomorphism; then
A3: J is antimonomorphism by Def13;
    then J is antilinear by Def9;
    hence J is additive &
     for x,y being
    Scalar of K holds J.(x*y) = J.y*J.x & J.(1_K) = 1_K by Def6,GROUP_1:def 13;
    thus J is one-to-one by A3,Def9;
    thus J is onto by A2,Def13;
  end;
  now
    assume that
A4: ( J is additive & for x,y
    being Scalar of K holds J.(x*y) = J.y*J.x )& J.(1_K) = 1_K and
A5: J is one-to-one and
A6: J is onto;
    J is additive antimultiplicative unity-preserving
      by A4,Def6,GROUP_1:def 13;
    then J is antimonomorphism by A5,Def9;
    hence J is antiisomorphism by A6,Def13;
  end;
  hence thesis by A1;
end;

Lm6: (for x,y being Scalar of K holds (id K).(x*y) = (id K).x*(id K).y) &
(id K).(1_K) = 1_K
proof
  set J = id K;
  thus for x,y being Scalar of K holds J.(x*y) = J.x*J.y
  proof
    let x,y be Scalar of K;
    J.(x*y) = x*y & J.x = x by FUNCT_1:18;
    hence thesis by FUNCT_1:18;
  end;
  thus (id K).(1_K) = 1_K by FUNCT_1:18;
end;

registration let K;
  cluster id K -> isomorphism;
  coherence
proof
  set J = id K;
  J is monomorphism by Def8;
  hence thesis by Def12;
end;
end;

reserve K,L for Ring;
reserve J for Function of K,L;
reserve x,y for Scalar of K;

Lm7: 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,VECTSP_1:def 20
    .= J.a+(0.L) by RLVECT_1:4;
  hence thesis by RLVECT_1:8;
end;

Lm8: 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,Lm7;
  hence thesis by A2,RLVECT_1:8;
end;

Lm9: 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,Lm8;
end;

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

Lm10: 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;

Lm11: 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,Lm10;
  hence thesis by A2,RLVECT_1:8;
end;

Lm12: 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,Lm11;
end;

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

theorem
  for K being 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 being Scalar of K holds J.(x*y) = J.y*J.x
    proof
      let x,y be Scalar of K;
A4:   J.y = y by FUNCT_1:18;
      J.(x*y) = x*y & J.x = x by FUNCT_1:18;
      hence thesis by A2,A4,Lm5;
    end;
    J.(1_K) = 1_K by Lm6;
    hence J is antiisomorphism by A3,Th22;
  end;
  now
    assume
A5: J is antiisomorphism;
    for x,y being Element of K holds x*y = y*x
    proof
      let x,y be Element of K;
A6:   J.y = y by FUNCT_1:18;
      J.(x*y) = x*y & J.x = x by FUNCT_1:18;
      hence thesis by A5,A6,Th22;
    end;
    hence K is comRing by GROUP_1:def 12;
  end;
  hence thesis by A1;
end;

theorem
  for K being 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 being Scalar of K holds J.(x*y) = J.y*J.x
    proof
      let x,y be Scalar of K;
A4:   J.y = y by FUNCT_1:18;
      J.(x*y) = x*y & J.x = x by FUNCT_1:18;
      hence thesis by A2,A4,GROUP_1:def 12;
    end;
    J.(1_K) = 1_K by Lm6;
    hence J is antiisomorphism by A3,Th22;
  end;
  now
    assume
A5: J is antiisomorphism;
    for x,y being Scalar of K holds x*y = y*x
    proof
      let x,y be Scalar of K;
A6:   J.y = y by FUNCT_1:18;
      J.(x*y) = x*y & J.x = x by FUNCT_1:18;
      hence thesis by A5,A6,Th22;
    end;
    hence K is Field by GROUP_1:def 12;
  end;
  hence thesis by A1;
end;

begin :: Opposite Morphisms

definition
  let K,L be non empty doubleLoopStr, J be Function of K,L;
  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;

Lm13:
  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 Th28:
  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 being 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 Lm13,A3,Def6,A2,
GROUP_1:def 13;
    hence J9 is antilinear;
  end;
  now
    assume
A4: J9 is antilinear;
A5: for x,y being 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 being 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,VECTSP_1:def 20
,GROUP_1:def 13,GROUP_6:def 6;
    hence J is linear;
  end;
  hence thesis by A1;
end;

theorem Th29:
  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 by GROUP_1:def 13;
    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,VECTSP_1:def 20
      .= J.x+J.y;
  end;
  hereby
    let x,y be Scalar of K;
    thus J.(x*y) = J9.x*J9.y by A4,GROUP_6:def 6
      .= J.y*J.x by Lm3;
  end;
  thus J.(1_K) = 1_L9 by A4,GROUP_1:def 13
    .= 1_L;
end;

theorem Th30:
  J is monomorphism iff opp(J) is antimonomorphism
proof
  set J9 = opp(J);
A1: J is linear iff J9 is antilinear by Th28;
  J9 is antimonomorphism iff J9 is antilinear & J9 is one-to-one by Def9;
  hence thesis by A1,Def8;
end;

theorem Th31:
  J is antimonomorphism iff opp(J) is monomorphism
proof
  set J9 = opp(J);
A1: J is antilinear iff J9 is linear by Th29;
  J9 is monomorphism iff J9 is linear & J9 is one-to-one by Def8;
  hence thesis by A1,Def9;
end;

theorem
  J is epimorphism iff opp(J) is antiepimorphism
proof
  set J9 = opp(J), L9 = opp(L);
  J is linear iff J9 is antilinear by Th28;
  hence thesis by Def10,Def11;
end;

theorem
  J is antiepimorphism iff opp(J) is epimorphism
proof
  set J9 = opp(J), L9 = opp(L);
  J is antilinear iff J9 is linear by Th29;
  hence thesis by Def10,Def11;
end;

theorem Th34:
  J is isomorphism iff opp(J) is antiisomorphism
proof
  set J9 = opp(J), L9 = opp(L);
  J is monomorphism iff J9 is antimonomorphism by Th30;
  hence thesis by Def12,Def13;
end;

theorem Th35:
  J is antiisomorphism iff opp(J) is isomorphism
proof
  set J9 = opp(J), L9 = opp(L);
  J is antimonomorphism iff J9 is monomorphism by Th31;
  hence thesis by Def12,Def13;
end;

reserve K for add-associative right_zeroed right_complementable well-unital
  non empty doubleLoopStr;
reserve J for Function of K,K;

theorem
  J is endomorphism iff opp(J) is antilinear
proof
  J is linear iff opp(J) is antilinear by Th28;
  hence thesis by Def14;
end;

theorem
  J is antiendomorphism iff opp(J) is linear
proof
  J is antilinear iff opp(J) is linear by Th29;
  hence thesis by Def15;
end;

theorem
  J is isomorphism iff opp(J) is antiisomorphism by Th34;

theorem
  J is antiisomorphism iff opp(J) is isomorphism by Th35;

begin :: Morphisms of Groups

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;

Lm14: 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;

Lm15: 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 Lm14;
  hence thesis by VECTSP_1:16;
end;

Lm16: 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 Lm15;
end;

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

begin :: Semilinear Maps

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;

Lm17: for x,y being 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 being 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;

Lm18: for a being Scalar of K, x being 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;

  mode Homomorphism of J,V,W -> Function of V,W means  :Def17:
    (for x,y being Vector of V holds it.(x+y) = it.x+it.y) &
    for a being Scalar of K, x being Vector of V holds it.(a*x) = J.a*it.x;
  existence
  proof
    take ZeroMap(V,W);
    thus thesis by Lm17,Lm18;
  end;
end;

theorem
  ZeroMap(V,W) is Homomorphism of J,V,W
proof
  set z = ZeroMap(V,W);
  ( for x,y being Vector of V holds z.(x+y) = z.x+z.y)& for a being Scalar
  of K, x being Vector of V holds z.(a*x) = J.a*z.x by Lm17,Lm18;
  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
  for f being Function of V,W holds f is Homomorphism of V,W iff
  (for x, y being Vector of V holds f.(x+y) = f.x+f.y) &
  for a being Scalar of K, x being Vector of V holds f.(a*x) = a*f.x
proof
  let f be Function of V,W;
  set J = id K;
A1: now
    assume
A2: for a being Scalar of K, x being Vector of V holds f.(a*x) = a*f.x;
    let a be Scalar of K, x be Vector of V;
    J.a = a by FUNCT_1:18;
    hence f.(a*x) = J.a*f.x by A2;
  end;
  now
    assume
A3: for a being Scalar of K, x being 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 by FUNCT_1:18;
    hence f.(a*x) = a*f.x by A3;
  end;
  hence thesis by A1,Def17;
end;

definition let K,V;
  mode Endomorphism of V is Homomorphism of V,V;
end;