:: MOD_4 semantic presentation

begin

registration
let G be non empty addMagma ;
cluster id G ->  bijective ;
coherence
 id G is bijective
proof
set f = id G;
 rng (id G) = the carrier of G by RELAT_1:45;
then  ( id G is one-to-one & id G is onto ) by FUNCT_2:def_3;
hence  id G is bijective ; ::_thesis: verum
end;
end;


definition
let A, B, C be non empty set ;
let f be Function of [:A,B:],C;
:: original: ~
redefine func ~ f ->  Function of [:B,A:],C;
coherence
 ~ f is Function of [:B,A:],C by FUNCT_4:50;
end;

theorem Th1: :: MOD_4:1
for C, A, B 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)
proof
let C, A, B be non empty set ; ::_thesis: 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)
let f be Function of [:A,B:],C; ::_thesis: for x being Element of A
for y being Element of B holds f . (x,y) = (~ f) . (y,x)
let x be Element of A; ::_thesis: for y being Element of B holds f . (x,y) = (~ f) . (y,x)
let y be Element of B; ::_thesis: f . (x,y) = (~ f) . (y,x)
 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  f . (x,y) = (~ f) . (y,x) by FUNCT_4:43; ::_thesis: verum
end;

begin

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
let K be non empty well-unital doubleLoopStr ; ::_thesis: for h, e being Element of (opp K) st e = 1. K holds
( h * e = h & e * h = h )
let h, e be Element of (opp K); ::_thesis: ( e = 1. K implies ( h * e = h & e * h = h ) )
assume A1: e = 1. K ; ::_thesis: ( h * e = h & e * h = h )
reconsider a = h, b = e as Element of K ;
thus h * e = b * a by Th1
.= h by A1, VECTSP_1:def_6 ; ::_thesis: e * h = h
thus e * h = a * b by Th1
.= h by A1, VECTSP_1:def_6 ; ::_thesis: verum
end;

registration
let K be non empty well-unital doubleLoopStr ;
cluster opp K ->  strict well-unital ;
coherence
 opp K is well-unital
proof
let x be Element of (opp K); :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. (opp K)) = x & (1. (opp K)) * x = x )
thus  ( x * (1. (opp K)) = x & (1. (opp K)) * x = x ) by Lm1; ::_thesis: verum
end;
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
thus  for x, y, z being Element of (opp K) holds x + (y + z) = (x + y) + z by Lm2; :: according to RLVECT_1:def_3 ::_thesis: ( opp K is right_zeroed & opp K is right_complementable )
thus  for x being Element of (opp K) holds x + (0. (opp K)) = x by Lm2; :: according to RLVECT_1:def_4 ::_thesis: opp K is right_complementable
let a be Element of (opp K); :: according to ALGSTR_0:def_16 ::_thesis: a is right_complementable
reconsider x = a as Element of K ;
reconsider y = - x as Element of (opp K) ;
take  y ; :: according to ALGSTR_0:def_11 ::_thesis: a + y = 0. (opp K)
thus a + y = x + (- x)
.= 0. (opp K) by RLVECT_1:5 ; ::_thesis: verum
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
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 )
let x, y be Scalar of K; ::_thesis: for a, b being Scalar of (opp K) st x = a & y = b holds
( x + y = a + b & x * y = b * a & - x = - a )
let a, b be Scalar of (opp K); ::_thesis: ( x = a & y = b implies ( x + y = a + b & x * y = b * a & - x = - a ) )
assume that
A1: x = a and
A2: y = b ; ::_thesis: ( x + y = a + b & x * y = b * a & - x = - a )
thus  x + y = a + b by A1, A2; ::_thesis: ( x * y = b * a & - x = - a )
thus  x * y = b * a by A1, A2, Th1; ::_thesis: - x = - a
reconsider c = - a as Element of K ;
c + x = (- a) + a by A1
.= 0. (opp K) by RLVECT_1:5
.= 0. K ;
hence  - x = - a by RLVECT_1:6; ::_thesis: verum
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
let K be non empty doubleLoopStr ; ::_thesis: ( 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 ) ) )
thus  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 #) ; ::_thesis: ( ( 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 ) ) )
hereby  ::_thesis: for x being set holds
( x is Scalar of (opp K) iff x is Scalar of K )
assume A1: ( K is add-associative & K is right_zeroed & K is right_complementable ) ; ::_thesis: comp (opp K) = comp K
A2: for x being set st x in the carrier of K holds
(comp (opp K)) . x = (comp K) . x
proof
let x be set ; ::_thesis: ( x in the carrier of K implies (comp (opp K)) . x = (comp K) . x )
assume  x in the carrier of K ; ::_thesis: (comp (opp K)) . x = (comp K) . x
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 ; ::_thesis: verum
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; ::_thesis: verum
end;
let x be set ; ::_thesis: ( x is Scalar of (opp K) iff x is Scalar of K )
thus  ( x is Scalar of (opp K) iff x is Scalar of K ) ; ::_thesis: verum
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
let K be non empty doubleLoopStr ; ::_thesis: 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) )
let x, y, z, u be Scalar of K; ::_thesis: 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) )
let a, b, c, d be Scalar of (opp K); ::_thesis: ( x = a & y = b & z = c & u = d implies ( (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) ) )
assume that
A1: ( x = a & y = b & z = c ) and
A2: u = d ; ::_thesis: ( (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) )
 ( x * y = b * a & y * z = c * b ) by A1, Th1;
hence  ( (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 A1, A2, Th1; ::_thesis: verum
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
let x, y be Element of (opp K); :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
reconsider a = x, b = y as Element of K ;
thus x + y = a + b
.= b + a
.= y + x ; ::_thesis: verum
end;
end;

registration
let K be non empty add-associative doubleLoopStr ;
cluster opp K ->  strict add-associative ;
coherence
 opp K is add-associative
proof
let x, y, z be Element of (opp K); :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
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) ; ::_thesis: verum
end;
end;

registration
let K be non empty right_zeroed doubleLoopStr ;
cluster opp K ->  strict right_zeroed ;
coherence
 opp K is right_zeroed
proof
let x be Element of (opp K); :: according to RLVECT_1:def_4 ::_thesis: x + (0. (opp K)) = x
reconsider a = x as Element of K ;
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 doubleLoopStr ;
cluster opp K ->  right_complementable strict ;
coherence
 opp K is right_complementable
proof
let x be Element of (opp K); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
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 ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. (opp K)
thus  x + y = 0. (opp K) by A1; ::_thesis: verum
end;
end;

registration
let K be non empty associative doubleLoopStr ;
cluster opp K ->  strict associative ;
coherence
 opp K is associative
proof
let x, y, z be Element of (opp K); :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z)
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 ; ::_thesis: verum
end;
end;

registration
let K be non empty distributive doubleLoopStr ;
cluster opp K ->  strict distributive ;
coherence
 opp K is distributive
proof
let x, y, z be Element of (opp K); :: according to VECTSP_1:def_7 ::_thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
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 ; ::_thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = a * (b + c) by Lm4
.= (a * b) + (a * c) by VECTSP_1:def_7
.= (y * x) + (z * x) by Lm4 ; ::_thesis: verum
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
let K be Skew-Field; ::_thesis: opp K is Skew-Field
set L = opp K;
 for x being Scalar of (opp K) holds
