:: Algebra of Complex Vector Valued Functions
:: by Noboru Endou
::
:: Received August 20, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, CLVECT_1, PARTFUN1, XCMPLX_0, SUBSET_1, ARYTM_3,
ARYTM_1, RELAT_1, NUMBERS, VALUED_1, NORMSP_1, FUNCT_1, SUPINF_2, CARD_1,
TARSKI, COMPLEX1, VFUNCT_1, REAL_1, XXREAL_0, XXREAL_2, RLVECT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, FUNCT_1, RELSET_1, PARTFUN1, STRUCT_0, RLVECT_1, VALUED_1,
COMSEQ_2, COMPLEX1, NORMSP_0, CLVECT_1, XXREAL_0, VFUNCT_1;
constructors REAL_1, COMPLEX1, CLVECT_1, VALUED_1, RELSET_1, VFUNCT_1,
COMSEQ_2;
registrations RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, VALUED_0,
RFUNCT_1, XCMPLX_0;
requirements SUBSET, BOOLE, ARITHM, NUMERALS;
definitions TARSKI, PARTFUN1, XBOOLE_0;
equalities XBOOLE_0, RLVECT_1, VALUED_1;
expansions PARTFUN1, XBOOLE_0;
theorems TARSKI, SUBSET_1, FUNCT_1, ABSVALUE, PARTFUN1, PARTFUN2, RFUNCT_1,
RLVECT_1, RELAT_1, XREAL_0, XBOOLE_0, XBOOLE_1, CLVECT_1, COMPLEX1,
CFUNCT_1, XREAL_1, XXREAL_0, VALUED_1, NORMSP_0, VFUNCT_1;
schemes PARTFUN2;
begin
reserve M for non empty set;
reserve V for ComplexNormSpace;
reserve f,f1,f2,f3 for PartFunc of M,V;
reserve z,z1,z2 for Complex;
::
::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 F(Element of M) = (f1/.$1) * (f2/.$1);
defpred P[set] means $1 in dom f1 /\ dom f2;
set X = dom f1 /\ dom f2;
func f1(#)f2 -> PartFunc of M,V means
:Def1:
dom it = dom f1 /\ dom f2 &
for c be Element of M st c in dom it holds it/.c = (f1/.c) * (f2/.c);
existence
proof
consider F be PartFunc of M,V such that
A1: for c be Element of M holds c in dom F iff P[c] and
A2: for c be Element of M st c in dom F holds F/.c = F(c) from
PARTFUN2:sch 2;
take F;
thus dom F = dom f1 /\ dom f2 by A1,SUBSET_1:3;
let c be Element of M;
assume c in dom F;
hence thesis by A2;
end;
uniqueness
proof
thus for f,g being PartFunc of M,V st (dom f=X & for c be
Element of M st c in dom f holds f/.c = F(c)) & (dom g=X & for c be Element of
M st c in dom g holds g/.c = F(c)) holds f = g from PARTFUN2:sch 3;
end;
end;
definition
let X be non empty set;
let V be ComplexNormSpace;
let f be PartFunc of X,V;
let z be Complex;
deffunc F(Element of X) = z * (f/.$1);
defpred P[set] means $1 in dom f;
set M = dom f;
func z(#)f -> PartFunc of X,V means
:Def2:
dom it = dom f &
for x be Element of X st x in dom it holds it/.x = z * (f/.x);
existence
proof
consider F be PartFunc of X,V such that
A1: for x be Element of X holds x in dom F iff P[x] and
A2: for x be Element of X st x in dom F holds F/.x = F(x) from
PARTFUN2:sch 2;
take F;
thus dom F = dom f by A1,SUBSET_1:3;
let x be Element of X;
assume x in dom F;
hence thesis by A2;
end;
uniqueness
proof
thus for f,g being PartFunc of X,V st (dom f=M & for x be
Element of X st x in dom f holds f/.x = F(x)) & (dom g=M & for x be Element of
X st x in dom g holds g/.x = F(x)) holds f = g from PARTFUN2:sch 3;
end;
end;
theorem
for f1 be PartFunc of M,COMPLEX, f2 be PartFunc of M,V
holds dom (f1(#)f2) \ (f1(#)f2)"{0.V} = (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{
0.V})
proof
let f1 be PartFunc of M,COMPLEX;
let f2 be PartFunc of M,V;
thus dom (f1(#)f2) \ (f1(#)f2)"{0.V} c= (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2
)"{0.V})
proof
let x be object;
assume
A1: x in dom (f1(#)f2) \ (f1(#)f2)"{0.V};
then reconsider x1=x as Element of M;
A2: x in dom (f1(#)f2) by A1,XBOOLE_0:def 5;
then
A3: x1 in dom f1 /\ dom f2 by Def1;
not x in (f1(#)f2)"{0.V} by A1,XBOOLE_0:def 5;
then not (f1(#)f2)/.x1 in {0.V} by A2,PARTFUN2:26;
then (f1(#)f2)/.x1 <> 0.V by TARSKI:def 1;
then
A4: (f1/.x1) * (f2/.x1) <> 0.V by A2,Def1;
then (f1/.x1) <> 0c by CLVECT_1:1;
then
A5: not f1/.x1 in {0} by TARSKI:def 1;
(f2/.x1) <> 0.V by A4,CLVECT_1:1;
then not (f2/.x1) in {0.V} by TARSKI:def 1;
then
A6: not x1 in (f2)"{0.V} by PARTFUN2:26;
x1 in dom f2 by A3,XBOOLE_0:def 4;
then
A7: x in dom f2 \ (f2)"{0.V} by A6,XBOOLE_0:def 5;
x1 in dom f1 by A3,XBOOLE_0:def 4;
then not f1.x1 in {0} by A5,PARTFUN1:def 6;
then
A8: not x1 in (f1)"{0} by FUNCT_1:def 7;
x1 in dom f1 by A3,XBOOLE_0:def 4;
then x in dom f1 \ (f1)"{0} by A8,XBOOLE_0:def 5;
hence thesis by A7,XBOOLE_0:def 4;
end;
thus (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0.V}) c= dom (f1(#)f2) \ (f1(#)
f2)"{0.V}
proof
let x be object;
assume
A9: x in (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0.V});
then reconsider x1=x as Element of M;
A10: x in dom f1 \ (f1)"{0} by A9,XBOOLE_0:def 4;
then
A11: x in dom f1 by XBOOLE_0:def 5;
not x in (f1)"{0} by A10,XBOOLE_0:def 5;
then not f1.x1 in {0} by A11,FUNCT_1:def 7;
then f1.x1 <> 0 by TARSKI:def 1;
then
A12: f1/.x1 <> 0 by A11,PARTFUN1:def 6;
A13: x in dom f2 \ (f2)"{0.V} by A9,XBOOLE_0:def 4;
then
A14: x in dom f2 by XBOOLE_0:def 5;
then x1 in dom f1 /\ dom f2 by A11,XBOOLE_0:def 4;
then
A15: x1 in dom (f1(#)f2) by Def1;
not x in (f2)"{0.V} by A13,XBOOLE_0:def 5;
then not (f2/.x1) in {0.V} by A14,PARTFUN2:26;
then (f2/.x1) <> 0.V by TARSKI:def 1;
then f1/.x1 * (f2/.x1) <>0.V by A12,CLVECT_1:2;
then (f1(#)f2)/.x1 <> 0.V by A15,Def1;
then not (f1(#)f2)/.x1 in {0.V} by TARSKI:def 1;
then not x in (f1(#)f2)"{0.V} by PARTFUN2:26;
hence thesis by A15,XBOOLE_0:def 5;
end;
end;
theorem
(||.f.||)"{0} = f"{0.V} & (-f)"{0.V} = f"{0.V}
proof
now
let c be Element of M;
thus c in (||.f.||)"{0} implies c in f"{0.V}
proof
assume
A1: c in (||.f.||)"{0};
then
A2: c in dom (||.f.||) by FUNCT_1:def 7;
(||.f.||).c in {0} by A1,FUNCT_1:def 7;
then (||.f.||).c = 0 by TARSKI:def 1;
then ||.f/.c.|| = 0 by A2,NORMSP_0:def 3;
then f/.c = 0.V by NORMSP_0:def 5;
then
A3: f/.c in {0.V} by TARSKI:def 1;
c in dom f by A2,NORMSP_0:def 3;
hence thesis by A3,PARTFUN2:26;
end;
assume
A4: c in (f)"{0.V};
then c in dom f by PARTFUN2:26;
then
A5: c in dom (||.f.||) by NORMSP_0:def 3;
f/.c in {0.V} by A4,PARTFUN2:26;
then f/.c = 0.V by TARSKI:def 1;
then ||.f/.c.|| = 0 by NORMSP_0:def 6;
then (||.f.||).c = 0 by A5,NORMSP_0:def 3;
then (||.f.||).c in {0} by TARSKI:def 1;
hence c in (||.f.||)"{0} by A5,FUNCT_1:def 7;
end;
hence (||.f.||)"{0} = f"{0.V} by SUBSET_1:3;
now
let c be Element of M;
thus c in (-f)"{0.V} implies c in f"{0.V}
proof
assume
A6: c in (-f)"{0.V};
then
A7: c in dom (-f) by PARTFUN2:26;
(-f)/.c in {0.V} by A6,PARTFUN2:26;
then (-f)/.c = 0.V by TARSKI:def 1;
then --(f/.c) = -0.V by A7,VFUNCT_1:def 5;
then --(f/.c) = 0.V by RLVECT_1:12;
then f/.c = 0.V by RLVECT_1:17;
then
A8: f/.c in {0.V} by TARSKI:def 1;
c in dom f by A7,VFUNCT_1:def 5;
hence thesis by A8,PARTFUN2:26;
end;
assume
A9: c in (f)"{0.V};
then c in dom f by PARTFUN2:26;
then
A10: c in dom (-f) by VFUNCT_1:def 5;
f/.c in {0.V} by A9,PARTFUN2:26;
then f/.c = 0.V by TARSKI:def 1;
then (-f)/.c = -0.V by A10,VFUNCT_1:def 5;
then (-f)/.c = 0.V by RLVECT_1:12;
then (-f)/.c in {0.V} by TARSKI:def 1;
hence c in (-f)"{0.V} by A10,PARTFUN2:26;
end;
hence thesis by SUBSET_1:3;
end;
theorem
z<>0c implies (z(#)f)"{0.V} = f"{0.V}
proof
assume
A1: z<>0c;
now
let x be Element of M;
thus x in (z(#)f)"{0.V} implies x in f"{0.V}
proof
assume
A2: x in (z(#)f)"{0.V};
then
A3: x in dom (z(#)f) by PARTFUN2:26;
(z(#)f)/.x in {0.V} by A2,PARTFUN2:26;
then (z(#)f)/.x = 0.V by TARSKI:def 1;
then z*f/.x = 0.V by A3,Def2;
then z*f/.x = z*0.V by CLVECT_1:1;
then f/.x = 0.V by A1,CLVECT_1:11;
then
A4: f/.x in {0.V} by TARSKI:def 1;
x in dom f by A3,Def2;
hence thesis by A4,PARTFUN2:26;
end;
assume
A5: x in (f)"{0.V};
then x in dom f by PARTFUN2:26;
then
A6: x in dom (z(#)f) by Def2;
f/.x in {0.V} by A5,PARTFUN2:26;
then z*f/.x = z*0.V by TARSKI:def 1;
then z*f/.x = 0.V by CLVECT_1:1;
then (z(#)f)/.x = 0.V by A6,Def2;
then (z(#)f)/.x in {0.V} by TARSKI:def 1;
hence x in (z(#)f)"{0.V} by A6,PARTFUN2:26;
end;
hence thesis by SUBSET_1:3;
end;
::
:: BASIC PROPERTIES OF OPERATIONS
::
theorem Th4:
f1 + f2 = f2 + f1;
definition
let M,V; let f1,f2;
redefine func f1+f2; :: redefines + (VFUNCT_1, definition)
commutativity by Th4;
end;
theorem
(f1 + f2) + f3 = f1 + (f2 + f3)
proof
A1: dom (f1 + f2 + f3) = dom (f1 + f2) /\ dom f3 by VFUNCT_1:def 1
.= dom f1 /\ dom f2 /\ dom f3 by VFUNCT_1:def 1
.= dom f1 /\ (dom f2 /\ dom f3) by XBOOLE_1:16
.= dom f1 /\ dom (f2 + f3) by VFUNCT_1:def 1
.= dom (f1 + (f2 + f3)) by VFUNCT_1:def 1;
now
let x be Element of M;
assume
A2: x in dom (f1 + f2 + f3);
then x in dom (f1 + f2) /\ dom f3 by VFUNCT_1:def 1;
then
A3: x in dom (f1 + f2) by XBOOLE_0:def 4;
x in dom f1 /\ dom (f2 + f3) by A1,A2,VFUNCT_1:def 1;
then
A4: x in dom (f2 + f3) by XBOOLE_0:def 4;
thus (f1 + f2 + f3)/.x = ((f1 + f2)/.x) + (f3/.x) by A2,VFUNCT_1:def 1
.= (f1/.x) + (f2/.x) + (f3/.x) by A3,VFUNCT_1:def 1
.= (f1/.x) + ((f2/.x) + (f3/.x)) by RLVECT_1:def 3
.= (f1/.x) + ((f2 + f3)/.x) by A4,VFUNCT_1:def 1
.= (f1 + (f2 + f3))/.x by A1,A2,VFUNCT_1:def 1;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for f1,f2 be PartFunc of M,COMPLEX,f3 be PartFunc of M,V
holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
proof
let f1,f2 be PartFunc of M,COMPLEX;
let f3 be PartFunc of M,V;
A1: dom (f1 (#) f2 (#) f3) = dom (f1 (#) f2) /\ dom f3 by Def1
.= dom f1 /\ dom f2 /\ dom f3 by VALUED_1:def 4
.= dom f1 /\ (dom f2 /\ dom f3) by XBOOLE_1:16
.= dom f1 /\ dom (f2 (#) f3) by Def1
.= dom (f1 (#) (f2 (#) f3)) by Def1;
now
let x be Element of M;
assume
A2: x in dom (f1(#)f2(#)f3);
then x in dom (f1 (#) f2) /\ dom f3 by Def1;
then
A3: x in dom (f1 (#) f2) by XBOOLE_0:def 4;
A4: dom (f1 (#) f2) = dom f1 /\ dom f2 by VALUED_1:def 4;
then x in dom f1 by A3,XBOOLE_0:def 4;
then
A5: f1.x = f1/.x by PARTFUN1:def 6;
x in dom f2 by A3,A4,XBOOLE_0:def 4;
then
A6: f2.x = f2/.x by PARTFUN1:def 6;
A7: (f1 (#) f2)/.x = (f1 (#) f2).x by A3,PARTFUN1:def 6
.= f1/.x * f2/.x by A3,A5,A6,VALUED_1:def 4;
x in dom f1 /\ dom (f2(#)f3) by A1,A2,Def1;
then
A8: x in dom (f2 (#) f3) by XBOOLE_0:def 4;
thus (f1 (#) f2 (#) f3)/.x = (f1 (#) f2)/.x * (f3/.x) by A2,Def1
.= f1/.x * (f2/.x * (f3/.x)) by A7,CLVECT_1:def 4
.= f1/.x * ((f2 (#) f3)/.x) by A8,Def1
.= (f1 (#) (f2 (#) f3))/.x by A1,A2,Def1;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for f1,f2 be PartFunc of M,COMPLEX holds
(f1 + f2) (#) f3 = f1 (#) f3 + f2 (#) f3
proof
let f1,f2 be PartFunc of M,COMPLEX;
A1: dom ((f1 + f2) (#) f3) = dom (f1 + f2) /\ dom f3 by Def1
.= dom f1 /\ dom f2 /\ (dom f3 /\ dom f3) by VALUED_1:def 1
.= dom f1 /\ dom f2 /\ dom f3 /\ dom f3 by XBOOLE_1:16
.= dom f1 /\ dom f3 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom f1 /\ dom f3 /\ (dom f2 /\ dom f3) by XBOOLE_1:16
.= dom (f1 (#) f3) /\ (dom f2 /\ dom f3) by Def1
.= dom (f1 (#) f3) /\ dom (f2 (#) f3) by Def1
.= dom (f1 (#) f3 + f2 (#) f3) by VFUNCT_1:def 1;
A2: dom (f1 + f2) = dom f1 /\ dom f2 by VALUED_1:def 1;
now
let x be Element of M;
assume
A3: x in dom ((f1 + f2)(#)f3);
then
A4: x in dom (f1(#)f3) /\ dom (f2(#)f3) by A1,VFUNCT_1:def 1;
then
A5: x in dom (f1(#)f3) by XBOOLE_0:def 4;
x in dom (f1 + f2) /\ dom f3 by A3,Def1;
then
A6: x in dom (f1 + f2) by XBOOLE_0:def 4;
then x in dom f1 by A2,XBOOLE_0:def 4;
then
A7: f1/.x = f1.x by PARTFUN1:def 6;
x in dom f2 by A2,A6,XBOOLE_0:def 4;
then
A8: f2/.x = f2.x by PARTFUN1:def 6;
A9: (f1 + f2)/.x = (f1 + f2).x by A6,PARTFUN1:def 6
.= f1/.x + f2/.x by A6,A7,A8,VALUED_1:def 1;
A10: x in dom (f2 (#) f3) by A4,XBOOLE_0:def 4;
thus ((f1 + f2) (#) f3)/.x = (f1 + f2)/.x * (f3/.x) by A3,Def1
.= f1/.x * (f3/.x) + f2/.x * (f3/.x) by A9,CLVECT_1:def 3
.= ((f1 (#) f3)/.x) + f2/.x* (f3/.x) by A5,Def1
.= ((f1 (#) f3)/.x) + ((f2 (#) f3)/.x) by A10,Def1
.= ((f1 (#) f3) + (f2 (#) f3))/.x by A1,A3,VFUNCT_1:def 1;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for f3 be PartFunc of M,COMPLEX holds f3(#)(f1 + f2) = f3(#)f1 + f3(#) f2
proof
let f3 be PartFunc of M,COMPLEX;
A1: dom (f3 (#) (f1 + f2)) = dom f3 /\ dom (f1 + f2) by Def1
.= dom f3 /\ (dom f1 /\ dom f2) by VFUNCT_1:def 1
.= dom f3 /\ dom f3 /\ dom f1 /\ dom f2 by XBOOLE_1:16
.= dom f3 /\ dom f1 /\ dom f3 /\ dom f2 by XBOOLE_1:16
.= dom f3 /\ dom f1 /\ (dom f3 /\ dom f2) by XBOOLE_1:16
.= dom (f3 (#) f1) /\ (dom f3 /\ dom f2) by Def1
.= dom (f3 (#) f1) /\ dom (f3 (#) f2) by Def1
.= dom (f3 (#) f1 + f3 (#) f2) by VFUNCT_1:def 1;
now
let x be Element of M;
assume
A2: x in dom (f3(#)(f1 + f2));
then x in dom f3 /\ dom (f1 + f2) by Def1;
then
A3: x in dom (f1 + f2) by XBOOLE_0:def 4;
A4: x in dom (f3(#)f1) /\ dom (f3(#)f2) by A1,A2,VFUNCT_1:def 1;
then
A5: x in dom (f3(#)f1) by XBOOLE_0:def 4;
A6: x in dom (f3 (#) f2) by A4,XBOOLE_0:def 4;
thus (f3 (#) (f1 + f2))/.x = f3/.x * ((f1 + f2)/.x) by A2,Def1
.= f3/.x * ((f1/.x) + (f2/.x)) by A3,VFUNCT_1:def 1
.= f3/.x * (f1/.x) + f3/.x * (f2/.x) by CLVECT_1:def 2
.= ((f3 (#) f1)/.x) + f3/.x* (f2/.x) by A5,Def1
.= ((f3 (#) f1)/.x) + ((f3 (#) f2)/.x) by A6,Def1
.= ((f3 (#) f1) + (f3 (#) f2))/.x by A1,A2,VFUNCT_1:def 1;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for f1 be PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = z (#) f1 (#) f2
proof
let f1 be PartFunc of M,COMPLEX;
A1: dom (f1 (#) f2) = dom f1 /\ dom f2 by Def1;
A2: dom (z(#)(f1 (#) f2)) = dom (f1 (#) f2) by Def2
.= dom (z(#)f1) /\ dom f2 by A1,VALUED_1:def 5
.= dom (z(#)f1(#)f2) by Def1;
now
let x be Element of M;
assume
A3: x in dom (z(#)(f1(#)f2));
then x in dom (z(#)f1) /\ dom f2 by A2,Def1;
then x in dom (z(#)f1) by XBOOLE_0:def 4;
then
A4: (z(#)f1)/.x = (z(#)f1).x by PARTFUN1:def 6;
A5: x in dom (f1(#)f2) by A3,Def2;
then x in dom f1 by A1,XBOOLE_0:def 4;
then
A6: f1/.x = f1.x by PARTFUN1:def 6;
thus (z(#)(f1(#)f2))/.x = z * ((f1(#)f2)/.x) by A3,Def2
.= z*(f1/.x * (f2/.x)) by A5,Def1
.= (z*f1/.x) * (f2/.x) by CLVECT_1:def 4
.= (z(#)f1)/.x * (f2/.x) by A4,A6,VALUED_1:6
.= (z(#)f1 (#) f2)/.x by A2,A3,Def1;
end;
hence thesis by A2,PARTFUN2:1;
end;
theorem
for f1 be PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = f1 (#) (z (#) f2)
proof
let f1 be PartFunc of M,COMPLEX;
A1: dom (z(#)(f1 (#) f2)) = dom (f1 (#) f2) by Def2
.= dom f1 /\ dom f2 by Def1
.= dom f1 /\ dom (z(#)f2) by Def2
.= dom (f1(#)(z(#)f2)) by Def1;
now
let x be Element of M;
assume
A2: x in dom (z(#)(f1(#)f2));
then
A3: x in dom (f1(#)f2) by Def2;
x in dom f1 /\ dom (z(#)f2) by A1,A2,Def1;
then
A4: x in dom (z(#)f2) by XBOOLE_0:def 4;
thus (z(#)(f1(#)f2))/.x = z * (f1(#)f2)/.x by A2,Def2
.= z * (f1/.x * (f2/.x)) by A3,Def1
.= f1/.x * z * (f2/.x) by CLVECT_1:def 4
.= f1/.x * (z * (f2/.x)) by CLVECT_1:def 4
.= f1/.x * ((z(#)f2)/.x) by A4,Def2
.= (f1(#)(z(#)f2))/.x by A1,A2,Def1;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for f1,f2 be PartFunc of M,COMPLEX holds (f1 - f2) (#) f3 = f1(#)f3 - f2(#)f3
proof
let f1,f2 be PartFunc of M,COMPLEX;
A1: dom ((f1 - f2) (#) f3) = dom (f1 + -f2) /\ dom f3 by Def1
.= dom f1 /\ dom (-f2) /\ (dom f3 /\ dom f3) by VALUED_1:def 1
.= dom f1 /\ dom f2 /\ (dom f3 /\ dom f3) by VALUED_1:8
.= dom f1 /\ dom f2 /\ dom f3 /\ dom f3 by XBOOLE_1:16
.= dom f1 /\ dom f3 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom f1 /\ dom f3 /\ (dom f2 /\ dom f3) by XBOOLE_1:16
.= dom (f1 (#) f3) /\ (dom f2 /\ dom f3) by Def1
.= dom (f1 (#) f3) /\ dom (f2 (#) f3) by Def1
.= dom (f1 (#) f3 - f2 (#) f3) by VFUNCT_1:def 2;
now
let x be Element of M;
assume
A2: x in dom ((f1 - f2)(#)f3);
then
A3: x in dom (f1(#)f3) /\ dom (f2(#)f3) by A1,VFUNCT_1:def 2;
then
A4: x in dom (f1(#)f3) by XBOOLE_0:def 4;
x in dom (f1 - f2) /\ dom f3 by A2,Def1;
then
A5: x in dom (f1 - f2) by XBOOLE_0:def 4;
then
A6: x in dom f1 /\ dom (-f2) by VALUED_1:def 1;
then
A7: x in dom (-f2) by XBOOLE_0:def 4;
x in dom f1 by A6,XBOOLE_0:def 4;
then
A8: f1/.x = f1.x by PARTFUN1:def 6;
(f1 + -f2)/.x = (f1 + -f2).x by A5,PARTFUN1:def 6;
then
A9: (f1 + -f2)/.x = f1.x + (-f2).x by A5,VALUED_1:def 1
.= f1/.x + (-f2)/.x by A7,A8,PARTFUN1:def 6;
dom -f2 = dom f2 by VALUED_1:8;
then
A10: (-f2).x = -(f2.x) & f2/.x = f2.x by A7,PARTFUN1:def 6,VALUED_1:8;
A11: x in dom (f2 (#) f3) by A3,XBOOLE_0:def 4;
(-f2)/.x = (-f2).x by A7,PARTFUN1:def 6;
hence ((f1 - f2) (#) f3)/.x = (f1/.x - f2/.x) * (f3/.x) by A2,A10,A9,Def1
.= f1/.x * (f3/.x) - f2/.x * (f3/.x) by CLVECT_1:10
.= ((f1 (#) f3)/.x) - f2/.x * (f3/.x) by A4,Def1
.= ((f1 (#) f3)/.x) - ((f2 (#) f3)/.x) by A11,Def1
.= ((f1 (#) f3) - (f2 (#) f3))/.x by A1,A2,VFUNCT_1:def 2;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for f3 be PartFunc of M,COMPLEX holds f3(#)f1 - f3(#)f2 = f3(#)(f1 - f2)
proof
let f3 be PartFunc of M,COMPLEX;
A1: dom (f3 (#) f1 - f3 (#) f2) = dom (f3 (#) f1) /\ dom (f3 (#) f2)
by VFUNCT_1:def 2
.= dom (f3 (#) f1) /\ (dom f3 /\ dom f2) by Def1
.= dom f3 /\ dom f1 /\ (dom f3 /\ dom f2) by Def1
.= dom f3 /\ (dom f3 /\ dom f1) /\ dom f2 by XBOOLE_1:16
.= dom f3 /\ dom f3 /\ dom f1 /\ dom f2 by XBOOLE_1:16
.= dom f3 /\ (dom f1 /\ dom f2) by XBOOLE_1:16
.= dom f3 /\ dom (f1 - f2) by VFUNCT_1:def 2
.= dom (f3(#)(f1 - f2)) by Def1;
now
let x be Element of M;
assume
A2: x in dom (f3(#)(f1 - f2));
then x in dom f3 /\ dom (f1 - f2) by Def1;
then
A3: x in dom (f1 - f2) by XBOOLE_0:def 4;
A4: x in dom (f3(#)f1) /\ dom (f3(#)f2) by A1,A2,VFUNCT_1:def 2;
then
A5: x in dom (f3(#)f1) by XBOOLE_0:def 4;
A6: x in dom (f3 (#) f2) by A4,XBOOLE_0:def 4;
thus (f3 (#) (f1 - f2))/.x = f3/.x * ((f1 - f2)/.x) by A2,Def1
.= f3/.x * ((f1/.x) - (f2/.x)) by A3,VFUNCT_1:def 2
.= f3/.x * (f1/.x) - f3/.x * (f2/.x) by CLVECT_1:9
.= ((f3 (#) f1)/.x) - f3/.x * (f2/.x) by A5,Def1
.= ((f3 (#) f1)/.x) - ((f3 (#) f2)/.x) by A6,Def1
.= ((f3 (#) f1) - (f3 (#) f2))/.x by A1,A2,VFUNCT_1:def 2;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
z(#)(f1 + f2) = z(#)f1 + z(#)f2
proof
A1: dom (z(#)(f1 + f2)) = dom (f1 + f2) by Def2
.= dom f1 /\ dom f2 by VFUNCT_1:def 1
.= dom f1 /\ dom (z(#)f2) by Def2
.= dom (z(#)f1) /\ dom (z(#)f2) by Def2
.= dom (z(#)f1 + z(#)f2) by VFUNCT_1:def 1;
now
let x be Element of M;
assume
A2: x in dom (z(#)(f1 + f2));
then
A3: x in dom (f1 + f2) by Def2;
A4: x in dom (z(#)f1) /\ dom (z(#)f2) by A1,A2,VFUNCT_1:def 1;
then
A5: x in dom (z(#)f1) by XBOOLE_0:def 4;
A6: x in dom (z(#)f2) by A4,XBOOLE_0:def 4;
thus (z(#)(f1 + f2))/.x = z * ((f1 + f2)/.x) by A2,Def2
.= z * ((f1/.x) + (f2/.x)) by A3,VFUNCT_1:def 1
.= z * (f1/.x) + z * (f2/.x) by CLVECT_1:def 2
.= ((z(#)f1)/.x) + z * (f2/.x) by A5,Def2
.= ((z(#)f1)/.x) + ((z(#)f2)/.x) by A6,Def2
.= (z(#)f1 + z(#)f2)/.x by A1,A2,VFUNCT_1:def 1;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem Th14:
(z1*z2)(#)f = z1(#)(z2(#)f)
proof
A1: dom ((z1*z2) (#) f) = dom f by Def2
.= dom (z2(#)f) by Def2
.= dom (z1(#)(z2(#)f)) by Def2;
now
let x be Element of M;
assume
A2: x in dom ((z1*z2)(#)f);
then
A3: x in dom (z2(#)f) by A1,Def2;
thus ((z1*z2)(#)f)/.x = z1*z2 * f/.x by A2,Def2
.= z1*(z2 * f/.x) by CLVECT_1:def 4
.= z1 * ((z2(#)f)/.x) by A3,Def2
.= (z1(#)(z2(#)f))/.x by A1,A2,Def2;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
z(#)(f1 - f2) = z(#)f1 - z(#)f2
proof
A1: dom (z(#)(f1 - f2)) = dom (f1 - f2) by Def2
.= dom f1 /\ dom f2 by VFUNCT_1:def 2
.= dom f1 /\ dom (z(#)f2) by Def2
.= dom (z(#)f1) /\ dom (z(#)f2) by Def2
.= dom (z(#)f1 - z(#)f2) by VFUNCT_1:def 2;
now
let x be Element of M;
assume
A2: x in dom (z(#)(f1 - f2));
then
A3: x in dom (f1 - f2) by Def2;
A4: x in dom (z(#)f1) /\ dom (z(#)f2) by A1,A2,VFUNCT_1:def 2;
then
A5: x in dom (z(#)f1) by XBOOLE_0:def 4;
A6: x in dom (z(#)f2) by A4,XBOOLE_0:def 4;
thus (z(#)(f1 - f2))/.x = z * ((f1 - f2)/.x) by A2,Def2
.= z * ((f1/.x) - (f2/.x)) by A3,VFUNCT_1:def 2
.= z * (f1/.x) - z * (f2/.x) by CLVECT_1:9
.= ((z(#)f1)/.x) - z * (f2/.x) by A5,Def2
.= ((z(#)f1)/.x) - ((z(#)f2)/.x) by A6,Def2
.= (z(#)f1 - z(#)f2)/.x by A1,A2,VFUNCT_1:def 2;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
f1-f2 = (-1r)(#)(f2-f1)
proof
A1: dom (f1 - f2) = dom f2 /\ dom f1 by VFUNCT_1:def 2
.= dom (f2 - f1) by VFUNCT_1:def 2
.= dom ((-1r)(#)(f2 - f1)) by Def2;
now
A2: dom (f1 - f2) = dom f2 /\ dom f1 by VFUNCT_1:def 2
.= dom (f2 - f1) by VFUNCT_1:def 2;
let x be Element of M such that
A3: x in dom (f1-f2);
thus (f1 - f2)/.x = (f1/.x) - (f2/.x) by A3,VFUNCT_1:def 2
.= -((f2/.x) - (f1/.x)) by RLVECT_1:33
.= (-1r)*((f2/.x) - (f1/.x)) by CLVECT_1:3
.= (-1r)*((f2 - f1)/.x) by A3,A2,VFUNCT_1:def 2
.= ((-1r)(#)(f2 - f1))/.x by A1,A3,Def2;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
f1 - (f2 + f3) = f1 - f2 - f3
proof
A1: dom (f1 - (f2 + f3)) = dom f1 /\ dom (f2 + f3) by VFUNCT_1:def 2
.= dom f1 /\ (dom f2 /\ dom f3) by VFUNCT_1:def 1
.= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom (f1 - f2) /\ dom f3 by VFUNCT_1:def 2
.= dom (f1 - f2 - f3) by VFUNCT_1:def 2;
now
let x be Element of M;
assume
A2: x in dom (f1 - (f2 + f3));
then x in dom f1 /\ dom (f2 + f3) by VFUNCT_1:def 2;
then
A3: x in dom (f2 + f3) by XBOOLE_0:def 4;
x in dom (f1 - f2) /\ dom f3 by A1,A2,VFUNCT_1:def 2;
then
A4: x in dom (f1 - f2) by XBOOLE_0:def 4;
thus (f1 - (f2 + f3))/.x = (f1/.x) - ((f2 + f3)/.x) by A2,VFUNCT_1:def 2
.= (f1/.x) - ((f2/.x) + (f3/.x)) by A3,VFUNCT_1:def 1
.= (f1/.x) - (f2/.x) - (f3/.x) by RLVECT_1:27
.= ((f1 - f2)/.x) - (f3/.x) by A4,VFUNCT_1:def 2
.= (f1 - f2 - f3)/.x by A1,A2,VFUNCT_1:def 2;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem Th18:
1r(#)f = f
proof
A1: now
let c be Element of M;
assume c in dom (1r(#)f);
hence (1r(#)f)/.c = 1r * f/.c by Def2
.= f/.c by CLVECT_1:def 5;
end;
dom (1r(#)f) = dom f by Def2;
hence thesis by A1,PARTFUN2:1;
end;
theorem
f1 - (f2 - f3) = f1 - f2 + f3
proof
A1: dom (f1 - (f2 - f3)) = dom f1 /\ dom (f2 - f3) by VFUNCT_1:def 2
.= dom f1 /\ (dom f2 /\ dom f3) by VFUNCT_1:def 2
.= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom (f1 - f2) /\ dom f3 by VFUNCT_1:def 2
.= dom (f1 - f2 + f3) by VFUNCT_1:def 1;
now
let c be Element of M;
assume
A2: c in dom (f1 - (f2 - f3));
then c in dom f1 /\ dom (f2 - f3) by VFUNCT_1:def 2;
then
A3: c in dom (f2 - f3) by XBOOLE_0:def 4;
c in dom (f1 - f2) /\ dom f3 by A1,A2,VFUNCT_1:def 1;
then
A4: c in dom (f1 - f2) by XBOOLE_0:def 4;
thus (f1 - (f2 - f3))/.c = (f1/.c) - ((f2 - f3)/.c) by A2,VFUNCT_1:def 2
.= (f1/.c) - ((f2/.c) - (f3/.c)) by A3,VFUNCT_1:def 2
.= (f1/.c) - (f2/.c) + (f3/.c) by RLVECT_1:29
.= ((f1 - f2)/.c) + (f3/.c) by A4,VFUNCT_1:def 2
.= (f1 - f2 + f3)/.c by A1,A2,VFUNCT_1:def 1;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
f1 + (f2 - f3) = f1 + f2 - f3
proof
A1: dom (f1 + (f2 - f3)) = dom f1 /\ dom (f2 - f3) by VFUNCT_1:def 1
.= dom f1 /\ (dom f2 /\ dom f3) by VFUNCT_1:def 2
.= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom (f1 + f2) /\ dom f3 by VFUNCT_1:def 1
.= dom (f1 + f2 - f3) by VFUNCT_1:def 2;
now
let c be Element of M;
assume
A2: c in dom (f1 + (f2 - f3));
then c in dom f1 /\ dom (f2 - f3) by VFUNCT_1:def 1;
then
A3: c in dom (f2 - f3) by XBOOLE_0:def 4;
c in dom (f1 + f2) /\ dom f3 by A1,A2,VFUNCT_1:def 2;
then
A4: c in dom (f1 + f2) by XBOOLE_0:def 4;
thus (f1 + (f2 - f3))/.c = (f1/.c) + ((f2 - f3)/.c) by A2,VFUNCT_1:def 1
.= (f1/.c) + ((f2/.c) - (f3/.c)) by A3,VFUNCT_1:def 2
.= (f1/.c) + (f2/.c) - (f3/.c) by RLVECT_1:def 3
.= ((f1 + f2)/.c) - (f3/.c) by A4,VFUNCT_1:def 1
.= (f1 + f2 - f3)/.c by A1,A2,VFUNCT_1:def 2;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
for f1 be PartFunc of M,COMPLEX holds ||.f1(#)f2.|| = |.f1.|(#)||.f2 .||
proof
let f1 be PartFunc of M,COMPLEX;
A1: dom (f1 (#) f2) = dom f1 /\ dom f2 by Def1;
A2: dom f1 /\ dom f2 = dom f1 /\ dom (||.f2.||) by NORMSP_0:def 3
.= dom (|.f1.|) /\ dom (||.f2.||) by VALUED_1:def 11
.= dom (|.f1.|(#)||.f2.||) by VALUED_1:def 4;
A3: dom (||.f1 (#) f2.||) = dom (f1 (#) f2) by NORMSP_0:def 3;
now
let c be Element of M;
assume
A4: c in dom (||.f1 (#) f2.||);
then c in dom (|.f1.|) /\ dom (||.f2.||) by A3,A1,A2,VALUED_1:def 4;
then
A5: c in dom (||.f2.||) by XBOOLE_0:def 4;
A6: c in dom (f1 (#) f2) by A4,NORMSP_0:def 3;
then c in dom f1 by A1,XBOOLE_0:def 4;
then
A7: f1/.c = f1.c by PARTFUN1:def 6;
thus (||.f1(#)f2.||).c = ||.(f1(#)f2)/.c.|| by A4,NORMSP_0:def 3
.= ||.f1/.c * (f2/.c).|| by A6,Def1
.= |.(f1/.c).| * ||.(f2/.c).|| by CLVECT_1:def 13
.= ((|.f1.|).c) * ||.(f2/.c).|| by A7,VALUED_1:18
.= ((|.f1.|).c) * (||.f2.||).c by A5,NORMSP_0:def 3
.= (|.f1.|(#)||.f2.||).c by VALUED_1:5;
end;
hence thesis by A3,A1,A2,PARTFUN1:5;
end;
theorem
||.z(#)f.|| = |.z.|(#)||.f.||
proof
A1: dom (||.z(#)f.||) = dom (z(#)f) by NORMSP_0:def 3
.= dom f by Def2
.= dom (||.f.||) by NORMSP_0:def 3
.= dom (|.z.|(#)||.f.||) by VALUED_1:def 5;
now
let c be Element of M;
assume
A2: c in dom (||.z(#)f.||);
then
A3: c in dom (||.f.||) by A1,VALUED_1:def 5;
A4: c in dom (z(#)f) by A2,NORMSP_0:def 3;
thus (||.z(#)f.||).c = ||.(z(#)f)/.c.|| by A2,NORMSP_0:def 3
.=||.z*(f/.c).|| by A4,Def2
.=|.z.|*||.f/.c.|| by CLVECT_1:def 13
.=|.z.|*(||.f.||.c) by A3,NORMSP_0:def 3
.=(|.z.|(#)||.f.||).c by A1,A2,VALUED_1:def 5;
end;
hence thesis by A1,PARTFUN1:5;
end;
theorem Th23:
-f = (-1r)(#)f
proof
A1: dom (-f) = dom f by VFUNCT_1:def 5
.= dom ((-1r)(#)f) by Def2;
now
let c be Element of M;
assume
A2: c in dom ((-1r)(#)f);
hence (-f)/.c = -(f/.c) by A1,VFUNCT_1:def 5
.= (-1r) * f/.c by CLVECT_1:3
.= ((-1r)(#)f)/.c by A2,Def2;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem Th24:
-(-f) = f
proof
thus -(-f) = (-1r)(#)(-f) by Th23
.= (-1r)(#)((-1r)(#)f) by Th23
.= ((-1r)*(-1r))(#)f by Th14
.= f by Th18,COMPLEX1:def 4;
end;
theorem Th25:
f1 - f2 = f1 + -f2
proof
A1: dom (f1 - f2) = dom f1 /\ dom f2 by VFUNCT_1:def 2
.= dom f1 /\ dom (-f2) by VFUNCT_1:def 5
.= dom (f1 + -f2) by VFUNCT_1:def 1;
now
let c be Element of M;
assume
A2: c in dom (f1+-f2);
then c in dom f1 /\ dom (-f2) by VFUNCT_1:def 1;
then
A3: c in dom (-f2) by XBOOLE_0:def 4;
thus (f1 + -f2)/.c = (f1/.c) + ((-f2)/.c) by A2,VFUNCT_1:def 1
.= (f1/.c) - (f2/.c) by A3,VFUNCT_1:def 5
.= (f1-f2)/.c by A1,A2,VFUNCT_1:def 2;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
f1 - (-f2) = f1 + f2
proof
thus f1 - (-f2) = f1 + (-(-f2)) by Th25
.= f1 + f2 by Th24;
end;
reserve X,Y for set;
theorem Th27:
(f1+f2)|X = f1|X + f2|X & (f1+f2)|X = f1|X + f2 & (f1+f2)|X = f1 + f2|X
proof
A1: now
let c be Element of M;
assume
A2: c in dom ((f1+f2)|X);
then
A3: c in dom (f1+f2) /\ X by RELAT_1:61;
then
A4: c in X by XBOOLE_0:def 4;
A5: c in dom (f1+f2) by A3,XBOOLE_0:def 4;
then
A6: c in dom f1 /\ dom f2 by VFUNCT_1:def 1;
then c in dom f2 by XBOOLE_0:def 4;
then c in dom f2 /\ X by A4,XBOOLE_0:def 4;
then
A7: c in dom (f2|X) by RELAT_1:61;
c in dom f1 by A6,XBOOLE_0:def 4;
then c in dom f1 /\ X by A4,XBOOLE_0:def 4;
then
A8: c in dom (f1|X) by RELAT_1:61;
then c in dom (f1|X) /\ dom (f2|X) by A7,XBOOLE_0:def 4;
then
A9: c in dom ((f1|X) + (f2|X)) by VFUNCT_1:def 1;
thus ((f1+f2)|X)/.c = (f1+f2)/.c by A2,PARTFUN2:15
.= (f1/.c) + (f2/.c) by A5,VFUNCT_1:def 1
.= ((f1|X)/.c) + (f2/.c) by A8,PARTFUN2:15
.= ((f1|X)/.c) + ((f2|X)/.c) by A7,PARTFUN2:15
.= ((f1|X)+(f2|X))/.c by A9,VFUNCT_1:def 1;
end;
dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ (X /\ X) by VFUNCT_1:def 1
.= dom f1 /\ (dom f2 /\ (X /\ X)) by XBOOLE_1:16
.= dom f1 /\ (dom f2 /\ X /\ X) by XBOOLE_1:16
.= dom f1 /\ (X /\ dom (f2|X)) by RELAT_1:61
.= dom f1 /\ X /\ dom (f2|X) by XBOOLE_1:16
.= dom (f1|X) /\ dom (f2|X) by RELAT_1:61
.= dom ((f1|X)+(f2|X)) by VFUNCT_1:def 1;
hence (f1+f2)|X = f1|X + f2|X by A1,PARTFUN2:1;
A10: now
let c be Element of M;
assume
A11: c in dom ((f1+f2)|X);
then
A12: c in dom (f1+f2) /\ X by RELAT_1:61;
then
A13: c in X by XBOOLE_0:def 4;
A14: c in dom (f1+f2) by A12,XBOOLE_0:def 4;
then
A15: c in dom f1 /\ dom f2 by VFUNCT_1:def 1;
then c in dom f1 by XBOOLE_0:def 4;
then c in dom f1 /\ X by A13,XBOOLE_0:def 4;
then
A16: c in dom (f1|X) by RELAT_1:61;
c in dom f2 by A15,XBOOLE_0:def 4;
then c in dom (f1|X) /\ dom f2 by A16,XBOOLE_0:def 4;
then
A17: c in dom ((f1|X) + f2) by VFUNCT_1:def 1;
thus ((f1+f2)|X)/.c = (f1+f2)/.c by A11,PARTFUN2:15
.= (f1/.c) + (f2/.c) by A14,VFUNCT_1:def 1
.= ((f1|X)/.c) +(f2/.c) by A16,PARTFUN2:15
.= ((f1|X)+f2)/.c by A17,VFUNCT_1:def 1;
end;
dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ X by VFUNCT_1:def 1
.= dom f1 /\ X /\ dom f2 by XBOOLE_1:16
.= dom (f1|X) /\ dom f2 by RELAT_1:61
.= dom ((f1|X)+ f2) by VFUNCT_1:def 1;
hence (f1+f2)|X = f1|X + f2 by A10,PARTFUN2:1;
A18: now
let c be Element of M;
assume
A19: c in dom ((f1+f2)|X);
then
A20: c in dom (f1+f2) /\ X by RELAT_1:61;
then
A21: c in X by XBOOLE_0:def 4;
A22: c in dom (f1+f2) by A20,XBOOLE_0:def 4;
then
A23: c in dom f1 /\ dom f2 by VFUNCT_1:def 1;
then c in dom f2 by XBOOLE_0:def 4;
then c in dom f2 /\ X by A21,XBOOLE_0:def 4;
then
A24: c in dom (f2|X) by RELAT_1:61;
c in dom f1 by A23,XBOOLE_0:def 4;
then c in dom f1 /\ dom (f2|X) by A24,XBOOLE_0:def 4;
then
A25: c in dom (f1 + (f2|X)) by VFUNCT_1:def 1;
thus ((f1+f2)|X)/.c = (f1+f2)/.c by A19,PARTFUN2:15
.= (f1/.c) +(f2/.c) by A22,VFUNCT_1:def 1
.= (f1/.c) + ((f2|X)/.c) by A24,PARTFUN2:15
.= (f1+(f2|X))/.c by A25,VFUNCT_1:def 1;
end;
dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ X by VFUNCT_1:def 1
.= dom f1 /\ (dom f2 /\ X) by XBOOLE_1:16
.= dom f1 /\ dom (f2|X) by RELAT_1:61
.= dom (f1 + (f2|X)) by VFUNCT_1:def 1;
hence thesis by A18,PARTFUN2:1;
end;
theorem
for f1 be PartFunc of M,COMPLEX holds (f1(#)f2)|X = f1|X (#) f2|X & (
f1(#)f2)|X = f1|X (#) f2 & (f1(#)f2)|X = f1 (#) f2|X
proof
let f1 be PartFunc of M,COMPLEX;
A1: now
let c be Element of M;
assume
A2: c in dom ((f1(#)f2)|X);
then
A3: c in dom (f1(#)f2) /\ X by RELAT_1:61;
then
A4: c in X by XBOOLE_0:def 4;
A5: c in dom (f1(#)f2) by A3,XBOOLE_0:def 4;
then
A6: c in dom f1 /\ dom f2 by Def1;
then
A7: c in dom f1 by XBOOLE_0:def 4;
then c in dom f1 /\ X by A4,XBOOLE_0:def 4;
then
A8: c in dom (f1|X) by RELAT_1:61;
then
A9: (f1|X)/.c = (f1|X).c by PARTFUN1:def 6
.= f1.c by A8,FUNCT_1:47
.= f1/.c by A7,PARTFUN1:def 6;
c in dom f2 by A6,XBOOLE_0:def 4;
then c in dom f2 /\ X by A4,XBOOLE_0:def 4;
then
A10: c in dom (f2|X) by RELAT_1:61;
then c in dom (f1|X) /\ dom (f2|X) by A8,XBOOLE_0:def 4;
then
A11: c in dom ((f1|X) (#) (f2|X)) by Def1;
thus ((f1(#)f2)|X)/.c = (f1(#)f2)/.c by A2,PARTFUN2:15
.= (f1/.c) * (f2/.c) by A5,Def1
.= ((f1|X)/.c) * ((f2|X)/.c) by A10,A9,PARTFUN2:15
.= ((f1|X)(#)(f2|X))/.c by A11,Def1;
end;
dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ (X /\ X) by Def1
.= dom f1 /\ (dom f2 /\ (X /\ X)) by XBOOLE_1:16
.= dom f1 /\ (dom f2 /\ X /\ X) by XBOOLE_1:16
.= dom f1 /\ (X /\ dom (f2|X)) by RELAT_1:61
.= dom f1 /\ X /\ dom (f2|X) by XBOOLE_1:16
.= dom (f1|X) /\ dom (f2|X) by RELAT_1:61
.= dom ((f1|X)(#)(f2|X)) by Def1;
hence (f1(#)f2)|X = f1|X (#) f2|X by A1,PARTFUN2:1;
A12: now
let c be Element of M;
assume
A13: c in dom ((f1(#)f2)|X);
then
A14: c in dom (f1(#)f2) /\ X by RELAT_1:61;
then
A15: c in dom (f1(#)f2) by XBOOLE_0:def 4;
then
A16: c in dom f1 /\ dom f2 by Def1;
then
A17: c in dom f1 by XBOOLE_0:def 4;
c in X by A14,XBOOLE_0:def 4;
then c in dom f1 /\ X by A17,XBOOLE_0:def 4;
then
A18: c in dom (f1|X) by RELAT_1:61;
then
A19: (f1|X)/.c = (f1|X).c by PARTFUN1:def 6
.= f1.c by A18,FUNCT_1:47;
c in dom f2 by A16,XBOOLE_0:def 4;
then c in dom (f1|X) /\ dom f2 by A18,XBOOLE_0:def 4;
then
A20: c in dom ((f1|X) (#) f2) by Def1;
thus ((f1(#)f2)|X)/.c = (f1(#)f2)/.c by A13,PARTFUN2:15
.= (f1/.c) * (f2/.c) by A15,Def1
.= ((f1|X)/.c) * (f2/.c) by A17,A19,PARTFUN1:def 6
.= ((f1|X)(#)f2)/.c by A20,Def1;
end;
dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ X by Def1
.= dom f1 /\ X /\ dom f2 by XBOOLE_1:16
.= dom (f1|X) /\ dom f2 by RELAT_1:61
.= dom ((f1|X)(#) f2) by Def1;
hence (f1(#)f2)|X = f1|X (#) f2 by A12,PARTFUN2:1;
A21: now
let c be Element of M;
assume
A22: c in dom ((f1(#)f2)|X);
then
A23: c in dom (f1(#)f2) /\ X by RELAT_1:61;
then
A24: c in X by XBOOLE_0:def 4;
A25: c in dom (f1(#)f2) by A23,XBOOLE_0:def 4;
then
A26: c in dom f1 /\ dom f2 by Def1;
then c in dom f2 by XBOOLE_0:def 4;
then c in dom f2 /\ X by A24,XBOOLE_0:def 4;
then
A27: c in dom (f2|X) by RELAT_1:61;
c in dom f1 by A26,XBOOLE_0:def 4;
then c in dom f1 /\ dom (f2|X) by A27,XBOOLE_0:def 4;
then
A28: c in dom (f1 (#) (f2|X)) by Def1;
thus ((f1(#)f2)|X)/.c = (f1(#)f2)/.c by A22,PARTFUN2:15
.= (f1/.c) * (f2/.c) by A25,Def1
.= (f1/.c) * ((f2|X)/.c) by A27,PARTFUN2:15
.= (f1(#)(f2|X))/.c by A28,Def1;
end;
dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ X by Def1
.= dom f1 /\ (dom f2 /\ X) by XBOOLE_1:16
.= dom f1 /\ dom (f2|X) by RELAT_1:61
.= dom (f1 (#) (f2|X)) by Def1;
hence thesis by A21,PARTFUN2:1;
end;
theorem Th29:
(-f)|X = -(f|X) & (||.f.||)|X = ||.(f|X).||
proof
A1: now
let c be Element of M;
assume
A2: c in dom ((-f)|X);
then
A3: c in dom (-f) /\ X by RELAT_1:61;
then
A4: c in X by XBOOLE_0:def 4;
A5: c in dom (-f) by A3,XBOOLE_0:def 4;
then c in dom f by VFUNCT_1:def 5;
then c in dom f /\ X by A4,XBOOLE_0:def 4;
then
A6: c in dom (f|X) by RELAT_1:61;
then
A7: c in dom (-(f|X)) by VFUNCT_1:def 5;
thus ((-f)|X)/.c = (-f)/.c by A2,PARTFUN2:15
.= -(f/.c) by A5,VFUNCT_1:def 5
.= -((f|X)/.c) by A6,PARTFUN2:15
.= (-(f|X))/.c by A7,VFUNCT_1:def 5;
end;
dom ((-f)|X) = dom (-f) /\ X by RELAT_1:61
.= dom f /\ X by VFUNCT_1:def 5
.= dom (f|X) by RELAT_1:61
.= dom (-(f|X)) by VFUNCT_1:def 5;
hence (-f)|X = -(f|X) by A1,PARTFUN2:1;
A8: dom ((||.f.||)|X) = dom (||.f.||) /\ X by RELAT_1:61
.= dom f /\ X by NORMSP_0:def 3
.= dom (f|X) by RELAT_1:61
.= dom (||.(f|X).||) by NORMSP_0:def 3;
now
let c be Element of M;
assume
A9: c in dom ((||.f.||)|X);
then
A10: c in dom (f|X) by A8,NORMSP_0:def 3;
c in dom (||.f.||) /\ X by A9,RELAT_1:61;
then
A11: c in dom (||.f.||) by XBOOLE_0:def 4;
thus ((||.f.||)|X).c = (||.f.||).c by A9,FUNCT_1:47
.= ||.f/.c.|| by A11,NORMSP_0:def 3
.= ||.(f|X)/.c.|| by A10,PARTFUN2:15
.= (||.(f|X).||).c by A8,A9,NORMSP_0:def 3;
end;
hence thesis by A8,PARTFUN1:5;
end;
theorem
(f1-f2)|X = f1|X - f2|X & (f1-f2)|X = f1|X - f2 &(f1-f2)|X = f1 - f2|X
proof
thus (f1-f2)|X = (f1+-f2)|X by Th25
.= (f1|X)+ (-f2)|X by Th27
.= (f1|X)+ -(f2|X) by Th29
.= (f1|X) - (f2|X) by Th25;
thus (f1-f2)|X = (f1+-f2)|X by Th25
.= (f1|X)+ -f2 by Th27
.= (f1|X) - f2 by Th25;
thus (f1-f2)|X = (f1+-f2)|X by Th25
.= f1+ (-f2)|X by Th27
.= f1 +- (f2|X) by Th29
.= f1 - (f2|X) by Th25;
end;
theorem
(z(#)f)|X = z(#)(f|X)
proof
A1: now
let c be Element of M;
assume
A2: c in dom ((z(#)f)|X);
then
A3: c in dom (z(#)f) /\ X by RELAT_1:61;
then
A4: c in X by XBOOLE_0:def 4;
A5: c in dom (z(#)f) by A3,XBOOLE_0:def 4;
then c in dom f by Def2;
then c in dom f /\ X by A4,XBOOLE_0:def 4;
then
A6: c in dom (f|X) by RELAT_1:61;
then
A7: c in dom (z(#)(f|X)) by Def2;
thus ((z(#)f)|X)/.c = (z(#)f)/.c by A2,PARTFUN2:15
.= z*(f/.c) by A5,Def2
.= z*((f|X)/.c) by A6,PARTFUN2:15
.= (z(#)(f|X))/.c by A7,Def2;
end;
dom ((z(#)f)|X) = dom (z(#)f) /\ X by RELAT_1:61
.= dom f /\ X by Def2
.= dom (f|X) by RELAT_1:61
.= dom (z(#)(f|X)) by Def2;
hence thesis by A1,PARTFUN2:1;
end;
::
:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN TO COMPLEX
::
theorem Th32:
(f1 is total & f2 is total iff f1+f2 is total) & (f1 is total &
f2 is total iff f1-f2 is total)
proof
thus f1 is total & f2 is total iff f1+f2 is total
proof
thus f1 is total & f2 is total implies f1+f2 is total
proof
assume f1 is total & f2 is total;
then dom f1 = M & dom f2 = M;
hence dom (f1+f2) = M /\ M by VFUNCT_1:def 1
.= M;
end;
assume f1+f2 is total;
then dom (f1+f2) = M;
then dom f1 /\ dom f2 = M by VFUNCT_1:def 1;
then M c= dom f1 & M c= dom f2 by XBOOLE_1:17;
hence dom f1 = M & dom f2 = M;
end;
thus f1 is total & f2 is total iff f1-f2 is total
proof
thus f1 is total & f2 is total implies f1-f2 is total
proof
assume f1 is total & f2 is total;
then dom f1 = M & dom f2 = M;
hence dom (f1-f2) = M /\ M by VFUNCT_1:def 2
.= M;
end;
assume f1-f2 is total;
then dom (f1-f2) = M;
then dom f1 /\ dom f2 = M by VFUNCT_1:def 2;
then M c= dom f1 & M c= dom f2 by XBOOLE_1:17;
hence dom f1 = M & dom f2 = M;
end;
end;
theorem Th33:
for f1 be PartFunc of M,COMPLEX holds (f1 is total & f2 is total
iff f1(#)f2 is total)
proof
let f1 be PartFunc of M,COMPLEX;
thus f1 is total & f2 is total implies f1(#)f2 is total
proof
assume f1 is total & f2 is total;
then dom f1 = M & dom f2 = M;
hence dom (f1(#)f2) = M /\ M by Def1
.= M;
end;
assume f1(#)f2 is total;
then dom (f1(#)f2) = M;
then dom f1 /\ dom f2 = M by Def1;
then M c= dom f1 & M c= dom f2 by XBOOLE_1:17;
hence dom f1 = M & dom f2 = M;
end;
theorem Th34:
f is total iff z(#)f is total
by Def2;
theorem Th35:
f is total iff -f is total
proof
thus f is total implies -f is total
proof
assume
A1: f is total;
-f = (-1r)(#)f by Th23;
hence thesis by A1,Th34;
end;
assume
A2: -f is total;
-f = (-1r)(#)f by Th23;
hence thesis by A2,Th34;
end;
theorem Th36:
f is total iff ||.f.|| is total
by NORMSP_0:def 3;
theorem
for x be Element of M st f1 is total & f2 is total holds (f1+f2)/.x =
(f1/.x) + (f2/.x) & (f1-f2)/.x = (f1/.x) - (f2/.x)
proof
let x be Element of M;
assume
A1: f1 is total & f2 is total;
then f1+f2 is total by Th32;
then dom (f1+f2) = M;
hence (f1+f2)/.x = (f1/.x) + (f2/.x) by VFUNCT_1:def 1;
f1-f2 is total by A1,Th32;
then dom (f1-f2) = M;
hence thesis by VFUNCT_1:def 2;
end;
theorem
for f1 be PartFunc of M,COMPLEX, x be Element of M holds f1 is total &
f2 is total implies (f1(#)f2)/.x = f1/.x * (f2/.x)
proof
let f1 be PartFunc of M,COMPLEX;
let x be Element of M;
assume f1 is total & f2 is total;
then f1(#)f2 is total by Th33;
then dom (f1(#)f2) = M;
hence thesis by Def1;
end;
theorem
for x be Element of M st f is total holds (z(#)f)/.x = z * (f/.x)
proof
let x be Element of M;
assume f is total;
then z(#)f is total by Th34;
then dom (z(#)f) = M;
hence thesis by Def2;
end;
theorem
for x be Element of M st f is total holds (-f)/.x = - f/.x & (||.f.||)
.x = ||. f/.x .||
proof
let x be Element of M;
assume
A1: f is total;
then -f is total by Th35;
then dom (-f) = M;
hence (-f)/.x = - f/.x by VFUNCT_1:def 5;
||.f.|| is total by A1,Th36;
then dom (||.f.||) = M;
hence thesis by NORMSP_0:def 3;
end;
::
:: BOUNDED AND CONSTANT PARTIAL FUNCTIONS
:: FROM A DOMAIN TO A NORMED COMPLEX SPACE
::
definition
let M;
let V;
let f,Y;
pred f is_bounded_on Y means
ex r be Real st for x be Element of M st
x in Y /\ dom f holds ||.f/.x.|| <= r;
end;
theorem
Y c= X & f is_bounded_on X implies f is_bounded_on Y
proof
assume that
A1: Y c= X and
A2: f is_bounded_on X;
consider r be Real such that
A3: for x be Element of M st x in X /\ dom f holds ||.f/.x.|| <= r by A2;
take r;
let x be Element of M;
assume x in Y /\ dom f;
then x in Y & x in dom f by XBOOLE_0:def 4;
then x in X /\ dom f by A1,XBOOLE_0:def 4;
hence thesis by A3;
end;
theorem
X misses dom f implies f is_bounded_on X
proof
assume X /\ dom f = {};
then for x be Element of M holds x in X /\ dom f implies ||.f/.x.|| <= 0;
hence thesis;
end;
theorem
0c(#)f is_bounded_on Y
proof
now
take p=0;
let c be Element of M;
|.0c.|*||.f/.c.|| <= 0 by COMPLEX1:44;
then
A1: ||.0c*(f/.c).|| <= 0 by CLVECT_1:def 13;
assume c in Y /\ dom (0c(#)f);
then c in dom (0c(#)f) by XBOOLE_0:def 4;
hence ||.(0c(#)f)/.c.|| <= p by A1,Def2;
end;
hence thesis;
end;
theorem Th44:
f is_bounded_on Y implies z(#)f is_bounded_on Y
proof
assume f is_bounded_on Y;
then consider r1 be Real such that
A1: for c be Element of M st c in Y /\ dom f holds ||.f/.c.|| <= r1;
reconsider p = |.z.|*|.r1.| as Real;
take p;
let c be Element of M;
assume
A2: c in Y /\ dom (z(#)f);
then
A3: c in Y by XBOOLE_0:def 4;
A4: c in dom (z(#)f) by A2,XBOOLE_0:def 4;
then c in dom f by Def2;
then c in Y /\ dom f by A3,XBOOLE_0:def 4;
then
A5: ||.f/.c.|| <= r1 by A1;
r1 <= |.r1.| by ABSVALUE:4;
then |.z.| >= 0 & ||.f/.c.|| <= |.r1.| by A5,COMPLEX1:46,XXREAL_0:2;
then |.z.| * ||.(f/.c).|| <= |.z.|*|.r1.| by XREAL_1:64;
then ||.z * (f/.c).|| <= p by CLVECT_1:def 13;
hence thesis by A4,Def2;
end;
theorem Th45:
f is_bounded_on Y implies ||.f.|||Y is bounded & -f is_bounded_on Y
proof
assume
A1: f is_bounded_on Y;
then consider r1 be Real such that
A2: for c be Element of M st c in Y /\ dom f holds ||.f/.c.|| <= r1;
now
let c be object;
assume
A3: c in Y /\ dom (||.f.||);
then
A4: c in Y by XBOOLE_0:def 4;
A5: c in dom (||.f.||) by A3,XBOOLE_0:def 4;
then c in dom f by NORMSP_0:def 3;
then c in Y /\ dom f by A4,XBOOLE_0:def 4;
then ||.f/.c.|| >= 0 & ||.f/.c.|| <= r1 by A2,CLVECT_1:105;
then |.||.f/.c.||.| <= r1 by ABSVALUE:def 1;
hence |.(||.f.||).c.| <= r1 by A5,NORMSP_0:def 3;
end;
hence ||.f.|||Y is bounded by RFUNCT_1:73;
(-1r)(#)f is_bounded_on Y by A1,Th44;
hence thesis by Th23;
end;
theorem Th46:
f1 is_bounded_on X & f2 is_bounded_on Y implies f1+f2 is_bounded_on (X /\ Y)
proof
assume that
A1: f1 is_bounded_on X and
A2: f2 is_bounded_on Y;
consider r1 be Real such that
A3: for c be Element of M st c in X /\ dom f1 holds ||.(f1/.c).|| <= r1
by A1;
consider r2 be Real such that
A4: for c be Element of M st c in Y /\ dom f2 holds ||.(f2/.c).|| <= r2
by A2;
take r=r1+r2;
let c be Element of M;
assume
A5: c in X /\ Y /\ dom (f1+f2);
then
A6: c in X /\ Y by XBOOLE_0:def 4;
then
A7: c in Y by XBOOLE_0:def 4;
A8: c in dom (f1+f2) by A5,XBOOLE_0:def 4;
then
A9: c in dom f1 /\ dom f2 by VFUNCT_1:def 1;
then c in dom f2 by XBOOLE_0:def 4;
then c in Y /\ dom f2 by A7,XBOOLE_0:def 4;
then
A10: ||.(f2/.c).|| <= r2 by A4;
A11: c in X by A6,XBOOLE_0:def 4;
c in dom f1 by A9,XBOOLE_0:def 4;
then c in X /\ dom f1 by A11,XBOOLE_0:def 4;
then ||.(f1/.c).|| <= r1 by A3;
then ||.(f1/.c) + (f2/.c).|| <= ||.(f1/.c).|| + ||.f2/.c.|| & ||.(f1/.c).||
+ ||. (f2/.c).|| <= r by A10,CLVECT_1:def 13,XREAL_1:7;
then ||.(f1/.c) + (f2/.c).|| <= r by XXREAL_0:2;
hence thesis by A8,VFUNCT_1:def 1;
end;
theorem
for f1 be PartFunc of M,COMPLEX holds f1|X is bounded & f2
is_bounded_on Y implies f1(#)f2 is_bounded_on (X /\ Y)
proof
let f1 be PartFunc of M,COMPLEX;
assume that
A1: f1|X is bounded and
A2: f2 is_bounded_on Y;
consider r1 be Real such that
A3: for c be Element of M st c in X /\ dom f1 holds |. f1/.c .| <= r1 by A1,
CFUNCT_1:69;
consider r2 be Real such that
A4: for c be Element of M st c in Y /\ dom f2 holds ||.(f2/.c).|| <= r2
by A2;
reconsider r1 as Real;
now
take r=r1*r2;
let c be Element of M;
assume
A5: c in X /\ Y /\ dom (f1(#)f2);
then
A6: c in X /\ Y by XBOOLE_0:def 4;
then
A7: c in X by XBOOLE_0:def 4;
A8: c in dom (f1(#)f2) by A5,XBOOLE_0:def 4;
then
A9: c in dom f1 /\ dom f2 by Def1;
then c in dom f1 by XBOOLE_0:def 4;
then c in X /\ dom f1 by A7,XBOOLE_0:def 4;
then
A10: |.(f1/.c).| <= r1 by A3;
A11: c in Y by A6,XBOOLE_0:def 4;
c in dom f2 by A9,XBOOLE_0:def 4;
then c in Y /\ dom f2 by A11,XBOOLE_0:def 4;
then
A12: ||.(f2/.c).|| <= r2 by A4;
0<=|.(f1/.c).| & 0<=||.(f2/.c).|| by CLVECT_1:105,COMPLEX1:46;
then |.(f1/.c).|*||.(f2/.c).|| <= r by A10,A12,XREAL_1:66;
then ||.f1/.c * (f2/.c).|| <= r by CLVECT_1:def 13;
hence ||.(f1(#)f2)/.c.|| <= r by A8,Def1;
end;
hence thesis;
end;
theorem
f1 is_bounded_on X & f2 is_bounded_on Y implies f1-f2 is_bounded_on X /\ Y
proof
assume that
A1: f1 is_bounded_on X and
A2: f2 is_bounded_on Y;
-f2 is_bounded_on Y by A2,Th45;
then f1+-f2 is_bounded_on (X /\ Y) by A1,Th46;
hence thesis by Th25;
end;
theorem
f is_bounded_on X & f is_bounded_on Y implies f is_bounded_on X \/ Y
proof
assume that
A1: f is_bounded_on X and
A2: f is_bounded_on Y;
consider r1 be Real such that
A3: for c be Element of M st c in X /\ dom f holds ||.f/.c.|| <= r1 by A1;
consider r2 be Real such that
A4: for c be Element of M st c in Y /\ dom f holds ||.f/.c.|| <= r2 by A2;
reconsider r = |.r1.| + |.r2.| as Real;
take r;
let c be Element of M;
assume
A5: c in (X \/ Y) /\ dom f;
then
A6: c in dom f by XBOOLE_0:def 4;
A7: c in X \/ Y by A5,XBOOLE_0:def 4;
now
per cases by A7,XBOOLE_0:def 3;
suppose
c in X;
then c in X /\ dom f by A6,XBOOLE_0:def 4;
then
A8: ||.f/.c.|| <= r1 by A3;
A9: 0 <= |.r2.| by COMPLEX1:46;
r1 <= |.r1.| by ABSVALUE:4;
then ||.f/.c.|| <= |.r1.| by A8,XXREAL_0:2;
then ||.f/.c.|| + 0 <= r by A9,XREAL_1:7;
hence thesis;
end;
suppose
c in Y;
then c in Y /\ dom f by A6,XBOOLE_0:def 4;
then
A10: ||.f/.c.|| <= r2 by A4;
A11: 0 <= |.r1.| by COMPLEX1:46;
r2 <= |.r2.| by ABSVALUE:4;
then ||.f/.c.|| <= |.r2.| by A10,XXREAL_0:2;
then 0 + ||.f/.c.|| <= r by A11,XREAL_1:7;
hence thesis;
end;
end;
hence thesis;
end;
theorem
f1|X is constant & f2|Y is constant implies (f1+f2)|(X /\ Y) is
constant & (f1-f2)|(X /\ Y) is constant
proof
assume that
A1: f1|X is constant and
A2: f2|Y is constant;
consider r1 being VECTOR of V such that
A3: for c be Element of M st c in X /\ dom f1 holds (f1/.c) = r1 by A1,
PARTFUN2:35;
consider r2 being VECTOR of V such that
A4: for c be Element of M st c in Y /\ dom f2 holds (f2/.c) = r2 by A2,
PARTFUN2:35;
now
let c be Element of M;
assume
A5: c in X /\ Y /\ dom (f1+f2);
then
A6: c in X /\ Y by XBOOLE_0:def 4;
then
A7: c in X by XBOOLE_0:def 4;
A8: c in dom (f1+f2) by A5,XBOOLE_0:def 4;
then
A9: c in (dom f1 /\ dom f2) by VFUNCT_1:def 1;
then c in dom f1 by XBOOLE_0:def 4;
then
A10: c in X /\ dom f1 by A7,XBOOLE_0:def 4;
A11: c in Y by A6,XBOOLE_0:def 4;
c in dom f2 by A9,XBOOLE_0:def 4;
then
A12: c in Y /\ dom f2 by A11,XBOOLE_0:def 4;
thus (f1+f2)/.c = (f1/.c) + (f2/.c) by A8,VFUNCT_1:def 1
.= r1 + (f2/.c) by A3,A10
.= r1 + r2 by A4,A12;
end;
hence (f1+f2)|(X /\ Y) is constant by PARTFUN2:35;
now
let c be Element of M;
assume
A13: c in X /\ Y /\ dom (f1-f2);
then
A14: c in X /\ Y by XBOOLE_0:def 4;
then
A15: c in X by XBOOLE_0:def 4;
A16: c in dom (f1-f2) by A13,XBOOLE_0:def 4;
then
A17: c in (dom f1 /\ dom f2) by VFUNCT_1:def 2;
then c in dom f1 by XBOOLE_0:def 4;
then
A18: c in X /\ dom f1 by A15,XBOOLE_0:def 4;
A19: c in Y by A14,XBOOLE_0:def 4;
c in dom f2 by A17,XBOOLE_0:def 4;
then
A20: c in Y /\ dom f2 by A19,XBOOLE_0:def 4;
thus (f1-f2)/.c = (f1/.c) - (f2/.c) by A16,VFUNCT_1:def 2
.= r1 - (f2/.c) by A3,A18
.= r1 - r2 by A4,A20;
end;
hence thesis by PARTFUN2:35;
end;
theorem
for f1 be PartFunc of M,COMPLEX holds f1|X is constant & f2|Y is
constant implies (f1(#)f2)|(X /\ Y) is constant
proof
let f1 be PartFunc of M,COMPLEX;
assume that
A1: f1|X is constant and
A2: f2|Y is constant;
consider z1 be Element of COMPLEX such that
A3: for c be Element of M st c in X /\ dom f1 holds f1.c = z1
by A1,PARTFUN2:57;
consider r2 being VECTOR of V such that
A4: for c be Element of M st c in Y /\ dom f2 holds (f2/.c) = r2 by A2,
PARTFUN2:35;
now
let c be Element of M;
assume
A5: c in X /\ Y /\ dom (f1(#)f2);
then
A6: c in X /\ Y by XBOOLE_0:def 4;
then
A7: c in Y by XBOOLE_0:def 4;
A8: c in dom (f1(#)f2) by A5,XBOOLE_0:def 4;
then
A9: c in (dom f1 /\ dom f2) by Def1;
then
A10: c in dom f1 by XBOOLE_0:def 4;
then
A11: f1/.c = f1.c by PARTFUN1:def 6;
c in dom f2 by A9,XBOOLE_0:def 4;
then
A12: c in Y /\ dom f2 by A7,XBOOLE_0:def 4;
c in X by A6,XBOOLE_0:def 4;
then
A13: c in X /\ dom f1 by A10,XBOOLE_0:def 4;
thus (f1(#)f2)/.c = f1/.c * (f2/.c) by A8,Def1
.= z1 * (f2/.c) by A3,A13,A11
.= z1 * r2 by A4,A12;
end;
hence thesis by PARTFUN2:35;
end;
theorem Th52:
f|Y is constant implies (z(#)f)|Y is constant
proof
assume f|Y is constant;
then consider r being VECTOR of V such that
A1: for c be Element of M st c in Y /\ dom f holds f/.c = r by PARTFUN2:35;
now
let c be Element of M;
assume
A2: c in Y /\ dom (z(#)f);
then
A3: c in Y by XBOOLE_0:def 4;
A4: c in dom (z(#)f) by A2,XBOOLE_0:def 4;
then c in dom f by Def2;
then
A5: c in Y /\ dom f by A3,XBOOLE_0:def 4;
thus (z(#)f)/.c = z * f/.c by A4,Def2
.= z*r by A1,A5;
end;
hence thesis by PARTFUN2:35;
end;
theorem Th53:
f|Y is constant implies ||.f.|||Y is constant & (-f)|Y is constant
proof
assume f|Y is constant;
then consider r being VECTOR of V such that
A1: for c be Element of M st c in Y /\ dom f holds f/.c = r by PARTFUN2:35;
A2: ||.r.|| in REAL by XREAL_0:def 1;
now
let c be Element of M;
assume
A3: c in Y /\ dom (||.f.||);
then
A4: c in Y by XBOOLE_0:def 4;
A5: c in dom (||.f.||) by A3,XBOOLE_0:def 4;
then c in dom f by NORMSP_0:def 3;
then
A6: c in Y /\ dom f by A4,XBOOLE_0:def 4;
thus (||.f.||).c = ||.f/.c.|| by A5,NORMSP_0:def 3
.= ||.r.|| by A1,A6;
end;
hence ||.f.|||Y is constant by PARTFUN2:57,A2;
now
take p=-r;
let c be Element of M;
assume
A7: c in Y /\ dom (-f);
then c in Y /\ dom f by VFUNCT_1:def 5;
then
A8: -f/.c = p by A1;
c in dom (-f) by A7,XBOOLE_0:def 4;
hence (-f)/.c = p by A8,VFUNCT_1:def 5;
end;
hence thesis by PARTFUN2:35;
end;
theorem Th54:
f|Y is constant implies f is_bounded_on Y
proof
assume f|Y is constant;
then consider r being VECTOR of V such that
A1: for c be Element of M st c in Y /\ dom f holds f/.c = r by PARTFUN2:35;
now
reconsider p=||.r.|| as Real;
take p;
let c be Element of M;
assume c in Y /\ dom f;
hence ||.f/.c.|| <= p by A1;
end;
hence thesis;
end;
theorem
f|Y is constant implies (for z holds z(#)f is_bounded_on Y) & -f
is_bounded_on Y & ||.f.|||Y is bounded
proof
assume
A1: f|Y is constant;
hereby
let z;
(z(#)f)|Y is constant by A1,Th52;
hence z(#)f is_bounded_on Y by Th54;
end;
(-f)|Y is constant by A1,Th53;
hence -f is_bounded_on Y by Th54;
||.f.|||Y is constant by A1,Th53;
hence thesis;
end;
theorem
f1 is_bounded_on X & f2|Y is constant implies f1+f2 is_bounded_on (X /\ Y)
proof
assume that
A1: f1 is_bounded_on X and
A2: f2|Y is constant;
f2 is_bounded_on Y by A2,Th54;
hence thesis by A1,Th46;
end;
theorem
f1 is_bounded_on X & f2|Y is constant implies f1-f2 is_bounded_on X /\
Y & f2-f1 is_bounded_on X /\ Y
proof
assume that
A1: f1 is_bounded_on X and
A2: f2|Y is constant;
A3: f2 is_bounded_on Y by A2,Th54;
then -f2 is_bounded_on Y by Th45;
then
A4: f1+-f2 is_bounded_on X /\ Y by A1,Th46;
-f1 is_bounded_on X by A1,Th45;
then f2+-f1 is_bounded_on Y /\ X by A3,Th46;
hence thesis by A4,Th25;
end;