begin
begin
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 )
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) )
Lm5:
for F being non empty commutative doubleLoopStr
for x, y being Element of F holds x * y = y * x
;
begin
definition
let K be non
empty doubleLoopStr ;
let V be non
empty VectSpStr over
K;
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 #)
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
end;
definition
let K be non
empty doubleLoopStr ;
let W be non
empty RightModStr over
K;
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 #)
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
end;
begin
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 )
Lm7:
for K, L being Ring
for J being Function of K,L st J is additive 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)
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)
begin
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
begin
Lm14:
for G, H being AddGroup
for f being Homomorphism of G,H holds f . (0. G) = 0. H
Lm15:
for H, G being AddGroup
for f being Homomorphism of G,H
for x being Element of G holds f . (- x) = - (f . x)
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)
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)
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)