let X be non empty set ; 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; 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)) #);
A1:
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 Th4;
A2:
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
proof
let u be
VECTOR of
CLSStruct(#
(Funcs (X, the carrier of Y)),
(FuncZero (X,Y)),
(FuncAdd (X,Y)),
(FuncExtMult (X,Y)) #);
u is right_complementable
reconsider u9 =
u as
Element of
Funcs (
X, the
carrier of
Y) ;
reconsider mj =
- 1r as
Element of
COMPLEX by XCMPLX_0:def 2;
reconsider w =
(FuncExtMult (X,Y)) . [mj,u9] as
VECTOR of
CLSStruct(#
(Funcs (X, the carrier of Y)),
(FuncZero (X,Y)),
(FuncAdd (X,Y)),
(FuncExtMult (X,Y)) #) ;
take
w
;
ALGSTR_0:def 11 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 Th6;
verum
end;
A3:
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;
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)) #);
a * (u + v) = (a * u) + (a * v)
reconsider a =
a as
Element of
COMPLEX by XCMPLX_0:def 2;
a * (u + v) = (a * u) + (a * v)
proof
reconsider v9 =
v,
u9 =
u as
Element of
Funcs (
X, the
carrier of
Y) ;
reconsider w =
(FuncExtMult (X,Y)) . [a,u9],
w9 =
(FuncExtMult (X,Y)) . [a,v9] 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)) . (u9,v9))]
by CLVECT_1:def 1
.=
(FuncAdd (X,Y)) . (
w,
w9)
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)
;
verum
end;
hence
a * (u + v) = (a * u) + (a * v)
;
verum
end;
A4:
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;
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)) #);
(a * b) * v = a * (b * v)
reconsider v9 =
v as
Element of
Funcs (
X, the
carrier of
Y) ;
thus (a * b) * v =
(FuncExtMult (X,Y)) . [(a * b),v9]
by CLVECT_1:def 1
.=
(FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,v9])]
by Th8
.=
(FuncExtMult (X,Y)) . [a,(b * v)]
by CLVECT_1:def 1
.=
a * (b * v)
by CLVECT_1:def 1
;
verum
end;
A5:
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;
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)) #);
(a + b) * v = (a * v) + (b * v)
reconsider a =
a,
b =
b as
Element of
COMPLEX by XCMPLX_0:def 2;
reconsider v9 =
v as
Element of
Funcs (
X, the
carrier of
Y) ;
reconsider w =
(FuncExtMult (X,Y)) . [a,v9],
w9 =
(FuncExtMult (X,Y)) . [b,v9] as
VECTOR of
CLSStruct(#
(Funcs (X, the carrier of Y)),
(FuncZero (X,Y)),
(FuncAdd (X,Y)),
(FuncExtMult (X,Y)) #) ;
(a + b) * v =
(FuncExtMult (X,Y)) . [(a + b),v9]
by CLVECT_1:def 1
.=
(FuncAdd (X,Y)) . (
w,
w9)
by Th9
.=
w + (b * v)
by CLVECT_1:def 1
.=
(a * v) + (b * v)
by CLVECT_1:def 1
;
hence
(a + b) * v = (a * v) + (b * v)
;
verum
end;
A6:
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
proof
let u be
VECTOR of
CLSStruct(#
(Funcs (X, the carrier of Y)),
(FuncZero (X,Y)),
(FuncAdd (X,Y)),
(FuncExtMult (X,Y)) #);
u + (0. CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #)) = u
reconsider u9 =
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)),
u9)
by Th3
.=
u
by Th5
;
verum
end;
A7:
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)) #);
1r * v = v
reconsider v9 =
v as
Element of
Funcs (
X, the
carrier of
Y) ;
thus 1r * v =
(FuncExtMult (X,Y)) . [1r,v9]
by CLVECT_1:def 1
.=
v
by Th7
;
verum
end;
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 Th3;
hence
CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is ComplexLinearSpace
by A1, A6, A2, A3, A5, A4, A7, ALGSTR_0:def 16, CLVECT_1:def 2, CLVECT_1:def 3, CLVECT_1:def 4, CLVECT_1:def 5, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4; verum