:: Property of Complex Functions
:: by Takashi Mitsuishi , Katsumi Wasaki and Yasunari Shidama
::
:: Received December 7, 1999
:: Copyright (c) 1999-2021 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, SUBSET_1, PARTFUN1, NUMBERS, RELAT_1, ARYTM_3, CARD_1,
COMPLEX1, ORDINAL4, FUNCT_1, ARYTM_1, VALUED_1, TARSKI, XXREAL_2,
XXREAL_0, FUNCT_7, REAL_1, XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, RFUNCT_1, COMPLEX1,
VALUED_1, COMSEQ_2, SEQ_2;
constructors PARTFUN1, XXREAL_0, REAL_1, COMPLEX1, PARTFUN2, VALUED_1,
RFUNCT_1, SEQ_2, NAT_1, RELSET_1, COMSEQ_2;
registrations RELSET_1, NUMBERS, XREAL_0, MEMBERED, VALUED_0, RFUNCT_1,
XCMPLX_0;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, PARTFUN1, XBOOLE_0, COMSEQ_2;
equalities XBOOLE_0, VALUED_1;
expansions PARTFUN1, XBOOLE_0, COMSEQ_2;
theorems TARSKI, SUBSET_1, FUNCT_1, PARTFUN1, PARTFUN2, RFUNCT_1, COMPLEX1,
RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0,
VALUED_1, XREAL_0, FUNCT_2;
schemes PARTFUN2;
begin
reserve x,y,X,Y for set;
reserve C for non empty set;
reserve c for Element of C;
reserve f,f1,f2,f3,g,g1 for PartFunc of C,COMPLEX;
reserve r1,r2,p1 for Real;
reserve r,q,cr1,cr2 for Complex;
::
::DEFINITIONS OF COMPLEX FUNCTIONS
::
definition
let C,f1,f2;
deffunc F(set) = f1/.$1 * (f2/.$1)";
func f1/f2 -> PartFunc of C,COMPLEX means
:Def1:
dom it = dom f1 /\ (dom f2 \ f2"{0}) &
for c st c in dom it holds it/.c = f1/.c * (f2/.c)";
existence
proof
deffunc F(set) = In(f1/.$1 * (f2/.$1)",COMPLEX);
defpred P[set] means $1 in dom f1 /\ (dom f2 \ f2"{0c});
consider F being PartFunc of C,COMPLEX such that
A1: for c holds c in dom F iff P[c] and
A2: for c st c in dom F holds F/.c = F(c) from PARTFUN2:sch 2;
take F;
thus dom F = dom f1 /\ (dom f2 \ f2"{0}) by A1,SUBSET_1:3;
let c;
assume c in dom F;
then F/.c = F(c) by A2;
hence thesis;
end;
uniqueness
proof
set X = dom f1 /\ (dom f2 \ f2"{0});
let f,g be PartFunc of C,COMPLEX such that
A3: dom f=X and
A4: for c be Element of C st c in dom f holds f/.c = F(c) and
A5: dom g=X and
A6: for c be Element of C st c in dom g holds g/.c = F(c);
now let c be Element of C;
assume
A7: c in dom f;
hence f/.c = F(c) by A4 .= g/.c by A7,A3,A5,A6;
end;
hence f = g by A3,A5,PARTFUN2:1;
end;
end;
definition
let C,f;
deffunc F(set) = (f/.$1)";
func f^ -> PartFunc of C,COMPLEX means
:Def2:
dom it = dom f \ f"{0} & for c st c in dom it holds it/.c = (f/.c)";
existence
proof
deffunc F(set) = In((f/.$1)",COMPLEX);
defpred P[set] means $1 in dom f \ f"{0c};
consider F being PartFunc of C,COMPLEX such that
A1: for c holds c in dom F iff P[c] and
A2: for c st c in dom F holds F/.c = F(c) from PARTFUN2:sch 2;
take F;
thus dom F = dom f \ f"{0} by A1,SUBSET_1:3;
let c;
assume c in dom F;
then F/.c = F(c) by A2;
hence thesis;
end;
uniqueness
proof
set X = dom f \ f"{0};
let f1,g1 be PartFunc of C,COMPLEX such that
A3: dom f1=X and
A4: for c be Element of C st c in dom f1 holds f1/.c = F(c) and
A5: dom g1=X and
A6: for c be Element of C st c in dom g1 holds g1/.c = F(c);
now let c be Element of C;
assume
A7: c in dom f1;
hence f1/.c = F(c) by A4 .= g1/.c by A7,A3,A5,A6;
end;
hence f1 = g1 by A3,A5,PARTFUN2:1;
end;
end;
theorem Th1:
dom (f1+f2) = dom f1 /\ dom f2 & for c st c in dom(f1+f2) holds (
f1+f2)/.c = (f1/.c) + (f2/.c)
proof
thus
A1: dom (f1+f2) = dom f1 /\ dom f2 by VALUED_1:def 1;
now
let c;
assume
A2: c in dom (f1+f2);
then c in dom f1 by A1,XBOOLE_0:def 4;
then
A3: f1.c = f1/.c by PARTFUN1:def 6;
c in dom f2 by A1,A2,XBOOLE_0:def 4;
then
A4: f2.c = f2/.c by PARTFUN1:def 6;
thus (f1+f2)/.c = (f1+f2).c by A2,PARTFUN1:def 6
.= f1/.c+f2/.c by A2,A3,A4,VALUED_1:def 1;
end;
hence thesis;
end;
theorem Th2:
dom (f1-f2) = dom f1 /\ dom f2 & for c st c in dom(f1-f2) holds (
f1-f2)/.c = (f1/.c) - (f2/.c)
proof
A1: dom (f1-f2) = dom f1 /\ dom(-f2) by VALUED_1:def 1;
hence dom (f1-f2) = dom f1 /\ dom f2 by VALUED_1:8;
now
let c;
assume
A2: c in dom (f1-f2);
then
A3: dom -f2 = dom f2 & c in dom -f2 by A1,VALUED_1:8,XBOOLE_0:def 4;
c in dom f1 by A1,A2,XBOOLE_0:def 4;
then
A4: f1/.c = f1.c by PARTFUN1:def 6;
thus (f1-f2)/.c = (f1-f2).c by A2,PARTFUN1:def 6
.= f1.c - f2.c by A2,VALUED_1:13
.= f1/.c - f2/.c by A3,A4,PARTFUN1:def 6;
end;
hence thesis;
end;
theorem Th3:
dom(f1(#)f2)=dom f1 /\ dom f2 & for c st c in dom(f1(#)f2) holds
(f1(#)f2)/.c =(f1/.c) * (f2/.c)
proof
thus
A1: dom (f1(#)f2) = dom f1 /\ dom f2 by VALUED_1:def 4;
now
let c;
assume
A2: c in dom (f1(#)f2);
then c in dom f1 by A1,XBOOLE_0:def 4;
then
A3: f1.c = f1/.c by PARTFUN1:def 6;
c in dom f2 by A1,A2,XBOOLE_0:def 4;
then
A4: f2.c = f2/.c by PARTFUN1:def 6;
thus (f1(#)f2)/.c = (f1(#)f2).c by A2,PARTFUN1:def 6
.= f1/.c * f2/.c by A2,A3,A4,VALUED_1:def 4;
end;
hence thesis;
end;
theorem Th4:
dom (r(#)f) = dom f &
for c st c in dom (r(#)f) holds (r(#)f)/.c = r * (f/.c)
proof
thus
A1: dom (r(#)f) = dom f by VALUED_1:def 5;
now
let c;
assume
A2: c in dom (r(#)f);
hence (r(#)f)/.c = (r(#)f).c by PARTFUN1:def 6
.= r *(f.c) by VALUED_1:6
.= r *(f/.c) by A1,A2,PARTFUN1:def 6;
end;
hence thesis;
end;
theorem Th5:
dom (-f) = dom f & for c st c in dom (-f) holds (-f)/.c = -f/.c
proof
thus
A1: dom (-f) = dom f by VALUED_1:8;
now
let c;
assume
A2: c in dom (-f);
hence (-f)/.c = (-f).c by PARTFUN1:def 6
.=-f.c by VALUED_1:8
.=-f/.c by A1,A2,PARTFUN1:def 6;
end;
hence thesis;
end;
Lm1: x in f"Y iff x in dom f & f/.x in Y by PARTFUN2:26;
theorem Th6:
dom (g^) c= dom g & dom g /\ (dom g \ g"{0}) = dom g \ g"{0}
proof
dom (g^) = dom g \ g"{0c} by Def2;
hence dom (g^) c= dom g by XBOOLE_1:36;
thus thesis by XBOOLE_1:28,36;
end;
theorem Th7:
dom (f1(#)f2) \ (f1(#)f2)"{0} = (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0})
proof
thus dom (f1(#)f2) \ (f1(#)f2)"{0} c= (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"
{0})
proof
let x be object;
assume
A1: x in dom (f1(#)f2) \ (f1(#)f2)"{0};
then
A2: x in dom (f1(#)f2) by XBOOLE_0:def 5;
reconsider x1=x as Element of C by A1;
not x in (f1(#)f2)"{0c} by A1,XBOOLE_0:def 5;
then not (f1(#)f2)/.x1 in {0c} by A2,PARTFUN2:26;
then (f1(#)f2)/.x1 <> 0c by TARSKI:def 1;
then
A3: (f1/.x1) * (f2/.x1) <> 0c by A2,Th3;
then (f2/.x1) <> 0c;
then not (f2/.x1) in {0c } by TARSKI:def 1;
then
A4: not x1 in (f2)"{0c} by PARTFUN2:26;
A5: x1 in dom f1 /\ dom f2 by A2,Th3;
then x1 in dom f2 by XBOOLE_0:def 4;
then
A6: x in dom f2 \ (f2)"{0c} by A4,XBOOLE_0:def 5;
(f1/.x1) <> 0c by A3;
then not (f1/.x1) in {0c} by TARSKI:def 1;
then
A7: not x1 in (f1)"{0c} by PARTFUN2:26;
x1 in dom f1 by A5,XBOOLE_0:def 4;
then x in dom f1 \ (f1)"{0c} by A7,XBOOLE_0:def 5;
hence thesis by A6,XBOOLE_0:def 4;
end;
thus (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0}) c= dom (f1(#)f2) \ (f1(#)f2)
"{0}
proof
let x be object;
assume
A8: x in (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0});
then reconsider x1=x as Element of C;
A9: x in dom f2 \ (f2)"{0c} by A8,XBOOLE_0:def 4;
then
A10: x in dom f2 by XBOOLE_0:def 5;
not x in (f2)"{0c } by A9,XBOOLE_0:def 5;
then not (f2/.x1) in {0c} by A10,PARTFUN2:26;
then
A11: (f2/.x1) <> 0c by TARSKI:def 1;
A12: x in dom f1 \ (f1)"{0c} by A8,XBOOLE_0:def 4;
then
A13: x in dom f1 by XBOOLE_0:def 5;
then x1 in dom f1 /\ dom f2 by A10,XBOOLE_0:def 4;
then
A14: x1 in dom (f1(#)f2) by Th3;
not x in (f1)"{0c} by A12,XBOOLE_0:def 5;
then not (f1/.x1) in {0c} by A13,PARTFUN2:26;
then (f1/.x1) <> 0c by TARSKI:def 1;
then (f1/.x1) * (f2/.x1) <>0c by A11,XCMPLX_1:6;
then (f1(#)f2)/.x1 <> 0c by A14,Th3;
then not (f1(#)f2)/.x1 in {0c} by TARSKI:def 1;
then not x in (f1(#)f2)"{0c} by PARTFUN2:26;
hence thesis by A14,XBOOLE_0:def 5;
end;
end;
theorem Th8:
c in dom (f^) implies (f/.c) <> 0
proof
assume that
A1: c in dom (f^) and
A2: (f/.c) = 0;
A3: c in dom f \ f"{0c} by A1,Def2;
then
A4: not c in f"{0c} by XBOOLE_0:def 5;
now
per cases by A4,PARTFUN2:26;
suppose
not c in dom f;
hence contradiction by A3,XBOOLE_0:def 5;
end;
suppose
not (f/.c) in {0c};
hence contradiction by A2,TARSKI:def 1;
end;
end;
hence contradiction;
end;
theorem Th9:
(f^)"{0} = {}
proof
set x = the Element of (f^)"{0c};
assume
A1: (f^)"{0} <> {};
then
A2: x in dom (f^) by Lm1;
A3: (f^)/.x in {0c} by A1,Lm1;
reconsider x as Element of C by A2;
x in dom f \ f"{0c} by A2,Def2;
then x in dom f & not x in f"{0c} by XBOOLE_0:def 5;
then
A4: not f/.x in {0c} by PARTFUN2:26;
(f^)/.x = 0c by A3,TARSKI:def 1;
then (f/.x)" = 0c by A2,Def2;
hence contradiction by A4,TARSKI:def 1,XCMPLX_1:202;
end;
theorem Th10:
|.f.|"{0} = f"{0} & (-f)"{0} = f"{0}
proof
A1: dom |.f.| = dom f by VALUED_1:def 11;
now
let c;
thus c in (|.f.|)"{0} implies c in f"{0c}
proof
assume
A2: c in (|.f.|)"{0};
then c in dom (|.f.|) by FUNCT_1:def 7;
then
A3: c in dom f by VALUED_1:def 11;
(|.f.|).c in {0} by A2,FUNCT_1:def 7;
then (|.f.|).c = 0 by TARSKI:def 1;
then
A4: |.(f.c).| = 0 by VALUED_1:18;
c in dom (|.f.|) by A2,FUNCT_1:def 7;
then f.c = f/.c by A1,PARTFUN1:def 6;
then (f/.c) = 0c by A4,COMPLEX1:45;
then (f/.c) in {0c} by TARSKI:def 1;
hence thesis by A3,PARTFUN2:26;
end;
assume
A5: c in (f)"{0c};
then (f/.c) in {0c} by PARTFUN2:26;
then
A6: |.(f/.c).| = 0 by COMPLEX1:44,TARSKI:def 1;
A7: c in dom f by A5,PARTFUN2:26;
then f.c = f/.c by PARTFUN1:def 6;
then (|.f.|).c = 0 by A6,VALUED_1:18;
then
A8: (|.f.|).c in {0} by TARSKI:def 1;
c in dom (|.f.|) by A7,VALUED_1:def 11;
hence c in (|.f.|)"{0} by A8,FUNCT_1:def 7;
end;
hence (|.f.|)"{0} = f"{0} by SUBSET_1:3;
now
let c;
thus c in (-f)"{0c} implies c in f"{0c}
proof
assume
A9: c in (-f)"{0c};
then
A10: c in dom (-f) by PARTFUN2:26;
(-f)/.c in {0c} by A9,PARTFUN2:26;
then (-f)/.c = 0c by TARSKI:def 1;
then --((f/.c)) = -0c by A10,Th5;
then
A11: (f/.c) in {0c} by TARSKI:def 1;
c in dom f by A10,Th5;
hence thesis by A11,PARTFUN2:26;
end;
assume
A12: c in (f)"{0c};
then (f/.c) in {0c} by PARTFUN2:26;
then
A13: (f/.c) = 0c by TARSKI:def 1;
A14: c in dom f by A12,PARTFUN2:26;
then c in dom (-f) by Th5;
then (-f)/.c = -0c by A13,Th5;
then
A15: (-f)/.c in {0c} by TARSKI:def 1;
c in dom (-f) by A14,Th5;
hence c in (-f)"{0c} by A15,PARTFUN2:26;
end;
hence thesis by SUBSET_1:3;
end;
theorem Th11:
dom (f^^) = dom (f|(dom (f^)))
proof
A1: dom (f^) = dom f \ f"{0c} by Def2;
thus dom (f^^) = dom (f^) \(f^)"{0c} by Def2
.= dom (f^) \ {} by Th9
.= dom f /\ dom (f^) by A1,XBOOLE_1:28,36
.= dom (f|(dom (f^))) by RELAT_1:61;
end;
theorem Th12:
r<>0 implies (r(#)f)"{0} = f"{0}
proof
assume
A1: r<>0;
now
let c;
thus c in (r(#)f)"{0c} implies c in f"{0c}
proof
assume
A2: c in (r(#)f)"{0c};
then
A3: c in dom (r(#)f) by PARTFUN2:26;
(r(#)f)/.c in {0c} by A2,PARTFUN2:26;
then (r(#)f)/.c = 0c by TARSKI:def 1;
then r*(f/.c) = 0c by A3,Th4;
then (f/.c) = 0c by A1,XCMPLX_1:6;
then
A4: (f/.c) in {0c} by TARSKI:def 1;
c in dom f by A3,Th4;
hence thesis by A4,PARTFUN2:26;
end;
assume
A5: c in (f)"{0c};
then (f/.c) in {0c} by PARTFUN2:26;
then (f/.c) = 0c by TARSKI:def 1;
then
A6: r*(f/.c) = 0c;
A7: c in dom f by A5,PARTFUN2:26;
then c in dom (r(#)f) by Th4;
then (r(#)f)/.c = 0c by A6,Th4;
then
A8: (r(#)f)/.c in {0c} by TARSKI:def 1;
c in dom (r(#)f) by A7,Th4;
hence c in (r(#)f)"{0c} by A8,PARTFUN2:26;
end;
hence thesis by SUBSET_1:3;
end;
begin
::
:: BASIC PROPERTIES OF OPERATIONS
::
theorem
(f1 + f2) + f3 = f1 + (f2 + f3)
proof
A1: dom (f1 + f2 + f3) = dom (f1 + f2) /\ dom f3 by VALUED_1:def 1
.= dom f1 /\ dom f2 /\ dom f3 by VALUED_1:def 1
.= dom f1 /\ (dom f2 /\ dom f3) by XBOOLE_1:16
.= dom f1 /\ dom (f2 + f3) by VALUED_1:def 1
.= dom (f1 + (f2 + f3)) by VALUED_1:def 1;
now
let c;
assume
A2: c in dom (f1 + f2 + f3);
then c in dom (f1 + f2) /\ dom f3 by VALUED_1:def 1;
then
A3: c in dom (f1 + f2) by XBOOLE_0:def 4;
c in dom f1 /\ dom (f2 + f3) by A1,A2,VALUED_1:def 1;
then
A4: c in dom (f2 + f3) by XBOOLE_0:def 4;
thus (f1 + f2 + f3)/.c = (f1 + f2)/.c + (f3/.c) by A2,Th1
.= ((f1/.c)) + ((f2/.c)) + (f3/.c) by A3,Th1
.= ((f1/.c)) + (((f2/.c)) + (f3/.c))
.= ((f1/.c)) + (f2 + f3)/.c by A4,Th1
.= (f1 + (f2 + f3))/.c by A1,A2,Th1;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem Th14:
(f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
proof
A1: dom (f1 (#) f2 (#) f3) = dom (f1 (#) f2) /\ dom f3 by Th3
.= dom f1 /\ dom f2 /\ dom f3 by Th3
.= dom f1 /\ (dom f2 /\ dom f3) by XBOOLE_1:16
.= dom f1 /\ dom (f2 (#) f3) by Th3
.= dom (f1 (#) (f2 (#) f3)) by Th3;
now
let c;
assume
A2: c in dom (f1(#)f2(#)f3);
then c in dom (f1 (#) f2) /\ dom f3 by Th3;
then
A3: c in dom (f1 (#) f2) by XBOOLE_0:def 4;
c in dom f1 /\ dom (f2(#)f3) by A1,A2,Th3;
then
A4: c in dom (f2 (#) f3) by XBOOLE_0:def 4;
thus (f1 (#) f2 (#) f3)/.c = (f1 (#) f2)/.c * (f3/.c) by A2,Th3
.= ((f1/.c)) * ((f2/.c)) * (f3/.c) by A3,Th3
.= ((f1/.c)) * (((f2/.c)) * (f3/.c))
.= ((f1/.c)) * ((f2 (#) f3)/.c) by A4,Th3
.= (f1 (#) (f2 (#) f3))/.c by A1,A2,Th3;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem Th15:
(f1 + f2) (#) f3=f1 (#) f3 + f2 (#) f3
proof
A1: dom ((f1 + f2) (#) f3) = dom (f1 + f2) /\ dom f3 by Th3
.= 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 Th3
.= dom (f1 (#) f3) /\ dom (f2 (#) f3) by Th3
.= dom (f1 (#) f3 + f2 (#) f3) by VALUED_1:def 1;
now
let c;
assume
A2: c in dom ((f1 + f2)(#)f3);
then
A3: c in dom (f1(#)f3) /\ dom (f2(#)f3) by A1,VALUED_1:def 1;
then
A4: c in dom (f1(#)f3) by XBOOLE_0:def 4;
c in dom (f1 + f2) /\ dom f3 by A2,Th3;
then
A5: c in dom (f1 + f2) by XBOOLE_0:def 4;
A6: c in dom (f2 (#) f3) by A3,XBOOLE_0:def 4;
thus ((f1 + f2) (#) f3)/.c = (f1 + f2)/.c * (f3/.c) by A2,Th3
.= (((f1/.c)) + ((f2/.c))) * (f3/.c) by A5,Th1
.= ((f1/.c)) * (f3/.c) + ((f2/.c)) * (f3/.c)
.= (f1 (#) f3)/.c + ((f2/.c))* (f3/.c) by A4,Th3
.= (f1 (#) f3)/.c + (f2 (#) f3)/.c by A6,Th3
.=((f1 (#) f3) + (f2 (#) f3))/.c by A1,A2,Th1;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
f3 (#) (f1 + f2)=f3(#)f1 + f3(#)f2 by Th15;
theorem Th17:
r(#)(f1(#)f2)=r(#)f1(#)f2
proof
A1: dom (r(#)(f1 (#) f2)) = dom (f1 (#) f2) by Th4
.= dom f1 /\ dom f2 by Th3
.= dom (r(#)f1) /\ dom f2 by Th4
.= dom (r(#)f1(#)f2) by Th3;
now
let c;
assume
A2: c in dom (r(#)(f1(#)f2));
then
A3: c in dom (f1(#)f2) by Th4;
c in dom (r(#)f1) /\ dom f2 by A1,A2,Th3;
then
A4: c in dom (r(#)f1) by XBOOLE_0:def 4;
thus (r(#)(f1(#)f2))/.c = r * ((f1(#)f2)/.c) by A2,Th4
.= r*(((f1/.c)) * ((f2/.c))) by A3,Th3
.= (r*((f1/.c))) * ((f2/.c))
.= (r(#)f1)/.c * ((f2/.c)) by A4,Th4
.= (r(#)f1 (#) f2)/.c by A1,A2,Th3;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem Th18:
r(#)(f1(#)f2)=f1(#)(r(#)f2)
proof
A1: dom (r(#)(f1 (#) f2)) = dom (f1 (#) f2) by Th4
.= dom f1 /\ dom f2 by Th3
.= dom f1 /\ dom (r(#)f2) by Th4
.= dom (f1(#)(r(#)f2)) by Th3;
now
let c;
assume
A2: c in dom (r(#)(f1(#)f2));
then
A3: c in dom (f1(#)f2) by Th4;
c in dom f1 /\ dom (r(#)f2) by A1,A2,Th3;
then
A4: c in dom (r(#)f2) by XBOOLE_0:def 4;
thus (r(#)(f1(#)f2))/.c = r * ((f1(#)f2)/.c) by A2,Th4
.= r * (((f1/.c)) * ((f2/.c))) by A3,Th3
.= ((f1/.c)) * (r * ((f2/.c)))
.= ((f1/.c)) * ((r(#)f2)/.c) by A4,Th4
.= (f1(#)(r(#)f2))/.c by A1,A2,Th3;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem Th19:
(f1 - f2)(#)f3=f1(#)f3 - f2(#)f3
proof
A1: dom ((f1 - f2) (#) f3) = dom (f1 - f2) /\ dom f3 by Th3
.= dom f1 /\ dom f2 /\ (dom f3 /\ dom f3) by Th2
.= 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 Th3
.= dom (f1 (#) f3) /\ dom (f2 (#) f3) by Th3
.= dom (f1 (#) f3 - f2 (#) f3) by Th2;
now
let c;
assume
A2: c in dom ((f1 - f2)(#)f3);
then c in dom (f1 - f2) /\ dom f3 by Th3;
then
A3: c in dom (f1 - f2) by XBOOLE_0:def 4;
A4: c in dom (f1(#)f3) /\ dom (f2(#)f3) by A1,A2,Th2;
then
A5: c in dom (f1(#)f3) by XBOOLE_0:def 4;
A6: c in dom (f2 (#) f3) by A4,XBOOLE_0:def 4;
thus ((f1 - f2) (#) f3)/.c = (f1 - f2)/.c * (f3/.c) by A2,Th3
.= (((f1/.c)) - ((f2/.c))) * (f3/.c) by A3,Th2
.= ((f1/.c)) * (f3/.c) - ((f2/.c)) * (f3/.c)
.= (f1 (#) f3)/.c - ((f2/.c)) * (f3/.c) by A5,Th3
.= (f1 (#) f3)/.c - (f2 (#) f3)/.c by A6,Th3
.=((f1 (#) f3) - (f2 (#) f3))/.c by A1,A2,Th2;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
f3(#)f1 - f3(#)f2 = f3(#)(f1 - f2) by Th19;
theorem
r(#)(f1 + f2) = r(#)f1 + r(#)f2
proof
A1: dom (r(#)(f1 + f2)) = dom (f1 + f2) by Th4
.= dom f1 /\ dom f2 by VALUED_1:def 1
.= dom f1 /\ dom (r(#)f2) by Th4
.= dom (r(#)f1) /\ dom (r(#)f2) by Th4
.= dom (r(#)f1 + r(#)f2) by VALUED_1:def 1;
now
let c;
assume
A2: c in dom (r(#)(f1 + f2));
then
A3: c in dom (f1 + f2) by Th4;
A4: c in dom (r(#)f1) /\ dom (r(#)f2) by A1,A2,VALUED_1:def 1;
then
A5: c in dom (r(#)f1) by XBOOLE_0:def 4;
A6: c in dom (r(#)f2) by A4,XBOOLE_0:def 4;
thus (r(#)(f1 + f2))/.c = r * ((f1 + f2)/.c) by A2,Th4
.= r * (((f1/.c)) + ((f2/.c))) by A3,Th1
.= r * ((f1/.c)) + r * ((f2/.c))
.= (r(#)f1)/.c + r * ((f2/.c)) by A5,Th4
.= (r(#)f1)/.c + (r(#)f2)/.c by A6,Th4
.= (r(#)f1 + r(#)f2)/.c by A1,A2,Th1;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
(r*q)(#)f = r(#)(q(#)f)
proof
A1: dom ((r*q) (#) f) = dom f by Th4
.= dom (q(#)f) by Th4
.= dom (r(#)(q(#)f)) by Th4;
now
let c;
assume
A2: c in dom ((r*q)(#)f);
then
A3: c in dom (q(#)f) by A1,Th4;
thus ((r*q)(#)f)/.c = r*q * (f/.c) by A2,Th4
.= r*(q * (f/.c))
.= r * ((q(#)f)/.c) by A3,Th4
.= (r(#)(q(#)f))/.c by A1,A2,Th4;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
r(#)(f1 - f2) = r(#)f1 - r(#)f2
proof
A1: dom (r(#)(f1 - f2)) = dom (f1 - f2) by Th4
.= dom f1 /\ dom f2 by Th2
.= dom f1 /\ dom (r(#)f2) by Th4
.= dom (r(#)f1) /\ dom (r(#)f2) by Th4
.= dom (r(#)f1 - r(#)f2) by Th2;
now
let c;
assume
A2: c in dom (r(#)(f1 - f2));
then
A3: c in dom (f1 - f2) by Th4;
A4: c in dom (r(#)f1) /\ dom (r(#)f2) by A1,A2,Th2;
then
A5: c in dom (r(#)f1) by XBOOLE_0:def 4;
A6: c in dom (r(#)f2) by A4,XBOOLE_0:def 4;
thus (r(#)(f1 - f2))/.c = r * ((f1 - f2)/.c) by A2,Th4
.= r * (((f1/.c)) - ((f2/.c))) by A3,Th2
.= r * ((f1/.c)) - r * ((f2/.c))
.= (r(#)f1)/.c - r * ((f2/.c)) by A5,Th4
.= (r(#)f1)/.c - (r(#)f2)/.c by A6,Th4
.= (r(#)f1 - r(#)f2)/.c by A1,A2,Th2;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
f1-f2 = (-1r)(#)(f2-f1)
proof
A1: dom (f1 - f2) = dom f2 /\ dom f1 by Th2
.= dom (f2 - f1) by Th2
.= dom ((-1r)(#)(f2 - f1)) by Th4;
now
A2: dom (f1 - f2) = dom f2 /\ dom f1 by Th2
.= dom (f2 - f1) by Th2;
let c such that
A3: c in dom (f1-f2);
thus (f1 - f2)/.c = ((f1/.c)) - ((f2/.c)) by A3,Th2
.= (-1)*(((f2/.c)) - ((f1/.c)))
.= (-1r)*((f2 - f1)/.c) by A3,A2,Th2,COMPLEX1:def 4
.= ((-1r)(#)(f2 - f1))/.c by A1,A3,Th4;
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 Th2
.= dom f1 /\ (dom f2 /\ dom f3) by VALUED_1:def 1
.= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom (f1 - f2) /\ dom f3 by Th2
.= dom (f1 - f2 - f3) by Th2;
now
let c;
assume
A2: c in dom (f1 - (f2 + f3));
then c in dom f1 /\ dom (f2 + f3) by Th2;
then
A3: c in dom (f2 + f3) by XBOOLE_0:def 4;
c in dom (f1 - f2) /\ dom f3 by A1,A2,Th2;
then
A4: c in dom (f1 - f2) by XBOOLE_0:def 4;
thus (f1 - (f2 + f3))/.c = ((f1/.c)) - (f2 + f3)/.c by A2,Th2
.= ((f1/.c)) - (((f2/.c)) + (f3/.c)) by A3,Th1
.= ((f1/.c)) - ((f2/.c)) - (f3/.c)
.= (f1 - f2)/.c - (f3/.c) by A4,Th2
.= (f1 - f2 - f3)/.c by A1,A2,Th2;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem
1r(#)f = f
proof
A1: now
let c;
assume c in dom (1r(#)f);
hence (1r(#)f)/.c = 1r * (f/.c) by Th4
.= (f/.c) by COMPLEX1:def 4;
end;
dom (1r(#)f) = dom f by Th4;
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 Th2
.= dom f1 /\ (dom f2 /\ dom f3) by Th2
.= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom (f1 - f2) /\ dom f3 by Th2
.= dom (f1 - f2 + f3) by VALUED_1:def 1;
now
let c;
assume
A2: c in dom (f1 - (f2 - f3));
then c in dom (f1 - f2) /\ dom f3 by A1,VALUED_1:def 1;
then
A3: c in dom (f1 - f2) by XBOOLE_0:def 4;
c in dom f1 /\ dom (f2 - f3) by A2,Th2;
then
A4: c in dom (f2 - f3) by XBOOLE_0:def 4;
thus (f1 - (f2 - f3))/.c = ((f1/.c)) - (f2 - f3)/.c by A2,Th2
.= ((f1/.c)) - (((f2/.c)) - (f3/.c)) by A4,Th2
.= ((f1/.c)) - ((f2/.c)) + (f3/.c)
.= (f1 - f2)/.c + (f3/.c) by A3,Th2
.= (f1 - f2 + f3)/.c by A1,A2,Th1;
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 VALUED_1:def 1
.= dom f1 /\ (dom f2 /\ dom f3) by Th2
.= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom (f1 + f2) /\ dom f3 by VALUED_1:def 1
.= dom (f1 + f2 - f3) by Th2;
now
let c;
assume
A2: c in dom (f1 + (f2 - f3));
then c in dom f1 /\ dom (f2 - f3) by VALUED_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,Th2;
then
A4: c in dom (f1 + f2) by XBOOLE_0:def 4;
thus (f1 + (f2 - f3))/.c = ((f1/.c)) + (f2 - f3)/.c by A2,Th1
.= ((f1/.c)) + (((f2/.c)) - (f3/.c)) by A3,Th2
.= ((f1/.c)) + ((f2/.c)) - (f3/.c)
.= (f1 + f2)/.c - (f3/.c) by A4,Th1
.= (f1 + f2 - f3)/.c by A1,A2,Th2;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem Th29:
|.f1(#)f2.| = |.f1.|(#)|.f2.|
proof
A1: dom (|.f1 (#) f2.|) = dom (f1 (#) f2) by VALUED_1:def 11
.= dom f1 /\ dom f2 by Th3
.= dom f1 /\ dom (|.f2.|) by VALUED_1:def 11
.= dom (|.f1.|) /\ dom (|.f2.|) by VALUED_1:def 11
.= dom (|.f1.|(#)|.f2.|) by VALUED_1:def 4;
now
A2: dom |.f2.| = dom f2 by VALUED_1:def 11;
let c;
A3: dom |.f1.| = dom f1 by VALUED_1:def 11;
assume
A4: c in dom (|.f1 (#) f2.|);
then
A5: c in dom (f1 (#) f2) by VALUED_1:def 11;
A6: c in dom (|.f1.|) /\ dom (|.f2.|) by A1,A4,VALUED_1:def 4;
then c in dom (|.f1.|) by XBOOLE_0:def 4;
then
A7: f1.c = f1/.c by A3,PARTFUN1:def 6;
c in dom (|.f2.|) by A6,XBOOLE_0:def 4;
then
A8: f2/.c = f2.c by A2,PARTFUN1:def 6;
thus (|.(f1(#)f2).|).c = |.(f1(#)f2).c.| by VALUED_1:18
.= |.(f1(#)f2)/.c.| by A5,PARTFUN1:def 6
.= |.((f1/.c)) * ((f2/.c)).| by A5,Th3
.= |.((f1/.c)).| * |.((f2/.c)).| by COMPLEX1:65
.= ((|.f1.|).c) *( |.((f2/.c)).|) by A7,VALUED_1:18
.= ((|.f1.|).c) * ((|.f2.|).c) by A8,VALUED_1:18
.= (|.f1.|(#)|.f2.|).c by VALUED_1:5;
end;
hence thesis by A1,PARTFUN1:5;
end;
theorem Th30:
|.r(#)f.| = |.r.|(#)|.f.|
proof
A1: dom f = dom (|.f.|) by VALUED_1:def 11;
A2: dom (|.r(#)f.|) = dom (r(#)f) by VALUED_1:def 11
.= dom f by Th4
.= dom (|.r.|(#)|.f.|) by A1,VALUED_1:def 5;
now
let c;
assume
A3: c in dom (|.r(#)f.|);
then
A4: c in dom (r(#)f) by VALUED_1:def 11;
A5: c in dom (|.f.|) by A2,A3,VALUED_1:def 5;
thus (|.r(#)f.|).c = |.(r(#)f).c.| by VALUED_1:18
.=|.(r(#)f)/.c.| by A4,PARTFUN1:def 6
.=|.r*((f/.c)).| by A4,Th4
.=|.r.|*|.((f/.c)).| by COMPLEX1:65
.=|.r.|*|.((f.c)).| by A1,A5,PARTFUN1:def 6
.=|.r.|*((|.f.|).c) by VALUED_1:18
.=(|.r.|(#)|.f.|).c by A2,A3,VALUED_1:def 5;
end;
hence thesis by A2,PARTFUN1:5;
end;
theorem
-f = (-1r)(#)f by COMPLEX1:def 4;
::$CT
theorem
f1 - (-f2) = f1 + f2;
theorem Th33:
f^^ = f|(dom (f^))
proof
A1: dom (f^^) = dom (f|(dom (f^))) by Th11;
now
let c;
assume
A2: c in dom (f^^);
then c in dom f /\ dom (f^) by A1,RELAT_1:61;
then
A3: c in dom (f^) by XBOOLE_0:def 4;
thus (f^^)/.c = ((f^)/.c)" by A2,Def2
.= (((f/.c))")" by A3,Def2
.= (f|(dom (f^)))/.c by A1,A2,PARTFUN2:15;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem Th34:
(f1(#)f2)^ = (f1^)(#)(f2^)
proof
A1: dom ((f1(#)f2)^) = dom (f1(#)f2) \ (f1(#)f2)"{0c} by Def2
.= (dom f1 \ f1"{0c}) /\ (dom f2 \ (f2)"{0c}) by Th7
.= dom (f1^) /\ (dom f2 \ (f2)"{0c}) by Def2
.= dom (f1^) /\ dom (f2^) by Def2
.= dom ((f1^) (#) (f2^)) by Th3;
now
let c;
assume
A2: c in dom ((f1(#)f2)^);
then c in dom (f1(#)f2) \ (f1(#)f2)"{0c} by Def2;
then
A3: c in dom (f1(#)f2) by XBOOLE_0:def 5;
A4: c in dom (f1^) /\ dom (f2^) by A1,A2,Th3;
then
A5: c in dom (f1^) by XBOOLE_0:def 4;
A6: c in dom (f2^) by A4,XBOOLE_0:def 4;
thus ((f1(#)f2)^)/.c = ((f1(#)f2)/.c)" by A2,Def2
.= (((f1/.c)) * ((f2/.c)))" by A3,Th3
.= (((f1/.c)))"* (((f2/.c)))" by XCMPLX_1:204
.= ((f1^)/.c)*(((f2/.c)))" by A5,Def2
.= ((f1^)/.c) *((f2^)/.c) by A6,Def2
.= ((f1^) (#) (f2^))/.c by A1,A2,Th3;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem Th35:
r<>0 implies (r(#)f)^ = r" (#) (f^)
proof
assume
A1: r<>0;
A2: dom ((r(#)f)^) = dom (r(#)f) \ (r(#)f)"{0c} by Def2
.= dom (r(#)f) \ f"{0c} by A1,Th12
.= dom f \ f"{0c} by Th4
.= dom (f^) by Def2
.= dom (r"(#)(f^)) by Th4;
now
let c;
assume
A3: c in dom ((r(#)f)^);
then
A4: c in dom (f^) by A2,Th4;
c in dom (r(#)f) \ (r(#)f)"{0c} by A3,Def2;
then
A5: c in dom (r(#)f) by XBOOLE_0:def 5;
thus ((r(#)f)^)/.c = ((r(#)f)/.c)" by A3,Def2
.= (r*((f/.c)))" by A5,Th4
.= r"* ((f/.c))" by XCMPLX_1:204
.= r"* ((f^)/.c) by A4,Def2
.= (r" (#) (f^))/.c by A2,A3,Th4;
end;
hence thesis by A2,PARTFUN2:1;
end;
Lm2: (-1r)"=-1r by COMPLEX1:def 4;
theorem
(-f)^ = (-1r)(#)(f^) by Lm2,Th35,COMPLEX1:def 4;
theorem Th37:
|.f.|^ = |. f^ .|
proof
A1: dom ((|.f.|)^) = dom (|.f.|) \ (|.f.|)"{0} by RFUNCT_1:def 2
.= dom f \ (|.f.|)"{0} by VALUED_1:def 11
.= dom f \ f"{0c} by Th10
.= dom (f^) by Def2
.= dom (|.(f^).|) by VALUED_1:def 11;
now
let c;
A2: dom f = dom |.f.| by VALUED_1:def 11;
assume
A3: c in dom ((|.f.|)^);
then
A4: c in dom (f^) by A1,VALUED_1:def 11;
c in dom (|.f.|) \ (|.f.|)"{0} by A3,RFUNCT_1:def 2;
then
A5: c in dom (|.f.|) by XBOOLE_0:def 5;
thus ((|.f.|)^).c = ((|.f.|).c)" by A3,RFUNCT_1:def 2
.= (|.(f.c) .|)" by VALUED_1:18
.= (|.(f/.c) .|)" by A5,A2,PARTFUN1:def 6
.= |.1r.|/|.(f/.c) .| by COMPLEX1:48,XCMPLX_1:215
.= |.1r/(f/.c) .| by COMPLEX1:67
.= |.((f/.c))" .| by COMPLEX1:def 4,XCMPLX_1:215
.= |.(f^)/.c .| by A4,Def2
.= |.(f^).c .| by A4,PARTFUN1:def 6
.= (|.(f^).|).c by VALUED_1:18;
end;
hence thesis by A1,PARTFUN1:5;
end;
theorem Th38:
f/g = f(#) (g^)
proof
A1: now
let c;
assume
A2: c in dom (f/g);
then c in dom f /\ (dom g \ g"{0c}) by Def1;
then
A3: c in dom f /\ dom (g^) by Def2;
then
A4: c in dom (g^) by XBOOLE_0:def 4;
A5: c in dom (f (#) (g^)) by A3,Th3;
thus (f/g)/.c = (f/.c) * (g/.c)" by A2,Def1
.= (f/.c) * ((g^)/.c) by A4,Def2
.= (f (#) (g^))/.c by A5,Th3;
end;
dom (f/g) = dom f /\ (dom g \ g"{0c}) by Def1
.= dom f /\ dom (g^) by Def2
.= dom (f(#)(g^)) by Th3;
hence thesis by A1,PARTFUN2:1;
end;
theorem Th39:
r(#)(g/f) = (r(#)g)/f
proof
thus r(#)(g/f) = r(#)(g(#)(f^)) by Th38
.= (r(#)g)(#)(f^) by Th17
.= (r(#)g)/f by Th38;
end;
theorem
(f/g)(#)g = (f|dom(g^))
proof
A1: dom ((f/g)(#)g) = dom (f/g) /\ dom g by Th3
.= dom f /\ (dom g \ g"{0c}) /\ dom g by Def1
.= dom f /\ ((dom g \ g"{0c}) /\ dom g) by XBOOLE_1:16
.= dom f /\ (dom (g^) /\ dom g) by Def2
.= dom f /\ dom (g^) by Th6,XBOOLE_1:28
.= dom (f|(dom (g^))) by RELAT_1:61;
now
let c;
assume
A2: c in dom ((f/g)(#)g);
then
A3: c in dom f /\ dom (g^) by A1,RELAT_1:61;
then
A4: c in dom (f(#)(g^)) by Th3;
A5: c in dom (g^) by A3,XBOOLE_0:def 4;
then
A6: g/.c <> 0c by Th8;
thus ((f/g)(#)g)/.c = ((f/g)/.c) * (g/.c )by A2,Th3
.= (f(#)(g^))/.c * (g/.c) by Th38
.= ((f/.c)) *((g^)/.c) * (g/.c) by A4,Th3
.= ((f/.c))*(g/.c)"*(g/.c) by A5,Def2
.= ((f/.c))*((g/.c)" * (g/.c))
.= ((f/.c))*1r by A6,COMPLEX1:def 4,XCMPLX_0:def 7
.= (f|(dom (g^)))/.c by A1,A2,COMPLEX1:def 4,PARTFUN2:15;
end;
hence thesis by A1,PARTFUN2:1;
end;
theorem Th41:
(f/g)(#)(f1/g1) = (f(#)f1)/(g(#)g1)
proof
A1: now
let c;
assume
A2: c in dom ((f/g)(#)(f1/g1));
then c in dom (f/g) /\ dom (f1/g1) by Th3;
then
A3: c in dom (f (#)(g^)) /\ dom (f1/g1) by Th38;
then
A4: c in dom (f (#)(g^)) by XBOOLE_0:def 4;
then
A5: c in dom f /\ dom(g^) by Th3;
c in dom (f (#)(g^)) /\ dom (f1(#)(g1^)) by A3,Th38;
then
A6: c in dom (f1(#)(g1^)) by XBOOLE_0:def 4;
then
A7: c in dom f1 /\ dom(g1^) by Th3;
then
A8: c in dom f1 by XBOOLE_0:def 4;
c in dom f by A5,XBOOLE_0:def 4;
then c in dom f /\ dom f1 by A8,XBOOLE_0:def 4;
then
A9: c in dom (f(#)f1) by Th3;
A10: c in dom(g1^) by A7,XBOOLE_0:def 4;
c in dom(g^) by A5,XBOOLE_0:def 4;
then c in dom (g^) /\ dom (g1^) by A10,XBOOLE_0:def 4;
then
A11: c in dom((g^)(#)(g1^)) by Th3;
then c in dom((g(#)g1)^) by Th34;
then c in dom (f(#)f1) /\ dom((g(#)g1)^) by A9,XBOOLE_0:def 4;
then
A12: c in dom ((f(#)f1)(#)((g(#)g1)^)) by Th3;
thus ((f/g)(#)(f1/g1))/.c = ((f/g)/.c)* ((f1/g1)/.c) by A2,Th3
.= ((f(#)(g^))/.c) * ((f1/g1)/.c) by Th38
.= ((f(#)(g^))/.c) * ((f1(#)(g1^))/.c) by Th38
.= ((f/.c)) * ((g^)/.c) *((f1(#)(g1^))/.c) by A4,Th3
.= ((f/.c)) * ((g^)/.c) * ((((f1/.c)))* ((g1^)/.c)) by A6,Th3
.= ((f/.c)) * ((((f1/.c))) * (((g^)/.c) * ((g1^)/.c)))
.= ((f/.c)) * ((((f1/.c))) * (((g^)(#)(g1^))/.c)) by A11,Th3
.= ((f/.c)) * (((f1/.c))) * (((g^)(#)(g1^))/.c)
.= ((f/.c)) * (((f1/.c))) * (((g(#)g1)^)/.c) by Th34
.= ((f(#)f1)/.c) * (((g(#)g1)^)/.c) by A9,Th3
.= ((f(#)f1)(#)((g(#)g1)^))/.c by A12,Th3
.= ((f(#)f1)/(g(#)g1))/.c by Th38;
end;
dom ((f/g)(#)(f1/g1)) = dom (f/g) /\ dom (f1/g1) by Th3
.= dom f /\ (dom g \ g"{0c}) /\ dom (f1/g1) by Def1
.= dom f /\ (dom g \ g"{0c}) /\ (dom f1 /\ (dom g1 \ g1"{0c})) by Def1
.= dom f /\ ((dom g \ g"{0c}) /\ (dom f1 /\ (dom g1 \ g1"{0c}))) by
XBOOLE_1:16
.= dom f /\ (dom f1 /\ ((dom g \ g"{0c}) /\ (dom g1 \ g1"{0c}))) by
XBOOLE_1:16
.= dom f /\ dom f1 /\ ((dom g \ g"{0c}) /\ (dom g1 \ g1"{0c})) by
XBOOLE_1:16
.= dom (f(#)f1) /\ ((dom g \ g"{0c}) /\ (dom g1 \ g1"{0c})) by Th3
.= dom (f(#)f1) /\ (dom (g(#)g1) \ (g(#)g1)"{0c}) by Th7
.= dom ((f(#)f1)/(g(#)g1)) by Def1;
hence thesis by A1,PARTFUN2:1;
end;
theorem Th42:
(f1/f2)^ = (f2|dom(f2^))/f1
proof
thus (f1/f2)^ = (f1(#)(f2^))^ by Th38
.= (f1^)(#)(f2^^) by Th34
.= (f2|dom(f2^))(#)(f1^) by Th33
.= (f2|dom(f2^))/f1 by Th38;
end;
theorem Th43:
g (#) (f1/f2) = (g (#) f1)/f2
proof
thus g (#) (f1/f2) = g (#) (f1 (#) (f2^)) by Th38
.= g (#) f1 (#) (f2^) by Th14
.= (g (#) f1)/f2 by Th38;
end;
theorem
g/(f1/f2) = (g(#)(f2|dom(f2^)))/f1
proof
thus g/(f1/f2) = g (#) ((f1/f2)^) by Th38
.= g (#) ((f2|dom(f2^))/f1) by Th42
.= (g (#) (f2|dom(f2^)))/f1 by Th43;
end;
theorem
-f/g = (-f)/g & f/(-g) = -f/g
proof
thus -f/g = (-1r)(#)(f/g) by COMPLEX1:def 4
.= (-f)/g by Th39,COMPLEX1:def 4;
thus f/(-g) = f (#) ((-g)^) by Th38
.= f (#) ((-1r) (#) (g^)) by Lm2,Th35,COMPLEX1:def 4
.= -(f (#) (g^)) by Th18,COMPLEX1:def 4
.= -(f/g) by Th38;
end;
theorem
f1/f + f2/f = (f1 + f2)/f & f1/f - f2/f = (f1 - f2)/f
proof
thus f1/f + f2/f = f1(#)(f^) +f2/f by Th38
.= f1(#)(f^) + f2(#)(f^) by Th38
.= (f1+f2) (#) (f^) by Th15
.= (f1+f2)/f by Th38;
thus f1/f - f2/f = f1(#)(f^) - f2/f by Th38
.= f1(#)(f^) -f2(#)(f^) by Th38
.= (f1-f2)(#)(f^) by Th19
.= (f1-f2)/f by Th38;
end;
theorem Th47:
f1/f + g1/g = (f1(#)g + g1(#)f)/(f(#)g)
proof
A1: now
let c;
A2: dom (f^) c= dom f by Th6;
assume
A3: c in dom ((f1/f) + (g1/g));
then
A4: c in dom (f1/f) /\ dom (g1/g) by VALUED_1:def 1;
then
A5: c in dom (f1/f) by XBOOLE_0:def 4;
A6: c in dom (g1/g) by A4,XBOOLE_0:def 4;
A7: c in dom (f1 (#)(f^)) /\ dom (g1/g) by A4,Th38;
then c in dom (f1 (#)(f^)) by XBOOLE_0:def 4;
then
A8: c in dom f1 /\ dom(f^) by Th3;
then
A9: c in dom(f^) by XBOOLE_0:def 4;
then
A10: (f/.c) <> 0c by Th8;
c in dom (f1 (#)(f^)) /\ dom (g1(#)(g^)) by A7,Th38;
then c in dom (g1(#)(g^)) by XBOOLE_0:def 4;
then
A11: c in dom g1 /\ dom(g^) by Th3;
then
A12: c in dom(g^) by XBOOLE_0:def 4;
then
A13: g/.c <> 0c by Th8;
c in dom g1 by A11,XBOOLE_0:def 4;
then c in dom g1 /\ dom f by A9,A2,XBOOLE_0:def 4;
then
A14: c in dom (g1(#)f) by Th3;
A15: dom (g^) c= dom g by Th6;
then c in dom f /\ dom g by A9,A12,A2,XBOOLE_0:def 4;
then
A16: c in dom (f(#)g) by Th3;
c in dom f1 by A8,XBOOLE_0:def 4;
then c in dom f1 /\ dom g by A12,A15,XBOOLE_0:def 4;
then
A17: c in dom (f1(#)g) by Th3;
then c in dom (f1(#)g) /\ dom (g1(#)f) by A14,XBOOLE_0:def 4;
then
A18: c in dom (f1(#)g + g1(#)f) by VALUED_1:def 1;
c in dom (f^) /\ dom (g^) by A9,A12,XBOOLE_0:def 4;
then c in dom ((f^)(#)(g^)) by Th3;
then c in dom ((f(#)g)^) by Th34;
then c in dom (f1(#)g + g1(#)f) /\ dom ((f(#)g)^) by A18,XBOOLE_0:def 4;
then c in dom ((f1(#)g + g1(#)f)(#)((f(#)g)^)) by Th3;
then
A19: c in dom ((f1(#)g + g1(#)f)/(f(#)g)) by Th38;
thus (f1/f + g1/g)/.c = (f1/f)/.c + (g1/g)/.c by A3,Th1
.= (((f1/.c))) * ((f/.c))" + (g1/g)/.c by A5,Def1
.= (((f1/.c))) *(1r*((f/.c))") + (g1/.c) * 1r * (g/.c)" by A6,Def1,
COMPLEX1:def 4
.= (((f1/.c))) *((g/.c) *(g/.c)"* ((f/.c))") + (g1/.c) * (1r * (g/.c)"
) by A13,COMPLEX1:def 4,XCMPLX_0:def 7
.= (((f1/.c))) *(g/.c *((g/.c)"* ((f/.c))")) + (g1/.c) * (((f/.c)) *((
f/.c))" * (g/.c)") by A10,COMPLEX1:def 4,XCMPLX_0:def 7
.= (((f1/.c))) *((g/.c) *((g/.c * (f/.c))")) + (g1/.c) * (((f/.c)) *((
(f/.c))" * (g/.c)")) by XCMPLX_1:204
.= (((f1/.c))) *((g/.c) *(((f/.c)* (g/.c))")) + (g1/.c) * (((f/.c)) *(
((f/.c) * (g/.c))")) by XCMPLX_1:204
.= (((f1/.c))) *((g/.c) * ((f(#)g)/.c)") + (g1/.c) * (((f/.c)) *(((f/.
c) * (g/.c))")) by A16,Th3
.= (((f1/.c))) *(g/.c) * ((f(#)g)/.c)" + (g1/.c) * (((f/.c)) * ((f(#)
g)/.c)") by A16,Th3
.= (f1(#)g)/.c * ((f(#)g)/.c)" + (g1/.c) *(f/.c) *((f(#)g)/.c)" by A17
,Th3
.= (f1(#)g)/.c * ((f(#)g)/.c)" + (g1(#)f)/.c *((f(#)g)/.c)" by A14,Th3
.= ((f1(#)g)/.c + (g1(#)f)/.c) *((f(#)g)/.c)"
.= (f1(#)g + g1(#)f)/.c *((f(#)g)/.c)" by A18,Th1
.= ((f1(#)g + g1(#)f)/(f(#)g))/.c by A19,Def1;
end;
dom ((f1/f) + (g1/g)) = dom (f1/f) /\ dom (g1/g) by VALUED_1:def 1
.= dom f1 /\ (dom f \ f"{0c}) /\ dom (g1/g) by Def1
.= dom f1 /\ (dom f \ f"{0c}) /\ (dom g1 /\ (dom g \ g"{0c})) by Def1
.= dom f1 /\ (dom f /\ (dom f \ f"{0c})) /\ (dom g1 /\ (dom g \ g"{0c}))
by Th6
.= dom f /\ (dom f \ f"{0c}) /\ dom f1 /\ (dom g /\ (dom g \ g"{0c}) /\
dom g1) by Th6
.= dom f /\ (dom f \ f"{0c}) /\ (dom f1 /\ (dom g /\ (dom g \ g"{0c}) /\
dom g1)) by XBOOLE_1:16
.= dom f /\ (dom f \ f"{0c}) /\ (dom f1 /\ (dom g /\ (dom g \ g"{0c}))
/\ dom g1) by XBOOLE_1:16
.= dom f /\ (dom f \ f"{0c}) /\ (dom f1 /\ dom g /\ (dom g \ g"{0c}) /\
dom g1) by XBOOLE_1:16
.= dom f /\ (dom f \ f"{0c}) /\ (dom (f1(#) g) /\ (dom g \ g"{0c}) /\
dom g1) by Th3
.= dom f /\ (dom f \ f"{0c}) /\ (dom (f1(#)g) /\ (dom g1 /\ (dom g \ g"{
0c}))) by XBOOLE_1:16
.= dom (f1(#)g) /\ ((dom f \ f"{0c}) /\ dom f /\ (dom g1 /\ (dom g \ g"{
0c}))) by XBOOLE_1:16
.= dom (f1(#)g) /\ ((dom f \ f"{0c}) /\ (dom f /\ (dom g1 /\ (dom g \ g"
{0c})))) by XBOOLE_1:16
.= dom (f1(#)g) /\ ((dom f \ f"{0c}) /\ (dom g1 /\ dom f /\ (dom g \ g"{
0c}))) by XBOOLE_1:16
.= dom (f1(#)g) /\ ((dom f \ f"{0c}) /\ (dom (g1(#)f) /\ (dom g \ g"{0c}
))) by Th3
.= dom (f1(#)g) /\ (dom (g1(#)f) /\ ((dom f \ f"{0c}) /\ (dom g \ g"{0c}
))) by XBOOLE_1:16
.= dom (f1(#)g) /\ dom (g1(#)f) /\ ((dom f \ f"{0c}) /\ (dom g \ g"{0c})
) by XBOOLE_1:16
.= dom (f1(#)g + g1(#)f) /\ ((dom f \ f"{0c}) /\ (dom g \ g"{0c})) by
VALUED_1:def 1
.= dom (f1(#)g + g1(#)f) /\ (dom (f(#)g) \ (f(#)g)"{0c}) by Th7
.= dom ((f1(#)g + g1(#)f)/(f(#)g)) by Def1;
hence thesis by A1,PARTFUN2:1;
end;
theorem
(f/g)/(f1/g1) = (f(#)(g1|dom(g1^)))/(g(#)f1)
proof
thus (f/g)/(f1/g1) = (f/g)(#)((f1/g1)^) by Th38
.= (f/g)(#)(((g1|dom(g1^)))/f1) by Th42
.= (f(#)(g1|dom(g1^)))/(g(#)f1) by Th41;
end;
theorem
f1/f - g1/g = (f1(#)g - g1(#)f)/(f(#)g)
proof
thus f1/f - g1/g = f1/f + ((-1r)(#) g1)/g by Th39,COMPLEX1:def 4
.= (f1(#)g + (-1r)(#) g1(#)f)/(f(#)g) by Th47
.= (f1(#)g - (g1(#)f))/(f(#)g) by Th17,COMPLEX1:def 4;
end;
theorem
|.f1/f2.| = |.f1.|/|.f2.|
proof
thus |.f1/f2.| = |.f1(#)(f2^).| by Th38
.= |.f1.|(#)|.(f2^).| by Th29
.= |.f1.|(#)((|.f2.|)^) by Th37
.= |.f1.|/|.f2.| by RFUNCT_1:31;
end;
theorem Th51:
(f1+f2)|X = f1|X + f2|X & (f1+f2)|X = f1|X + f2 & (f1+f2)|X = f1 + f2|X
proof
A1: now
let c;
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 VALUED_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 VALUED_1:def 1;
thus ((f1+f2)|X)/.c = (f1+f2)/.c by A2,PARTFUN2:15
.= (((f1/.c))) + (((f2/.c))) by A5,Th1
.= ((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,Th1;
end;
dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ (X /\ X) by VALUED_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 VALUED_1:def 1;
hence (f1+f2)|X = f1|X + f2|X by A1,PARTFUN2:1;
A10: now
let c;
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 VALUED_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 VALUED_1:def 1;
thus ((f1+f2)|X)/.c = (f1+f2)/.c by A11,PARTFUN2:15
.= (((f1/.c))) +(((f2/.c))) by A14,Th1
.= ((f1|X)/.c) +(((f2/.c))) by A16,PARTFUN2:15
.= ((f1|X)+f2)/.c by A17,Th1;
end;
dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ X by VALUED_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 VALUED_1:def 1;
hence (f1+f2)|X = f1|X + f2 by A10,PARTFUN2:1;
A18: now
let c;
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 VALUED_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 VALUED_1:def 1;
thus ((f1+f2)|X)/.c = (f1+f2)/.c by A19,PARTFUN2:15
.= (((f1/.c))) +(((f2/.c))) by A22,Th1
.= (((f1/.c))) +((f2|X)/.c) by A24,PARTFUN2:15
.= (f1+(f2|X))/.c by A25,Th1;
end;
dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ X by VALUED_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 VALUED_1:def 1;
hence thesis by A18,PARTFUN2:1;
end;
theorem Th52:
(f1(#)f2)|X = f1|X (#) f2|X & (f1(#)f2)|X = f1|X (#) f2 & (f1(#)
f2)|X = f1 (#) f2|X
proof
A1: now
let c;
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 Th3;
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 Th3;
thus ((f1(#)f2)|X)/.c = (f1(#)f2)/.c by A2,PARTFUN2:15
.= (((f1/.c))) *(((f2/.c))) by A5,Th3
.= ((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,Th3;
end;
dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ (X /\ X) by Th3
.= 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 Th3;
hence (f1(#)f2)|X = f1|X (#) f2|X by A1,PARTFUN2:1;
A10: now
let c;
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 Th3;
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 Th3;
thus ((f1(#)f2)|X)/.c = (f1(#)f2)/.c by A11,PARTFUN2:15
.= (((f1/.c))) *(((f2/.c))) by A14,Th3
.= ((f1|X)/.c) *(((f2/.c))) by A16,PARTFUN2:15
.= ((f1|X)(#)f2)/.c by A17,Th3;
end;
dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ X by Th3
.= dom f1 /\ X /\ dom f2 by XBOOLE_1:16
.= dom (f1|X) /\ dom f2 by RELAT_1:61
.= dom ((f1|X)(#) f2) by Th3;
hence (f1(#)f2)|X = f1|X (#) f2 by A10,PARTFUN2:1;
A18: now
let c;
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 Th3;
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 Th3;
thus ((f1(#)f2)|X)/.c = (f1(#)f2)/.c by A19,PARTFUN2:15
.= (((f1/.c))) *(((f2/.c))) by A22,Th3
.= (((f1/.c))) *((f2|X)/.c) by A24,PARTFUN2:15
.= (f1(#)(f2|X))/.c by A25,Th3;
end;
dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:61
.= dom f1 /\ dom f2 /\ X by Th3
.= dom f1 /\ (dom f2 /\ X) by XBOOLE_1:16
.= dom f1 /\ dom (f2|X) by RELAT_1:61
.= dom (f1 (#) (f2|X)) by Th3;
hence thesis by A18,PARTFUN2:1;
end;
theorem Th53:
(-f)|X = -(f|X) & (f^)|X = (f|X)^ & (|.f.|)|X = |.(f|X).|
proof
A1: dom ((f^)|X) = dom (f^) /\ X by RELAT_1:61
.= (dom f \ f"{0c}) /\ X by Def2
.= dom f /\ X \ f"{0c} /\ X by XBOOLE_1:50
.= dom (f|X) \ X /\ f"{0c} by RELAT_1:61
.= dom (f|X) \ (f|X)"{0c} by FUNCT_1:70
.= dom ((f|X)^) by Def2;
A2: now
let c;
assume
A3: c in dom ((-f)|X);
then
A4: c in dom (-f) /\ X by RELAT_1:61;
then
A5: c in X by XBOOLE_0:def 4;
A6: c in dom (-f) by A4,XBOOLE_0:def 4;
then c in dom f by Th5;
then c in dom f /\ X by A5,XBOOLE_0:def 4;
then
A7: c in dom (f|X) by RELAT_1:61;
then
A8: c in dom (-(f|X)) by Th5;
thus ((-f)|X)/.c = (-f)/.c by A3,PARTFUN2:15
.= -((f/.c)) by A6,Th5
.= -((f|X)/.c) by A7,PARTFUN2:15
.= (-(f|X))/.c by A8,Th5;
end;
dom ((-f)|X) = dom (-f) /\ X by RELAT_1:61
.= dom f /\ X by Th5
.= dom (f|X) by RELAT_1:61
.= dom (-(f|X)) by Th5;
hence (-f)|X = -(f|X) by A2,PARTFUN2:1;
A9: dom ((f|X)^) c= dom (f|X) by Th6;
now
let c;
assume
A10: c in dom ((f^)|X);
then c in dom (f^) /\ X by RELAT_1:61;
then
A11: c in dom (f^) by XBOOLE_0:def 4;
thus ((f^)|X)/.c = (f^)/.c by A10,PARTFUN2:15
.= ((f/.c))" by A11,Def2
.= ((f|X)/.c)" by A9,A1,A10,PARTFUN2:15
.= ((f|X)^)/.c by A1,A10,Def2;
end;
hence (f^)|X = (f|X)^ by A1,PARTFUN2:1;
A12: dom ((|.f.|)|X) = dom (|.f.|) /\ X by RELAT_1:61
.= dom f /\ X by VALUED_1:def 11
.= dom (f|X) by RELAT_1:61
.= dom (|.(f|X).|) by VALUED_1:def 11;
now
let c;
A13: dom |.f.| = dom f by VALUED_1:def 11;
assume
A14: c in dom ((|.f.|)|X);
then
A15: c in dom (f|X) by A12,VALUED_1:def 11;
c in dom (|.f.|) /\ X by A14,RELAT_1:61;
then
A16: c in dom (|.f.|) by XBOOLE_0:def 4;
thus ((|.f.|)|X).c = (|.f.|).c by A14,FUNCT_1:47
.= |.(f.c).| by VALUED_1:18
.= |.(f/.c).| by A16,A13,PARTFUN1:def 6
.= |.(f|X)/.c.| by A15,PARTFUN2:15
.= |.(f|X).c.| by A15,PARTFUN1:def 6
.= (|.(f|X).|).c by VALUED_1:18;
end;
hence thesis by A12,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|X)+ (-f2)|X by Th51
.= (f1|X) - (f2|X) by Th53;
thus (f1-f2)|X = (f1|X)+ -f2 by Th51
.= (f1|X) - f2;
thus (f1-f2)|X = f1+ (-f2)|X by Th51
.= f1 - (f2|X) by Th53;
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 Th38
.= (f1|X) (#) (f2^|X) by Th52
.= (f1|X) (#) ((f2|X)^) by Th53
.= (f1|X)/(f2|X) by Th38;
thus (f1/f2)|X = (f1(#)(f2^))|X by Th38
.= (f1|X) (#) (f2^) by Th52
.= (f1|X)/f2 by Th38;
thus (f1/f2)|X = (f1(#)(f2^))|X by Th38
.= f1 (#) (f2^)|X by Th52
.= f1 (#) ((f2|X)^) by Th53
.= f1/(f2|X) by Th38;
end;
theorem
(r(#)f)|X = r(#)(f|X)
proof
A1: now
let c;
assume
A2: c in dom ((r(#)f)|X);
then
A3: c in dom (r(#)f) /\ X by RELAT_1:61;
then
A4: c in X by XBOOLE_0:def 4;
A5: c in dom (r(#)f) by A3,XBOOLE_0:def 4;
then c in dom f by Th4;
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 (r(#)(f|X)) by Th4;
thus ((r(#)f)|X)/.c = (r(#)f)/.c by A2,PARTFUN2:15
.= r*((f/.c)) by A5,Th4
.= r*((f|X)/.c) by A6,PARTFUN2:15
.= (r(#)(f|X))/.c by A7,Th4;
end;
dom ((r(#)f)|X) = dom (r(#)f) /\ X by RELAT_1:61
.= dom f /\ X by Th4
.= dom (f|X) by RELAT_1:61
.= dom (r(#)(f|X)) by Th4;
hence thesis by A1,PARTFUN2:1;
end;
begin
::
:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN, TO COMPLEX
::
theorem Th57:
(f1 is total & f2 is total iff f1+f2 is total) & (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 = C & dom f2 = C;
hence dom (f1+f2) = C /\ C by VALUED_1:def 1
.= C;
end;
assume f1+f2 is total;
then dom (f1+f2) = C;
then dom f1 /\ dom f2 = C by VALUED_1:def 1;
then C c= dom f1 & C c= dom f2 by XBOOLE_1:17;
hence dom f1 = C & dom f2 = C;
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 = C & dom f2 = C;
hence dom (f1-f2) = C /\ C by Th2
.= C;
end;
assume f1-f2 is total;
then dom (f1-f2) = C;
then dom f1 /\ dom f2 = C by Th2;
then C c= dom f1 & C c= dom f2 by XBOOLE_1:17;
hence dom f1 = C & dom f2 = C;
end;
thus f1 is total & f2 is total implies f1(#)f2 is total
proof
assume f1 is total & f2 is total;
then dom f1 = C & dom f2 = C;
hence dom (f1(#)f2) = C /\ C by Th3
.= C;
end;
assume f1(#)f2 is total;
then dom (f1(#)f2) = C;
then dom f1 /\ dom f2 = C by Th3;
then C c= dom f1 & C c= dom f2 by XBOOLE_1:17;
hence dom f1 = C & dom f2 = C;
end;
theorem Th58:
f is total iff r(#)f is total
by Th4;
theorem Th59:
f is total iff -f is total
by Th58;
theorem Th60:
f is total iff |.f.| is total
by VALUED_1:def 11;
theorem Th61:
f^ is total iff f"{0} = {} & f is total
proof
thus f^ is total implies f"{0} = {} & f is total
proof
assume f^ is total;
then
A1: dom (f^) = C;
f"{0c} c= C;
then f"{0c} c= dom f \ f"{0c} by A1,Def2;
hence f"{0} = {} by XBOOLE_1:38;
then C = dom f \ {} by A1,Def2;
hence dom f = C;
end;
assume
A2: f"{0} = {} & f is total;
thus dom (f^) = dom f \ f"{0c} by Def2
.= C by A2;
end;
theorem Th62:
f1 is total & f2"{0} = {} & f2 is total iff f1/f2 is total
proof
thus f1 is total & f2"{0} = {} & f2 is total implies f1/f2 is total
proof
assume that
A1: f1 is total and
A2: f2"{0} = {} & f2 is total;
f2^ is total by A2,Th61;
then f1(#)(f2^) is total by A1,Th57;
hence thesis by Th38;
end;
assume f1/f2 is total;
then
A3: f1(#)(f2^) is total by Th38;
hence f1 is total by Th57;
f2^ is total by A3,Th57;
hence thesis by Th61;
end;
theorem
f1 is total & f2 is total implies (f1+f2)/.c = ((f1/.c)) + ((f2/.c)) &
(f1-f2)/.c = ((f1/.c)) - ((f2/.c)) & (f1(#) f2)/.c = ((f1/.c)) * ((f2/.c))
proof
assume
A1: f1 is total & f2 is total;
then f1+f2 is total by Th57;
then dom (f1+f2) = C;
hence (f1+f2)/.c = ((f1/.c)) + ((f2/.c)) by Th1;
f1-f2 is total by A1,Th57;
then dom (f1-f2) = C;
hence (f1-f2)/.c = ((f1/.c)) - ((f2/.c)) by Th2;
f1(#)f2 is total by A1,Th57;
then dom (f1(#)f2) = C;
hence thesis by Th3;
end;
theorem
f is total implies (r(#)f)/.c = r * ((f/.c))
proof
assume f is total;
then r(#)f is total by Th58;
then dom (r(#)f) = C;
hence thesis by Th4;
end;
theorem
f is total implies (-f)/.c = - (f/.c) & (|.f.|).c = |. (f/.c) .|
proof
assume
A1: f is total;
then |.f.| is total by Th60;
then
A2: dom |.f.| = dom f & dom (|.f.|) = C by VALUED_1:def 11;
-f is total by A1,Th59;
then dom (-f) = C;
hence (-f)/.c = - (f/.c) by Th5;
thus (|.f.|).c = |. (f.c) .| by VALUED_1:18
.= |. (f/.c) .| by A2,PARTFUN1:def 6;
end;
theorem
f^ is total implies (f^)/.c = ((f/.c))"
by Def2;
theorem
f1 is total & f2^ is total implies (f1/f2)/.c = ((f1/.c)) *(((f2/.c))) "
proof
assume that
A1: f1 is total and
A2: f2^ is total;
f2"{0c} = {} & f2 is total by A2,Th61;
then f1/f2 is total by A1,Th62;
then dom (f1/f2) = C;
hence thesis by Def1;
end;
begin
::
:: BOUNDED AND CONSTANT PARTIAL FUNCTIONS FROM A DOMAIN, TO COMPLEX
::
Lm3: |.f.| is bounded iff f is bounded
proof
A1: dom f = dom |.f.| by VALUED_1:def 11;
thus |.f.| is bounded implies f is bounded
proof
assume |.f.| is bounded;
then consider r1 being Real such that
A2: for y st y in dom |.f.| holds |.abs(f).y.| < r1;
take r1;
let y;
assume
A3: y in dom f;
then |.abs(f).y.| < r1 by A1,A2;
then |.|.f.y.|.| < r1 by A1,A3,VALUED_1:def 11;
hence thesis;
end;
given r1 such that
A4: for y st y in dom f holds |.f.y.|