let X, Y be ComplexNormSpace; :: thesis: BoundedLinearOperators (X,Y) is linearly-closed

set W = BoundedLinearOperators (X,Y);

A1: for v, u being VECTOR of (C_VectorSpace_of_LinearOperators (X,Y)) st v in BoundedLinearOperators (X,Y) & u in BoundedLinearOperators (X,Y) holds

v + u in BoundedLinearOperators (X,Y)

for v being VECTOR of (C_VectorSpace_of_LinearOperators (X,Y)) st v in BoundedLinearOperators (X,Y) holds

c * v in BoundedLinearOperators (X,Y)

set W = BoundedLinearOperators (X,Y);

A1: for v, u being VECTOR of (C_VectorSpace_of_LinearOperators (X,Y)) st v in BoundedLinearOperators (X,Y) & u in BoundedLinearOperators (X,Y) holds

v + u in BoundedLinearOperators (X,Y)

proof

for c being Complex
let v, u be VECTOR of (C_VectorSpace_of_LinearOperators (X,Y)); :: thesis: ( v in BoundedLinearOperators (X,Y) & u in BoundedLinearOperators (X,Y) implies v + u in BoundedLinearOperators (X,Y) )

assume that

A2: v in BoundedLinearOperators (X,Y) and

A3: u in BoundedLinearOperators (X,Y) ; :: thesis: v + u in BoundedLinearOperators (X,Y)

reconsider f = v + u as LinearOperator of X,Y by Def4;

f is Lipschitzian

end;assume that

A2: v in BoundedLinearOperators (X,Y) and

A3: u in BoundedLinearOperators (X,Y) ; :: thesis: v + u in BoundedLinearOperators (X,Y)

reconsider f = v + u as LinearOperator of X,Y by Def4;

f is Lipschitzian

proof

hence
v + u in BoundedLinearOperators (X,Y)
by Def7; :: thesis: verum
reconsider v1 = v as Lipschitzian LinearOperator of X,Y by A2, Def7;

consider K2 being Real such that

A4: 0 <= K2 and

A5: for x being VECTOR of X holds ||.(v1 . x).|| <= K2 * ||.x.|| by Def6;

reconsider u1 = u as Lipschitzian LinearOperator of X,Y by A3, Def7;

consider K1 being Real such that

A6: 0 <= K1 and

A7: for x being VECTOR of X holds ||.(u1 . x).|| <= K1 * ||.x.|| by Def6;

take K3 = K1 + K2; :: according to CLOPBAN1:def 6 :: thesis: ( 0 <= K3 & ( for x being VECTOR of X holds ||.(f . x).|| <= K3 * ||.x.|| ) )

end;consider K2 being Real such that

A4: 0 <= K2 and

A5: for x being VECTOR of X holds ||.(v1 . x).|| <= K2 * ||.x.|| by Def6;

reconsider u1 = u as Lipschitzian LinearOperator of X,Y by A3, Def7;

consider K1 being Real such that

A6: 0 <= K1 and

A7: for x being VECTOR of X holds ||.(u1 . x).|| <= K1 * ||.x.|| by Def6;

take K3 = K1 + K2; :: according to CLOPBAN1:def 6 :: thesis: ( 0 <= K3 & ( for x being VECTOR of X holds ||.(f . x).|| <= K3 * ||.x.|| ) )

now :: thesis: for x being VECTOR of X holds ||.(f . x).|| <= K3 * ||.x.||

hence
( 0 <= K3 & ( for x being VECTOR of X holds ||.(f . x).|| <= K3 * ||.x.|| ) )
by A6, A4; :: thesis: verumlet x be VECTOR of X; :: thesis: ||.(f . x).|| <= K3 * ||.x.||

A8: ||.((u1 . x) + (v1 . x)).|| <= ||.(u1 . x).|| + ||.(v1 . x).|| by CLVECT_1:def 13;

A9: ||.(v1 . x).|| <= K2 * ||.x.|| by A5;

||.(u1 . x).|| <= K1 * ||.x.|| by A7;

then A10: ||.(u1 . x).|| + ||.(v1 . x).|| <= (K1 * ||.x.||) + (K2 * ||.x.||) by A9, XREAL_1:7;

||.(f . x).|| = ||.((u1 . x) + (v1 . x)).|| by Th15;

hence ||.(f . x).|| <= K3 * ||.x.|| by A8, A10, XXREAL_0:2; :: thesis: verum

end;A8: ||.((u1 . x) + (v1 . x)).|| <= ||.(u1 . x).|| + ||.(v1 . x).|| by CLVECT_1:def 13;

