let X be RealBanachSpace; :: thesis: for T being Subset of (DualSp X) st ( for x being Point of X ex K being Real st
( 0 <= K & ( for f being Point of (DualSp X) st f in T holds
|.(f . x).| <= K ) ) ) holds
ex L being Real st
( 0 <= L & ( for f being Point of (DualSp X) st f in T holds
||.f.|| <= L ) )
let T be Subset of (DualSp X); :: thesis: ( ( for x being Point of X ex K being Real st
( 0 <= K & ( for f being Point of (DualSp X) st f in T holds
|.(f . x).| <= K ) ) ) implies ex L being Real st
( 0 <= L & ( for f being Point of (DualSp X) st f in T holds
||.f.|| <= L ) ) )
assume AS: for x being Point of X ex K being Real st
( 0 <= K & ( for f being Point of (DualSp X) st f in T holds
|.(f . x).| <= K ) ) ; :: thesis: ex L being Real st
( 0 <= L & ( for f being Point of (DualSp X) st f in T holds
||.f.|| <= L ) )
reconsider T1 = T as Subset of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) by DUALSP02:14;
for x being Point of X ex K being Real st
( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st f in T1 holds
||.(f . x).|| <= K ) )
proof
let x be Point of X; :: thesis: ex K being Real st
( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st f in T1 holds
||.(f . x).|| <= K ) )
consider K being Real such that
B1: ( 0 <= K & ( for f being Point of (DualSp X) st f in T holds
|.(f . x).| <= K ) ) by AS;
take K ; :: thesis: ( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st f in T1 holds
||.(f . x).|| <= K ) )
for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st f in T1 holds
||.(f . x).|| <= K
proof
let f be Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)); :: thesis: ( f in T1 implies ||.(f . x).|| <= K )
assume C2: f in T1 ; :: thesis: ||.(f . x).|| <= K
then reconsider f1 = f as Point of (DualSp X) ;
|.(f1 . x).| = ||.(f . x).|| by EUCLID:def 2;
hence ||.(f . x).|| <= K by C2, B1; :: thesis: verum
end;
hence ( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st f in T1 holds
||.(f . x).|| <= K ) ) by B1; :: thesis: verum
end;
then consider L being Real such that
A1: ( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st f in T1 holds
||.f.|| <= L ) ) by LOPBAN_5:5;
take L ; :: thesis: ( 0 <= L & ( for f being Point of (DualSp X) st f in T holds
||.f.|| <= L ) )
for f being Point of (DualSp X) st f in T holds
||.f.|| <= L
proof
let f be Point of (DualSp X); :: thesis: ( f in T implies ||.f.|| <= L )
assume C5: f in T ; :: thesis: ||.f.|| <= L
then f in T1 ;
then reconsider f1 = f as Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) ;
||.f1.|| = ||.f.|| by DUALSP02:18;
hence ||.f.|| <= L by C5, A1; :: thesis: verum
end;
hence ( 0 <= L & ( for f being Point of (DualSp X) st f in T holds
||.f.|| <= L ) ) by A1; :: thesis: verum