let X be non empty set ; :: thesis: for Y being ComplexNormSpace holds ComplexBoundedFunctions (X,Y) is linearly-closed
let Y be ComplexNormSpace; :: thesis: ComplexBoundedFunctions (X,Y) is linearly-closed
set W = ComplexBoundedFunctions (X,Y);
A1: for v, u being VECTOR of (ComplexVectSpace (X,Y)) st v in ComplexBoundedFunctions (X,Y) & u in ComplexBoundedFunctions (X,Y) holds
v + u in ComplexBoundedFunctions (X,Y)
proof
let v, u be VECTOR of (ComplexVectSpace (X,Y)); :: thesis: ( v in ComplexBoundedFunctions (X,Y) & u in ComplexBoundedFunctions (X,Y) implies v + u in ComplexBoundedFunctions (X,Y) )
assume that
A2: v in ComplexBoundedFunctions (X,Y) and
A3: u in ComplexBoundedFunctions (X,Y) ; :: thesis: v + u in ComplexBoundedFunctions (X,Y)
reconsider f = v + u as Function of X, the carrier of Y by FUNCT_2:66;
f is bounded
proof
reconsider v1 = v as bounded Function of X, the carrier of Y by A2, Def5;
consider K2 being Real such that
A4: 0 <= K2 and
A5: for x being Element of X holds ||.(v1 . x).|| <= K2 by Def4;
reconsider u1 = u as bounded Function of X, the carrier of Y by A3, Def5;
consider K1 being Real such that
A6: 0 <= K1 and
A7: for x being Element of X holds ||.(u1 . x).|| <= K1 by Def4;
take K3 = K1 + K2; :: according to CSSPACE4:def 4 :: thesis: ( 0 <= K3 & ( for x being Element of X holds ||.(f . x).|| <= K3 ) )
now :: thesis: for x being Element of X holds ||.(f . x).|| <= K3
let x be Element of X; :: thesis: ||.(f . x).|| <= K3
( ||.(u1 . x).|| <= K1 & ||.(v1 . x).|| <= K2 ) by A7, A5;
then A8: ||.(u1 . x).|| + ||.(v1 . x).|| <= K1 + K2 by XREAL_1:7;
( ||.(f . x).|| = ||.((v1 . x) + (u1 . x)).|| & ||.((u1 . x) + (v1 . x)).|| <= ||.(u1 . x).|| + ||.(v1 . x).|| ) by CLOPBAN1:11, CLVECT_1:def 13;
hence ||.(f . x).|| <= K3 by A8, XXREAL_0:2; :: thesis: verum
end;
hence ( 0 <= K3 & ( for x being Element of X holds ||.(f . x).|| <= K3 ) ) by A6, A4; :: thesis: verum
end;
hence v + u in ComplexBoundedFunctions (X,Y) by Def5; :: thesis: verum
end;
for c being Complex
for v being VECTOR of (ComplexVectSpace (X,Y)) st v in ComplexBoundedFunctions (X,Y) holds
c * v in ComplexBoundedFunctions (X,Y)
proof
let c be Complex; :: thesis: for v being VECTOR of (ComplexVectSpace (X,Y)) st v in ComplexBoundedFunctions (X,Y) holds
c * v in ComplexBoundedFunctions (X,Y)
let v be VECTOR of (ComplexVectSpace (X,Y)); :: thesis: ( v in ComplexBoundedFunctions (X,Y) implies c * v in ComplexBoundedFunctions (X,Y) )
assume A9: v in ComplexBoundedFunctions (X,Y) ; :: thesis: c * v in ComplexBoundedFunctions (X,Y)
reconsider f = c * v as Function of X, the carrier of Y by FUNCT_2:66;
f is bounded
proof
reconsider v1 = v as bounded Function of X, the carrier of Y by A9, Def5;
consider K being Real such that
A10: 0 <= K and
A11: for x being Element of X holds ||.(v1 . x).|| <= K by Def4;
take |.c.| * K ; :: according to CSSPACE4:def 4 :: thesis: ( 0 <= |.c.| * K & ( for x being Element of X holds ||.(f . x).|| <= |.c.| * K ) )
A12: now :: thesis: for x being Element of X holds ||.(f . x).|| <= |.c.| * K
let x be Element of X; :: thesis: ||.(f . x).|| <= |.c.| * K
A13: 0 <= |.c.| by COMPLEX1:46;
( ||.(f . x).|| = ||.(c * (v1 . x)).|| & ||.(c * (v1 . x)).|| = |.c.| * ||.(v1 . x).|| ) by CLOPBAN1:12, CLVECT_1:def 13;
hence ||.(f . x).|| <= |.c.| * K by A11, A13, XREAL_1:64; :: thesis: verum
end;
0 <= |.c.| by COMPLEX1:46;
hence ( 0 <= |.c.| * K & ( for x being Element of X holds ||.(f . x).|| <= |.c.| * K ) ) by A10, A12; :: thesis: verum
end;
hence c * v in ComplexBoundedFunctions (X,Y) by Def5; :: thesis: verum
end;
hence ComplexBoundedFunctions (X,Y) is linearly-closed by A1, CLVECT_1:def 7; :: thesis: verum