let X be non empty set ; :: thesis: for f, g being PartFunc of X,COMPLEX holds
( Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) & Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) )
let f, g be PartFunc of X,COMPLEX ; :: thesis: ( Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) & Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) )
A0:
( dom (Re (f (#) g)) = dom (f (#) g) & dom (Im (f (#) g)) = dom (f (#) g) )
by MESFUN6C:def 1, MESFUN6C:def 2;
then A1:
( dom (Re (f (#) g)) = (dom f) /\ (dom g) & dom (Im (f (#) g)) = (dom f) /\ (dom g) )
by VALUED_1:def 4;
A2:
dom (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) = (dom ((Re f) (#) (Re g))) /\ (dom ((Im f) (#) (Im g)))
by VALUED_1:12;
B2:
dom (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) = (dom ((Im f) (#) (Re g))) /\ (dom ((Re f) (#) (Im g)))
by VALUED_1:def 1;
A3:
( dom ((Re f) (#) (Re g)) = (dom (Re f)) /\ (dom (Re g)) & dom ((Im f) (#) (Im g)) = (dom (Im f)) /\ (dom (Im g)) & dom ((Im f) (#) (Re g)) = (dom (Im f)) /\ (dom (Re g)) & dom ((Re f) (#) (Im g)) = (dom (Re f)) /\ (dom (Im g)) )
by VALUED_1:def 4;
A4:
( dom (Re f) = dom f & dom (Im f) = dom f & dom (Re g) = dom g & dom (Im g) = dom g )
by MESFUN6C:def 1, MESFUN6C:def 2;
now let x be
set ;
:: thesis: ( x in dom (Re (f (#) g)) implies (Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) . x )assume A5:
x in dom (Re (f (#) g))
;
:: thesis: (Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) . xthen
(Re (f (#) g)) . x = Re ((f (#) g) . x)
by MESFUN6C:def 1;
then
(Re (f (#) g)) . x = Re ((f . x) * (g . x))
by A0, A5, VALUED_1:def 4;
then A6:
(Re (f (#) g)) . x = ((Re (f . x)) * (Re (g . x))) - ((Im (f . x)) * (Im (g . x)))
by COMPLEX1:24;
(
x in dom f &
x in dom g )
by A1, A5, XBOOLE_0:def 4;
then
(
(Re f) . x = Re (f . x) &
(Im f) . x = Im (f . x) &
(Re g) . x = Re (g . x) &
(Im g) . x = Im (g . x) )
by A4, MESFUN6C:def 1, MESFUN6C:def 2;
then
(Re (f (#) g)) . x = (((Re f) (#) (Re g)) . x) - (((Im f) . x) * ((Im g) . x))
by A1, A3, A4, A5, A6, VALUED_1:def 4;
then
(Re (f (#) g)) . x = (((Re f) (#) (Re g)) . x) - (((Im f) (#) (Im g)) . x)
by A1, A3, A4, A5, VALUED_1:def 4;
hence
(Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) . x
by A4, A1, A2, A3, A5, VALUED_1:13;
:: thesis: verum end;
hence
Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g))
by A4, A1, A2, A3, FUNCT_1:9; :: thesis: Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g))
now let x be
set ;
:: thesis: ( x in dom (Im (f (#) g)) implies (Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) . x )assume P01:
x in dom (Im (f (#) g))
;
:: thesis: (Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) . xthen
(Im (f (#) g)) . x = Im ((f (#) g) . x)
by MESFUN6C:def 2;
then
(Im (f (#) g)) . x = Im ((f . x) * (g . x))
by A0, P01, VALUED_1:def 4;
then B6:
(Im (f (#) g)) . x = ((Im (f . x)) * (Re (g . x))) + ((Re (f . x)) * (Im (g . x)))
by COMPLEX1:24;
(
x in dom f &
x in dom g )
by P01, A1, XBOOLE_0:def 4;
then
(
(Re f) . x = Re (f . x) &
(Im f) . x = Im (f . x) &
(Re g) . x = Re (g . x) &
(Im g) . x = Im (g . x) )
by A4, MESFUN6C:def 1, MESFUN6C:def 2;
then
(Im (f (#) g)) . x = (((Im f) (#) (Re g)) . x) + (((Re f) . x) * ((Im g) . x))
by P01, A1, A4, A3, B6, VALUED_1:def 4;
then
(Im (f (#) g)) . x = (((Im f) (#) (Re g)) . x) + (((Re f) (#) (Im g)) . x)
by P01, A1, A4, A3, VALUED_1:def 4;
hence
(Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) . x
by A4, A1, B2, A3, P01, VALUED_1:def 1;
:: thesis: verum end;
hence
Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g))
by A1, B2, A3, A4, FUNCT_1:9; :: thesis: verum