:: by Micha{\l} Muzalewski

::

:: Received June 22, 1992

:: Copyright (c) 1992-2018 Association of Mizar Users

registration
end;

theorem :: MOD_4:1

definition

let K be non empty doubleLoopStr ;

coherence

doubleLoopStr(# the carrier of K, the addF of K,(~ the multF of K),(1. K),(0. K) #) is strict doubleLoopStr ;

;

end;
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 doubleLoopStr(# the carrier of K, the addF of K,(~ the multF of K),(1. K),(0. K) #);

coherence

doubleLoopStr(# the carrier of K, the addF of K,(~ the multF of K),(1. K),(0. K) #) is strict doubleLoopStr ;

;

:: 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) #);

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) #);

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
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 )

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

end;
( (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;
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

registration

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

coherence

( opp K is add-associative & opp K is right_zeroed & opp K is right_complementable )

end;
coherence

( opp K is add-associative & opp K is right_zeroed & opp K is right_complementable )

proof 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 ) ) )

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

( 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
end;

registration
end;

registration

let K be non empty right_complementable doubleLoopStr ;

coherence

opp K is right_complementable

end;
coherence

opp K is right_complementable

proof end;

registration
end;

registration
end;

registration

let K be Skew-Field;

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

Lm5: for F being non empty commutative doubleLoopStr

for x, y being Element of F holds x * y = y * x

;

definition

let K be non empty doubleLoopStr ;

let V be non empty ModuleStr over K;

ex b_{1} 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

b_{1} = RightModStr(# the carrier of V, the addF of V,(0. V),o #)

for b_{1}, b_{2} 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

b_{1} = 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

b_{2} = RightModStr(# the carrier of V, the addF of V,(0. V),o #) ) holds

b_{1} = b_{2}

end;
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 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 #);

ex b

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

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines opp MOD_4:def 2 :

for K being non empty doubleLoopStr

for V being non empty ModuleStr over K

for b_{3} being strict RightModStr over opp K holds

( b_{3} = 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

b_{3} = RightModStr(# the carrier of V, the addF of V,(0. V),o #) );

for K being non empty doubleLoopStr

for V being non empty ModuleStr over K

for b

( b

b

registration

let K be non empty doubleLoopStr ;

let V be non empty ModuleStr over K;

coherence

not opp V is empty

end;
let V be non empty ModuleStr over K;

coherence

not opp V is empty

proof 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) ) ) )

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;

~ o is Function of [: the carrier of (opp V), the carrier of (opp K):], the carrier of (opp V)

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

~ o is Function of [: the carrier of (opp V), the carrier of (opp K):], the carrier of (opp V)

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

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

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;

ex b_{1} 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

b_{1} = ModuleStr(# the carrier of W, the addF of W,(0. W),o #)

for b_{1}, b_{2} 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

b_{1} = 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

b_{2} = ModuleStr(# the carrier of W, the addF of W,(0. W),o #) ) holds

b_{1} = b_{2}

end;
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 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 #);

ex b

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

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines opp MOD_4:def 4 :

for K being non empty doubleLoopStr

for W being non empty RightModStr over K

for b_{3} being strict ModuleStr over opp K holds

( b_{3} = 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

b_{3} = ModuleStr(# the carrier of W, the addF of W,(0. W),o #) );

for K being non empty doubleLoopStr

for W being non empty RightModStr over K

for b

( b

b

registration

let K be non empty doubleLoopStr ;

let W be non empty RightModStr over K;

coherence

not opp W is empty

end;
let W be non empty RightModStr over K;

coherence

not opp W is empty

proof 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) ) ) )

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;

~ o is Function of [: the carrier of (opp K), the carrier of (opp W):], the carrier of (opp W)

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

~ o is Function of [: the carrier of (opp K), the carrier of (opp W):], the carrier of (opp W)

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

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

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;

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

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

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;

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

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

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 #)

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 #)

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;

registration

let K be Ring;

let V be LeftMod of K;

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;
let V be LeftMod of K;

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;

registration

let K be Ring;

let W be RightMod of K;

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

definition

let K, L be non empty multMagma ;

let IT be Function of K,L;

end;
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);

for x, y being Scalar of K holds IT . (x * y) = (IT . y) * (IT . x);

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

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;

end;
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 );

( IT is additive & IT is antimultiplicative & IT is unity-preserving );

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

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

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

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

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

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

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

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

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

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 ;

for b_{1} being Function of K,L st b_{1} is antilinear holds

( b_{1} is additive & b_{1} is antimultiplicative & b_{1} is unity-preserving )
;

for b_{1} being Function of K,L st b_{1} is additive & b_{1} is antimultiplicative & b_{1} is unity-preserving holds

b_{1} is antilinear
;

coherence

for b_{1} being Function of K,L st b_{1} is monomorphism holds

( b_{1} is linear & b_{1} is one-to-one )
;

coherence

for b_{1} being Function of K,L st b_{1} is linear & b_{1} is one-to-one holds

b_{1} is monomorphism
;

coherence

for b_{1} being Function of K,L st b_{1} is antimonomorphism holds

( b_{1} is antilinear & b_{1} is one-to-one )
;

coherence

for b_{1} being Function of K,L st b_{1} is antilinear & b_{1} is one-to-one holds

b_{1} is antimonomorphism
;

coherence

for b_{1} being Function of K,L st b_{1} is epimorphism holds

( b_{1} is linear & b_{1} is onto )
;

coherence

for b_{1} being Function of K,L st b_{1} is linear & b_{1} is onto holds

b_{1} is epimorphism
;

coherence

for b_{1} being Function of K,L st b_{1} is antiepimorphism holds

( b_{1} is antilinear & b_{1} is onto )
;

coherence

for b_{1} being Function of K,L st b_{1} is antilinear & b_{1} is onto holds

b_{1} is antiepimorphism
;

coherence

for b_{1} being Function of K,L st b_{1} is isomorphism holds

( b_{1} is monomorphism & b_{1} is onto )
;

coherence

for b_{1} being Function of K,L st b_{1} is monomorphism & b_{1} is onto holds

b_{1} is isomorphism
;

coherence

for b_{1} being Function of K,L st b_{1} is antiisomorphism holds

( b_{1} is antimonomorphism & b_{1} is onto )
;

coherence

for b_{1} being Function of K,L st b_{1} is antimonomorphism & b_{1} is onto holds

b_{1} is antiisomorphism
;

end;
cluster Function-like quasi_total antilinear -> additive unity-preserving antimultiplicative for Function of ,;

coherence for b

( b

cluster Function-like quasi_total additive unity-preserving antimultiplicative -> antilinear for Function of ,;

coherence for b

b

coherence

for b

( b

coherence

for b

b

coherence

for b

( b

coherence

for b

b

coherence

for b

( b

coherence

for b

b

coherence

for b

( b

coherence

for b

b

coherence

for b

( b

coherence

for b

b

coherence

for b

( b

coherence

for b

b

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

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

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 ;

coherence

for b_{1} being Function of K,K st b_{1} is endomorphism holds

b_{1} is linear
;

coherence

for b_{1} being Function of K,K st b_{1} is linear holds

b_{1} is endomorphism
;

coherence

for b_{1} being Function of K,K st b_{1} is antiendomorphism holds

b_{1} is antilinear
;

coherence

for b_{1} being Function of K,K st b_{1} is antilinear holds

b_{1} is antiendomorphism
;

end;
coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

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 ) )

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 ) )

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

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

definition

let K, L be non empty doubleLoopStr ;

let J be Function of K,L;

coherence

J is Function of K,(opp L) ;

end;
let J be Function of K,L;

coherence

J is Function of K,(opp L) ;

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

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;

::$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 )

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 )

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;

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;

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;

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;

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;

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;

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;

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;

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;

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;

for J being Function of K,K holds

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

registration

let G be AddGroup;

ex b_{1} being Endomorphism of G st b_{1} is bijective

end;
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 Endomorphism of ;

existence ex b

proof 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

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;

ex b_{1} being Function of V,W st

( ( for x, y being Vector of V holds b_{1} . (x + y) = (b_{1} . x) + (b_{1} . y) ) & ( for a being Scalar of K

for x being Vector of V holds b_{1} . (a * x) = (J . a) * (b_{1} . x) ) )

end;
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 ( ( 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) ) );

ex b

( ( for x, y being Vector of V holds b

for x being Vector of V holds b

proof 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 b_{6} being Function of V,W holds

( b_{6} is Homomorphism of J,V,W iff ( ( for x, y being Vector of V holds b_{6} . (x + y) = (b_{6} . x) + (b_{6} . y) ) & ( for a being Scalar of K

for x being Vector of V holds b_{6} . (a * x) = (J . a) * (b_{6} . x) ) ) );

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 b

( b

for x being Vector of V holds b

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

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;
let J be Function of K,K;

let V be LeftMod of K;

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

definition
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) ) ) )

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;