let n be non zero Element of NAT ; for g being PartFunc of REAL,(REAL-NS n)
for x0 being Real
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,(REAL-NS n); for x0 being Real
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 Real; 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 DFG being LinearFunc of (REAL-NS n) ex GR being RestFunc of (REAL-NS n) st
( diff (g,x0) = DFG /. 1 & ( for x being Real st x in N holds
(g /. x) - (g /. x0) = (DFG /. (x - x0)) + (GR /. (x - x0)) ) ) )
by NDIFF_3:def 4;
consider DFG being LinearFunc of (REAL-NS n), GR being RestFunc of (REAL-NS n) such that
A3:
( diff (g,x0) = DFG /. 1 & ( for x being Real st x in N holds
(g /. x) - (g /. x0) = (DFG /. (x - x0)) + (GR /. (x - x0)) ) )
by A2;
consider LP being Point of (REAL-NS n) such that
A4:
for p being Real holds DFG /. p = p * LP
by NDIFF_3:def 2;
A5:
the carrier of (REAL-NS n) = REAL n
by REAL_NS1:def 4;
then reconsider PG = proj (i,n) as Function of (REAL-NS n),REAL ;
the carrier of (REAL-NS n) = REAL n
by REAL_NS1:def 4;
then reconsider L = (proj (i,n)) * DFG as Function of REAL,REAL ;
A6:
for r being Real holds L . r = ((proj (i,n)) . LP) * r
reconsider L = L as LinearFunc by A6, FDIFF_1:def 3;
A8:
GR is total
by NDIFF_3:def 1;
then reconsider FGR = GR as Function of REAL,(REAL-NS n) ;
A9:
(proj (i,n)) * FGR is Function of REAL,REAL
by A5;
(proj (i,n)) * GR is RestFunc
proof
A10:
dom GR = REAL
by A8, PARTFUN1:def 2;
reconsider R =
(proj (i,n)) * GR as
PartFunc of
REAL,
REAL ;
for
r being
Real st
r > 0 holds
ex
d being
Real st
(
d > 0 & ( for
z being
Real st
z <> 0 &
|.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 Real st z <> 0 & |.z.| < d holds
(|.z.| ") * |.(R /. z).| < r ) ) )
assume
r > 0
;
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * |.(R /. z).| < r ) )
then consider d being
Real such that A11:
(
d > 0 & ( for
z being
Real st
z <> 0 &
|.z.| < d holds
(|.z.| ") * ||.(GR /. z).|| < r ) )
by A8, NDIFF_4:23;
take
d
;
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * |.(R /. z).| < r ) )
thus
d > 0
by A11;
for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * |.(R /. z).| < r
let z be
Real;
( z <> 0 & |.z.| < d implies (|.z.| ") * |.(R /. z).| < r )
assume A12:
(
z <> 0 &
|.z.| < d )
;
(|.z.| ") * |.(R /. z).| < r
A13:
z in REAL
by XREAL_0:def 1;
A14:
GR /. z = GR . z
by A10, PARTFUN1:def 6, XREAL_0:def 1;
A15:
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
Real ;
the
carrier of
(REAL-NS n) = REAL n
by REAL_NS1:def 4;
then
dom (proj (i,n)) = the
carrier of
(REAL-NS n)
by PARTFUN1:def 2;
then A16:
z in dom ((proj (i,n)) * GR)
by A10, A14, FUNCT_1:11, A13;
then A17:
((proj (i,n)) * GR) . z =
(proj (i,n)) . (GR . z)
by FUNCT_1:12
.=
(proj (i,n)) . GRz1
by A10, A13, PARTFUN1:def 6
;
A18:
|.GRzi.| <= ||.(GR /. z).||
by A15, REAL_NS1:9;
A19:
0 <= |.z.|
by COMPLEX1:46;
0 <= |.GRzi.|
by COMPLEX1:46;
then A20:
(|.z.| ") * |.GRzi.| <= (|.z.| ") * ||.(GR /. z).||
by A18, A19, XREAL_1:66;
(|.z.| ") * ||.(GR /. z).|| < r
by A11, A12;
then A21:
(|.z.| ") * |.GRzi.| < r
by A20, XXREAL_0:2;
reconsider Rz =
((proj (i,n)) * GR) . z as
Element of
REAL by XREAL_0:def 1;
(|.z.| ") * |.Rz.| < r
by A21, PDIFF_1:def 1, A17;
hence
(|.z.| ") * |.(R /. z).| < r
by A16, PARTFUN1:def 6;
verum
end;
hence
(proj (i,n)) * GR is
RestFunc
by A9, Th35;
verum
end;
then reconsider R = (proj (i,n)) * GR as RestFunc ;
set pg = (proj (i,n)) * g;
the carrier of (REAL-NS n) = REAL n
by REAL_NS1:def 4;
then
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:
for x being Real 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
Real;
( x in N implies (((proj (i,n)) * g) . x) - (((proj (i,n)) * g) . x0) = (L . (x - x0)) + (R . (x - x0)) )
reconsider xx =
x as
Element of
REAL by XREAL_0:def 1;
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 A24:
x in N
;
( x in N implies (((proj (i,n)) * g) . x) - (((proj (i,n)) * g) . x0) = (L . (x - x0)) + (R . (x - x0)) )then A25:
(g /. x) - (g /. x0) = (DFG /. (xx - x0)) + (GR /. (xx - x0))
by A3;
A26:
x0 in N
by RCOMP_1:16;
A27:
(
g /. x = g . x &
g /. x0 = g . x0 )
by A2, A24, A26, PARTFUN1:def 6;
reconsider PGSx =
(((proj (i,n)) * g) . x) - (((proj (i,n)) * g) . x0) as
Element of
REAL by XREAL_0:def 1;
reconsider PGdx =
((proj (i,n)) * g) . x as
Element of
REAL by XREAL_0:def 1;
reconsider PGdx0 =
((proj (i,n)) * g) . x0 as
Element of
REAL by XREAL_0:def 1;
g . x in rng g
by A2, A24, 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, A26, 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);
reconsider projGx =
(proj (i,n)) . (g . x) as
Element of
REAL by XREAL_0:def 1;
set projGx0 =
(proj (i,n)) . (g . x0);
reconsider projGx0 =
(proj (i,n)) . (g . x0) as
Element of
REAL by XREAL_0:def 1;
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;
reconsider dxx0 =
x - x0 as
Element of
REAL by XREAL_0:def 1;
reconsider Ldxx0 =
L . (x - x0) as
Element of
REAL by XREAL_0:def 1;
A28:
dom R = REAL
by A9, PARTFUN1:def 2;
reconsider Rdxx0 =
R . (x - x0) as
Element of
REAL by XREAL_0:def 1;
reconsider Lxx0Rxx0 =
(L . (x - x0)) + (R . (x - x0)) as
Element of
REAL by XREAL_0:def 1;
reconsider Ldiff =
DFG /. (x - x0) as
Element of
REAL n by REAL_NS1:def 4;
set projLdiff =
(proj (i,n)) . Ldiff;
reconsider projLdiff =
(proj (i,n)) . Ldiff as
Element of
REAL ;
A29:
dom GR = REAL
by A8, PARTFUN1:def 2;
then
GR . dxx0 in rng GR
by FUNCT_1:3;
then reconsider Rdiff =
GR . dxx0 as
Element of
REAL n by REAL_NS1:def 4;
set projRdiff =
(proj (i,n)) . Rdiff;
reconsider projRdiff =
(proj (i,n)) . Rdiff as
Element of
REAL ;
dom DFG = REAL
by FUNCT_2:def 1;
then A30:
Ldiff = DFG . (x - x0)
by PARTFUN1:def 6, XREAL_0:def 1;
dom L = REAL
by FUNCT_2:def 1;
then A31:
L . (x - x0) = (proj (i,n)) . Ldiff
by FUNCT_1:12, XREAL_0:def 1, A30;
A32:
R . (x - x0) = (proj (i,n)) . Rdiff
by A28, FUNCT_1:12;
A33:
(proj (i,n)) . Ldiff = Ldiff . i
by PDIFF_1:def 1;
A34:
(proj (i,n)) . Rdiff = Rdiff . i
by PDIFF_1:def 1;
reconsider diffGR =
(DFG /. (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 =
projGx - PGdx0
by A2, A22, A24, FUNCT_1:12
.=
((proj (i,n)) . Gx1) - ((proj (i,n)) . Gx01)
by A2, A22, A26, FUNCT_1:12
.=
(Gx . i) - ((proj (i,n)) . Gx01)
by PDIFF_1:def 1
.=
(Gx . i) - (Gx0 . i)
by PDIFF_1:def 1
.=
(Gsx - Gsx0) . i
by A27, RVSUM_1:27
.=
diffGR . i
by A25, 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, A33, A34, A29, PARTFUN1:def 6, A32;
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 A35:
(proj (i,n)) * g is_differentiable_in x0
by A2, A22; (proj (i,n)) . (diff (g,x0)) = diff (((proj (i,n)) * g),x0)
L . 1 =
1 * ((proj (i,n)) . LP)
by A6
.=
(proj (i,n)) . (1 * LP)
by RLVECT_1:def 8
.=
(proj (i,n)) . (diff (g,x0))
by A3, A4
;
hence
(proj (i,n)) . (diff (g,x0)) = diff (((proj (i,n)) * g),x0)
by A35, A2, A22, A23, FDIFF_1:def 5; verum