:: MOD_4 semantic presentation

definition
let c1, c2, c3 be non empty set ;
let c4 be Function of [:c1,c2:],c3;
redefine func ~ as ~ c4 -> Function of [:a2,a1:],a3;
coherence
~ c4 is Function of [:c2,c1:],c3 by FUNCT_4:51;
end;

theorem Th1: :: MOD_4:1
for b1, b2, b3 being non empty set
for b4 being Function of [:b2,b3:],b1
for b5 being Element of b2
for b6 being Element of b3 holds b4 . b5,b6 = (~ b4) . b6,b5
proof end;

definition
let c1 be non empty doubleLoopStr ;
func opp c1 -> strict doubleLoopStr equals :: MOD_4:def 1
 doubleLoopStr(# the carrier of a1,the add of a1,(~ the mult of a1),the unity of a1,the Zero of a1 #);
correctness
coherence
doubleLoopStr(# the carrier of c1,the add of c1,(~ the mult of c1),the unity of c1,the Zero of c1 #) is strict doubleLoopStr ;
;
end;

:: deftheorem Def1 defines opp MOD_4:def 1 :
for b1 being non empty doubleLoopStr holds opp b1 = doubleLoopStr(# the carrier of b1,the add of b1,(~ the mult of b1),the unity of b1,the Zero of b1 #);

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

Lemma2: for b1 being non empty doubleLoopStr
for b2, b3 being Scalar of b1
for b4, b5 being Scalar of (opp b1) st b2 = b4 & b3 = b5 holds
( b2 + b3 = b4 + b5 & b2 * b3 = b5 * b4 )
by Th1;

Lemma3: for b1 being non empty unital doubleLoopStr
for b2, b3 being Element of (opp b1) st b3 = 1. b1 holds
( b2 * b3 = b2 & b3 * b2 = b2 )
proof end;

registration
let c1 be non empty unital doubleLoopStr ;
cluster opp a1 -> non empty unital strict ;
coherence
opp c1 is unital
proof end;
end;

Lemma4: for b1 being non empty unital doubleLoopStr holds 1. b1 = 1. (opp b1)
proof end;

E5: now
let c1 be non empty add-associative right_zeroed right_complementable doubleLoopStr ;
set c2 = opp c1;
thus for b1, b2, b3 being Scalar of (opp c1) holds
( (b1 + b2) + b3 = b1 + (b2 + b3) & b1 + (0. (opp c1)) = b1 )
proof
let c3, c4, c5 be Scalar of (opp c1);
reconsider c6 = c3, c7 = c4, c8 = c5 as Scalar of c1 ;
thus (c3 + c4) + c5 = (c6 + c7) + c8
.= c6 + (c7 + c8) by RLVECT_1:def 6
.= c3 + (c4 + c5) ;
thus c3 + (0. (opp c1)) = c6 + (0. c1)
.= c3 by RLVECT_1:def 7 ;
end;
end;

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

Lemma6: for b1 being non empty add-associative right_zeroed right_complementable doubleLoopStr
for b2, b3 being Scalar of b1
for b4, b5 being Scalar of (opp b1) st b2 = b4 & b3 = b5 holds
( b2 + b3 = b4 + b5 & b2 * b3 = b5 * b4 & - b2 = - b4 )
proof end;

theorem Th2: :: MOD_4:2
for b1 being non empty doubleLoopStr holds
( LoopStr(# the carrier of (opp b1),the add of (opp b1),the Zero of (opp b1) #) = LoopStr(# the carrier of b1,the add of b1,the Zero of b1 #) & ( b1 is add-associative & b1 is right_zeroed & b1 is right_complementable implies comp (opp b1) = comp b1 ) & ( for b2 being set holds
( b2 is Scalar of (opp b1) iff b2 is Scalar of b1 ) ) )
proof end;

theorem Th3: :: MOD_4:3
for b1 being non empty doubleLoopStr holds opp (opp b1) = doubleLoopStr(# the carrier of b1,the add of b1,the mult of b1,the unity of b1,the Zero of b1 #) by FUNCT_4:56;

Lemma8: for b1 being non empty add-associative right_zeroed right_complementable doubleLoopStr
for b2, b3, b4, b5 being Scalar of b1
for b6, b7, b8, b9 being Scalar of (opp b1) st b2 = b6 & b3 = b7 & b4 = b8 & b5 = b9 holds
( (b2 + b3) + b4 = (b6 + b7) + b8 & b2 + (b3 + b4) = b6 + (b7 + b8) & (b2 * b3) * b4 = b8 * (b7 * b6) & b2 * (b3 * b4) = (b8 * b7) * b6 & b2 * (b3 + b4) = (b7 + b8) * b6 & (b3 + b4) * b2 = b6 * (b7 + b8) & (b2 * b3) + (b4 * b5) = (b7 * b6) + (b9 * b8) )
proof end;

theorem Th4: :: MOD_4:4
( ( for b1 being non empty unital doubleLoopStr holds 1. b1 = 1. (opp b1) ) & ( for b1 being non empty add-associative right_zeroed right_complementable doubleLoopStr holds
( 0. b1 = 0. (opp b1) & ( for b2, b3, b4, b5 being Scalar of b1
for b6, b7, b8, b9 being Scalar of (opp b1) st b2 = b6 & b3 = b7 & b4 = b8 & b5 = b9 holds
( b2 + b3 = b6 + b7 & b2 * b3 = b7 * b6 & - b2 = - b6 & (b2 + b3) + b4 = (b6 + b7) + b8 & b2 + (b3 + b4) = b6 + (b7 + b8) & (b2 * b3) * b4 = b8 * (b7 * b6) & b2 * (b3 * b4) = (b8 * b7) * b6 & b2 * (b3 + b4) = (b7 + b8) * b6 & (b3 + b4) * b2 = b6 * (b7 + b8) & (b2 * b3) + (b4 * b5) = (b7 * b6) + (b9 * b8) ) ) ) ) ) by Lemma6, Lemma8, Lemma4;

theorem Th5: :: MOD_4:5
for b1 being Ring holds opp b1 is strict Ring
proof end;

registration
let c1 be Ring;
cluster opp a1 -> non empty Abelian add-associative right_zeroed right_complementable unital strict distributive ;
coherence
( opp c1 is Abelian & opp c1 is add-associative & opp c1 is right_zeroed & opp c1 is right_complementable & opp c1 is unital & opp c1 is distributive ) by Th5;
end;

theorem Th6: :: MOD_4:6
for b1 being Ring holds opp b1 is Ring
proof end;

registration
let c1 be Ring;
cluster opp a1 -> non empty Abelian add-associative right_zeroed right_complementable unital associative strict distributive ;
coherence
opp c1 is associative by Th6;
end;

theorem Th7: :: MOD_4:7
for b1 being Skew-Field holds opp b1 is Skew-Field
proof end;

registration
let c1 be Skew-Field;
cluster opp a1 -> non empty Abelian add-associative right_zeroed right_complementable unital associative strict distributive Field-like non degenerated ;
coherence
( not opp c1 is degenerated & opp c1 is Field-like & opp c1 is associative & opp c1 is Abelian & opp c1 is add-associative & opp c1 is right_zeroed & opp c1 is right_complementable & opp c1 is unital & opp c1 is distributive ) by Th7;
end;

Lemma12: for b1 being non empty commutative doubleLoopStr
for b2, b3 being Element of b1 holds b2 * b3 = b3 * b2
;

theorem Th8: :: MOD_4:8
for b1 being Field holds opp b1 is strict Field
proof end;

registration
let c1 be Field;
cluster opp a1 -> non empty Abelian add-associative right_zeroed right_complementable unital associative strict distributive Field-like non degenerated ;
coherence
( opp c1 is strict & opp c1 is Field-like ) ;
end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be non empty VectSpStr of c1;
func opp c2 -> strict RightModStr of opp a1 means :Def2: :: MOD_4:def 2
for b1 being Function of [:the carrier of a2,the carrier of (opp a1):],the carrier of a2 st b1 = ~ the lmult of a2 holds
a3 = RightModStr(# the carrier of a2,the add of a2,the Zero of a2,b1 #);
existence
ex b1 being strict RightModStr of opp c1 st
for b2 being Function of [:the carrier of c2,the carrier of (opp c1):],the carrier of c2 st b2 = ~ the lmult of c2 holds
b1 = RightModStr(# the carrier of c2,the add of c2,the Zero of c2,b2 #)
proof end;
uniqueness
for b1, b2 being strict RightModStr of opp c1 st ( for b3 being Function of [:the carrier of c2,the carrier of (opp c1):],the carrier of c2 st b3 = ~ the lmult of c2 holds
b1 = RightModStr(# the carrier of c2,the add of c2,the Zero of c2,b3 #) ) & ( for b3 being Function of [:the carrier of c2,the carrier of (opp c1):],the carrier of c2 st b3 = ~ the lmult of c2 holds
b2 = RightModStr(# the carrier of c2,the add of c2,the Zero of c2,b3 #) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines opp MOD_4:def 2 :
for b1 being non empty doubleLoopStr
for b2 being non empty VectSpStr of b1
for b3 being strict RightModStr of opp b1 holds
( b3 = opp b2 iff for b4 being Function of [:the carrier of b2,the carrier of (opp b1):],the carrier of b2 st b4 = ~ the lmult of b2 holds
b3 = RightModStr(# the carrier of b2,the add of b2,the Zero of b2,b4 #) );

registration
let c1 be non empty doubleLoopStr ;
let c2 be non empty VectSpStr of c1;
cluster opp a2 -> non empty strict ;
coherence
not opp c2 is empty
proof end;
end;

theorem Th9: :: MOD_4:9
for b1 being non empty doubleLoopStr
for b2 being non empty VectSpStr of b1 holds
( LoopStr(# the carrier of (opp b2),the add of (opp b2),the Zero of (opp b2) #) = LoopStr(# the carrier of b2,the add of b2,the Zero of b2 #) & ( for b3 being set holds
( b3 is Vector of b2 iff b3 is Vector of (opp b2) ) ) )
proof end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be non empty VectSpStr of c1;
let c3 be Function of [:the carrier of c1,the carrier of c2:],the carrier of c2;
func opp c3 -> Function of [:the carrier of (opp a2),the carrier of (opp a1):],the carrier of (opp a2) equals :: MOD_4:def 3
 ~ a3;
coherence
~ c3 is Function of [:the carrier of (opp c2),the carrier of (opp c1):],the carrier of (opp c2)
proof end;
end;

:: deftheorem Def3 defines opp MOD_4:def 3 :
for b1 being non empty doubleLoopStr
for b2 being non empty VectSpStr of b1
for b3 being Function of [:the carrier of b1,the carrier of b2:],the carrier of b2 holds opp b3 = ~ b3;

theorem Th10: :: MOD_4:10
for b1 being non empty doubleLoopStr
for b2 being non empty VectSpStr of b1 holds the rmult of (opp b2) = opp the lmult of b2
proof end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be non empty RightModStr of c1;
func opp c2 -> strict VectSpStr of opp a1 means :Def4: :: MOD_4:def 4
for b1 being Function of [:the carrier of (opp a1),the carrier of a2:],the carrier of a2 st b1 = ~ the rmult of a2 holds
a3 = VectSpStr(# the carrier of a2,the add of a2,the Zero of a2,b1 #);
existence
ex b1 being strict VectSpStr of opp c1 st
for b2 being Function of [:the carrier of (opp c1),the carrier of c2:],the carrier of c2 st b2 = ~ the rmult of c2 holds
b1 = VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,b2 #)
proof end;
uniqueness
for b1, b2 being strict VectSpStr of opp c1 st ( for b3 being Function of [:the carrier of (opp c1),the carrier of c2:],the carrier of c2 st b3 = ~ the rmult of c2 holds
b1 = VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,b3 #) ) & ( for b3 being Function of [:the carrier of (opp c1),the carrier of c2:],the carrier of c2 st b3 = ~ the rmult of c2 holds
b2 = VectSpStr(# the carrier of c2,the add of c2,the Zero of c2,b3 #) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines opp MOD_4:def 4 :
for b1 being non empty doubleLoopStr
for b2 being non empty RightModStr of b1
for b3 being strict VectSpStr of opp b1 holds
( b3 = opp b2 iff for b4 being Function of [:the carrier of (opp b1),the carrier of b2:],the carrier of b2 st b4 = ~ the rmult of b2 holds
b3 = VectSpStr(# the carrier of b2,the add of b2,the Zero of b2,b4 #) );

registration
let c1 be non empty doubleLoopStr ;
let c2 be non empty RightModStr of c1;
cluster opp a2 -> non empty strict ;
coherence
not opp c2 is empty
proof end;
end;

theorem Th11: :: MOD_4:11
canceled;

theorem Th12: :: MOD_4:12
for b1 being non empty doubleLoopStr
for b2 being non empty RightModStr of b1 holds
( LoopStr(# the carrier of (opp b2),the add of (opp b2),the Zero of (opp b2) #) = LoopStr(# the carrier of b2,the add of b2,the Zero of b2 #) & ( for b3 being set holds
( b3 is Vector of b2 iff b3 is Vector of (opp b2) ) ) )
proof end;

definition
let c1 be non empty doubleLoopStr ;
let c2 be non empty RightModStr of c1;
let c3 be Function of [:the carrier of c2,the carrier of c1:],the carrier of c2;
func opp c3 -> Function of [:the carrier of (opp a1),the carrier of (opp a2):],the carrier of (opp a2) equals :: MOD_4:def 5
 ~ a3;
coherence
~ c3 is Function of [:the carrier of (opp c1),the carrier of (opp c2):],the carrier of (opp c2)
proof end;
end;

:: deftheorem Def5 defines opp MOD_4:def 5 :
for b1 being non empty doubleLoopStr
for b2 being non empty RightModStr of b1
for b3 being Function of [:the carrier of b2,the carrier of b1:],the carrier of b2 holds opp b3 = ~ b3;

theorem Th13: :: MOD_4:13
for b1 being non empty doubleLoopStr
for b2 being non empty RightModStr of b1 holds the lmult of (opp b2) = opp the rmult of b2
proof end;

theorem Th14: :: MOD_4:14
canceled;

theorem Th15: :: MOD_4:15
for b1 being non empty doubleLoopStr
for b2 being non empty VectSpStr of b1
for b3 being Function of [:the carrier of b1,the carrier of b2:],the carrier of b2 holds opp (opp b3) = b3 by FUNCT_4:56;

theorem Th16: :: MOD_4:16
for b1 being non empty doubleLoopStr
for b2 being non empty VectSpStr of b1
for b3 being Function of [:the carrier of b1,the carrier of b2:],the carrier of b2
for b4 being Scalar of b1
for b5 being Scalar of (opp b1)
for b6 being Vector of b2
for b7 being Vector of (opp b2) st b4 = b5 & b6 = b7 holds
(opp b3) . b7,b5 = b3 . b4,b6 by Th1;

theorem Th17: :: MOD_4:17
for b1, b2 being Ring
for b3 being non empty VectSpStr of b1
for b4 being non empty RightModStr of b2
for b5 being Scalar of b1
for b6 being Scalar of b2
for b7 being Vector of b3
for b8 being Vector of b4 st b2 = opp b1 & b4 = opp b3 & b5 = b6 & b7 = b8 holds
b8 * b6 = b5 * b7
proof end;

theorem Th18: :: MOD_4:18
for b1, b2 being Ring
for b3 being non empty VectSpStr of b1
for b4 being non empty RightModStr of b2
for b5, b6 being Vector of b3
for b7, b8 being Vector of b4 st b2 = opp b1 & b4 = opp b3 & b5 = b7 & b6 = b8 holds
b7 + b8 = b5 + b6
proof end;

theorem Th19: :: MOD_4:19
for b1 being non empty doubleLoopStr
for b2 being non empty RightModStr of b1
for b3 being Function of [:the carrier of b2,the carrier of b1:],the carrier of b2 holds opp (opp b3) = b3 by FUNCT_4:56;

theorem Th20: :: MOD_4:20
for b1 being non empty doubleLoopStr
for b2 being non empty RightModStr of b1
for b3 being Function of [:the carrier of b2,the carrier of b1:],the carrier of b2
for b4 being Scalar of b1
for b5 being Scalar of (opp b1)
for b6 being Vector of b2
for b7 being Vector of (opp b2) st b4 = b5 & b6 = b7 holds
(opp b3) . b5,b7 = b3 . b6,b4 by Th1;

theorem Th21: :: MOD_4:21
for b1, b2 being Ring
for b3 being non empty VectSpStr of b1
for b4 being non empty RightModStr of b2
for b5 being Scalar of b1
for b6 being Scalar of b2
for b7 being Vector of b3
for b8 being Vector of b4 st b1 = opp b2 & b3 = opp b4 & b5 = b6 & b7 = b8 holds
b8 * b6 = b5 * b7
proof end;

theorem Th22: :: MOD_4:22
for b1, b2 being Ring
for b3 being non empty VectSpStr of b1
for b4 being non empty RightModStr of b2
for b5, b6 being Vector of b3
for b7, b8 being Vector of b4 st b1 = opp b2 & b3 = opp b4 & b5 = b7 & b6 = b8 holds
b7 + b8 = b5 + b6
proof end;

theorem Th23: :: MOD_4:23
for b1 being non empty strict doubleLoopStr
for b2 being non empty VectSpStr of b1 holds opp (opp b2) = VectSpStr(# the carrier of b2,the add of b2,the Zero of b2,the lmult of b2 #)
proof end;

theorem Th24: :: MOD_4:24
for b1 being non empty strict doubleLoopStr
for b2 being non empty RightModStr of b1 holds opp (opp b2) = RightModStr(# the carrier of b2,the add of b2,the Zero of b2,the rmult of b2 #)
proof end;

theorem Th25: :: MOD_4:25
for b1 being Ring
for b2 being LeftMod of b1 holds opp b2 is strict RightMod of opp b1
proof end;

registration
let c1 be Ring;
let c2 be LeftMod of c1;
cluster opp a2 -> non empty Abelian add-associative right_zeroed right_complementable strict RightMod-like ;
coherence
( opp c2 is Abelian & opp c2 is add-associative & opp c2 is right_zeroed & opp c2 is right_complementable & opp c2 is RightMod-like ) by Th25;
end;

theorem Th26: :: MOD_4:26
for b1 being Ring
for b2 being RightMod of b1 holds opp b2 is strict LeftMod of opp b1
proof end;

registration
let c1 be Ring;
let c2 be RightMod of c1;
cluster opp a2 -> non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like ;
coherence
( opp c2 is Abelian & opp c2 is add-associative & opp c2 is right_zeroed & opp c2 is right_complementable & opp c2 is VectSp-like ) by Th26;
end;

definition
let c1, c2 be non empty doubleLoopStr ;
let c3 be Function of c1,c2;
attr a3 is antilinear means :Def6: :: MOD_4:def 6
( ( for b1, b2 being Scalar of a1 holds a3 . (b1 + b2) = (a3 . b1) + (a3 . b2) ) & ( for b1, b2 being Scalar of a1 holds a3 . (b1 * b2) = (a3 . b2) * (a3 . b1) ) & a3 . (1. a1) = 1. a2 );
end;

:: deftheorem Def6 defines antilinear MOD_4:def 6 :
for b1, b2 being non empty doubleLoopStr
for b3 being Function of b1,b2 holds
( b3 is antilinear iff ( ( for b4, b5 being Scalar of b1 holds b3 . (b4 + b5) = (b3 . b4) + (b3 . b5) ) & ( for b4, b5 being Scalar of b1 holds b3 . (b4 * b5) = (b3 . b5) * (b3 . b4) ) & b3 . (1. b1) = 1. b2 ) );

definition
let c1, c2 be non empty doubleLoopStr ;
let c3 be Function of c1,c2;
attr a3 is monomorphism means :Def7: :: MOD_4:def 7
( a3 is linear & a3 is one-to-one );
attr a3 is antimonomorphism means :Def8: :: MOD_4:def 8
( a3 is antilinear & a3 is one-to-one );
end;

:: deftheorem Def7 defines monomorphism MOD_4:def 7 :
for b1, b2 being non empty doubleLoopStr
for b3 being Function of b1,b2 holds
( b3 is monomorphism iff ( b3 is linear & b3 is one-to-one ) );

:: deftheorem Def8 defines antimonomorphism MOD_4:def 8 :
for b1, b2 being non empty doubleLoopStr
for b3 being Function of b1,b2 holds
( b3 is antimonomorphism iff ( b3 is antilinear & b3 is one-to-one ) );

definition
let c1, c2 be non empty doubleLoopStr ;
let c3 be Function of c1,c2;
attr a3 is epimorphism means :Def9: :: MOD_4:def 9
( a3 is linear & rng a3 = the carrier of a2 );
attr a3 is antiepimorphism means :Def10: :: MOD_4:def 10
( a3 is antilinear & rng a3 = the carrier of a2 );
end;

:: deftheorem Def9 defines epimorphism MOD_4:def 9 :
for b1, b2 being non empty doubleLoopStr
for b3 being Function of b1,b2 holds
( b3 is epimorphism iff ( b3 is linear & rng b3 = the carrier of b2 ) );

:: deftheorem Def10 defines antiepimorphism MOD_4:def 10 :
for b1, b2 being non empty doubleLoopStr
for b3 being Function of b1,b2 holds
( b3 is antiepimorphism iff ( b3 is antilinear & rng b3 = the carrier of b2 ) );

definition
let c1, c2 be non empty doubleLoopStr ;
let c3 be Function of c1,c2;
attr a3 is isomorphism means :Def11: :: MOD_4:def 11
( a3 is monomorphism & rng a3 = the carrier of a2 );
attr a3 is antiisomorphism means :Def12: :: MOD_4:def 12
( a3 is antimonomorphism & rng a3 = the carrier of a2 );
end;

:: deftheorem Def11 defines isomorphism MOD_4:def 11 :
for b1, b2 being non empty doubleLoopStr
for b3 being Function of b1,b2 holds
( b3 is isomorphism iff ( b3 is monomorphism & rng b3 = the carrier of b2 ) );

:: deftheorem Def12 defines antiisomorphism MOD_4:def 12 :
for b1, b2 being non empty doubleLoopStr
for b3 being Function of b1,b2 holds
( b3 is antiisomorphism iff ( b3 is antimonomorphism & rng b3 = the carrier of b2 ) );

definition
let c1 be non empty doubleLoopStr ;
let c2 be Function of c1,c1;
attr a2 is endomorphism means :Def13: :: MOD_4:def 13
a2 is linear;
attr a2 is antiendomorphism means :Def14: :: MOD_4:def 14
a2 is antilinear;
attr a2 is automorphism means :Def15: :: MOD_4:def 15
a2 is isomorphism;
attr a2 is antiautomorphism means :Def16: :: MOD_4:def 16
a2 is antiisomorphism;
end;

:: deftheorem Def13 defines endomorphism MOD_4:def 13 :
for b1 being non empty doubleLoopStr
for b2 being Function of b1,b1 holds
( b2 is endomorphism iff b2 is linear );

:: deftheorem Def14 defines antiendomorphism MOD_4:def 14 :
for b1 being non empty doubleLoopStr
for b2 being Function of b1,b1 holds
( b2 is antiendomorphism iff b2 is antilinear );

:: deftheorem Def15 defines automorphism MOD_4:def 15 :
for b1 being non empty doubleLoopStr
for b2 being Function of b1,b1 holds
( b2 is automorphism iff b2 is isomorphism );

:: deftheorem Def16 defines antiautomorphism MOD_4:def 16 :
for b1 being non empty doubleLoopStr
for b2 being Function of b1,b1 holds
( b2 is antiautomorphism iff b2 is antiisomorphism );

theorem Th27: :: MOD_4:27
for b1 being non empty doubleLoopStr
for b2 being Function of b1,b1 holds
( b2 is automorphism iff ( ( for b3, b4 being Scalar of b1 holds b2 . (b3 + b4) = (b2 . b3) + (b2 . b4) ) & ( for b3, b4 being Scalar of b1 holds b2 . (b3 * b4) = (b2 . b3) * (b2 . b4) ) & b2 . (1. b1) = 1. b1 & b2 is one-to-one & rng b2 = the carrier of b1 ) )
proof end;

theorem Th28: :: MOD_4:28
for b1 being non empty doubleLoopStr
for b2 being Function of b1,b1 holds
( b2 is antiautomorphism iff ( ( for b3, b4 being Scalar of b1 holds b2 . (b3 + b4) = (b2 . b3) + (b2 . b4) ) & ( for b3, b4 being Scalar of b1 holds b2 . (b3 * b4) = (b2 . b4) * (b2 . b3) ) & b2 . (1. b1) = 1. b1 & b2 is one-to-one & rng b2 = the carrier of b1 ) )
proof end;

Lemma41: for b1 being non empty doubleLoopStr holds
( ( for b2, b3 being Scalar of b1 holds (id b1) . (b2 + b3) = ((id b1) . b2) + ((id b1) . b3) ) & ( for b2, b3 being Scalar of b1 holds (id b1) . (b2 * b3) = ((id b1) . b2) * ((id b1) . b3) ) & (id b1) . (1. b1) = 1. b1 & id b1 is one-to-one & rng (id b1) = the carrier of b1 )
proof end;

theorem Th29: :: MOD_4:29
for b1 being non empty doubleLoopStr holds id b1 is automorphism
proof end;

Lemma42: for b1, b2 being Ring
for b3 being Function of b1,b2 st b3 is linear holds
b3 . (0. b1) = 0. b2
proof end;

Lemma43: for b1, b2 being Ring
for b3 being Function of b2,b1
for b4 being Scalar of b2 st b3 is linear holds
b3 . (- b4) = - (b3 . b4)
proof end;

Lemma44: for b1, b2 being Ring
for b3 being Function of b2,b1
for b4, b5 being Scalar of b2 st b3 is linear holds
b3 . (b4 - b5) = (b3 . b4) - (b3 . b5)
proof end;

theorem Th30: :: MOD_4:30
for b1, b2 being Ring
for b3 being Function of b1,b2
for b4, b5 being Scalar of b1 st b3 is linear holds
( b3 . (0. b1) = 0. b2 & b3 . (- b4) = - (b3 . b4) & b3 . (b4 - b5) = (b3 . b4) - (b3 . b5) ) by Lemma42, Lemma43, Lemma44;

Lemma45: for b1, b2 being Ring
for b3 being Function of b1,b2 st b3 is antilinear holds
b3 . (0. b1) = 0. b2
proof end;

Lemma46: for b1, b2 being Ring
for b3 being Function of b2,b1
for b4 being Scalar of b2 st b3 is antilinear holds
b3 . (- b4) = - (b3 . b4)
proof end;

Lemma47: for b1, b2 being Ring
for b3 being Function of b2,b1
for b4, b5 being Scalar of b2 st b3 is antilinear holds
b3 . (b4 - b5) = (b3 . b4) - (b3 . b5)
proof end;

theorem Th31: :: MOD_4:31
for b1, b2 being Ring
for b3 being Function of b1,b2
for b4, b5 being Scalar of b1 st b3 is antilinear holds
( b3 . (0. b1) = 0. b2 & b3 . (- b4) = - (b3 . b4) & b3 . (b4 - b5) = (b3 . b4) - (b3 . b5) ) by Lemma45, Lemma46, Lemma47;

theorem Th32: :: MOD_4:32
for b1 being Ring holds
( id b1 is antiautomorphism iff b1 is comRing )
proof end;

theorem Th33: :: MOD_4:33
for b1 being Skew-Field holds
( id b1 is antiautomorphism iff b1 is Field )
proof end;

definition
let c1, c2 be non empty doubleLoopStr ;
let c3 be Function of c1,c2;
func opp c3 -> Function of a1,(opp a2) equals :: MOD_4:def 17
a3;
coherence
c3 is Function of c1,(opp c2) ;
end;

:: deftheorem Def17 defines opp MOD_4:def 17 :
for b1, b2 being non empty doubleLoopStr
for b3 being Function of b1,b2 holds opp b3 = b3;

theorem Th34: :: MOD_4:34
for b1, b2 being non empty add-associative right_zeroed right_complementable doubleLoopStr
for b3 being Function of b1,b2 holds opp (opp b3) = b3 ;

theorem Th35: :: MOD_4:35
for b1 being non empty add-associative right_zeroed right_complementable doubleLoopStr
for b2 being non empty add-associative right_zeroed right_complementable unital doubleLoopStr
for b3 being Function of b1,b2 holds
( b3 is linear iff opp b3 is antilinear )
proof end;

theorem Th36: :: MOD_4:36
for b1 being non empty add-associative right_zeroed right_complementable doubleLoopStr
for b2 being non empty add-associative right_zeroed right_complementable unital doubleLoopStr
for b3 being Function of b1,b2 holds
( b3 is antilinear iff opp b3 is linear )
proof end;

theorem Th37: :: MOD_4:37
for b1 being non empty add-associative right_zeroed right_complementable doubleLoopStr
for b2 being non empty add-associative right_zeroed right_complementable unital doubleLoopStr
for b3 being Function of b1,b2 holds
( b3 is monomorphism iff opp b3 is antimonomorphism )
proof end;

theorem Th38: :: MOD_4:38
for b1 being non empty add-associative right_zeroed right_complementable doubleLoopStr
for b2 being non empty add-associative right_zeroed right_complementable unital doubleLoopStr
for b3 being Function of b1,b2 holds
( b3 is antimonomorphism iff opp b3 is monomorphism )
proof end;

theorem Th39: :: MOD_4:39
for b1 being non empty add-associative right_zeroed right_complementable doubleLoopStr
for b2 being non empty add-associative right_zeroed right_complementable unital doubleLoopStr
for b3 being Function of b1,b2 holds
( b3 is epimorphism iff opp b3 is antiepimorphism )
proof end;

theorem Th40: :: MOD_4:40
for b1 being non empty add-associative right_zeroed right_complementable doubleLoopStr
for b2 being non empty add-associative right_zeroed right_complementable unital doubleLoopStr
for b3 being Function of b1,b2 holds
( b3 is antiepimorphism iff opp b3 is epimorphism )
proof end;

theorem Th41: :: MOD_4:41
for b1 being non empty add-associative right_zeroed right_complementable doubleLoopStr
for b2 being non empty add-associative right_zeroed right_complementable unital doubleLoopStr
for b3 being Function of b1,b2 holds
( b3 is isomorphism iff opp b3 is antiisomorphism )
proof end;

theorem Th42: :: MOD_4:42
for b1 being non empty add-associative right_zeroed right_complementable doubleLoopStr
for b2 being non empty add-associative right_zeroed right_complementable unital doubleLoopStr
for b3 being Function of b1,b2 holds
( b3 is antiisomorphism iff opp b3 is isomorphism )
proof end;

theorem Th43: :: MOD_4:43
for b1 being non empty add-associative right_zeroed right_complementable unital doubleLoopStr
for b2 being Function of b1,b1 holds
( b2 is endomorphism iff opp b2 is antilinear )
proof end;

theorem Th44: :: MOD_4:44
for b1 being non empty add-associative right_zeroed right_complementable unital doubleLoopStr
for b2 being Function of b1,b1 holds
( b2 is antiendomorphism iff opp b2 is linear )
proof end;

theorem Th45: :: MOD_4:45
for b1 being non empty add-associative right_zeroed right_complementable unital doubleLoopStr
for b2 being Function of b1,b1 holds
( b2 is automorphism iff opp b2 is antiisomorphism )
proof end;

theorem Th46: :: MOD_4:46
for b1 being non empty add-associative right_zeroed right_complementable unital doubleLoopStr
for b2 being Function of b1,b1 holds
( b2 is antiautomorphism iff opp b2 is isomorphism )
proof end;

Lemma54: for b1, b2 being AddGroup
for b3, b4 being Element of b1 holds (ZeroMap b1,b2) . (b3 + b4) = ((ZeroMap b1,b2) . b3) + ((ZeroMap b1,b2) . b4)
proof end;

definition
let c1, c2 be AddGroup;
mode Homomorphism of c1,c2 -> Function of a1,a2 means :Def18: :: MOD_4:def 18
for b1, b2 being Element of a1 holds a3 . (b1 + b2) = (a3 . b1) + (a3 . b2);
existence
ex b1 being Function of c1,c2 st
for b2, b3 being Element of c1 holds b1 . (b2 + b3) = (b1 . b2) + (b1 . b3)
proof end;
end;

:: deftheorem Def18 defines Homomorphism MOD_4:def 18 :
for b1, b2 being AddGroup
for b3 being Function of b1,b2 holds
( b3 is Homomorphism of b1,b2 iff for b4, b5 being Element of b1 holds b3 . (b4 + b5) = (b3 . b4) + (b3 . b5) );

definition
let c1, c2 be AddGroup;
redefine func ZeroMap as ZeroMap c1,c2 -> Homomorphism of a1,a2;
coherence
ZeroMap c1,c2 is Homomorphism of c1,c2
proof end;
end;

definition
let c1, c2 be AddGroup;
let c3 be Homomorphism of c1,c2;
attr a3 is monomorphism means :: MOD_4:def 19
a3 is one-to-one;
end;

:: deftheorem Def19 defines monomorphism MOD_4:def 19 :
for b1, b2 being AddGroup
for b3 being Homomorphism of b1,b2 holds
( b3 is monomorphism iff b3 is one-to-one );

definition
let c1, c2 be AddGroup;
let c3 be Homomorphism of c1,c2;
attr a3 is epimorphism means :: MOD_4:def 20
 rng a3 = the carrier of a2;
end;

:: deftheorem Def20 defines epimorphism MOD_4:def 20 :
for b1, b2 being AddGroup
for b3 being Homomorphism of b1,b2 holds
( b3 is epimorphism iff rng b3 = the carrier of b2 );

definition
let c1, c2 be AddGroup;
let c3 be Homomorphism of c1,c2;
attr a3 is isomorphism means :Def21: :: MOD_4:def 21
( a3 is one-to-one & rng a3 = the carrier of a2 );
end;

:: deftheorem Def21 defines isomorphism MOD_4:def 21 :
for b1, b2 being AddGroup
for b3 being Homomorphism of b1,b2 holds
( b3 is isomorphism iff ( b3 is one-to-one & rng b3 = the carrier of b2 ) );

definition
let c1 be AddGroup;
mode Endomorphism of a1 is Homomorphism of a1,a1;
end;

Lemma57: for b1 being AddGroup
for b2 being Element of b1 holds (id b1) . b2 = b2
proof end;

Lemma58: for b1 being AddGroup holds
( ( for b2, b3 being Element of b1 holds (id b1) . (b2 + b3) = ((id b1) . b2) + ((id b1) . b3) ) & id b1 is one-to-one & rng (id b1) = the carrier of b1 )
proof end;

registration
let c1 be AddGroup;
cluster isomorphism Homomorphism of a1,a1;
existence
ex b1 being Endomorphism of c1 st b1 is isomorphism
proof end;
end;

definition
let c1 be AddGroup;
mode Automorphism of a1 is isomorphism Endomorphism of a1;
end;

definition
let c1 be AddGroup;
redefine func id as id c1 -> Automorphism of a1;
coherence
id c1 is Automorphism of c1
proof end;
end;

Lemma59: for b1, b2 being AddGroup
for b3 being Homomorphism of b1,b2 holds b3 . (0. b1) = 0. b2
proof end;

Lemma60: for b1, b2 being AddGroup
for b3 being Homomorphism of b2,b1
for b4 being Element of b2 holds b3 . (- b4) = - (b3 . b4)
proof end;

Lemma61: for b1, b2 being AddGroup
for b3 being Homomorphism of b2,b1
for b4, b5 being Element of b2 holds b3 . (b4 - b5) = (b3 . b4) - (b3 . b5)
proof end;

theorem Th47: :: MOD_4:47
canceled;

theorem Th48: :: MOD_4:48
for b1, b2 being AddGroup
for b3 being Homomorphism of b1,b2
for b4, b5 being Element of b1 holds
( b3 . (0. b1) = 0. b2 & b3 . (- b4) = - (b3 . b4) & b3 . (b4 - b5) = (b3 . b4) - (b3 . b5) ) by Lemma59, Lemma60, Lemma61;

theorem Th49: :: MOD_4:49
for b1, b2 being AbGroup
for b3 being Homomorphism of b2,b1
for b4, b5 being Element of b2 holds b3 . (b4 - b5) = (b3 . b4) - (b3 . b5)
proof end;

Lemma62: for b1, b2 being Ring
for b3 being LeftMod of b1
for b4 being LeftMod of b2
for b5, b6 being Vector of b3 holds (ZeroMap b3,b4) . (b5 + b6) = ((ZeroMap b3,b4) . b5) + ((ZeroMap b3,b4) . b6)
proof end;

Lemma63: for b1, b2 being Ring
for b3 being Function of b2,b1
for b4 being LeftMod of b2
for b5 being LeftMod of b1
for b6 being Scalar of b2
for b7 being Vector of b4 holds (ZeroMap b4,b5) . (b6 * b7) = (b3 . b6) * ((ZeroMap b4,b5) . b7)
proof end;

definition
let c1, c2 be Ring;
let c3 be Function of c1,c2;
let c4 be LeftMod of c1;
let c5 be LeftMod of c2;
canceled;
mode Homomorphism of c3,c4,c5 -> Function of a4,a5 means :Def23: :: MOD_4:def 23
( ( for b1, b2 being Vector of a4 holds a6 . (b1 + b2) = (a6 . b1) + (a6 . b2) ) & ( for b1 being Scalar of a1
for b2 being Vector of a4 holds a6 . (b1 * b2) = (a3 . b1) * (a6 . b2) ) );
existence
ex b1 being Function of c4,c5 st
( ( for b2, b3 being Vector of c4 holds b1 . (b2 + b3) = (b1 . b2) + (b1 . b3) ) & ( for b2 being Scalar of c1
for b3 being Vector of c4 holds b1 . (b2 * b3) = (c3 . b2) * (b1 . b3) ) )
proof end;
end;

:: deftheorem Def22 MOD_4:def 22 :
canceled;

:: deftheorem Def23 defines Homomorphism MOD_4:def 23 :
for b1, b2 being Ring
for b3 being Function of b1,b2
for b4 being LeftMod of b1
for b5 being LeftMod of b2
for b6 being Function of b4,b5 holds
( b6 is Homomorphism of b3,b4,b5 iff ( ( for b7, b8 being Vector of b4 holds b6 . (b7 + b8) = (b6 . b7) + (b6 . b8) ) & ( for b7 being Scalar of b1
for b8 being Vector of b4 holds b6 . (b7 * b8) = (b3 . b7) * (b6 . b8) ) ) );

theorem Th50: :: MOD_4:50
for b1, b2 being Ring
for b3 being Function of b1,b2
for b4 being LeftMod of b1
for b5 being LeftMod of b2 holds ZeroMap b4,b5 is Homomorphism of b3,b4,b5
proof end;

definition
let c1, c2 be Ring;
let c3 be Function of c1,c2;
let c4 be LeftMod of c1;
let c5 be LeftMod of c2;
let c6 be Homomorphism of c3,c4,c5;
pred c6 is_monomorphism_wrp c3 means :: MOD_4:def 24
a6 is one-to-one;
pred c6 is_epimorphism_wrp c3 means :: MOD_4:def 25
 rng a6 = the carrier of a5;
pred c6 is_isomorphism_wrp c3 means :: MOD_4:def 26
( a6 is one-to-one & rng a6 = the carrier of a5 );
end;

:: deftheorem Def24 defines is_monomorphism_wrp MOD_4:def 24 :
for b1, b2 being Ring
for b3 being Function of b1,b2
for b4 being LeftMod of b1
for b5 being LeftMod of b2
for b6 being Homomorphism of b3,b4,b5 holds
( b6 is_monomorphism_wrp b3 iff b6 is one-to-one );

:: deftheorem Def25 defines is_epimorphism_wrp MOD_4:def 25 :
for b1, b2 being Ring
for b3 being Function of b1,b2
for b4 being LeftMod of b1
for b5 being LeftMod of b2
for b6 being Homomorphism of b3,b4,b5 holds
( b6 is_epimorphism_wrp b3 iff rng b6 = the carrier of b5 );

:: deftheorem Def26 defines is_isomorphism_wrp MOD_4:def 26 :
for b1, b2 being Ring
for b3 being Function of b1,b2
for b4 being LeftMod of b1
for b5 being LeftMod of b2
for b6 being Homomorphism of b3,b4,b5 holds
( b6 is_isomorphism_wrp b3 iff ( b6 is one-to-one & rng b6 = the carrier of b5 ) );

definition
let c1 be Ring;
let c2 be Function of c1,c1;
let c3 be LeftMod of c1;
mode Endomorphism of a2,a3 is Homomorphism of a2,a3,a3;
end;

definition
let c1 be Ring;
let c2 be Function of c1,c1;
let c3 be LeftMod of c1;
let c4 be Homomorphism of c2,c3,c3;
pred c4 is_automorphism_wrp c2 means :: MOD_4:def 27
( a4 is one-to-one & rng a4 = the carrier of a3 );
end;

:: deftheorem Def27 defines is_automorphism_wrp MOD_4:def 27 :
for b1 being Ring
for b2 being Function of b1,b1
for b3 being LeftMod of b1
for b4 being Homomorphism of b2,b3,b3 holds
( b4 is_automorphism_wrp b2 iff ( b4 is one-to-one & rng b4 = the carrier of b3 ) );

definition
let c1 be Ring;
let c2, c3 be LeftMod of c1;
mode Homomorphism of a2,a3 is Homomorphism of id a1,a2,a3;
end;

theorem Th51: :: MOD_4:51
for b1 being Ring
for b2, b3 being LeftMod of b1
for b4 being Function of b2,b3 holds
( b4 is Homomorphism of b2,b3 iff ( ( for b5, b6 being Vector of b2 holds b4 . (b5 + b6) = (b4 . b5) + (b4 . b6) ) & ( for b5 being Scalar of b1
for b6 being Vector of b2 holds b4 . (b5 * b6) = b5 * (b4 . b6) ) ) )
proof end;

definition
let c1 be Ring;
let c2, c3 be LeftMod of c1;
let c4 be Homomorphism of c2,c3;
attr a4 is monomorphism means :: MOD_4:def 28
a4 is one-to-one;
attr a4 is epimorphism means :: MOD_4:def 29
 rng a4 = the carrier of a3;
attr a4 is isomorphism means :: MOD_4:def 30
( a4 is one-to-one & rng a4 = the carrier of a3 );
end;

:: deftheorem Def28 defines monomorphism MOD_4:def 28 :
for b1 being Ring
for b2, b3 being LeftMod of b1
for b4 being Homomorphism of b2,b3 holds
( b4 is monomorphism iff b4 is one-to-one );

:: deftheorem Def29 defines epimorphism MOD_4:def 29 :
for b1 being Ring
for b2, b3 being LeftMod of b1
for b4 being Homomorphism of b2,b3 holds
( b4 is epimorphism iff rng b4 = the carrier of b3 );

:: deftheorem Def30 defines isomorphism MOD_4:def 30 :
for b1 being Ring
for b2, b3 being LeftMod of b1
for b4 being Homomorphism of b2,b3 holds
( b4 is isomorphism iff ( b4 is one-to-one & rng b4 = the carrier of b3 ) );

definition
let c1 be Ring;
let c2 be LeftMod of c1;
mode Endomorphism of a2 is Homomorphism of a2,a2;
end;

definition
let c1 be Ring;
let c2 be LeftMod of c1;
let c3 be Endomorphism of c2;
attr a3 is automorphism means :: MOD_4:def 31
( a3 is one-to-one & rng a3 = the carrier of a2 );
end;

:: deftheorem Def31 defines automorphism MOD_4:def 31 :
for b1 being Ring
for b2 being LeftMod of b1
for b3 being Endomorphism of b2 holds
( b3 is automorphism iff ( b3 is one-to-one & rng b3 = the carrier of b2 ) );