( ( x <> 0. (opp K) implies ex y being Scalar of (opp K) st y * x = 1_ (opp K) ) & 0. (opp K) <> 1_ (opp K) )
proof
let x be Scalar of (opp K); ::_thesis: ( ( x <> 0. (opp K) implies ex y being Scalar of (opp K) st y * x = 1_ (opp K) ) & 0. (opp K) <> 1_ (opp K) )
 ( x <> 0. (opp K) implies ex y being Scalar of (opp K) st y * x = 1_ (opp K) )
proof
reconsider a = x as Scalar of K ;
assume  x <> 0. (opp K) ; ::_thesis: ex y being Scalar of (opp K) st y * x = 1_ (opp K)
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 ; ::_thesis: y * x = 1_ (opp K)
thus  y * x = 1_ (opp K) by A1, Lm3; ::_thesis: verum
end;
hence  ( ( x <> 0. (opp K) implies ex y being Scalar of (opp K) st y * x = 1_ (opp K) ) & 0. (opp K) <> 1_ (opp K) ) ; ::_thesis: verum
end;
hence  opp K is Skew-Field by STRUCT_0:def_8, VECTSP_1:def_9; ::_thesis: verum
end;

registration
let K be Skew-Field;
cluster opp K ->  non degenerated right_complementable almost_left_invertible strict unital associative distributive Abelian add-associative right_zeroed ;
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
let K be Field; ::_thesis: opp K is strict Field
set L = opp K;
 for x, y being Scalar of (opp K) holds x * y = y * x
proof
let x, y be Scalar of (opp K); ::_thesis: x * y = y * x
reconsider a = x, b = y as Scalar of K ;
 b * a = x * y by Lm3;
hence  x * y = y * x by Lm3; ::_thesis: verum
end;
hence  opp K is strict Field by GROUP_1:def_12; ::_thesis: verum
end;

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

begin

definition
let K be non empty doubleLoopStr ;
let V be non empty VectSpStr 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
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 #) ; ::_thesis: 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
RightModStr(# the carrier of V, the addF of V,(0. V),o #) = RightModStr(# the carrier of V, the addF of V,(0. V),o #)
thus  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
RightModStr(# the carrier of V, the addF of V,(0. V),o #) = RightModStr(# the carrier of V, the addF of V,(0. V),o #) ; ::_thesis: verum
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
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; ::_thesis: ( ( 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 #) ) & ( 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 #) ) implies M1 = M2 )
assume 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 #) ; ::_thesis: M1 = M2
thus M1 = RightModStr(# the carrier of V, the addF of V,(0. V),o #) by A1
.= M2 by A2 ; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines opp MOD_4:def_2_:_
 for K being non empty doubleLoopStr
for V being non empty VectSpStr 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 VectSpStr over K;
cluster opp V ->  non empty strict ;
coherence
 not opp V is empty
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  not the carrier of (opp V) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

theorem Th7: :: MOD_4:7
for K being non empty doubleLoopStr
for V being non empty VectSpStr 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
let K be non empty doubleLoopStr ; ::_thesis: for V being non empty VectSpStr 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) ) ) )
let V be non empty VectSpStr over K; ::_thesis: ( 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) ) ) )
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  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 #) ; ::_thesis: for x being set holds
( x is Vector of V iff x is Vector of (opp V) )
let x be set ; ::_thesis: ( x is Vector of V iff x is Vector of (opp V) )
thus  ( x is Vector of V iff x is Vector of (opp V) ) by A1; ::_thesis: verum
end;

definition
let K be non empty doubleLoopStr ;
let V be non empty VectSpStr 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
 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 #) by Th7;
hence  ~ o is Function of [: the carrier of (opp V), the carrier of (opp K):], the carrier of (opp V) ; ::_thesis: verum
end;
end;

:: deftheorem  defines opp MOD_4:def_3_:_
 for K being non empty doubleLoopStr
for V being non empty VectSpStr 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 VectSpStr over K holds the rmult of (opp V) = opp the lmult of V
proof
let K be non empty doubleLoopStr ; ::_thesis: for V being non empty VectSpStr over K holds the rmult of (opp V) = opp the lmult of V
let V be non empty VectSpStr over K; ::_thesis: the rmult of (opp V) = opp the lmult of V
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  the rmult of (opp V) = opp the lmult of V ; ::_thesis: verum
end;

