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 A1:
(
f in x &
g in y )
;
f + g in x + y
x in the
carrier of
(Pre-Lp-Space (M,k))
;
then A2:
x in CosetSet (
M,
k)
by Def11;
then consider a being
PartFunc of
X,
REAL such that A3:
(
x = a.e-eq-class_Lp (
a,
M,
k) &
a in Lp_Functions (
M,
k) )
;
A4:
a in x
by A3, Th38;
y in the
carrier of
(Pre-Lp-Space (M,k))
;
then A5:
y in CosetSet (
M,
k)
by Def11;
then consider b being
PartFunc of
X,
REAL such that A6:
(
y = a.e-eq-class_Lp (
b,
M,
k) &
b in Lp_Functions (
M,
k) )
;
b in y
by A6, Th38;
then
(addCoset (M,k)) . (
x,
y)
= a.e-eq-class_Lp (
(a + b),
M,
k)
by A2, A5, A4, Def8;
then A7:
x + y = a.e-eq-class_Lp (
(a + b),
M,
k)
by Def11;
ex
r being
PartFunc of
X,
REAL st
(
f = r &
r in Lp_Functions (
M,
k) &
a a.e.= r,
M )
by A1, A3;
then A8:
a.e-eq-class_Lp (
a,
M,
k)
= a.e-eq-class_Lp (
f,
M,
k)
by Th42;
ex
r being
PartFunc of
X,
REAL st
(
g = r &
r in Lp_Functions (
M,
k) &
b a.e.= r,
M )
by A1, A6;
then
a.e-eq-class_Lp (
b,
M,
k)
= a.e-eq-class_Lp (
g,
M,
k)
by Th42;
then
a.e-eq-class_Lp (
(a + b),
M,
k)
= a.e-eq-class_Lp (
(f + g),
M,
k)
by A1, A3, A6, A8, Th45;
hence
f + g in x + y
by Th38, A7, Th25, A3, A1, A6;
verum
end;
hereby verum
assume A9:
f in x
;
a (#) f in a * x
x in the
carrier of
(Pre-Lp-Space (M,k))
;
then A10:
x in CosetSet (
M,
k)
by Def11;
then consider f1 being
PartFunc of
X,
REAL such that A11:
(
x = a.e-eq-class_Lp (
f1,
M,
k) &
f1 in Lp_Functions (
M,
k) )
;
f1 in x
by A11, Th38;
then
(lmultCoset (M,k)) . (
a,
x)
= a.e-eq-class_Lp (
(a (#) f1),
M,
k)
by A10, Def10;
then A12:
a * x = a.e-eq-class_Lp (
(a (#) f1),
M,
k)
by Def11;
ex
r being
PartFunc of
X,
REAL st
(
f = r &
r in Lp_Functions (
M,
k) &
f1 a.e.= r,
M )
by A9, A11;
then
a.e-eq-class_Lp (
f1,
M,
k)
= a.e-eq-class_Lp (
f,
M,
k)
by Th42;
then
a.e-eq-class_Lp (
(a (#) f1),
M,
k)
= a.e-eq-class_Lp (
(a (#) f),
M,
k)
by A11, A9, Th47;
hence
a (#) f in a * x
by A12, Th26, A9, A11, Th38;
verum
end;