let X be non empty set ; :: thesis: for Y being RealLinearSpace holds RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is RealLinearSpace
let Y be RealLinearSpace; :: thesis: RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is RealLinearSpace
set IT = RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #);
( RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is Abelian & RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is add-associative & RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is right_zeroed & RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is right_complementable & RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is RealLinearSpace-like )
proof
thus
for
u,
v being
VECTOR of
RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
u + v = v + u
by Th6;
:: according to RLVECT_1:def 5 :: thesis: ( RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is add-associative & RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is right_zeroed & RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is right_complementable & RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is RealLinearSpace-like )
thus
for
u,
v,
w being
VECTOR of
RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
(u + v) + w = u + (v + w)
by Th7;
:: according to RLVECT_1:def 6 :: thesis: ( RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is right_zeroed & RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is right_complementable & RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is RealLinearSpace-like )
thus
for
u being
VECTOR of
RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
u + (0. RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #)) = u
:: according to RLVECT_1:def 7 :: thesis: ( RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is right_complementable & RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is RealLinearSpace-like )proof
let u be
VECTOR of
RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #);
:: thesis: u + (0. RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #)) = u
reconsider u' =
u as
Element of
Funcs X,the
carrier of
Y ;
thus u + (0. RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #)) =
(FuncAdd X,Y) . (FuncZero X,Y),
u'
by Th6
.=
u
by Th8
;
:: thesis: verum
end;
thus
RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) is
right_complementable
:: thesis: RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is RealLinearSpace-like proof
let u be
VECTOR of
RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #);
:: according to ALGSTR_0:def 16 :: thesis: u is right_complementable
reconsider u' =
u as
Element of
Funcs X,the
carrier of
Y ;
reconsider w =
(FuncExtMult X,Y) . [(- 1),u'] as
VECTOR of
RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) ;
take
w
;
:: according to ALGSTR_0:def 11 :: thesis: u + w = 0. RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #)
thus
u + w = 0. RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #)
by Th9;
:: thesis: verum
end;
thus
for
a being
real number for
u,
v being
VECTOR of
RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
a * (u + v) = (a * u) + (a * v)
:: according to RLVECT_1:def 9 :: thesis: ( ( for b1, b2 being set
for b3 being Element of the carrier of RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) holds (b1 + b2) * b3 = (b1 * b3) + (b2 * b3) ) & ( for b1, b2 being set
for b3 being Element of the carrier of RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) holds (b1 * b2) * b3 = b1 * (b2 * b3) ) & ( for b1 being Element of the carrier of RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) holds 1 * b1 = b1 ) )proof
let a be
real number ;
:: thesis: for u, v being VECTOR of RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) holds a * (u + v) = (a * u) + (a * v)
reconsider a =
a as
Real by XREAL_0:def 1;
for
u,
v being
VECTOR of
RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
a * (u + v) = (a * u) + (a * v)
by Lm2;
hence
for
u,
v being
VECTOR of
RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
a * (u + v) = (a * u) + (a * v)
;
:: thesis: verum
end;
thus
for
a,
b being
real number for
v being
VECTOR of
RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
(a + b) * v = (a * v) + (b * v)
:: thesis: ( ( for b1, b2 being set
for b3 being Element of the carrier of RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) holds (b1 * b2) * b3 = b1 * (b2 * b3) ) & ( for b1 being Element of the carrier of RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) holds 1 * b1 = b1 ) )proof
let a,
b be
real number ;
:: thesis: for v being VECTOR of RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) holds (a + b) * v = (a * v) + (b * v)
reconsider a =
a,
b =
b as
Real by XREAL_0:def 1;
for
v being
VECTOR of
RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
(a + b) * v = (a * v) + (b * v)
by Th12;
hence
for
v being
VECTOR of
RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
(a + b) * v = (a * v) + (b * v)
;
:: thesis: verum
end;
thus
for
a,
b being
real number for
v being
VECTOR of
RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
(a * b) * v = a * (b * v)
:: thesis: for b1 being Element of the carrier of RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) holds 1 * b1 = b1proof
let a,
b be
real number ;
:: thesis: for v being VECTOR of RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) holds (a * b) * v = a * (b * v)
reconsider a =
a,
b =
b as
Real by XREAL_0:def 1;
for
v being
VECTOR of
RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
(a * b) * v = a * (b * v)
by Th11;
hence
for
v being
VECTOR of
RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
(a * b) * v = a * (b * v)
;
:: thesis: verum
end;
thus
for
b1 being
Element of the
carrier of
RLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds 1
* b1 = b1
by Th10;
:: thesis: verum
end;
hence
RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is RealLinearSpace
; :: thesis: verum