definition
let K be non empty doubleLoopStr ;
let W be non empty RightModStr over K;
func opp W ->  strict VectSpStr 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 = VectSpStr(# the carrier of W, the addF of W,(0. W),o #);
existence
 ex b1 being strict VectSpStr 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 = VectSpStr(# the carrier of W, the addF of W,(0. W),o #)
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 #) ; ::_thesis: 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
VectSpStr(# the carrier of W, the addF of W,(0. W),o #) = VectSpStr(# the carrier of W, the addF of W,(0. W),o #)
thus  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
VectSpStr(# the carrier of W, the addF of W,(0. W),o #) = VectSpStr(# the carrier of W, the addF of W,(0. W),o #) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict VectSpStr 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 = VectSpStr(# 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 = VectSpStr(# the carrier of W, the addF of W,(0. W),o #) ) holds
b1 = b2
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; ::_thesis: ( ( 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 #) ) & ( 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 #) ) implies M1 = M2 )
assume 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 #) ; ::_thesis: M1 = M2
thus M1 = VectSpStr(# the carrier of W, the addF of W,(0. W),o #) by A1
.= M2 by A2 ; ::_thesis: verum
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 VectSpStr 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 = VectSpStr(# 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
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  not the carrier of (opp W) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
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
let K be non empty doubleLoopStr ; ::_thesis: 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) ) ) )
let W be non empty RightModStr over K; ::_thesis: ( 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) ) ) )
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  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 #) ; ::_thesis: for x being set holds
( x is Vector of W iff x is Vector of (opp W) )
let x be set ; ::_thesis: ( x is Vector of W iff x is Vector of (opp W) )
thus  ( x is Vector of W iff x is Vector of (opp W) ) by A1; ::_thesis: verum
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
 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 #) 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  ~ o is Function of [: the carrier of (opp K), the carrier of (opp W):], the carrier of (opp W) ; ::_thesis: verum
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
let K be non empty doubleLoopStr ; ::_thesis: for W being non empty RightModStr over K holds the lmult of (opp W) = opp the rmult of W
let W be non empty RightModStr over K; ::_thesis: the lmult of (opp W) = opp the rmult of W
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  the lmult of (opp W) = opp the rmult of W ; ::_thesis: verum
end;

theorem :: MOD_4:11
for K being non empty doubleLoopStr
for V being non empty VectSpStr 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 Th1;

theorem Th12: :: MOD_4:12
for K, L being Ring
for V being non empty VectSpStr 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
let K, L be Ring; ::_thesis: for V being non empty VectSpStr 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
let V be non empty VectSpStr over K; ::_thesis: 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
let W be non empty RightModStr over L; ::_thesis: 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
let x be Scalar of K; ::_thesis: 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
let y be Scalar of L; ::_thesis: 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
let v be Vector of V; ::_thesis: for w being Vector of W st L = opp K & W = opp V & x = y & v = w holds
w * y = x * v
let w be Vector of W; ::_thesis: ( L = opp K & W = opp V & x = y & v = w implies w * y = x * v )
assume that
A1: ( L = opp K & W = opp V ) and
A2: ( x = y & v = w ) ; ::_thesis: w * y = x * v
set o = the lmult of V;
 opp the lmult of V = the rmult of (opp V) by Th8;
hence w * y = (opp the lmult of V) . (w,y) by A1, VECTSP_2:def_7
.= x * v by A2, Th1 ;
::_thesis: verum
end;

theorem Th13: :: MOD_4:13
for K, L being Ring
for V being non empty VectSpStr 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
let K, L be Ring; ::_thesis: for V being non empty VectSpStr 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
let V be non empty VectSpStr over K; ::_thesis: 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
A1: 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 #) by Th7;
let W be non empty RightModStr over L; ::_thesis: 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
let v1, v2 be Vector of V; ::_thesis: for w1, w2 being Vector of W st W = opp V & v1 = w1 & v2 = w2 holds
w1 + w2 = v1 + v2
let w1, w2 be Vector of W; ::_thesis: ( W = opp V & v1 = w1 & v2 = w2 implies w1 + w2 = v1 + v2 )
assume  ( W = opp V & v1 = w1 & v2 = w2 ) ; ::_thesis: w1 + w2 = v1 + v2
hence  w1 + w2 = v1 + v2 by A1; ::_thesis: verum
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 Th1;

theorem Th15: :: MOD_4:15
for K, L being Ring
for V being non empty VectSpStr 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
let K, L be Ring; ::_thesis: for V being non empty VectSpStr 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
let V be non empty VectSpStr over K; ::_thesis: 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
let W be non empty RightModStr over L; ::_thesis: 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
let x be Scalar of K; ::_thesis: 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
let y be Scalar of L; ::_thesis: 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
let v be Vector of V; ::_thesis: for w being Vector of W st V = opp W & x = y & v = w holds
w * y = x * v
let w be Vector of W; ::_thesis: ( V = opp W & x = y & v = w implies w * y = x * v )
assume A1: ( V = opp W & x = y & v = w ) ; ::_thesis: w * y = x * v
set o = the rmult of W;
A2: opp the rmult of W = the lmult of (opp W) by Th10;
thus w * y = the rmult of W . (w,y) by VECTSP_2:def_7
.= x * v by A1, A2, Th1 ; ::_thesis: verum
end;

theorem Th16: :: MOD_4:16
for K, L being Ring
for V being non empty VectSpStr 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
let K, L be Ring; ::_thesis: for V being non empty VectSpStr 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
let V be non empty VectSpStr over K; ::_thesis: 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
let W be non empty RightModStr over L; ::_thesis: 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
A1: 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 #) by Th9;
let v1, v2 be Vector of V; ::_thesis: for w1, w2 being Vector of W st V = opp W & v1 = w1 & v2 = w2 holds
w1 + w2 = v1 + v2
let w1, w2 be Vector of W; ::_thesis: ( V = opp W & v1 = w1 & v2 = w2 implies w1 + w2 = v1 + v2 )
assume  ( V = opp W & v1 = w1 & v2 = w2 ) ; ::_thesis: w1 + w2 = v1 + v2
hence  w1 + w2 = v1 + v2 by A1; ::_thesis: verum
end;

theorem :: MOD_4:17
for K being non empty strict doubleLoopStr
for V being non empty VectSpStr over K holds opp (opp V) = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
proof
let K be non empty strict doubleLoopStr ; ::_thesis: for V being non empty VectSpStr over K holds opp (opp V) = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
let V be non empty VectSpStr over K; ::_thesis: opp (opp V) = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
set W = opp V;
A1: opp (opp K) = K by FUNCT_4:53;
A2: opp the rmult of (opp V) = opp (opp the lmult of V) by Th8
.= the lmult of V by FUNCT_4:53 ;
addLoopStr(# the carrier of (opp (opp V)), the addF of (opp (opp V)), the ZeroF of (opp (opp V)) #) = addLoopStr(# the carrier of (opp V), the addF of (opp V), the ZeroF of (opp V) #) by Th9
.= addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) by Th7 ;
hence  opp (opp V) = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by A2, A1, Th10; ::_thesis: verum
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
let K be non empty strict doubleLoopStr ; ::_thesis: 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 #)
let W be non empty RightModStr over K; ::_thesis: opp (opp W) = RightModStr(# the carrier of W, the addF of W, the ZeroF of W, the rmult of W #)
set V = opp W;
A1: opp (opp K) = K by FUNCT_4:53;
A2: opp the lmult of (opp W) = opp (opp the rmult of W) by Th10
.= the rmult of W by FUNCT_4:53 ;
addLoopStr(# the carrier of (opp (opp W)), the addF of (opp (opp W)), the ZeroF of (opp (opp W)) #) = addLoopStr(# the carrier of (opp W), the addF of (opp W), the ZeroF of (opp W) #) by Th7
.= addLoopStr(# the carrier of W, the addF of W, the ZeroF of W #) by Th9 ;
hence  opp (opp W) = RightModStr(# the carrier of W, the addF of W, the ZeroF of W, the rmult of W #) by A2, A1, Th8; ::_thesis: verum
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
let K be Ring; ::_thesis: for V being LeftMod of K holds opp V is strict RightMod of opp K
let V be LeftMod of K; ::_thesis: opp V is strict RightMod of opp K
set R = opp K;
reconsider W = opp V as non empty RightModStr over opp K ;
A1: 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 #) by Th7;
then A2: for a, b being Element of (opp V)
for x, y being Element of V st x = a & b = y holds
a + b = x + y ;
A3: ( opp V is Abelian & opp V is add-associative & opp V is right_zeroed & opp V is right_complementable )
proof
thus  opp V is Abelian ::_thesis: ( opp V is add-associative & opp V is right_zeroed & opp V is right_complementable )
proof
let a, b be Element of (opp V); :: according to RLVECT_1:def_2 ::_thesis: a + b = b + a
reconsider x = a, y = b as Element of V by Th7;
thus a + b = y + x by A2
.= b + a by A1 ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_3 ::_thesis: ( opp V is right_zeroed & opp V is right_complementable )
let a, b, c be Element of (opp V); ::_thesis: (a + b) + c = a + (b + c)
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 ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_4 ::_thesis: opp V is right_complementable
let a be Element of (opp V); ::_thesis: a + (0. (opp V)) = a
reconsider x = a as Element of V by Th7;
thus a + (0. (opp V)) = x + (0. V) by A1
.= a by RLVECT_1:4 ; ::_thesis: verum
end;
let a be Element of (opp V); :: according to ALGSTR_0:def_16 ::_thesis: a is right_complementable
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 ; :: according to ALGSTR_0:def_11 ::_thesis: a + b9 = 0. (opp V)
thus  a + b9 = 0. (opp V) by A1, A4; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_Scalar_of_(opp_K)
for_v,_w_being_Vector_of_W_holds_
(_(v_+_w)_*_x_=_(v_*_x)_+_(w_*_x)_&_v_*_(x_+_y)_=_(v_*_x)_+_(v_*_y)_&_v_*_(y_*_x)_=_(v_*_y)_*_x_&_v_*_(1__(opp_K))_=_v_)
let x, y be Scalar of (opp K); ::_thesis: for v, w being Vector of W holds
( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ (opp K)) = v )
let v, w be Vector of W; ::_thesis: ( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ (opp K)) = v )
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 ;
::_thesis: ( v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ (opp K)) = v )
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 ; ::_thesis: ( v * (y * x) = (v * y) * x & v * (1_ (opp K)) = v )
thus v * (y * x) = (a * b) * p by Lm3, Th12
.= a * (b * p) by VECTSP_1:def_16
.= (v * y) * x by A5, Th12 ; ::_thesis: v * (1_ (opp K)) = v
thus v * (1_ (opp K)) = (1_ K) * p by Th12
.= v by VECTSP_1:def_17 ; ::_thesis: verum
end;
hence  opp V is strict RightMod of opp K by A3, VECTSP_2:def_9; ::_thesis: verum
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
let K be Ring; ::_thesis: for W being RightMod of K holds opp W is strict LeftMod of opp K
let W be RightMod of K; ::_thesis: opp W is strict LeftMod of opp K
set R = opp K;
reconsider V = opp W as non empty VectSpStr over opp K ;
A1: 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 #) by Th9;
then A2: for a, b being Element of (opp W)
for x, y being Element of W st x = a & b = y holds
a + b = x + y ;
A3: ( opp W is Abelian & opp W is add-associative & opp W is right_zeroed & opp W is right_complementable )
proof
thus  opp W is Abelian ::_thesis: ( opp W is add-associative & opp W is right_zeroed & opp W is right_complementable )
proof
let a, b be Element of (opp W); :: according to RLVECT_1:def_2 ::_thesis: a + b = b + a
reconsider x = a, y = b as Element of W by Th9;
thus a + b = y + x by A2
.= b + a by A1 ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_3 ::_thesis: ( opp W is right_zeroed & opp W is right_complementable )
let a, b, c be Element of (opp W); ::_thesis: (a + b) + c = a + (b + c)
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 ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_4 ::_thesis: opp W is right_complementable
let a be Element of (opp W); ::_thesis: a + (0. (opp W)) = a
reconsider x = a as Element of W by Th9;
thus a + (0. (opp W)) = x + (0. W) by A1
.= a by RLVECT_1:4 ; ::_thesis: verum
end;
let a be Element of (opp W); :: according to ALGSTR_0:def_16 ::_thesis: a is right_complementable
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 ; :: according to ALGSTR_0:def_11 ::_thesis: a + b9 = 0. (opp W)
thus  a + b9 = 0. (opp W) by A1, A4; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_Scalar_of_(opp_K)
for_v,_w_being_Vector_of_V_holds_
(_x_*_(v_+_w)_=_(x_*_v)_+_(x_*_w)_&_(x_+_y)_*_v_=_(x_*_v)_+_(y_*_v)_&_(x_*_y)_*_v_=_x_*_(y_*_v)_&_(1__(opp_K))_*_v_=_v_)
let x, y be Scalar of (opp K); ::_thesis: for v, w being Vector of V holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ (opp K)) * v = v )
let v, w be Vector of V; ::_thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ (opp K)) * v = 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 ;
::_thesis: ( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ (opp K)) * v = v )
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 ; ::_thesis: ( (x * y) * v = x * (y * v) & (1_ (opp K)) * v = v )
 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 ;
