let m, n be non empty Element of NAT ; for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x0 being Point of (REAL-NS m)
for i being Element of NAT st 1 <= i & i <= n & g is_differentiable_in x0 holds
( (Proj i,n) * g is_differentiable_in x0 & (Proj i,n) * (diff g,x0) = diff ((Proj i,n) * g),x0 )
let g be PartFunc of (REAL-NS m),(REAL-NS n); for x0 being Point of (REAL-NS m)
for i being Element of NAT st 1 <= i & i <= n & g is_differentiable_in x0 holds
( (Proj i,n) * g is_differentiable_in x0 & (Proj i,n) * (diff g,x0) = diff ((Proj i,n) * g),x0 )
let x0 be Point of (REAL-NS m); for i being Element of NAT st 1 <= i & i <= n & g is_differentiable_in x0 holds
( (Proj i,n) * g is_differentiable_in x0 & (Proj i,n) * (diff g,x0) = diff ((Proj i,n) * g),x0 )
let i be Element of NAT ; ( 1 <= i & i <= n & g is_differentiable_in x0 implies ( (Proj i,n) * g is_differentiable_in x0 & (Proj i,n) * (diff g,x0) = diff ((Proj i,n) * g),x0 ) )
assume AS0:
( 1 <= i & i <= n & g is_differentiable_in x0 )
; ( (Proj i,n) * g is_differentiable_in x0 & (Proj i,n) * (diff g,x0) = diff ((Proj i,n) * g),x0 )
then consider N being Neighbourhood of x0 such that
AS1:
( N c= dom g & ex GR being REST of (REAL-NS m),(REAL-NS n) st
for x being Point of (REAL-NS m) st x in N holds
(g /. x) - (g /. x0) = ((diff g,x0) . (x - x0)) + (GR /. (x - x0)) )
by NDIFF_1:def 7;
consider GR being REST of (REAL-NS m),(REAL-NS n) such that
AS2:
for x being Point of (REAL-NS m) st x in N holds
(g /. x) - (g /. x0) = ((diff g,x0) . (x - x0)) + (GR /. (x - x0))
by AS1;
set RLB = R_NormSpace_of_BoundedLinearOperators (REAL-NS m),(REAL-NS n);
set RLB0 = R_NormSpace_of_BoundedLinearOperators (REAL-NS m),(REAL-NS 1);
reconsider DFG = diff g,x0 as LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def 10;
reconsider PG = Proj i,n as Function of the carrier of (REAL-NS n),the carrier of (REAL-NS 1) ;
PG * DFG is Function of the carrier of (REAL-NS m),the carrier of (REAL-NS 1)
;
then reconsider L = (Proj i,n) * (diff g,x0) as Function of (REAL-NS m),(REAL-NS 1) ;
AD1:
for x, y being VECTOR of (REAL-NS m) holds L . (x + y) = (L . x) + (L . y)
for x being VECTOR of (REAL-NS m)
for r being Real holds L . (r * x) = r * (L . x)
then reconsider L = L as LinearOperator of (REAL-NS m),(REAL-NS 1) by AD1, GRCAT_1:def 13, LOPBAN_1:def 6;
reconsider L = L as Point of (R_NormSpace_of_BoundedLinearOperators (REAL-NS m),(REAL-NS 1)) by LOPBAN_1:def 10;
A01:
GR is total
by NDIFF_1:def 5;
then reconsider FGR = GR as Function of the carrier of (REAL-NS m),the carrier of (REAL-NS n) ;
A3:
(Proj i,n) * FGR is Function of the carrier of (REAL-NS m),the carrier of (REAL-NS 1)
;
(Proj i,n) * GR is REST of (REAL-NS m),(REAL-NS 1)
proof
B21:
dom GR = the
carrier of
(REAL-NS m)
by A01, PARTFUN1:def 4;
reconsider R =
(Proj i,n) * GR as
PartFunc of
(REAL-NS m),
(REAL-NS 1) ;
for
r being
Real st
r > 0 holds
ex
d being
Real st
(
d > 0 & ( for
z being
Point of
(REAL-NS m) st
z <> 0. (REAL-NS m) &
||.z.|| < d holds
(||.z.|| " ) * ||.(R /. z).|| < r ) )
proof
let r be
Real;
( r > 0 implies ex d being Real st
( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| " ) * ||.(R /. z).|| < r ) ) )
assume
r > 0
;
ex d being Real st
( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| " ) * ||.(R /. z).|| < r ) )
then consider d being
Real such that B5:
(
d > 0 & ( for
z being
Point of
(REAL-NS m) st
z <> 0. (REAL-NS m) &
||.z.|| < d holds
(||.z.|| " ) * ||.(GR /. z).|| < r ) )
by A01, NDIFF_1:26;
take
d
;
( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| " ) * ||.(R /. z).|| < r ) )
thus
d > 0
by B5;
for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| " ) * ||.(R /. z).|| < r
let z be
Point of
(REAL-NS m);
( z <> 0. (REAL-NS m) & ||.z.|| < d implies (||.z.|| " ) * ||.(R /. z).|| < r )
assume B6:
(
z <> 0. (REAL-NS m) &
||.z.|| < d )
;
(||.z.|| " ) * ||.(R /. z).|| < r
Q12:
GR /. z = GR . z
by B21, PARTFUN1:def 8;
Q121:
i in Seg n
by AS0;
reconsider GRz =
GR /. z as
Point of
(REAL-NS n) ;
reconsider GRz1 =
GRz as
Element of
REAL n by REAL_NS1:def 4;
reconsider GRzi =
GRz1 . i as
Element of
REAL ;
dom (Proj i,n) = the
carrier of
(REAL-NS n)
by PARTFUN1:def 4;
then Q123:
z in dom ((Proj i,n) * GR)
by B21, Q12, FUNCT_1:21;
then ((Proj i,n) * GR) . z =
(Proj i,n) . (GR . z)
by FUNCT_1:22
.=
<*((proj i,n) . GRz1)*>
by Q12, PDIFF_1:def 4
;
then Q13:
((Proj i,n) * GR) . z = <*GRzi*>
by PDIFF_1:def 1;
Q15:
abs GRzi <= ||.(GR /. z).||
by Q121, REAL_NS1:9;
Q151:
0 <= ||.z.||
by NORMSP_1:8;
0 <= abs GRzi
by COMPLEX1:132;
then Q16:
(||.z.|| " ) * (abs GRzi) <= (||.z.|| " ) * ||.(GR /. z).||
by Q15, Q151, XREAL_1:68;
(||.z.|| " ) * ||.(GR /. z).|| < r
by B5, B6;
then B71:
(||.z.|| " ) * (abs GRzi) < r
by Q16, XXREAL_0:2;
((Proj i,n) * GR) . z in rng ((Proj i,n) * GR)
by Q123, FUNCT_1:12;
then reconsider Rz =
((Proj i,n) * GR) . z as
VECTOR of
(REAL-NS 1) ;
set VGRzi =
<*GRzi*>;
<*GRzi*> is
Element of
REAL 1
by FINSEQ_2:118;
then
||.Rz.|| = |.<*GRzi*>.|
by Q13, REAL_NS1:1;
then
(||.z.|| " ) * ||.Rz.|| < r
by B71, JORDAN2C:12;
hence
(||.z.|| " ) * ||.(R /. z).|| < r
by Q123, PARTFUN1:def 8;
verum
end;
hence
(Proj i,n) * GR is
REST of
(REAL-NS m),
(REAL-NS 1)
by A3, NDIFF_1:26;
verum
end;
then reconsider R = (Proj i,n) * GR as REST of (REAL-NS m),(REAL-NS 1) ;
set pg = (Proj i,n) * g;
E1:
dom (Proj i,n) = the carrier of (REAL-NS n)
by FUNCT_2:def 1;
then
rng g c= dom (Proj i,n)
;
then E3:
dom g = dom ((Proj i,n) * g)
by RELAT_1:46;
E4:
dom (Proj i,n) = REAL n
by E1, REAL_NS1:def 4;
A5:
for x being Point of (REAL-NS m) st x in N holds
(((Proj i,n) * g) /. x) - (((Proj i,n) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be
Point of
(REAL-NS m);
( x in N implies (((Proj i,n) * g) /. x) - (((Proj i,n) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
now assume C1:
x in N
;
( x in N implies (((Proj i,n) * g) /. x) - (((Proj i,n) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )then C2:
(g /. x) - (g /. x0) = ((diff g,x0) . (x - x0)) + (GR /. (x - x0))
by AS2;
C3:
x0 in N
by NFCONT_1:4;
then C31:
(
((Proj i,n) * g) /. x = ((Proj i,n) * g) . x &
((Proj i,n) * g) /. x0 = ((Proj i,n) * g) . x0 )
by AS1, E3, C1, PARTFUN1:def 8;
C33:
(
g /. x = g . x &
g /. x0 = g . x0 )
by AS1, C1, C3, PARTFUN1:def 8;
reconsider PGSx =
(((Proj i,n) * g) /. x) - (((Proj i,n) * g) /. x0) as
Element of
REAL 1
by REAL_NS1:def 4;
((Proj i,n) * g) . x in rng ((Proj i,n) * g)
by AS1, E3, C1, FUNCT_1:12;
then reconsider PGdx =
((Proj i,n) * g) . x as
Element of
REAL 1
by REAL_NS1:def 4;
((Proj i,n) * g) . x0 in rng ((Proj i,n) * g)
by AS1, E3, C3, FUNCT_1:12;
then reconsider PGdx0 =
((Proj i,n) * g) . x0 as
Element of
REAL 1
by REAL_NS1:def 4;
g . x in rng g
by AS1, C1, FUNCT_1:12;
then reconsider Gx =
g . x as
Element of
REAL n by REAL_NS1:def 4;
g . x0 in rng g
by AS1, C3, FUNCT_1:12;
then reconsider Gx0 =
g . x0 as
Element of
REAL n by REAL_NS1:def 4;
set ProjGx =
(Proj i,n) . (g . x);
Gx in dom (Proj i,n)
by E4;
then
(Proj i,n) . (g . x) in rng (Proj i,n)
by FUNCT_1:12;
then reconsider ProjGx =
(Proj i,n) . (g . x) as
Element of
REAL 1
by REAL_NS1:def 4;
set ProjGx0 =
(Proj i,n) . (g . x0);
Gx0 in dom (Proj i,n)
by E4;
then
(Proj i,n) . (g . x0) in rng (Proj i,n)
by FUNCT_1:12;
then reconsider ProjGx0 =
(Proj i,n) . (g . x0) as
Element of
REAL 1
by REAL_NS1:def 4;
reconsider Gx1 =
Gx as
Element of
(REAL-NS n) by REAL_NS1:def 4;
reconsider Gx01 =
Gx0 as
Element of
(REAL-NS n) by REAL_NS1:def 4;
reconsider Gsx =
g /. x as
Element of
REAL n by REAL_NS1:def 4;
reconsider Gsx0 =
g /. x0 as
Element of
REAL n by REAL_NS1:def 4;
set dxx0 =
x - x0;
reconsider Ldxx0 =
L . (x - x0) as
Element of
(REAL-NS 1) ;
F4:
dom R = the
carrier of
(REAL-NS m)
by A3, PARTFUN1:def 4;
then F5:
R /. (x - x0) = R . (x - x0)
by PARTFUN1:def 8;
then reconsider Rdxx0 =
R . (x - x0) as
Element of
(REAL-NS 1) ;
reconsider Lxx0Rxx0 =
(L . (x - x0)) + (R /. (x - x0)) as
Element of
REAL 1
by REAL_NS1:def 4;
reconsider Ldiff =
(diff g,x0) . (x - x0) as
Element of
REAL n by REAL_NS1:def 4;
set ProjLdiff =
(Proj i,n) . Ldiff;
(Proj i,n) . Ldiff in rng (Proj i,n)
by E1, FUNCT_1:12;
then reconsider ProjLdiff =
(Proj i,n) . Ldiff as
Element of
REAL 1
by REAL_NS1:def 4;
F6:
dom GR = the
carrier of
(REAL-NS m)
by A01, PARTFUN1:def 4;
then
GR . (x - x0) in rng GR
by FUNCT_1:12;
then reconsider Rdiff =
GR . (x - x0) as
Element of
REAL n by REAL_NS1:def 4;
F82:
Rdiff = GR /. (x - x0)
by F6, PARTFUN1:def 8;
set ProjRdiff =
(Proj i,n) . Rdiff;
(Proj i,n) . Rdiff in rng (Proj i,n)
by E4, FUNCT_1:12;
then reconsider ProjRdiff =
(Proj i,n) . Rdiff as
Element of
REAL 1
by REAL_NS1:def 4;
dom L = the
carrier of
(REAL-NS m)
by FUNCT_2:def 1;
then
(
L . (x - x0) = (Proj i,n) . Ldiff &
R . (x - x0) = (Proj i,n) . Rdiff )
by F4, FUNCT_1:22;
then Lm1:
Ldxx0 + Rdxx0 = ProjLdiff + ProjRdiff
by REAL_NS1:2;
(Proj i,n) . Ldiff = <*((proj i,n) . Ldiff)*>
by PDIFF_1:def 4;
then Lm2:
(Proj i,n) . Ldiff = <*(Ldiff . i)*>
by PDIFF_1:def 1;
Rdiff in dom (Proj i,n)
by E4;
then
(Proj i,n) . Rdiff = <*((proj i,n) . Rdiff)*>
by PDIFF_1:def 4;
then Lm3:
(Proj i,n) . Rdiff = <*(Rdiff . i)*>
by PDIFF_1:def 1;
reconsider diffGR =
((diff g,x0) . (x - x0)) + (GR /. (x - x0)) as
Element of
REAL n by REAL_NS1:def 4;
reconsider Rsdiff =
GR /. (x - x0) as
Element of
REAL n by REAL_NS1:def 4;
PGSx =
PGdx - PGdx0
by C31, REAL_NS1:5
.=
ProjGx - PGdx0
by AS1, E3, C1, FUNCT_1:22
.=
ProjGx - ProjGx0
by AS1, E3, C3, FUNCT_1:22
.=
<*((proj i,n) . Gx1)*> - ProjGx0
by PDIFF_1:def 4
.=
<*((proj i,n) . Gx1)*> - <*((proj i,n) . Gx01)*>
by PDIFF_1:def 4
.=
<*(Gx . i)*> - <*((proj i,n) . Gx01)*>
by PDIFF_1:def 1
.=
<*(Gx . i)*> - <*(Gx0 . i)*>
by PDIFF_1:def 1
.=
<*((Gx . i) - (Gx0 . i))*>
by RVSUM_1:50
.=
<*((Gsx - Gsx0) . i)*>
by C33, RVSUM_1:48
.=
<*(diffGR . i)*>
by C2, REAL_NS1:5
.=
<*((Ldiff + Rsdiff) . i)*>
by REAL_NS1:2
.=
<*((Ldiff . i) + (Rsdiff . i))*>
by RVSUM_1:27
;
hence
(
x in N implies
(((Proj i,n) * g) /. x) - (((Proj i,n) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
by F5, Lm1, Lm2, Lm3, F82, RVSUM_1:29;
verum end;
hence
(
x in N implies
(((Proj i,n) * g) /. x) - (((Proj i,n) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
;
verum
end;
hence
(Proj i,n) * g is_differentiable_in x0
by AS1, E3, NDIFF_1:def 6; (Proj i,n) * (diff g,x0) = diff ((Proj i,n) * g),x0
hence
(Proj i,n) * (diff g,x0) = diff ((Proj i,n) * g),x0
by AS1, E3, A5, NDIFF_1:def 7; verum