:: Differentiation in Normed Spaces
:: by Noboru Endou and Yasunari Shidama
::
:: Received May 19, 2013
:: Copyright (c) 2013 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 NUMBERS, REAL_1, ZFMISC_1, NORMSP_1, PRE_TOPC, PARTFUN1, FUNCT_1,
NAT_1, FDIFF_1, SUBSET_1, RELAT_1, LOPBAN_1, ORDINAL4, RCOMP_1, TARSKI,
ARYTM_3, VALUED_1, FUNCT_2, ARYTM_1, CARD_1, XXREAL_0, XBOOLE_0, CARD_3,
FINSEQ_1, NDIFF_6;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, CARD_3, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, FINSEQ_1, STRUCT_0, PRE_TOPC, RLVECT_1, NORMSP_1,
VFUNCT_1, LOPBAN_1, NFCONT_1, NDIFF_1;
constructors NFCONT_1, VFUNCT_1, NDIFF_1, RELSET_1, PRVECT_2;
registrations RELSET_1, STRUCT_0, ORDINAL1, XREAL_0, FUNCT_1, INT_1, FUNCT_2,
XBOOLE_0, SUBSET_1, FINSEQ_1, CARD_3, LOPBAN_1, PRVECT_3, NAT_1,
AOFA_A00;
requirements SUBSET, REAL, NUMERALS, ARITHM;
equalities XCMPLX_0, BINOP_1;
theorems TARSKI, ZFMISC_1, XBOOLE_0, XBOOLE_1, BINOP_1, NAT_1, RELAT_1,
FUNCT_1, VFUNCT_1, INT_1, FUNCT_2, FINSEQ_1, NDIFF_1, XREAL_1, XXREAL_0,
RELSET_1, PRVECT_3, XTUPLE_0, PARTFUN1;
schemes FUNCT_2, NAT_1, BINOP_1, RECDEF_1;
begin :: Preliminaries
theorem
for D,E,F be non empty set holds
ex I be Function of Funcs(D,Funcs(E,F)), Funcs([:D,E:],F)
st I is bijective
& for f be Function of D,Funcs(E,F), d,e be element st d in D & e in E
holds (I.f).(d,e) = (f.d).e
proof
let D,E,F be non empty set;
defpred P[element,element] means
ex f be Function of D,Funcs(E,F), g be Function of [:D,E:],F
st $1=f & $2=g &
for d,e be element st d in D & e in E holds g.(d,e) = (f.d).e;
P1:for x be element st x in Funcs(D,Funcs(E,F))
ex y be element st y in Funcs([:D,E:],F) & P[x,y]
proof
let x be element;
assume x in Funcs(D,Funcs(E,F)); then
consider f being Function such that
P12: x = f & dom f = D & rng f c= Funcs(E,F) by FUNCT_2:def 2;
reconsider f as Function of D,Funcs(E,F) by FUNCT_2:2,P12;
deffunc F0(element, element) = (f.$1).$2;
P13:for x,y be element st x in D & y in E holds F0(x,y) in F
proof
let d,e be element;
assume P131: d in D & e in E; then
f.d is Function of E,F by FUNCT_2:5,66;
hence thesis by P131,FUNCT_2:5;
end;
consider g being Function of [:D,E:],F such that
P14: for x,y be element st
x in D & y in E holds g.(x,y) = F0(x,y) from BINOP_1:sch 2(P13);
g in Funcs([:D,E:],F) by FUNCT_2:8;
hence thesis by P12,P14;
end;
consider I be Function of Funcs(D,Funcs(E,F)), Funcs([:D,E:],F) such that
P2: for x be element st x in Funcs(D,Funcs(E,F)) holds P[x,I.x]
from FUNCT_2:sch 1(P1);
P3:for f be Function of D,Funcs(E,F), d,e be element st d in D & e in E holds
(I.f).(d,e) = (f.d).e
proof
let f be Function of D,Funcs(E,F), d,e be element;
assume P31: d in D & e in E;
f in Funcs(D,Funcs(E,F)) by FUNCT_2:8; then
ex f0 be Function of D,Funcs(E,F), g0 be Function of [:D,E:],F
st f=f0 & I.f=g0 &
for d,e be element st d in D & e in E holds g0.(d,e) = (f0.d).e by P2;
hence (I.f).(d,e) = (f.d).e by P31;
end;
now let z1,z2 be element;
assume P41: z1 in Funcs(D,Funcs(E,F))
& z2 in Funcs(D,Funcs(E,F)) & I.z1=I.z2; then
reconsider z1f = z1, z2f = z2 as Function of D,Funcs(E,F) by FUNCT_2:66;
now let d be element;
assume P42: d in D; then
P44: z1f.d is Function of E,F & z2f.d is Function of E,F by FUNCT_2:5,66;
now let e be element;
assume P43: e in E; then
(z1f.d).e = (I.z2f).(d,e) by P3,P42,P41;
hence (z1f.d).e = (z2f.d).e by P3,P42,P43;
end;
hence z1f.d = z2f.d by P44,FUNCT_2:12;
end;
hence z1=z2 by FUNCT_2:12;
end; then
P4:I is one-to-one by FUNCT_2:19;
now let w be element;
assume w in Funcs([:D,E:],F); then
reconsider wf = w as Function of [:D,E:],F by FUNCT_2:66;
defpred P[element,element] means
ex f be Function of E,F st
$2=f &
for e be element st e in E holds f.e = wf.($1,e);
P6: for d be element st d in D ex y be element st y in Funcs(E,F) & P[d,y]
proof
let d be element;
assume P61: d in D;
deffunc F0(element) = wf.(d,$1);
P62: for e be element st e in E holds F0(e) in F
proof
let e be element;
assume e in E; then
[d,e] in [:D,E:] by P61,ZFMISC_1:def 2;
hence thesis by FUNCT_2:5;
end;
consider f being Function of E,F such that
P63: for e be element st e in E holds f.e = F0(e) from FUNCT_2:sch 2(P62);
f in Funcs(E,F) by FUNCT_2:8;
hence thesis by P63;
end;
consider zf be Function of D,Funcs(E,F) such that
P7: for d be element st d in D holds P[d,zf.d] from FUNCT_2:sch 1(P6);
P8: zf in Funcs(D,Funcs(E,F)) by FUNCT_2:8;
P9: now let d,e be set;
assume P8: d in D & e in E; then
P10: (I.zf).(d,e) = (zf.d).e by P3;
ex L be Function of E,F st
zf.d = L
& for e be element st e in E holds L.e = wf.(d,e) by P7,P8;
hence (I.zf).(d,e) = wf.(d,e) by P10,P8;
end;
I.zf is Function of [:D,E:],F by P8,FUNCT_2:5,66; then
I.zf = w by BINOP_1:1,P9;
hence w in rng I by P8,FUNCT_2:112;
end; then
Funcs([:D,E:],F) c= rng I by TARSKI:def 3; then
I is onto by FUNCT_2:def 3,XBOOLE_0:def 10;
hence thesis by P3,P4;
end;
theorem Th02:
for D,E,F be non empty set holds
ex I be Function of Funcs(D,Funcs(E,F)), Funcs([:E,D:],F)
st I is bijective
& for f be Function of D,Funcs(E,F), e,d be element
st e in E & d in D holds (I.f).(e,d) = (f.d).e
proof
let D,E,F be non empty set;
defpred P[element,element] means
ex f be Function of D,Funcs(E,F), g be Function of [:E,D:],F
st $1=f & $2=g
& for e,d be element st e in E & d in D holds g.(e,d) = (f.d).e;
P1:for x be element st x in Funcs(D,Funcs(E,F))
ex y be element st y in Funcs([:E,D:],F) & P[x,y]
proof
let x be element;
assume x in Funcs(D,Funcs(E,F)); then
consider f being Function such that
P12: x = f & dom f = D & rng f c= Funcs(E,F) by FUNCT_2:def 2;
reconsider f as Function of D,Funcs(E,F) by FUNCT_2:2,P12;
deffunc F0(element,element) = (f.$2).$1;
P13:for y,x be element st y in E & x in D holds F0(y,x) in F
proof
let e,d be element;
assume P131: e in E & d in D; then
f.d is Function of E,F by FUNCT_2:5,66;
hence F0(e,d) in F by P131,FUNCT_2:5;
end;
consider g being Function of [:E,D:],F such that
P14: for y,x be element st
y in E & x in D holds g.(y,x) = F0(y,x) from BINOP_1:sch 2(P13);
g in Funcs([:E,D:],F) by FUNCT_2:8;
hence thesis by P12,P14;
end;
consider I be Function of Funcs(D,Funcs(E,F)), Funcs([:E,D:],F)
such that
P2: for x be element st x in Funcs(D,Funcs(E,F)) holds P[x,I.x]
from FUNCT_2:sch 1(P1);
P3:for f be Function of D,Funcs(E,F), e,d be element st
e in E & d in D holds (I.f).(e,d) = (f.d).e
proof
let f be Function of D,Funcs(E,F), e,d be element;
assume P31: e in E & d in D;
f in Funcs(D,Funcs(E,F)) by FUNCT_2:8; then
ex f0 be Function of D,Funcs(E,F), g0 be Function of [:E,D:],F
st f=f0 & I.f=g0
& for e,d be element st e in E & d in D holds
g0.(e,d) = (f0.d).e by P2;
hence (I.f).(e,d) = (f.d).e by P31;
end;
now let z1,z2 be element;
assume P41: z1 in Funcs(D,Funcs(E,F))
& z2 in Funcs(D,Funcs(E,F))
& I.z1=I.z2; then
reconsider z1f = z1, z2f = z2 as Function of D,Funcs(E,F) by FUNCT_2:66;
now let d be element;
assume P42: d in D; then
P44: z1f.d is Function of E,F & z2f.d is Function of E,F by FUNCT_2:5,66;
now let e be element;
assume P43: e in E; then
(z1f.d).e = (I.z2f).(e,d) by P3,P42,P41;
hence (z1f.d).e = (z2f.d).e by P3,P42,P43;
end;
hence z1f.d = z2f.d by P44,FUNCT_2:12;
end;
hence z1=z2 by FUNCT_2:12;
end; then
P4:I is one-to-one by FUNCT_2:19;
now let w be element;
assume w in Funcs([:E,D:],F); then
reconsider wf = w as Function of [:E,D:],F by FUNCT_2:66;
defpred P[element,element] means
ex f be Function of E,F
st $2=f & for e be element st e in E holds f.e = wf.(e,$1);
P6: for d be element st d in D
ex y be element st y in Funcs(E,F) & P[d,y]
proof
let d be element;
assume P61: d in D;
deffunc F0(element) = wf.($1,d);
P62: for e be element st e in E holds F0(e) in F
proof
let e be element;
assume e in E; then
[e,d] in [:E,D:] by P61,ZFMISC_1:def 2;
hence thesis by FUNCT_2:5;
end;
consider f being Function of E,F such that
P63: for e be element st e in E holds f.e = F0(e) from FUNCT_2:sch 2(P62);
f in Funcs(E,F) by FUNCT_2:8;
hence thesis by P63;
end;
consider zf be Function of D,Funcs(E,F) such that
P7: for d be element st d in D holds P[d,zf.d] from FUNCT_2:sch 1(P6);
P8: zf in Funcs(D,Funcs(E,F)) by FUNCT_2:8;
P9: now let e,d be set;
assume P10: e in E & d in D; then
P11: (I.zf).(e,d) = (zf.d).e by P3;
ex L be Function of E,F st
zf.d = L &
for e be element st e in E holds L.e = wf.(e,d) by P7,P10;
hence (I.zf).(e,d) = wf.(e,d) by P11,P10;
end;
I.zf is Function of [:E,D:],F by P8,FUNCT_2:5,66; then
I.zf = w by BINOP_1:1,P9;
hence w in rng I by P8,FUNCT_2:112;
end; then
Funcs([:E,D:],F) c= rng I by TARSKI:def 3; then
I is onto by FUNCT_2:def 3,XBOOLE_0:def 10;
hence thesis by P3,P4;
end;
theorem
for D,E be non-empty non empty FinSequence, F be non empty set holds
ex L being Function of Funcs(product D,Funcs(product E,F)),
Funcs(product(E^D),F)
st L is bijective
& for f be Function of product D,Funcs(product E,F),
e,d be FinSequence
st e in product E & d in product D holds (L.f).(e^d) = (f.d).e
proof
let D,E be non-empty non empty FinSequence, F be non empty set;
consider I be Function of Funcs(product D,Funcs(product E,F)),
Funcs([:product E,product D:],F) such that
P1: I is bijective
& for f be Function of product D,Funcs(product E,F), e,d be element
st e in product E & d in product D
holds (I.f).(e,d) = (f.d).e by Th02;
consider J be Function of [: product E,product D :],product(E^D)
such that
P2: J is one-to-one onto
& for x,y be FinSequence st x in product E & y in product D
holds J.(x,y) = x^y by PRVECT_3:6;
P21:
rng J = product(E^D) by P2,FUNCT_2:def 3; then
reconsider K = J" as Function of product(E^D),[: product E,product D :]
by FUNCT_2:25,P2;
deffunc F0(element)=(I.$1) * K;
P3:for x be element st x in Funcs(product D,Funcs(product E,F))
holds F0(x) in Funcs(product(E^D),F)
proof
let x be element;
assume x in Funcs(product D,Funcs(product E,F)); then
P31:I.x in Funcs([:product E,product D:],F) by FUNCT_2:5;
K in Funcs(product(E^D),[:product E,product D:]) by FUNCT_2:8;
hence thesis by P31,FUNCT_2:128;
end;
consider L being Function of Funcs(product D,Funcs(product E,F)),
Funcs(product(E^D),F) such that
P4: for e be element st e in Funcs(product D,Funcs(product E,F))
holds L.e = F0(e) from FUNCT_2:sch 2(P3);
P54:
K*J = id [:product E,product D:] by P2,P21,FUNCT_2:29;
P54A:
J*K = id product(E^D) by P2,P21,FUNCT_2:29;
now let z1,z2 be element;
assume P51: z1 in Funcs(product D,Funcs(product E,F))
& z2 in Funcs(product D,Funcs(product E,F)) & L.z1=L.z2;
(I.z1) * K = L.z2 by P4,P51; then
P52:((I.z1) * K)*J =((I.z2) * K)*J by P4,P51;
(I.z1)*(K*J) =((I.z1) * K)*J by RELAT_1:36; then
P53:(I.z1)*(K*J) = (I.z2)*(K*J) by P52,RELAT_1:36;
I.z1 is Function of [:product E,product D:],F &
I.z2 is Function of [:product E,product D:],F by P51,FUNCT_2:5,66; then
(I.z1)*(K*J) = I.z1 & (I.z2)*(K*J) = I.z2 by P54,FUNCT_2:17;
hence z1=z2 by P1,FUNCT_2:19,P51,P53;
end; then
P5:L is one-to-one by FUNCT_2:19;
now let w be element;
assume w in Funcs(product(E^D),F); then
reconsider wf = w as Function of product(E^D),F by FUNCT_2:66;
wf*J in Funcs([: product E,product D :],F ) by FUNCT_2:8; then
wf*J in rng I by P1,FUNCT_2:def 3; then
consider zf be element such that
P62: zf in Funcs(product D,Funcs(product E,F)) & I.zf = wf*J by FUNCT_2:11;
L.zf = wf*J*K by P4,P62; then
L.zf = wf* id (product(E^D)) by P54A,RELAT_1:36; then
L.zf =w by FUNCT_2:17;
hence w in rng L by P62,FUNCT_2:112;
end;
then Funcs(product(E^D),F) c= rng L by TARSKI:def 3; then
P6:L is onto by FUNCT_2:def 3,XBOOLE_0:def 10;
for f be Function of product D,Funcs(product E,F), e,d be FinSequence
st e in product E & d in product D
holds (L.f).(e^d) = (f.d).e
proof
let f be Function of product D,Funcs(product E,F), e,d be FinSequence;
assume A1: e in product E & d in product D; then
A2: (I.f).(e,d) = (f.d).e by P1;
A3: J.(e,d) = e^d by P2,A1;
A7: [e,d] in [: product E,product D :] by A1,ZFMISC_1:87;
A6: K.(J.(e,d)) = [e,d] by FUNCT_2:26,P2,A1,ZFMISC_1:87;
f in Funcs(product D,Funcs(product E,F)) by FUNCT_2:8; then
(L.f).(e^d) = ((I.f)*K).(J.(e,d)) by A3,P4;
hence (L.f).(e^d) = (f.d).e by A2,A6,A7,FUNCT_2:5,15;
end;
hence thesis by P5,P6;
end;
theorem Th21:
for X,Y be non empty set holds
ex I be Function of [:X,Y:],[:X,product <*Y*>:]
st I is bijective
& for x,y be element st x in X & y in Y holds I.(x,y) = [x,<*y*>]
proof
let X,Y be non empty set;
consider J be Function of Y,product <*Y*> such that
A1: J is one-to-one onto
& for y be element st y in Y holds J.y = <*y*> by PRVECT_3:4;
defpred P[element,element,element] means $3 = [ $1,<* $2 *> ];
A2:for x,y be element st x in X & y in Y
ex z be element st z in [:X,product <*Y*>:] & P[x,y,z]
proof
let x,y be element;
assume A3: x in X & y in Y; then
J.y = <*y*> by A1; then
<*y*> in product <*Y*> by A3,FUNCT_2:5;
hence thesis by A3,ZFMISC_1:87;
end;
consider I be Function of [: X, Y:],[:X,product <*Y*>:] such that
A4: for x,y be element st x in X & y in Y holds P[x,y,I.(x,y)]
from BINOP_1:sch 1(A2);
reconsider I as Function of [:X,Y:],[:X, product <*Y*>:];
take I;
now let z1,z2 be element;
assume A5: z1 in [:X,Y:] & z2 in [:X,Y:] & I.z1=I.z2; then
consider x1,y1 be element such that
A6: x1 in X & y1 in Y & z1=[x1,y1] by ZFMISC_1:def 2;
consider x2,y2 be element such that
A7: x2 in X & y2 in Y & z2=[x2,y2] by A5,ZFMISC_1:def 2;
[x1,<*y1*>] = I.(x1,y1) by A4,A6
.= I.(x2,y2) by A5,A6,A7
.= [x2,<*y2*>] by A4,A7; then
x1=x2 & <*y1*>=<*y2*> by XTUPLE_0:1;
hence z1=z2 by A6,A7,FINSEQ_1:76;
end;
then T1: I is one-to-one by FUNCT_2:19;
now let w be element;
assume w in [:X, product <*Y*>:]; then
consider x,y1 be element such that
A8: x in X & y1 in product <*Y*> & w=[x,y1] by ZFMISC_1:def 2;
y1 in rng J by A1,A8,FUNCT_2:def 3; then
consider y be element such that
A9: y in Y & y1=J.y by FUNCT_2:11;
J.y = <*y*> by A9,A1; then
A10:w = I.(x,y) by A4,A8,A9;
[x,y] in [:X,Y:] by A8,A9,ZFMISC_1:87;
hence w in rng I by A10,FUNCT_2:4;
end; then
[:X, product <*Y*>:] c= rng I by TARSKI:def 3;
then I is onto by FUNCT_2:def 3,XBOOLE_0:def 10;
hence thesis by A4,T1;
end;
theorem Th22:
for X be non-empty non empty FinSequence, Y be non empty set holds
ex K be Function of [:product X,Y:],product(X^<*Y*>)
st K is bijective
& for x be FinSequence, y be element
st x in product X & y in Y holds K.(x,y) = x^<*y*>
proof
let X be non-empty non empty FinSequence;
let Y be non empty set;
consider I be Function of [:product X,Y:],[: product X, product <*Y*>:]
such that
A1: I is bijective
& for x be element, y be element
st x in product X & y in Y holds I.(x,y) = [x,<*y*>] by Th21;
consider J be Function of [:product X,product <*Y*>:],product (X^<*Y*>)
such that
A2: J is one-to-one onto
& for x,y be FinSequence
st x in product X & y in product <*Y*> holds J.(x,y) = x^y by PRVECT_3:6;
J is bijective by A2;
set K=J*I;
reconsider K as Function of [:product X,Y:],product (X^<*Y*>);
take K;
A3:rng J = product (X^<*Y*>) by A2,FUNCT_2:def 3;
rng I = [:product X,product <*Y*>:] by A1,FUNCT_2:def 3; then
rng(J*I) = J.:([:product X,product <*Y*>:]) by RELAT_1:127
.= product (X^<*Y*>) by A3,RELSET_1:22;
then K is onto by FUNCT_2:def 3;
hence K is bijective by A1,A2;
thus for x be FinSequence, y be element st
x in product X & y in Y holds K.(x,y) = x^<*y*>
proof
let x be FinSequence, y be element;
assume AS0:x in product X & y in Y; then
A4: I.(x,y) = [x,<*y*>] by A1;
[x,y] in [:product X,Y:] by AS0,ZFMISC_1:87; then
I.([x,y]) in [:product X,product <*Y*>:] by FUNCT_2:5; then
<*y*> in product <*Y*> by A4,ZFMISC_1:87; then
J.(x,<*y*>) = x^<*y*> by AS0,A2;
hence thesis by A4,AS0,ZFMISC_1:87,FUNCT_2:15;
end;
end;
theorem
for D be non empty set,
E be non-empty non empty FinSequence,
F be non empty set holds
ex L being Function of Funcs(D,Funcs(product E,F)),
Funcs(product(E^<*D*>),F)
st L is bijective
& for f be Function of D,Funcs(product E,F),
e be FinSequence, d be element
st e in product E & d in D holds (L.f).(e^<*d*>) = (f.d).e
proof
let D be non empty set,
E be non-empty non empty FinSequence,
F be non empty set;
consider I be Function of Funcs(D,Funcs(product E,F)),
Funcs([:product E, D:],F) such that
P1: I is bijective
& for f be Function of D,Funcs(product E,F), e,d be element
st e in product E & d in D holds (I.f).(e,d) = (f.d).e by Th02;
consider J be Function of [: product E,D :],product(E^<*D*>) such that
P2: J is bijective
& for x be FinSequence, y be element st x in product E & y in D
holds J.(x,y) = x^<*y*> by Th22;
P21:rng J = product(E^<*D*>) by P2,FUNCT_2:def 3; then
reconsider K = J" as Function of product(E^<*D*>),[:product E,D:]
by FUNCT_2:25,P2;
deffunc F0(element)=(I.$1) * K;
P3:for x be element st x in Funcs(D,Funcs(product E,F))
holds F0(x) in Funcs(product(E^<*D*>),F)
proof
let x be element;
assume x in Funcs(D,Funcs(product E,F)); then
I.x in Funcs([:product E,D:],F) &
K in Funcs(product(E^<*D*>),[:product E,D:]) by FUNCT_2:5,8;
hence thesis by FUNCT_2:128;
end;
consider L being Function of Funcs(D,Funcs(product E,F)),
Funcs(product(E^<*D*>),F) such that
P4: for e be element st
e in Funcs(D,Funcs(product E,F)) holds L.e = F0(e) from FUNCT_2:sch 2(P3);
take L;
P54:
(K*J) = id [: product E,D :] by P2,P21,FUNCT_2:29;
P54A:
(J*K) = id product(E^<*D*>) by P2,P21,FUNCT_2:29;
now let z1,z2 be element;
assume P51: z1 in Funcs(D,Funcs(product E,F))
& z2 in Funcs(D,Funcs(product E,F)) & L.z1=L.z2;
(I.z1) * K = L.z2 by P4,P51; then
P52:((I.z1) * K)*J =((I.z2) * K)*J by P4,P51;
(I.z1)*(K*J) = ((I.z1)* K)*J by RELAT_1:36; then
P53:(I.z1)*(K*J) = (I.z2)*(K*J) by P52,RELAT_1:36;
I.z1 is Function of [:product E,D:],F &
I.z2 is Function of [:product E,D:],F by P51,FUNCT_2:5,66; then
(I.z1)*(K*J) = I.z1 & (I.z2)*(K*J) = I.z2 by P54,FUNCT_2:17;
hence z1=z2 by P1,FUNCT_2:19,P51,P53;
end;
then T1: L is one-to-one by FUNCT_2:19;
now let w be element;
assume w in Funcs(product(E^<*D*>),F); then
reconsider wf = w as Function of product(E^<*D*>),F by FUNCT_2:66;
wf*J in Funcs([: product E, D :],F ) by FUNCT_2:8; then
wf*J in rng I by P1,FUNCT_2:def 3; then
consider zf be element such that
P62: zf in Funcs(D,Funcs(product E,F)) & I.zf = wf*J by FUNCT_2:11;
L.zf = wf*J*K by P4,P62; then
L.zf = wf* id (product(E^<*D*>)) by P54A,RELAT_1:36; then
L.zf = w by FUNCT_2:17;
hence w in rng L by P62,FUNCT_2:112;
end;
then Funcs(product(E^<*D*>),F) c= rng L by TARSKI:def 3;
then L is onto by FUNCT_2:def 3,XBOOLE_0:def 10;
hence L is bijective by T1;
thus for f be Function of D,Funcs(product E,F),
e be FinSequence, d be element
st e in product E & d in D holds (L.f).(e^<*d*>) = (f.d).e
proof
let f be Function of D,Funcs(product E,F),
e be FinSequence, d be element;
assume A1: e in product E & d in D; then
A2: (I.f).(e,d) = (f.d).e by P1;
A3: J.(e,d) = e^<*d*> by P2,A1;
[e,d] in [:product E,D:] by A1,ZFMISC_1:def 2; then
A5: J.(e,d) in product(E^<*D*>) & K.(J.(e,d)) = [e,d] by P2,FUNCT_2:5,26;
f in Funcs(D,Funcs(product E,F)) by FUNCT_2:8; then
(L.f).(e^<*d*>) = ((I.f)*K).(J.(e,d)) by A3,P4;
hence (L.f).(e^<*d*>) = (f.d).e by A2,A5,FUNCT_2:15;
end;
end;
reserve S,T for RealNormSpace;
reserve f,f1,f2 for PartFunc of S,T;
reserve Z for Subset of S;
reserve i,n for Nat;
definition let S be set;
assume AS: S is RealNormSpace;
func modetrans(S) -> RealNormSpace equals :defmode:
S;
correctness by AS;
end;
definition let S,T be RealNormSpace;
func diff_SP(S,T) -> Function means :DiffSP:
dom it = NAT & it.0 = T &
for i be Nat holds
it.(i+1) = R_NormSpace_of_BoundedLinearOperators(S,modetrans(it.i));
existence
proof
defpred R[Nat,set,set] means
$3= R_NormSpace_of_BoundedLinearOperators(S,modetrans($2));
A1:for n being Nat for x be set ex y being set st R[n,x,y]
proof
let n be Nat;
let x be set;
take y = R_NormSpace_of_BoundedLinearOperators(S,modetrans(x));
thus thesis;
end;
thus ex g be Function st
dom g = NAT & g.0 = T &
for n being Nat holds R[n,g.n,g.(n+1)] from RECDEF_1:sch 1(A1);
end;
uniqueness
proof
let seq1,seq2 be Function;
assume that
A3: dom seq1 = NAT & seq1.0=T &
for n be Nat holds
seq1.(n+1) = R_NormSpace_of_BoundedLinearOperators(S,modetrans(seq1.n))
and
A5: dom seq2 = NAT & seq2.0=T &
for n be Nat holds
seq2.(n+1) = R_NormSpace_of_BoundedLinearOperators(S,modetrans(seq2.n));
defpred P[Nat] means seq1.$1 = seq2.$1;
A7:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k]; then
seq2.(k+1)
= R_NormSpace_of_BoundedLinearOperators(S,modetrans(seq1.k)) by A5;
hence seq1.(k+1) = seq2.(k+1) by A3;
end;
A9:P[0] by A3,A5;
for n be Nat holds P[n] from NAT_1:sch 2(A9,A7); then
for n be element st n in dom seq1 holds seq1.n = seq2.n by A3;
hence seq1 = seq2 by FUNCT_1:2,A3,A5;
end;
end;
theorem THdiff01:
(diff_SP(S,T)).0 = T &
(diff_SP(S,T)).1 = R_NormSpace_of_BoundedLinearOperators(S,T) &
(diff_SP(S,T)).2
= R_NormSpace_of_BoundedLinearOperators( S,
R_NormSpace_of_BoundedLinearOperators(S,T) )
proof
thus A1: (diff_SP(S,T)).0 = T by DiffSP;
(diff_SP(S,T)).1 = (diff_SP(S,T)).((0 qua Nat) + 1); then
(diff_SP(S,T)).1
= R_NormSpace_of_BoundedLinearOperators(S,modetrans(diff_SP(S,T).0))
by DiffSP;
hence A2: (diff_SP(S,T)).1
= R_NormSpace_of_BoundedLinearOperators(S,T) by A1,defmode;
(diff_SP(S,T)).2 = (diff_SP(S,T)).(1+1); then
(diff_SP(S,T)).2
= R_NormSpace_of_BoundedLinearOperators(S,modetrans(diff_SP(S,T).1))
by DiffSP;
hence (diff_SP(S,T)).2
= R_NormSpace_of_BoundedLinearOperators(S,
R_NormSpace_of_BoundedLinearOperators(S,T) ) by A2,defmode;
end;
theorem THdiff02:
for i be Nat holds (diff_SP(S,T)).i is RealNormSpace
proof
defpred P[Nat] means (diff_SP(S,T)).$1 is RealNormSpace;
P0:P[0] by THdiff01;
P1:now let i be Nat;
assume P[i]; then
reconsider H = diff_SP(S,T).i as RealNormSpace;
modetrans(diff_SP(S,T).i) = H by defmode; then
(diff_SP(S,T)).(i+1)
= R_NormSpace_of_BoundedLinearOperators(S,H) by DiffSP;
hence P[i+1];
end;
for n be Nat holds P[n] from NAT_1:sch 2(P0,P1);
hence thesis;
end;
theorem THdiff03:
for i be Nat holds
ex H be RealNormSpace st H = (diff_SP(S,T)).i
& (diff_SP(S,T)).(i+1) = R_NormSpace_of_BoundedLinearOperators(S,H)
proof
let i be Nat;
take H = modetrans(diff_SP(S,T).i);
thus H = diff_SP(S,T).i by defmode,THdiff02;
thus (diff_SP(S,T)).(i+1)
= R_NormSpace_of_BoundedLinearOperators(S,H) by DiffSP;
end;
definition
let S,T be RealNormSpace, i be Nat;
func diff_SP(i,S,T) -> RealNormSpace equals
diff_SP(S,T).i;
correctness
proof
ex H be RealNormSpace st H = diff_SP(S,T).i
& (diff_SP(S,T)).(i+1) = R_NormSpace_of_BoundedLinearOperators(S,H)
by THdiff03;
hence thesis;
end;
end;
theorem THdiff03A:
for i be Nat holds
diff_SP(i+1,S,T) = R_NormSpace_of_BoundedLinearOperators(S,diff_SP(i,S,T))
proof
let i be Nat;
set H = diff_SP(i,S,T);
ex H1 be RealNormSpace st H1 = (diff_SP(S,T)).i
& (diff_SP(S,T)).(i+1) = R_NormSpace_of_BoundedLinearOperators(S,H1)
by THdiff03;
hence thesis;
end;
definition let S,T be RealNormSpace, f be set;
assume AS: f is PartFunc of S,T;
func modetrans(f,S,T) -> PartFunc of S,T equals :defmode1:
f;
correctness by AS;
end;
definition let S,T be RealNormSpace, f be PartFunc of S,T,
Z be Subset of S;
func diff(f,Z) -> Function means :DiffSQ:
dom it = NAT & it.0 = f|Z &
for i be Nat holds
it.(i+1) = modetrans(it.i,S,diff_SP(i,S,T)) `| Z;
existence
proof
defpred R[Nat,set,set] means
$3= modetrans($2,S,diff_SP($1,S,T)) `| Z;
A1:for n being Nat for x be set ex y being set st R[n,x,y];
ex g be Function st
dom g = NAT & g.0 = f|Z &
for n being Nat holds R[n,g.n,g.(n+1)] from RECDEF_1:sch 1(A1);
hence thesis;
end;
uniqueness
proof
let seq1,seq2 be Function;
assume that
A3: dom seq1 = NAT & seq1.0=f|Z &
for n be Nat holds
seq1.(n+1) = modetrans(seq1.n,S,diff_SP(n,S,T)) `| Z and
A5: dom seq2 = NAT & seq2.0=f|Z &
for n be Nat holds
seq2.(n+1) = modetrans(seq2.n,S,diff_SP(n,S,T)) `| Z;
defpred P[Nat] means seq1.$1 = seq2.$1;
A7:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k]; then
modetrans(seq1.k,S,diff_SP(k,S,T)) `| Z = seq2.(k+1) by A5;
hence seq1.(k+1) = seq2.(k+1) by A3;
end;
A9:P[0] by A3,A5;
for n be Nat holds P[n] from NAT_1:sch 2(A9,A7); then
for n be element st n in dom seq1 holds seq1.n = seq2.n by A3;
hence seq1 = seq2 by FUNCT_1:2,A3,A5;
end;
end;
theorem THdiff04:
diff(f,Z).0 = f|Z & diff(f,Z).1 = (f|Z)`| Z &
diff(f,Z).2 = ((f|Z)`| Z) `| Z
proof
thus A1: diff(f,Z).0 = f|Z by DiffSQ;
B2:diff_SP(0,S,T) = T by THdiff01; then
B3:modetrans(diff(f,Z).0,S,diff_SP(0,S,T)) = f|Z by A1,defmode1;
diff(f,Z).1 = diff(f,Z).( (0 qua Nat) + 1);
hence A2: diff(f,Z).1 = (f|Z)`| Z by B3,B2,DiffSQ;
B5:diff_SP(1,S,T) = R_NormSpace_of_BoundedLinearOperators(S,T)
by THdiff01; then
B6:modetrans(diff(f,Z).1,S,diff_SP(1,S,T))
= (f|Z)`| Z by A2,defmode1;
diff(f,Z).2 = diff(f,Z).( 1 + 1);
hence diff(f,Z).2 = ((f|Z)`| Z) `| Z by B5,B6,DiffSQ;
end;
theorem THdiff05:
for i be Nat holds diff(f,Z).i is PartFunc of S,diff_SP(i,S,T)
proof
defpred P[Nat] means
diff(f,Z).$1 is PartFunc of S,diff_SP($1,S,T);
diff(f,Z).0 = f|Z by DiffSQ; then
P0:P[0] by THdiff01;
P1:now let i be Nat;
assume P[i];
P5: diff(f,Z).(i+1) = (modetrans(diff(f,Z).i,S,diff_SP(i,S,T))) `| Z by DiffSQ;
diff_SP(i+1,S,T)
= R_NormSpace_of_BoundedLinearOperators(S,modetrans(diff_SP(S,T).i))
by DiffSP
.= R_NormSpace_of_BoundedLinearOperators(S,diff_SP(i,S,T)) by defmode;
hence P[i+1] by P5;
end;
for n be Nat holds P[n] from NAT_1:sch 2(P0,P1);
hence thesis;
end;
definition
let S,T be RealNormSpace, f be PartFunc of S,T,
Z be Subset of S, i be Nat;
func diff(f,i,Z) -> PartFunc of S,diff_SP(i,S,T) equals
diff(f,Z).i;
correctness by THdiff05;
end;
theorem THdiff06:
diff(f,i+1,Z) = diff(f,i,Z) `|Z
proof
A1:diff(f,Z).i is PartFunc of S,diff_SP(i,S,T) by THdiff05;
B5:modetrans(diff_SP(S,T).i) = diff_SP(S,T).i by defmode,THdiff02; then
modetrans(diff(f,Z).i,S,modetrans(diff_SP(S,T).i))
= diff(f,Z).i by A1,defmode1;
hence thesis by B5,DiffSQ;
end;
definition
let S,T be RealNormSpace;
let f be PartFunc of S,T;
let Z be Subset of S;
let n be Nat;
pred f is_differentiable_on n,Z means
Z c= dom f
& for i be Nat st i <= n-1 holds
modetrans(diff(f,Z).i,S,diff_SP(i,S,T)) is_differentiable_on Z;
end;
theorem THdiff07:
f is_differentiable_on n,Z
iff
Z c= dom f & for i be Nat st i <= n-1 holds diff(f,i,Z) is_differentiable_on Z
proof
hereby assume A1: f is_differentiable_on n,Z;
hence Z c= dom f;
hereby let i be Nat;
assume i <= n-1; then
modetrans(diff(f,Z).i,S,diff_SP(i,S,T))
is_differentiable_on Z by A1;
hence diff(f,i,Z) is_differentiable_on Z by defmode1;
end;
end;
assume A0: Z c= dom f
& for i be Nat st i<=n-1 holds diff(f,i,Z) is_differentiable_on Z;
now let i be Nat;
assume i <= n-1; then
diff(f,i,Z) is_differentiable_on Z by A0;
hence modetrans(diff(f,Z).i,S,diff_SP(i,S,T))
is_differentiable_on Z by defmode1;
end;
hence f is_differentiable_on n,Z by A0;
end;
theorem THdiff07A:
f is_differentiable_on 1,Z
iff
Z c= dom f & f|Z is_differentiable_on Z
proof
hereby assume A1: f is_differentiable_on 1,Z;
hence Z c= dom f;
A2: diff(f,0,Z) is_differentiable_on Z by A1,THdiff07;
diff(f,Z).0 = f|Z by DiffSQ;
hence f|Z is_differentiable_on Z by A2,THdiff01;
end;
assume AS: Z c= dom f & f|Z is_differentiable_on Z;
for i be Nat st i <= 1-1 holds
diff(f,i,Z) is_differentiable_on Z
proof
let i be Nat;
assume i <= 1-1; then
B1: i = 0;
f|Z = diff(f,0,Z) by DiffSQ;
hence diff(f,i,Z) is_differentiable_on Z by B1,AS,THdiff01;
end;
hence f is_differentiable_on 1,Z by AS,THdiff07;
end;
theorem
f is_differentiable_on 2,Z
iff
Z c= dom f & f|Z is_differentiable_on Z &
(f|Z)`|Z is_differentiable_on Z
proof
hereby assume AS:f is_differentiable_on 2,Z;
hence Z c= dom f;
A1: diff(f,0,Z) is_differentiable_on Z by AS,THdiff07;
diff(f,Z).0 = f|Z by DiffSQ;
hence f|Z is_differentiable_on Z by A1,THdiff01;
A2: diff(f,1,Z) is_differentiable_on Z by AS,THdiff07;
diff(f,Z).1 = (f|Z)`|Z by THdiff04;
hence (f|Z)`|Z is_differentiable_on Z by A2,THdiff01;
end;
assume AS: Z c= dom f & f|Z is_differentiable_on Z
& (f|Z)`|Z is_differentiable_on Z;
for i be Nat st i <= 2-1 holds diff(f,i,Z) is_differentiable_on Z
proof
let i be Nat;
assume A0: i <= 2-1;
per cases;
suppose C1: i = 1;
(f|Z)`|Z = diff(f,1,Z) by THdiff04;
hence diff(f,i,Z) is_differentiable_on Z by C1,AS,THdiff01;
end;
suppose i <> 1; then
i < 1 by A0,XXREAL_0:1; then
A1: i = 0 by NAT_1:14;
f|Z = diff(f,0,Z) by DiffSQ;
hence diff(f,i,Z) is_differentiable_on Z by A1,AS,THdiff01;
end;
end;
hence f is_differentiable_on 2,Z by THdiff07,AS;
end;
theorem THdiff08:
for S,T be RealNormSpace, f be PartFunc of S,T,
Z be Subset of S, n be Nat st
f is_differentiable_on n,Z for m be Nat st m <= n
holds f is_differentiable_on m, Z
proof
let S,T be RealNormSpace,
f be PartFunc of S,T, Z be Subset of S;
let n be Nat such that
A1: f is_differentiable_on n,Z;
let m be Nat;
assume m <=n; then
A3:m-1 <=n-1 by XREAL_1:13;
thus Z c= dom f by A1;
thus thesis by A1,A3,XXREAL_0:2;
end;
theorem THdiff9:
for n be Nat, f be PartFunc of S,T
st 1 <= n & f is_differentiable_on n,Z holds Z is open
proof
let n be Nat, f be PartFunc of S,T;
assume 1 <= n & f is_differentiable_on n,Z; then
f is_differentiable_on 1,Z by THdiff08; then
Z c= dom f & f|Z is_differentiable_on Z by THdiff07A;
hence Z is open by NDIFF_1:32;
end;
theorem THdiff10:
for n being Nat, f being PartFunc of S,T st 1<=n & f is_differentiable_on n,Z
holds
for i being Nat st i <= n holds
diff_SP(S,T).i is RealNormSpace
& diff(f,Z).i is PartFunc of S,diff_SP(i,S,T) & dom diff(f,i,Z) = Z
proof
let n be Nat, f be PartFunc of S,T;
assume AS: 1<=n & f is_differentiable_on n,Z;
let i be Nat;
assume A1: i<=n;
diff_SP(i,S,T) is RealNormSpace;
hence diff_SP(S,T).i is RealNormSpace;
diff(f,i,Z) is PartFunc of S,diff_SP(i,S,T);
hence diff(f,Z).i is PartFunc of S,diff_SP(i,S,T);
per cases;
suppose i = 0; then
f|Z = diff(f,Z).i by DiffSQ;
hence dom diff(f,i,Z) = Z by RELAT_1:62,AS;
end;
suppose i <> 0; then
reconsider i1=i-1 as Element of NAT by INT_1:3;
B3: diff(f,i1+1,Z) = diff(f,i1,Z)`|Z by THdiff06;
diff(f,i1,Z) is_differentiable_on Z by AS,XREAL_1:9,A1,THdiff07;
hence dom diff(f,i,Z) = Z by B3,NDIFF_1:def 9;
end;
end;
theorem THdiff11:
for n being Nat, f,g being PartFunc of S,T
st 1<=n & f is_differentiable_on n,Z & g is_differentiable_on n,Z
holds
for i being Nat st i<=n holds diff(f+g,i,Z) = diff(f,i,Z) + diff(g,i,Z)
proof
let n be Nat, f,g be PartFunc of S,T;
assume AS: 1<=n & f is_differentiable_on n,Z
& g is_differentiable_on n,Z; then
AS12:
Z is open by THdiff9;
defpred P[Nat] means $1 <= n implies
diff(f+g,$1,Z) = diff(f,$1,Z) + diff(g,$1,Z);
P0:P[0]
proof
assume 0<=n;
diff_SP(0,S,T)=T & f|Z=diff(f,0,Z) & g|Z=diff(g,0,Z)
& diff(f+g,0,Z) = (f+g)|Z by DiffSP,DiffSQ;
hence diff(f+g,0,Z) = diff(f,0,Z) + diff(g,0,Z) by VFUNCT_1:27;
end;
PN:for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume A1: P[i];
assume A0: i+1 <= n; then
i + 1 - 1 <= n-1 by XREAL_1:9; then
D1: diff(f,i,Z) is_differentiable_on Z
& diff(g,i,Z) is_differentiable_on Z by THdiff07,AS;
B6: i <= i +1 by NAT_1:11; then
B2: i <= n by A0,XXREAL_0:2;
set f0 = diff(f,i,Z);
set g0 = diff(g,i,Z);
E1: diff_SP(S,T).i is RealNormSpace
& diff(f,Z).i is PartFunc of S,diff_SP(i,S,T) & dom diff(f,i,Z) = Z
by THdiff10,B2,AS;
E2: diff_SP(S,T).i is RealNormSpace
& diff(g,Z).i is PartFunc of S,diff_SP(i,S,T) & dom diff(g,i,Z) = Z
by THdiff10,B2,AS;
Z = (dom f0) /\ Z by E1; then
D6: Z = dom (f0+g0) by E2,VFUNCT_1:def 1; then
f0+g0 is_differentiable_on Z by AS12,D1,NDIFF_1:39; then
D8: dom ((f0+g0)`|Z) = Z by NDIFF_1:def 9;
DD: f0`|Z = diff(f,i+1,Z) & g0`|Z = diff(g,i+1,Z)
& diff(f+g,i+1,Z) = diff(f+g,i,Z)`|Z by THdiff06;
D9: dom(f0`|Z) = Z & dom(g0`|Z) = Z by D1,NDIFF_1:def 9; then
F2: dom(f0`|Z + g0`|Z) = Z /\ Z & dom(diff(f,i+1,Z)+diff(g,i+1,Z)) = Z /\ Z
by DD,VFUNCT_1:def 1;
now let x be Point of S;
assume P1: x in dom(diff(f,i+1,Z) + diff(g,i+1,Z)); then
(f0`|Z + g0`|Z).x = (f0`|Z + g0`|Z)/.x by F2,PARTFUN1:def 6; then
E8: (f0`|Z + g0`|Z).x = (f0`|Z)/.x + (g0`|Z)/.x by P1,F2,VFUNCT_1:def 1;
(f0`|Z)/.x = (diff(f,i+1,Z)).x & (g0`|Z)/.x = (diff(g,i+1,Z)).x
by F2,P1,DD,D9,PARTFUN1:def 6; then
(f0`|Z)/.x = (diff(f,i+1,Z))/.x & (g0`|Z)/.x = (diff(g,i+1,Z))/.x
by F2,P1,DD,D9,PARTFUN1:def 6; then
(f0`|Z + g0`|Z).x = (diff(f,i+1,Z))/.x + (diff(g,i+1,Z))/.x
by E8,THdiff03A; then
(f0`|Z + g0`|Z).x = (diff(f,i+1,Z) + diff(g,i+1,Z))/.x
by P1,VFUNCT_1:def 1; then
P5: (diff(f,i+1,Z) + diff(g,i+1,Z)).x = (f0`|Z + g0`|Z).x
by P1,PARTFUN1:def 6;
((f0+g0)`|Z)/.x = diff(f0,x)+diff(g0,x)
by NDIFF_1:39,D1,AS12,D6,F2,P1; then
P6: ((f0+g0)`|Z)/.x = (f0`|Z)/.x + diff(g0,x) by NDIFF_1:def 9,D1,F2,P1;
(diff(f+g,i+1,Z)).x = ((f0+g0)`|Z)/.x
by DD,A1,B6,F2,D8,P1,PARTFUN1:def 6,A0,XXREAL_0:2;
hence (diff(f+g,i+1,Z)).x = (diff(f,i+1,Z) + diff(g,i+1,Z)).x
by E8,P5,P6,NDIFF_1:def 9,D1,F2,P1;
end;
hence diff(f+g,i+1,Z) = diff(f,i+1,Z) + diff(g,i+1,Z)
by F2,D8,DD,B6,A1,A0,XXREAL_0:2,PARTFUN1:5;
end;
for n be Nat holds P[n] from NAT_1:sch 2(P0,PN);
hence thesis;
end;
theorem
for n be Nat, f,g be PartFunc of S,T
st 1 <= n & f is_differentiable_on n,Z & g is_differentiable_on n,Z
holds f+g is_differentiable_on n,Z
proof
let n be Nat, f,g be PartFunc of S,T;
assume AS: 1<= n & f is_differentiable_on n,Z
& g is_differentiable_on n,Z; then
AS12: Z is open by THdiff9;
Z /\ Z c= (dom f) /\ (dom g) by AS,XBOOLE_1:19; then
A3:Z c= dom (f+g) by VFUNCT_1:def 1;
for i be Nat st i <= n-1 holds
diff(f+g,i,Z) is_differentiable_on Z
proof
let i be Nat;
assume A4: i <= n-1; then
A5: diff(f,i,Z) is_differentiable_on Z & diff(g,i,Z) is_differentiable_on Z
by THdiff07,AS;
n-1 <= n by XREAL_1:43; then
A6: i <= n by A4,XXREAL_0:2; then
dom diff(f,i,Z) = Z & dom diff(g,i,Z) = Z by THdiff10,AS; then
Z /\ Z c= dom diff(f,i,Z) /\ dom diff(g,i,Z); then
Z c= dom (diff(f,i,Z) + diff(g,i,Z)) by VFUNCT_1:def 1; then
diff(f,i,Z) + diff(g,i,Z) is_differentiable_on Z by AS12,A5,NDIFF_1:39;
hence diff(f+g,i,Z) is_differentiable_on Z by AS,A6,THdiff11;
end;
hence thesis by THdiff07,A3;
end;
theorem THdiff12:
for n being Nat, f,g being PartFunc of S,T
st 1<=n & f is_differentiable_on n,Z & g is_differentiable_on n,Z
holds
for i being Nat st i<=n holds diff(f-g,i,Z) = diff(f,i,Z) - diff(g,i,Z)
proof
let n be Nat, f,g be PartFunc of S,T;
assume AS: 1<=n & f is_differentiable_on n,Z
& g is_differentiable_on n,Z; then
AS12:
Z is open by THdiff9;
defpred P[Nat] means $1 <= n implies
diff(f-g,$1,Z) = diff(f,$1,Z) - diff(g,$1,Z);
P0:P[0]
proof
assume 0<=n;
diff_SP(0,S,T)=T & f|Z=diff(f,0,Z) & g|Z=diff(g,0,Z)
& diff(f-g,0,Z) = (f-g)|Z by DiffSP,DiffSQ;
hence diff(f-g,0,Z) = diff(f,0,Z) - diff(g,0,Z) by VFUNCT_1:30;
end;
PN:for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume A1: P[i];
assume A0: i+1 <= n; then
i + 1 - 1 <= n-1 by XREAL_1:9; then
D1: diff(f,i,Z) is_differentiable_on Z
& diff(g,i,Z) is_differentiable_on Z by THdiff07,AS;
B6: i <= i +1 by NAT_1:11; then
B2: i <= n by A0,XXREAL_0:2;
set f0 = diff(f,i,Z);
set g0 = diff(g,i,Z);
E1: diff_SP(S,T).i is RealNormSpace
& diff(f,Z).i is PartFunc of S,diff_SP(i,S,T) & dom diff(f,i,Z) = Z
by THdiff10,B2,AS;
E2: diff_SP(S,T).i is RealNormSpace
& diff(g,Z).i is PartFunc of S,diff_SP(i,S,T) & dom diff(g,i,Z) = Z
by THdiff10,B2,AS;
Z = (dom f0) /\ Z by E1; then
D6: Z = dom (f0-g0) by E2,VFUNCT_1:def 2; then
f0-g0 is_differentiable_on Z by AS12,D1,NDIFF_1:40; then
D8: dom ((f0-g0)`|Z) = Z by NDIFF_1:def 9;
DD: f0`|Z = diff(f,i+1,Z) & g0`|Z = diff(g,i+1,Z)
& diff(f-g,i+1,Z) = diff(f-g,i,Z)`|Z by THdiff06;
D9: dom(f0`|Z) = Z & dom(g0`|Z) = Z by D1,NDIFF_1:def 9; then
F2: dom(f0`|Z - g0`|Z) = Z /\ Z & dom(diff(f,i+1,Z)-diff(g,i+1,Z)) = Z /\ Z
by DD,VFUNCT_1:def 2;
now let x be Point of S;
assume P1: x in dom(diff(f,i+1,Z) - diff(g,i+1,Z)); then
(f0`|Z - g0`|Z).x = (f0`|Z - g0`|Z)/.x by F2,PARTFUN1:def 6; then
E8: (f0`|Z - g0`|Z).x = (f0`|Z)/.x - (g0`|Z)/.x by P1,F2,VFUNCT_1:def 2;
(f0`|Z)/.x = (diff(f,i+1,Z)).x & (g0`|Z)/.x = (diff(g,i+1,Z)).x
by F2,P1,DD,D9,PARTFUN1:def 6; then
(f0`|Z)/.x = (diff(f,i+1,Z))/.x & (g0`|Z)/.x = (diff(g,i+1,Z))/.x
by F2,P1,DD,D9,PARTFUN1:def 6; then
(f0`|Z - g0`|Z).x = (diff(f,i+1,Z))/.x - (diff(g,i+1,Z))/.x
by E8,THdiff03A; then
(f0`|Z - g0`|Z).x = (diff(f,i+1,Z) - diff(g,i+1,Z))/.x
by P1,VFUNCT_1:def 2; then
P5: (diff(f,i+1,Z) - diff(g,i+1,Z)).x = (f0`|Z - g0`|Z).x
by P1,PARTFUN1:def 6;
((f0-g0)`|Z)/.x = diff(f0,x)-diff(g0,x)
by NDIFF_1:40,D1,AS12,D6,F2,P1; then
P6: ((f0-g0)`|Z)/.x = (f0`|Z)/.x - diff(g0,x) by NDIFF_1:def 9,D1,F2,P1;
(diff(f-g,i+1,Z)).x = ((f0-g0)`|Z)/.x
by DD,A1,B6,F2,D8,P1,PARTFUN1:def 6,A0,XXREAL_0:2;
hence (diff(f-g,i+1,Z)).x = (diff(f,i+1,Z) - diff(g,i+1,Z)).x
by E8,P5,P6,NDIFF_1:def 9,D1,F2,P1;
end;
hence diff(f-g,i+1,Z) = diff(f,i+1,Z) - diff(g,i+1,Z)
by F2,D8,DD,B6,A1,A0,XXREAL_0:2,PARTFUN1:5;
end;
for n be Nat holds P[n] from NAT_1:sch 2(P0,PN);
hence thesis;
end;
theorem
for n be Nat, f,g be PartFunc of S,T
st 1 <= n & f is_differentiable_on n,Z & g is_differentiable_on n,Z
holds f-g is_differentiable_on n,Z
proof
let n be Nat, f,g be PartFunc of S,T;
assume AS: 1<= n & f is_differentiable_on n,Z
& g is_differentiable_on n,Z; then
AS12: Z is open by THdiff9;
Z /\ Z c= (dom f) /\ (dom g) by AS,XBOOLE_1:19; then
A3:Z c= dom (f-g) by VFUNCT_1:def 2;
for i be Nat st i <= n-1 holds
diff(f-g,i,Z) is_differentiable_on Z
proof
let i be Nat;
assume A4: i <= n-1; then
A5: diff(f,i,Z) is_differentiable_on Z & diff(g,i,Z) is_differentiable_on Z
by THdiff07,AS;
n-1 <= n by XREAL_1:43; then
A6: i <= n by A4,XXREAL_0:2; then
dom diff(f,i,Z) = Z & dom diff(g,i,Z) = Z by THdiff10,AS; then
Z /\ Z c= dom diff(f,i,Z) /\ dom diff(g,i,Z); then
Z c= dom (diff(f,i,Z) - diff(g,i,Z)) by VFUNCT_1:def 2; then
diff(f,i,Z) - diff(g,i,Z) is_differentiable_on Z by AS12,A5,NDIFF_1:40;
hence diff(f-g,i,Z) is_differentiable_on Z by AS,A6,THdiff12;
end;
hence thesis by THdiff07,A3;
end;
theorem THdiff13:
for n be Nat, r be Real, f be PartFunc of S,T
st 1<= n & f is_differentiable_on n,Z
holds
for i be Nat st i <= n holds diff(r(#)f,i,Z) = r(#)diff(f,i,Z)
proof
let n be Nat, r be Real, f be PartFunc of S,T;
assume AS: 1 <= n & f is_differentiable_on n,Z;
AS12: Z is open by THdiff9,AS;
defpred P[Nat] means $1 <= n implies diff(r(#)f,$1,Z) = r(#)diff(f,$1,Z);
P0:P[0]
proof
assume 0 <= n;
set H = diff_SP(S,T).0;
diff_SP(S,T).0 = T & f|Z = diff(f,0,Z) by DiffSP,DiffSQ; then
(r(#)f)|Z = r(#)diff(f,0,Z) by VFUNCT_1:31;
hence diff(r(#)f,0,Z) = r(#)diff(f,0,Z) by DiffSQ;
end;
PN:for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume A1: P[i];
assume A0: i + 1 <= n;
B2: i <= i + 1 by NAT_1:11; then
B0: i <= n by A0,XXREAL_0:2;
i + 1 - 1 <= n-1 by A0,XREAL_1:9; then
D1: diff(f,i,Z) is_differentiable_on Z by THdiff07,AS; then
D9: Z = (dom (diff(f,i,Z)`|Z)) by NDIFF_1:def 9;
dom diff(f,i,Z) = Z by THdiff10,B0,AS; then
D6: Z = dom (r(#)diff(f,i,Z)) by VFUNCT_1:def 4; then
r(#)diff(f,i,Z) is_differentiable_on Z by AS12,D1,NDIFF_1:41; then
D8: dom ((r(#)diff(f,i,Z))`|Z) = Z by NDIFF_1:def 9;
now let x be Point of S;
assume D10: x in dom ( (r(#)diff(f,i,Z))`|Z ); then
((r(#)diff(f,i,Z))`|Z)/.x = r*diff(diff(f,i,Z),x)
by NDIFF_1:41,D1,AS12,D6,D8;
hence ((r(#)diff(f,i,Z))`|Z)/.x = r*(diff(f,i,Z)`|Z)/.x
by NDIFF_1:def 9,D1,D8,D10;
end; then
D5: (r(#)diff(f,i,Z))`|Z = r(#)(diff(f,i,Z)`|Z) by D8,D9,VFUNCT_1:def 4;
A8: (diff_SP(i+1,S,T))
= R_NormSpace_of_BoundedLinearOperators(S,diff_SP(i,S,T))
by THdiff03A;
diff(r(#)f,i+1,Z) = diff(r(#)f,i,Z)`|Z by THdiff06;
hence diff(r(#)f,i+1,Z) = r(#)diff(f,i+1,Z)
by THdiff06,A8,D5,A1,B2,A0,XXREAL_0:2;
end;
for n be Nat holds P[n] from NAT_1:sch 2(P0,PN);
hence thesis;
end;
theorem THdiff16:
for n be Nat, r be Real, f be PartFunc of S,T
st 1 <= n & f is_differentiable_on n,Z
holds r(#)f is_differentiable_on n,Z
proof
let n be Nat, r be Real, f be PartFunc of S,T;
assume AS: 1 <= n & f is_differentiable_on n,Z; then
A3:Z c= dom (r(#)f) by VFUNCT_1:def 4;
AS12: Z is open by THdiff9,AS;
for i be Nat st i <= n-1 holds diff(r(#)f,i,Z) is_differentiable_on Z
proof
let i be Nat;
assume A4: i <= n-1;
set H = diff_SP(i,S,T);
set f1 = diff(f,i,Z);
A5: diff(f,i,Z) is_differentiable_on Z by AS,A4,THdiff07;
n-1 - 0 <= n-1 + 1 by XREAL_1:7; then
B0: i <= n by A4,XXREAL_0:2; then
B1: diff(r(#)f,i,Z) = r(#)diff(f,i,Z) by AS,THdiff13;
dom diff(f,i,Z) = Z by THdiff10,B0,AS; then
Z c= dom (r(#)f1) by VFUNCT_1:def 4;
hence diff(r(#)f,i,Z) is_differentiable_on Z by AS12,A5,B1,NDIFF_1:41;
end;
hence thesis by THdiff07,A3;
end;
theorem
for n be Nat, f be PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z
holds
for i be Nat st i <= n holds diff(-f,i,Z) = -diff(f,i,Z)
proof
let n be Nat, f be PartFunc of S,T;
assume AS: 1 <= n & f is_differentiable_on n,Z;
let i be Nat;
assume i <= n; then
diff((-1)(#)f,i,Z) = (-1)(#)diff(f,i,Z) by THdiff13,AS; then
diff((-1)(#)f,Z).i = -diff(f,i,Z) by VFUNCT_1:23;
hence diff(-f,i,Z) = -diff(f,i,Z) by VFUNCT_1:23;
end;
theorem
for n be Nat, f be PartFunc of S,T st 1<= n & f is_differentiable_on n,Z
holds -f is_differentiable_on n,Z
proof
let n be Nat, f be PartFunc of S,T;
assume 1 <= n & f is_differentiable_on n, Z; then
(-1)(#)f is_differentiable_on n,Z by THdiff16;
hence thesis by VFUNCT_1:23;
end;