set l = L-1-CSpace M;
L-1-CSpace M is ComplexNormSpace-like
proof
let x,
y be
Point of
(L-1-CSpace M);
CLVECT_1:def 13 for b1 being object holds
( ||.(b1 * x).|| = |.b1.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )let a be
Complex;
( ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
consider f being
PartFunc of
X,
COMPLEX such that A1:
f in x
and A2:
||.x.|| = Integral (
M,
(abs f))
by Def20;
set aa =
|.a.|;
abs f is_integrable_on M
by A1, Th41;
then
Integral (
M,
(|.a.| (#) (abs f)))
= |.a.| * (Integral (M,(abs f)))
by MESFUNC6:102;
then
Integral (
M,
(abs (a (#) f)))
= |.a.| * (Integral (M,(abs f)))
by RFUNCT_1:25;
then A3:
Integral (
M,
(abs (a (#) f)))
= |.a.| * ||.x.||
by A2;
reconsider a1 =
a as
Element of
COMPLEX by XCMPLX_0:def 2;
A4:
(
f is_integrable_on M &
f in L1_CFunctions M )
by A1, Th41;
consider g being
PartFunc of
X,
COMPLEX such that A5:
g in y
and A6:
||.y.|| = Integral (
M,
(abs g))
by Def20;
A7:
(
g is_integrable_on M &
g in L1_CFunctions M )
by A5, Th41;
A8:
||.(x + y).|| = Integral (
M,
(abs (f + g)))
by A1, A5, Th45, Th43;
a1 (#) f in a1 * x
by A1, Th45;
then A9:
||.(a * x).|| = |.a.| * ||.x.||
by A3, Th43;
(Integral (M,(abs f))) + (Integral (M,(abs g))) = ||.x.|| + ||.y.||
by A2, A6;
then
||.(x + y).|| <= ||.x.|| + ||.y.||
by A4, A8, A7, Th47;
hence
(
||.(a * x).|| = |.a.| * ||.x.|| &
||.(x + y).|| <= ||.x.|| + ||.y.|| )
by A9;
verum
end;
hence
( L-1-CSpace M is ComplexNormSpace-like & L-1-CSpace M is vector-distributive & L-1-CSpace M is scalar-distributive & L-1-CSpace M is scalar-associative & L-1-CSpace M is scalar-unital & L-1-CSpace M is Abelian & L-1-CSpace M is add-associative & L-1-CSpace M is right_zeroed & L-1-CSpace M is right_complementable )
by CSSPACE3:2; verum