A9: ||.(v1 . x).|| <= K2 * ||.x.|| by A5;

||.(u1 . x).|| <= K1 * ||.x.|| by A7;

then A10: ||.(u1 . x).|| + ||.(v1 . x).|| <= (K1 * ||.x.||) + (K2 * ||.x.||) by A9, XREAL_1:7;

||.(f . x).|| = ||.((u1 . x) + (v1 . x)).|| by Th15;

hence ||.(f . x).|| <= K3 * ||.x.|| by A8, A10, XXREAL_0:2; :: thesis: verum

for v being VECTOR of (C_VectorSpace_of_LinearOperators (X,Y)) st v in BoundedLinearOperators (X,Y) holds

c * v in BoundedLinearOperators (X,Y)

proof

hence
BoundedLinearOperators (X,Y) is linearly-closed
by A1, CLVECT_1:def 7; :: thesis: verum
let c be Complex; :: thesis: for v being VECTOR of (C_VectorSpace_of_LinearOperators (X,Y)) st v in BoundedLinearOperators (X,Y) holds

c * v in BoundedLinearOperators (X,Y)

let v be VECTOR of (C_VectorSpace_of_LinearOperators (X,Y)); :: thesis: ( v in BoundedLinearOperators (X,Y) implies c * v in BoundedLinearOperators (X,Y) )

assume A11: v in BoundedLinearOperators (X,Y) ; :: thesis: c * v in BoundedLinearOperators (X,Y)

reconsider f = c * v as LinearOperator of X,Y by Def4;

f is Lipschitzian

end;c * v in BoundedLinearOperators (X,Y)

let v be VECTOR of (C_VectorSpace_of_LinearOperators (X,Y)); :: thesis: ( v in BoundedLinearOperators (X,Y) implies c * v in BoundedLinearOperators (X,Y) )

assume A11: v in BoundedLinearOperators (X,Y) ; :: thesis: c * v in BoundedLinearOperators (X,Y)

reconsider f = c * v as LinearOperator of X,Y by Def4;

f is Lipschitzian

proof

hence
c * v in BoundedLinearOperators (X,Y)
by Def7; :: thesis: verum
reconsider v1 = v as Lipschitzian LinearOperator of X,Y by A11, Def7;

consider K being Real such that

A12: 0 <= K and

A13: for x being VECTOR of X holds ||.(v1 . x).|| <= K * ||.x.|| by Def6;

take |.c.| * K ; :: according to CLOPBAN1:def 6 :: thesis: ( 0 <= |.c.| * K & ( for x being VECTOR of X holds ||.(f . x).|| <= (|.c.| * K) * ||.x.|| ) )

hence ( 0 <= |.c.| * K & ( for x being VECTOR of X holds ||.(f . x).|| <= (|.c.| * K) * ||.x.|| ) ) by A12, A14; :: thesis: verum

end;consider K being Real such that

A12: 0 <= K and

A13: for x being VECTOR of X holds ||.(v1 . x).|| <= K * ||.x.|| by Def6;

take |.c.| * K ; :: according to CLOPBAN1:def 6 :: thesis: ( 0 <= |.c.| * K & ( for x being VECTOR of X holds ||.(f . x).|| <= (|.c.| * K) * ||.x.|| ) )

A14: now :: thesis: for x being VECTOR of X holds ||.(f . x).|| <= (|.c.| * K) * ||.x.||

0 <= |.c.|
by COMPLEX1:46;let x be VECTOR of X; :: thesis: ||.(f . x).|| <= (|.c.| * K) * ||.x.||

0 <= |.c.| by COMPLEX1:46;

then A15: |.c.| * ||.(v1 . x).|| <= |.c.| * (K * ||.x.||) by A13, XREAL_1:64;

||.(c * (v1 . x)).|| = |.c.| * ||.(v1 . x).|| by CLVECT_1:def 13;

hence ||.(f . x).|| <= (|.c.| * K) * ||.x.|| by A15, Th16; :: thesis: verum

end;0 <= |.c.| by COMPLEX1:46;

then A15: |.c.| * ||.(v1 . x).|| <= |.c.| * (K * ||.x.||) by A13, XREAL_1:64;

||.(c * (v1 . x)).|| = |.c.| * ||.(v1 . x).|| by CLVECT_1:def 13;

hence ||.(f . x).|| <= (|.c.| * K) * ||.x.|| by A15, Th16; :: thesis: verum

hence ( 0 <= |.c.| * K & ( for x being VECTOR of X holds ||.(f . x).|| <= (|.c.| * K) * ||.x.|| ) ) by A12, A14; :: thesis: verum