let X, Y be ComplexLinearSpace; :: thesis: LinearOperators X,Y is linearly-closed
set W = LinearOperators X,Y;
A1: for v, u being VECTOR of (ComplexVectSpace the carrier of X,Y) st v in LinearOperators X,Y & u in LinearOperators X,Y holds
v + u in LinearOperators X,Y

proof

let v, u be VECTOR of (ComplexVectSpace the carrier of X,Y); :: thesis: ( v in LinearOperators X,Y & u in LinearOperators X,Y implies v + u in LinearOperators X,Y )
assume A2: ( v in LinearOperators X,Y & u in LinearOperators X,Y ) ; :: thesis: v + u in LinearOperators X,Y
v + u is LinearOperator of X,Y

proof

reconsider f = v + u as Function of X,Y by FUNCT_2:121;
f is LinearOperator of X,Y

proof

A3: f is additive

proof

let x, y be VECTOR of X; :: according to CLOPBAN1:def 3 :: thesis: f . (x + y) = (f . x) + (f . y)
reconsider v' = v, u' = u as Element of Funcs the carrier of X,the carrier of Y ;
A4: u' is LinearOperator of X,Y by A2, Def5;
A5: v' is LinearOperator of X,Y by A2, Def5;
thus f . (x + y) = (u' . (x + y)) + (v' . (x + y)) by LOPBAN_1:3
.= ((u' . x) + (u' . y)) + (v' . (x + y)) by A4, Def3
.= ((u' . x) + (u' . y)) + ((v' . x) + (v' . y)) by A5, Def3
.= (((u' . x) + (u' . y)) + (v' . x)) + (v' . y) by RLVECT_1:def 6
.= (((u' . x) + (v' . x)) + (u' . y)) + (v' . y) by RLVECT_1:def 6
.= ((f . x) + (u' . y)) + (v' . y) by LOPBAN_1:3
.= (f . x) + ((u' . y) + (v' . y)) by RLVECT_1:def 6
.= (f . x) + (f . y) by LOPBAN_1:3 ; :: thesis: verum

end;

f is homogeneous

proof

let x be VECTOR of X; :: according to CLOPBAN1:def 4 :: thesis: for r being Complex holds f . (r * x) = r * (f . x)
let s be Complex; :: thesis: f . (s * x) = s * (f . x)
reconsider v' = v, u' = u as Element of Funcs the carrier of X,the carrier of Y ;
A6: u' is LinearOperator of X,Y by A2, Def5;
A7: v' is LinearOperator of X,Y by A2, Def5;
thus f . (s * x) = (u' . (s * x)) + (v' . (s * x)) by LOPBAN_1:3
.= (s * (u' . x)) + (v' . (s * x)) by A6, Def4
.= (s * (u' . x)) + (s * (v' . x)) by A7, Def4
.= s * ((u' . x) + (v' . x)) by CLVECT_1:def 2
.= s * (f . x) by LOPBAN_1:3 ; :: thesis: verum

end;

hence f is LinearOperator of X,Y by A3; :: thesis: verum

end;

hence v + u is LinearOperator of X,Y ; :: thesis: verum

end;

hence v + u in LinearOperators X,Y by Def5; :: thesis: verum

end;

for c being Complex
for v being VECTOR of (ComplexVectSpace the carrier of X,Y) st v in LinearOperators X,Y holds
c * v in LinearOperators X,Y

proof

let c be Complex; :: thesis: for v being VECTOR of (ComplexVectSpace the carrier of X,Y) st v in LinearOperators X,Y holds
c * v in LinearOperators X,Y
let v be VECTOR of (ComplexVectSpace the carrier of X,Y); :: thesis: ( v in LinearOperators X,Y implies c * v in LinearOperators X,Y )
assume A8: v in LinearOperators X,Y ; :: thesis: c * v in LinearOperators X,Y
c * v is LinearOperator of X,Y

proof

reconsider f = c * v as Function of X,Y by FUNCT_2:121;
f is LinearOperator of X,Y

proof

A9: f is additive

proof

let x, y be VECTOR of X; :: according to CLOPBAN1:def 3 :: thesis: f . (x + y) = (f . x) + (f . y)
reconsider v' = v as Element of Funcs the carrier of X,the carrier of Y ;
A10: f = (FuncExtMult the carrier of X,Y) . [c,v'] by CLVECT_1:def 1;
A11: v' is LinearOperator of X,Y by A8, Def5;
thus f . (x + y) = c * (v' . (x + y)) by A10, Th3
.= c * ((v' . x) + (v' . y)) by A11, Def3
.= (c * (v' . x)) + (c * (v' . y)) by CLVECT_1:def 2
.= (f . x) + (c * (v' . y)) by A10, Th3
.= (f . x) + (f . y) by A10, Th3 ; :: thesis: verum

end;

f is homogeneous

proof

let x be VECTOR of X; :: according to CLOPBAN1:def 4 :: thesis: for r being Complex holds f . (r * x) = r * (f . x)
let s be Complex; :: thesis: f . (s * x) = s * (f . x)
reconsider v' = v as Element of Funcs the carrier of X,the carrier of Y ;
A12: f = (FuncExtMult the carrier of X,Y) . [c,v'] by CLVECT_1:def 1;
A13: v' is LinearOperator of X,Y by A8, Def5;
thus f . (s * x) = c * (v' . (s * x)) by A12, Th3
.= c * (s * (v' . x)) by A13, Def4
.= (c * s) * (v' . x) by CLVECT_1:def 2
.= s * (c * (v' . x)) by CLVECT_1:def 2
.= s * (f . x) by A12, Th3 ; :: thesis: verum

end;

hence f is LinearOperator of X,Y by A9; :: thesis: verum

end;

hence c * v is LinearOperator of X,Y ; :: thesis: verum

end;

hence c * v in LinearOperators X,Y by Def5; :: thesis: verum

end;

hence LinearOperators X,Y is linearly-closed by A1, CLVECT_1:def 4; :: thesis: verum