set X0 = the carrier of X;
set Z0 = the ZeroF of X;
set ADD = the addF of X;
set LMLT = Mult_INT* X;
set XP = ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #);
A1: ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #) is vector-distributive
proof
let x be Scalar of R; :: according to VECTSP_1:def 13 :: thesis: for b1, b2 being Element of the carrier of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #) holds x * (b1 + b2) = (x * b1) + (x * b2)
let v, w be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #); :: thesis: x * (v + w) = (x * v) + (x * w)
set x1 = x;
reconsider v1 = v, w1 = w as Element of X ;
thus x * (v + w) = x * (v1 + w1)
.= (x * v1) + (x * w1) by VECTSP_1:def 14
.= (x * v) + (x * w) ; :: thesis: verum
end;
A2: ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #) is scalar-distributive
proof
let x, y be Scalar of R; :: according to VECTSP_1:def 14 :: thesis: for b1 being Element of the carrier of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #) holds (x + y) * b1 = (x * b1) + (y * b1)
let v be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #); :: thesis: (x + y) * v = (x * v) + (y * v)
set x1 = x;
set y1 = y;
reconsider v1 = v as Element of X ;
thus (x + y) * v = (x + y) * v1
.= (x * v1) + (y * v1) by VECTSP_1:def 15
.= (x * v) + (y * v) ; :: thesis: verum
end;
A3: ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #) is scalar-associative
proof
let x, y be Scalar of R; :: according to VECTSP_1:def 15 :: thesis: for b1 being Element of the carrier of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #) holds (x * y) * b1 = x * (y * b1)
let v be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #); :: thesis: (x * y) * v = x * (y * v)
set x1 = x;
set y1 = y;
reconsider v1 = v as Element of X ;
thus (x * y) * v = (x * y) * v1
.= x * (y * v1) by VECTSP_1:def 16
.= x * (y * v) ; :: thesis: verum
end;
A4: ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #) is scalar-unital
proof
let v be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #); :: according to VECTSP_1:def 16 :: thesis: (1. R) * v = v
reconsider v1 = v as Element of X ;
thus (1. R) * v = (1. R) * v1
.= v1 by VECTSP_1:def 17
.= v ; :: thesis: verum
end;
A5: now :: thesis: for u, v, w being Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #) holds u + (v + w) = (u + v) + w
let u, v, w be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #); :: thesis: u + (v + w) = (u + v) + w
reconsider u1 = u, v1 = v, w1 = w as Element of X ;
thus u + (v + w) = u1 + (v1 + w1)
.= (u1 + v1) + w1 by RLVECT_1:def 3
.= (u + v) + w ; :: thesis: verum
end;
A6: now :: thesis: for v being Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #) holds v + (0. ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #)) = v
let v be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #); :: thesis: v + (0. ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #)) = v
reconsider v1 = v as Element of X ;
thus v + (0. ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #)) = v1 + (0. X)
.= v by RLVECT_1:def 4 ; :: thesis: verum
end;
A7: now :: thesis: for v being Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #) holds v is right_complementable
let v be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #); :: thesis:
reconsider v1 = v as Element of X ;
consider w1 being Element of X such that
A8: v1 + w1 = 0. X by ALGSTR_0:def 11;
reconsider w = w1 as Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #) ;
v + w = 0. ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #) by A8;
hence v is right_complementable ; :: thesis: verum
end;
now :: thesis: for v, w being Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #) holds v + w = w + v
let v, w be Element of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #); :: thesis: v + w = w + v
reconsider v1 = v, w1 = w as Element of X ;
thus v + w = v1 + w1
.= w1 + v1
.= w + v ; :: thesis: verum
end;
hence ( modetrans X is Abelian & modetrans X is add-associative & modetrans X is right_zeroed & modetrans X is right_complementable & modetrans X is vector-distributive & modetrans X is scalar-distributive & modetrans X is scalar-associative & modetrans X is scalar-unital ) by A1, A2, A3, A4, A5, A6, A7; :: thesis: verum