:: Opposite Rings, Modules and their Morphisms
:: by Micha{\l} Muzalewski
::
:: Received June 22, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users


registration
let G be non empty addMagma ;
cluster id G -> bijective ;
coherence
id G is bijective
proof end;
end;

theorem :: MOD_4:1
for A, B, C being non empty set
for f being Function of [:A,B:],C
for x being Element of A
for y being Element of B holds f . (x,y) = (~ f) . (y,x) by FUNCT_4:def 8;

definition
let K be non empty doubleLoopStr ;
func opp K -> strict doubleLoopStr equals :: MOD_4:def 1
 doubleLoopStr(# the carrier of K, the addF of K,(~ the multF of K),(1. K),(0. K) #);
correctness
coherence
doubleLoopStr(# the carrier of K, the addF of K,(~ the multF of K),(1. K),(0. K) #) is strict doubleLoopStr ;
;
end;

:: deftheorem defines opp MOD_4:def 1 :
for K being non empty doubleLoopStr holds opp K = doubleLoopStr(# the carrier of K, the addF of K,(~ the multF of K),(1. K),(0. K) #);

registration
let K be non empty doubleLoopStr ;
cluster opp K -> non empty strict ;
coherence
not opp K is empty ;
end;

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

registration
let K be non empty well-unital doubleLoopStr ;
cluster opp K -> strict well-unital ;
coherence
opp K is well-unital by Lm1;
end;

Lm2: now :: thesis: for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for x, y, z being Scalar of (opp K) holds
( (x + y) + z = x + (y + z) & x + (0. (opp K)) = x )
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ; :: thesis: for x, y, z being Scalar of (opp K) holds
( (x + y) + z = x + (y + z) & x + (0. (opp K)) = x )
set L = opp K;
thus for x, y, z being Scalar of (opp K) holds
( (x + y) + z = x + (y + z) & x + (0. (opp K)) = x ) :: thesis: verum
proof
let x, y, z be Scalar of (opp K); :: thesis: ( (x + y) + z = x + (y + z) & x + (0. (opp K)) = x )
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) ; :: thesis: x + (0. (opp K)) = x
thus x + (0. (opp K)) = a + (0. K)
.= x by RLVECT_1:def 4 ; :: thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
cluster opp K -> right_complementable strict add-associative right_zeroed ;
coherence
( opp K is add-associative & opp K is right_zeroed & opp K is right_complementable )
proof end;
end;

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

theorem :: MOD_4:2
for K being non empty doubleLoopStr holds
( addLoopStr(# the carrier of (opp K), the addF of (opp K), the ZeroF of (opp K) #) = addLoopStr(# the carrier of K, the addF of K, the ZeroF of K #) & ( K is add-associative & K is right_zeroed & K is 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 end;

Lm4: for K being non empty doubleLoopStr
for x, y, z, u being Scalar of K
for 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 end;

theorem :: MOD_4:3
( ( for K being non empty unital doubleLoopStr holds 1. K = 1. (opp K) ) & ( for K being non empty right_complementable add-associative right_zeroed doubleLoopStr holds
( 0. K = 0. (opp K) & ( for x, y, z, u being Scalar of K
for 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 non empty Abelian doubleLoopStr ;
cluster opp K -> strict Abelian ;
coherence
opp K is Abelian
proof end;
end;

registration
let K be non empty add-associative doubleLoopStr ;
cluster opp K -> strict add-associative ;
coherence
opp K is add-associative
proof end;
end;

registration
let K be non empty right_zeroed doubleLoopStr ;
cluster opp K -> strict right_zeroed ;
coherence
opp K is right_zeroed
proof end;
end;

registration
let K be non empty right_complementable doubleLoopStr ;
cluster opp K -> right_complementable strict ;
coherence
opp K is right_complementable
proof end;
end;

registration
let K be non empty associative doubleLoopStr ;
cluster opp K -> strict associative ;
coherence
opp K is associative
proof end;
end;

registration
let K be non empty distributive doubleLoopStr ;
cluster opp K -> strict distributive ;
coherence
opp K is distributive
proof end;
end;

theorem :: MOD_4:4
for K being Ring holds opp K is strict Ring ;

theorem Th5: :: MOD_4:5
for K being Skew-Field holds opp K is Skew-Field
proof end;

registration
let K be Skew-Field;
cluster opp K -> non degenerated right_complementable almost_left_invertible strict distributive Abelian add-associative right_zeroed unital associative ;
coherence
( not opp K is degenerated & opp K is almost_left_invertible & opp K is associative & opp K is Abelian & opp K is add-associative & opp K is right_zeroed & opp K is right_complementable & opp K is unital & opp K is distributive ) by Th5;
end;

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

theorem :: MOD_4:6
for K being Field holds opp K is strict Field
proof end;

registration
let K be Field;
cluster opp K -> almost_left_invertible strict ;
coherence
opp K is almost_left_invertible ;
end;

definition
let K be non empty doubleLoopStr ;
let V be non empty ModuleStr over K;
func opp V -> strict RightModStr over opp K means :Def2: :: MOD_4:def 2
 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
ex b1 being strict RightModStr over opp K st
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
b1 = RightModStr(# the carrier of V, the addF of V,(0. V),o #)
proof end;
uniqueness
for b1, b2 being strict RightModStr over opp K st ( 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
b1 = RightModStr(# the carrier of V, the addF of V,(0. V),o #) ) & ( 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
b2 = RightModStr(# the carrier of V, the addF of V,(0. V),o #) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines opp MOD_4:def 2 :
for K being non empty doubleLoopStr
for V being non empty ModuleStr over K
for b3 being strict RightModStr over opp K holds
( b3 = opp V iff 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
b3 = RightModStr(# the carrier of V, the addF of V,(0. V),o #) );

registration
let K be non empty doubleLoopStr ;
let V be non empty ModuleStr over K;
cluster opp V -> non empty strict ;
coherence
not opp V is empty
proof end;
end;

theorem Th7: :: MOD_4:7
for K being non empty doubleLoopStr
for V being non empty ModuleStr over K holds
( addLoopStr(# the carrier of (opp V), the addF of (opp V), the ZeroF of (opp V) #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) & ( for x being set holds
( x is Vector of V iff x is Vector of (opp V) ) ) )
proof end;

definition
let K be non empty doubleLoopStr ;
let V be non empty ModuleStr over K;
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 :: MOD_4:def 3
 ~ o;
coherence
~ o is Function of [: the carrier of (opp V), the carrier of (opp K):], the carrier of (opp V)
proof end;
end;

:: deftheorem defines opp MOD_4:def 3 :
for K being non empty doubleLoopStr
for V being non empty ModuleStr over K
for o being Function of [: the carrier of K, the carrier of V:], the carrier of V holds opp o = ~ o;

theorem Th8: :: MOD_4:8
for K being non empty doubleLoopStr
for V being non empty ModuleStr over K holds the rmult of (opp V) = opp the lmult of V
proof end;

definition
let K be non empty doubleLoopStr ;
let W be non empty RightModStr over K;
func opp W -> strict ModuleStr over opp K means :Def4: :: MOD_4:def 4
 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 = ModuleStr(# the carrier of W, the addF of W,(0. W),o #);
existence
ex b1 being strict ModuleStr over opp K st
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
b1 = ModuleStr(# the carrier of W, the addF of W,(0. W),o #)
proof end;
uniqueness
for b1, b2 being strict ModuleStr over opp K st ( 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
b1 = ModuleStr(# the carrier of W, the addF of W,(0. W),o #) ) & ( 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
b2 = ModuleStr(# the carrier of W, the addF of W,(0. W),o #) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines opp MOD_4:def 4 :
for K being non empty doubleLoopStr
for W being non empty RightModStr over K
for b3 being strict ModuleStr over opp K holds
( b3 = opp W iff 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
b3 = ModuleStr(# the carrier of W, the addF of W,(0. W),o #) );

registration
let K be non empty doubleLoopStr ;
let W be non empty RightModStr over K;
cluster opp W -> non empty strict ;
coherence
not opp W is empty
proof end;
end;

theorem Th9: :: MOD_4:9
for K being non empty doubleLoopStr
for W being non empty RightModStr over K holds
( addLoopStr(# the carrier of (opp W), the addF of (opp W), the ZeroF of (opp W) #) = addLoopStr(# the carrier of W, the addF of W, the ZeroF of W #) & ( for x being set holds
( x is Vector of W iff x is Vector of (opp W) ) ) )
proof end;

definition
let K be non empty doubleLoopStr ;
let W be non empty RightModStr over K;
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 :: MOD_4:def 5
 ~ o;
coherence
~ o is Function of [: the carrier of (opp K), the carrier of (opp W):], the carrier of (opp W)
proof end;
end;

:: deftheorem defines opp MOD_4:def 5 :
for K being non empty doubleLoopStr
for W being non empty RightModStr over K
for o being Function of [: the carrier of W, the carrier of K:], the carrier of W holds opp o = ~ o;

theorem Th10: :: MOD_4:10
for K being non empty doubleLoopStr
for W being non empty RightModStr over K holds the lmult of (opp W) = opp the rmult of W
proof end;

theorem :: MOD_4:11
for K being non empty doubleLoopStr
for V being non empty ModuleStr over K
for o being Function of [: the carrier of K, the carrier of V:], the carrier of V
for x being Scalar of K
for y being Scalar of (opp K)
for v being Vector of V
for w being Vector of (opp V) st x = y & v = w holds
(opp o) . (w,y) = o . (x,v) by FUNCT_4:def 8;

theorem Th12: :: MOD_4:12
for K, L being Ring
for V being non empty ModuleStr over K
for W being non empty RightModStr over L
for x being Scalar of K
for y being Scalar of L
for v being Vector of V
for w being Vector of W st L = opp K & W = opp V & x = y & v = w holds
w * y = x * v
proof end;

theorem Th13: :: MOD_4:13
for K, L being Ring
for V being non empty ModuleStr over K
for W being non empty RightModStr over L
for v1, v2 being Vector of V
for w1, w2 being Vector of W st W = opp V & v1 = w1 & v2 = w2 holds
w1 + w2 = v1 + v2
proof end;

theorem :: MOD_4:14
for K being non empty doubleLoopStr
for W being non empty RightModStr over K
for o being Function of [: the carrier of W, the carrier of K:], the carrier of W
for x being Scalar of K
for y being Scalar of (opp K)
for v being Vector of W
for w being Vector of (opp W) st x = y & v = w holds
(opp o) . (y,w) = o . (v,x) by FUNCT_4:def 8;

theorem Th15: :: MOD_4:15
for K, L being Ring
for V being non empty ModuleStr over K
for W being non empty RightModStr over L
for x being Scalar of K
for y being Scalar of L
for v being Vector of V
for w being Vector of W st V = opp W & x = y & v = w holds
w * y = x * v
proof end;

theorem Th16: :: MOD_4:16
for K, L being Ring
for V being non empty ModuleStr over K
for W being non empty RightModStr over L
for v1, v2 being Vector of V
for w1, w2 being Vector of W st V = opp W & v1 = w1 & v2 = w2 holds
w1 + w2 = v1 + v2
proof end;

theorem :: MOD_4:17
for K being non empty strict doubleLoopStr
for V being non empty ModuleStr over K holds opp (opp V) = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
proof end;

theorem :: MOD_4:18
for K being non empty strict doubleLoopStr
for W being non empty RightModStr over K holds opp (opp W) = RightModStr(# the carrier of W, the addF of W, the ZeroF of W, the rmult of W #)
proof end;

theorem Th19: :: MOD_4:19
for K being Ring
for V being LeftMod of K holds opp V is strict RightMod of opp K
proof end;

registration
let K be Ring;
let V be LeftMod of K;
cluster opp V -> right_complementable Abelian add-associative right_zeroed strict RightMod-like ;
coherence
( opp V is Abelian & opp V is add-associative & opp V is right_zeroed & opp V is right_complementable & opp V is RightMod-like ) by Th19;
end;

theorem Th20: :: MOD_4:20
for K being Ring
for W being RightMod of K holds opp W is strict LeftMod of opp K
proof end;

registration
let K be Ring;
let W be RightMod of K;
cluster opp W -> right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ;
coherence
( opp W is Abelian & opp W is add-associative & opp W is right_zeroed & opp W is right_complementable & opp W is vector-distributive & opp W is scalar-distributive & opp W is scalar-associative & opp W is scalar-unital ) by Th20;
end;

definition
let K, L be non empty multMagma ;
let IT be Function of K,L;
attr IT is antimultiplicative means :Def6: :: MOD_4:def 6
 for x, y being Scalar of K holds IT . (x * y) = (IT . y) * (IT . x);
end;

:: deftheorem Def6 defines antimultiplicative MOD_4:def 6 :
for K, L being non empty multMagma
for IT being Function of K,L holds
( IT is antimultiplicative iff for x, y being Scalar of K holds IT . (x * y) = (IT . y) * (IT . x) );

definition
let K, L be non empty doubleLoopStr ;
let IT be Function of K,L;
attr IT is antilinear means :: MOD_4:def 7
( IT is additive & IT is antimultiplicative & IT is unity-preserving );
end;

:: deftheorem defines antilinear MOD_4:def 7 :
for K, L being non empty doubleLoopStr
for IT being Function of K,L holds
( IT is antilinear iff ( IT is additive & IT is antimultiplicative & IT is unity-preserving ) );

definition
let K, L be non empty doubleLoopStr ;
let IT be Function of K,L;
attr IT is monomorphism means :: MOD_4:def 8
( IT is linear & IT is one-to-one );
attr IT is antimonomorphism means :: MOD_4:def 9
( IT is antilinear & IT is one-to-one );
attr IT is epimorphism means :: MOD_4:def 10
( IT is linear & IT is onto );
attr IT is antiepimorphism means :: MOD_4:def 11
( IT is antilinear & IT is onto );
end;

:: deftheorem defines monomorphism MOD_4:def 8 :
for K, L being non empty doubleLoopStr
for IT being Function of K,L holds
( IT is monomorphism iff ( IT is linear & IT is one-to-one ) );

:: deftheorem defines antimonomorphism MOD_4:def 9 :
for K, L being non empty doubleLoopStr
for IT being Function of K,L holds
( IT is antimonomorphism iff ( IT is antilinear & IT is one-to-one ) );

:: deftheorem defines epimorphism MOD_4:def 10 :
for K, L being non empty doubleLoopStr
for IT being Function of K,L holds
( IT is epimorphism iff ( IT is linear & IT is onto ) );

:: deftheorem defines antiepimorphism MOD_4:def 11 :
for K, L being non empty doubleLoopStr
for IT being Function of K,L holds
( IT is antiepimorphism iff ( IT is antilinear & IT is onto ) );

definition
let K, L be non empty doubleLoopStr ;
let IT be Function of K,L;
attr IT is isomorphism means :: MOD_4:def 12
( IT is monomorphism & IT is onto );
attr IT is antiisomorphism means :: MOD_4:def 13
( IT is antimonomorphism & IT is onto );
end;

:: deftheorem defines isomorphism MOD_4:def 12 :
for K, L being non empty doubleLoopStr
for IT being Function of K,L holds
( IT is isomorphism iff ( IT is monomorphism & IT is onto ) );

:: deftheorem defines antiisomorphism MOD_4:def 13 :
for K, L being non empty doubleLoopStr
for IT being Function of K,L holds
( IT is antiisomorphism iff ( IT is antimonomorphism & IT is onto ) );

registration
let K, L be non empty doubleLoopStr ;
cluster Function-like quasi_total antilinear -> additive unity-preserving antimultiplicative for Element of bool [: the carrier of K, the carrier of L:];
coherence
for b1 being Function of K,L st b1 is antilinear holds
( b1 is additive & b1 is antimultiplicative & b1 is unity-preserving ) ;
cluster Function-like quasi_total additive unity-preserving antimultiplicative -> antilinear for Element of bool [: the carrier of K, the carrier of L:];
coherence
for b1 being Function of K,L st b1 is additive & b1 is antimultiplicative & b1 is unity-preserving holds
b1 is antilinear ;
cluster Function-like quasi_total monomorphism -> one-to-one linear for Element of bool [: the carrier of K, the carrier of L:];
coherence
for b1 being Function of K,L st b1 is monomorphism holds
( b1 is linear & b1 is one-to-one ) ;
cluster Function-like one-to-one quasi_total linear -> monomorphism for Element of bool [: the carrier of K, the carrier of L:];
coherence
for b1 being Function of K,L st b1 is linear & b1 is one-to-one holds
b1 is monomorphism ;
cluster Function-like quasi_total antimonomorphism -> one-to-one antilinear for Element of bool [: the carrier of K, the carrier of L:];
coherence
for b1 being Function of K,L st b1 is antimonomorphism holds
( b1 is antilinear & b1 is one-to-one ) ;
cluster Function-like one-to-one quasi_total antilinear -> antimonomorphism for Element of bool [: the carrier of K, the carrier of L:];
coherence
for b1 being Function of K,L st b1 is antilinear & b1 is one-to-one holds
b1 is antimonomorphism ;
cluster Function-like quasi_total epimorphism -> onto linear for Element of bool [: the carrier of K, the carrier of L:];
coherence
for b1 being Function of K,L st b1 is epimorphism holds
( b1 is linear & b1 is onto ) ;
cluster Function-like quasi_total onto linear -> epimorphism for Element of bool [: the carrier of K, the carrier of L:];
coherence
for b1 being Function of K,L st b1 is linear & b1 is onto holds
b1 is epimorphism ;
cluster Function-like quasi_total antiepimorphism -> onto antilinear for Element of bool [: the carrier of K, the carrier of L:];
coherence
for b1 being Function of K,L st b1 is antiepimorphism holds
( b1 is antilinear & b1 is onto ) ;
cluster Function-like quasi_total onto antilinear -> antiepimorphism for Element of bool [: the carrier of K, the carrier of L:];
coherence
for b1 being Function of K,L st b1 is antilinear & b1 is onto holds
b1 is antiepimorphism ;
cluster Function-like quasi_total isomorphism -> onto monomorphism for Element of bool [: the carrier of K, the carrier of L:];
coherence
for b1 being Function of K,L st b1 is isomorphism holds
( b1 is monomorphism & b1 is onto ) ;
cluster Function-like quasi_total onto monomorphism -> isomorphism for Element of bool [: the carrier of K, the carrier of L:];
coherence
for b1 being Function of K,L st b1 is monomorphism & b1 is onto holds
b1 is isomorphism ;
cluster Function-like quasi_total antiisomorphism -> onto antimonomorphism for Element of bool [: the carrier of K, the carrier of L:];
coherence
for b1 being Function of K,L st b1 is antiisomorphism holds
( b1 is antimonomorphism & b1 is onto ) ;
cluster Function-like quasi_total onto antimonomorphism -> antiisomorphism for Element of bool [: the carrier of K, the carrier of L:];
coherence
for b1 being Function of K,L st b1 is antimonomorphism & b1 is onto holds
b1 is antiisomorphism ;
end;

definition
let K be non empty doubleLoopStr ;
let IT be Function of K,K;
attr IT is endomorphism means :: MOD_4:def 14
IT is linear ;
attr IT is antiendomorphism means :: MOD_4:def 15
IT is antilinear ;
end;

:: deftheorem defines endomorphism MOD_4:def 14 :
for K being non empty doubleLoopStr
for IT being Function of K,K holds
( IT is endomorphism iff IT is linear );

:: deftheorem defines antiendomorphism MOD_4:def 15 :
for K being non empty doubleLoopStr
for IT being Function of K,K holds
( IT is antiendomorphism iff IT is antilinear );

registration
let K be non empty doubleLoopStr ;
cluster Function-like quasi_total endomorphism -> linear for Element of bool [: the carrier of K, the carrier of K:];
coherence
for b1 being Function of K,K st b1 is endomorphism holds
b1 is linear ;
cluster Function-like quasi_total linear -> endomorphism for Element of bool [: the carrier of K, the carrier of K:];
coherence
for b1 being Function of K,K st b1 is linear holds
b1 is endomorphism ;
cluster Function-like quasi_total antiendomorphism -> antilinear for Element of bool [: the carrier of K, the carrier of K:];
coherence
for b1 being Function of K,K st b1 is antiendomorphism holds
b1 is antilinear ;
cluster Function-like quasi_total antilinear -> antiendomorphism for Element of bool [: the carrier of K, the carrier of K:];
coherence
for b1 being Function of K,K st b1 is antilinear holds
b1 is antiendomorphism ;
end;

theorem :: MOD_4:21
for K being non empty doubleLoopStr
for J being Function of K,K holds
( 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 & J is onto ) )
proof end;

theorem Th22: :: MOD_4:22
for K being non empty doubleLoopStr
for J being Function of K,K holds
( 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 end;

registration
let K be non empty doubleLoopStr ;
cluster id K -> isomorphism ;
coherence
id K is isomorphism ;
end;

Lm6: for K, L being Ring
for J being Function of K,L st J is additive holds
J . (0. K) = 0. L
proof end;

Lm7: for K, L being Ring
for J being Function of K,L
for x being Scalar of K st J is linear holds
J . (- x) = - (J . x)
proof end;

Lm8: for K, L being Ring
for J being Function of K,L
for x, y being Scalar of K st J is linear holds
J . (x - y) = (J . x) - (J . y)
proof end;

theorem :: MOD_4:23
for K, L being Ring
for J being Function of K,L
for x, y being Scalar of K st J is linear holds
( J . (0. K) = 0. L & J . (- x) = - (J . x) & J . (x - y) = (J . x) - (J . y) ) by Lm6, Lm7, Lm8;

Lm9: for K, L being Ring
for J being Function of K,L st J is antilinear holds
J . (0. K) = 0. L
proof end;

Lm10: for K, L being Ring
for J being Function of K,L
for x being Scalar of K st J is antilinear holds
J . (- x) = - (J . x)
proof end;

Lm11: for K, L being Ring
for J being Function of K,L
for x, y being Scalar of K st J is antilinear holds
J . (x - y) = (J . x) - (J . y)
proof end;

theorem :: MOD_4:24
for K, L being Ring
for J being Function of K,L
for x, y being Scalar of K st J is antilinear holds
( 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 being Ring holds
( id K is antiisomorphism iff K is comRing )
proof end;

theorem :: MOD_4:26
for K being Skew-Field holds
( id K is antiisomorphism iff K is Field )
proof end;

definition
let K, L be non empty doubleLoopStr ;
let J be Function of K,L;
func opp J -> Function of K,(opp L) equals :: MOD_4:def 16
J;
coherence
J is Function of K,(opp L) ;
end;

:: deftheorem defines opp MOD_4:def 16 :
for K, L being non empty doubleLoopStr
for J being Function of K,L holds opp J = J;

Lm12: for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for L being non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr
for J being Function of K,L st J is linear holds
opp J is additive
proof end;

theorem :: MOD_4:27
canceled;

::$CT
theorem Th27: :: MOD_4:28
for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for L being non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr
for J being Function of K,L holds
( J is linear iff opp J is antilinear )
proof end;

theorem Th28: :: MOD_4:29
for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for L being non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr
for J being Function of K,L holds
( J is antilinear iff opp J is linear )
proof end;

theorem Th29: :: MOD_4:30
for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for L being non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr
for J being Function of K,L holds
( J is monomorphism iff opp J is antimonomorphism ) by Th27;

theorem Th30: :: MOD_4:31
for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for L being non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr
for J being Function of K,L holds
( J is antimonomorphism iff opp J is monomorphism ) by Th28;

theorem :: MOD_4:32
for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for L being non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr
for J being Function of K,L holds
( J is epimorphism iff opp J is antiepimorphism ) by Th27;

theorem :: MOD_4:33
for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for L being non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr
for J being Function of K,L holds
( J is antiepimorphism iff opp J is epimorphism ) by Th28;

theorem :: MOD_4:34
for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for L being non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr
for J being Function of K,L holds
( J is isomorphism iff opp J is antiisomorphism ) by Th29;

theorem :: MOD_4:35
for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for L being non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr
for J being Function of K,L holds
( J is antiisomorphism iff opp J is isomorphism ) by Th30;

theorem :: MOD_4:36
for K being non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr
for J being Function of K,K holds
( J is endomorphism iff opp J is antilinear ) by Th27;

theorem :: MOD_4:37
for K being non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr
for J being Function of K,K holds
( J is antiendomorphism iff opp J is linear ) by Th28;

theorem :: MOD_4:38
for K being non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr
for J being Function of K,K holds
( J is isomorphism iff opp J is antiisomorphism ) by Th29;

theorem :: MOD_4:39
for K being non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr
for J being Function of K,K holds
( J is antiisomorphism iff opp J is isomorphism ) by Th30;

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 non empty Relation-like the carrier of G -defined the carrier of G -valued Function-like V17( the carrier of G) quasi_total bijective additive for Element of bool [: the carrier of G, the carrier of G:];
existence
ex b1 being Endomorphism of G st b1 is bijective
proof end;
end;

definition
let G be AddGroup;
mode Automorphism of G is bijective Endomorphism of G;
end;

Lm13: for G, H being AddGroup
for f being Homomorphism of G,H holds f . (0. G) = 0. H
proof end;

Lm14: for G, H being AddGroup
for f being Homomorphism of G,H
for x being Element of G holds f . (- x) = - (f . x)
proof end;

Lm15: for G, H being AddGroup
for f being Homomorphism of G,H
for x, y being Element of G holds f . (x - y) = (f . x) - (f . y)
proof end;

theorem :: MOD_4:40
for G, H being AddGroup
for f being Homomorphism of G,H
for x, y being Element of G holds
( f . (0. G) = 0. H & f . (- x) = - (f . x) & f . (x - y) = (f . x) - (f . y) ) by Lm13, Lm14, Lm15;

Lm16: for K, L being Ring
for V being LeftMod of K
for W being LeftMod of L
for x, y being Vector of V holds (ZeroMap (V,W)) . (x + y) = ((ZeroMap (V,W)) . x) + ((ZeroMap (V,W)) . y)
proof end;

Lm17: for K, L being Ring
for J being Function of K,L
for V being LeftMod of K
for W being LeftMod of L
for a being Scalar of K
for x being Vector of V holds (ZeroMap (V,W)) . (a * x) = (J . a) * ((ZeroMap (V,W)) . x)
proof end;

definition
let K, L be Ring;
let J be Function of K,L;
let V be LeftMod of K;
let W be LeftMod of L;
mode Homomorphism of J,V,W -> Function of V,W means :Def17: :: MOD_4:def 17
( ( for x, y being Vector of V holds it . (x + y) = (it . x) + (it . y) ) & ( for a being Scalar of K
for x being Vector of V holds it . (a * x) = (J . a) * (it . x) ) );
existence
ex b1 being Function of V,W st
( ( for x, y being Vector of V holds b1 . (x + y) = (b1 . x) + (b1 . y) ) & ( for a being Scalar of K
for x being Vector of V holds b1 . (a * x) = (J . a) * (b1 . x) ) )
proof end;
end;

:: deftheorem Def17 defines Homomorphism MOD_4:def 17 :
for K, L being Ring
for J being Function of K,L
for V being LeftMod of K
for W being LeftMod of L
for b6 being Function of V,W holds
( b6 is Homomorphism of J,V,W iff ( ( for x, y being Vector of V holds b6 . (x + y) = (b6 . x) + (b6 . y) ) & ( for a being Scalar of K
for x being Vector of V holds b6 . (a * x) = (J . a) * (b6 . x) ) ) );

theorem :: MOD_4:41
for K, L being Ring
for J being Function of K,L
for V being LeftMod of K
for W being LeftMod of L holds ZeroMap (V,W) is Homomorphism of J,V,W
proof end;

definition
let K be Ring;
let J be Function of K,K;
let V be LeftMod of K;
mode Endomorphism of J,V is Homomorphism of J,V,V;
end;

definition
let K be Ring;
let V, W be LeftMod of K;
mode Homomorphism of V,W is Homomorphism of id K,V,W;
end;

theorem :: MOD_4:42
for K being Ring
for V, W being LeftMod of K
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
for x being Vector of V holds f . (a * x) = a * (f . x) ) ) )
proof end;

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