let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = dom (f + g) & Integral M,(|.(f + g).| | E) <= (Integral M,(|.f.| | E)) + (Integral M,(|.g.| | E)) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = dom (f + g) & Integral M,(|.(f + g).| | E) <= (Integral M,(|.f.| | E)) + (Integral M,(|.g.| | E)) )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = dom (f + g) & Integral M,(|.(f + g).| | E) <= (Integral M,(|.f.| | E)) + (Integral M,(|.g.| | E)) )
let f, g be PartFunc of X,COMPLEX ; :: thesis: ( f is_integrable_on M & g is_integrable_on M implies ex E being Element of S st
( E = dom (f + g) & Integral M,(|.(f + g).| | E) <= (Integral M,(|.f.| | E)) + (Integral M,(|.g.| | E)) ) )
assume B1: ( f is_integrable_on M & g is_integrable_on M ) ; :: thesis: ex E being Element of S st
( E = dom (f + g) & Integral M,(|.(f + g).| | E) <= (Integral M,(|.f.| | E)) + (Integral M,(|.g.| | E)) )
( Re f is_integrable_on M & Im f is_integrable_on M & Re g is_integrable_on M & Im g is_integrable_on M ) by B1, MESFUN6C:def 4;
then P1: ( R_EAL (Re f) is_integrable_on M & R_EAL (Im f) is_integrable_on M & R_EAL (Re g) is_integrable_on M & R_EAL (Im g) is_integrable_on M ) by MESFUNC6:def 9;
then consider A1 being Element of S such that
P2: ( A1 = dom (R_EAL (Re f)) & R_EAL (Re f) is_measurable_on A1 ) by MESFUNC5:def 17;
consider A2 being Element of S such that
P3: ( A2 = dom (R_EAL (Im f)) & R_EAL (Im f) is_measurable_on A2 ) by P1, MESFUNC5:def 17;
P4: ( A1 = dom f & A2 = dom f ) by P2, P3, MESFUN6C:def 1, MESFUN6C:def 2;
consider B1 being Element of S such that
Q2: ( B1 = dom (R_EAL (Re g)) & R_EAL (Re g) is_measurable_on B1 ) by P1, MESFUNC5:def 17;
consider B2 being Element of S such that
Q3: ( B2 = dom (R_EAL (Im g)) & R_EAL (Im g) is_measurable_on B2 ) by P1, MESFUNC5:def 17;
Q4: ( B1 = dom g & B2 = dom g ) by Q2, Q3, MESFUN6C:def 1, MESFUN6C:def 2;
reconsider A = A1 /\ B1 as Element of S ;
Q5: ( A c= A1 & A c= A2 & A c= B1 & A c= B2 ) by P4, Q4, XBOOLE_1:17;
( Re f is_measurable_on A1 & Im f is_measurable_on A2 ) by P2, P3, MESFUNC6:def 6;
then R6: ( Re f is_measurable_on A & Im f is_measurable_on A ) by P4, MESFUNC6:16, XBOOLE_1:17;
( Re g is_measurable_on B1 & Im g is_measurable_on B2 ) by Q2, Q3, MESFUNC6:def 6;
then ( Re g is_measurable_on A & Im g is_measurable_on A ) by Q4, MESFUNC6:16, XBOOLE_1:17;
then B2: ( f is_measurable_on A & g is_measurable_on A ) by R6, MESFUN6C:def 3;
then ( |.f.| is_measurable_on A & |.g.| is_measurable_on A ) by P4, Q4, MESFUN6C:30, XBOOLE_1:17;
then C1: |.f.| + |.g.| is_measurable_on A by MESFUNC6:26;
( |.f.| is_integrable_on M & |.g.| is_integrable_on M ) by B1, LEM7;
then A3: |.f.| + |.g.| is_integrable_on M by MESFUNC6:100;
A4: f + g is_integrable_on M by B1, MESFUN6C:33;
B3: ( dom (f + g) = (dom f) /\ (dom g) & dom (|.f.| + |.g.|) = (dom |.f.|) /\ (dom |.g.|) ) by VALUED_1:def 1;
then C2: ( A c= dom |.f.| & A c= dom |.g.| & dom |.(f + g).| = A ) by Q5, P4, Q4, VALUED_1:def 11;
then T3: (dom |.(f + g).|) /\ (dom (|.f.| + |.g.|)) = A by B3, XBOOLE_1:19, XBOOLE_1:28;
C3: |.(f + g).| is_measurable_on A by B3, P4, Q4, B2, MESFUN6C:11, MESFUN6C:30;
A5: |.(f + g).| is_integrable_on M by A4, LEM7;
for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x by Th21;
then (|.f.| + |.g.|) - |.(f + g).| is nonnegative by MES71;
then consider E being Element of S such that
A6: ( E = (dom (|.f.| + |.g.|)) /\ (dom |.(f + g).|) & Integral M,(|.(f + g).| | E) <= Integral M,((|.f.| + |.g.|) | E) ) by A3, A5, C1, C3, T3, MESFUN6C:42;
take E ; :: thesis: ( E = dom (f + g) & Integral M,(|.(f + g).| | E) <= (Integral M,(|.f.| | E)) + (Integral M,(|.g.| | E)) )
thus E = dom (f + g) by A6, B3, P4, Q4, C2, XBOOLE_1:19, XBOOLE_1:28; :: thesis: Integral M,(|.(f + g).| | E) <= (Integral M,(|.f.| | E)) + (Integral M,(|.g.| | E))
set F = |.f.|;
set G = |.g.|;
( |.f.| | E is_integrable_on M & |.g.| | E is_integrable_on M ) by B1, LEM7, MESFUNC6:91;
then consider E1 being Element of S such that
A7: ( E1 = (dom (|.f.| | E)) /\ (dom (|.g.| | E)) & Integral M,((|.f.| | E) + (|.g.| | E)) = (Integral M,((|.f.| | E) | E1)) + (Integral M,((|.g.| | E) | E1)) ) by MESFUNC6:101;
( dom (|.f.| | E) = E & dom (|.g.| | E) = E ) by A6, T3, C2, RELAT_1:91;
then ( (|.f.| | E) | E1 = |.f.| | E & (|.g.| | E) | E1 = |.g.| | E ) by A7, FUNCT_1:82;
hence Integral M,(|.(f + g).| | E) <= (Integral M,(|.f.| | E)) + (Integral M,(|.g.| | E)) by A6, A7, C2, T3, Th20; :: thesis: verum