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)) #);
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)) #); :: thesis:
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 ; :: 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 Th6; :: thesis: 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; :: 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)
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) ; :: thesis: verum
end;
hence a * (u + v) = (a * u) + (a * v) ; :: thesis: 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; :: 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 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 ; :: thesis: 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; :: 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 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) ; :: thesis: 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)) #); :: thesis: 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 ; :: thesis: 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)) #); :: thesis: 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 ; :: thesis: 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 ; :: thesis: verum