let X be non empty set ; :: thesis: for a being Complex
for F, G being Point of holds
( ( = 0 implies F = 0. ) & ( F = 0. implies = 0 ) & ||.(a * F).|| = |.a.| * & ||.(F + G).|| <= + )

let a be Complex; :: thesis: for F, G being Point of holds
( ( = 0 implies F = 0. ) & ( F = 0. implies = 0 ) & ||.(a * F).|| = |.a.| * & ||.(F + G).|| <= + )

let F, G be Point of ; :: thesis: ( ( = 0 implies F = 0. ) & ( F = 0. implies = 0 ) & ||.(a * F).|| = |.a.| * & ||.(F + G).|| <= + )
A1: now :: thesis: ( F = 0. implies = 0 )
set z = X --> 0c;
reconsider z = X --> 0c as Function of X,COMPLEX ;
F in ComplexBoundedFunctions X ;
then consider g being Function of X,COMPLEX such that
A2: F = g and
A3: g | X is bounded ;
A4: ( not PreNorms g is empty & PreNorms g is bounded_above ) by ;
consider r0 being object such that
A5: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 = r0 as Real by A5;
A6: ( ( for s being Real st s in PreNorms g holds
s <= 0 ) implies upper_bound () <= 0 ) by SEQ_4:45;
assume F = 0. ; :: thesis:
then A7: z = g by ;
A8: now :: thesis: for r being Real st r in PreNorms g holds
( 0 <= r & r <= 0 )
let r be Real; :: thesis: ( r in PreNorms g implies ( 0 <= r & r <= 0 ) )
assume r in PreNorms g ; :: thesis: ( 0 <= r & r <= 0 )
then consider t being Element of X such that
A9: r = |.(g . t).| ;
|.(g . t).| = by A7
.= 0 ;
hence ( 0 <= r & r <= 0 ) by A9; :: thesis: verum
end;
then 0 <= r0 by A5;
then upper_bound () = 0 by ;
hence ||.F.|| = 0 by A2, A3, Th13; :: thesis: verum
end;
A10: ||.(F + G).|| <= +
proof
F + G in ComplexBoundedFunctions X ;
then consider h1 being Function of X,COMPLEX such that
A11: h1 = F + G and
A12: h1 | X is bounded ;
G in ComplexBoundedFunctions X ;
then consider g1 being Function of X,COMPLEX such that
A13: g1 = G and
A14: g1 | X is bounded ;
F in ComplexBoundedFunctions X ;
then consider f1 being Function of X,COMPLEX such that
A15: f1 = F and
A16: f1 | X is bounded ;
A17: now :: thesis: for t being Element of X holds |.(h1 . t).| <= +
let t be Element of X; :: thesis: |.(h1 . t).| <= +
( |.(f1 . t).| <= & |.(g1 . t).| <= ) by A15, A16, A13, A14, Th19;
then A18: |.(f1 . t).| + |.(g1 . t).| <= + by XREAL_1:7;
( |.(h1 . t).| = |.((f1 . t) + (g1 . t)).| & |.((f1 . t) + (g1 . t)).| <= |.(f1 . t).| + |.(g1 . t).| ) by ;
hence |.(h1 . t).| <= + by ; :: thesis: verum
end;
A19: now :: thesis: for r being Real st r in PreNorms h1 holds
r <= +
let r be Real; :: thesis: ( r in PreNorms h1 implies r <= + )
assume r in PreNorms h1 ; :: thesis:
then ex t being Element of X st r = |.(h1 . t).| ;
hence r <= + by A17; :: thesis: verum
end;
( ( for s being Real st s in PreNorms h1 holds
s <= + ) implies upper_bound (PreNorms h1) <= + ) by SEQ_4:45;
hence ||.(F + G).|| <= + by ; :: thesis: verum
end;
A20: ||.(a * F).|| = |.a.| *
proof
F in ComplexBoundedFunctions X ;
then consider f1 being Function of X,COMPLEX such that
A21: f1 = F and
A22: f1 | X is bounded ;
a * F in ComplexBoundedFunctions X ;
then consider h1 being Function of X,COMPLEX such that
A23: h1 = a * F and
A24: h1 | X is bounded ;
A25: now :: thesis: for t being Element of X holds |.(h1 . t).| <= |.a.| *
let t be Element of X; :: thesis: |.(h1 . t).| <= |.a.| *
|.(h1 . t).| = |.(a * (f1 . t)).| by ;
then |.(h1 . t).| = |.a.| * |.(f1 . t).| by COMPLEX1:65;
hence |.(h1 . t).| <= |.a.| * by ; :: thesis: verum
end;
A26: now :: thesis: for r being Real st r in PreNorms h1 holds
r <= |.a.| *
let r be Real; :: thesis: ( r in PreNorms h1 implies r <= |.a.| * )
assume r in PreNorms h1 ; :: thesis:
then ex t being Element of X st r = |.(h1 . t).| ;
hence r <= |.a.| * by A25; :: thesis: verum
end;
( ( for s being Real st s in PreNorms h1 holds
s <= |.a.| * ) implies upper_bound (PreNorms h1) <= |.a.| * ) by SEQ_4:45;
then A27: ||.(a * F).|| <= |.a.| * by ;
per cases ( a <> 0 or a = 0 ) ;
suppose A28: a <> 0 ; :: thesis: ||.(a * F).|| = |.a.| *
A29: now :: thesis: for t being Element of X holds |.(f1 . t).| <= () * ||.(a * F).||
let t be Element of X; :: thesis: |.(f1 . t).| <= () * ||.(a * F).||
|.(a ").| = |.(1 / a).| ;
then A30: |.(a ").| = 1 / |.a.| by COMPLEX1:80;
h1 . t = a * (f1 . t) by ;
then (a ") * (h1 . t) = ((a ") * a) * (f1 . t) ;
then A31: (a ") * (h1 . t) = 1 * (f1 . t) by ;
( |.((a ") * (h1 . t)).| = |.(a ").| * |.(h1 . t).| & 0 <= |.(a ").| ) by COMPLEX1:65;
hence |.(f1 . t).| <= () * ||.(a * F).|| by ; :: thesis: verum
end;
A32: now :: thesis: for r being Real st r in PreNorms f1 holds
r <= () * ||.(a * F).||
let r be Real; :: thesis: ( r in PreNorms f1 implies r <= () * ||.(a * F).|| )
assume r in PreNorms f1 ; :: thesis: r <= () * ||.(a * F).||
then ex t being Element of X st r = |.(f1 . t).| ;
hence r <= () * ||.(a * F).|| by A29; :: thesis: verum
end;
( ( for s being Real st s in PreNorms f1 holds
s <= () * ||.(a * F).|| ) implies upper_bound (PreNorms f1) <= () * ||.(a * F).|| ) by SEQ_4:45;
then ||.F.|| <= () * ||.(a * F).|| by ;
then |.a.| * <= |.a.| * (() * ||.(a * F).||) by XREAL_1:64;
then |.a.| * <= (|.a.| * ()) * ||.(a * F).|| ;
then |.a.| * <= 1 * ||.(a * F).|| by ;
hence ||.(a * F).|| = |.a.| * by ; :: thesis: verum
end;
suppose A33: a = 0 ; :: thesis: ||.(a * F).|| = |.a.| *
reconsider fz = F as VECTOR of ;
a * fz = (a + a) * fz by A33
.= (a * fz) + (a * fz) by CLVECT_1:def 3 ;
then 0. = (- (a * fz)) + ((a * fz) + (a * fz)) by VECTSP_1:16;
then 0. = ((- (a * fz)) + (a * fz)) + (a * fz) by RLVECT_1:def 3;
then 0. = + (a * fz) by VECTSP_1:16;
then A34: a * F = 0. by RLVECT_1:4;
|.a.| * = 0 * by A33;
hence ||.(a * F).|| = |.a.| * by ; :: thesis: verum
end;
end;
end;
now :: thesis: ( = 0 implies F = 0. )
set z = X --> 0c;
reconsider z = X --> 0c as Function of X,COMPLEX ;
F in ComplexBoundedFunctions X ;
then consider g being Function of X,COMPLEX such that
A35: F = g and
A36: g | X is bounded ;
assume A37: ||.F.|| = 0 ; :: thesis:
now :: thesis: for t being Element of X holds g . t = z . t
let t be Element of X; :: thesis: g . t = z . t
|.(g . t).| = 0 by ;
hence g . t = 0
.= z . t ;
:: thesis: verum
end;
then g = z by FUNCT_2:63;
hence F = 0. by ; :: thesis: verum
end;
hence ( ( ||.F.|| = 0 implies F = 0. ) & ( F = 0. implies = 0 ) & ||.(a * F).|| = |.a.| * & ||.(F + G).|| <= + ) by A1, A20, A10; :: thesis: verum