let m, n be non zero Nat; for g being PartFunc of (REAL-NS m),(REAL-NS n)
for x0 being Point of (REAL-NS m)
for i being 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 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 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 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 A1:
( 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
A2:
( N c= dom g & ex GR being RestFunc 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 RestFunc of (REAL-NS m),(REAL-NS n) such that
A3:
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 A2;
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 9;
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) ;
A4:
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 A4, LOPBAN_1:def 5, VECTSP_1:def 20;
reconsider L = L as Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) by LOPBAN_1:def 9;
A8:
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) ;
A9:
(Proj (i,n)) * FGR is Function of the carrier of (REAL-NS m), the carrier of (REAL-NS 1)
;
(Proj (i,n)) * GR is RestFunc of (REAL-NS m),(REAL-NS 1)
proof
A10:
dom GR = the
carrier of
(REAL-NS m)
by A8, PARTFUN1:def 2;
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 A11:
(
d > 0 & ( for
z being
Point of
(REAL-NS m) st
z <> 0. (REAL-NS m) &
||.z.|| < d holds
(||.z.|| ") * ||.(GR /. z).|| < r ) )
by A8, NDIFF_1:23;
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 A11;
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 A12:
(
z <> 0. (REAL-NS m) &
||.z.|| < d )
;
(||.z.|| ") * ||.(R /. z).|| < r
A13:
GR /. z = GR . z
by A10, PARTFUN1:def 6;
A14:
i in Seg n
by A1;
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 by XREAL_0:def 1;
dom (Proj (i,n)) = the
carrier of
(REAL-NS n)
by PARTFUN1:def 2;
then A15:
z in dom ((Proj (i,n)) * GR)
by A10, A13, FUNCT_1:11;
then ((Proj (i,n)) * GR) . z =
(Proj (i,n)) . (GR . z)
by FUNCT_1:12
.=
<*((proj (i,n)) . GRz1)*>
by A13, PDIFF_1:def 4
;
then A16:
((Proj (i,n)) * GR) . z = <*GRzi*>
by PDIFF_1:def 1;
A17:
|.GRzi.| <= ||.(GR /. z).||
by A14, REAL_NS1:9;
A18:
0 <= ||.z.||
by NORMSP_1:4;
0 <= |.GRzi.|
by COMPLEX1:46;
then A19:
(||.z.|| ") * |.GRzi.| <= (||.z.|| ") * ||.(GR /. z).||
by A17, A18, XREAL_1:66;
(||.z.|| ") * ||.(GR /. z).|| < r
by A11, A12;
then A20:
(||.z.|| ") * |.GRzi.| < r
by A19, XXREAL_0:2;
((Proj (i,n)) * GR) . z in rng ((Proj (i,n)) * GR)
by A15, FUNCT_1:3;
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:98;
then
||.Rz.|| = |.<*GRzi*>.|
by A16, REAL_NS1:1;
then
(||.z.|| ") * ||.Rz.|| < r
by A20, JORDAN2C:10;
hence
(||.z.|| ") * ||.(R /. z).|| < r
by A15, PARTFUN1:def 6;
verum
end;
hence
(Proj (i,n)) * GR is
RestFunc of
(REAL-NS m),
(REAL-NS 1)
by A9, NDIFF_1:23;
verum
end;
then reconsider R = (Proj (i,n)) * GR as RestFunc of (REAL-NS m),(REAL-NS 1) ;
set pg = (Proj (i,n)) * g;
A21:
dom (Proj (i,n)) = the carrier of (REAL-NS n)
by FUNCT_2:def 1;
then
rng g c= dom (Proj (i,n))
;
then A22:
dom g = dom ((Proj (i,n)) * g)
by RELAT_1:27;
A23:
dom (Proj (i,n)) = REAL n
by A21, REAL_NS1:def 4;
A24:
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 ( x in N & x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )assume A25:
x in N
;
( x in N implies (((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )then A26:
(g /. x) - (g /. x0) = ((diff (g,x0)) . (x - x0)) + (GR /. (x - x0))
by A3;
A27:
x0 in N
by NFCONT_1:4;
then A28:
(
((Proj (i,n)) * g) /. x = ((Proj (i,n)) * g) . x &
((Proj (i,n)) * g) /. x0 = ((Proj (i,n)) * g) . x0 )
by A2, A22, A25, PARTFUN1:def 6;
A29:
(
g /. x = g . x &
g /. x0 = g . x0 )
by A2, A25, A27, PARTFUN1:def 6;
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 A2, A22, A25, FUNCT_1:3;
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 A2, A22, A27, FUNCT_1:3;
then reconsider PGdx0 =
((Proj (i,n)) * g) . x0 as
Element of
REAL 1
by REAL_NS1:def 4;
g . x in rng g
by A2, A25, FUNCT_1:3;
then reconsider Gx =
g . x as
Element of
REAL n by REAL_NS1:def 4;
g . x0 in rng g
by A2, A27, FUNCT_1:3;
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 A23;
then
(Proj (i,n)) . (g . x) in rng (Proj (i,n))
by FUNCT_1:3;
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 A23;
then
(Proj (i,n)) . (g . x0) in rng (Proj (i,n))
by FUNCT_1:3;
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) ;
A30:
dom R = the
carrier of
(REAL-NS m)
by A9, PARTFUN1:def 2;
then A31:
R /. (x - x0) = R . (x - x0)
by PARTFUN1:def 6;
then reconsider Rdxx0 =
R . (x - x0) as
Element of
(REAL-NS 1) ;
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 A21, FUNCT_1:3;
then reconsider ProjLdiff =
(Proj (i,n)) . Ldiff as
Element of
REAL 1
by REAL_NS1:def 4;
A32:
dom GR = the
carrier of
(REAL-NS m)
by A8, PARTFUN1:def 2;
then
GR . (x - x0) in rng GR
by FUNCT_1:3;
then reconsider Rdiff =
GR . (x - x0) as
Element of
REAL n by REAL_NS1:def 4;
A33:
Rdiff = GR /. (x - x0)
by A32, PARTFUN1:def 6;
set ProjRdiff =
(Proj (i,n)) . Rdiff;
(Proj (i,n)) . Rdiff in rng (Proj (i,n))
by A23, FUNCT_1:3;
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 A30, FUNCT_1:12;
then A34:
Ldxx0 + Rdxx0 = ProjLdiff + ProjRdiff
by REAL_NS1:2;
(Proj (i,n)) . Ldiff = <*((proj (i,n)) . Ldiff)*>
by PDIFF_1:def 4;
then A35:
(Proj (i,n)) . Ldiff = <*(Ldiff . i)*>
by PDIFF_1:def 1;
Rdiff in dom (Proj (i,n))
by A23;
then
(Proj (i,n)) . Rdiff = <*((proj (i,n)) . Rdiff)*>
by PDIFF_1:def 4;
then A36:
(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 A28, REAL_NS1:5
.=
ProjGx - PGdx0
by A2, A22, A25, FUNCT_1:12
.=
ProjGx - ProjGx0
by A2, A22, A27, FUNCT_1:12
.=
<*((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:29
.=
<*((Gsx - Gsx0) . i)*>
by A29, RVSUM_1:27
.=
<*(diffGR . i)*>
by A26, REAL_NS1:5
.=
<*((Ldiff + Rsdiff) . i)*>
by REAL_NS1:2
.=
<*((Ldiff . i) + (Rsdiff . i))*>
by RVSUM_1:11
;
hence
(
x in N implies
(((Proj (i,n)) * g) /. x) - (((Proj (i,n)) * g) /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
by A31, A34, A35, A36, A33, RVSUM_1:13;
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 A2, A22, 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 A2, A22, A24, NDIFF_1:def 7; verum