let i be Element of NAT ; for n being non zero Element of NAT
for g being PartFunc of REAL,(REAL-NS n)
for x0 being Real 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 n be non zero Element of NAT ; for g being PartFunc of REAL,(REAL-NS n)
for x0 being Real 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 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; ( 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 GR being RestFunc of (REAL-NS n), DFG being LinearFunc 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;
reconsider PG = Proj (i,n) as Function of (REAL-NS n),(REAL-NS 1) ;
reconsider L = (Proj (i,n)) * DFG as Function of REAL,(REAL-NS 1) ;
A5:
for r being Real holds L /. r = r * ((Proj (i,n)) . LP)
then reconsider L = L as LinearFunc of (REAL-NS 1) by NDIFF_3:def 2;
A7:
GR is total
by NDIFF_3:def 1;
then reconsider FGR = GR as Function of REAL,(REAL-NS n) ;
A8:
(Proj (i,n)) * FGR is Function of REAL,(REAL-NS 1)
;
(Proj (i,n)) * GR is RestFunc of (REAL-NS 1)
proof
A9:
dom GR = REAL
by A7, PARTFUN1:def 2;
reconsider R =
(Proj (i,n)) * GR as
PartFunc of
REAL,
(REAL-NS 1) ;
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 A10:
(
d > 0 & ( for
z being
Real st
z <> 0 &
|.z.| < d holds
(|.z.| ") * ||.(GR /. z).|| < r ) )
by A7, Th23;
take
d
;
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < r ) )
thus
d > 0
by A10;
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 A11:
(
z <> 0 &
|.z.| < d )
;
(|.z.| ") * ||.(R /. z).|| < r
reconsider z =
z as
Element of
REAL by XREAL_0:def 1;
A12:
GR /. z = GR . z
by A9, PARTFUN1:def 6;
A13:
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 A14:
z in dom ((Proj (i,n)) * GR)
by A9, A12, FUNCT_1:11;
then ((Proj (i,n)) * GR) . z =
(Proj (i,n)) . (GR . z)
by FUNCT_1:12
.=
<*((proj (i,n)) . GRz1)*>
by A12, PDIFF_1:def 4
;
then A15:
((Proj (i,n)) * GR) . z = <*GRzi*>
by PDIFF_1:def 1;
A16:
|.GRzi.| <= ||.(GR /. z).||
by A13, REAL_NS1:9;
A17:
0 <= |.z.|
by COMPLEX1:46;
0 <= |.GRzi.|
by COMPLEX1:46;
then A18:
(|.z.| ") * |.GRzi.| <= (|.z.| ") * ||.(GR /. z).||
by A16, A17, XREAL_1:66;
(|.z.| ") * ||.(GR /. z).|| < r
by A10, A11;
then A19:
(|.z.| ") * |.GRzi.| < r
by A18, XXREAL_0:2;
((Proj (i,n)) * GR) . z in rng ((Proj (i,n)) * GR)
by A14, 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 A15, REAL_NS1:1;
then
(|.z.| ") * ||.Rz.|| < r
by A19, JORDAN2C:10;
hence
(|.z.| ") * ||.(R /. z).|| < r
by A14, PARTFUN1:def 6;
verum
end;
hence
(Proj (i,n)) * GR is
RestFunc of
(REAL-NS 1)
by A8, Th23;
verum
end;
then reconsider R = (Proj (i,n)) * GR as RestFunc of (REAL-NS 1) ;
set pg = (Proj (i,n)) * g;
A20:
dom (Proj (i,n)) = the carrier of (REAL-NS n)
by FUNCT_2:def 1;
then
rng g c= dom (Proj (i,n))
;
then A21:
dom g = dom ((Proj (i,n)) * g)
by RELAT_1:27;
A22:
dom (Proj (i,n)) = REAL n
by A20, REAL_NS1:def 4;
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)) )
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 /. (x - x0)) + (GR /. (x - x0))
by A3;
A26:
x0 in N
by RCOMP_1:16;
then A27:
(
((Proj (i,n)) * g) /. x = ((Proj (i,n)) * g) . x &
((Proj (i,n)) * g) /. x0 = ((Proj (i,n)) * g) . x0 )
by A2, A21, A24, PARTFUN1:def 6;
A28:
(
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 1
by REAL_NS1:def 4;
((Proj (i,n)) * g) . x in rng ((Proj (i,n)) * g)
by A2, A21, A24, 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, A21, A26, 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, 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);
Gx in dom (Proj (i,n))
by A22;
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 A22;
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;
reconsider dxx0 =
x - x0 as
Element of
REAL by XREAL_0:def 1;
reconsider Ldxx0 =
L /. (x - x0) as
Element of
(REAL-NS 1) ;
A29:
dom R = REAL
by A8, PARTFUN1:def 2;
then A30:
R /. (x - x0) = R . dxx0
by PARTFUN1:def 6;
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 =
DFG /. (x - x0) as
Element of
REAL n by REAL_NS1:def 4;
dom DFG = REAL
by FUNCT_2:def 1;
then A31:
Ldiff = DFG . dxx0
by PARTFUN1:def 6;
set ProjLdiff =
(Proj (i,n)) . Ldiff;
(Proj (i,n)) . Ldiff in rng (Proj (i,n))
by A20, FUNCT_1:3;
then reconsider ProjLdiff =
(Proj (i,n)) . Ldiff as
Element of
REAL 1
by REAL_NS1:def 4;
A32:
dom GR = REAL
by A7, 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;
A33:
Rdiff = GR /. dxx0
by A32, PARTFUN1:def 6;
set ProjRdiff =
(Proj (i,n)) . Rdiff;
(Proj (i,n)) . Rdiff in rng (Proj (i,n))
by A22, FUNCT_1:3;
then reconsider ProjRdiff =
(Proj (i,n)) . Rdiff as
Element of
REAL 1
by REAL_NS1:def 4;
dom L = REAL
by FUNCT_2:def 1;
then A34:
dxx0 in dom L
;
A35:
L /. dxx0 =
L . dxx0
.=
(Proj (i,n)) . (DFG . dxx0)
by A34, FUNCT_1:12
.=
(Proj (i,n)) . Ldiff
by A31
;
R . (x - x0) = (Proj (i,n)) . Rdiff
by A29, FUNCT_1:12;
then A36:
Ldxx0 + Rdxx0 = ProjLdiff + ProjRdiff
by A35, REAL_NS1:2;
(Proj (i,n)) . Ldiff = <*((proj (i,n)) . Ldiff)*>
by PDIFF_1:def 4;
then A37:
(Proj (i,n)) . Ldiff = <*(Ldiff . i)*>
by PDIFF_1:def 1;
Rdiff in dom (Proj (i,n))
by A22;
then
(Proj (i,n)) . Rdiff = <*((proj (i,n)) . Rdiff)*>
by PDIFF_1:def 4;
then A38:
(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 =
PGdx - PGdx0
by A27, REAL_NS1:5
.=
ProjGx - PGdx0
by A2, A21, A24, FUNCT_1:12
.=
ProjGx - ProjGx0
by A2, A21, A26, 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 A28, 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 A30, A36, A37, A38, 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 A39:
(Proj (i,n)) * g is_differentiable_in x0
by A2, A21, NDIFF_3:def 3; (Proj (i,n)) . (diff (g,x0)) = diff (((Proj (i,n)) * g),x0)
L /. jj =
1 * ((Proj (i,n)) . LP)
by A5
.=
(Proj (i,n)) . LP
by RLVECT_1:def 8
.=
(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 A39, A2, A21, A23, NDIFF_3:def 4; verum