let A be non empty set ; :: thesis: CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is ComplexLinearSpace
set IT = CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #);
( CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is Abelian & CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is add-associative & CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is right_zeroed & CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is right_complementable & CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is ComplexLinearSpace-like )
proof
thus
for
u,
v being
VECTOR of
CLSStruct(#
(Funcs A,COMPLEX ),
(ComplexFuncZero A),
(ComplexFuncAdd A),
(ComplexFuncExtMult A) #) holds
u + v = v + u
by Th7;
:: according to RLVECT_1:def 5 :: thesis: ( CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is add-associative & CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is right_zeroed & CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is right_complementable & CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is ComplexLinearSpace-like )
thus
for
u,
v,
w being
VECTOR of
CLSStruct(#
(Funcs A,COMPLEX ),
(ComplexFuncZero A),
(ComplexFuncAdd A),
(ComplexFuncExtMult A) #) holds
(u + v) + w = u + (v + w)
by Th8;
:: according to RLVECT_1:def 6 :: thesis: ( CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is right_zeroed & CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is right_complementable & CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is ComplexLinearSpace-like )
thus
for
u being
VECTOR of
CLSStruct(#
(Funcs A,COMPLEX ),
(ComplexFuncZero A),
(ComplexFuncAdd A),
(ComplexFuncExtMult A) #) holds
u + (0. CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #)) = u
:: according to RLVECT_1:def 7 :: thesis: ( CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is right_complementable & CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is ComplexLinearSpace-like )proof
let u be
VECTOR of
CLSStruct(#
(Funcs A,COMPLEX ),
(ComplexFuncZero A),
(ComplexFuncAdd A),
(ComplexFuncExtMult A) #);
:: thesis: u + (0. CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #)) = u
reconsider u' =
u as
Element of
Funcs A,
COMPLEX ;
thus u + (0. CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #)) =
(ComplexFuncAdd A) . (ComplexFuncZero A),
u'
by Th7
.=
u
by Th12
;
:: thesis: verum
end;
thus
for
u being
VECTOR of
CLSStruct(#
(Funcs A,COMPLEX ),
(ComplexFuncZero A),
(ComplexFuncAdd A),
(ComplexFuncExtMult A) #) holds
u is
right_complementable
:: according to ALGSTR_0:def 16 :: thesis: CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is ComplexLinearSpace-like proof
let u be
VECTOR of
CLSStruct(#
(Funcs A,COMPLEX ),
(ComplexFuncZero A),
(ComplexFuncAdd A),
(ComplexFuncExtMult A) #);
:: thesis: u is right_complementable
reconsider u' =
u as
Element of
Funcs A,
COMPLEX ;
reconsider w =
(ComplexFuncExtMult A) . [(- 1r ),u'] as
VECTOR of
CLSStruct(#
(Funcs A,COMPLEX ),
(ComplexFuncZero A),
(ComplexFuncAdd A),
(ComplexFuncExtMult A) #) ;
take
w
;
:: according to ALGSTR_0:def 11 :: thesis: u + w = 0. CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #)
thus
u + w = 0. CLSStruct(#
(Funcs A,COMPLEX ),
(ComplexFuncZero A),
(ComplexFuncAdd A),
(ComplexFuncExtMult A) #)
by Th13;
:: thesis: verum
end;
thus
for
a being
Complex for
u,
v being
VECTOR of
CLSStruct(#
(Funcs A,COMPLEX ),
(ComplexFuncZero A),
(ComplexFuncAdd A),
(ComplexFuncExtMult A) #) holds
a * (u + v) = (a * u) + (a * v)
by Lm2;
:: according to CLVECT_1:def 2 :: thesis: ( ( for b1, b2 being Element of COMPLEX
for b3 being Element of the carrier of CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) holds (b1 + b2) * b3 = (b1 * b3) + (b2 * b3) ) & ( for b1, b2 being Element of COMPLEX
for b3 being Element of the carrier of CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) holds (b1 * b2) * b3 = b1 * (b2 * b3) ) & ( for b1 being Element of the carrier of CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) holds 1r * b1 = b1 ) )
thus
for
a,
b being
Complex for
v being
VECTOR of
CLSStruct(#
(Funcs A,COMPLEX ),
(ComplexFuncZero A),
(ComplexFuncAdd A),
(ComplexFuncExtMult A) #) holds
(a + b) * v = (a * v) + (b * v)
by Th16;
:: thesis: ( ( for b1, b2 being Element of COMPLEX
for b3 being Element of the carrier of CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) holds (b1 * b2) * b3 = b1 * (b2 * b3) ) & ( for b1 being Element of the carrier of CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) holds 1r * b1 = b1 ) )
thus
for
a,
b being
Complex for
v being
VECTOR of
CLSStruct(#
(Funcs A,COMPLEX ),
(ComplexFuncZero A),
(ComplexFuncAdd A),
(ComplexFuncExtMult A) #) holds
(a * b) * v = a * (b * v)
by Th15;
:: thesis: for b1 being Element of the carrier of CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) holds 1r * b1 = b1
thus
for
b1 being
Element of the
carrier of
CLSStruct(#
(Funcs A,COMPLEX ),
(ComplexFuncZero A),
(ComplexFuncAdd A),
(ComplexFuncExtMult A) #) holds
1r * b1 = b1
by Th14;
:: thesis: verum
end;
hence
CLSStruct(# (Funcs A,COMPLEX ),(ComplexFuncZero A),(ComplexFuncAdd A),(ComplexFuncExtMult A) #) is ComplexLinearSpace
; :: thesis: verum