set W = BoundedMultilinearOperators (X,Y);
A1: for v, u being VECTOR of (R_VectorSpace_of_MultilinearOperators (X,Y)) st v in BoundedMultilinearOperators (X,Y) & u in BoundedMultilinearOperators (X,Y) holds
v + u in BoundedMultilinearOperators (X,Y)
proof
let v, u be VECTOR of (R_VectorSpace_of_MultilinearOperators (X,Y)); :: thesis: ( v in BoundedMultilinearOperators (X,Y) & u in BoundedMultilinearOperators (X,Y) implies v + u in BoundedMultilinearOperators (X,Y) )
assume that
A2: v in BoundedMultilinearOperators (X,Y) and
A3: u in BoundedMultilinearOperators (X,Y) ; :: thesis: v + u in BoundedMultilinearOperators (X,Y)
reconsider f = v + u as MultilinearOperator of X,Y by Def6;
f is Lipschitzian
proof
reconsider v1 = v as Lipschitzian MultilinearOperator of X,Y by A2, Def9;
consider K2 being Real such that
A4: 0 <= K2 and
A5: for x being Point of (product X) holds ||.(v1 . x).|| <= K2 * (NrProduct x) by Def8;
reconsider u1 = u as Lipschitzian MultilinearOperator of X,Y by A3, Def9;
consider K1 being Real such that
A6: 0 <= K1 and
A7: for x being Point of (product X) holds ||.(u1 . x).|| <= K1 * (NrProduct x) by Def8;
take K3 = K1 + K2; :: according to LOPBAN10:def 10 :: thesis: ( 0 <= K3 & ( for x being Point of (product X) holds ||.(f . x).|| <= K3 * (NrProduct x) ) )
now :: thesis: for x being VECTOR of (product X) holds ||.(f . x).|| <= K3 * (NrProduct x)
let x be VECTOR of (product X); :: thesis: ||.(f . x).|| <= K3 * (NrProduct x)
A8: ||.((u1 . x) + (v1 . x)).|| <= ||.(u1 . x).|| + ||.(v1 . x).|| by NORMSP_1:def 1;
A9: ||.(v1 . x).|| <= K2 * (NrProduct x) by A5;
||.(u1 . x).|| <= K1 * (NrProduct x) by A7;
then A10: ||.(u1 . x).|| + ||.(v1 . x).|| <= (K1 * (NrProduct x)) + (K2 * (NrProduct x)) by A9, XREAL_1:7;
||.(f . x).|| = ||.((u1 . x) + (v1 . x)).|| by Th16;
hence ||.(f . x).|| <= K3 * (NrProduct x) by A8, A10, XXREAL_0:2; :: thesis: verum
end;
hence ( 0 <= K3 & ( for x being Point of (product X) holds ||.(f . x).|| <= K3 * (NrProduct x) ) ) by A4, A6; :: thesis: verum
end;
hence v + u in BoundedMultilinearOperators (X,Y) by Def9; :: thesis: verum
end;
for a being Real
for v being VECTOR of (R_VectorSpace_of_MultilinearOperators (X,Y)) st v in BoundedMultilinearOperators (X,Y) holds
a * v in BoundedMultilinearOperators (X,Y)
proof
let a be Real; :: thesis: for v being VECTOR of (R_VectorSpace_of_MultilinearOperators (X,Y)) st v in BoundedMultilinearOperators (X,Y) holds
a * v in BoundedMultilinearOperators (X,Y)
let v be VECTOR of (R_VectorSpace_of_MultilinearOperators (X,Y)); :: thesis: ( v in BoundedMultilinearOperators (X,Y) implies a * v in BoundedMultilinearOperators (X,Y) )
assume A11: v in BoundedMultilinearOperators (X,Y) ; :: thesis: a * v in BoundedMultilinearOperators (X,Y)
reconsider f = a * v as MultilinearOperator of X,Y by Def6;
f is Lipschitzian
proof
reconsider v1 = v as Lipschitzian MultilinearOperator of X,Y by A11, Def9;
consider K being Real such that
A12: 0 <= K and
A13: for x being Point of (product X) holds ||.(v1 . x).|| <= K * (NrProduct x) by Def8;
take |.a.| * K ; :: according to LOPBAN10:def 10 :: thesis: ( 0 <= |.a.| * K & ( for x being Point of (product X) holds ||.(f . x).|| <= (|.a.| * K) * (NrProduct x) ) )
A14: now :: thesis: for x being VECTOR of (product X) holds ||.(f . x).|| <= (|.a.| * K) * (NrProduct x)
let x be VECTOR of (product X); :: thesis: ||.(f . x).|| <= (|.a.| * K) * (NrProduct x)
0 <= |.a.| by COMPLEX1:46;
then A16: |.a.| * ||.(v1 . x).|| <= |.a.| * (K * (NrProduct x)) by A13, XREAL_1:64;
||.(a * (v1 . x)).|| = |.a.| * ||.(v1 . x).|| by NORMSP_1:def 1;
hence ||.(f . x).|| <= (|.a.| * K) * (NrProduct x) by A16, Th17; :: thesis: verum
end;
0 <= |.a.| by COMPLEX1:46;
hence ( 0 <= |.a.| * K & ( for x being Point of (product X) holds ||.(f . x).|| <= (|.a.| * K) * (NrProduct x) ) ) by A12, A14; :: thesis: verum
end;
hence a * v in BoundedMultilinearOperators (X,Y) by Def9; :: thesis: verum
end;
hence BoundedMultilinearOperators (X,Y) is linearly-closed by A1, RLSUB_1:def 1; :: thesis: verum