let u be PartFunc of (REAL 2),REAL ; :: thesis: for x0, y0 being Real
for xy0 being Element of REAL 2 st xy0 = <*x0,y0*> & <>* u is_differentiable_in xy0 holds
( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & <*(partdiff u,xy0,1)*> = (diff (<>* u),xy0) . <*1,0 *> & <*(partdiff u,xy0,2)*> = (diff (<>* u),xy0) . <*0 ,1*> )
let x0, y0 be Real; :: thesis: for xy0 being Element of REAL 2 st xy0 = <*x0,y0*> & <>* u is_differentiable_in xy0 holds
( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & <*(partdiff u,xy0,1)*> = (diff (<>* u),xy0) . <*1,0 *> & <*(partdiff u,xy0,2)*> = (diff (<>* u),xy0) . <*0 ,1*> )
let xy0 be Element of REAL 2; :: thesis: ( xy0 = <*x0,y0*> & <>* u is_differentiable_in xy0 implies ( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & <*(partdiff u,xy0,1)*> = (diff (<>* u),xy0) . <*1,0 *> & <*(partdiff u,xy0,2)*> = (diff (<>* u),xy0) . <*0 ,1*> ) )
assume that
A2:
xy0 = <*x0,y0*>
and
A3:
<>* u is_differentiable_in xy0
; :: thesis: ( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & <*(partdiff u,xy0,1)*> = (diff (<>* u),xy0) . <*1,0 *> & <*(partdiff u,xy0,2)*> = (diff (<>* u),xy0) . <*0 ,1*> )
reconsider zxy0 = xy0 as Point of (REAL-NS 2) by A2, Lm021;
reconsider ex0 = <*1,0 *> as Point of (REAL-NS 2) by Lm021;
reconsider ey0 = <*0 ,1*> as Point of (REAL-NS 2) by Lm021;
consider g being PartFunc of (REAL-NS 2),(REAL-NS 1), gxy0 being Point of (REAL-NS 2) such that
X1:
( <>* u = g & xy0 = gxy0 & g is_differentiable_in gxy0 )
by A3, PDIFF_1:def 7;
consider f being PartFunc of (REAL-NS 2),(REAL-NS 1), fxy0 being Point of (REAL-NS 2) such that
X2:
( <>* u = f & xy0 = fxy0 & diff (<>* u),xy0 = diff f,fxy0 )
by A3, PDIFF_1:def 8;
consider N being Neighbourhood of gxy0 such that
X3:
( N c= dom g & ex R being REST of (REAL-NS 2),(REAL-NS 1) st
for xy being Point of (REAL-NS 2) st xy in N holds
(g /. xy) - (g /. gxy0) = ((diff g,gxy0) . (xy - gxy0)) + (R /. (xy - gxy0)) )
by NDIFF_1:def 7, X1;
consider R being REST of (REAL-NS 2),(REAL-NS 1) such that
X4:
for xy being Point of (REAL-NS 2) st xy in N holds
(g /. xy) - (g /. gxy0) = ((diff g,gxy0) . (xy - gxy0)) + (R /. (xy - gxy0))
by X3;
set W = (proj 1,1) " ;
rng u c= dom ((proj 1,1) " )
by PDIFF_1:2;
then V01:
dom (<>* u) = dom u
by RELAT_1:46;
LmXY:
for xy being Element of REAL 2
for L1, R1 being Real
for z being Element of REAL 2 st xy in N & z = xy - xy0 & <*L1*> = (diff (<>* u),xy0) . z & <*R1*> = R . z holds
(u . xy) - (u . xy0) = L1 + R1
proof
let xy be
Element of
REAL 2;
:: thesis: for L1, R1 being Real
for z being Element of REAL 2 st xy in N & z = xy - xy0 & <*L1*> = (diff (<>* u),xy0) . z & <*R1*> = R . z holds
(u . xy) - (u . xy0) = L1 + R1let L1,
R1 be
Real;
:: thesis: for z being Element of REAL 2 st xy in N & z = xy - xy0 & <*L1*> = (diff (<>* u),xy0) . z & <*R1*> = R . z holds
(u . xy) - (u . xy0) = L1 + R1let z be
Element of
REAL 2;
:: thesis: ( xy in N & z = xy - xy0 & <*L1*> = (diff (<>* u),xy0) . z & <*R1*> = R . z implies (u . xy) - (u . xy0) = L1 + R1 )
assume AS1:
(
xy in N &
z = xy - xy0 &
<*L1*> = (diff (<>* u),xy0) . z &
<*R1*> = R . z )
;
:: thesis: (u . xy) - (u . xy0) = L1 + R1
set W =
(proj 1,1) " ;
P11:
xy0 in N
by X1, NFCONT_1:4;
reconsider zxy =
xy as
Point of
(REAL-NS 2) by REAL_NS1:def 4;
reconsider dxy =
z as
Point of
(REAL-NS 2) by REAL_NS1:def 4;
P1:
(g /. zxy) - (g /. gxy0) = ((diff g,gxy0) . (zxy - gxy0)) + (R /. (zxy - gxy0))
by X4, AS1;
P21:
g /. zxy =
g . xy
by PARTFUN1:def 8, AS1, X3
.=
(<>* u) /. xy
by PARTFUN1:def 8, AS1, X1, X3
;
P22:
g /. gxy0 =
g . xy0
by PARTFUN1:def 8, X1, X3, P11
.=
(<>* u) /. xy0
by PARTFUN1:def 8, P11, X1, X3
;
P23:
(<>* u) /. xy =
(<>* u) . xy
by AS1, X3, X1, PARTFUN1:def 8
.=
<*(u . xy)*>
by Lm022, AS1, X3, X1, V01
;
P24:
(<>* u) /. xy0 =
(<>* u) . xy0
by P11, X1, X3, PARTFUN1:def 8
.=
<*(u . xy0)*>
by Lm022, P11, X1, X3, V01
;
P2:
(g /. zxy) - (g /. gxy0) =
<*(u . xy)*> - <*(u . xy0)*>
by P21, P22, REAL_NS1:5, P23, P24
.=
<*(u . xy)*> + <*(- (u . xy0))*>
by RVSUM_1:38
.=
<*((u . xy) - (u . xy0))*>
by RVSUM_1:29
;
P9:
zxy - gxy0 = z
by AS1, X1, REAL_NS1:5;
R is
total
by NDIFF_1:def 5;
then
dom R = the
carrier of
(REAL-NS 2)
by PARTFUN1:def 4;
then
R /. (zxy - gxy0) = <*R1*>
by P9, PARTFUN1:def 8, AS1;
then
((diff g,gxy0) . (zxy - gxy0)) + (R /. (zxy - gxy0)) = <*(L1 + R1)*>
by X1, X2, AS1, P9, Lm012;
hence (u . xy) - (u . xy0) =
<*(L1 + R1)*> . 1
by FINSEQ_1:def 8, P1, P2
.=
L1 + R1
by FINSEQ_1:def 8
;
:: thesis: verum
end;
consider r0 being Real such that
P991:
( 0 < r0 & { xy where xy is Point of (REAL-NS 2) : ||.(xy - gxy0).|| < r0 } c= N )
by NFCONT_1:def 3;
set Nx0 = ].(x0 - r0),(x0 + r0).[;
reconsider Nx0 = ].(x0 - r0),(x0 + r0).[ as Neighbourhood of x0 by P991, RCOMP_1:def 7;
P9x0:
for x being Real st x in Nx0 holds
<*x,y0*> in N
proof
let x be
Real;
:: thesis: ( x in Nx0 implies <*x,y0*> in N )
assume
x in Nx0
;
:: thesis: <*x,y0*> in N
then K1:
|.(x - x0).| < r0
by RCOMP_1:8;
reconsider xy =
<*x,y0*> as
Point of
(REAL-NS 2) by Lm021;
K2:
xy - gxy0 =
<*(x - x0),(y0 - y0)*>
by X1, A2, Lm212
.=
<*(x - x0),0 *>
;
reconsider xx =
<*(x - x0),0 *> as
Element of
REAL 2
by FINSEQ_2:121;
reconsider xx1 =
xx as
Point of
(TOP-REAL 2) by EUCLID:25;
K4:
xx1 `2 = 0
by FINSEQ_1:61;
K5:
abs (xx1 `1 ) = |.(x - x0).|
by FINSEQ_1:61;
K6:
abs (xx1 `2 ) = 0
by K4, ABSVALUE:7;
K7:
|.xx.| <= (abs (xx1 `1 )) + (abs (xx1 `2 ))
by JGRAPH_1:48;
||.(xy - gxy0).|| = |.xx.|
by K2, REAL_NS1:1;
then
||.(xy - gxy0).|| < r0
by K1, K7, K5, K6, XXREAL_0:2;
then
xy in { z where z is Point of (REAL-NS 2) : ||.(z - gxy0).|| < r0 }
;
hence
<*x,y0*> in N
by P991;
:: thesis: verum
end;
set Ny0 = ].(y0 - r0),(y0 + r0).[;
reconsider Ny0 = ].(y0 - r0),(y0 + r0).[ as Neighbourhood of y0 by P991, RCOMP_1:def 7;
P9y0:
for y being Real st y in Ny0 holds
<*x0,y*> in N
proof
let y be
Real;
:: thesis: ( y in Ny0 implies <*x0,y*> in N )
assume
y in Ny0
;
:: thesis: <*x0,y*> in N
then K1:
|.(y - y0).| < r0
by RCOMP_1:8;
reconsider xy =
<*x0,y*> as
Point of
(REAL-NS 2) by Lm021;
K2:
xy - gxy0 =
<*(x0 - x0),(y - y0)*>
by X1, A2, Lm212
.=
<*0 ,(y - y0)*>
;
reconsider xx =
<*0 ,(y - y0)*> as
Element of
REAL 2
by FINSEQ_2:121;
reconsider xx1 =
xx as
Point of
(TOP-REAL 2) by EUCLID:25;
K3:
xx1 `1 = 0
by FINSEQ_1:61;
K5:
abs (xx1 `1 ) = 0
by K3, ABSVALUE:7;
|.xx.| <= (abs (xx1 `1 )) + (abs (xx1 `2 ))
by JGRAPH_1:48;
then K7:
|.xx.| <= |.(y - y0).|
by K5, FINSEQ_1:61;
||.(xy - gxy0).|| = |.xx.|
by K2, REAL_NS1:1;
then
||.(xy - gxy0).|| < r0
by K1, K7, XXREAL_0:2;
then
xy in { z where z is Point of (REAL-NS 2) : ||.(z - gxy0).|| < r0 }
;
hence
<*x0,y*> in N
by P991;
:: thesis: verum
end;
defpred S1[ Element of REAL , Element of REAL ] means ex vx being Element of REAL 2 st
( vx = <*$1,0 *> & <*$2*> = R . vx );
consider R1 being Function of REAL ,REAL such that
P501:
for x being Element of REAL holds S1[x,R1 . x]
from FUNCT_2:sch 10(S1);
defpred S2[ Element of REAL , Element of REAL ] means ex vy being Element of REAL 2 st
( vy = <*0 ,$1*> & <*$2*> = R . vy );
consider R3 being Function of REAL ,REAL such that
P501:
for x being Element of REAL holds S2[x,R3 . x]
from FUNCT_2:sch 10(S1);
Z2:
for h being convergent_to_0 Real_Sequence holds
( (h " ) (#) (R1 /* h) is convergent & lim ((h " ) (#) (R1 /* h)) = 0 )
reconsider R1 = R1 as REST by FDIFF_1:def 3, Z2;
Z6:
for h being convergent_to_0 Real_Sequence holds
( (h " ) (#) (R3 /* h) is convergent & lim ((h " ) (#) (R3 /* h)) = 0 )
reconsider R3 = R3 as REST by FDIFF_1:def 3, Z6;
P141: (proj 1,2) . xy0 =
xy0 . 1
by PDIFF_1:def 1
.=
x0
by A2, FINSEQ_1:61
;
P142: (proj 2,2) . xy0 =
xy0 . 2
by PDIFF_1:def 1
.=
y0
by A2, FINSEQ_1:61
;
P15u:
for x being Real holds (u * (reproj 1,xy0)) . x = u . <*x,y0*>
proof
let x be
Real;
:: thesis: (u * (reproj 1,xy0)) . x = u . <*x,y0*>
x in REAL
;
then P1:
x in dom (reproj 1,xy0)
by PDIFF_1:def 5;
thus (u * (reproj 1,xy0)) . x =
u . ((reproj 1,xy0) . x)
by P1, FUNCT_1:23
.=
u . (Replace xy0,1,x)
by PDIFF_1:def 5
.=
u . <*x,y0*>
by A2, FINSEQ_7:15
;
:: thesis: verum
end;
P16u:
for y being Real holds (u * (reproj 2,xy0)) . y = u . <*x0,y*>
ex0 is Element of REAL 2
by REAL_NS1:def 4;
then
(diff (<>* u),xy0) . ex0 is Element of REAL 1
by FUNCT_2:7;
then consider Dux being Real such that
P17a:
<*Dux*> = (diff (<>* u),xy0) . ex0
by FINSEQ_2:117;
deffunc H1( Real) -> Element of REAL = Dux * $1;
consider LD1 being Function of REAL ,REAL such that
P17:
for x being Real holds LD1 . x = H1(x)
from FUNCT_2:sch 4();
ey0 is Element of REAL 2
by REAL_NS1:def 4;
then
(diff (<>* u),xy0) . ey0 is Element of REAL 1
by FUNCT_2:7;
then consider Duy being Real such that
P18a:
<*Duy*> = (diff (<>* u),xy0) . ey0
by FINSEQ_2:117;
deffunc H2( Real) -> Element of REAL = Duy * $1;
consider LD3 being Function of REAL ,REAL such that
P18:
for x being Real holds LD3 . x = H2(x)
from FUNCT_2:sch 4();
reconsider LD1 = LD1 as LINEAR by FDIFF_1:def 4, P17;
reconsider LD3 = LD3 as LINEAR by FDIFF_1:def 4, P18;
P30u:
for x being Real st x in Nx0 holds
((u * (reproj 1,xy0)) . x) - ((u * (reproj 1,xy0)) . x0) = (LD1 . (x - x0)) + (R1 . (x - x0))
proof
let x be
Real;
:: thesis: ( x in Nx0 implies ((u * (reproj 1,xy0)) . x) - ((u * (reproj 1,xy0)) . x0) = (LD1 . (x - x0)) + (R1 . (x - x0)) )
assume AS30:
x in Nx0
;
:: thesis: ((u * (reproj 1,xy0)) . x) - ((u * (reproj 1,xy0)) . x0) = (LD1 . (x - x0)) + (R1 . (x - x0))
reconsider xy =
<*x,y0*> as
Element of
REAL 2
by FINSEQ_2:121;
ex0 is
Element of
REAL 2
by REAL_NS1:def 4;
then reconsider D1 =
(diff (<>* u),xy0) . ex0 as
Element of
REAL 1
by FUNCT_2:7;
L01:
xy - xy0 =
<*(x - x0),(y0 - y0)*>
by Lm014, A2
.=
<*((x - x0) * 1),((x - x0) * 0 )*>
.=
(x - x0) * ex0
by Lm213
;
L02:
diff f,
fxy0 is
LinearOperator of
(REAL-NS 2),
(REAL-NS 1)
by LOPBAN_1:def 10;
L0:
(x - x0) * D1 =
(x - x0) * ((diff f,fxy0) . ex0)
by X2, REAL_NS1:3
.=
(diff (<>* u),xy0) . (xy - xy0)
by L01, L02, LOPBAN_1:def 6, X2
;
LD1 . (x - x0) = Dux * (x - x0)
by P17;
then L1:
<*(LD1 . (x - x0))*> = (diff (<>* u),xy0) . (xy - xy0)
by P17a, RVSUM_1:69, L0;
<*(x - x0),0 *> =
<*(x - x0),(y0 - y0)*>
.=
xy - xy0
by Lm014, A2
;
then L2:
<*(R1 . (x - x0))*> = R . (xy - xy0)
by P500;
thus ((u * (reproj 1,xy0)) . x) - ((u * (reproj 1,xy0)) . x0) =
(u . <*x,y0*>) - ((u * (reproj 1,xy0)) . x0)
by P15u
.=
(u . xy) - (u . xy0)
by P15u, A2
.=
(LD1 . (x - x0)) + (R1 . (x - x0))
by L1, L2, AS30, P9x0, LmXY
;
:: thesis: verum
end;
P31u:
for y being Real st y in Ny0 holds
((u * (reproj 2,xy0)) . y) - ((u * (reproj 2,xy0)) . y0) = (LD3 . (y - y0)) + (R3 . (y - y0))
proof
let y be
Real;
:: thesis: ( y in Ny0 implies ((u * (reproj 2,xy0)) . y) - ((u * (reproj 2,xy0)) . y0) = (LD3 . (y - y0)) + (R3 . (y - y0)) )
assume AS31:
y in Ny0
;
:: thesis: ((u * (reproj 2,xy0)) . y) - ((u * (reproj 2,xy0)) . y0) = (LD3 . (y - y0)) + (R3 . (y - y0))
reconsider xy =
<*x0,y*> as
Element of
REAL 2
by FINSEQ_2:121;
ey0 is
Element of
REAL 2
by REAL_NS1:def 4;
then reconsider D1 =
(diff (<>* u),xy0) . ey0 as
Element of
REAL 1
by FUNCT_2:7;
L01:
xy - xy0 =
<*(x0 - x0),(y - y0)*>
by Lm014, A2
.=
<*((y - y0) * 0 ),((y - y0) * 1)*>
.=
(y - y0) * ey0
by Lm213
;
L02:
diff f,
fxy0 is
LinearOperator of
(REAL-NS 2),
(REAL-NS 1)
by LOPBAN_1:def 10;
L0:
(y - y0) * D1 =
(y - y0) * ((diff f,fxy0) . ey0)
by X2, REAL_NS1:3
.=
(diff (<>* u),xy0) . (xy - xy0)
by L01, L02, LOPBAN_1:def 6, X2
;
LD3 . (y - y0) = Duy * (y - y0)
by P18;
then L1:
<*(LD3 . (y - y0))*> = (diff (<>* u),xy0) . (xy - xy0)
by P18a, RVSUM_1:69, L0;
<*0 ,(y - y0)*> =
<*(x0 - x0),(y - y0)*>
.=
xy - xy0
by Lm014, A2
;
then L2:
<*(R3 . (y - y0))*> = R . (xy - xy0)
by P502;
thus ((u * (reproj 2,xy0)) . y) - ((u * (reproj 2,xy0)) . y0) =
(u . <*x0,y*>) - ((u * (reproj 2,xy0)) . y0)
by P16u
.=
(u . xy) - (u . xy0)
by P16u, A2
.=
(LD3 . (y - y0)) + (R3 . (y - y0))
by L1, L2, AS31, P9y0, LmXY
;
:: thesis: verum
end;
P51: LD1 . 1 =
Dux * 1
by P17
.=
Dux
;
PL01:
dom (reproj 1,xy0) = REAL
by FUNCT_2:def 1;
now let s be
set ;
:: thesis: ( s in (reproj 1,xy0) .: Nx0 implies s in dom u )assume
s in (reproj 1,xy0) .: Nx0
;
:: thesis: s in dom uthen consider x being
Element of
REAL such that PL2:
(
x in Nx0 &
s = (reproj 1,xy0) . x )
by FUNCT_2:116;
PL3:
s =
Replace xy0,1,
x
by PDIFF_1:def 5, PL2
.=
<*x,y0*>
by A2, FINSEQ_7:15
;
<*x,y0*> in N
by P9x0, PL2;
hence
s in dom u
by X3, X1, V01, PL3;
:: thesis: verum end;
then
(reproj 1,xy0) .: Nx0 c= dom u
by TARSKI:def 3;
then P61:
Nx0 c= dom (u * (reproj 1,xy0))
by PL01, FUNCT_3:3;
then P71:
u * (reproj 1,xy0) is_differentiable_in (proj 1,2) . xy0
by FDIFF_1:def 5, P30u, P141;
Q51: LD3 . 1 =
Duy * 1
by P18
.=
Duy
;
PL01:
dom (reproj 2,xy0) = REAL
by FUNCT_2:def 1;
now let s be
set ;
:: thesis: ( s in (reproj 2,xy0) .: Ny0 implies s in dom u )assume
s in (reproj 2,xy0) .: Ny0
;
:: thesis: s in dom uthen consider y being
Element of
REAL such that PL2:
(
y in Ny0 &
s = (reproj 2,xy0) . y )
by FUNCT_2:116;
PL3:
s =
Replace xy0,2,
y
by PDIFF_1:def 5, PL2
.=
<*x0,y*>
by A2, FINSEQ_7:16
;
<*x0,y*> in N
by P9y0, PL2;
hence
s in dom u
by X3, X1, V01, PL3;
:: thesis: verum end;
then
(reproj 2,xy0) .: Ny0 c= dom u
by TARSKI:def 3;
then Q61:
Ny0 c= dom (u * (reproj 2,xy0))
by PL01, FUNCT_3:3;
then
u * (reproj 2,xy0) is_differentiable_in (proj 2,2) . xy0
by FDIFF_1:def 5, P31u, P142;
hence
( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & <*(partdiff u,xy0,1)*> = (diff (<>* u),xy0) . <*1,0 *> & <*(partdiff u,xy0,2)*> = (diff (<>* u),xy0) . <*0 ,1*> )
by P71, P17a, FDIFF_1:def 6, P51, P61, P30u, P141, Q51, Q61, P31u, P142, P18a, PDIFF_1:def 11; :: thesis: verum