let X be RealNormSpace; :: thesis: for x being Point of (DualSp X)
for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st x = v holds
||.x.|| = ||.v.||
let x be Point of (DualSp X); :: thesis: for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st x = v holds
||.x.|| = ||.v.||
let v be Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)); :: thesis: ( x = v implies ||.x.|| = ||.v.|| )
assume AS: x = v ; :: thesis: ||.x.|| = ||.v.||
BX: R_NormSpace_of_BoundedLinearOperators (X,RNS_Real) = NORMSTR(# (BoundedLinearOperators (X,RNS_Real)),(Zero_ ((BoundedLinearOperators (X,RNS_Real)),(R_VectorSpace_of_LinearOperators (X,RNS_Real)))),(Add_ ((BoundedLinearOperators (X,RNS_Real)),(R_VectorSpace_of_LinearOperators (X,RNS_Real)))),(Mult_ ((BoundedLinearOperators (X,RNS_Real)),(R_VectorSpace_of_LinearOperators (X,RNS_Real)))),(BoundedLinearOperatorsNorm (X,RNS_Real)) #) by LOPBAN_1:def 14;
reconsider x1 = x as Lipschitzian linear-Functional of X by DUALSP01:def 10;
reconsider v1 = v as Lipschitzian LinearOperator of X,RNS_Real by LOPBAN_1:def 9, BX;
now :: thesis: for r being Real st r in PreNorms v1 holds
r <= ||.x.||
let r be Real; :: thesis: ( r in PreNorms v1 implies r <= ||.x.|| )
assume AS2: r in PreNorms v1 ; :: thesis: r <= ||.x.||
PreNorms v1 = { ||.(v . t).|| where t is VECTOR of X : ||.t.|| <= 1 } by LOPBAN_1:def 12;
then consider t being VECTOR of X such that
B1: ( r = ||.(v . t).|| & ||.t.|| <= 1 ) by AS2;
|.(x1 . t).| <= ||.x.|| * ||.t.|| by DUALSP01:26;
then B2: ||.(v . t).|| <= ||.x.|| * ||.t.|| by AS, EUCLID:def 2;
||.x.|| * ||.t.|| <= ||.x.|| * 1 by B1, XREAL_1:64;
hence r <= ||.x.|| by B1, B2, XXREAL_0:2; :: thesis: verum
end;
then upper_bound (PreNorms v1) <= ||.x.|| by SEQ_4:45;
then A4: ||.v.|| <= ||.x.|| by BX, LOPBAN_1:30;
now :: thesis: for r being Real st r in PreNorms x1 holds
r <= ||.v.||
let r be Real; :: thesis: ( r in PreNorms x1 implies r <= ||.v.|| )
assume r in PreNorms x1 ; :: thesis: r <= ||.v.||
then consider t being VECTOR of X such that
B1: ( r = |.(x . t).| & ||.t.|| <= 1 ) ;
||.(v1 . t).|| <= ||.v.|| * ||.t.|| by LOPBAN_1:32;
then B2: |.(x . t).| <= ||.v.|| * ||.t.|| by AS, EUCLID:def 2;
||.v.|| * ||.t.|| <= ||.v.|| * 1 by B1, XREAL_1:64;
hence r <= ||.v.|| by B1, B2, XXREAL_0:2; :: thesis: verum
end;
then upper_bound (PreNorms x1) <= ||.v.|| by SEQ_4:45;
then ||.x.|| <= ||.v.|| by DUALSP01:24;
hence ||.x.|| = ||.v.|| by A4, XXREAL_0:1; :: thesis: verum