::_thesis: (1_ (opp K)) * v = v
thus (1_ (opp K)) * v = p * (1_ K) by Th15
.= v by VECTSP_2:def_9 ; ::_thesis: verum
end;
hence  opp W is strict LeftMod of opp K by A3, VECTSP_1:def_14, VECTSP_1:def_15, VECTSP_1:def_16, VECTSP_1:def_17; ::_thesis: verum
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;

begin

definition
let K, L be non empty multMagma ;
let IT be Function of K,L;
attrIT 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;
attrIT is antilinear  means :Def7: :: MOD_4:def 7
( IT is additive & IT is antimultiplicative & IT is unity-preserving );
end;

:: deftheorem Def7 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 ) );

registration
let K, L be non empty doubleLoopStr ;
cluster Function-like quasi_total antilinear  ->  unity-preserving additive 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 ) by Def7;
cluster Function-like quasi_total unity-preserving additive 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 by Def7;
end;

definition
let K, L be non empty doubleLoopStr ;
let IT be Function of K,L;
attrIT is monomorphism  means :Def8: :: MOD_4:def 8
( IT is linear & IT is one-to-one );
attrIT is antimonomorphism  means :Def9: :: MOD_4:def 9
( IT is antilinear & IT is one-to-one );
end;

:: deftheorem Def8 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 Def9 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 ) );

definition
let K, L be non empty doubleLoopStr ;
let IT be Function of K,L;
attrIT is epimorphism  means :Def10: :: MOD_4:def 10
( IT is linear & IT is onto );
attrIT is antiepimorphism  means :Def11: :: MOD_4:def 11
( IT is antilinear & IT is onto );
end;

:: deftheorem Def10 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 Def11 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;
attrIT is isomorphism  means :Def12: :: MOD_4:def 12
( IT is monomorphism & IT is onto );
attrIT is antiisomorphism  means :Def13: :: MOD_4:def 13
( IT is antimonomorphism & IT is onto );
end;

:: deftheorem Def12 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 Def13 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 ) );

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

:: deftheorem Def14 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 Def15 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 );

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
let K be non empty doubleLoopStr ; ::_thesis: 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 ) )
let J be Function of K,K; ::_thesis: ( 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 ) )
A1: now__::_thesis:_(_J_is_isomorphism_implies_(_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_)_)
assume A2: J is isomorphism ; ::_thesis: ( 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 )
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; ::_thesis: ( J is one-to-one & J is onto )
thus  J is one-to-one by A3, Def8; ::_thesis: J is onto
thus  J is onto by A2, Def12; ::_thesis: verum
end;
now__::_thesis:_(_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_implies_J_is_isomorphism_)
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 ; ::_thesis: J is isomorphism
 ( J is multiplicative & J is 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; ::_thesis: verum
end;
hence  ( 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 ) ) by A1; ::_thesis: verum
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
let K be non empty doubleLoopStr ; ::_thesis: 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 ) )
let J be Function of K,K; ::_thesis: ( 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 ) )
A1: now__::_thesis:_(_J_is_antiisomorphism_implies_(_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_)_)
assume A2: J is antiisomorphism ; ::_thesis: ( 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 )
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; ::_thesis: ( J is one-to-one & J is onto )
thus  J is one-to-one by A3, Def9; ::_thesis: J is onto
thus  J is onto by A2, Def13; ::_thesis: verum
end;
now__::_thesis:_(_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_implies_J_is_antiisomorphism_)
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 ; ::_thesis: J is antiisomorphism
 ( J is additive & J is antimultiplicative & J is unity-preserving ) by A4, Def6, GROUP_1:def_13;
