let R be Ring; :: thesis: ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #) is strict LeftMod of R
set G = ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #);
A1: for a, b being Element of ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #)
for x, y being Element of Trivial-addLoopStr st x = a & b = y holds
a + b = x + y ;
A2: ( ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #) is Abelian & ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #) is add-associative & ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #) is right_zeroed & ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #) is right_complementable )
proof
thus ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #) is Abelian :: thesis: ( ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #) is add-associative & ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #) is right_zeroed & ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #) is right_complementable )
proof
let a, b be Element of ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #); :: according to RLVECT_1:def 2 :: thesis: a + b = b + a
reconsider x = a, y = b as Element of Trivial-addLoopStr ;
thus a + b = y + x by A1
.= b + a ; :: thesis: verum
end;
hereby :: according to RLVECT_1:def 3 :: thesis: ( ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #) is right_zeroed & ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #) is right_complementable )
let a, b, c be Element of ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #); :: thesis: (a + b) + c = a + (b + c)
reconsider x = a, y = b, z = c as Element of Trivial-addLoopStr ;
thus (a + b) + c = (x + y) + z
.= x + (y + z) by RLVECT_1:def 3
.= a + (b + c) ; :: thesis: verum
end;
hereby :: according to RLVECT_1:def 4 :: thesis: ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #) is right_complementable
let a be Element of ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #); :: thesis: a + (0. ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #)) = a
reconsider x = a as Element of Trivial-addLoopStr ;
thus a + (0. ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #)) = x +
.= a by RLVECT_1:4 ; :: thesis: verum
end;
let a be Element of ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #); :: according to ALGSTR_0:def 16 :: thesis:
reconsider x = a as Element of Trivial-addLoopStr ;
consider b being Element of Trivial-addLoopStr such that
A3: x + b = 0. Trivial-addLoopStr by ALGSTR_0:def 11;
reconsider b9 = b as Element of ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #) ;
take b9 ; :: according to ALGSTR_0:def 11 :: thesis: a + b9 = 0. ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #)
thus a + b9 = 0. ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #) by A3; :: thesis: verum
end;
now :: thesis: for x, y being Scalar of R
for v, w being Vector of ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. R) * v = v )
let x, y be Scalar of R; :: thesis: for v, w being Vector of ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. R) * v = v )

let v, w be Vector of ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #); :: thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. R) * v = v )
A4: ( (x * y) * v = 0. Trivial-addLoopStr & (1. R) * v = 0. Trivial-addLoopStr ) by GRCAT_1:4;
( x * (v + w) = 0. Trivial-addLoopStr & (x + y) * v = 0. Trivial-addLoopStr ) by GRCAT_1:4;
hence ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. R) * v = v ) by ; :: thesis: verum
end;
hence ModuleStr(# ,op2,op0,(pr2 ( the carrier of R,)) #) is strict LeftMod of R by ; :: thesis: verum