let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for k being geq_than_1 Real holds

( Lp-Space (M,k) is reflexive & Lp-Space (M,k) is discerning & Lp-Space (M,k) is RealNormSpace-like & Lp-Space (M,k) is vector-distributive & Lp-Space (M,k) is scalar-distributive & Lp-Space (M,k) is scalar-associative & Lp-Space (M,k) is scalar-unital & Lp-Space (M,k) is Abelian & Lp-Space (M,k) is add-associative & Lp-Space (M,k) is right_zeroed & Lp-Space (M,k) is right_complementable )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for k being geq_than_1 Real holds

( Lp-Space (M,k) is reflexive & Lp-Space (M,k) is discerning & Lp-Space (M,k) is RealNormSpace-like & Lp-Space (M,k) is vector-distributive & Lp-Space (M,k) is scalar-distributive & Lp-Space (M,k) is scalar-associative & Lp-Space (M,k) is scalar-unital & Lp-Space (M,k) is Abelian & Lp-Space (M,k) is add-associative & Lp-Space (M,k) is right_zeroed & Lp-Space (M,k) is right_complementable )

let M be sigma_Measure of S; :: thesis: for k being geq_than_1 Real holds

( Lp-Space (M,k) is reflexive & Lp-Space (M,k) is discerning & Lp-Space (M,k) is RealNormSpace-like & Lp-Space (M,k) is vector-distributive & Lp-Space (M,k) is scalar-distributive & Lp-Space (M,k) is scalar-associative & Lp-Space (M,k) is scalar-unital & Lp-Space (M,k) is Abelian & Lp-Space (M,k) is add-associative & Lp-Space (M,k) is right_zeroed & Lp-Space (M,k) is right_complementable )

let k be geq_than_1 Real; :: thesis: ( Lp-Space (M,k) is reflexive & Lp-Space (M,k) is discerning & Lp-Space (M,k) is RealNormSpace-like & Lp-Space (M,k) is vector-distributive & Lp-Space (M,k) is scalar-distributive & Lp-Space (M,k) is scalar-associative & Lp-Space (M,k) is scalar-unital & Lp-Space (M,k) is Abelian & Lp-Space (M,k) is add-associative & Lp-Space (M,k) is right_zeroed & Lp-Space (M,k) is right_complementable )

set x = 0. (Lp-Space (M,k));

0. (Lp-Space (M,k)) = 0. (Pre-Lp-Space (M,k)) ;

then 0. (Lp-Space (M,k)) = zeroCoset (M,k) by Def11;

then X --> 0 in 0. (Lp-Space (M,k)) by Th38, Th23;

then ex r being Real st

( 0 <= r & r = Integral (M,((abs (X --> 0)) to_power k)) & ||.(0. (Lp-Space (M,k))).|| = r to_power (1 / k) ) by Th55;

then consider r0 being Real such that

A1: ( r0 = Integral (M,((abs (X --> 0)) to_power k)) & (Lp-Norm (M,k)) . (0. (Lp-Space (M,k))) = r0 to_power (1 / k) ) ;

r0 = 0 by A1, Th58;

hence ||.(0. (Lp-Space (M,k))).|| = 0 by A1, POWER:def 2; :: according to NORMSP_0:def 6 :: thesis: ( Lp-Space (M,k) is discerning & Lp-Space (M,k) is RealNormSpace-like & Lp-Space (M,k) is vector-distributive & Lp-Space (M,k) is scalar-distributive & Lp-Space (M,k) is scalar-associative & Lp-Space (M,k) is scalar-unital & Lp-Space (M,k) is Abelian & Lp-Space (M,k) is add-associative & Lp-Space (M,k) is right_zeroed & Lp-Space (M,k) is right_complementable )

for M being sigma_Measure of S

for k being geq_than_1 Real holds

( Lp-Space (M,k) is reflexive & Lp-Space (M,k) is discerning & Lp-Space (M,k) is RealNormSpace-like & Lp-Space (M,k) is vector-distributive & Lp-Space (M,k) is scalar-distributive & Lp-Space (M,k) is scalar-associative & Lp-Space (M,k) is scalar-unital & Lp-Space (M,k) is Abelian & Lp-Space (M,k) is add-associative & Lp-Space (M,k) is right_zeroed & Lp-Space (M,k) is right_complementable )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for k being geq_than_1 Real holds