then  J is antimonomorphism by A5, Def9;
hence  J is antiisomorphism by A6, Def13; ::_thesis: verum
end;
hence  ( 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 ) ) by A1; ::_thesis: verum
end;

Lm6:  for K being non empty doubleLoopStr holds
( ( 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
let K be non empty doubleLoopStr ; ::_thesis: ( ( for x, y being Scalar of K holds (id K) . (x * y) = ((id K) . x) * ((id K) . y) ) & (id K) . (1_ K) = 1_ K )
set J = id K;
thus  for x, y being Scalar of K holds (id K) . (x * y) = ((id K) . x) * ((id K) . y) ::_thesis: (id K) . (1_ K) = 1_ K
proof
let x, y be Scalar of K; ::_thesis: (id K) . (x * y) = ((id K) . x) * ((id K) . y)
 ( (id K) . (x * y) = x * y & (id K) . x = x ) by FUNCT_1:18;
hence  (id K) . (x * y) = ((id K) . x) * ((id K) . y) by FUNCT_1:18; ::_thesis: verum
end;
thus  (id K) . (1_ K) = 1_ K by FUNCT_1:18; ::_thesis: verum
end;

registration
let K be non empty doubleLoopStr ;
cluster id K ->  isomorphism ;
coherence
 id K is isomorphism
proof
set J = id K;
 id K is monomorphism by Def8;
hence  id K is isomorphism by Def12; ::_thesis: verum
end;
end;

     Lm7:  for K, L being Ring
for J being Function of K,L st J is additive holds
J . (0. K) = 0. L
proof
let K, L be Ring; ::_thesis: for J being Function of K,L st J is additive holds
J . (0. K) = 0. L
let J be Function of K,L; ::_thesis: ( J is additive implies J . (0. K) = 0. L )
set a = 0. K;
assume A1: J is additive ; ::_thesis: J . (0. K) = 0. L
 (0. K) + (0. K) = 0. K by RLVECT_1:4;
then (J . (0. K)) + (J . (0. K)) = J . (0. K) by A1, VECTSP_1:def_20
.= (J . (0. K)) + (0. L) by RLVECT_1:4 ;
hence  J . (0. K) = 0. L by RLVECT_1:8; ::_thesis: verum
end;

Lm8:  for L, K 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
let L, K be Ring; ::_thesis: for J being Function of K,L
for x being Scalar of K st J is linear holds
J . (- x) = - (J . x)
let J be Function of K,L; ::_thesis: for x being Scalar of K st J is linear holds
J . (- x) = - (J . x)
let x be Scalar of K; ::_thesis: ( J is linear implies J . (- x) = - (J . x) )
set a = 0. K;
set b = 0. L;
set y = J . x;
A1: x + (- x) = 0. K by RLVECT_1:5;
A2: (J . x) + (- (J . x)) = 0. L by RLVECT_1:5;
assume A3: J is linear ; ::_thesis: J . (- x) = - (J . x)
then (J . x) + (J . (- x)) = J . (0. K) by A1, VECTSP_1:def_20
.= 0. L by A3, Lm7 ;
hence  J . (- x) = - (J . x) by A2, RLVECT_1:8; ::_thesis: verum
end;

Lm9:  for L, K 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
let L, K be Ring; ::_thesis: 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)
let J be Function of K,L; ::_thesis: for x, y being Scalar of K st J is linear holds
J . (x - y) = (J . x) - (J . y)
let x, y be Scalar of K; ::_thesis: ( J is linear implies J . (x - y) = (J . x) - (J . y) )
assume A1: J is linear ; ::_thesis: J . (x - y) = (J . x) - (J . y)
hence J . (x - y) = (J . x) + (J . (- y)) by VECTSP_1:def_20
.= (J . x) - (J . y) by A1, Lm8 ;
::_thesis: verum
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 Lm7, Lm8, Lm9;

Lm10:  for K, L being Ring
for J being Function of K,L st J is antilinear holds
J . (0. K) = 0. L
proof
let K, L be Ring; ::_thesis: for J being Function of K,L st J is antilinear holds
J . (0. K) = 0. L
let J be Function of K,L; ::_thesis: ( J is antilinear implies J . (0. K) = 0. L )
set a = 0. K;
A1: (0. K) + (0. K) = 0. K by RLVECT_1:4;
assume  J is antilinear ; ::_thesis: J . (0. K) = 0. L
then (J . (0. K)) + (J . (0. K)) = J . (0. K) by A1, VECTSP_1:def_20
.= (J . (0. K)) + (0. L) by RLVECT_1:4 ;
hence  J . (0. K) = 0. L by RLVECT_1:8; ::_thesis: verum
end;

Lm11:  for L, K 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
let L, K be Ring; ::_thesis: for J being Function of K,L
for x being Scalar of K st J is antilinear holds
J . (- x) = - (J . x)
let J be Function of K,L; ::_thesis: for x being Scalar of K st J is antilinear holds
J . (- x) = - (J . x)
let x be Scalar of K; ::_thesis: ( J is antilinear implies J . (- x) = - (J . x) )
assume A1: J is antilinear ; ::_thesis: J . (- x) = - (J . x)
set a = 0. K;
set b = 0. L;
set y = J . x;
A2: (J . x) + (- (J . x)) = 0. L by RLVECT_1:5;
 x + (- x) = 0. K by RLVECT_1:5;
then (J . x) + (J . (- x)) = J . (0. K) by A1, VECTSP_1:def_20
.= 0. L by A1, Lm10 ;
hence  J . (- x) = - (J . x) by A2, RLVECT_1:8; ::_thesis: verum
end;

Lm12:  for L, K 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
let L, K be Ring; ::_thesis: 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)
let J be Function of K,L; ::_thesis: for x, y being Scalar of K st J is antilinear holds
J . (x - y) = (J . x) - (J . y)
let x, y be Scalar of K; ::_thesis: ( J is antilinear implies J . (x - y) = (J . x) - (J . y) )
assume A1: J is antilinear ; ::_thesis: J . (x - y) = (J . x) - (J . y)
hence J . (x - y) = (J . x) + (J . (- y)) by VECTSP_1:def_20
.= (J . x) - (J . y) by A1, Lm11 ;
::_thesis: verum
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 Lm10, Lm11, Lm12;

theorem :: MOD_4:25
for K being Ring holds
( id K is antiisomorphism iff K is comRing )
proof
let K be Ring; ::_thesis: ( id K is antiisomorphism iff K is comRing )
set J = id K;
A1: now__::_thesis:_(_K_is_comRing_implies_id_K_is_antiisomorphism_)
assume A2: K is comRing ; ::_thesis: id K is antiisomorphism
A3: for x, y being Scalar of K holds (id K) . (x * y) = ((id K) . y) * ((id K) . x)
proof
let x, y be Scalar of K; ::_thesis: (id K) . (x * y) = ((id K) . y) * ((id K) . x)
A4: (id K) . y = y by FUNCT_1:18;
 ( (id K) . (x * y) = x * y & (id K) . x = x ) by FUNCT_1:18;
