let E, G, F be RealNormSpace; :: thesis: for Z being Subset of [:E,F:]
for f being PartFunc of [:E,F:],G
for a being Point of E
for b being Point of F
for c being Point of G
for z being Point of [:E,F:]
for A being Subset of E
for B being Subset of F
for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & z = [a,b] & f . (a,b) = c & f is_differentiable_in z & dom g = A & rng g c= B & a in A & g . a = b & g is_continuous_in a & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is invertible holds
( g is_differentiable_in a & diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) )
let Z be Subset of [:E,F:]; :: thesis: for f being PartFunc of [:E,F:],G
for a being Point of E
for b being Point of F
for c being Point of G
for z being Point of [:E,F:]
for A being Subset of E
for B being Subset of F
for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & z = [a,b] & f . (a,b) = c & f is_differentiable_in z & dom g = A & rng g c= B & a in A & g . a = b & g is_continuous_in a & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is invertible holds
( g is_differentiable_in a & diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) )
let f be PartFunc of [:E,F:],G; :: thesis: for a being Point of E
for b being Point of F
for c being Point of G
for z being Point of [:E,F:]
for A being Subset of E
for B being Subset of F
for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & z = [a,b] & f . (a,b) = c & f is_differentiable_in z & dom g = A & rng g c= B & a in A & g . a = b & g is_continuous_in a & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is invertible holds
( g is_differentiable_in a & diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) )
let a be Point of E; :: thesis: for b being Point of F
for c being Point of G
for z being Point of [:E,F:]
for A being Subset of E
for B being Subset of F
for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & z = [a,b] & f . (a,b) = c & f is_differentiable_in z & dom g = A & rng g c= B & a in A & g . a = b & g is_continuous_in a & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is invertible holds
( g is_differentiable_in a & diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) )
let b be Point of F; :: thesis: for c being Point of G
for z being Point of [:E,F:]
for A being Subset of E
for B being Subset of F
for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & z = [a,b] & f . (a,b) = c & f is_differentiable_in z & dom g = A & rng g c= B & a in A & g . a = b & g is_continuous_in a & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is invertible holds
( g is_differentiable_in a & diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) )
let c be Point of G; :: thesis: for z being Point of [:E,F:]
for A being Subset of E
for B being Subset of F
for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & z = [a,b] & f . (a,b) = c & f is_differentiable_in z & dom g = A & rng g c= B & a in A & g . a = b & g is_continuous_in a & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is invertible holds
( g is_differentiable_in a & diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) )
let z be Point of [:E,F:]; :: thesis: for A being Subset of E
for B being Subset of F
for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & z = [a,b] & f . (a,b) = c & f is_differentiable_in z & dom g = A & rng g c= B & a in A & g . a = b & g is_continuous_in a & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is invertible holds
( g is_differentiable_in a & diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) )
let A be Subset of E; :: thesis: for B being Subset of F
for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & z = [a,b] & f . (a,b) = c & f is_differentiable_in z & dom g = A & rng g c= B & a in A & g . a = b & g is_continuous_in a & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is invertible holds
( g is_differentiable_in a & diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) )
let B be Subset of F; :: thesis: for g being PartFunc of E,F st Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & z = [a,b] & f . (a,b) = c & f is_differentiable_in z & dom g = A & rng g c= B & a in A & g . a = b & g is_continuous_in a & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is invertible holds
( g is_differentiable_in a & diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) )
let g be PartFunc of E,F; :: thesis: ( Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & z = [a,b] & f . (a,b) = c & f is_differentiable_in z & dom g = A & rng g c= B & a in A & g . a = b & g is_continuous_in a & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is invertible implies ( g is_differentiable_in a & diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) )
assume A1: ( Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & z = [a,b] & f . (a,b) = c & f is_differentiable_in z & dom g = A & rng g c= B & a in A & g . a = b & g is_continuous_in a & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & partdiff`2 (f,z) is invertible ) ; :: thesis: ( g is_differentiable_in a & diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) )
then b in rng g by FUNCT_1:def 3;
then consider r2 being Real such that
A3: ( 0 < r2 & Ball (b,r2) c= B ) by A1, NDIFF_8:20;
consider r3 being Real such that
A4: ( 0 < r3 & ( for x1 being Point of E st x1 in dom g & ||.(x1 - a).|| < r3 holds
||.((g /. x1) - (g /. a)).|| < r2 ) ) by A1, A3, NFCONT_1:7;
consider r4 being Real such that
A5: ( 0 < r4 & Ball (a,r4) c= A ) by A1, NDIFF_8:20;
set r1 = min (r3,r4);
A6: ( 0 < min (r3,r4) & min (r3,r4) <= r3 & min (r3,r4) <= r4 ) by A4, A5, XXREAL_0:17, XXREAL_0:21;
set g1 = g | (Ball (a,(min (r3,r4))));
B6: Ball (a,(min (r3,r4))) c= Ball (a,r4) by A6, NDIFF_8:15;
then A7: Ball (a,(min (r3,r4))) c= A by A5, XBOOLE_1:1;
A8: dom (g | (Ball (a,(min (r3,r4))))) = Ball (a,(min (r3,r4))) by A1, A5, B6, RELAT_1:62, XBOOLE_1:1;
A17: a in Ball (a,(min (r3,r4))) by A6, NDIFF_8:13;
A26: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of E st x1 in dom (g | (Ball (a,(min (r3,r4))))) & ||.(x1 - a).|| < s holds
||.(((g | (Ball (a,(min (r3,r4))))) /. x1) - ((g | (Ball (a,(min (r3,r4))))) /. a)).|| < r ) ) A28: for x being Point of E st x in Ball (a,(min (r3,r4))) holds
f . (x,((g | (Ball (a,(min (r3,r4))))) . x)) = c b in Ball (b,r2) by A3, NDIFF_8:13;
then A31: [a,b] in [:(Ball (a,(min (r3,r4)))),(Ball (b,r2)):] by A17, ZFMISC_1:87;
A32: [:(Ball (a,(min (r3,r4)))),(Ball (b,r2)):] c= [:A,B:] by A3, A7, ZFMISC_1:96;
reconsider Q = (partdiff`2 (f,z)) " as Lipschitzian LinearOperator of G,F by A1, LOPBAN_1:def 9;
reconsider P = partdiff`1 (f,z) as Lipschitzian LinearOperator of E,G by LOPBAN_1:def 9;
( Z is open & dom f = Z & z = [a,b] & z in Z & f . (a,b) = c & f is_differentiable_in z & 0 < min (r3,r4) & 0 < r2 & dom (g | (Ball (a,(min (r3,r4))))) = Ball (a,(min (r3,r4))) & rng (g | (Ball (a,(min (r3,r4))))) c= Ball (b,r2) & (g | (Ball (a,(min (r3,r4))))) . a = b & g | (Ball (a,(min (r3,r4)))) is_continuous_in a & ( for x being Point of E st x in Ball (a,(min (r3,r4))) holds
f . (x,((g | (Ball (a,(min (r3,r4))))) . x)) = c ) & partdiff`2 (f,z) is one-to-one & Q = (partdiff`2 (f,z)) " & P = partdiff`1 (f,z) ) by A1, A3, A6, A8, B8, A26, A28, A31, A32, FUNCT_1:49, NDIFF_8:13, NFCONT_1:7, TARSKI:def 3;
then A33: ( g | (Ball (a,(min (r3,r4)))) is_differentiable_in a & diff ((g | (Ball (a,(min (r3,r4))))),a) = - (Q * P) ) by Th5;
then consider N being Neighbourhood of a such that
A34: ( N c= dom (g | (Ball (a,(min (r3,r4))))) & ex R being RestFunc of E,F st
for x being Point of E st x in N holds
((g | (Ball (a,(min (r3,r4))))) /. x) - ((g | (Ball (a,(min (r3,r4))))) /. a) = ((diff ((g | (Ball (a,(min (r3,r4))))),a)) . (x - a)) + (R /. (x - a)) ) by NDIFF_1:def 7;
consider R being RestFunc of E,F such that
A35: for x being Point of E st x in N holds
((g | (Ball (a,(min (r3,r4))))) /. x) - ((g | (Ball (a,(min (r3,r4))))) /. a) = ((diff ((g | (Ball (a,(min (r3,r4))))),a)) . (x - a)) + (R /. (x - a)) by A34;
A37: N c= A by A7, A8, A34, XBOOLE_1:1;
A38: N c= dom g by A1, A7, A8, A34, XBOOLE_1:1;
A39: for x being Point of E st x in N holds
(g /. x) - (g /. a) = ((diff ((g | (Ball (a,(min (r3,r4))))),a)) . (x - a)) + (R /. (x - a)) hence g is_differentiable_in a by A1, A7, A8, A34, NDIFF_1:def 6, XBOOLE_1:1; :: thesis: diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z)))
then A48: diff (g,a) = diff ((g | (Ball (a,(min (r3,r4))))),a) by A38, A39, NDIFF_1:def 7;
Q = Inv (partdiff`2 (f,z)) by A1, LOPBAN13:def 2;
then modetrans ((Inv (partdiff`2 (f,z))),G,F) = Q by LOPBAN_1:def 11;
then A51: (Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z)) = Q * P by LOPBAN_1:def 11;
then Q * P is Lipschitzian LinearOperator of E,F by LOPBAN_1:def 9;
hence diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) by A33, A48, A51, LOPBAN13:31; :: thesis: verum