( Lp-Space (M,k) is reflexive & Lp-Space (M,k) is discerning & Lp-Space (M,k) is RealNormSpace-like & Lp-Space (M,k) is vector-distributive & Lp-Space (M,k) is scalar-distributive & Lp-Space (M,k) is scalar-associative & Lp-Space (M,k) is scalar-unital & Lp-Space (M,k) is Abelian & Lp-Space (M,k) is add-associative & Lp-Space (M,k) is right_zeroed & Lp-Space (M,k) is right_complementable )

let M be sigma_Measure of S; :: thesis: for k being geq_than_1 Real holds

( Lp-Space (M,k) is reflexive & Lp-Space (M,k) is discerning & Lp-Space (M,k) is RealNormSpace-like & Lp-Space (M,k) is vector-distributive & Lp-Space (M,k) is scalar-distributive & Lp-Space (M,k) is scalar-associative & Lp-Space (M,k) is scalar-unital & Lp-Space (M,k) is Abelian & Lp-Space (M,k) is add-associative & Lp-Space (M,k) is right_zeroed & Lp-Space (M,k) is right_complementable )

let k be geq_than_1 Real; :: thesis: ( Lp-Space (M,k) is reflexive & Lp-Space (M,k) is discerning & Lp-Space (M,k) is RealNormSpace-like & Lp-Space (M,k) is vector-distributive & Lp-Space (M,k) is scalar-distributive & Lp-Space (M,k) is scalar-associative & Lp-Space (M,k) is scalar-unital & Lp-Space (M,k) is Abelian & Lp-Space (M,k) is add-associative & Lp-Space (M,k) is right_zeroed & Lp-Space (M,k) is right_complementable )

set x = 0. (Lp-Space (M,k));

0. (Lp-Space (M,k)) = 0. (Pre-Lp-Space (M,k)) ;

then 0. (Lp-Space (M,k)) = zeroCoset (M,k) by Def11;

then X --> 0 in 0. (Lp-Space (M,k)) by Th38, Th23;

then ex r being Real st

( 0 <= r & r = Integral (M,((abs (X --> 0)) to_power k)) & ||.(0. (Lp-Space (M,k))).|| = r to_power (1 / k) ) by Th55;

then consider r0 being Real such that

A1: ( r0 = Integral (M,((abs (X --> 0)) to_power k)) & (Lp-Norm (M,k)) . (0. (Lp-Space (M,k))) = r0 to_power (1 / k) ) ;

r0 = 0 by A1, Th58;

hence ||.(0. (Lp-Space (M,k))).|| = 0 by A1, POWER:def 2; :: according to NORMSP_0:def 6 :: thesis: ( Lp-Space (M,k) is discerning & Lp-Space (M,k) is RealNormSpace-like & Lp-Space (M,k) is vector-distributive & Lp-Space (M,k) is scalar-distributive & Lp-Space (M,k) is scalar-associative & Lp-Space (M,k) is scalar-unital & Lp-Space (M,k) is Abelian & Lp-Space (M,k) is add-associative & Lp-Space (M,k) is right_zeroed & Lp-Space (M,k) is right_complementable )

now :: thesis: for x, y being Point of (Lp-Space (M,k))

for a being Real holds