hence  (id K) . (x * y) = ((id K) . y) * ((id K) . x) by A2, A4, Lm5; ::_thesis: verum
end;
 (id K) . (1_ K) = 1_ K by Lm6;
hence  id K is antiisomorphism by A3, Th22; ::_thesis: verum
end;
now__::_thesis:_(_id_K_is_antiisomorphism_implies_K_is_comRing_)
assume A5: id K is antiisomorphism ; ::_thesis: K is comRing
 for x, y being Element of K holds x * y = y * x
proof
let x, y be Element of K; ::_thesis: x * y = y * x
A6: (id K) . y = y by FUNCT_1:18;
 ( (id K) . (x * y) = x * y & (id K) . x = x ) by FUNCT_1:18;
hence  x * y = y * x by A5, A6, Th22; ::_thesis: verum
end;
hence  K is comRing by GROUP_1:def_12; ::_thesis: verum
end;
hence  ( id K is antiisomorphism iff K is comRing ) by A1; ::_thesis: verum
end;

theorem :: MOD_4:26
for K being Skew-Field holds
( id K is antiisomorphism iff K is Field )
proof
let K be Skew-Field; ::_thesis: ( id K is antiisomorphism iff K is Field )
set J = id K;
A1: now__::_thesis:_(_K_is_Field_implies_id_K_is_antiisomorphism_)
assume A2: K is Field ; ::_thesis: id K is antiisomorphism
A3: for x, y being Scalar of K holds (id K) . (x * y) = ((id K) . y) * ((id K) . x)
proof
let x, y be Scalar of K; ::_thesis: (id K) . (x * y) = ((id K) . y) * ((id K) . x)
A4: (id K) . y = y by FUNCT_1:18;
 ( (id K) . (x * y) = x * y & (id K) . x = x ) by FUNCT_1:18;
hence  (id K) . (x * y) = ((id K) . y) * ((id K) . x) by A2, A4, GROUP_1:def_12; ::_thesis: verum
end;
 (id K) . (1_ K) = 1_ K by Lm6;
hence  id K is antiisomorphism by A3, Th22; ::_thesis: verum
end;
now__::_thesis:_(_id_K_is_antiisomorphism_implies_K_is_Field_)
assume A5: id K is antiisomorphism ; ::_thesis: K is Field
 for x, y being Scalar of K holds x * y = y * x
proof
let x, y be Scalar of K; ::_thesis: x * y = y * x
A6: (id K) . y = y by FUNCT_1:18;
 ( (id K) . (x * y) = x * y & (id K) . x = x ) by FUNCT_1:18;
hence  x * y = y * x by A5, A6, Th22; ::_thesis: verum
end;
hence  K is Field by GROUP_1:def_12; ::_thesis: verum
end;
hence  ( id K is antiisomorphism iff K is Field ) by A1; ::_thesis: verum
end;

begin

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;

      Lm13:  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
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ; ::_thesis: 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
let L be non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for J being Function of K,L st J is linear holds
opp J is additive
let J be Function of K,L; ::_thesis: ( J is linear implies opp J is additive )
set J9 = opp J;
assume A1: J is linear ; ::_thesis: opp J is additive
let x, y be Scalar of K; :: according to VECTSP_1:def_20 ::_thesis: (opp J) . (x + y) = ((opp J) . x) + ((opp J) . y)
thus (opp J) . (x + y) = (J . x) + (J . y) by A1, VECTSP_1:def_20
.= ((opp J) . x) + ((opp J) . y) ; ::_thesis: verum
end;

theorem :: MOD_4:27
canceled;

theorem Th28: :: 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
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 )
let L be non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for J being Function of K,L holds
( J is linear iff opp J is antilinear )
let J be Function of K,L; ::_thesis: ( J is linear iff opp J is antilinear )
set J9 = opp J;
set L9 = opp L;
A1: now__::_thesis:_(_J_is_linear_implies_opp_J_is_antilinear_)
assume A2: J is linear ; ::_thesis: opp J is antilinear
A3: for x, y being Scalar of K holds (opp J) . (x * y) = ((opp J) . y) * ((opp J) . x)
proof
let x, y be Scalar of K; ::_thesis: (opp J) . (x * y) = ((opp J) . y) * ((opp J) . x)
thus (opp J) . (x * y) = (J . x) * (J . y) by A2, GROUP_6:def_6
.= ((opp J) . y) * ((opp J) . x) by Lm3 ; ::_thesis: verum
end;
(opp J) . (1_ K) = 1_ L by A2, GROUP_1:def_13
.= 1_ (opp L) ;
then  ( opp J is additive & opp J is antimultiplicative & opp J is unity-preserving ) by Lm13, A3, Def6, A2, GROUP_1:def_13;
hence  opp J is antilinear ; ::_thesis: verum
end;
now__::_thesis:_(_opp_J_is_antilinear_implies_J_is_linear_)
assume A4: opp J is antilinear ; ::_thesis: J is linear
A5: for x, y being Scalar of K holds J . (x + y) = (J . x) + (J . y)
proof
let x, y be Scalar of K; ::_thesis: J . (x + y) = (J . x) + (J . y)
thus J . (x + y) = ((opp J) . x) + ((opp J) . y) by A4, VECTSP_1:def_20
.= (J . x) + (J . y) ; ::_thesis: verum
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; ::_thesis: J . (x * y) = (J . x) * (J . y)
thus J . (x * y) = ((opp J) . y) * ((opp J) . x) by A4, Def6
.= (J . x) * (J . y) by Lm3 ; ::_thesis: verum
end;
J . (1_ K) = 1_ (opp L) by A4, GROUP_1:def_13
.= 1_ L ;
then  ( J is additive & J is multiplicative & J is unity-preserving ) by A5, A6, VECTSP_1:def_20, GROUP_1:def_13, GROUP_6:def_6;
hence  J is linear ; ::_thesis: verum
end;
hence  ( J is linear iff opp J is antilinear ) by A1; ::_thesis: verum
end;

