let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S holds
( L-1-Space M is RealNormSpace-like & L-1-Space M is vector-distributive & L-1-Space M is scalar-distributive & L-1-Space M is scalar-associative & L-1-Space M is scalar-unital & L-1-Space M is Abelian & L-1-Space M is add-associative & L-1-Space M is right_zeroed & L-1-Space M is right_complementable )
let S be SigmaField of X; for M being sigma_Measure of S holds
( L-1-Space M is RealNormSpace-like & L-1-Space M is vector-distributive & L-1-Space M is scalar-distributive & L-1-Space M is scalar-associative & L-1-Space M is scalar-unital & L-1-Space M is Abelian & L-1-Space M is add-associative & L-1-Space M is right_zeroed & L-1-Space M is right_complementable )
let M be sigma_Measure of S; ( L-1-Space M is RealNormSpace-like & L-1-Space M is vector-distributive & L-1-Space M is scalar-distributive & L-1-Space M is scalar-associative & L-1-Space M is scalar-unital & L-1-Space M is Abelian & L-1-Space M is add-associative & L-1-Space M is right_zeroed & L-1-Space M is right_complementable )
now for x, y being Point of (L-1-Space M)
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (L-1-Space M) ) & ( x = 0. (L-1-Space M) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )let x,
y be
Point of
(L-1-Space M);
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (L-1-Space M) ) & ( x = 0. (L-1-Space M) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )let a be
Real;
( ( ||.x.|| = 0 implies x = 0. (L-1-Space M) ) & ( x = 0. (L-1-Space M) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )consider f being
PartFunc of
X,
REAL such that A1:
f in x
and A2:
||.x.|| = Integral (
M,
(abs f))
by Def19;
abs f is_integrable_on M
by A1, Th47;
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, EXTREAL1:1;
hereby ( ( x = 0. (L-1-Space M) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )
set g =
X --> 0;
reconsider x1 =
x as
Point of
(Pre-L-Space M) ;
consider f being
PartFunc of
X,
REAL such that A4:
f in x1
and
(L-1-Norm M) . x1 = Integral (
M,
(abs f))
by Def19;
A5:
f in L1_Functions M
by A4, Th47;
then A6:
a.e-eq-class (
f,
M)
in CosetSet M
;
A7:
X --> 0 in L1_Functions M
by Lm3;
assume
||.x.|| = 0
;
x = 0. (L-1-Space M)then
Integral (
M,
(abs f))
= 0
by A4, Th49;
then
f a.e.= X --> 0,
M
by A5, Th53;
then
a.e-eq-class (
(X --> 0),
M)
= a.e-eq-class (
f,
M)
by A5, A7, Th39;
then
zeroCoset M = a.e-eq-class (
f,
M)
by A7, A6, Def16;
then
0. (Pre-L-Space M) = a.e-eq-class (
f,
M)
by Def18;
hence
x = 0. (L-1-Space M)
by A4, Th50;
verum
end; A11:
f is_integrable_on M
by A1, Th47;
then
|.(Integral (M,f)).| <= Integral (
M,
(abs f))
by MESFUNC6:95;
hence
0 <= ||.x.||
by A2, EXTREAL1:14;
( ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )consider g being
PartFunc of
X,
REAL such that A12:
g in y
and A13:
||.y.|| = Integral (
M,
(abs g))
by Def19;
A14:
g is_integrable_on M
by A12, Th47;
f + g in x + y
by A1, A12, Th51;
then A15:
||.(x + y).|| = Integral (
M,
(abs (f + g)))
by Th49;
(Integral (M,(abs f))) + (Integral (M,(abs g))) = ||.x.|| + ||.y.||
by A2, A13, SUPINF_2:1;
hence
||.(x + y).|| <= ||.x.|| + ||.y.||
by A11, A15, A14, Th55;
||.(a * x).|| = |.a.| * ||.x.||
a (#) f in a * x
by A1, Th51;
hence
||.(a * x).|| = |.a.| * ||.x.||
by A3, Th49;
verum end;
hence
( L-1-Space M is RealNormSpace-like & L-1-Space M is vector-distributive & L-1-Space M is scalar-distributive & L-1-Space M is scalar-associative & L-1-Space M is scalar-unital & L-1-Space M is Abelian & L-1-Space M is add-associative & L-1-Space M is right_zeroed & L-1-Space M is right_complementable )
by NORMSP_1:def 1, RSSPACE3:2; verum