let X be RealNormSpace; :: thesis: for x being Point of X st not X is trivial holds
||.x.|| = ||.((BidualFunc X) . x).||
let x be Point of X; :: thesis: ( not X is trivial implies ||.x.|| = ||.((BidualFunc X) . x).|| )
assume AS: not X is trivial ; :: thesis: ||.x.|| = ||.((BidualFunc X) . x).||
reconsider f = BiDual x as Lipschitzian linear-Functional of (DualSp X) by DUALSP01:def 10;
consider Y being non empty Subset of REAL such that
A1: ( Y = { |.((Bound2Lipschitz (s,X)) . x).| where s is Point of (DualSp X) : ||.s.|| <= 1 } & ||.x.|| = upper_bound Y ) by AS, Th71;
set Z = { |.(f . t).| where t is Point of (DualSp X) : ||.t.|| <= 1 } ;
A2: Y c= { |.(f . t).| where t is Point of (DualSp X) : ||.t.|| <= 1 }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in { |.(f . t).| where t is Point of (DualSp X) : ||.t.|| <= 1 } )
assume y in Y ; :: thesis: y in { |.(f . t).| where t is Point of (DualSp X) : ||.t.|| <= 1 }
then consider s being Point of (DualSp X) such that
B1: ( y = |.((Bound2Lipschitz (s,X)) . x).| & ||.s.|| <= 1 ) by A1;
s is Lipschitzian linear-Functional of X by DUALSP01:def 10;
then B2: |.((Bound2Lipschitz (s,X)) . x).| = |.(s . x).| by DUALSP01:23;
f . s = s . x by Def1;
hence y in { |.(f . t).| where t is Point of (DualSp X) : ||.t.|| <= 1 } by B1, B2; :: thesis: verum
end;
upper_bound Y <= upper_bound (PreNorms f) by A2, SEQ_4:48;
then A4: ||.x.|| <= ||.(BiDual x).|| by A1, DUALSP01:24;
{ |.(f . t).| where t is Point of (DualSp X) : ||.t.|| <= 1 } c= Y
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { |.(f . t).| where t is Point of (DualSp X) : ||.t.|| <= 1 } or y in Y )
assume y in { |.(f . t).| where t is Point of (DualSp X) : ||.t.|| <= 1 } ; :: thesis: y in Y
then consider t being Point of (DualSp X) such that
C1: ( y = |.(f . t).| & ||.t.|| <= 1 ) ;
t is Lipschitzian linear-Functional of X by DUALSP01:def 10;
then C2: |.((Bound2Lipschitz (t,X)) . x).| = |.(t . x).| by DUALSP01:23;
|.(f . t).| = |.(t . x).| by Def1;
hence y in Y by C1, C2, A1; :: thesis: verum
end;
then Y = { |.(f . t).| where t is Point of (DualSp X) : ||.t.|| <= 1 } by A2;
then upper_bound (PreNorms f) <= upper_bound Y ;
then ||.(BiDual x).|| <= upper_bound Y by DUALSP01:24;
then ||.(BiDual x).|| = ||.x.|| by A1, A4, XXREAL_0:1;
hence ||.x.|| = ||.((BidualFunc X) . x).|| by Def2; :: thesis: verum