theorem Th29: :: 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
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 )
let L be non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for J being Function of K,L holds
( J is antilinear iff opp J is linear )
let J be Function of K,L; ::_thesis: ( J is antilinear iff opp J is linear )
set J9 = opp J;
set L9 = opp L;
hereby  ::_thesis: ( opp J is linear implies J is antilinear )
assume A1: J is antilinear ; ::_thesis: opp J is linear
A2: opp J is additive
proof
let x, y be Scalar of K; :: according to VECTSP_1:def_20 ::_thesis: (opp J) . (x + y) = ((opp J) . x) + ((opp J) . y)
thus (opp J) . (x + y) = (J . x) + (J . y) by A1, VECTSP_1:def_20
.= ((opp J) . x) + ((opp J) . y) ; ::_thesis: verum
end;
A3: opp J is multiplicative
proof
let x, y be Scalar of K; :: according to GROUP_6:def_6 ::_thesis: (opp J) . (x * y) = ((opp J) . x) * ((opp J) . y)
thus (opp J) . (x * y) = (J . y) * (J . x) by A1, Def6
.= ((opp J) . x) * ((opp J) . y) by Lm3 ; ::_thesis: verum
end;
(opp J) . (1_ K) = 1_ L by A1, GROUP_1:def_13
.= 1_ (opp L) ;
then  opp J is unity-preserving by GROUP_1:def_13;
hence  opp J is linear by A2, A3; ::_thesis: verum
end;
assume A4: ( opp J is additive & opp J is multiplicative & opp J is unity-preserving ) ; :: according to RINGCAT1:def_1 ::_thesis: J is antilinear
hereby  :: according to VECTSP_1:def_20,MOD_4:def_7 ::_thesis: ( J is antimultiplicative & J is unity-preserving )
let x, y be Scalar of K; ::_thesis: J . (x + y) = (J . x) + (J . y)
thus J . (x + y) = ((opp J) . x) + ((opp J) . y) by A4, VECTSP_1:def_20
.= (J . x) + (J . y) ; ::_thesis: verum
end;
hereby  :: according to MOD_4:def_6 ::_thesis: J is unity-preserving
let x, y be Scalar of K; ::_thesis: J . (x * y) = (J . y) * (J . x)
thus J . (x * y) = ((opp J) . x) * ((opp J) . y) by A4, GROUP_6:def_6
.= (J . y) * (J . x) by Lm3 ; ::_thesis: verum
end;
thus J . (1_ K) = 1_ (opp L) by A4, GROUP_1:def_13
.= 1_ L ; :: according to GROUP_1:def_13 ::_thesis: verum
end;

theorem Th30: :: 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 )
proof
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 )
let L be non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for J being Function of K,L holds
( J is monomorphism iff opp J is antimonomorphism )
let J be Function of K,L; ::_thesis: ( J is monomorphism iff opp J is antimonomorphism )
set J9 = opp J;
A1: ( J is linear iff opp J is antilinear ) by Th28;
 ( opp J is antimonomorphism iff ( opp J is antilinear & opp J is one-to-one ) ) by Def9;
hence  ( J is monomorphism iff opp J is antimonomorphism ) by A1, Def8; ::_thesis: verum
end;

theorem Th31: :: 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 )
proof
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 )
let L be non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for J being Function of K,L holds
( J is antimonomorphism iff opp J is monomorphism )
let J be Function of K,L; ::_thesis: ( J is antimonomorphism iff opp J is monomorphism )
set J9 = opp J;
A1: ( J is antilinear iff opp J is linear ) by Th29;
 ( opp J is monomorphism iff ( opp J is linear & opp J is one-to-one ) ) by Def8;
hence  ( J is antimonomorphism iff opp J is monomorphism ) by A1, Def9; ::_thesis: verum
end;

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 )
proof
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 )
let L be non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for J being Function of K,L holds
( J is epimorphism iff opp J is antiepimorphism )
let J be Function of K,L; ::_thesis: ( J is epimorphism iff opp J is antiepimorphism )
set J9 = opp J;
set L9 = opp L;
 ( J is linear iff opp J is antilinear ) by Th28;
hence  ( J is epimorphism iff opp J is antiepimorphism ) by Def10, Def11; ::_thesis: verum
end;

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 )
proof
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 )
let L be non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for J being Function of K,L holds
( J is antiepimorphism iff opp J is epimorphism )
let J be Function of K,L; ::_thesis: ( J is antiepimorphism iff opp J is epimorphism )
set J9 = opp J;
set L9 = opp L;
 ( J is antilinear iff opp J is linear ) by Th29;
hence  ( J is antiepimorphism iff opp J is epimorphism ) by Def10, Def11; ::_thesis: verum
end;

theorem Th34: :: 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 )
proof
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 )
let L be non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for J being Function of K,L holds
( J is isomorphism iff opp J is antiisomorphism )
let J be Function of K,L; ::_thesis: ( J is isomorphism iff opp J is antiisomorphism )
set J9 = opp J;
set L9 = opp L;
 ( J is monomorphism iff opp J is antimonomorphism ) by Th30;
hence  ( J is isomorphism iff opp J is antiisomorphism ) by Def12, Def13; ::_thesis: verum
end;

theorem Th35: :: 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 )
proof
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ; ::_thesis: 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 )
let L be non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for J being Function of K,L holds
( J is antiisomorphism iff opp J is isomorphism )
let J be Function of K,L; ::_thesis: ( J is antiisomorphism iff opp J is isomorphism )
set J9 = opp J;
set L9 = opp L;
 ( J is antimonomorphism iff opp J is monomorphism ) by Th31;
hence  ( J is antiisomorphism iff opp J is isomorphism ) by Def12, Def13; ::_thesis: verum
end;


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 )
proof
let K be non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for J being Function of K,K holds
( J is endomorphism iff opp J is antilinear )
let J be Function of K,K; ::_thesis: ( J is endomorphism iff opp J is antilinear )
 ( J is linear iff opp J is antilinear ) by Th28;
hence  ( J is endomorphism iff opp J is antilinear ) by Def14; ::_thesis: verum
end;

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 )
proof
let K be non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for J being Function of K,K holds
( J is antiendomorphism iff opp J is linear )
let J be Function of K,K; ::_thesis: ( J is antiendomorphism iff opp J is linear )
 ( J is antilinear iff opp J is linear ) by Th29;
hence  ( J is antiendomorphism iff opp J is linear ) by Def15; ::_thesis: verum
end;

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 Th34;

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 Th35;

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 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
take  id G ; ::_thesis: id G is bijective
thus  id G is bijective ; ::_thesis: verum
end;
end;

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

     Lm14:  for G, H being AddGroup
for f being Homomorphism of G,H holds f . (0. G) = 0. H
proof
let G, H be AddGroup; ::_thesis: for f being Homomorphism of G,H holds f . (0. G) = 0. H
let f be Homomorphism of G,H; ::_thesis: f . (0. G) = 0. H
set a = 0. G;
 (0. G) + (0. G) = 0. G by RLVECT_1:def_4;
then (f . (0. G)) + (f . (0. G)) = f . (0. G) by VECTSP_1:def_20
.= (f . (0. G)) + (0. H) by RLVECT_1:def_4 ;
hence  f . (0. G) = 0. H by RLVECT_1:8; ::_thesis: verum
end;

Lm15:  for H, G being AddGroup
for f being Homomorphism of G,H
for x being Element of G holds f . (- x) = - (f . x)
proof
let H, G be AddGroup; ::_thesis: for f being Homomorphism of G,H
for x being Element of G holds f . (- x) = - (f . x)
let f be Homomorphism of G,H; ::_thesis: for x being Element of G holds f . (- x) = - (f . x)
let x be Element of G; ::_thesis: f . (- x) = - (f . x)
set a = 0. G;
set b = 0. H;
set y = f . x;
 x + (- x) = 0. G by RLVECT_1:def_10;
