let X be non empty set ; :: thesis: for Y being ComplexLinearSpace holds CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is ComplexLinearSpace
let Y be ComplexLinearSpace; :: thesis: CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is ComplexLinearSpace
set IT = CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #);
( CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is Abelian & CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is add-associative & CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is right_zeroed & CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is right_complementable & CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is ComplexLinearSpace-like )
proof
thus
for
u,
v being
VECTOR of
CLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
u + v = v + u
by Th4;
:: according to RLVECT_1:def 5 :: thesis: ( CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is add-associative & CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is right_zeroed & CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is right_complementable & CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is ComplexLinearSpace-like )
thus
for
u,
v,
w being
VECTOR of
CLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
(u + v) + w = u + (v + w)
by Th5;
:: according to RLVECT_1:def 6 :: thesis: ( CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is right_zeroed & CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is right_complementable & CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is ComplexLinearSpace-like )
thus
for
u being
VECTOR of
CLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
u + (0. CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #)) = u
:: according to RLVECT_1:def 7 :: thesis: ( CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is right_complementable & CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is ComplexLinearSpace-like )proof
let u be
VECTOR of
CLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #);
:: thesis: u + (0. CLSStruct(# (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. CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #)) =
(FuncAdd X,Y) . (FuncZero X,Y),
u'
by Th4
.=
u
by Th6
;
:: thesis: verum
end;
thus
for
u being
VECTOR of
CLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
u is
right_complementable
:: according to ALGSTR_0:def 16 :: thesis: CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is ComplexLinearSpace-like proof
let u be
VECTOR of
CLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #);
:: thesis: u is right_complementable
reconsider u' =
u as
Element of
Funcs X,the
carrier of
Y ;
reconsider w =
(FuncExtMult X,Y) . [(- 1r ),u'] as
VECTOR of
CLSStruct(#
(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. CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #)
thus
u + w = 0. CLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #)
by Th7;
:: thesis: verum
end;
A1:
for
a being
Complex for
u,
v being
VECTOR of
CLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
a * (u + v) = (a * u) + (a * v)
proof
let a be
Complex;
:: thesis: for u, v being VECTOR of CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) holds a * (u + v) = (a * u) + (a * v)let u,
v be
VECTOR of
CLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #);
:: thesis: a * (u + v) = (a * u) + (a * v)
a * (u + v) = (a * u) + (a * v)
proof
reconsider v' =
v,
u' =
u as
Element of
Funcs X,the
carrier of
Y ;
reconsider w =
(FuncExtMult X,Y) . [a,u'],
w' =
(FuncExtMult X,Y) . [a,v'] as
VECTOR of
CLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) ;
a * (u + v) =
(FuncExtMult X,Y) . [a,((FuncAdd X,Y) . u',v')]
by CLVECT_1:def 1
.=
(FuncAdd X,Y) . w,
w'
by Lm1
.=
w + (a * v)
by CLVECT_1:def 1
.=
(a * u) + (a * v)
by CLVECT_1:def 1
;
hence
a * (u + v) = (a * u) + (a * v)
;
:: thesis: verum
end;
hence
a * (u + v) = (a * u) + (a * v)
;
:: thesis: verum
end;
A2:
for
a,
b being
Complex for
v being
VECTOR of
CLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
(a + b) * v = (a * v) + (b * v)
proof
let a,
b be
Complex;
:: thesis: for v being VECTOR of CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) holds (a + b) * v = (a * v) + (b * v)let v be
VECTOR of
CLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #);
:: thesis: (a + b) * v = (a * v) + (b * v)
reconsider v' =
v as
Element of
Funcs X,the
carrier of
Y ;
reconsider w =
(FuncExtMult X,Y) . [a,v'],
w' =
(FuncExtMult X,Y) . [b,v'] as
VECTOR of
CLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) ;
thus (a + b) * v =
(FuncExtMult X,Y) . [(a + b),v']
by CLVECT_1:def 1
.=
(FuncAdd X,Y) . w,
w'
by Th10
.=
w + (b * v)
by CLVECT_1:def 1
.=
(a * v) + (b * v)
by CLVECT_1:def 1
;
:: thesis: verum
end;
A3:
for
a,
b being
Complex for
v being
VECTOR of
CLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
(a * b) * v = a * (b * v)
proof
let a,
b be
Complex;
:: thesis: for v being VECTOR of CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) holds (a * b) * v = a * (b * v)let v be
VECTOR of
CLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #);
:: thesis: (a * b) * v = a * (b * v)
reconsider v' =
v as
Element of
Funcs X,the
carrier of
Y ;
thus (a * b) * v =
(FuncExtMult X,Y) . [(a * b),v']
by CLVECT_1:def 1
.=
(FuncExtMult X,Y) . [a,((FuncExtMult X,Y) . [b,v'])]
by Th9
.=
(FuncExtMult X,Y) . [a,(b * v)]
by CLVECT_1:def 1
.=
a * (b * v)
by CLVECT_1:def 1
;
:: thesis: verum
end;
for
v being
VECTOR of
CLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) holds
1r * v = v
proof
let v be
VECTOR of
CLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #);
:: thesis: 1r * v = v
reconsider v' =
v as
Element of
Funcs X,the
carrier of
Y ;
thus 1r * v =
(FuncExtMult X,Y) . [1r ,v']
by CLVECT_1:def 1
.=
v
by Th8
;
:: thesis: verum
end;
hence
CLSStruct(#
(Funcs X,the carrier of Y),
(FuncZero X,Y),
(FuncAdd X,Y),
(FuncExtMult X,Y) #) is
ComplexLinearSpace-like
by A1, A2, A3, CLVECT_1:def 2;
:: thesis: verum
end;
hence
CLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is ComplexLinearSpace
; :: thesis: verum