let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for a being Real
for k being positive Real
for x, y being Point of (Lp-Space (M,k)) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )
let S be SigmaField of X; for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for a being Real
for k being positive Real
for x, y being Point of (Lp-Space (M,k)) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )
let M be sigma_Measure of S; for f, g being PartFunc of X,REAL
for a being Real
for k being positive Real
for x, y being Point of (Lp-Space (M,k)) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )
let f, g be PartFunc of X,REAL; for a being Real
for k being positive Real
for x, y being Point of (Lp-Space (M,k)) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )
let a be Real; for k being positive Real
for x, y being Point of (Lp-Space (M,k)) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )
let k be positive Real; for x, y being Point of (Lp-Space (M,k)) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )
let x, y be Point of (Lp-Space (M,k)); ( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )
set C = CosetSet (M,k);
hereby ( f in x implies a (#) f in a * x )
assume A2:
(
f in x &
g in y )
;
f + g in x + y
x in the
carrier of
(Pre-Lp-Space (M,k))
;
then A3:
x in CosetSet (
M,
k)
by VSPDef6X;
then consider a being
PartFunc of
X,
REAL such that A4:
(
x = a.e-eq-class_Lp (
a,
M,
k) &
a in Lp_Functions (
M,
k) )
;
A5:
a in x
by A4, EQC01;
y in the
carrier of
(Pre-Lp-Space (M,k))
;
then A6:
y in CosetSet (
M,
k)
by VSPDef6X;
then consider b being
PartFunc of
X,
REAL such that A7:
(
y = a.e-eq-class_Lp (
b,
M,
k) &
b in Lp_Functions (
M,
k) )
;
b in y
by A7, EQC01;
then
(addCoset (M,k)) . (
x,
y)
= a.e-eq-class_Lp (
(a + b),
M,
k)
by A3, A6, A5, VSPDef3X;
then A9:
x + y = a.e-eq-class_Lp (
(a + b),
M,
k)
by VSPDef6X;
ex
r being
PartFunc of
X,
REAL st
(
f = r &
r in Lp_Functions (
M,
k) &
a a.e.= r,
M )
by A2, A4;
then A11:
a.e-eq-class_Lp (
a,
M,
k)
= a.e-eq-class_Lp (
f,
M,
k)
by EQC02bx;
ex
r being
PartFunc of
X,
REAL st
(
g = r &
r in Lp_Functions (
M,
k) &
b a.e.= r,
M )
by A2, A7;
then
a.e-eq-class_Lp (
b,
M,
k)
= a.e-eq-class_Lp (
g,
M,
k)
by EQC02bx;
then
a.e-eq-class_Lp (
(a + b),
M,
k)
= a.e-eq-class_Lp (
(f + g),
M,
k)
by A2, A4, A7, A11, EQC03b;
hence
f + g in x + y
by EQC01, A9, Th01aLp, A4, A2, A7;
verum
end;
hereby verum
assume A15:
f in x
;
a (#) f in a * x
x in the
carrier of
(Pre-Lp-Space (M,k))
;
then A16:
x in CosetSet (
M,
k)
by VSPDef6X;
then consider f1 being
PartFunc of
X,
REAL such that A17:
(
x = a.e-eq-class_Lp (
f1,
M,
k) &
f1 in Lp_Functions (
M,
k) )
;
f1 in x
by A17, EQC01;
then
(lmultCoset (M,k)) . (
a,
x)
= a.e-eq-class_Lp (
(a (#) f1),
M,
k)
by A16, VSPDef5X;
then A19:
a * x = a.e-eq-class_Lp (
(a (#) f1),
M,
k)
by VSPDef6X;
ex
r being
PartFunc of
X,
REAL st
(
f = r &
r in Lp_Functions (
M,
k) &
f1 a.e.= r,
M )
by A15, A17;
then
a.e-eq-class_Lp (
f1,
M,
k)
= a.e-eq-class_Lp (
f,
M,
k)
by EQC02bx;
then
a.e-eq-class_Lp (
(a (#) f1),
M,
k)
= a.e-eq-class_Lp (
(a (#) f),
M,
k)
by A17, A15, EQC04b;
hence
a (#) f in a * x
by A19, Th01bLp, A15, A17, EQC01;
verum
end;