:: Differentiation in Normed Spaces
:: by Noboru Endou and Yasunari Shidama
::
:: Received May 19, 2013
:: Copyright (c) 2013-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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 object 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[object,object] 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 object st d in D & e in E holds g.(d,e) = (f.d).e;
A1:for x be object st x in Funcs(D,Funcs(E,F))
ex y be object st y in Funcs([:D,E:],F) & P[x,y]
proof
let x be object;
assume x in Funcs(D,Funcs(E,F)); then
consider f being Function such that
A2: 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,A2;
deffunc F0(object, object) = (f.$1).$2;
A3:for x,y be object st x in D & y in E holds F0(x,y) in F
proof
let d,e be object;
assume A4: d in D & e in E; then
f.d is Function of E,F by FUNCT_2:5,66;
hence thesis by A4,FUNCT_2:5;
end;
consider g being Function of [:D,E:],F such that
A5: for x,y be object st
x in D & y in E holds g.(x,y) = F0(x,y) from BINOP_1:sch 2(A3);
g in Funcs([:D,E:],F) by FUNCT_2:8;
hence thesis by A2,A5;
end;
consider I be Function of Funcs(D,Funcs(E,F)), Funcs([:D,E:],F) such that
A6: for x be object st x in Funcs(D,Funcs(E,F)) holds P[x,I.x]
from FUNCT_2:sch 1(A1);
A7:for f be Function of D,Funcs(E,F), d,e be object 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 object;
assume A8: 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 object st d in D & e in E holds g0.(d,e) = (f0.d).e by A6;
hence (I.f).(d,e) = (f.d).e by A8;
end;
now let z1,z2 be object;
assume A9: 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 object;
assume A10: d in D; then
A11: z1f.d is Function of E,F & z2f.d is Function of E,F by FUNCT_2:5,66;
now let e be object;
assume A12: e in E; then
(z1f.d).e = (I.z2f).(d,e) by A7,A10,A9;
hence (z1f.d).e = (z2f.d).e by A7,A10,A12;
end;
hence z1f.d = z2f.d by A11,FUNCT_2:12;
end;
hence z1=z2 by FUNCT_2:12;
end; then
A13:I is one-to-one by FUNCT_2:19;
now let w be object;
assume w in Funcs([:D,E:],F); then
reconsider wf = w as Function of [:D,E:],F by FUNCT_2:66;
defpred P[object,object] means
ex f be Function of E,F st
$2=f &
for e be object st e in E holds f.e = wf.($1,e);
A14: for d be object st d in D ex y be object st y in Funcs(E,F) & P[d,y]
proof
let d be object;
assume A15: d in D;
deffunc F0(object) = wf.(d,$1);
A16: for e be object st e in E holds F0(e) in F
proof
let e be object;
assume e in E; then
[d,e] in [:D,E:] by A15,ZFMISC_1:def 2;
hence thesis by FUNCT_2:5;
end;
consider f being Function of E,F such that
A17: for e be object st e in E holds f.e = F0(e) from FUNCT_2:sch 2(A16);
f in Funcs(E,F) by FUNCT_2:8;
hence thesis by A17;
end;
consider zf be Function of D,Funcs(E,F) such that
A18: for d be object st d in D holds P[d,zf.d] from FUNCT_2:sch 1(A14);
A19: zf in Funcs(D,Funcs(E,F)) by FUNCT_2:8;
A20: now let d,e be set;
assume A21: d in D & e in E; then
A22: (I.zf).(d,e) = (zf.d).e by A7;
ex L be Function of E,F st
zf.d = L
& for e be object st e in E holds L.e = wf.(d,e) by A18,A21;
hence (I.zf).(d,e) = wf.(d,e) by A22,A21;
end;
I.zf is Function of [:D,E:],F by A19,FUNCT_2:5,66; then
I.zf = w by BINOP_1:1,A20;
hence w in rng I by A19,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 A7,A13;
end;
theorem Th2:
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 object
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[object,object] 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 object st e in E & d in D holds g.(e,d) = (f.d).e;
A1:for x be object st x in Funcs(D,Funcs(E,F))
ex y be object st y in Funcs([:E,D:],F) & P[x,y]
proof
let x be object;
assume x in Funcs(D,Funcs(E,F)); then
consider f being Function such that
A2: 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,A2;
deffunc F0(object,object) = (f.$2).$1;
A3:for y,x be object st y in E & x in D holds F0(y,x) in F
proof
let e,d be object;
assume A4: 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 A4,FUNCT_2:5;
end;
consider g being Function of [:E,D:],F such that
A5: for y,x be object st
y in E & x in D holds g.(y,x) = F0(y,x) from BINOP_1:sch 2(A3);
g in Funcs([:E,D:],F) by FUNCT_2:8;
hence thesis by A2,A5;
end;
consider I be Function of Funcs(D,Funcs(E,F)), Funcs([:E,D:],F)
such that
A6: for x be object st x in Funcs(D,Funcs(E,F)) holds P[x,I.x]
from FUNCT_2:sch 1(A1);
A7:for f be Function of D,Funcs(E,F), e,d be object 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 object;
assume A8: 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 object st e in E & d in D holds
g0.(e,d) = (f0.d).e by A6;
hence (I.f).(e,d) = (f.d).e by A8;
end;
now let z1,z2 be object;
assume A9: 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 object;
assume A10: d in D; then
A11: z1f.d is Function of E,F & z2f.d is Function of E,F by FUNCT_2:5,66;
now let e be object;
assume A12: e in E; then
(z1f.d).e = (I.z2f).(e,d) by A7,A10,A9;
hence (z1f.d).e = (z2f.d).e by A7,A10,A12;
end;
hence z1f.d = z2f.d by A11,FUNCT_2:12;
end;
hence z1=z2 by FUNCT_2:12;
end; then
A13:I is one-to-one by FUNCT_2:19;
now let w be object;
assume w in Funcs([:E,D:],F); then
reconsider wf = w as Function of [:E,D:],F by FUNCT_2:66;
defpred P[object,object] means
ex f be Function of E,F
st $2=f & for e be object st e in E holds f.e = wf.(e,$1);
A14: for d be object st d in D
ex y be object st y in Funcs(E,F) & P[d,y]
proof
let d be object;
assume A15: d in D;
deffunc F0(object) = wf.($1,d);
A16: for e be object st e in E holds F0(e) in F
proof
let e be object;
assume e in E; then
[e,d] in [:E,D:] by A15,ZFMISC_1:def 2;
hence thesis by FUNCT_2:5;
end;
consider f being Function of E,F such that
A17: for e be object st e in E holds f.e = F0(e) from FUNCT_2:sch 2(A16);
f in Funcs(E,F) by FUNCT_2:8;
hence thesis by A17;
end;
consider zf be Function of D,Funcs(E,F) such that
A18: for d be object st d in D holds P[d,zf.d] from FUNCT_2:sch 1(A14);
A19: zf in Funcs(D,Funcs(E,F)) by FUNCT_2:8;
A20: now let e,d be set;
assume A21: e in E & d in D; then
A22: (I.zf).(e,d) = (zf.d).e by A7;
ex L be Function of E,F st
zf.d = L &
for e be object st e in E holds L.e = wf.(e,d) by A18,A21;
hence (I.zf).(e,d) = wf.(e,d) by A22,A21;
end;
I.zf is Function of [:E,D:],F by A19,FUNCT_2:5,66; then
I.zf = w by BINOP_1:1,A20;
hence w in rng I by A19,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 A7,A13;
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
A1: I is bijective
& for f be Function of product D,Funcs(product E,F), e,d be object
st e in product E & d in product D
holds (I.f).(e,d) = (f.d).e by Th2;
consider J be Function of [: product E,product D :],product(E^D)
such that
A2: 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;
A3:
rng J = product(E^D) by A2,FUNCT_2:def 3; then
reconsider K = J" as Function of product(E^D),[: product E,product D :]
by FUNCT_2:25,A2;
deffunc F0(object)=(I.$1) * K;
A4:for x be object st x in Funcs(product D,Funcs(product E,F))
holds F0(x) in Funcs(product(E^D),F)
proof
let x be object;
assume x in Funcs(product D,Funcs(product E,F)); then
A5: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 A5,FUNCT_2:128;
end;
consider L being Function of Funcs(product D,Funcs(product E,F)),
Funcs(product(E^D),F) such that
A6: for e be object st e in Funcs(product D,Funcs(product E,F))
holds L.e = F0(e) from FUNCT_2:sch 2(A4);
A7:
K*J = id [:product E,product D:] by A2,A3,FUNCT_2:29;
A8:
J*K = id product(E^D) by A2,A3,FUNCT_2:29;
now let z1,z2 be object;
assume A9: 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 A6,A9; then
A10:((I.z1) * K)*J =((I.z2) * K)*J by A6,A9;
(I.z1)*(K*J) =((I.z1) * K)*J by RELAT_1:36; then
A11:(I.z1)*(K*J) = (I.z2)*(K*J) by A10,RELAT_1:36;
I.z1 is Function of [:product E,product D:],F &
I.z2 is Function of [:product E,product D:],F by A9,FUNCT_2:5,66; then
(I.z1)*(K*J) = I.z1 & (I.z2)*(K*J) = I.z2 by A7,FUNCT_2:17;
hence z1=z2 by A1,FUNCT_2:19,A9,A11;
end; then
A12:L is one-to-one by FUNCT_2:19;
now let w be object;
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 A1,FUNCT_2:def 3; then
consider zf be object such that
A13: zf in Funcs(product D,Funcs(product E,F)) & I.zf = wf*J by FUNCT_2:11;
L.zf = wf*J*K by A6,A13; then
L.zf = wf* id (product(E^D)) by A8,RELAT_1:36; then
L.zf =w by FUNCT_2:17;
hence w in rng L by A13,FUNCT_2:112;
end;
then Funcs(product(E^D),F) c= rng L by TARSKI:def 3; then
A14: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 A15: e in product E & d in product D; then
A16: (I.f).(e,d) = (f.d).e by A1;
A17: J.(e,d) = e^d by A2,A15;
A18: [e,d] in [: product E,product D :] by A15,ZFMISC_1:87;
A19: K.(J.(e,d)) = [e,d] by FUNCT_2:26,A2,A15,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 A17,A6;
hence (L.f).(e^d) = (f.d).e by A16,A19,A18,FUNCT_2:5,15;
end;
hence thesis by A12,A14;
end;
theorem Th4:
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 object 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 object st y in Y holds J.y = <*y*> by PRVECT_3:4;
defpred P[object,object,object] means $3 = [ $1,<* $2 *> ];
A2:for x,y be object st x in X & y in Y
ex z be object st z in [:X,product <*Y*>:] & P[x,y,z]
proof
let x,y be object;
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 object 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 object;
assume A5: z1 in [:X,Y:] & z2 in [:X,Y:] & I.z1=I.z2; then
consider x1,y1 be object such that
A6: x1 in X & y1 in Y & z1=[x1,y1] by ZFMISC_1:def 2;
consider x2,y2 be object 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 A8: I is one-to-one by FUNCT_2:19;
now let w be object;
assume w in [:X, product <*Y*>:]; then
consider x,y1 be object such that
A9: x in X & y1 in product <*Y*> & w=[x,y1] by ZFMISC_1:def 2;
y1 in rng J by A1,A9,FUNCT_2:def 3; then
consider y be object such that
A10: y in Y & y1=J.y by FUNCT_2:11;
J.y = <*y*> by A10,A1; then
A11:w = I.(x,y) by A4,A9,A10;
[x,y] in [:X,Y:] by A9,A10,ZFMISC_1:87;
hence w in rng I by A11,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,A8;
end;
theorem Th5:
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 object
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 object, y be object
st x in product X & y in Y holds I.(x,y) = [x,<*y*>] by Th4;
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;
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 object st
x in product X & y in Y holds K.(x,y) = x^<*y*>
proof
let x be FinSequence, y be object;
assume A4:x in product X & y in Y; then
A5: I.(x,y) = [x,<*y*>] by A1;
[x,y] in [:product X,Y:] by A4,ZFMISC_1:87; then
I.([x,y]) in [:product X,product <*Y*>:] by FUNCT_2:5; then
<*y*> in product <*Y*> by A5,ZFMISC_1:87; then
J.(x,<*y*>) = x^<*y*> by A4,A2;
hence thesis by A5,A4,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 object
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
A1: I is bijective
& for f be Function of D,Funcs(product E,F), e,d be object
st e in product E & d in D holds (I.f).(e,d) = (f.d).e by Th2;
consider J be Function of [: product E,D :],product(E^<*D*>) such that
A2: J is bijective
& for x be FinSequence, y be object st x in product E & y in D
holds J.(x,y) = x^<*y*> by Th5;
A3:rng J = product(E^<*D*>) by A2,FUNCT_2:def 3; then
reconsider K = J" as Function of product(E^<*D*>),[:product E,D:]
by FUNCT_2:25,A2;
deffunc F0(object)=(I.$1) * K;
A4:for x be object st x in Funcs(D,Funcs(product E,F))
holds F0(x) in Funcs(product(E^<*D*>),F)
proof
let x be object;
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
A5: for e be object st
e in Funcs(D,Funcs(product E,F)) holds L.e = F0(e) from FUNCT_2:sch 2(A4);
take L;
A6:
(K*J) = id [: product E,D :] by A2,A3,FUNCT_2:29;
A7:
(J*K) = id product(E^<*D*>) by A2,A3,FUNCT_2:29;
now let z1,z2 be object;
assume A8: 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 A5,A8; then
A9:((I.z1) * K)*J =((I.z2) * K)*J by A5,A8;
(I.z1)*(K*J) = ((I.z1)* K)*J by RELAT_1:36; then
A10:(I.z1)*(K*J) = (I.z2)*(K*J) by A9,RELAT_1:36;
I.z1 is Function of [:product E,D:],F &
I.z2 is Function of [:product E,D:],F by A8,FUNCT_2:5,66; then
(I.z1)*(K*J) = I.z1 & (I.z2)*(K*J) = I.z2 by A6,FUNCT_2:17;
hence z1=z2 by A1,FUNCT_2:19,A8,A10;
end;
then A11: L is one-to-one by FUNCT_2:19;
now let w be object;
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 A1,FUNCT_2:def 3; then
consider zf be object such that
A12: zf in Funcs(D,Funcs(product E,F)) & I.zf = wf*J by FUNCT_2:11;
L.zf = wf*J*K by A5,A12; then
L.zf = wf* id (product(E^<*D*>)) by A7,RELAT_1:36; then
L.zf = w by FUNCT_2:17;
hence w in rng L by A12,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 A11;
thus for f be Function of D,Funcs(product E,F),
e be FinSequence, d be object
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 object;
assume A13: e in product E & d in D; then
A14: (I.f).(e,d) = (f.d).e by A1;
A15: J.(e,d) = e^<*d*> by A2,A13;
[e,d] in [:product E,D:] by A13,ZFMISC_1:def 2; then
A16: J.(e,d) in product(E^<*D*>) & K.(J.(e,d)) = [e,d] by A2,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 A15,A5;
hence (L.f).(e^<*d*>) = (f.d).e by A14,A16,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 A1: S is RealNormSpace;
func modetrans(S) -> RealNormSpace equals :Def1:
S;
correctness by A1;
end;
definition let S,T be RealNormSpace;
func diff_SP(S,T) -> Function means :Def2:
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
A2: dom seq1 = NAT & seq1.0=T &
for n be Nat holds
seq1.(n+1) = R_NormSpace_of_BoundedLinearOperators(S,modetrans(seq1.n))
and
A3: 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;
A4: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 A3;
hence seq1.(k+1) = seq2.(k+1) by A2;
end;
A5:P[0] by A2,A3;
for n be Nat holds P[n] from NAT_1:sch 2(A5,A4); then
for n be object st n in dom seq1 holds seq1.n = seq2.n by A2;
hence seq1 = seq2 by FUNCT_1:2,A2,A3;
end;
end;
theorem Th7:
(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 Def2;
(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 Def2;
hence A2: (diff_SP(S,T)).1
= R_NormSpace_of_BoundedLinearOperators(S,T) by A1,Def1;
(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 Def2;
hence (diff_SP(S,T)).2
= R_NormSpace_of_BoundedLinearOperators(S,
R_NormSpace_of_BoundedLinearOperators(S,T) ) by A2,Def1;
end;
theorem Th8:
for i be Nat holds (diff_SP(S,T)).i is RealNormSpace
proof
defpred P[Nat] means (diff_SP(S,T)).$1 is RealNormSpace;
A1:P[0] by Th7;
A2: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 Def1; then
(diff_SP(S,T)).(i+1)
= R_NormSpace_of_BoundedLinearOperators(S,H) by Def2;
hence P[i+1];
end;
for n be Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th9:
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 Def1,Th8;
thus (diff_SP(S,T)).(i+1)
= R_NormSpace_of_BoundedLinearOperators(S,H) by Def2;
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 Th9;
hence thesis;
end;
end;
theorem Th10:
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 Th9;
hence thesis;
end;
definition let S,T be RealNormSpace, f be set;
assume A1: f is PartFunc of S,T;
func modetrans(f,S,T) -> PartFunc of S,T equals :Def4:
f;
correctness by A1;
end;
definition let S,T be RealNormSpace, f be PartFunc of S,T,
Z be Subset of S;
func diff(f,Z) -> Function means :Def5:
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
A2: 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
A3: 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;
A4: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 A3;
hence seq1.(k+1) = seq2.(k+1) by A2;
end;
A5:P[0] by A2,A3;
for n be Nat holds P[n] from NAT_1:sch 2(A5,A4); then
for n be object st n in dom seq1 holds seq1.n = seq2.n by A2;
hence seq1 = seq2 by FUNCT_1:2,A2,A3;
end;
end;
theorem Th11:
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 Def5;
A2:diff_SP(0,S,T) = T by Th7; then
A3:modetrans(diff(f,Z).0,S,diff_SP(0,S,T)) = f|Z by A1,Def4;
diff(f,Z).1 = diff(f,Z).( (0 qua Nat) + 1);
hence A4: diff(f,Z).1 = (f|Z)`| Z by A3,A2,Def5;
A5:diff_SP(1,S,T) = R_NormSpace_of_BoundedLinearOperators(S,T)
by Th7; then
A6:modetrans(diff(f,Z).1,S,diff_SP(1,S,T))
= (f|Z)`| Z by A4,Def4;
diff(f,Z).2 = diff(f,Z).( 1 + 1);
hence diff(f,Z).2 = ((f|Z)`| Z) `| Z by A5,A6,Def5;
end;
theorem Th12:
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 Def5; then
A1:P[0] by Th7;
A2:now let i be Nat;
assume P[i];
A3: diff(f,Z).(i+1) = (modetrans(diff(f,Z).i,S,diff_SP(i,S,T))) `| Z by Def5;
diff_SP(i+1,S,T)
= R_NormSpace_of_BoundedLinearOperators(S,modetrans(diff_SP(S,T).i))
by Def2
.= R_NormSpace_of_BoundedLinearOperators(S,diff_SP(i,S,T)) by Def1;
hence P[i+1] by A3;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A1,A2);
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 Th12;
end;
theorem Th13:
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 Th12;
A2:modetrans(diff_SP(S,T).i) = diff_SP(S,T).i by Def1,Th8; then
modetrans(diff(f,Z).i,S,modetrans(diff_SP(S,T).i))
= diff(f,Z).i by A1,Def4;
hence thesis by A2,Def5;
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 Th14:
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 Def4;
end;
end;
assume A2: 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 A2;
hence modetrans(diff(f,Z).i,S,diff_SP(i,S,T))
is_differentiable_on Z by Def4;
end;
hence f is_differentiable_on n,Z by A2;
end;
theorem Th15:
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,Th14;
diff(f,Z).0 = f|Z by Def5;
hence f|Z is_differentiable_on Z by A2,Th7;
end;
assume A3: 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
A4: i = 0;
f|Z = diff(f,0,Z) by Def5;
hence diff(f,i,Z) is_differentiable_on Z by A4,A3,Th7;
end;
hence f is_differentiable_on 1,Z by A3,Th14;
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 A1:f is_differentiable_on 2,Z;
hence Z c= dom f;
A2: diff(f,0,Z) is_differentiable_on Z by A1,Th14;
diff(f,Z).0 = f|Z by Def5;
hence f|Z is_differentiable_on Z by A2,Th7;
A3: diff(f,1,Z) is_differentiable_on Z by A1,Th14;
diff(f,Z).1 = (f|Z)`|Z by Th11;
hence (f|Z)`|Z is_differentiable_on Z by A3,Th7;
end;
assume A4: 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 A5: i <= 2-1;
per cases;
suppose A6: i = 1;
(f|Z)`|Z = diff(f,1,Z) by Th11;
hence diff(f,i,Z) is_differentiable_on Z by A6,A4,Th7;
end;
suppose i <> 1; then
i < 1 by A5,XXREAL_0:1; then
A7: i = 0 by NAT_1:14;
f|Z = diff(f,0,Z) by Def5;
hence diff(f,i,Z) is_differentiable_on Z by A7,A4,Th7;
end;
end;
hence f is_differentiable_on 2,Z by Th14,A4;
end;
theorem Th17:
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
A2:m-1 <=n-1 by XREAL_1:13;
thus Z c= dom f by A1;
thus thesis by A1,A2,XXREAL_0:2;
end;
theorem Th18:
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 Th17; then
Z c= dom f & f|Z is_differentiable_on Z by Th15;
hence Z is open by NDIFF_1:32;
end;
theorem Th19:
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 A1: 1<=n & f is_differentiable_on n,Z;
let i be Nat;
assume A2: 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 Def5;
hence dom diff(f,i,Z) = Z by RELAT_1:62,A1;
end;
suppose i <> 0; then
reconsider i1=i-1 as Element of NAT by INT_1:3;
A3: diff(f,i1+1,Z) = diff(f,i1,Z)`|Z by Th13;
diff(f,i1,Z) is_differentiable_on Z by A1,XREAL_1:9,A2,Th14;
hence dom diff(f,i,Z) = Z by A3,NDIFF_1:def 9;
end;
end;
theorem Th20:
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 A1: 1<=n & f is_differentiable_on n,Z
& g is_differentiable_on n,Z; then
A2:
Z is open by Th18;
defpred P[Nat] means $1 <= n implies
diff(f+g,$1,Z) = diff(f,$1,Z) + diff(g,$1,Z);
A3: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 Def2,Def5;
hence diff(f+g,0,Z) = diff(f,0,Z) + diff(g,0,Z) by VFUNCT_1:27;
end;
A4:for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume A5: P[i];
assume A6: i+1 <= n; then
i + 1 - 1 <= n-1 by XREAL_1:9; then
A7: diff(f,i,Z) is_differentiable_on Z
& diff(g,i,Z) is_differentiable_on Z by Th14,A1;
A8: i <= i +1 by NAT_1:11; then
A9: i <= n by A6,XXREAL_0:2;
set f0 = diff(f,i,Z);
set g0 = diff(g,i,Z);
A10: 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 Th19,A9,A1;
A11: 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 Th19,A9,A1;
Z = (dom f0) /\ Z by A10; then
A12: Z = dom (f0+g0) by A11,VFUNCT_1:def 1; then
f0+g0 is_differentiable_on Z by A2,A7,NDIFF_1:39; then
A13: dom ((f0+g0)`|Z) = Z by NDIFF_1:def 9;
A14: 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 Th13;
A15: dom(f0`|Z) = Z & dom(g0`|Z) = Z by A7,NDIFF_1:def 9; then
A16: dom(f0`|Z + g0`|Z) = Z /\ Z & dom(diff(f,i+1,Z)+diff(g,i+1,Z)) = Z /\ Z
by A14,VFUNCT_1:def 1;
now let x be Point of S;
assume A17: 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 A16,PARTFUN1:def 6; then
A18: (f0`|Z + g0`|Z).x = (f0`|Z)/.x + (g0`|Z)/.x by A17,A16,VFUNCT_1:def 1;
(f0`|Z)/.x = (diff(f,i+1,Z)).x & (g0`|Z)/.x = (diff(g,i+1,Z)).x
by A16,A17,A14,A15,PARTFUN1:def 6; then
(f0`|Z)/.x = (diff(f,i+1,Z))/.x & (g0`|Z)/.x = (diff(g,i+1,Z))/.x
by A16,A17,A14,A15,PARTFUN1:def 6; then
(f0`|Z + g0`|Z).x = (diff(f,i+1,Z))/.x + (diff(g,i+1,Z))/.x
by A18,Th10; then
(f0`|Z + g0`|Z).x = (diff(f,i+1,Z) + diff(g,i+1,Z))/.x
by A17,VFUNCT_1:def 1; then
A19: (diff(f,i+1,Z) + diff(g,i+1,Z)).x = (f0`|Z + g0`|Z).x
by A17,PARTFUN1:def 6;
((f0+g0)`|Z)/.x = diff(f0,x)+diff(g0,x)
by NDIFF_1:39,A7,A2,A12,A16,A17; then
A20: ((f0+g0)`|Z)/.x = (f0`|Z)/.x + diff(g0,x) by NDIFF_1:def 9,A7,A16,A17;
(diff(f+g,i+1,Z)).x = ((f0+g0)`|Z)/.x
by A14,A5,A8,A16,A13,A17,PARTFUN1:def 6,A6,XXREAL_0:2;
hence (diff(f+g,i+1,Z)).x = (diff(f,i+1,Z) + diff(g,i+1,Z)).x
by A18,A19,A20,NDIFF_1:def 9,A7,A16,A17;
end;
hence diff(f+g,i+1,Z) = diff(f,i+1,Z) + diff(g,i+1,Z)
by A16,A13,A14,A8,A5,A6,XXREAL_0:2,PARTFUN1:5;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A3,A4);
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 A1: 1<= n & f is_differentiable_on n,Z
& g is_differentiable_on n,Z; then
A2: Z is open by Th18;
Z /\ Z c= (dom f) /\ (dom g) by A1,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 Th14,A1;
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 Th19,A1; 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 A2,A5,NDIFF_1:39;
hence diff(f+g,i,Z) is_differentiable_on Z by A1,A6,Th20;
end;
hence thesis by Th14,A3;
end;
theorem Th22:
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 A1: 1<=n & f is_differentiable_on n,Z
& g is_differentiable_on n,Z; then
A2:
Z is open by Th18;
defpred P[Nat] means $1 <= n implies
diff(f-g,$1,Z) = diff(f,$1,Z) - diff(g,$1,Z);
A3: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 Def2,Def5;
hence diff(f-g,0,Z) = diff(f,0,Z) - diff(g,0,Z) by VFUNCT_1:30;
end;
A4:for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume A5: P[i];
assume A6: i+1 <= n; then
i + 1 - 1 <= n-1 by XREAL_1:9; then
A7: diff(f,i,Z) is_differentiable_on Z
& diff(g,i,Z) is_differentiable_on Z by Th14,A1;
A8: i <= i +1 by NAT_1:11; then
A9: i <= n by A6,XXREAL_0:2;
set f0 = diff(f,i,Z);
set g0 = diff(g,i,Z);
A10: 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 Th19,A9,A1;
A11: 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 Th19,A9,A1;
Z = (dom f0) /\ Z by A10; then
A12: Z = dom (f0-g0) by A11,VFUNCT_1:def 2; then
f0-g0 is_differentiable_on Z by A2,A7,NDIFF_1:40; then
A13: dom ((f0-g0)`|Z) = Z by NDIFF_1:def 9;
A14: 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 Th13;
A15: dom(f0`|Z) = Z & dom(g0`|Z) = Z by A7,NDIFF_1:def 9; then
A16: dom(f0`|Z - g0`|Z) = Z /\ Z & dom(diff(f,i+1,Z)-diff(g,i+1,Z)) = Z /\ Z
by A14,VFUNCT_1:def 2;
now let x be Point of S;
assume A17: 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 A16,PARTFUN1:def 6; then
A18: (f0`|Z - g0`|Z).x = (f0`|Z)/.x - (g0`|Z)/.x by A17,A16,VFUNCT_1:def 2;
(f0`|Z)/.x = (diff(f,i+1,Z)).x & (g0`|Z)/.x = (diff(g,i+1,Z)).x
by A16,A17,A14,A15,PARTFUN1:def 6; then
(f0`|Z)/.x = (diff(f,i+1,Z))/.x & (g0`|Z)/.x = (diff(g,i+1,Z))/.x
by A16,A17,A14,A15,PARTFUN1:def 6; then
(f0`|Z - g0`|Z).x = (diff(f,i+1,Z))/.x - (diff(g,i+1,Z))/.x
by A18,Th10; then
(f0`|Z - g0`|Z).x = (diff(f,i+1,Z) - diff(g,i+1,Z))/.x
by A17,VFUNCT_1:def 2; then
A19: (diff(f,i+1,Z) - diff(g,i+1,Z)).x = (f0`|Z - g0`|Z).x
by A17,PARTFUN1:def 6;
((f0-g0)`|Z)/.x = diff(f0,x)-diff(g0,x)
by NDIFF_1:40,A7,A2,A12,A16,A17; then
A20: ((f0-g0)`|Z)/.x = (f0`|Z)/.x - diff(g0,x) by NDIFF_1:def 9,A7,A16,A17;
(diff(f-g,i+1,Z)).x = ((f0-g0)`|Z)/.x
by A14,A5,A8,A16,A13,A17,PARTFUN1:def 6,A6,XXREAL_0:2;
hence (diff(f-g,i+1,Z)).x = (diff(f,i+1,Z) - diff(g,i+1,Z)).x
by A18,A19,A20,NDIFF_1:def 9,A7,A16,A17;
end;
hence diff(f-g,i+1,Z) = diff(f,i+1,Z) - diff(g,i+1,Z)
by A16,A13,A14,A8,A5,A6,XXREAL_0:2,PARTFUN1:5;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A3,A4);
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 A1: 1<= n & f is_differentiable_on n,Z
& g is_differentiable_on n,Z; then
A2: Z is open by Th18;
Z /\ Z c= (dom f) /\ (dom g) by A1,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 Th14,A1;
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 Th19,A1; 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 A2,A5,NDIFF_1:40;
hence diff(f-g,i,Z) is_differentiable_on Z by A1,A6,Th22;
end;
hence thesis by Th14,A3;
end;
theorem Th24:
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 A1: 1 <= n & f is_differentiable_on n,Z;
A2: Z is open by Th18,A1;
defpred P[Nat] means $1 <= n implies diff(r(#)f,$1,Z) = r(#)diff(f,$1,Z);
A3: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 Def2,Def5; 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 Def5;
end;
A4:for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume A5: P[i];
assume A6: i + 1 <= n;
A7: i <= i + 1 by NAT_1:11; then
A8: i <= n by A6,XXREAL_0:2;
i + 1 - 1 <= n-1 by A6,XREAL_1:9; then
A9: diff(f,i,Z) is_differentiable_on Z by Th14,A1; then
A10: Z = (dom (diff(f,i,Z)`|Z)) by NDIFF_1:def 9;
dom diff(f,i,Z) = Z by Th19,A8,A1; then
A11: Z = dom (r(#)diff(f,i,Z)) by VFUNCT_1:def 4; then
r(#)diff(f,i,Z) is_differentiable_on Z by A2,A9,NDIFF_1:41; then
A12: dom ((r(#)diff(f,i,Z))`|Z) = Z by NDIFF_1:def 9;
now let x be Point of S;
assume A13: 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,A9,A2,A11,A12;
hence ((r(#)diff(f,i,Z))`|Z)/.x = r*(diff(f,i,Z)`|Z)/.x
by NDIFF_1:def 9,A9,A12,A13;
end; then
A14: (r(#)diff(f,i,Z))`|Z = r(#)(diff(f,i,Z)`|Z) by A12,A10,VFUNCT_1:def 4;
A15: (diff_SP(i+1,S,T))
= R_NormSpace_of_BoundedLinearOperators(S,diff_SP(i,S,T))
by Th10;
diff(r(#)f,i+1,Z) = diff(r(#)f,i,Z)`|Z by Th13;
hence diff(r(#)f,i+1,Z) = r(#)diff(f,i+1,Z)
by Th13,A15,A14,A5,A7,A6,XXREAL_0:2;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A3,A4);
hence thesis;
end;
theorem Th25:
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 A1: 1 <= n & f is_differentiable_on n,Z; then
A2:Z c= dom (r(#)f) by VFUNCT_1:def 4;
A3: Z is open by Th18,A1;
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 A1,A4,Th14;
n-1 - 0 <= n-1 + 1 by XREAL_1:7; then
A6: i <= n by A4,XXREAL_0:2; then
A7: diff(r(#)f,i,Z) = r(#)diff(f,i,Z) by A1,Th24;
dom diff(f,i,Z) = Z by Th19,A6,A1; then
Z c= dom (r(#)f1) by VFUNCT_1:def 4;
hence diff(r(#)f,i,Z) is_differentiable_on Z by A3,A5,A7,NDIFF_1:41;
end;
hence thesis by Th14,A2;
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 A1: 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 Th24,A1; 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 Th25;
hence thesis by VFUNCT_1:23;
end;