Copyright (c) 1990 Association of Mizar Users
environ
vocabulary PARTFUN1, ARYTM, ARYTM_1, RELAT_1, ARYTM_3, BOOLE, FUNCT_1,
FINSEQ_1, SEQ_1, ABSVALUE, FUNCT_3, PARTFUN2, RFUNCT_1;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, FUNCT_1, FUNCT_3, ABSVALUE, RELSET_1, PARTFUN1, PARTFUN2, SEQ_1;
constructors REAL_1, FUNCT_3, ABSVALUE, PARTFUN1, PARTFUN2, SEQ_1, MEMBERED,
XBOOLE_0;
clusters RELSET_1, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, PARTFUN1, XBOOLE_0;
theorems TARSKI, AXIOMS, SUBSET_1, FUNCT_1, FUNCT_3, REAL_1, ABSVALUE,
PARTFUN1, PARTFUN2, RELSET_1, SEQ_1, RELAT_1, XREAL_0, XBOOLE_0,
XBOOLE_1, XCMPLX_0, XCMPLX_1;
schemes SEQ_1;
begin
reserve x,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,REAL;
reserve r,r1,r2,p,p1 for real number;
Lm1: (-1)"=-1;
canceled;
theorem Th2:
0<=p & 0<=r & p<=p1 & r<=r1 implies p*r<=p1*r1
proof assume A1: 0<=p & 0<=r & p<=p1 & r<=r1;
then A2: p*r1<=p1*r1 by AXIOMS:25;
p*r<=p*r1 by A1,AXIOMS:25;
hence thesis by A2,AXIOMS:22;
end;
::
::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN, TO THE SET OF REAL NUMBERS
::
definition let C;let f1,f2;
canceled 3;
func f1/f2 -> PartFunc of C,REAL means :Def4:
dom it = dom f1 /\ (dom f2 \ f2"{0}) &
for c st c in dom it holds it.c = f1.c * (f2.c)";
existence
proof
defpred P[set] means $1 in dom f1 /\ (dom f2 \ f2"{0});
deffunc G(set)=f1.$1 * (f2.$1)";
consider F being PartFunc of C,REAL 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 = G(c) from LambdaPFD';
take F;
thus dom F = dom f1 /\ (dom f2 \ f2"{0}) by A1,SUBSET_1:8;
let c; assume c in dom F; hence thesis by A2;
end;
uniqueness
proof
deffunc F(set)=f1.$1 * (f2.$1)";
for f,g being PartFunc of C,REAL st
(dom f=dom f1 /\ (dom f2 \ f2"{0})
& for c be Element of C st c in dom f holds f.c = F(c)) &
(dom g=dom f1 /\ (dom f2 \ f2"{0})
& for c be Element of C st c in dom g holds g.c = F(c))
holds f = g from UnPartFuncD';
hence thesis;
end;
end;
definition let C; let f;
canceled 3;
func f^ -> PartFunc of C,REAL means :Def8:
dom it = dom f \ f"{0} & for c st c in dom it holds it.c = (f.c)";
existence
proof
defpred P[set] means $1 in dom f \ f"{0};
deffunc H(set)=(f.$1)";
consider F being PartFunc of C,REAL 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 = H(c) from LambdaPFD';
take F;
thus dom F = dom f \ f"{0} by A1,SUBSET_1:8;
let c; assume c in dom F; hence thesis by A2;
end;
uniqueness
proof
deffunc H(Element of C)=(f.$1)";
for f1,g being PartFunc of C,REAL st
( dom f1= (dom f \ f"{0})
& for c be Element of C st c in dom f1 holds f1.c = H(c) ) &
(dom g= (dom f \ f"{0})
& for c be Element of C st c in dom g holds g.c = H(c))
holds f1 = g from UnPartFuncD';
hence thesis;
end;
end;
canceled 8;
theorem Th11: dom (g^) c= dom g & dom g /\ (dom g \ g"{0}) = dom g \ g"{0}
proof
dom (g^) = dom g \ g"{0} by Def8; hence dom (g^) c= dom g by XBOOLE_1:36;
dom g \ g"{0} c= dom g by XBOOLE_1:36; hence thesis by XBOOLE_1:28;
end;
theorem Th12:
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; assume A1: x in dom (f1(#)f2) \ (f1(#)f2)"{0};
then A2: x in dom (f1(#)f2) & not x in (f1(#)f2)"{0} by XBOOLE_0:def 4;
reconsider x1=x as Element of C by A1;
not (f1(#)f2).x1 in {0} by A2,FUNCT_1:def 13;
then (f1(#)f2).x1 <> 0 by TARSKI:def 1;
then f1.x1 * f2.x1 <> 0 by A2,SEQ_1:def 5;
then f1.x1 <> 0 & f2.x1 <> 0;
then x1 in dom f1 /\ dom f2 & not f1.x1 in {0} & not f2.x1 in {0}
by A2,SEQ_1:def 5,TARSKI:def 1;
then x1 in dom f1 & x1 in dom f2 & not x1 in (f1)"{0} & not f2.x1 in {0}
by FUNCT_1:def 13,XBOOLE_0:def 3;
then x in dom f1 \ (f1)"{0} & x1 in dom f2 & not x1 in (f2)"{0}
by FUNCT_1:def 13,XBOOLE_0:def 4;
then x in dom f1 \ (f1)"{0} & x in dom f2 \ (f2)"{0} by XBOOLE_0:def 4;
hence x in (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0}) by XBOOLE_0:def 3;
end;
thus (dom f1 \ (f1)"{0}) /\
(dom f2 \ (f2)"{0}) c= dom (f1(#)f2) \ (f1(#)f2)"{0}
proof let x; assume A3: x in (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{0});
then x in dom f1 \ (f1)"{0} & x in dom f2 \ (f2)"{0} by XBOOLE_0:def 3;
then A4: x in dom f1 & not x in (f1)"{0} & x in dom f2 & not x in (f2)"{0}
by XBOOLE_0:def 4;
reconsider x1=x as Element of C by A3;
not f1.x1 in {0} by A4,FUNCT_1:def 13;
then A5: f1.x1 <> 0 by TARSKI:def 1;
not f2.x1 in {0} by A4,FUNCT_1:def 13;
then f2.x1 <> 0 by TARSKI:def 1;
then A6: f1.x1 * f2.x1 <>0 by A5,XCMPLX_1:6;
x1 in dom f1 /\ dom f2 by A4,XBOOLE_0:def 3;
then A7: x1 in dom (f1(#)f2) by SEQ_1:def 5;
then (f1(#)f2).x1 <> 0 by A6,SEQ_1:def 5;
then not (f1(#)f2).x1 in {0} by TARSKI:def 1;
then not x in (f1(#)f2)"{0} by FUNCT_1:def 13;
hence x in dom (f1(#)f2) \ (f1(#)f2)"{0}by A7,XBOOLE_0:def 4;
end;
end;
theorem Th13:
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"{0} by A1,Def8;
then A4: c in dom f & not c in f"{0} by XBOOLE_0:def 4;
now per cases by A4,FUNCT_1:def 13;
suppose not c in dom f; hence contradiction by A3,XBOOLE_0:def 4;
suppose not f.c in {0}; hence contradiction by A2,TARSKI:def 1;
end;
hence contradiction;
end;
theorem Th14:
(f^)"{0} = {}
proof assume A1: (f^)"{0} <> {};
consider x being Element of (f^)"{0};
A2: x in dom (f^) & ((f^) qua Function).x in {0} by A1,FUNCT_1:def 13;
then reconsider x as Element of C;
(f^).x = 0 by A2,TARSKI:def 1;
then A3: (f.x)" = 0 by A2,Def8;
x in dom f \ f"{0} by A2,Def8;
then x in dom f & not x in f"{0} by XBOOLE_0:def 4;
then not f.x in {0} by FUNCT_1:def 13;
then f.x <> 0 by TARSKI:def 1;
hence contradiction by A3,XCMPLX_1:203;
end;
theorem Th15:
(abs(f))"{0} = f"{0} & (-f)"{0} = f"{0}
proof
now let c;
thus c in (abs(f))"{0} implies c in f"{0}
proof assume c in (abs(f))"{0};
then c in dom (abs(f)) & (abs(f)).c in {0} by FUNCT_1:def 13;
then c in dom (abs(f)) & (abs(f)).c = 0 by TARSKI:def 1;
then c in dom (abs(f)) & abs(f.c) = 0 by SEQ_1:def 10;
then c in dom f & f.c = 0 by ABSVALUE:7,SEQ_1:def 10;
then c in dom f & f.c in {0} by TARSKI:def 1;
hence thesis by FUNCT_1:def 13;
end;
assume c in (f)"{0};
then c in dom f & f.c in {0} by FUNCT_1:def 13;
then c in dom (abs(f)) & f.c = 0 by SEQ_1:def 10,TARSKI:def 1;
then c in dom (abs(f)) & abs(f.c) = 0 by ABSVALUE:7;
then c in dom (abs(f)) & (abs(f)).c = 0 by SEQ_1:def 10;
then c in dom (abs(f)) & (abs(f)).c in {0} by TARSKI:def 1;
hence c in (abs(f))"{0} by FUNCT_1:def 13;
end;
hence (abs(f))"{0} = f"{0} by SUBSET_1:8;
now let c;
thus c in (-f)"{0} implies c in f"{0}
proof assume c in (-f)"{0};
then c in dom (-f) & (-f).c in {0} by FUNCT_1:def 13;
then c in dom (-f) & (-f).c = 0 by TARSKI:def 1;
then c in dom (-f) & --(f.c) = -0 by SEQ_1:def 7;
then c in dom f & f.c in {0} by SEQ_1:def 7,TARSKI:def 1;
hence thesis by FUNCT_1:def 13;
end;
assume c in (f)"{0};
then c in dom f & f.c in {0} by FUNCT_1:def 13;
then c in dom (-f) & f.c = 0 by SEQ_1:def 7,TARSKI:def 1;
then c in dom (-f) & (-f).c = 0 by REAL_1:26,SEQ_1:def 7;
then c in dom (-f) & (-f).c in {0} by TARSKI:def 1;
hence c in (-f)"{0} by FUNCT_1:def 13;
end;
hence thesis by SUBSET_1:8;
end;
theorem Th16:
dom (f^^) = dom (f|(dom (f^)))
proof
dom (f^) = dom f \ f"{0} by Def8;
then A1: dom (f^) c= dom f by XBOOLE_1:36;
thus dom (f^^) = dom (f^) \(f^)"{0} by Def8
.= dom (f^) \ {} by Th14
.= dom f /\ dom (f^) by A1,XBOOLE_1:28
.= dom (f|(dom (f^))) by RELAT_1:90;
end;
theorem Th17:
r<>0 implies (r(#)f)"{0} = f"{0}
proof assume A1: r<>0;
now let c;
thus c in (r(#)f)"{0} implies c in f"{0}
proof assume c in (r(#)f)"{0};
then c in dom (r(#)f) & (r(#)f).c in {0} by FUNCT_1:def 13;
then c in dom (r(#)f) & (r(#)f).c = 0 by TARSKI:def 1;
then c in dom (r(#)f) & r*f.c = 0 by SEQ_1:def 6;
then c in dom f & f.c = 0 by A1,SEQ_1:def 6,XCMPLX_1:6;
then c in dom f & f.c in {0} by TARSKI:def 1;
hence thesis by FUNCT_1:def 13;
end;
assume c in (f)"{0};
then c in dom f & f.c in {0} by FUNCT_1:def 13;
then c in dom f & f.c = 0 by TARSKI:def 1;
then c in dom (r(#)f) & r*f.c = 0 by SEQ_1:def 6;
then c in dom (r(#)f) & (r(#)f).c = 0 by SEQ_1:def 6;
then c in dom (r(#)f) & (r(#)f).c in {0} by TARSKI:def 1;
hence c in (r(#)f)"{0} by FUNCT_1:def 13;
end;
hence thesis by SUBSET_1:8;
end;
::
:: BASIC PROPERTIES OF OPERATIONS
::
canceled;
theorem
(f1 + f2) + f3 = f1 + (f2 + f3)
proof
A1: dom (f1 + f2 + f3) = dom (f1 + f2) /\ dom f3 by SEQ_1:def 3
.= dom f1 /\ dom f2 /\ dom f3 by SEQ_1:def 3
.= dom f1 /\ (dom f2 /\ dom f3) by XBOOLE_1:16
.= dom f1 /\ dom (f2 + f3) by SEQ_1:def 3
.= dom (f1 + (f2 + f3)) by SEQ_1:def 3;
now let c; assume A2: c in dom (f1 + f2 + f3);
then c in dom f1 /\ dom (f2 + f3) by A1,SEQ_1:def 3;
then A3: c in dom (f2 + f3) by XBOOLE_0:def 3;
c in dom (f1 + f2) /\ dom f3 by A2,SEQ_1:def 3;
then A4: c in dom (f1 + f2) by XBOOLE_0:def 3;
thus (f1 + f2 + f3).c = (f1 + f2).c + f3.c by A2,SEQ_1:def 3
.= f1.c + f2.c + f3.c by A4,SEQ_1:def 3
.= f1.c + (f2.c + f3.c) by XCMPLX_1:1
.= f1.c + (f2 + f3).c by A3,SEQ_1:def 3
.= (f1 + (f2 + f3)).c by A1,A2,SEQ_1:def 3;
end;
hence thesis by A1,PARTFUN1:34;
end;
canceled;
theorem Th21:
(f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
proof
A1: dom (f1 (#) f2 (#) f3) = dom (f1 (#) f2) /\ dom f3 by SEQ_1:def 5
.= dom f1 /\ dom f2 /\ dom f3 by SEQ_1:def 5
.= dom f1 /\ (dom f2 /\ dom f3) by XBOOLE_1:16
.= dom f1 /\ dom (f2 (#) f3) by SEQ_1:def 5
.= dom (f1 (#) (f2 (#) f3)) by SEQ_1:def 5;
now let c; assume A2: c in dom (f1(#)f2(#)f3);
then c in dom f1 /\ dom (f2(#)f3) by A1,SEQ_1:def 5;
then A3: c in dom (f2 (#) f3) by XBOOLE_0:def 3;
c in dom (f1 (#) f2) /\ dom f3 by A2,SEQ_1:def 5;
then A4: c in dom (f1 (#) f2) by XBOOLE_0:def 3;
thus (f1 (#) f2 (#) f3).c = (f1 (#) f2).c * f3.c by A2,SEQ_1:def 5
.= f1.c * f2.c * f3.c by A4,SEQ_1:def 5
.= f1.c * (f2.c * f3.c) by XCMPLX_1:4
.= f1.c * (f2 (#) f3).c by A3,SEQ_1:def 5
.= (f1 (#) (f2 (#) f3)).c by A1,A2,SEQ_1:def 5;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem Th22:
(f1 + f2) (#) f3=f1 (#) f3 + f2 (#) f3
proof
A1: dom ((f1 + f2) (#) f3) = dom (f1 + f2) /\ dom f3 by SEQ_1:def 5
.= dom f1 /\ dom f2 /\ (dom f3 /\ dom f3) by SEQ_1:def 3
.= 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 SEQ_1:def 5
.= dom (f1 (#) f3) /\ dom (f2 (#) f3) by SEQ_1:def 5
.= dom (f1 (#) f3 + f2 (#) f3) by SEQ_1:def 3;
now let c; assume A2: c in dom ((f1 + f2)(#)f3);
then c in dom (f1(#)f3) /\ dom (f2(#)f3) by A1,SEQ_1:def 3;
then A3: c in dom (f1(#)f3) & c in dom (f2 (#) f3) by XBOOLE_0:def 3;
c in dom (f1 + f2) /\ dom f3 by A2,SEQ_1:def 5;
then A4: c in dom (f1 + f2) by XBOOLE_0:def 3;
thus ((f1 + f2) (#) f3).c = (f1 + f2).c * f3.c by A2,SEQ_1:def 5
.= (f1.c + f2.c) * f3.c by A4,SEQ_1:def 3
.= f1.c * f3.c + f2.c * f3.c by XCMPLX_1:8
.= (f1 (#) f3).c + f2.c* f3.c by A3,SEQ_1:def 5
.= (f1 (#) f3).c + (f2 (#) f3).c by A3,SEQ_1:def 5
.=((f1 (#) f3) + (f2 (#) f3)).c by A1,A2,SEQ_1:def 3;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem
f3 (#) (f1 + f2)=f3(#)f1 + f3(#)f2 by Th22;
theorem Th24:
r(#)(f1(#)f2)=r(#)f1(#)f2
proof
A1: dom (r(#)(f1 (#) f2)) = dom (f1 (#) f2) by SEQ_1:def 6
.= dom f1 /\ dom f2 by SEQ_1:def 5
.= dom (r(#)f1) /\ dom f2 by SEQ_1:def 6
.= dom (r(#)f1(#)f2) by SEQ_1:def 5;
now let c; assume A2: c in dom (r(#)(f1(#)f2));
then c in dom (r(#)f1) /\ dom f2 by A1,SEQ_1:def 5;
then A3: c in dom (r(#)f1) & c in dom f2 by XBOOLE_0:def 3;
A4: c in dom (f1(#)f2) by A2,SEQ_1:def 6;
thus (r(#)(f1(#)f2)).c = r * (f1(#)f2).c by A2,SEQ_1:def 6
.= r*(f1.c * f2.c) by A4,SEQ_1:def 5
.= (r*f1.c) * f2.c by XCMPLX_1:4
.= (r(#)f1).c * f2.c by A3,SEQ_1:def 6
.= (r(#)f1 (#) f2).c by A1,A2,SEQ_1:def 5;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem Th25:
r(#)(f1(#)f2)=f1(#)(r(#)f2)
proof
A1: dom (r(#)(f1 (#) f2)) = dom (f1 (#) f2) by SEQ_1:def 6
.= dom f1 /\ dom f2 by SEQ_1:def 5
.= dom f1 /\ dom (r(#)f2) by SEQ_1:def 6
.= dom (f1(#)(r(#)f2)) by SEQ_1:def 5;
now let c; assume A2: c in dom (r(#)(f1(#)f2));
then c in dom f1 /\ dom (r(#)f2) by A1,SEQ_1:def 5;
then A3: c in dom f1 & c in dom (r(#)f2) by XBOOLE_0:def 3;
A4: c in dom (f1(#)f2) by A2,SEQ_1:def 6;
thus (r(#)(f1(#)f2)).c = r * (f1(#)f2).c by A2,SEQ_1:def 6
.= r * (f1.c * f2.c) by A4,SEQ_1:def 5
.= f1.c * (r * f2.c) by XCMPLX_1:4
.= f1.c * (r(#)f2).c by A3,SEQ_1:def 6
.= (f1(#)(r(#)f2)).c by A1,A2,SEQ_1:def 5;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem Th26:
(f1 - f2)(#)f3=f1(#)f3 - f2(#)f3
proof
A1: dom ((f1 - f2) (#) f3) = dom (f1 - f2) /\ dom f3 by SEQ_1:def 5
.= dom f1 /\ dom f2 /\ (dom f3 /\ dom f3) by SEQ_1:def 4
.= 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 SEQ_1:def 5
.= dom (f1 (#) f3) /\ dom (f2 (#) f3) by SEQ_1:def 5
.= dom (f1 (#) f3 - f2 (#) f3) by SEQ_1:def 4;
now let c; assume A2: c in dom ((f1 - f2)(#)f3);
then c in dom (f1(#)f3) /\ dom (f2(#)f3) by A1,SEQ_1:def 4;
then A3: c in dom (f1(#)f3) & c in dom (f2 (#) f3) by XBOOLE_0:def 3;
c in dom (f1 - f2) /\ dom f3 by A2,SEQ_1:def 5;
then A4: c in dom (f1 - f2) by XBOOLE_0:def 3;
thus ((f1 - f2) (#) f3).c = (f1 - f2).c * f3.c by A2,SEQ_1:def 5
.= (f1.c - f2.c) * f3.c by A4,SEQ_1:def 4
.= f1.c * f3.c - f2.c * f3.c by XCMPLX_1:40
.= (f1 (#) f3).c - f2.c * f3.c by A3,SEQ_1:def 5
.= (f1 (#) f3).c - (f2 (#) f3).c by A3,SEQ_1:def 5
.=((f1 (#) f3) - (f2 (#) f3)).c by A1,A2,SEQ_1:def 4;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem
f3(#)f1 - f3(#)f2 = f3(#)(f1 - f2) by Th26;
theorem
r(#)(f1 + f2) = r(#)f1 + r(#)f2
proof
A1: dom (r(#)(f1 + f2)) = dom (f1 + f2) by SEQ_1:def 6
.= dom f1 /\ dom f2 by SEQ_1:def 3
.= dom f1 /\ dom (r(#)f2) by SEQ_1:def 6
.= dom (r(#)f1) /\ dom (r(#)f2) by SEQ_1:def 6
.= dom (r(#)f1 + r(#)f2) by SEQ_1:def 3;
now let c; assume A2: c in dom (r(#)(f1 + f2));
then c in dom (r(#)f1) /\ dom (r(#)f2) by A1,SEQ_1:def 3;
then A3: c in dom (r(#)f1) & c in dom (r(#)f2) by XBOOLE_0:def 3;
A4: c in dom (f1 + f2) by A2,SEQ_1:def 6;
thus (r(#)(f1 + f2)).c = r * (f1 + f2).c by A2,SEQ_1:def 6
.= r * (f1.c + f2.c) by A4,SEQ_1:def 3
.= r * f1.c + r * f2.c by XCMPLX_1:8
.= (r(#)f1).c + r * f2.c by A3,SEQ_1:def 6
.= (r(#)f1).c + (r(#)f2).c by A3,SEQ_1:def 6
.= (r(#)f1 + r(#)f2).c by A1,A2,SEQ_1:def 3;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem Th29:
(r*p)(#)f = r(#)(p(#)f)
proof
A1: dom ((r*p) (#) f) = dom f by SEQ_1:def 6
.= dom (p(#)f) by SEQ_1:def 6
.= dom (r(#)(p(#)f)) by SEQ_1:def 6;
now let c; assume A2: c in dom ((r*p)(#)f);
then A3: c in dom (p(#)f) by A1,SEQ_1:def 6;
thus ((r*p)(#)f).c = r*p * f.c by A2,SEQ_1:def 6
.= r*(p * f.c) by XCMPLX_1:4
.= r * (p(#)f).c by A3,SEQ_1:def 6
.= (r(#)(p(#)f)).c by A1,A2,SEQ_1:def 6;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem
r(#)(f1 - f2) = r(#)f1 - r(#)f2
proof
A1: dom (r(#)(f1 - f2)) = dom (f1 - f2) by SEQ_1:def 6
.= dom f1 /\ dom f2 by SEQ_1:def 4
.= dom f1 /\ dom (r(#)f2) by SEQ_1:def 6
.= dom (r(#)f1) /\ dom (r(#)f2) by SEQ_1:def 6
.= dom (r(#)f1 - r(#)f2) by SEQ_1:def 4;
now let c; assume A2: c in dom (r(#)(f1 - f2));
then c in dom (r(#)f1) /\ dom (r(#)f2) by A1,SEQ_1:def 4;
then A3: c in dom (r(#)f1) & c in dom (r(#)f2) by XBOOLE_0:def 3;
A4: c in dom (f1 - f2) by A2,SEQ_1:def 6;
thus (r(#)(f1 - f2)).c = r * (f1 - f2).c by A2,SEQ_1:def 6
.= r * (f1.c - f2.c) by A4,SEQ_1:def 4
.= r * f1.c - r * f2.c by XCMPLX_1:40
.= (r(#)f1).c - r * f2.c by A3,SEQ_1:def 6
.= (r(#)f1).c - (r(#)f2).c by A3,SEQ_1:def 6
.= (r(#)f1 - r(#)f2).c by A1,A2,SEQ_1:def 4;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem
f1-f2 = (-1)(#)(f2-f1)
proof
A1: dom (f1 - f2) = dom f2 /\ dom f1 by SEQ_1:def 4
.= dom (f2 - f1) by SEQ_1:def 4
.= dom ((-1)(#)(f2 - f1)) by SEQ_1:def 6;
now let c such that A2: c in dom (f1-f2);
A3: dom (f1 - f2) = dom f2 /\ dom f1 by SEQ_1:def 4
.= dom (f2 - f1) by SEQ_1:def 4;
thus (f1 - f2).c = f1.c - f2.c by A2,SEQ_1:def 4
.= 1*(-(f2.c - f1.c)) by XCMPLX_1:143
.= (-1)*(f2.c - f1.c) by XCMPLX_1:176
.= (-1)*((f2 - f1).c) by A2,A3,SEQ_1:def 4
.= ((-1)(#)(f2 - f1)).c by A1,A2,SEQ_1:def 6;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem
f1 - (f2 + f3) = f1 - f2 - f3
proof
A1: dom (f1 - (f2 + f3)) = dom f1 /\ dom (f2 + f3) by SEQ_1:def 4
.= dom f1 /\ (dom f2 /\ dom f3) by SEQ_1:def 3
.= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom (f1 - f2) /\ dom f3 by SEQ_1:def 4
.= dom (f1 - f2 - f3) by SEQ_1:def 4;
now let c; assume A2: c in dom (f1 - (f2 + f3));
then c in dom (f1 - f2) /\ dom f3 by A1,SEQ_1:def 4;
then A3: c in dom (f1 - f2) by XBOOLE_0:def 3;
c in dom f1 /\ dom (f2 + f3) by A2,SEQ_1:def 4;
then A4: c in dom (f2 + f3) by XBOOLE_0:def 3;
thus (f1 - (f2 + f3)).c = f1.c - (f2 + f3).c by A2,SEQ_1:def 4
.= f1.c - (f2.c + f3.c) by A4,SEQ_1:def 3
.= f1.c - f2.c - f3.c by XCMPLX_1:36
.= (f1 - f2).c - f3.c by A3,SEQ_1:def 4
.= (f1 - f2 - f3).c by A1,A2,SEQ_1:def 4;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem Th33:
1(#)f = f
proof
A1: dom (1(#)f) = dom f by SEQ_1:def 6;
now let c; assume c in dom (1(#)f);
hence (1(#)f).c = 1 * f.c by SEQ_1:def 6
.= f.c;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem
f1 - (f2 - f3) = f1 - f2 + f3
proof
A1: dom (f1 - (f2 - f3)) = dom f1 /\ dom (f2 - f3) by SEQ_1:def 4
.= dom f1 /\ (dom f2 /\ dom f3) by SEQ_1:def 4
.= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom (f1 - f2) /\ dom f3 by SEQ_1:def 4
.= dom (f1 - f2 + f3) by SEQ_1:def 3;
now let c; assume A2: c in dom (f1 - (f2 - f3));
then c in dom (f1 - f2) /\ dom f3 by A1,SEQ_1:def 3;
then A3: c in dom (f1 - f2) by XBOOLE_0:def 3;
c in dom f1 /\ dom (f2 - f3) by A2,SEQ_1:def 4;
then A4: c in dom (f2 - f3) by XBOOLE_0:def 3;
thus (f1 - (f2 - f3)).c = f1.c - (f2 - f3).c by A2,SEQ_1:def 4
.= f1.c - (f2.c - f3.c) by A4,SEQ_1:def 4
.= f1.c - f2.c + f3.c by XCMPLX_1:37
.= (f1 - f2).c + f3.c by A3,SEQ_1:def 4
.= (f1 - f2 + f3).c by A1,A2,SEQ_1:def 3;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem
f1 + (f2 - f3) =f1 + f2 - f3
proof
A1: dom (f1 + (f2 - f3)) = dom f1 /\ dom (f2 - f3) by SEQ_1:def 3
.= dom f1 /\ (dom f2 /\ dom f3) by SEQ_1:def 4
.= dom f1 /\ dom f2 /\ dom f3 by XBOOLE_1:16
.= dom (f1 + f2) /\ dom f3 by SEQ_1:def 3
.= dom (f1 + f2 - f3) by SEQ_1:def 4;
now let c; assume A2: c in dom (f1 + (f2 - f3));
then c in dom (f1 + f2) /\ dom f3 by A1,SEQ_1:def 4;
then A3: c in dom (f1 + f2) by XBOOLE_0:def 3;
c in dom f1 /\ dom (f2 - f3) by A2,SEQ_1:def 3;
then A4: c in dom (f2 - f3) by XBOOLE_0:def 3;
thus (f1 + (f2 - f3)).c = f1.c + (f2 - f3).c by A2,SEQ_1:def 3
.= f1.c + (f2.c - f3.c) by A4,SEQ_1:def 4
.= f1.c + f2.c - f3.c by XCMPLX_1:29
.= (f1 + f2).c - f3.c by A3,SEQ_1:def 3
.= (f1 + f2 - f3).c by A1,A2,SEQ_1:def 4;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem Th36:
abs(f1(#)f2) = abs(f1)(#)abs(f2)
proof
A1: dom (abs(f1 (#) f2)) = dom (f1 (#) f2) by SEQ_1:def 10
.= dom f1 /\ dom f2 by SEQ_1:def 5
.= dom f1 /\ dom (abs(f2)) by SEQ_1:def 10
.= dom (abs(f1)) /\ dom (abs(f2)) by SEQ_1:def 10
.= dom (abs(f1)(#)abs(f2)) by SEQ_1:def 5;
now let c; assume A2: c in dom (abs(f1 (#) f2));
then c in dom (abs(f1)) /\ dom (abs(f2)) by A1,SEQ_1:def 5;
then A3: c in dom (abs(f1)) & c in dom (abs(f2)) by XBOOLE_0:def 3;
A4: c in dom (f1 (#) f2) by A2,SEQ_1:def 10;
thus (abs(f1(#)f2)).c = abs((f1(#)f2).c) by A2,SEQ_1:def 10
.= abs(f1.c * f2.c) by A4,SEQ_1:def 5
.= abs(f1.c) * abs(f2.c) by ABSVALUE:10
.= ((abs(f1)).c) * abs(f2.c) by A3,SEQ_1:def 10
.= ((abs(f1)).c) * (abs(f2)).c by A3,SEQ_1:def 10
.= (abs(f1)(#)abs(f2)).c by A1,A2,SEQ_1:def 5;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem
abs(r(#)f) = abs(r)(#)abs(f)
proof
A1: dom (abs(r(#)f)) = dom (r(#)f) by SEQ_1:def 10
.= dom f by SEQ_1:def 6
.= dom (abs(f)) by SEQ_1:def 10
.= dom (abs(r)(#)abs(f)) by SEQ_1:def 6;
now let c; assume A2: c in dom (abs(r(#)f));
then A3: c in dom (abs(f)) by A1,SEQ_1:def 6;
A4: c in dom (r(#)f) by A2,SEQ_1:def 10;
thus (abs(r(#)f)).c = abs((r(#)f).c) by A2,SEQ_1:def 10
.=abs(r*(f.c)) by A4,SEQ_1:def 6
.=abs(r)*abs(f.c) by ABSVALUE:10
.=abs(r)*(abs(f)).c by A3,SEQ_1:def 10
.=(abs(r)(#)abs(f)).c by A1,A2,SEQ_1:def 6;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem Th38:
-f = (-1)(#)f
proof
A1: dom (-f) = dom f by SEQ_1:def 7
.= dom ((-1)(#)f) by SEQ_1:def 6;
now let c; assume A2: c in dom ((-1)(#)f);
hence (-f).c = 1*(-f.c) by A1,SEQ_1:def 7
.= (-1) * f.c by XCMPLX_1:176
.= ((-1)(#)f).c by A2,SEQ_1:def 6;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem Th39:
-(-f) = f
proof
thus -(-f) = (-1)(#)(-f) by Th38
.= (-1)(#)((-1)(#)f) by Th38
.= ((-1)*(-1))(#)f by Th29
.= f by Th33;
end;
theorem Th40:
f1 - f2 = f1 + -f2
proof
A1: dom (f1 - f2) = dom f1 /\ dom f2 by SEQ_1:def 4
.= dom f1 /\ dom (-f2) by SEQ_1:def 7
.= dom (f1 + -f2) by SEQ_1:def 3;
now let c; assume A2: c in dom (f1+-f2);
then c in dom f1 /\ dom (-f2) by SEQ_1:def 3;
then A3: c in dom (-f2) by XBOOLE_0:def 3;
thus (f1 + -f2).c = f1.c + (-f2).c by A2,SEQ_1:def 3
.= f1.c + -(f2.c) by A3,SEQ_1:def 7
.= f1.c - f2.c by XCMPLX_0:def 8
.= (f1-f2).c by A1,A2,SEQ_1:def 4;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem
f1 - (-f2) = f1 + f2
proof
thus f1 - (-f2) = f1 + (-(-f2)) by Th40
.= f1 + f2 by Th39;
end;
theorem Th42:
f^^ = f|(dom (f^))
proof
A1: dom (f^^) = dom (f|(dom (f^))) by Th16;
now let c; assume A2: c in dom (f^^);
then c in dom f /\ dom (f^) by A1,RELAT_1:90;
then A3:c in dom f & c in dom (f^) by XBOOLE_0:def 3;
thus (f^^).c = ((f^).c)" by A2,Def8
.= ((f.c)")" by A3,Def8
.= (f|(dom (f^))).c by A1,A2,FUNCT_1:70;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem Th43:
(f1(#)f2)^ = (f1^)(#)(f2^)
proof
A1: dom ((f1(#)f2)^) = dom (f1(#)f2) \ (f1(#)f2)"{0} by Def8
.= (dom f1 \ f1"{0}) /\ (dom f2 \ (f2)"{0}) by Th12
.= dom (f1^) /\ (dom f2 \ (f2)"{0}) by Def8
.= dom (f1^) /\ dom (f2^) by Def8
.= dom ((f1^) (#) (f2^)) by SEQ_1:def 5;
now let c; assume A2: c in dom ((f1(#)f2)^);
then c in dom (f1^) /\ dom (f2^) by A1,SEQ_1:def 5;
then A3: c in dom (f1^) & c in dom (f2^) by XBOOLE_0:def 3;
c in dom (f1(#)f2) \ (f1(#)f2)"{0} by A2,Def8;
then A4: c in dom (f1(#)f2) by XBOOLE_0:def 4;
thus ((f1(#)f2)^).c = ((f1(#)f2).c)" by A2,Def8
.= (f1.c * f2.c)" by A4,SEQ_1:def 5
.= (f1.c)"* (f2.c)" by XCMPLX_1:205
.= ((f1^).c)*(f2.c)" by A3,Def8
.= ((f1^).c) *((f2^).c) by A3,Def8
.= ((f1^) (#) (f2^)).c by A1,A2,SEQ_1:def 5;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem Th44:
r<>0 implies (r(#)f)^ = r" (#) (f^)
proof assume A1: r<>0;
A2: dom ((r(#)f)^) = dom (r(#)f) \ (r(#)f)"{0} by Def8
.= dom (r(#)f) \ f"{0} by A1,Th17
.= dom f \ f"{0} by SEQ_1:def 6
.= dom (f^) by Def8
.= dom (r"(#)(f^)) by SEQ_1:def 6;
now let c; assume A3: c in dom ((r(#)f)^);
then c in dom (r(#)f) \ (r(#)f)"{0} by Def8;
then A4: c in dom (r(#)f) by XBOOLE_0:def 4;
A5: c in dom (f^) by A2,A3,SEQ_1:def 6;
thus ((r(#)f)^).c = ((r(#)f).c)" by A3,Def8
.= (r*(f.c))" by A4,SEQ_1:def 6
.= r"* (f.c)" by XCMPLX_1:205
.= r"* ((f^).c) by A5,Def8
.= (r" (#) (f^)).c by A2,A3,SEQ_1:def 6;
end;
hence thesis by A2,PARTFUN1:34;
end;
theorem Th45:
(-f)^ = (-1)(#)(f^)
proof
thus (-f)^=((-1)(#)f)^ by Th38
.= (-1)(#)(f^) by Lm1,Th44;
end;
theorem Th46:
(abs(f))^ = abs((f^))
proof
A1: dom ((abs(f))^) = dom (abs(f)) \ (abs(f))"{0} by Def8
.= dom f \ (abs(f))"{0} by SEQ_1:def 10
.= dom f \ f"{0} by Th15
.= dom (f^) by Def8
.= dom (abs((f^))) by SEQ_1:def 10;
now let c; assume A2: c in dom ((abs(f))^);
then c in dom (abs(f)) \ (abs(f))"{0} by Def8;
then A3: c in dom (abs(f)) by XBOOLE_0:def 4;
A4: c in dom (f^) by A1,A2,SEQ_1:def 10;
thus ((abs(f))^).c = ((abs(f)).c)" by A2,Def8
.= (abs(f.c ))" by A3,SEQ_1:def 10
.= 1/abs(f.c ) by XCMPLX_1:217
.= abs(1/f.c ) by ABSVALUE:15
.= abs((f.c)" ) by XCMPLX_1:217
.= abs((f^).c ) by A4,Def8
.= (abs((f^))).c by A1,A2,SEQ_1:def 10;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem Th47:
f/g = f(#) (g^)
proof
A1: dom (f/g) = dom f /\ (dom g \ g"{0}) by Def4
.= dom f /\ dom (g^) by Def8
.= dom (f(#)(g^)) by SEQ_1:def 5;
now let c; assume A2: c in dom (f/g);
then c in dom f /\ (dom g \ g"{0}) by Def4;
then A3: c in dom f /\ dom (g^) by Def8;
then A4: c in dom (g^) by XBOOLE_0:def 3;
A5: c in dom (f (#) (g^)) by A3,SEQ_1:def 5;
thus (f/g).c = f.c * (g.c)" by A2,Def4
.= f.c * (g^).c by A4,Def8
.= (f (#) (g^)).c by A5,SEQ_1:def 5;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem Th48:
r(#)(g/f) = (r(#)g)/f
proof
thus r(#)(g/f) = r(#)(g(#)(f^)) by Th47
.= (r(#)g)(#)(f^) by Th24
.= (r(#)g)/f by Th47;
end;
theorem
(f/g)(#)g = (f|dom(g^))
proof
A1: dom (g^) c= dom g by Th11;
A2: dom ((f/g)(#)g) = dom (f/g) /\ dom g by SEQ_1:def 5
.= dom f /\ (dom g \ g"{0}) /\ dom g by Def4
.= dom f /\ ((dom g \ g"{0}) /\ dom g) by XBOOLE_1:16
.= dom f /\ (dom (g^) /\ dom g) by Def8
.= dom f /\ dom (g^) by A1,XBOOLE_1:28
.= dom (f|(dom (g^))) by RELAT_1:90;
now let c; assume A3: c in dom ((f/g)(#)g);
then A4: c in dom f /\ dom (g^) by A2,RELAT_1:90;
then A5: c in dom (f(#)(g^)) by SEQ_1:def 5;
A6: c in dom f & c in dom (g^) by A4,XBOOLE_0:def 3;
then A7: g.c <> 0 by Th13;
thus ((f/g)(#)g).c = ((f/g).c) * g.c by A3,SEQ_1:def 5
.= (f(#)(g^)).c * g.c by Th47
.= (f.c) *((g^).c) * g.c by A5,SEQ_1:def 5
.= (f.c)*(g.c)"*g.c by A6,Def8
.= (f.c)*((g.c)" * (g.c)) by XCMPLX_1:4
.= (f.c)*1 by A7,XCMPLX_0:def 7
.= (f|(dom (g^))).c by A2,A3,FUNCT_1:70;
end;
hence thesis by A2,PARTFUN1:34;
end;
theorem Th50:
(f/g)(#)(f1/g1) = (f(#)f1)/(g(#)g1)
proof
A1: dom ((f/g)(#)(f1/g1)) = dom (f/g) /\ dom (f1/g1) by SEQ_1:def 5
.= dom f /\ (dom g \ g"{0}) /\ dom (f1/g1) by Def4
.= dom f /\ (dom g \ g"{0}) /\ (dom f1 /\ (dom g1 \ g1"{0})) by Def4
.= dom f /\ ((dom g \ g"{0}) /\ (dom f1 /\ (dom g1 \ g1"{0}))) by XBOOLE_1:16
.= dom f /\ (dom f1 /\ ((dom g \ g"{0}) /\ (dom g1 \ g1"{0}))) by XBOOLE_1:16
.= dom f /\ dom f1 /\ ((dom g \ g"{0}) /\ (dom g1 \ g1"{0})) by XBOOLE_1:16
.= dom (f(#)f1) /\ ((dom g \ g"{0}) /\ (dom g1 \ g1"{0})) by SEQ_1:def 5
.= dom (f(#)f1) /\ (dom (g(#)g1) \ (g(#)g1)"{0}) by Th12
.= dom ((f(#)f1)/(g(#)g1)) by Def4;
now let c; assume A2: c in dom ((f/g)(#)(f1/g1));
then c in dom (f/g) /\ dom (f1/g1) by SEQ_1:def 5;
then c in dom (f (#)(g^)) /\ dom (f1/g1) by Th47;
then c in dom (f (#)(g^)) /\ dom (f1(#)(g1^)) by Th47;
then A3: c in dom (f (#)(g^)) & c in dom (f1(#)(g1^)) by XBOOLE_0:def 3;
then c in dom f /\ dom(g^) & c in dom f1 /\ dom(g1^) by SEQ_1:def 5;
then c in dom f & c in dom(g^) & c in dom f1 & c in dom(g1^) by XBOOLE_0:def
3
;
then c in dom f /\ dom f1 & c in dom (g^) /\ dom (g1^) by XBOOLE_0:def 3;
then A4: c in dom (f(#)f1) & c in dom((g^)(#)(g1^)) by SEQ_1:def 5;
then c in dom (f(#)f1) & c in dom((g(#)g1)^) by Th43;
then c in dom (f(#)f1) /\ dom((g(#)g1)^) by XBOOLE_0:def 3;
then A5: c in dom ((f(#)f1)(#)((g(#)g1)^)) by SEQ_1:def 5;
thus ((f/g)(#)(f1/g1)).c = ((f/g).c)* (f1/g1).c by A2,SEQ_1:def 5
.= ((f(#)(g^)).c) * (f1/g1).c by Th47
.= ((f(#)(g^)).c) * (f1(#)(g1^)).c by Th47
.= (f.c) * ((g^).c) * (f1(#)(g1^)).c by A3,SEQ_1:def 5
.= (f.c) * ((g^).c) * ((f1.c)* (g1^).c) by A3,SEQ_1:def 5
.= (f.c) * ((g^).c) * (f1.c) * (g1^).c by XCMPLX_1:4
.= (f.c) * ((f1.c) * (g^).c) * (g1^).c by XCMPLX_1:4
.= (f.c) * (((f1.c) * (g^).c) * (g1^).c) by XCMPLX_1:4
.= (f.c) * ((f1.c) * (((g^).c) * (g1^).c)) by XCMPLX_1:4
.= (f.c) * ((f1.c) * ((g^)(#)(g1^)).c) by A4,SEQ_1:def 5
.= (f.c) * (f1.c) * ((g^)(#)(g1^)).c by XCMPLX_1:4
.= (f.c) * (f1.c) * ((g(#)g1)^).c by Th43
.= ((f(#)f1).c) * ((g(#)g1)^).c by A4,SEQ_1:def 5
.= ((f(#)f1)(#)((g(#)g1)^)).c by A5,SEQ_1:def 5
.= ((f(#)f1)/(g(#)g1)).c by Th47;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem Th51:
(f1/f2)^ = (f2|dom(f2^))/f1
proof
thus (f1/f2)^ = (f1(#)(f2^))^ by Th47
.= (f1^)(#)(f2^^) by Th43
.= (f2|dom(f2^))(#)(f1^) by Th42
.= (f2|dom(f2^))/f1 by Th47;
end;
theorem Th52:
g (#) (f1/f2) = (g (#) f1)/f2
proof
thus g (#) (f1/f2) = g (#) (f1 (#) (f2^)) by Th47
.= g (#) f1 (#) (f2^) by Th21
.= (g (#) f1)/f2 by Th47;
end;
theorem
g/(f1/f2) = (g(#)(f2|dom(f2^)))/f1
proof
thus g/(f1/f2) = g (#) ((f1/f2)^) by Th47
.= g (#) ((f2|dom(f2^))/f1) by Th51
.= (g (#) (f2|dom(f2^)))/f1 by Th52;
end;
theorem
-f/g = (-f)/g & f/(-g) = -f/g
proof
thus -f/g = (-1)(#)(f/g) by Th38
.= ((-1) (#) f)/g by Th48
.= (-f)/g by Th38;
thus f/(-g) = f (#) ((-g)^) by Th47
.= f (#) ((-1) (#) (g^)) by Th45
.= (-1) (#) (f (#) (g^)) by Th25
.= -(f (#) (g^)) by Th38
.= -(f/g) by Th47;
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 Th47
.= f1(#)(f^) + f2(#)(f^) by Th47
.= (f1+f2) (#) (f^) by Th22
.= (f1+f2)/f by Th47;
thus f1/f - f2/f = f1(#)(f^) - f2/f by Th47
.= f1(#)(f^) -f2(#)(f^) by Th47
.= (f1-f2)(#)(f^) by Th26
.= (f1-f2)/f by Th47;
end;
theorem Th56:
f1/f + g1/g = (f1(#)g + g1(#)f)/(f(#)g)
proof
A1: dom ((f1/f) + (g1/g)) = dom (f1/f) /\ dom (g1/g) by SEQ_1:def 3
.= dom f1 /\ (dom f \ f"{0}) /\ dom (g1/g) by Def4
.= dom f1 /\ (dom f \ f"{0}) /\ (dom g1 /\ (dom g \ g"{0})) by Def4
.= dom f1 /\ (dom f /\ (dom f \ f"{0})) /\
(dom g1 /\ (dom g \ g"{0})) by Th11
.= dom f /\ (dom f \ f"{0}) /\ dom f1 /\
(dom g /\ (dom g \ g"{0}) /\ dom g1) by Th11
.= dom f /\ (dom f \ f"{0}) /\ (dom f1 /\
(dom g /\ (dom g \ g"{0}) /\ dom g1)) by XBOOLE_1:16
.= dom f /\ (dom f \ f"{0}) /\ (dom f1 /\
(dom g /\ (dom g \ g"{0})) /\ dom g1) by XBOOLE_1:16
.= dom f /\ (dom f \ f"{0}) /\ (dom f1 /\
dom g /\ (dom g \ g"{0}) /\ dom g1) by XBOOLE_1:16
.= dom f /\ (dom f \ f"{0}) /\ (dom (f1(#)g) /\ (dom g \ g"{0}) /\ dom g1)
by SEQ_1:def 5
.= dom f /\ (dom f \ f"{0}) /\ (dom (f1(#)g) /\
(dom g1 /\ (dom g \ g"{0}))) by XBOOLE_1:16
.= dom (f1(#)g) /\ ((dom f \ f"{0}) /\ dom f /\
(dom g1 /\ (dom g \ g"{0}))) by XBOOLE_1:16
.= dom (f1(#)g) /\ ((dom f \ f"{0}) /\ (dom f /\
(dom g1 /\ (dom g \ g"{0})))) by XBOOLE_1:16
.= dom (f1(#)g) /\ ((dom f \ f"{0}) /\ (dom g1 /\
dom f /\ (dom g \ g"{0}))) by XBOOLE_1:16
.= dom (f1(#)g) /\ ((dom f \ f"{0}) /\ (dom (g1(#)f) /\ (dom g \ g"{0})))
by SEQ_1:def 5
.= dom (f1(#)g) /\ (dom (g1(#)f) /\ ((dom f \ f"{0}) /\
(dom g \ g"{0}))) by XBOOLE_1:16
.= dom (f1(#)g) /\ dom (g1(#)
f) /\ ((dom f \ f"{0}) /\ (dom g \ g"{0})) by XBOOLE_1:16
.= dom (f1(#)g + g1(#)f) /\ ((dom f \ f"{0}) /\
(dom g \ g"{0})) by SEQ_1:def 3
.= dom (f1(#)g + g1(#)f) /\ (dom (f(#)g) \ (f(#)g)"{0}) by Th12
.= dom ((f1(#)g + g1(#)f)/(f(#)g)) by Def4;
now let c; assume A2: c in dom ((f1/f) + (g1/g));
then A3: c in dom (f1/f) /\ dom (g1/g) by SEQ_1:def 3;
then A4: c in dom (f1/f) & c in dom (g1/g) by XBOOLE_0:def 3;
c in dom (f1 (#)(f^)) /\ dom (g1/g) by A3,Th47;
then c in dom (f1 (#)(f^)) /\ dom (g1(#)(g^)) by Th47;
then c in dom (f1 (#)(f^)) & c in dom (g1(#)(g^)) by XBOOLE_0:def 3;
then c in dom f1 /\ dom(f^) & c in dom g1 /\ dom(g^) by SEQ_1:def 5;
then A5: c in dom f1 & c in dom(f^) & c in dom g1 & c in dom(g^)
by XBOOLE_0:def 3;
then A6: f.c <> 0 & g.c <> 0 by Th13;
c in dom f1 /\ dom g1 & c in dom (f^) /\ dom (g^) by A5,XBOOLE_0:def 3;
then c in dom f1 /\ dom g1 & c in dom ((f^)(#)(g^)) by SEQ_1:def 5;
then A7: c in dom f1 /\ dom g1 & c in dom ((f(#)g)^) by Th43;
A8: dom (g^) c= dom g & dom (f^) c= dom f by Th11;
then c in dom f /\ dom g by A5,XBOOLE_0:def 3;
then A9:c in dom (f(#)g) by SEQ_1:def 5;
c in dom f1 /\ dom g & c in dom g1 /\ dom f by A5,A8,XBOOLE_0:def 3;
then A10: c in dom (f1(#)g) & c in dom (g1(#)f) by SEQ_1:def 5;
then c in dom (f1(#)g) /\ dom (g1(#)f) by XBOOLE_0:def 3;
then A11: c in dom (f1(#)g + g1(#)f) by SEQ_1:def 3;
then c in dom (f1(#)g + g1(#)f) /\ dom ((f(#)g)^) by A7,XBOOLE_0:def 3;
then c in dom ((f1(#)g + g1(#)f)(#)((f(#)g)^)) by SEQ_1:def 5;
then A12: c in dom ((f1(#)g + g1(#)f)/(f(#)g)) by Th47;
thus (f1/f + g1/g).c = (f1/f).c + (g1/g).c by A2,SEQ_1:def 3
.= (f1.c) * (f.c)" + (g1/g).c by A4,Def4
.= (f1.c) *(1*(f.c)") + (g1.c) * 1 * (g.c)" by A4,Def4
.= (f1.c) *((g.c) *(g.c)"* (f.c)") +
(g1.c) * (1 * (g.c)") by A6,XCMPLX_0:def 7
.= (f1.c) *((g.c) *(g.c)"* (f.c)") +
(g1.c) * ((f.c) *(f.c)" * (g.c)") by A6,XCMPLX_0:def 7
.= (f1.c) *(g.c *((g.c)"* (f.c)")) +
(g1.c) * ((f.c) *(f.c)" * (g.c)") by XCMPLX_1:4
.= (f1.c) *((g.c) *((g.c)"* (f.c)")) +
(g1.c) * ((f.c) *((f.c)" * (g.c)")) by XCMPLX_1:4
.= (f1.c) *((g.c) *((g.c * f.c)")) +
(g1.c) * ((f.c) *((f.c)" * (g.c)")) by XCMPLX_1:205
.= (f1.c) *((g.c) *((f.c* g.c)")) +
(g1.c) * ((f.c) *((f.c * g.c)")) by XCMPLX_1:205
.= (f1.c) *((g.c) * ((f(#)g).c)") + (g1.c) * ((f.c) *((f.c * g.c)"))
by A9,SEQ_1:def 5
.= (f1.c) *((g.c) *((f(#)g).c)") + (g1.c) *((f.c) *((f(#)g).c)")
by A9,SEQ_1:def 5
.= (f1.c) *(g.c) * ((f(#)g).c)" + (g1.c) * ((f.c) * ((f(#)
g).c)") by XCMPLX_1:4
.= (f1.c) *(g.c) * ((f(#)g).c)" + (g1.c) * (f.c) * ((f(#)g).c)" by XCMPLX_1:4
.= (f1(#)g).c * ((f(#)g).c)" + (g1.c) *f.c *((f(#)g).c)" by A10,SEQ_1:def 5
.= (f1(#)g).c * ((f(#)g).c)" + (g1(#)f).c *((f(#)g).c)" by A10,SEQ_1:def 5
.= ((f1(#)g).c + (g1(#)f).c) *((f(#)g).c)" by XCMPLX_1:8
.= (f1(#)g + g1(#)f).c *((f(#)g).c)" by A11,SEQ_1:def 3
.= ((f1(#)g + g1(#)f)/(f(#)g)).c by A12,Def4;
end;
hence f1/f + g1/g = (f1(#)g + g1(#)f)/(f(#)g) by A1,PARTFUN1:34;
end;
theorem
(f/g)/(f1/g1) = (f(#)(g1|dom(g1^)))/(g(#)f1)
proof
thus (f/g)/(f1/g1) = (f/g)(#)((f1/g1)^) by Th47
.= (f/g)(#)(((g1|dom(g1^)))/f1) by Th51
.= (f(#)(g1|dom(g1^)))/(g(#)f1) by Th50;
end;
theorem
f1/f - g1/g = (f1(#)g - g1(#)f)/(f(#)g)
proof
thus f1/f - g1/g = f1/f +- g1/g by Th40
.= f1/f + (-1)(#) (g1/g) by Th38
.= f1/f + ((-1)(#) g1)/g by Th48
.= (f1(#)g + (-1)(#) g1(#)f)/(f(#)g) by Th56
.= (f1(#)g + (-1)(#) (g1(#)f))/(f(#)g) by Th24
.= (f1(#)g + - (g1(#)f))/(f(#)g) by Th38
.= (f1(#)g - (g1(#)f))/(f(#)g) by Th40;
end;
theorem
abs(f1/f2) = abs(f1)/abs(f2)
proof
thus abs(f1/f2) = abs(f1(#)(f2^)) by Th47
.= abs(f1)(#)abs((f2^)) by Th36
.= abs(f1)(#)((abs(f2))^) by Th46
.= abs(f1)/abs(f2) by Th47;
end;
theorem Th60:
(f1+f2)|X = f1|X + f2|X & (f1+f2)|X = f1|X + f2 & (f1+f2)|X = f1 + f2|X
proof
A1: dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:90
.= dom f1 /\ dom f2 /\ (X /\ X) by SEQ_1:def 3
.= 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:90
.= dom f1 /\ X /\ dom (f2|X) by XBOOLE_1:16
.= dom (f1|X) /\ dom (f2|X) by RELAT_1:90
.= dom ((f1|X)+(f2|X)) by SEQ_1:def 3;
now let c; assume A2: c in dom ((f1+f2)|X);
then c in dom (f1+f2) /\ X by RELAT_1:90;
then A3: c in dom (f1+f2) & c in X by XBOOLE_0:def 3;
then c in dom f1 /\ dom f2 by SEQ_1:def 3;
then c in dom f1 & c in dom f2 by XBOOLE_0:def 3;
then c in dom f1 /\ X & c in dom f2 /\ X by A3,XBOOLE_0:def 3;
then A4: c in dom (f1|X) & c in dom (f2|X) by RELAT_1:90;
then c in dom (f1|X) /\ dom (f2|X) by XBOOLE_0:def 3;
then A5: c in dom ((f1|X) + (f2|X)) by SEQ_1:def 3;
thus ((f1+f2)|X).c = (f1+f2).c by A2,FUNCT_1:70
.= (f1.c) + (f2.c) by A3,SEQ_1:def 3
.= ((f1|X).c) + (f2.c) by A4,FUNCT_1:70
.= ((f1|X).c) + ((f2|X).c) by A4,FUNCT_1:70
.= ((f1|X)+(f2|X)).c by A5,SEQ_1:def 3;
end;
hence (f1+f2)|X = f1|X + f2|X by A1,PARTFUN1:34;
A6: dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:90
.= dom f1 /\ dom f2 /\ X by SEQ_1:def 3
.= dom f1 /\ X /\ dom f2 by XBOOLE_1:16
.= dom (f1|X) /\ dom f2 by RELAT_1:90
.= dom ((f1|X)+ f2) by SEQ_1:def 3;
now let c; assume A7: c in dom ((f1+f2)|X);
then c in dom (f1+f2) /\ X by RELAT_1:90;
then A8: c in dom (f1+f2) & c in X by XBOOLE_0:def 3;
then c in dom f1 /\ dom f2 by SEQ_1:def 3;
then c in dom f1 & c in dom f2 by XBOOLE_0:def 3;
then c in dom f1 /\ X & c in dom f2 by A8,XBOOLE_0:def 3;
then A9: c in dom (f1|X) & c in dom f2 by RELAT_1:90;
then c in dom (f1|X) /\ dom f2 by XBOOLE_0:def 3;
then A10: c in dom ((f1|X) + f2) by SEQ_1:def 3;
thus ((f1+f2)|X).c = (f1+f2).c by A7,FUNCT_1:70
.= (f1.c) +(f2.c) by A8,SEQ_1:def 3
.= ((f1|X).c) +(f2.c) by A9,FUNCT_1:70
.= ((f1|X)+f2).c by A10,SEQ_1:def 3;
end;
hence (f1+f2)|X = f1|X + f2 by A6,PARTFUN1:34;
A11: dom ((f1+f2)|X) = dom (f1+f2) /\ X by RELAT_1:90
.= dom f1 /\ dom f2 /\ X by SEQ_1:def 3
.= dom f1 /\ (dom f2 /\ X) by XBOOLE_1:16
.= dom f1 /\ dom (f2|X) by RELAT_1:90
.= dom (f1 + (f2|X)) by SEQ_1:def 3;
now let c; assume A12: c in dom ((f1+f2)|X);
then c in dom (f1+f2) /\ X by RELAT_1:90;
then A13: c in dom (f1+f2) & c in X by XBOOLE_0:def 3;
then c in dom f1 /\ dom f2 by SEQ_1:def 3;
then c in dom f1 & c in dom f2 by XBOOLE_0:def 3;
then c in dom f1 & c in dom f2 /\ X by A13,XBOOLE_0:def 3;
then A14: c in dom f1 & c in dom (f2|X) by RELAT_1:90;
then c in dom f1 /\ dom (f2|X) by XBOOLE_0:def 3;
then A15: c in dom (f1 + (f2|X)) by SEQ_1:def 3;
thus ((f1+f2)|X).c = (f1+f2).c by A12,FUNCT_1:70
.= (f1.c) +(f2.c) by A13,SEQ_1:def 3
.= (f1.c) +((f2|X).c) by A14,FUNCT_1:70
.= (f1+(f2|X)).c by A15,SEQ_1:def 3;
end;
hence thesis by A11,PARTFUN1:34;
end;
theorem Th61:
(f1(#)f2)|X = f1|X (#) f2|X & (f1(#)f2)|X = f1|X (#) f2 & (f1(#)f2)|X = f1 (#)
f2|X
proof
A1: dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:90
.= dom f1 /\ dom f2 /\ (X /\ X) by SEQ_1:def 5
.= 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:90
.= dom f1 /\ X /\ dom (f2|X) by XBOOLE_1:16
.= dom (f1|X) /\ dom (f2|X) by RELAT_1:90
.= dom ((f1|X)(#)(f2|X)) by SEQ_1:def 5;
now let c; assume A2: c in dom ((f1(#)f2)|X);
then c in dom (f1(#)f2) /\ X by RELAT_1:90;
then A3: c in dom (f1(#)f2) & c in X by XBOOLE_0:def 3;
then c in dom f1 /\ dom f2 by SEQ_1:def 5;
then c in dom f1 & c in dom f2 by XBOOLE_0:def 3;
then c in dom f1 /\ X & c in dom f2 /\ X by A3,XBOOLE_0:def 3;
then A4: c in dom (f1|X) & c in dom (f2|X) by RELAT_1:90;
then c in dom (f1|X) /\ dom (f2|X) by XBOOLE_0:def 3;
then A5: c in dom ((f1|X) (#) (f2|X)) by SEQ_1:def 5;
thus ((f1(#)f2)|X).c = (f1(#)f2).c by A2,FUNCT_1:70
.= (f1.c) *(f2.c) by A3,SEQ_1:def 5
.= ((f1|X).c) *(f2.c) by A4,FUNCT_1:70
.= ((f1|X).c) *((f2|X).c) by A4,FUNCT_1:70
.= ((f1|X)(#)(f2|X)).c by A5,SEQ_1:def 5;
end;
hence (f1(#)f2)|X = f1|X (#) f2|X by A1,PARTFUN1:34;
A6: dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:90
.= dom f1 /\ dom f2 /\ X by SEQ_1:def 5
.= dom f1 /\ X /\ dom f2 by XBOOLE_1:16
.= dom (f1|X) /\ dom f2 by RELAT_1:90
.= dom ((f1|X)(#) f2) by SEQ_1:def 5;
now let c; assume A7: c in dom ((f1(#)f2)|X);
then c in dom (f1(#)f2) /\ X by RELAT_1:90;
then A8: c in dom (f1(#)f2) & c in X by XBOOLE_0:def 3;
then c in dom f1 /\ dom f2 by SEQ_1:def 5;
then c in dom f1 & c in dom f2 by XBOOLE_0:def 3;
then c in dom f1 /\ X & c in dom f2 by A8,XBOOLE_0:def 3;
then A9: c in dom (f1|X) & c in dom f2 by RELAT_1:90;
then c in dom (f1|X) /\ dom f2 by XBOOLE_0:def 3;
then A10: c in dom ((f1|X) (#) f2) by SEQ_1:def 5;
thus ((f1(#)f2)|X).c = (f1(#)f2).c by A7,FUNCT_1:70
.= (f1.c) *(f2.c) by A8,SEQ_1:def 5
.= ((f1|X).c) *(f2.c) by A9,FUNCT_1:70
.= ((f1|X)(#)f2).c by A10,SEQ_1:def 5;
end;
hence (f1(#)f2)|X = f1|X (#) f2 by A6,PARTFUN1:34;
A11: dom ((f1(#)f2)|X) = dom (f1(#)f2) /\ X by RELAT_1:90
.= dom f1 /\ dom f2 /\ X by SEQ_1:def 5
.= dom f1 /\ (dom f2 /\ X) by XBOOLE_1:16
.= dom f1 /\ dom (f2|X) by RELAT_1:90
.= dom (f1 (#) (f2|X)) by SEQ_1:def 5;
now let c; assume A12: c in dom ((f1(#)f2)|X);
then c in dom (f1(#)f2) /\ X by RELAT_1:90;
then A13: c in dom (f1(#)f2) & c in X by XBOOLE_0:def 3;
then c in dom f1 /\ dom f2 by SEQ_1:def 5;
then c in dom f1 & c in dom f2 by XBOOLE_0:def 3;
then c in dom f1 & c in dom f2 /\ X by A13,XBOOLE_0:def 3;
then A14: c in dom f1 & c in dom (f2|X) by RELAT_1:90;
then c in dom f1 /\ dom (f2|X) by XBOOLE_0:def 3;
then A15: c in dom (f1 (#) (f2|X)) by SEQ_1:def 5;
thus ((f1(#)f2)|X).c = (f1(#)f2).c by A12,FUNCT_1:70
.= (f1.c) *(f2.c) by A13,SEQ_1:def 5
.= (f1.c) *((f2|X).c) by A14,FUNCT_1:70
.= (f1(#)(f2|X)).c by A15,SEQ_1:def 5;
end;
hence thesis by A11,PARTFUN1:34;
end;
theorem Th62:
(-f)|X = -(f|X) & (f^)|X = (f|X)^ & (abs(f))|X = abs((f|X))
proof
A1: dom ((-f)|X) = dom (-f) /\ X by RELAT_1:90
.= dom f /\ X by SEQ_1:def 7
.= dom (f|X) by RELAT_1:90
.= dom (-(f|X)) by SEQ_1:def 7;
now let c; assume A2: c in dom ((-f)|X);
then c in dom (-f) /\ X by RELAT_1:90;
then A3: c in dom (-f) & c in X by XBOOLE_0:def 3;
then c in dom f by SEQ_1:def 7;
then c in dom f /\ X by A3,XBOOLE_0:def 3;
then A4: c in dom (f|X) by RELAT_1:90;
then A5: c in dom (-(f|X)) by SEQ_1:def 7;
thus ((-f)|X).c = (-f).c by A2,FUNCT_1:70
.= -(f.c) by A3,SEQ_1:def 7
.= -((f|X).c) by A4,FUNCT_1:70
.= (-(f|X)).c by A5,SEQ_1:def 7;
end;
hence (-f)|X = -(f|X) by A1,PARTFUN1:34;
A6: dom ((f|X)^) c= dom (f|X) by Th11;
A7: dom ((f^)|X) = dom (f^) /\ X by RELAT_1:90
.= (dom f \ f"{0}) /\ X by Def8
.= dom f /\ X \ f"{0} /\ X by XBOOLE_1:50
.= dom (f|X) \ X /\ f"{0} by RELAT_1:90
.= dom (f|X) \ (f|X)"{0} by FUNCT_1:139
.= dom ((f|X)^) by Def8;
now let c; assume A8: c in dom ((f^)|X);
then c in dom (f^) /\ X by RELAT_1:90;
then A9: c in dom (f^) & c in X by XBOOLE_0:def 3;
thus ((f^)|X).c = (f^).c by A8,FUNCT_1:70
.= (f.c)" by A9,Def8
.= ((f|X).c)" by A6,A7,A8,FUNCT_1:70
.= ((f|X)^).c by A7,A8,Def8;
end;
hence (f^)|X = (f|X)^ by A7,PARTFUN1:34;
A10: dom ((abs(f))|X) = dom (abs(f)) /\ X by RELAT_1:90
.= dom f /\ X by SEQ_1:def 10
.= dom (f|X) by RELAT_1:90
.= dom (abs((f|X))) by SEQ_1:def 10;
now let c; assume A11: c in dom ((abs(f))|X);
then c in dom (abs(f)) /\ X by RELAT_1:90;
then A12: c in dom (abs(f)) & c in X by XBOOLE_0:def 3;
A13: c in dom (f|X) by A10,A11,SEQ_1:def 10;
thus ((abs(f))|X).c = (abs(f)).c by A11,FUNCT_1:70
.= abs(f.c) by A12,SEQ_1:def 10
.= abs((f|X).c) by A13,FUNCT_1:70
.= (abs((f|X))).c by A10,A11,SEQ_1:def 10;
end;
hence thesis by A10,PARTFUN1:34;
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 Th40
.= (f1|X)+ (-f2)|X by Th60
.= (f1|X)+ -(f2|X) by Th62
.= (f1|X) - (f2|X) by Th40;
thus (f1-f2)|X = (f1+-f2)|X by Th40
.= (f1|X)+ -f2 by Th60
.= (f1|X) - f2 by Th40;
thus (f1-f2)|X = (f1+-f2)|X by Th40
.= f1+ (-f2)|X by Th60
.= f1 +- (f2|X) by Th62
.= f1 - (f2|X) by Th40;
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 Th47
.= (f1|X) (#) (f2^|X) by Th61
.= (f1|X) (#) ((f2|X)^) by Th62
.= (f1|X)/(f2|X) by Th47;
thus (f1/f2)|X = (f1(#)(f2^))|X by Th47
.= (f1|X) (#) (f2^) by Th61
.= (f1|X)/f2 by Th47;
thus (f1/f2)|X = (f1(#)(f2^))|X by Th47
.= f1 (#) (f2^)|X by Th61
.= f1 (#) ((f2|X)^) by Th62
.= f1/(f2|X) by Th47;
end;
theorem
(r(#)f)|X = r(#)(f|X)
proof
A1: dom ((r(#)f)|X) = dom (r(#)f) /\ X by RELAT_1:90
.= dom f /\ X by SEQ_1:def 6
.= dom (f|X) by RELAT_1:90
.= dom (r(#)(f|X)) by SEQ_1:def 6;
now let c; assume A2: c in dom ((r(#)f)|X);
then c in dom (r(#)f) /\ X by RELAT_1:90;
then A3: c in dom (r(#)f) & c in X by XBOOLE_0:def 3;
then c in dom f by SEQ_1:def 6;
then c in dom f /\ X by A3,XBOOLE_0:def 3;
then A4: c in dom (f|X) by RELAT_1:90;
then A5: c in dom (r(#)(f|X)) by SEQ_1:def 6;
thus ((r(#)f)|X).c = (r(#)f).c by A2,FUNCT_1:70
.= r*(f.c) by A3,SEQ_1:def 6
.= r*(f|X).c by A4,FUNCT_1:70
.= (r(#)(f|X)).c by A5,SEQ_1:def 6;
end;
hence thesis by A1,PARTFUN1:34;
end;
::
:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN, TO REAL
::
theorem Th66:
(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 by PARTFUN1:def 4;
hence dom (f1+f2) = C /\ C by SEQ_1:def 3
.= C;
end;
assume f1+f2 is total; then dom (f1+f2) = C by PARTFUN1:def 4;
then dom f1 /\ dom f2 = C by SEQ_1:def 3;
then C c= dom f1 & C c= dom f2 by XBOOLE_1:17;
hence dom f1 = C & dom f2 = C by XBOOLE_0:def 10;
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 by PARTFUN1:def 4;
hence dom (f1-f2) = C /\ C by SEQ_1:def 4
.= C;
end;
assume f1-f2 is total; then dom (f1-f2) = C by PARTFUN1:def 4;
then dom f1 /\ dom f2 = C by SEQ_1:def 4;
then C c= dom f1 & C c= dom f2 by XBOOLE_1:17;
hence dom f1 = C & dom f2 = C by XBOOLE_0:def 10;
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 by PARTFUN1:def 4;
hence dom (f1(#)f2) = C /\ C by SEQ_1:def 5
.= C;
end;
assume f1(#)f2 is total; then dom (f1(#)f2) = C by PARTFUN1:def 4;
then dom f1 /\ dom f2 = C by SEQ_1:def 5;
then C c= dom f1 & C c= dom f2 by XBOOLE_1:17;
hence dom f1 = C & dom f2 = C by XBOOLE_0:def 10;
end;
theorem Th67:
f is total iff r(#)f is total
proof
thus f is total implies r(#)f is total
proof assume f is total; then dom f = C by PARTFUN1:def 4;
hence dom (r(#)f) = C by SEQ_1:def 6;
end;
assume r(#)f is total; then dom (r(#)f) = C by PARTFUN1:def 4;
hence dom f = C by SEQ_1:def 6;
end;
theorem Th68:
f is total iff -f is total
proof
thus f is total implies -f is total
proof assume A1: f is total; -f = (-1)(#)
f by Th38; hence -f is total by A1,Th67
;
end;
assume A2: -f is total; -f = (-1)(#)f by Th38; hence f is total by A2,Th67;
end;
theorem Th69:
f is total iff abs(f) is total
proof
thus f is total implies abs(f) is total
proof assume f is total; then dom f = C by PARTFUN1:def 4;
hence dom (abs(f)) = C by SEQ_1:def 10;
end;
assume abs(f) is total; then dom (abs(f)) = C by PARTFUN1:def 4;
hence dom f = C by SEQ_1:def 10;
end;
theorem Th70:
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 by PARTFUN1:def 4;
f"{0} c= C; then f"{0} c= dom f \ f"{0} by A1,Def8;
hence f"{0} = {} by XBOOLE_1:38; then C = dom f \ {} by A1,Def8;
hence dom f = C;
end;
assume A2: f"{0} = {} & f is total;
thus dom (f^) = dom f \ f"{0} by Def8
.= C by A2,PARTFUN1:def 4;
end;
theorem Th71:
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 A1: f1 is total & f2"{0} = {} & f2 is total;
then f2^ is total by Th70; then f1(#)(f2^) is total by A1,Th66;
hence f1/f2 is total by Th47;
end;
assume f1/f2 is total; then A2: f1(#)(f2^) is total by Th47;
hence f1 is total by Th66; f2^ is total by A2,Th66;
hence thesis by Th70;
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 Th66; then dom (f1+f2) = C by PARTFUN1:def 4;
hence (f1+f2).c = f1.c + f2.c by SEQ_1:def 3;
f1-f2 is total by A1,Th66; then dom (f1-f2) = C by PARTFUN1:def 4;
hence (f1-f2).c = f1.c - f2.c by SEQ_1:def 4;
f1(#)f2 is total by A1,Th66; then dom (f1(#)f2) = C by PARTFUN1:def 4;
hence (f1(#)f2).c = f1.c * f2.c by SEQ_1:def 5;
end;
theorem
f is total implies (r(#)f).c = r * (f.c)
proof assume f is total; then r(#)f is total by Th67;
then dom (r(#)f) = C by PARTFUN1:def 4;
hence (r(#)f).c = r * (f.c) by SEQ_1:def 6;
end;
theorem
f is total implies (-f).c = - f.c & (abs(f)).c = abs( f.c )
proof assume A1: f is total; then -f is total by Th68;
then dom (-f) = C by PARTFUN1:def 4;
hence (-f).c = - f.c by SEQ_1:def 7;
abs(f) is total by A1,Th69; then dom (abs(f)) = C by PARTFUN1:def 4;
hence (abs(f)).c = abs( f.c ) by SEQ_1:def 10;
end;
theorem
f^ is total implies (f^).c = (f.c)"
proof assume f^ is total; then dom (f^) = C by PARTFUN1:def 4;
hence (f^).c = (f.c)" by Def8;
end;
theorem
f1 is total & f2^ is total implies (f1/f2).c = f1.c *(f2.c)"
proof assume f1 is total & f2^ is total;
then f1 is total & f2"{0} = {} & f2 is total by Th70;
then f1/f2 is total by Th71; then dom (f1/f2) = C by PARTFUN1:def 4;
hence thesis by Def4;
end;
::
:: CHARCTERISTIC FUNCTION OF A SUBSET OF A DOMAIN
::
definition let X,C be set;
redefine func chi(X,C) -> PartFunc of C,REAL;
coherence
proof A1: dom chi(X,C) =C by FUNCT_3:def 3;
now let x; assume x in rng chi(X,C);
then x = 0 or x = 1 by TARSKI:def 2;
hence x in REAL;
end;
then rng chi(X,C) c= REAL by TARSKI:def 3;
hence thesis by A1,RELSET_1:11;
end;
end;
theorem Th77:
f= chi(X,C) iff ( dom f = C &
for c holds (c in X implies f.c = 1) & (not c in X implies f.c = 0))
proof
thus f= chi(X,C) implies (dom f = C &
for c holds (c in X implies f.c = 1) & (not c in X implies f.c = 0)) by
FUNCT_3:def 3;
assume A1: dom f = C &
for c holds (c in X implies f.c = 1) & (not c in X implies f.c = 0);
then for x st x in C holds
(x in X implies (f qua Function).x = 1) &
(not x in X implies (f qua Function).x = 0);
hence thesis by A1,FUNCT_3:def 3;
end;
theorem
chi(X,C) is total
proof dom chi(X,C) = C by Th77; hence thesis by PARTFUN1:def 4; end;
theorem
c in X iff chi(X,C).c = 1 by Th77;
theorem
not c in X iff chi(X,C).c = 0 by Th77;
theorem
c in C \ X iff chi(X,C).c = 0
proof
thus c in C \ X implies chi(X,C).c = 0
proof assume c in C \ X;
then not c in X by XBOOLE_0:def 4; hence thesis by Th77;
end;
assume chi(X,C).c = 0;
then not c in X by Th77; hence thesis by XBOOLE_0:def 4;
end;
canceled;
theorem
chi(C,C).c = 1 by Th77;
theorem Th84:
chi(X,C).c <> 1 iff chi(X,C).c = 0
proof
thus chi(X,C).c <> 1 implies chi(X,C).c = 0
proof assume A1: chi(X,C).c <> 1;
c in C; then c in dom chi(X,C) by Th77;
then A2: chi(X,C).c in rng chi(X,C) by FUNCT_1:def 5;
rng chi(X,C) c= {0,1} by FUNCT_3:48; hence thesis by A1,A2,TARSKI:def 2;
end;
assume that A3: chi(X,C).c = 0 and
A4: chi(X,C).c = 1;
thus contradiction by A3,A4;
end;
theorem
X misses Y implies chi(X,C) + chi(Y,C) = chi(X \/ Y,C)
proof assume A1: X /\ Y = {};
A2: dom (chi(X,C) + chi(Y,C)) = dom chi(X,C) /\ dom chi(Y,C) by SEQ_1:def 3
.= C /\ dom chi(Y,C) by Th77
.= C /\ C by Th77
.= dom chi(X \/ Y,C) by Th77;
now let c such that A3: c in dom (chi(X,C) + chi(Y,C));
now per cases;
suppose A4: c in X;
then A5: chi(X,C).c = 1 by Th77;
not c in Y by A1,A4,XBOOLE_0:def 3;
then A6: chi(Y,C).c = 0 by Th77; c in X \/ Y by A4,XBOOLE_0:def 2;
hence chi(X,C).c + chi(Y,C).c = chi(X \/ Y,C).c by A5,A6,Th77;
suppose A7: not c in X;
then A8: chi(X,C).c = 0 by Th77;
now per cases;
suppose A9: c in Y;
then A10: chi(Y,C).c = 1 by Th77;
c in X \/ Y by A9,XBOOLE_0:def 2;
hence chi(X,C).c + chi(Y,C).c = chi(X \/ Y,C).c by A8,A10,Th77;
suppose A11: not c in Y;
then A12: chi(Y,C).c = 0 by Th77;
not c in X \/ Y by A7,A11,XBOOLE_0:def 2;
hence chi(X,C).c + chi(Y,C).c = chi(X \/ Y,C).c by A8,A12,Th77;
end;
hence chi(X,C).c + chi(Y,C).c = chi(X \/ Y,C).c;
end;
hence (chi(X,C) + chi(Y,C)).c = chi(X \/ Y,C).c by A3,SEQ_1:def 3;
end;
hence thesis by A2,PARTFUN1:34;
end;
theorem
chi(X,C) (#) chi(Y,C) = chi(X /\ Y,C)
proof
A1: dom (chi(X,C) (#) chi(Y,C)) = dom chi(X,C) /\ dom chi(Y,C) by SEQ_1:def 5
.= C /\ dom chi(Y,C) by Th77
.= C /\ C by Th77
.= dom chi(X /\ Y,C) by Th77;
now let c such that A2: c in dom (chi(X,C) (#) chi(Y,C));
now per cases;
suppose A3: chi(X,C).c * chi(Y,C).c = 0;
now per cases by A3,XCMPLX_1:6;
suppose chi(X,C).c = 0;
then not c in X by Th77; then not c in X /\ Y by XBOOLE_0:def 3;
hence chi(X,C).c * chi(Y,C).c = chi(X /\ Y,C).c by A3,Th77;
suppose chi(Y,C).c = 0;
then not c in Y by Th77; then not c in X /\ Y by XBOOLE_0:def 3;
hence chi(X,C).c * chi(Y,C).c = chi(X /\ Y,C).c by A3,Th77;
end;
hence chi(X,C).c * chi(Y,C).c = chi(X /\ Y,C).c;
suppose chi(X,C).c * chi(Y,C).c <> 0;
then A4: chi(X,C).c <> 0 & chi(Y,C).c <> 0;
then A5: chi(X,C).c = 1 & chi(Y,C).c = 1 by Th84;
c in X & c in Y by A4,Th77;
then c in X /\ Y by XBOOLE_0:def 3;
hence chi(X,C).c * chi(Y,C).c = chi(X /\ Y,C).c by A5,Th77;
end;
hence (chi(X,C)(#)chi(Y,C)).c = chi(X /\ Y,C).c by A2,SEQ_1:def 5;
end;
hence thesis by A1,PARTFUN1:34;
end;
::
:: BOUNDED AND CONSTANT PARTIAL FUNCTIONS FROM A DOMAIN, TO REAL
::
definition let C; let f,Y;
pred f is_bounded_above_on Y means :Def9:
ex r st for c st c in Y /\ dom f holds f.c <= r;
pred f is_bounded_below_on Y means :Def10:
ex r st for c st c in Y /\ dom f holds r <= f.c;
end;
definition let C; let f,Y;
pred f is_bounded_on Y means :Def11:
f is_bounded_above_on Y & f is_bounded_below_on Y;
end;
canceled 3;
theorem Th90:
f is_bounded_on Y iff ex r st for c st c in Y /\ dom f holds abs(f.c)<=r
proof
thus f is_bounded_on Y implies
ex r st for c st c in Y /\ dom f holds abs(f.c)<=r
proof assume A1: f is_bounded_on Y;
then f is_bounded_above_on Y by Def11;
then consider r1 such that A2: for c st c in Y /\ dom f holds f.c <= r1 by
Def9;
f is_bounded_below_on Y by A1,Def11;
then consider r2 such that A3: for c st c in Y /\ dom f holds r2 <= f.c by
Def10;
take g=abs(r1)+abs(r2);
let c such that A4: c in Y /\ dom f;
A5: 0 <= abs(r1) by ABSVALUE:5;
A6: 0 <= abs(r2) by ABSVALUE:5;
A7: r1 <= abs(r1) by ABSVALUE:11;
f.c <= r1 by A2,A4; then f.c <= abs(r1) by A7,AXIOMS:22;
then A8: f.c + 0 <= abs(r1)+abs(r2) by A6,REAL_1:55;
A9: -abs(r2) <= r2 by ABSVALUE:11;
A10: -abs(r1) <= 0 by A5,REAL_1:26,50;
r2 <= f.c by A3,A4;
then -abs(r2) <= f.c by A9,AXIOMS:22;
then A11: -abs(r1)+-abs(r2) <= 0 + f.c by A10,REAL_1:55;
-abs(r1)+-abs(r2) = -abs(r1)+-(1*abs(r2))
.= -(1*abs(r1)) + (-1)*abs(r2) by XCMPLX_1:175
.= (-1)*abs(r1) + (-1)*abs(r2) by XCMPLX_1:175
.= (-1)*g by XCMPLX_1:8
.= -(1*g) by XCMPLX_1:175
.= -g;
hence abs(f.c) <= g by A8,A11,ABSVALUE:12;
end;
given r such that A12: for c st c in Y /\ dom f holds abs(f.c) <= r;
now let c; assume c in Y /\ dom f;
then A13: abs(f.c) <= r by A12;
f.c <= abs(f.c) by ABSVALUE:11;
hence f.c <= r by A13,AXIOMS:22;
end;
then A14: f is_bounded_above_on Y by Def9;
now let c; assume c in Y /\ dom f;
then abs(f.c) <= r by A12;
then A15: -r <= -abs(f.c) by REAL_1:50;
-abs(f.c) <= f.c by ABSVALUE:11;
hence -r <= f.c by A15,AXIOMS:22;
end;
then f is_bounded_below_on Y by Def10;
hence thesis by A14,Def11;
end;
theorem
(Y c= X & f is_bounded_above_on X implies f is_bounded_above_on Y) &
(Y c= X & f is_bounded_below_on X implies f is_bounded_below_on Y) &
(Y c= X & f is_bounded_on X implies f is_bounded_on Y)
proof
thus A1: (Y c= X & f is_bounded_above_on X implies f is_bounded_above_on Y)
proof assume A2: Y c= X & f is_bounded_above_on X;
then consider r such that
A3: for c st c in X /\ dom f holds f.c <= r by Def9;
take r; let c; assume c in Y /\ dom f;
then c in Y & c in dom f by XBOOLE_0:def 3;
then c in X /\ dom f by A2,XBOOLE_0:def 3; hence thesis by A3;
end;
thus A4: (Y c= X & f is_bounded_below_on X implies f is_bounded_below_on Y)
proof assume A5: Y c= X & f is_bounded_below_on X;
then consider r such that
A6: for c st c in X /\ dom f holds r <= f.c by Def10;
take r; let c; assume c in Y /\ dom f;
then c in Y & c in dom f by XBOOLE_0:def 3;
then c in X /\ dom f by A5,XBOOLE_0:def 3; hence thesis by A6;
end;
assume Y c= X & f is_bounded_on X;
hence thesis by A1,A4,Def11;
end;
theorem
f is_bounded_above_on X & f is_bounded_below_on Y implies f is_bounded_on X
/\
Y
proof assume A1: f is_bounded_above_on X & f is_bounded_below_on Y;
then consider r1 such that
A2: for c st c in X /\ dom f holds f.c <= r1 by Def9;
consider r2 such that
A3: for c st c in Y /\ dom f holds r2 <= f.c by A1,Def10;
now let c; assume c in X /\ Y /\ dom f;
then c in X /\ Y & c in dom f by XBOOLE_0:def 3;
then c in X & c in dom f by XBOOLE_0:def 3;
then c in X /\ dom f by XBOOLE_0:def 3; hence f.c <= r1 by A2;
end;
hence f is_bounded_above_on X /\ Y by Def9;
now let c; assume c in X /\ Y /\ dom f;
then c in X /\ Y & c in dom f by XBOOLE_0:def 3;
then c in Y & c in dom f by XBOOLE_0:def 3;
then c in Y /\ dom f by XBOOLE_0:def 3; hence r2 <= f.c by A3;
end;
hence thesis by Def10;
end;
theorem
X misses dom f implies f is_bounded_on X
proof assume X /\ dom f = {};
then for c holds c in X /\ dom f implies abs(f.c) <= 0;
hence thesis by Th90;
end;
theorem
0 = r implies r(#)f is_bounded_on Y
proof assume A1: 0 = r;
reconsider p1 = 0 as Real;
now take p=p1; let c; assume c in Y /\ dom (r(#)f);
then A2: c in dom (r(#)f) by XBOOLE_0:def 3;
r*f.c <= 0 by A1; hence (r(#)f).c <= p by A2,SEQ_1:def 6;
end;
hence r(#)f is_bounded_above_on Y by Def9;
take p=p1; let c; assume c in Y /\ dom (r(#)f);
then A3: c in dom (r(#)f) by XBOOLE_0:def 3; 0 <= r*f.c by A1;
hence p <= (r(#)f).c by A3,SEQ_1:def 6;
end;
theorem Th95:
(f is_bounded_above_on Y & 0<=r implies r(#)f is_bounded_above_on Y) &
(f is_bounded_above_on Y & r<=0 implies r(#)f is_bounded_below_on Y)
proof
thus f is_bounded_above_on Y & 0<=r implies r(#)f is_bounded_above_on Y
proof assume A1: f is_bounded_above_on Y & 0<=r;
then consider r1 such that
A2: for c st c in Y /\ dom f holds f.c <= r1 by Def9;
take p = r*abs(r1);
let c; assume c in Y /\ dom (r(#)f);
then A3: c in Y & c in dom (r(#)f) by XBOOLE_0:def 3;
then c in Y & c in dom f by SEQ_1:def 6;
then c in Y /\ dom f by XBOOLE_0:def 3;
then A4: f.c <= r1 by A2;
r1 <= abs(r1) by ABSVALUE:11; then f.c <= abs(r1) by A4,AXIOMS:22;
then r * (f.c) <= abs(r1)*r by A1,AXIOMS:25;
hence (r(#)f).c <= p by A3,SEQ_1:def 6;
end;
assume A5: f is_bounded_above_on Y & r<=0;
then consider r1 such that
A6: for c st c in Y /\ dom f holds f.c <= r1 by Def9;
take p=r*abs(r1); let c; assume c in Y /\ dom (r(#)f);
then A7: c in Y & c in dom (r(#)f) by XBOOLE_0:def 3;
then c in Y & c in dom f by SEQ_1:def 6;
then c in Y /\ dom f by XBOOLE_0:def 3;
then A8: f.c <= r1 by A6;
r1<=abs(r1) by ABSVALUE:11;
then f.c <= abs(r1) by A8,AXIOMS:22;
then p <= r * f.c by A5,REAL_1:52;
hence p <= (r(#)f).c by A7,SEQ_1:def 6;
end;
theorem Th96:
(f is_bounded_below_on Y & 0<=r implies r(#)f is_bounded_below_on Y) &
(f is_bounded_below_on Y & r<=0 implies r(#)f is_bounded_above_on Y)
proof
thus f is_bounded_below_on Y & 0<=r implies r(#)f is_bounded_below_on Y
proof assume A1: f is_bounded_below_on Y & 0<=r;
then consider r1 such that
A2: for c st c in Y /\ dom f holds r1 <= f.c by Def10;
take p = r*r1;
let c; assume c in Y /\ dom (r(#)f);
then A3: c in Y & c in dom (r(#)f) by XBOOLE_0:def 3;
then c in Y & c in dom f by SEQ_1:def 6; then c in Y /\ dom f by XBOOLE_0:def
3
;
then r1 <= f.c by A2;
then p <= (f.c)*r by A1,AXIOMS:25;
hence p <= (r(#)f).c by A3,SEQ_1:def 6;
end;
assume A4: f is_bounded_below_on Y & r<=0;
then consider r1 such that
A5: for c st c in Y /\ dom f holds r1 <= f.c by Def10;
take p=r*(-abs(r1));
let c; assume c in Y /\ dom (r(#)f);
then A6: c in Y & c in dom (r(#)f) by XBOOLE_0:def 3;
then c in Y & c in dom f by SEQ_1:def 6; then c in Y /\ dom f by XBOOLE_0:def
3
;
then A7: r1 <= f.c by A5;
-abs(r1) <= r1 by ABSVALUE:11; then -abs(r1) <= f.c by A7,AXIOMS:22;
then r * f.c <= p by A4,REAL_1:52; hence (r(#)f).c <= p by A6,SEQ_1:def 6;
end;
theorem Th97:
f is_bounded_on Y implies r(#)f is_bounded_on Y
proof assume f is_bounded_on Y;
then A1: f is_bounded_above_on Y & f is_bounded_below_on Y by Def11;
now per cases;
suppose A2: 0 <= r;
hence r(#)f is_bounded_above_on Y by A1,Th95;
thus r(#)f is_bounded_below_on Y by A1,A2,Th96;
suppose A3: r <= 0;
hence r(#)f is_bounded_above_on Y by A1,Th96;
thus r(#)f is_bounded_below_on Y by A1,A3,Th95;
end;
hence r(#)f is_bounded_on Y by Def11;
end;
theorem
abs(f) is_bounded_below_on X
proof consider p such that A1: p=0;
take p; let c; assume c in X /\ dom (abs(f));
then A2: c in dom (abs(f)) by XBOOLE_0:def 3; 0 <= abs( f.c ) by ABSVALUE:5;
hence p <= (abs(f)).c by A1,A2,SEQ_1:def 10;
end;
theorem Th99:
f is_bounded_on Y implies abs(f) is_bounded_on Y & -f is_bounded_on Y
proof assume A1: f is_bounded_on Y;
then consider r1 such that
A2: for c st c in Y /\ dom f holds abs(f.c) <= r1 by Th90;
now let c; assume c in Y /\ dom (abs(f));
then A3: c in Y & c in dom (abs(f)) by XBOOLE_0:def 3
; then c in Y & c in dom f by SEQ_1:def 10;
then c in Y /\ dom f by XBOOLE_0:def 3;
then abs(abs(f.c)) <= r1 by A2;
hence abs((abs(f)).c) <= r1 by A3,SEQ_1:def 10;
end;
hence abs(f) is_bounded_on Y by Th90;
(-1)(#)f is_bounded_on Y by A1,Th97; hence thesis by Th38;
end;
theorem Th100:
(f1 is_bounded_above_on X & f2 is_bounded_above_on Y implies
f1+f2 is_bounded_above_on (X /\ Y)) &
(f1 is_bounded_below_on X & f2 is_bounded_below_on Y implies
f1+f2 is_bounded_below_on (X /\ Y)) &
(f1 is_bounded_on X & f2 is_bounded_on Y implies
f1+f2 is_bounded_on (X /\ Y))
proof
thus A1: f1 is_bounded_above_on X & f2 is_bounded_above_on Y implies
f1+f2 is_bounded_above_on (X /\ Y)
proof assume A2: f1 is_bounded_above_on X & f2 is_bounded_above_on Y;
then consider r1 such that
A3: for c st c in X /\ dom f1 holds f1.c <= r1 by Def9;
consider r2 such that
A4: for c st c in Y /\ dom f2 holds f2.c <= r2 by A2,Def9;
take r=r1+r2; let c; assume c in X /\ Y /\ dom (f1+f2);
then A5: c in X /\ Y & c in dom (f1+f2) by XBOOLE_0:def 3;
then c in X & c in Y & c in dom f1 /\ dom f2 by SEQ_1:def 3,XBOOLE_0:def 3;
then c in X & c in Y & c in dom f1 & c in dom f2 by XBOOLE_0:def 3;
then A6: c in X /\ dom f1 & c in Y /\ dom f2 by XBOOLE_0:def 3;
then A7: f1.c <= r1 by A3; f2.c <= r2 by A4,A6; then f1.c + f2.c <=
r by A7,REAL_1:55;
hence (f1+f2).c <= r by A5,SEQ_1:def 3;
end;
thus A8: f1 is_bounded_below_on X & f2 is_bounded_below_on Y implies
f1+f2 is_bounded_below_on (X /\ Y)
proof assume A9: f1 is_bounded_below_on X & f2 is_bounded_below_on Y;
then consider r1 such that
A10: for c st c in X /\ dom f1 holds r1 <= f1.c by Def10;
consider r2 such that
A11: for c st c in Y /\ dom f2 holds r2 <= f2.c by A9,Def10;
take r=r1+r2; let c; assume c in X /\ Y /\ dom (f1+f2);
then A12: c in X /\ Y & c in dom (f1+f2) by XBOOLE_0:def 3;
then c in X & c in Y & c in dom f1 /\ dom f2 by SEQ_1:def 3,XBOOLE_0:def 3;
then c in X & c in Y & c in dom f1 & c in dom f2 by XBOOLE_0:def 3;
then A13: c in X /\ dom f1 & c in Y /\ dom f2 by XBOOLE_0:def 3;
then A14: r1 <= f1.c by A10; r2 <= f2.c by A11,A13; then r <= f1.c + f2.c by
A14,REAL_1:55;
hence r <= (f1+f2).c by A12,SEQ_1:def 3;
end;
assume A15: f1 is_bounded_on X & f2 is_bounded_on Y;
hence f1+f2 is_bounded_above_on (X /\ Y) by A1,Def11;
thus f1+f2 is_bounded_below_on (X /\ Y) by A8,A15,Def11;
end;
theorem Th101:
f1 is_bounded_on X & f2 is_bounded_on Y implies
f1(#)f2 is_bounded_on (X /\ Y) & f1-f2 is_bounded_on X /\ Y
proof assume A1: f1 is_bounded_on X & f2 is_bounded_on Y;
then consider r1 such that
A2: for c st c in X /\ dom f1 holds abs(f1.c) <= r1 by Th90;
consider r2 such that
A3: for c st c in Y /\ dom f2 holds abs(f2.c) <= r2 by A1,Th90;
now take r=r1*r2; let c; assume c in X /\ Y /\ dom (f1(#)f2);
then A4: c in X /\ Y & c in dom (f1(#)f2) by XBOOLE_0:def 3;
then c in X & c in Y & c in dom f1 /\ dom f2 by SEQ_1:def 5,XBOOLE_0:def 3;
then c in X & c in Y & c in dom f1 & c in dom f2 by XBOOLE_0:def 3;
then A5: c in X /\ dom f1 & c in Y /\ dom f2 by XBOOLE_0:def 3;
then A6: abs(f1.c) <= r1 by A2;
A7: abs(f2.c) <= r2 by A3,A5;
A8: 0<=abs(f1.c) by ABSVALUE:5;
0<=abs(f2.c) by ABSVALUE:5;
then abs(f1.c)*abs(f2.c) <= r by A6,A7,A8,Th2;
then abs(f1.c * f2.c) <= r by ABSVALUE:10; hence abs((f1(#)f2).c) <=
r by A4,SEQ_1:def 5;
end;
hence f1(#)f2 is_bounded_on X /\ Y by Th90;
-f2 is_bounded_on Y by A1,Th99; then f1+-f2 is_bounded_on (X /\ Y) by A1,
Th100;
hence thesis by Th40;
end;
theorem Th102:
f is_bounded_above_on X & f is_bounded_above_on Y implies
f is_bounded_above_on X \/ Y
proof assume A1: f is_bounded_above_on X & f is_bounded_above_on Y;
then consider r1 such that
A2: for c st c in X /\ dom f holds f.c <= r1 by Def9;
consider r2 such that
A3: for c st c in Y /\ dom f holds f.c <= r2 by A1,Def9;
take r = abs(r1) + abs(r2); let c; assume c in (X \/ Y) /\ dom f;
then A4: c in X \/ Y & c in dom f by XBOOLE_0:def 3;
now per cases by A4,XBOOLE_0:def 2;
suppose c in X; then c in X /\ dom f by A4,XBOOLE_0:def 3
; then A5: f.c <= r1 by A2;
r1 <= abs(r1) by ABSVALUE:11;
then A6: f.c <= abs(r1) by A5,AXIOMS:22;
0 <= abs(r2) by ABSVALUE:5; then f.c + 0 <= r by A6,REAL_1:55;
hence f.c <= r;
suppose c in Y; then c in Y /\ dom f by A4,XBOOLE_0:def 3
; then A7: f.c <= r2 by A3;
r2 <= abs(r2) by ABSVALUE:11;
then A8: f.c <= abs(r2) by A7,AXIOMS:22;
0 <= abs(r1) by ABSVALUE:5; then 0 + f.c <= r by A8,REAL_1:55;
hence f.c <= r;
end;
hence f.c <= r;
end;
theorem Th103:
f is_bounded_below_on X & f is_bounded_below_on Y implies
f is_bounded_below_on X \/ Y
proof assume A1: f is_bounded_below_on X & f is_bounded_below_on Y;
then consider r1 such that
A2: for c st c in X /\ dom f holds r1 <= f.c by Def10;
consider r2 such that
A3: for c st c in Y /\ dom f holds r2 <= f.c by A1,Def10;
take r = -abs(r1) - abs(r2); let c; assume c in (X \/ Y) /\ dom f;
then A4: c in X \/ Y & c in dom f by XBOOLE_0:def 3;
now per cases by A4,XBOOLE_0:def 2;
suppose c in X; then c in X /\ dom f by A4,XBOOLE_0:def 3
; then A5: r1 <= f.c by A2;
-abs(r1) <= r1 by ABSVALUE:11;
then A6: -abs(r1) <= f.c by A5,AXIOMS:22;
0 <= abs(r2) by ABSVALUE:5; then r <= f.c - 0 by A6,REAL_1:92;
hence r <= f.c;
suppose c in Y; then c in Y /\ dom f by A4,XBOOLE_0:def 3;
then A7: r2 <= f.c by A3;
-abs(r2) <= r2 by ABSVALUE:11;
then A8: -abs(r2) <= f.c by A7,AXIOMS:22;
0 <= abs(r1) by ABSVALUE:5;
then -abs(r2) - abs(r1) <= f.c - 0 by A8,REAL_1:92;
then -abs(r1) +- abs(r2) <= f.c - 0 by XCMPLX_0:def 8;
hence r <= f.c by XCMPLX_0:def 8;
end;
hence r <= f.c;
end;
theorem
f is_bounded_on X & f is_bounded_on Y implies
f is_bounded_on X \/ Y
proof assume A1: f is_bounded_on X & f is_bounded_on Y;
then A2: f is_bounded_above_on X & f is_bounded_below_on X by Def11;
A3: f is_bounded_above_on Y & f is_bounded_below_on Y by A1,Def11;
hence f is_bounded_above_on X \/ Y by A2,Th102;
thus f is_bounded_below_on X \/ Y by A2,A3,Th103;
end;
theorem
f1 is_constant_on X & f2 is_constant_on Y implies
(f1 + f2) is_constant_on (X /\ Y) &
(f1 - f2) is_constant_on (X /\ Y) &
(f1 (#) f2) is_constant_on (X /\ Y)
proof assume A1: f1 is_constant_on X & f2 is_constant_on Y;
then consider r1 be Real such that
A2: for c st c in X /\ dom f1 holds f1.c = r1 by PARTFUN2:76;
consider r2 be Real such that
A3: for c st c in Y /\ dom f2 holds f2.c = r2 by A1,PARTFUN2:76;
now let c; assume c in X /\ Y /\ dom (f1+f2);
then A4: c in X /\ Y & c in dom (f1+f2) by XBOOLE_0:def 3;
then c in X & c in Y & c in (dom f1 /\ dom f2) by SEQ_1:def 3,XBOOLE_0:def 3
;
then c in X & c in Y & c in dom f1 & c in dom f2 by XBOOLE_0:def 3;
then A5: c in X /\ dom f1 & c in Y /\ dom f2 by XBOOLE_0:def 3;
thus (f1+f2).c =f1.c + f2.c by A4,SEQ_1:def 3
.= r1 + f2.c by A2,A5
.= r1 + r2 by A3,A5;
end;
hence (f1 + f2) is_constant_on (X /\ Y) by PARTFUN2:76;
now let c; assume c in X /\ Y /\ dom (f1-f2);
then A6: c in X /\ Y & c in dom (f1-f2) by XBOOLE_0:def 3;
then c in X & c in Y & c in (dom f1 /\ dom f2) by SEQ_1:def 4,XBOOLE_0:def 3
;
then c in X & c in Y & c in dom f1 & c in dom f2 by XBOOLE_0:def 3;
then A7: c in X /\ dom f1 & c in Y /\ dom f2 by XBOOLE_0:def 3;
thus (f1-f2).c = f1.c - f2.c by A6,SEQ_1:def 4
.= r1 - f2.c by A2,A7
.= r1 - r2 by A3,A7;
end;
hence (f1 - f2) is_constant_on (X /\ Y) by PARTFUN2:76;
now let c; assume c in X /\ Y /\ dom (f1(#)f2);
then A8: c in X /\ Y & c in dom (f1(#)f2) by XBOOLE_0:def 3;
then c in X & c in Y & c in (dom f1 /\ dom f2) by SEQ_1:def 5,XBOOLE_0:def 3
;
then c in X & c in Y & c in dom f1 & c in dom f2 by XBOOLE_0:def 3;
then A9: c in X /\ dom f1 & c in Y /\ dom f2 by XBOOLE_0:def 3;
thus (f1(#)f2).c =f1.c * f2.c by A8,SEQ_1:def 5
.= r1 * f2.c by A2,A9
.= r1 * r2 by A3,A9;
end;
hence thesis by PARTFUN2:76;
end;
theorem Th106:
f is_constant_on Y implies p(#)f is_constant_on Y
proof assume f is_constant_on Y;
then consider r be Real such that
A1: for c be Element of C st c in Y /\ dom f holds f.c = r by PARTFUN2:76;
reconsider p as Real by XREAL_0:def 1;
now let c; assume c in Y /\ dom (p(#)f);
then A2: c in dom (p(#)f) & c in Y by XBOOLE_0:def 3;
then c in dom f by SEQ_1:def 6;
then A3: c in Y /\ dom f by A2,XBOOLE_0:def 3;
thus (p(#)f).c = p * f.c by A2,SEQ_1:def 6
.= p*r by A1,A3;
end;
hence thesis by PARTFUN2:76;
end;
theorem Th107:
f is_constant_on Y implies abs(f) is_constant_on Y &
-f is_constant_on Y
proof assume f is_constant_on Y;
then consider r be Real such that A1: for c st c in Y /\ dom f holds f.c = r
by PARTFUN2:76;
now let c; assume c in Y /\ dom (abs(f));
then A2: c in dom (abs(f)) & c in Y by XBOOLE_0:def 3;
then c in dom f by SEQ_1:def 10;
then A3: c in Y /\ dom f by A2,XBOOLE_0:def 3;
thus (abs(f)).c = abs(f.c) by A2,SEQ_1:def 10
.= abs(r) by A1,A3;
end;
hence abs(f) is_constant_on Y by PARTFUN2:76;
now take p=-r; let c; assume A4: c in Y /\ dom (-f);
then c in Y /\ dom f by SEQ_1:def 7;
then A5: -f.c = p by A1; c in dom (-f) by A4,XBOOLE_0:def 3;
hence (-f).c = p by A5,SEQ_1:def 7;
end;
hence thesis by PARTFUN2:76;
end;
theorem Th108:
f is_constant_on Y implies f is_bounded_on Y
proof assume f is_constant_on Y;
then consider r be Real such that
A1: for c st c in Y /\ dom f holds f.c = r by PARTFUN2:76;
now take p=abs(r); let c; assume c in Y /\ dom f;
hence abs(f.c) <= p by A1;
end;
hence thesis by Th90;
end;
theorem
f is_constant_on Y implies (for r holds r(#)f is_bounded_on Y) &
(-f is_bounded_on Y) &
abs(f) is_bounded_on Y
proof assume A1: f is_constant_on Y;
now let r; r(#)f is_constant_on Y by A1,Th106;
hence r(#)f is_bounded_on Y by Th108;
end;
hence for r holds r(#)f is_bounded_on Y;
-f is_constant_on Y by A1,Th107; hence -f is_bounded_on Y by Th108;
abs(f) is_constant_on Y by A1,Th107; hence thesis by Th108;
end;
theorem Th110:
(f1 is_bounded_above_on X & f2 is_constant_on Y implies
f1+f2 is_bounded_above_on (X /\ Y)) &
(f1 is_bounded_below_on X & f2 is_constant_on Y implies
f1+f2 is_bounded_below_on (X /\ Y)) &
(f1 is_bounded_on X & f2 is_constant_on Y implies
f1+f2 is_bounded_on (X /\ Y))
proof
thus f1 is_bounded_above_on X & f2 is_constant_on Y implies
f1+f2 is_bounded_above_on (X /\ Y)
proof assume A1: f1 is_bounded_above_on X & f2 is_constant_on Y;
then f2 is_bounded_on Y by Th108;
then f2 is_bounded_above_on Y by Def11;
hence thesis by A1,Th100;
end;
thus f1 is_bounded_below_on X & f2 is_constant_on Y implies
f1+f2 is_bounded_below_on (X /\ Y)
proof assume A2: f1 is_bounded_below_on X & f2 is_constant_on Y;
then f2 is_bounded_on Y by Th108; then f2 is_bounded_below_on Y by Def11;
hence thesis by A2,Th100;
end;
assume A3: f1 is_bounded_on X & f2 is_constant_on Y;
then f2 is_bounded_on Y by Th108; hence thesis by A3,Th100;
end;
theorem
(f1 is_bounded_above_on X & f2 is_constant_on Y implies
f1-f2 is_bounded_above_on (X /\ Y)) &
(f1 is_bounded_below_on X & f2 is_constant_on Y implies
f1-f2 is_bounded_below_on X /\ Y) &
(f1 is_bounded_on X & f2 is_constant_on Y implies
f1-f2 is_bounded_on X /\ Y &
f2-f1 is_bounded_on X /\ Y & f1(#)f2 is_bounded_on X /\ Y)
proof
thus f1 is_bounded_above_on X & f2 is_constant_on Y implies
f1-f2 is_bounded_above_on X /\ Y
proof assume A1: f1 is_bounded_above_on X & f2 is_constant_on Y;
then -f2 is_constant_on Y by Th107;
then f1+-f2 is_bounded_above_on X /\ Y by A1,Th110; hence thesis by Th40;
end;
thus f1 is_bounded_below_on X & f2 is_constant_on Y implies
f1-f2 is_bounded_below_on X /\ Y
proof assume A2: f1 is_bounded_below_on X & f2 is_constant_on Y;
then -f2 is_constant_on Y by Th107;
then f1+-f2 is_bounded_below_on X /\ Y by A2,Th110; hence thesis by Th40;
end;
assume A3: f1 is_bounded_on X & f2 is_constant_on Y;
then -f2 is_constant_on Y by Th107;
then f1+-f2 is_bounded_on X /\ Y by A3,Th110;
hence f1-f2 is_bounded_on X /\ Y by Th40;
A4: f2 is_bounded_on Y by A3,Th108;
hence f2-f1 is_bounded_on X /\ Y by A3,Th101; thus thesis by A3,A4,Th101;
end;