:: Algebra of Complex Vector Valued Functions
:: by Noboru Endou
::
:: Received August 20, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

::
::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN TO THE SET OF COMPLEX NUMBERS
::
definition
let M be non empty set ;
let V be ComplexNormSpace;
let f1 be PartFunc of M,COMPLEX;
let f2 be PartFunc of M,V;
deffunc H1( Element of M) ->  Element of the U1 of V = (f1 /. $1) * (f2 /. $1);
defpred S1[ set ] means $1 in (dom f1) /\ (dom f2);
set X = (dom f1) /\ (dom f2);
funcf1 (#) f2 ->  PartFunc of M,V means :Def1: :: VFUNCT_2:def 1
( dom it = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom it holds
it /. c = (f1 /. c) * (f2 /. c) ) );
existence
 ex b1 being PartFunc of M,V st
( dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom b1 holds
b1 /. c = (f1 /. c) * (f2 /. c) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of M,V st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom b1 holds
b1 /. c = (f1 /. c) * (f2 /. c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom b2 holds
b2 /. c = (f1 /. c) * (f2 /. c) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines (#) VFUNCT_2:def_1_:_
 for M being non empty set
for V being ComplexNormSpace
for f1 being PartFunc of M,COMPLEX
for f2, b5 being PartFunc of M,V holds
( b5 = f1 (#) f2 iff ( dom b5 = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom b5 holds
b5 /. c = (f1 /. c) * (f2 /. c) ) ) );

definition
let X be non empty set ;
let V be ComplexNormSpace;
let f be PartFunc of X,V;
let z be Complex;
deffunc H1( Element of X) ->  Element of the U1 of V = z * (f /. $1);
defpred S1[ set ] means $1 in dom f;
set M = dom f;
funcz (#) f ->  PartFunc of X,V means :Def2: :: VFUNCT_2:def 2
( dom it = dom f & ( for x being Element of X st x in dom it holds
it /. x = z * (f /. x) ) );
existence
 ex b1 being PartFunc of X,V st
( dom b1 = dom f & ( for x being Element of X st x in dom b1 holds
b1 /. x = z * (f /. x) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of X,V st dom b1 = dom f & ( for x being Element of X st x in dom b1 holds
b1 /. x = z * (f /. x) ) & dom b2 = dom f & ( for x being Element of X st x in dom b2 holds
b2 /. x = z * (f /. x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines (#) VFUNCT_2:def_2_:_
 for X being non empty set
for V being ComplexNormSpace
for f being PartFunc of X,V
for z being Complex
for b5 being PartFunc of X,V holds
( b5 = z (#) f iff ( dom b5 = dom f & ( for x being Element of X st x in dom b5 holds
b5 /. x = z * (f /. x) ) ) );

theorem :: VFUNCT_2:1
for M being non empty set
for V being ComplexNormSpace
for f1 being PartFunc of M,COMPLEX
for f2 being PartFunc of M,V holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {(0. V)}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {(0. V)}))
proofend;

theorem :: VFUNCT_2:2
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V holds
( ||.f.|| " {0} = f " {(0. V)} & (- f) " {(0. V)} = f " {(0. V)} )
proofend;

theorem :: VFUNCT_2:3
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX st z <> 0c holds
(z (#) f) " {(0. V)} = f " {(0. V)}
proofend;

::
:: BASIC PROPERTIES OF OPERATIONS
::
theorem Th4: :: VFUNCT_2:4
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V holds f1 + f2 = f2 + f1
proofend;

definition
let M be non empty set ;
let V be ComplexNormSpace;
let f1, f2 be PartFunc of M,V;
:: original:+
redefine funcf1 + f2 ->  Element of K6(K7(M, the U1 of V));
commutativity
 for f1, f2 being PartFunc of M,V holds f1 + f2 = f2 + f1 by Th4;
end;

theorem :: VFUNCT_2:5
for M being non empty set
for V being ComplexNormSpace
for f1, f2, f3 being PartFunc of M,V holds (f1 + f2) + f3 = f1 + (f2 + f3)
proofend;

theorem :: VFUNCT_2:6
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,COMPLEX
for f3 being PartFunc of M,V holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
proofend;

theorem :: VFUNCT_2:7
for M being non empty set
for V being ComplexNormSpace
for f3 being PartFunc of M,V
for f1, f2 being PartFunc of M,COMPLEX holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3)
proofend;

theorem :: VFUNCT_2:8
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for f3 being PartFunc of M,COMPLEX holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2)
proofend;

theorem :: VFUNCT_2:9
for M being non empty set
for V being ComplexNormSpace
for f2 being PartFunc of M,V
for z being Element of COMPLEX
for f1 being PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = (z (#) f1) (#) f2
proofend;

theorem :: VFUNCT_2:10
for M being non empty set
for V being ComplexNormSpace
for f2 being PartFunc of M,V
for z being Element of COMPLEX
for f1 being PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = f1 (#) (z (#) f2)
proofend;

theorem :: VFUNCT_2:11
for M being non empty set
for V being ComplexNormSpace
for f3 being PartFunc of M,V
for f1, f2 being PartFunc of M,COMPLEX holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3)
proofend;

theorem :: VFUNCT_2:12
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for f3 being PartFunc of M,COMPLEX holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2)
proofend;

theorem :: VFUNCT_2:13
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for z being Element of COMPLEX holds z (#) (f1 + f2) = (z (#) f1) + (z (#) f2)
proofend;

theorem Th14: :: VFUNCT_2:14
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for z1, z2 being Element of COMPLEX holds (z1 * z2) (#) f = z1 (#) (z2 (#) f)
proofend;

theorem :: VFUNCT_2:15
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for z being Element of COMPLEX holds z (#) (f1 - f2) = (z (#) f1) - (z (#) f2)
proofend;

theorem :: VFUNCT_2:16
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V holds f1 - f2 = (- 1r) (#) (f2 - f1)
proofend;

theorem :: VFUNCT_2:17
for M being non empty set
for V being ComplexNormSpace
for f1, f2, f3 being PartFunc of M,V holds f1 - (f2 + f3) = (f1 - f2) - f3
proofend;

theorem Th18: :: VFUNCT_2:18
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V holds 1r (#) f = f
proofend;

theorem :: VFUNCT_2:19
for M being non empty set
for V being ComplexNormSpace
for f1, f2, f3 being PartFunc of M,V holds f1 - (f2 - f3) = (f1 - f2) + f3
proofend;

theorem :: VFUNCT_2:20
for M being non empty set
for V being ComplexNormSpace
for f1, f2, f3 being PartFunc of M,V holds f1 + (f2 - f3) = (f1 + f2) - f3
proofend;

theorem :: VFUNCT_2:21
for M being non empty set
for V being ComplexNormSpace
for f2 being PartFunc of M,V
for f1 being PartFunc of M,COMPLEX holds ||.(f1 (#) f2).|| = |.f1.| (#) ||.f2.||
proofend;

theorem :: VFUNCT_2:22
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX holds ||.(z (#) f).|| = |.z.| (#) ||.f.||
proofend;

theorem Th23: :: VFUNCT_2:23
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V holds - f = (- 1r) (#) f
proofend;

theorem Th24: :: VFUNCT_2:24
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V holds - (- f) = f
proofend;

theorem Th25: :: VFUNCT_2:25
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V holds f1 - f2 = f1 + (- f2)
proofend;

theorem :: VFUNCT_2:26
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V holds f1 - (- f2) = f1 + f2
proofend;

theorem Th27: :: VFUNCT_2:27
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X being set holds
( (f1 + f2) | X = (f1 | X) + (f2 | X) &amp; (f1 + f2) | X = (f1 | X) + f2 &amp; (f1 + f2) | X = f1 + (f2 | X) )
proofend;

theorem :: VFUNCT_2:28
for M being non empty set
for V being ComplexNormSpace
for f2 being PartFunc of M,V
for X being set
for f1 being PartFunc of M,COMPLEX holds
( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) &amp; (f1 (#) f2) | X = (f1 | X) (#) f2 &amp; (f1 (#) f2) | X = f1 (#) (f2 | X) )
proofend;

theorem Th29: :: VFUNCT_2:29
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for X being set holds
( (- f) | X = - (f | X) &amp; ||.f.|| | X = ||.(f | X).|| )
proofend;

theorem :: VFUNCT_2:30
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X being set holds
( (f1 - f2) | X = (f1 | X) - (f2 | X) &amp; (f1 - f2) | X = (f1 | X) - f2 &amp; (f1 - f2) | X = f1 - (f2 | X) )
proofend;

theorem :: VFUNCT_2:31
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX
for X being set holds (z (#) f) | X = z (#) (f | X)
proofend;

::
:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN TO COMPLEX
::
theorem Th32: :: VFUNCT_2:32
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V holds
( ( f1 is total &amp; f2 is total implies f1 + f2 is total ) &amp; ( f1 + f2 is total implies ( f1 is total &amp; f2 is total ) ) &amp; ( f1 is total &amp; f2 is total implies f1 - f2 is total ) &amp; ( f1 - f2 is total implies ( f1 is total &amp; f2 is total ) ) )
proofend;

theorem Th33: :: VFUNCT_2:33
for M being non empty set
for V being ComplexNormSpace
for f2 being PartFunc of M,V
for f1 being PartFunc of M,COMPLEX holds
( ( f1 is total &amp; f2 is total ) iff f1 (#) f2 is total )
proofend;

theorem Th34: :: VFUNCT_2:34
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX holds
( f is total iff z (#) f is total )
proofend;

theorem Th35: :: VFUNCT_2:35
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V holds
( f is total iff - f is total )
proofend;

theorem Th36: :: VFUNCT_2:36
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V holds
( f is total iff ||.f.|| is total )
proofend;

theorem :: VFUNCT_2:37
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for x being Element of M st f1 is total &amp; f2 is total holds
( (f1 + f2) /. x = (f1 /. x) + (f2 /. x) &amp; (f1 - f2) /. x = (f1 /. x) - (f2 /. x) )
proofend;

theorem :: VFUNCT_2:38
for M being non empty set
for V being ComplexNormSpace
for f2 being PartFunc of M,V
for f1 being PartFunc of M,COMPLEX
for x being Element of M st f1 is total &amp; f2 is total holds
(f1 (#) f2) /. x = (f1 /. x) * (f2 /. x)
proofend;

theorem :: VFUNCT_2:39
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX
for x being Element of M st f is total holds
(z (#) f) /. x = z * (f /. x)
proofend;

theorem :: VFUNCT_2:40
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for x being Element of M st f is total holds
( (- f) /. x = - (f /. x) &amp; ||.f.|| . x = ||.(f /. x).|| )
proofend;

::
:: BOUNDED AND CONSTANT PARTIAL FUNCTIONS
:: FROM A DOMAIN TO A NORMED COMPLEX SPACE
::
definition
let M be non empty set ;
let V be ComplexNormSpace;
let f be PartFunc of M,V;
let Y be set ;
predf is_bounded_on Y means :Def3: :: VFUNCT_2:def 3
 ex r being Real st
for x being Element of M st x in Y /\ (dom f) holds
||.(f /. x).|| <= r;
end;

:: deftheorem Def3 defines is_bounded_on VFUNCT_2:def_3_:_
 for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set holds
( f is_bounded_on Y iff ex r being Real st
for x being Element of M st x in Y /\ (dom f) holds
||.(f /. x).|| <= r );

theorem :: VFUNCT_2:41
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for Y, X being set st Y c= X &amp; f is_bounded_on X holds
f is_bounded_on Y
proofend;

theorem :: VFUNCT_2:42
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for X being set st X misses dom f holds
f is_bounded_on X
proofend;

theorem :: VFUNCT_2:43
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set holds 0c (#) f is_bounded_on Y
proofend;

theorem Th44: :: VFUNCT_2:44
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX
for Y being set st f is_bounded_on Y holds
z (#) f is_bounded_on Y
proofend;

theorem Th45: :: VFUNCT_2:45
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set st f is_bounded_on Y holds
( ||.f.|| | Y is bounded &amp; - f is_bounded_on Y )
proofend;

theorem Th46: :: VFUNCT_2:46
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X, Y being set st f1 is_bounded_on X &amp; f2 is_bounded_on Y holds
f1 + f2 is_bounded_on X /\ Y
proofend;

theorem :: VFUNCT_2:47
for M being non empty set
for V being ComplexNormSpace
for f2 being PartFunc of M,V
for X, Y being set
for f1 being PartFunc of M,COMPLEX st f1 | X is bounded &amp; f2 is_bounded_on Y holds
f1 (#) f2 is_bounded_on X /\ Y
proofend;

theorem :: VFUNCT_2:48
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X, Y being set st f1 is_bounded_on X &amp; f2 is_bounded_on Y holds
f1 - f2 is_bounded_on X /\ Y
proofend;

theorem :: VFUNCT_2:49
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for X, Y being set st f is_bounded_on X &amp; f is_bounded_on Y holds
f is_bounded_on X \/ Y
proofend;

theorem :: VFUNCT_2:50
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X, Y being set st f1 | X is constant &amp; f2 | Y is constant holds
( (f1 + f2) | (X /\ Y) is constant &amp; (f1 - f2) | (X /\ Y) is constant )
proofend;

theorem :: VFUNCT_2:51
for M being non empty set
for V being ComplexNormSpace
for f2 being PartFunc of M,V
for X, Y being set
for f1 being PartFunc of M,COMPLEX st f1 | X is constant &amp; f2 | Y is constant holds
(f1 (#) f2) | (X /\ Y) is constant
proofend;

theorem Th52: :: VFUNCT_2:52
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Element of COMPLEX
for Y being set st f | Y is constant holds
(z (#) f) | Y is constant
proofend;

theorem Th53: :: VFUNCT_2:53
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set st f | Y is constant holds
( ||.f.|| | Y is constant &amp; (- f) | Y is constant )
proofend;

theorem Th54: :: VFUNCT_2:54
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set st f | Y is constant holds
f is_bounded_on Y
proofend;

theorem :: VFUNCT_2:55
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set st f | Y is constant holds
( ( for z being Element of COMPLEX holds z (#) f is_bounded_on Y ) &amp; - f is_bounded_on Y &amp; ||.f.|| | Y is bounded )
proofend;

theorem :: VFUNCT_2:56
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X, Y being set st f1 is_bounded_on X &amp; f2 | Y is constant holds
f1 + f2 is_bounded_on X /\ Y
proofend;

theorem :: VFUNCT_2:57
for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X, Y being set st f1 is_bounded_on X &amp; f2 | Y is constant holds
( f1 - f2 is_bounded_on X /\ Y &amp; f2 - f1 is_bounded_on X /\ Y )
proofend;