( ( ||.x.|| = 0 implies x = 0. (Lp-Space (M,k)) ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )

hence
( Lp-Space (M,k) is discerning & Lp-Space (M,k) is RealNormSpace-like & Lp-Space (M,k) is vector-distributive & Lp-Space (M,k) is scalar-distributive & Lp-Space (M,k) is scalar-associative & Lp-Space (M,k) is scalar-unital & Lp-Space (M,k) is Abelian & Lp-Space (M,k) is add-associative & Lp-Space (M,k) is right_zeroed & Lp-Space (M,k) is right_complementable )
by NORMSP_1:def 1, RSSPACE3:2; :: thesis: verumfor a being Real holds

( ( ||.x.|| = 0 implies x = 0. (Lp-Space (M,k)) ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )

let x, y be Point of (Lp-Space (M,k)); :: thesis: for a being Real holds

( ( ||.x.|| = 0 implies x = 0. (Lp-Space (M,k)) ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )

let a be Real; :: thesis: ( ( ||.x.|| = 0 implies x = 0. (Lp-Space (M,k)) ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )

A2: 1 <= k by Def1;

A7: ( f in x & ex r1 being Real st

( r1 = Integral (M,((abs f) to_power k)) & ||.x.|| = r1 to_power (1 / k) ) ) by Def12;

A8: ( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) ) by Th51, A7;

consider g being PartFunc of X,REAL such that

A9: ( g in y & ex r2 being Real st

( r2 = Integral (M,((abs g) to_power k)) & ||.y.|| = r2 to_power (1 / k) ) ) by Def12;

A10: ( (abs g) to_power k is_integrable_on M & g in Lp_Functions (M,k) ) by Th51, A9;

consider s1 being Real such that

A11: ( s1 = Integral (M,((abs f) to_power k)) & ||.x.|| = s1 to_power (1 / k) ) by A7;

A12: ( s1 = 0 implies s1 to_power (1 / k) >= 0 ) by POWER:def 2;

( s1 > 0 implies s1 to_power (1 / k) >= 0 ) by POWER:34;

hence 0 <= ||.x.|| by A12, A8, A11, Th49; :: thesis: ( ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )

set t = f + g;

set w = x + y;

A13: s1 >= 0 by A8, A11, Th49;

consider s2 being Real such that

A14: ( s2 = Integral (M,((abs g) to_power k)) & ||.y.|| = s2 to_power (1 / k) ) by A9;

f + g in x + y by Th54, A7, A9;

then ex r being Real st

( 0 <= r & r = Integral (M,((abs (f + g)) to_power k)) & ||.(x + y).|| = r to_power (1 / k) ) by Th53;

hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by Th61, A2, A8, A10, A14, A11; :: thesis: ||.(a * x).|| = |.a.| * ||.x.||

set t = a (#) f;

set w = a * x;

a (#) f in a * x by Th54, A7;

then ex r being Real st

( 0 <= r & r = Integral (M,((abs (a (#) f)) to_power k)) & ||.(a * x).|| = r to_power (1 / k) ) by Th53;

then consider s being Real such that

A15: ( s = Integral (M,((abs (a (#) f)) to_power k)) & ||.(a * x).|| = s to_power (1 / k) ) ;

reconsider r = |.a.| to_power k as Real ;

A16: s = Integral (M,(r (#) ((abs f) to_power k))) by A15, Th18

.= r * (Integral (M,((abs f) to_power k))) by A8, MESFUNC6:102

.= r * s1 by A11, EXTREAL1:1

.= (|.a.| to_power k) * s1 ;

|.a.| to_power k >= 0 by Th4, COMPLEX1:46;

then ||.(a * x).|| = ((|.a.| to_power k) to_power (1 / k)) * (s1 to_power (1 / k)) by A13, A15, A16, Th5

.= (|.a.| to_power (k * (1 / k))) * (s1 to_power (1 / k)) by COMPLEX1:46, HOLDER_1:2

.= (|.a.| to_power 1) * (s1 to_power (1 / k)) by XCMPLX_1:106 ;

hence ||.(a * x).|| = |.a.| * ||.x.|| by A11, POWER:25; :: thesis: verum

end;( ( ||.x.|| = 0 implies x = 0. (Lp-Space (M,k)) ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )

let a be Real; :: thesis: ( ( ||.x.|| = 0 implies x = 0. (Lp-Space (M,k)) ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )

A2: 1 <= k by Def1;

hereby :: thesis: ( 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )

consider f being PartFunc of X,REAL such that assume A3:
||.x.|| = 0
; :: thesis: x = 0. (Lp-Space (M,k))

consider f being PartFunc of X,REAL such that

A4: ( f in x & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) ) by Def12;

A5: f in Lp_Functions (M,k) by Th51, A4;

then consider r1 being Real such that

A6: ( r1 = Integral (M,((abs f) to_power k)) & r1 >= 0 & (Lp-Norm (M,k)) . x = r1 to_power (1 / k) ) by A4, Th49;

r1 = 0 by A3, A6, POWER:34;

then zeroCoset (M,k) = a.e-eq-class_Lp (f,M,k) by A5, A6, Th57, Th42;

then 0. (Pre-Lp-Space (M,k)) = a.e-eq-class_Lp (f,M,k) by Def11;

hence x = 0. (Lp-Space (M,k)) by A4, Th55; :: thesis: verum

end;consider f being PartFunc of X,REAL such that

A4: ( f in x & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) ) by Def12;

A5: f in Lp_Functions (M,k) by Th51, A4;

then consider r1 being Real such that

A6: ( r1 = Integral (M,((abs f) to_power k)) & r1 >= 0 & (Lp-Norm (M,k)) . x = r1 to_power (1 / k) ) by A4, Th49;

r1 = 0 by A3, A6, POWER:34;

then zeroCoset (M,k) = a.e-eq-class_Lp (f,M,k) by A5, A6, Th57, Th42;

then 0. (Pre-Lp-Space (M,k)) = a.e-eq-class_Lp (f,M,k) by Def11;

hence x = 0. (Lp-Space (M,k)) by A4, Th55; :: thesis: verum

A7: ( f in x & ex r1 being Real st

( r1 = Integral (M,((abs f) to_power k)) & ||.x.|| = r1 to_power (1 / k) ) ) by Def12;

A8: ( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) ) by Th51, A7;

consider g being PartFunc of X,REAL such that

A9: ( g in y & ex r2 being Real st

( r2 = Integral (M,((abs g) to_power k)) & ||.y.|| = r2 to_power (1 / k) ) ) by Def12;

A10: ( (abs g) to_power k is_integrable_on M & g in Lp_Functions (M,k) ) by Th51, A9;

consider s1 being Real such that

A11: ( s1 = Integral (M,((abs f) to_power k)) & ||.x.|| = s1 to_power (1 / k) ) by A7;

A12: ( s1 = 0 implies s1 to_power (1 / k) >= 0 ) by POWER:def 2;

( s1 > 0 implies s1 to_power (1 / k) >= 0 ) by POWER:34;

hence 0 <= ||.x.|| by A12, A8, A11, Th49; :: thesis: ( ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )

set t = f + g;

set w = x + y;

A13: s1 >= 0 by A8, A11, Th49;

consider s2 being Real such that

A14: ( s2 = Integral (M,((abs g) to_power k)) & ||.y.|| = s2 to_power (1 / k) ) by A9;

f + g in x + y by Th54, A7, A9;

then ex r being Real st

( 0 <= r & r = Integral (M,((abs (f + g)) to_power k)) & ||.(x + y).|| = r to_power (1 / k) ) by Th53;

hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by Th61, A2, A8, A10, A14, A11; :: thesis: ||.(a * x).|| = |.a.| * ||.x.||

set t = a (#) f;

set w = a * x;

a (#) f in a * x by Th54, A7;

then ex r being Real st

( 0 <= r & r = Integral (M,((abs (a (#) f)) to_power k)) & ||.(a * x).|| = r to_power (1 / k) ) by Th53;

then consider s being Real such that

A15: ( s = Integral (M,((abs (a (#) f)) to_power k)) & ||.(a * x).|| = s to_power (1 / k) ) ;

reconsider r = |.a.| to_power k as Real ;

A16: s = Integral (M,(r (#) ((abs f) to_power k))) by A15, Th18

.= r * (Integral (M,((abs f) to_power k))) by A8, MESFUNC6:102

.= r * s1 by A11, EXTREAL1:1

.= (|.a.| to_power k) * s1 ;

|.a.| to_power k >= 0 by Th4, COMPLEX1:46;

then ||.(a * x).|| = ((|.a.| to_power k) to_power (1 / k)) * (s1 to_power (1 / k)) by A13, A15, A16, Th5

.= (|.a.| to_power (k * (1 / k))) * (s1 to_power (1 / k)) by COMPLEX1:46, HOLDER_1:2

.= (|.a.| to_power 1) * (s1 to_power (1 / k)) by XCMPLX_1:106 ;

hence ||.(a * x).|| = |.a.| * ||.x.|| by A11, POWER:25; :: thesis: verum