let R be comRing; :: thesis: for M, N being LeftMod of R holds Hom (R,M,N) is LeftMod of R
let M, N be LeftMod of R; :: thesis: Hom (R,M,N) is LeftMod of R
A1: Hom (R,M,N) is Abelian

proof

for v, w being Element of (Hom (R,M,N)) holds v + w = w + v

proof

let f, g be Element of (Hom (R,M,N)); :: thesis: f + g = g + f
( f in Hom (R,M,N) & g in Hom (R,M,N) ) ;
then reconsider f1 = f, g1 = g as Element of (Func_Mod (R,M,N)) ;
f + g = f1 + g1 by Th23
.= g + f by Th23 ;
hence f + g = g + f ; :: thesis: verum

end;

hence Hom (R,M,N) is Abelian ; :: thesis: verum

end;

A2: Hom (R,M,N) is add-associative

proof

for f, g, h being Element of (Hom (R,M,N)) holds (f + g) + h = f + (g + h)

proof

let f, g, h be Element of (Hom (R,M,N)); :: thesis: (f + g) + h = f + (g + h)
( f in Hom (R,M,N) & g in Hom (R,M,N) & h in Hom (R,M,N) ) ;
then reconsider f1 = f, g1 = g, h1 = h as Element of (Func_Mod (R,M,N)) ;
A3: g + h = g1 + h1 by Th23;
f + g = f1 + g1 by Th23;
then (f + g) + h = (f1 + g1) + h1 by Th23
.= f1 + (g1 + h1) by Lm17
.= f + (g + h) by A3, Th23 ;
hence (f + g) + h = f + (g + h) ; :: thesis: verum

end;

hence Hom (R,M,N) is add-associative ; :: thesis: verum

end;

A4: Hom (R,M,N) is right_zeroed

proof

for f being Element of (Hom (R,M,N)) holds f + (0. (Hom (R,M,N))) = f

proof

let f be Element of (Hom (R,M,N)); :: thesis: f + (0. (Hom (R,M,N))) = f
f in Hom (R,M,N) ;
then reconsider f1 = f as Element of (Func_Mod (R,M,N)) ;
f + (0. (Hom (R,M,N))) = f1 + (0. (Func_Mod (R,M,N))) by Th23
.= f by Lm18 ;
hence f + (0. (Hom (R,M,N))) = f ; :: thesis: verum

end;

hence Hom (R,M,N) is right_zeroed ; :: thesis: verum

end;

A5: Hom (R,M,N) is right_complementable

proof

let f be Element of (Hom (R,M,N)); :: according to ALGSTR_0:def 16 :: thesis: f is right_complementable
f in Hom (R,M,N) ;
then reconsider f1 = f as Element of (Func_Mod (R,M,N)) ;
reconsider r = - (1. R) as Element of R ;
r * f = r * f1 by Lm30;
then f + (r * f) = f1 + (r * f1) by Th23
.= 0. (Hom (R,M,N)) by Lm19 ;
hence f is right_complementable ; :: thesis: verum

end;

A6: Hom (R,M,N) is vector-distributive

proof

for a being Element of R
for v, w being Element of (Hom (R,M,N)) holds a * (v + w) = (a * v) + (a * w)

proof

let a be Element of R; :: thesis: for v, w being Element of (Hom (R,M,N)) holds a * (v + w) = (a * v) + (a * w)
let v, w be Element of (Hom (R,M,N)); :: thesis: a * (v + w) = (a * v) + (a * w)
( v in Hom (R,M,N) & w in Hom (R,M,N) ) ;
then reconsider v1 = v, w1 = w as Element of (Func_Mod (R,M,N)) ;
A7: v + w = v1 + w1 by Th23;
A8: ( a * v = a * v1 & a * w = a * w1 ) by Lm30;
a * (v + w) = a * (v1 + w1) by A7, Lm30
.= (a * v1) + (a * w1) by Lm20
.= (a * v) + (a * w) by A8, Th23 ;
hence a * (v + w) = (a * v) + (a * w) ; :: thesis: verum

end;

hence Hom (R,M,N) is vector-distributive ; :: thesis: verum

end;

A9: Hom (R,M,N) is scalar-distributive

proof

for a, b being Element of R
for f being Element of (Hom (R,M,N)) holds (a + b) * f = (a * f) + (b * f)

proof

let a, b be Element of R; :: thesis: for f being Element of (Hom (R,M,N)) holds (a + b) * f = (a * f) + (b * f)
let f be Element of (Hom (R,M,N)); :: thesis: (a + b) * f = (a * f) + (b * f)
f in Hom (R,M,N) ;
then reconsider f1 = f as Element of (Func_Mod (R,M,N)) ;
A10: ( a * f = a * f1 & b * f = b * f1 ) by Lm30;
(a + b) * f = (a + b) * f1 by Lm30
.= (a * f1) + (b * f1) by Lm21
.= (a * f) + (b * f) by A10, Th23 ;
hence (a + b) * f = (a * f) + (b * f) ; :: thesis: verum

end;

hence Hom (R,M,N) is scalar-distributive ; :: thesis: verum

end;

A11: Hom (R,M,N) is scalar-associative

proof

for a, b being Element of R
for f being Element of (Hom (R,M,N)) holds (a * b) * f = a * (b * f)

proof

let a, b be Element of R; :: thesis: for f being Element of (Hom (R,M,N)) holds (a * b) * f = a * (b * f)
let f be Element of (Hom (R,M,N)); :: thesis: (a * b) * f = a * (b * f)
f in Hom (R,M,N) ;
then reconsider f1 = f as Element of (Func_Mod (R,M,N)) ;
A12: ( (a * b) * f = (a * b) * f1 & b * f = b * f1 ) by Lm30;
(a * b) * f = (a * b) * f1 by Lm30
.= a * (b * f1) by Lm22
.= a * (b * f) by A12, Lm30 ;
hence (a * b) * f = a * (b * f) ; :: thesis: verum

end;

hence Hom (R,M,N) is scalar-associative ; :: thesis: verum

end;

Hom (R,M,N) is scalar-unital

proof

for f being Element of (Hom (R,M,N)) holds (1. R) * f = f

proof

let f be Element of (Hom (R,M,N)); :: thesis: (1. R) * f = f
f in Hom (R,M,N) ;
then reconsider f1 = f as Element of (Func_Mod (R,M,N)) ;
(1. R) * f = (1. R) * f1 by Lm30
.= f ;
hence (1. R) * f = f ; :: thesis: verum

end;

hence Hom (R,M,N) is scalar-unital ; :: thesis: verum

end;

hence Hom (R,M,N) is LeftMod of R by A1, A2, A4, A5, A6, A9, A11; :: thesis: verum