let X be non empty set ; for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for A being Element of S st f is A -measurable & A c= dom f holds
|.f.| is A -measurable
let S be SigmaField of X; for f being PartFunc of X,COMPLEX
for A being Element of S st f is A -measurable & A c= dom f holds
|.f.| is A -measurable
let f be PartFunc of X,COMPLEX; for A being Element of S st f is A -measurable & A c= dom f holds
|.f.| is A -measurable
let A be Element of S; ( f is A -measurable & A c= dom f implies |.f.| is A -measurable )
assume that
A1:
f is A -measurable
and
A2:
A c= dom f
; |.f.| is A -measurable
A3:
dom (Im f) = dom f
by COMSEQ_3:def 4;
then A5:
|.(Im f).| to_power 2 is nonnegative
by Th26, MESFUNC6:52;
A6:
dom |.(Im f).| = dom (Im f)
by VALUED_1:def 11;
then A7:
dom (|.(Im f).| to_power 2) = dom f
by A3, Def4;
Im f is A -measurable
by A1;
then
|.(Im f).| is A -measurable
by A2, A3, MESFUNC6:48;
then A8:
|.(Im f).| to_power 2 is A -measurable
by A2, A6, A3, A4, Th29, MESFUNC6:52;
A9:
dom (Re f) = dom f
by COMSEQ_3:def 3;
then A12:
|.(Re f).| to_power 2 is nonnegative
by Th26, MESFUNC6:52;
set F = (|.(Re f).| to_power 2) + (|.(Im f).| to_power 2);
A13:
dom |.f.| = dom f
by VALUED_1:def 11;
A14:
dom |.(Re f).| = dom (Re f)
by VALUED_1:def 11;
then A15:
dom (|.(Re f).| to_power 2) = dom f
by A9, Def4;
A16:
dom ((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) = (dom (|.(Re f).| to_power 2)) /\ (dom (|.(Im f).| to_power 2))
by VALUED_1:def 1;
then A17:
dom |.f.| = dom (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2))
by A13, A15, A7, Def4;
now for x being object st x in dom |.f.| holds
|.f.| . x = (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . xlet x be
object ;
( x in dom |.f.| implies |.f.| . x = (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . x )assume A18:
x in dom |.f.|
;
|.f.| . x = (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . xthen
(|.(Re f).| to_power 2) . x = (|.(Re f).| . x) to_power 2
by A13, A15, Def4;
then
(|.(Re f).| to_power 2) . x = |.((Re f) . x).| to_power 2
by A14, A13, A9, A18, VALUED_1:def 11;
then
(|.(Re f).| to_power 2) . x = |.(Re (f . x)).| to_power 2
by A13, A9, A18, COMSEQ_3:def 3;
then
(|.(Re f).| to_power 2) . x = |.(Re (f . x)).| ^2
by POWER:46;
then A19:
(|.(Re f).| to_power 2) . x = (Re (f . x)) ^2
by COMPLEX1:75;
(|.(Im f).| to_power 2) . x = (|.(Im f).| . x) to_power 2
by A13, A7, A18, Def4;
then
(|.(Im f).| to_power 2) . x = |.((Im f) . x).| to_power 2
by A6, A13, A3, A18, VALUED_1:def 11;
then
(|.(Im f).| to_power 2) . x = |.(Im (f . x)).| to_power 2
by A13, A3, A18, COMSEQ_3:def 4;
then
(|.(Im f).| to_power 2) . x = |.(Im (f . x)).| ^2
by POWER:46;
then A20:
(|.(Im f).| to_power 2) . x = (Im (f . x)) ^2
by COMPLEX1:75;
(((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) . x) to_power (1 / 2) =
sqrt (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) . x)
by A12, A5, Th27, MESFUNC6:56
.=
sqrt (((Re (f . x)) ^2) + ((Im (f . x)) ^2))
by A13, A16, A15, A7, A18, A19, A20, VALUED_1:def 1
;
then
(((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . x = |.(f . x).|
by A17, A18, Def4;
hence
|.f.| . x = (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . x
by A18, VALUED_1:def 11;
verum end;
then A21:
|.f.| = ((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)
by A17, FUNCT_1:2;
Re f is A -measurable
by A1;
then
|.(Re f).| is A -measurable
by A2, A9, MESFUNC6:48;
then
|.(Re f).| to_power 2 is A -measurable
by A2, A14, A9, A10, Th29, MESFUNC6:52;
then
(|.(Re f).| to_power 2) + (|.(Im f).| to_power 2) is A -measurable
by A8, MESFUNC6:26;
hence
|.f.| is A -measurable
by A2, A12, A5, A16, A15, A7, A21, Th29, MESFUNC6:56; verum