:: Opposite Rings, Modules and their Morphisms
:: by Micha{\l} Muzalewski
::
:: Received June 22, 1992
:: Copyright (c) 1992 Association of Mizar Users
theorem Th1: :: MOD_4:1
:: deftheorem defines opp MOD_4:def 1 :
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 )
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 )
theorem :: MOD_4:2
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) )
theorem :: MOD_4:3
canceled;
theorem :: MOD_4:4
theorem :: MOD_4:5
theorem :: MOD_4:6
theorem Th7: :: MOD_4:7
Lm5:
for F being non empty commutative doubleLoopStr
for x, y being Element of F holds x * y = y * x
;
theorem :: MOD_4:8
definition
let K be non
empty doubleLoopStr ;
let V be non
empty VectSpStr of
K;
func opp V -> strict RightModStr of
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 of 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 #)
uniqueness
for b1, b2 being strict RightModStr of 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
end;
:: deftheorem Def2 defines opp MOD_4:def 2 :
theorem Th9: :: MOD_4:9
:: deftheorem defines opp MOD_4:def 3 :
theorem Th10: :: MOD_4:10
definition
let K be non
empty doubleLoopStr ;
let W be non
empty RightModStr of
K;
func opp W -> strict VectSpStr of
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 of 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 #)
uniqueness
for b1, b2 being strict VectSpStr of 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
end;
:: deftheorem Def4 defines opp MOD_4:def 4 :
theorem :: MOD_4:11
canceled;
theorem Th12: :: MOD_4:12
:: deftheorem defines opp MOD_4:def 5 :
theorem Th13: :: MOD_4:13
theorem :: MOD_4:14
canceled;
theorem :: MOD_4:15
canceled;
theorem :: MOD_4:16
theorem Th17: :: MOD_4:17
theorem Th18: :: MOD_4:18
theorem :: MOD_4:19
canceled;
theorem :: MOD_4:20
theorem Th21: :: MOD_4:21
theorem Th22: :: MOD_4:22
theorem :: MOD_4:23
theorem :: MOD_4:24
theorem Th25: :: MOD_4:25
theorem Th26: :: MOD_4:26
:: deftheorem Def6 defines antimultiplicative MOD_4:def 6 :
:: deftheorem Def7 defines antilinear MOD_4:def 7 :
:: deftheorem Def8 defines monomorphism MOD_4:def 8 :
:: deftheorem Def9 defines antimonomorphism MOD_4:def 9 :
:: deftheorem Def10 defines epimorphism MOD_4:def 10 :
:: deftheorem Def11 defines antiepimorphism MOD_4:def 11 :
:: deftheorem Def12 defines isomorphism MOD_4:def 12 :
:: deftheorem Def13 defines antiisomorphism MOD_4:def 13 :
:: deftheorem Def14 defines endomorphism MOD_4:def 14 :
:: deftheorem Def15 defines antiendomorphism MOD_4:def 15 :
:: deftheorem Def16 defines automorphism MOD_4:def 16 :
:: deftheorem Def17 defines antiautomorphism MOD_4:def 17 :
theorem :: MOD_4:27
theorem Th28: :: MOD_4:28
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) ) & ( for x, y being Scalar of K holds (id K) . (x * y) = ((id K) . x) * ((id K) . y) ) & (id K) . (1_ K) = 1_ K & id K is one-to-one & rng (id K) = the carrier of K )
theorem :: MOD_4:29
Lm7:
for K, L being Ring
for J being Function of K,L st J is linear holds
J . (0. K) = 0. L
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)
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)
theorem :: MOD_4:30
Lm10:
for K, L being Ring
for J being Function of K,L st J is antilinear holds
J . (0. K) = 0. L
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)
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)
theorem :: MOD_4:31
theorem :: MOD_4:32
theorem :: MOD_4:33
:: deftheorem defines opp MOD_4:def 18 :
theorem :: MOD_4:34
theorem Th35: :: MOD_4:35
theorem Th36: :: MOD_4:36
theorem Th37: :: MOD_4:37
theorem Th38: :: MOD_4:38
theorem :: MOD_4:39
theorem :: MOD_4:40
theorem Th41: :: MOD_4:41
theorem Th42: :: MOD_4:42
theorem :: MOD_4:43
theorem :: MOD_4:44
theorem :: MOD_4:45
theorem :: MOD_4:46
Lm13:
for G, H being AddGroup
for x, y being Element of G holds (ZeroMap G,H) . (x + y) = ((ZeroMap G,H) . x) + ((ZeroMap G,H) . y)
:: deftheorem Def19 defines Homomorphism MOD_4:def 19 :
Lm14:
for G being AddGroup holds
( ( for x, y being Element of G holds (id G) . (x + y) = ((id G) . x) + ((id G) . y) ) & id G is one-to-one & id G is onto )
Lm15:
for G, H being AddGroup
for f being Homomorphism of G,H holds f . (0. G) = 0. H
Lm16:
for H, G being AddGroup
for f being Homomorphism of G,H
for x being Element of G holds f . (- x) = - (f . x)
Lm17:
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)
theorem :: MOD_4:47
canceled;
theorem :: MOD_4:48
theorem :: MOD_4:49
Lm18:
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)
Lm19:
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)
:: deftheorem MOD_4:def 20 :
canceled;
:: deftheorem MOD_4:def 21 :
canceled;
:: deftheorem MOD_4:def 22 :
canceled;
:: deftheorem MOD_4:def 23 :
canceled;
:: deftheorem Def24 defines Homomorphism MOD_4:def 24 :
theorem :: MOD_4:50
:: deftheorem defines is_monomorphism_wrp MOD_4:def 25 :
:: deftheorem defines is_epimorphism_wrp MOD_4:def 26 :
:: deftheorem defines is_isomorphism_wrp MOD_4:def 27 :
:: deftheorem defines is_automorphism_wrp MOD_4:def 28 :
theorem :: MOD_4:51
:: deftheorem defines monomorphism MOD_4:def 29 :
:: deftheorem defines epimorphism MOD_4:def 30 :
:: deftheorem defines isomorphism MOD_4:def 31 :
:: deftheorem defines automorphism MOD_4:def 32 :