then (f . x) + (f . (- x)) = f . (0. G) by VECTSP_1:def_20
.= 0. H by Lm14 ;
hence  f . (- x) = - (f . x) by VECTSP_1:16; ::_thesis: verum
end;

Lm16:  for H, G 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
let H, G be AddGroup; ::_thesis: for f being Homomorphism of G,H
for x, y being Element of G holds f . (x - y) = (f . x) - (f . y)
let f be Homomorphism of G,H; ::_thesis: for x, y being Element of G holds f . (x - y) = (f . x) - (f . y)
let x, y be Element of G; ::_thesis: f . (x - y) = (f . x) - (f . y)
thus f . (x - y) = (f . x) + (f . (- y)) by VECTSP_1:def_20
.= (f . x) - (f . y) by Lm15 ; ::_thesis: verum
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 Lm14, Lm15, Lm16;

begin

          Lm17:  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
let K, L be Ring; ::_thesis: 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)
let V be LeftMod of K; ::_thesis: 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)
let W be LeftMod of L; ::_thesis: for x, y being Vector of V holds (ZeroMap (V,W)) . (x + y) = ((ZeroMap (V,W)) . x) + ((ZeroMap (V,W)) . y)
set f = ZeroMap (V,W);
thus  for x, y being Vector of V holds (ZeroMap (V,W)) . (x + y) = ((ZeroMap (V,W)) . x) + ((ZeroMap (V,W)) . y) ::_thesis: verum
proof
let x, y be Vector of V; ::_thesis: (ZeroMap (V,W)) . (x + y) = ((ZeroMap (V,W)) . x) + ((ZeroMap (V,W)) . y)
A1: (ZeroMap (V,W)) . y = 0. W by FUNCOP_1:7;
 ( (ZeroMap (V,W)) . (x + y) = 0. W & (ZeroMap (V,W)) . x = 0. W ) by FUNCOP_1:7;
hence  (ZeroMap (V,W)) . (x + y) = ((ZeroMap (V,W)) . x) + ((ZeroMap (V,W)) . y) by A1, RLVECT_1:def_4; ::_thesis: verum
end;
end;

Lm18:  for L, K 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
let L, K be Ring; ::_thesis: 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)
let J be Function of K,L; ::_thesis: 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)
let V be LeftMod of K; ::_thesis: 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)
let W be LeftMod of L; ::_thesis: for a being Scalar of K
for x being Vector of V holds (ZeroMap (V,W)) . (a * x) = (J . a) * ((ZeroMap (V,W)) . x)
let a be Scalar of K; ::_thesis: for x being Vector of V holds (ZeroMap (V,W)) . (a * x) = (J . a) * ((ZeroMap (V,W)) . x)
let x be Vector of V; ::_thesis: (ZeroMap (V,W)) . (a * x) = (J . a) * ((ZeroMap (V,W)) . x)
set z = ZeroMap (V,W);
 ( (ZeroMap (V,W)) . (a * x) = 0. W & (ZeroMap (V,W)) . x = 0. W ) by FUNCOP_1:7;
hence  (ZeroMap (V,W)) . (a * x) = (J . a) * ((ZeroMap (V,W)) . x) by VECTSP_1:14; ::_thesis: verum
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
take  ZeroMap (V,W) ; ::_thesis: ( ( for x, y being Vector of V holds (ZeroMap (V,W)) . (x + y) = ((ZeroMap (V,W)) . x) + ((ZeroMap (V,W)) . y) ) & ( for a being Scalar of K
for x being Vector of V holds (ZeroMap (V,W)) . (a * x) = (J . a) * ((ZeroMap (V,W)) . x) ) )
thus  ( ( for x, y being Vector of V holds (ZeroMap (V,W)) . (x + y) = ((ZeroMap (V,W)) . x) + ((ZeroMap (V,W)) . y) ) & ( for a being Scalar of K
for x being Vector of V holds (ZeroMap (V,W)) . (a * x) = (J . a) * ((ZeroMap (V,W)) . x) ) ) by Lm17, Lm18; ::_thesis: verum
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
let K, L be Ring; ::_thesis: 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
let J be Function of K,L; ::_thesis: for V being LeftMod of K
for W being LeftMod of L holds ZeroMap (V,W) is Homomorphism of J,V,W
let V be LeftMod of K; ::_thesis: for W being LeftMod of L holds ZeroMap (V,W) is Homomorphism of J,V,W
let W be LeftMod of L; ::_thesis: ZeroMap (V,W) is Homomorphism of J,V,W
set z = ZeroMap (V,W);
 ( ( for x, y being Vector of V holds (ZeroMap (V,W)) . (x + y) = ((ZeroMap (V,W)) . x) + ((ZeroMap (V,W)) . y) ) & ( for a being Scalar of K
for x being Vector of V holds (ZeroMap (V,W)) . (a * x) = (J . a) * ((ZeroMap (V,W)) . x) ) ) by Lm17, Lm18;
hence  ZeroMap (V,W) is Homomorphism of J,V,W by Def17; ::_thesis: verum
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
let K be Ring; ::_thesis: 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) ) ) )
let V, W be LeftMod of K; ::_thesis: 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) ) ) )
let f be Function of V,W; ::_thesis: ( 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) ) ) )
set J = id K;
A1: now__::_thesis:_(_(_for_a_being_Scalar_of_K
for_x_being_Vector_of_V_holds_f_._(a_*_x)_=_a_*_(f_._x)_)_implies_for_a_being_Scalar_of_K
for_x_being_Vector_of_V_holds_f_._(a_*_x)_=_((id_K)_._a)_*_(f_._x)_)
assume A2: for a being Scalar of K
for x being Vector of V holds f . (a * x) = a * (f . x) ; ::_thesis: for a being Scalar of K
for x being Vector of V holds f . (a * x) = ((id K) . a) * (f . x)
let a be Scalar of K; ::_thesis: for x being Vector of V holds f . (a * x) = ((id K) . a) * (f . x)
let x be Vector of V; ::_thesis: f . (a * x) = ((id K) . a) * (f . x)
 (id K) . a = a by FUNCT_1:18;
hence  f . (a * x) = ((id K) . a) * (f . x) by A2; ::_thesis: verum
end;
now__::_thesis:_(_(_for_a_being_Scalar_of_K
for_x_being_Vector_of_V_holds_f_._(a_*_x)_=_((id_K)_._a)_*_(f_._x)_)_implies_for_a_being_Scalar_of_K
for_x_being_Vector_of_V_holds_f_._(a_*_x)_=_a_*_(f_._x)_)
assume A3: for a being Scalar of K
for x being Vector of V holds f . (a * x) = ((id K) . a) * (f . x) ; ::_thesis: for a being Scalar of K
for x being Vector of V holds f . (a * x) = a * (f . x)
let a be Scalar of K; ::_thesis: for x being Vector of V holds f . (a * x) = a * (f . x)
let x be Vector of V; ::_thesis: f . (a * x) = a * (f . x)
 (id K) . a = a by FUNCT_1:18;
hence  f . (a * x) = a * (f . x) by A3; ::_thesis: verum
end;
hence  ( 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) ) ) ) by A1, Def17; ::_thesis: verum
end;

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