let f be PartFunc of (REAL-NS 1),(REAL-NS 1); for g being PartFunc of REAL,REAL
for x being Point of (REAL-NS 1)
for y being Real st f = <>* g & x = <*y*> & g is_differentiable_in y holds
( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )
let g be PartFunc of REAL,REAL; for x being Point of (REAL-NS 1)
for y being Real st f = <>* g & x = <*y*> & g is_differentiable_in y holds
( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )
let x be Point of (REAL-NS 1); for y being Real st f = <>* g & x = <*y*> & g is_differentiable_in y holds
( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )
let y be Real; ( f = <>* g & x = <*y*> & g is_differentiable_in y implies ( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> ) )
set J = proj (1,1);
assume that
A1:
f = <>* g
and
A2:
x = <*y*>
and
A3:
g is_differentiable_in y
; ( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )
reconsider x0 = y as Real ;
consider N0 being Neighbourhood of x0 such that
A4:
N0 c= dom g
and
A5:
ex L0 being LinearFunc ex R0 being RestFunc st
( diff (g,x0) = L0 . 1 & ( for y0 being Real st y0 in N0 holds
(g . y0) - (g . x0) = (L0 . (y0 - x0)) + (R0 . (y0 - x0)) ) )
by A3, FDIFF_1:def 5;
consider e0 being Real such that
A6:
0 < e0
and
A7:
N0 = ].(x0 - e0),(x0 + e0).[
by RCOMP_1:def 6;
reconsider e = e0 as Real ;
set N = { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ;
A8:
rng (g * (proj (1,1))) c= REAL
;
consider L0 being LinearFunc, R0 being RestFunc such that
A9:
diff (g,x0) = L0 . 1
and
A10:
for y0 being Real st y0 in N0 holds
(g . y0) - (g . x0) = (L0 . (y0 - x0)) + (R0 . (y0 - x0))
by A5;
reconsider R = (I * R0) * (proj (1,1)) as RestFunc of (REAL-NS 1),(REAL-NS 1) by Th6;
reconsider L = (I * L0) * (proj (1,1)) as Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) by Th6;
A11:
dom g c= REAL
;
dom f c= the carrier of (REAL-NS 1)
;
then A12:
dom f c= rng I
by Th2, REAL_NS1:def 4;
A13:
(proj (1,1)) * I = id REAL
by Lm1, FUNCT_1:39;
now for z being object holds
( ( z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } implies z in I .: N0 ) & ( z in I .: N0 implies z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ) )let z be
object ;
( ( z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } implies z in I .: N0 ) & ( z in I .: N0 implies z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } ) )hereby ( z in I .: N0 implies z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } )
assume
z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e }
;
z in I .: N0then consider w being
Point of
(REAL-NS 1) such that A14:
z = w
and A15:
||.(w - x).|| < e
;
reconsider y =
(proj (1,1)) . w as
Element of
REAL by XREAL_0:def 1;
(proj (1,1)) . x = x0
by A2, Lm1;
then
(proj (1,1)) . (w - x) = y - x0
by Th4;
then
|.(y - x0).| < e
by A15, Th4;
then A16:
y in N0
by A7, RCOMP_1:1;
w in the
carrier of
(REAL-NS 1)
;
then
w in dom (proj (1,1))
by Lm1, REAL_NS1:def 4;
then
w = I . y
by FUNCT_1:34;
hence
z in I .: N0
by A14, A16, FUNCT_2:35;
verum
end; assume
z in I .: N0
;
z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } then consider yy being
object such that A17:
yy in REAL
and A18:
yy in N0
and A19:
z = I . yy
by FUNCT_2:64;
reconsider y =
yy as
Element of
REAL by A17;
reconsider w =
I . y as
Point of
(REAL-NS 1) by REAL_NS1:def 4;
I . x0 = x
by A2, Lm1;
then A20:
w - x = I . (y - x0)
by Th3;
|.(y - x0).| < e
by A7, A18, RCOMP_1:1;
then
||.(w - x).|| < e
by A20, Th3;
hence
z in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e }
by A19;
verum end;
then A21:
{ z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } = I .: N0
by TARSKI:2;
(proj (1,1)) * f = (proj (1,1)) * (I * (g * (proj (1,1))))
by A1, RELAT_1:36;
then
(proj (1,1)) * f = (id REAL) * (g * (proj (1,1)))
by A13, RELAT_1:36;
then
((proj (1,1)) * f) * I = (g * (proj (1,1))) * I
by A8, RELAT_1:53;
then
((proj (1,1)) * f) * I = g * (id REAL)
by A13, RELAT_1:36;
then
g = ((proj (1,1)) * f) * I
by A11, RELAT_1:51;
then A22:
dom g = I " (dom ((proj (1,1)) * f))
by RELAT_1:147;
rng f c= the carrier of (REAL-NS 1)
;
then
rng f c= dom (proj (1,1))
by Lm1, REAL_NS1:def 4;
then
I .: (dom g) = I .: (I " (dom f))
by A22, RELAT_1:27;
then
I .: (dom g) = dom f
by A12, FUNCT_1:77;
then A23:
{ z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } c= dom f
by A4, A21, RELAT_1:123;
{ z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } c= the carrier of (REAL-NS 1)
then A24:
{ z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } is Neighbourhood of x
by A6, NFCONT_1:def 1;
(proj (1,1)) * I = id REAL
by Lm1, FUNCT_1:39;
then
((proj (1,1)) * I) .: N0 = N0
by FRECHET:13;
then A25:
(proj (1,1)) .: { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } = N0
by A21, RELAT_1:126;
A26:
for y being Point of (REAL-NS 1) st y in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } holds
(f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x))
proof
x in the
carrier of
(REAL-NS 1)
;
then
x in dom (proj (1,1))
by Lm1, REAL_NS1:def 4;
then A27:
I . (g . ((proj (1,1)) . x)) = I . ((g * (proj (1,1))) . x)
by FUNCT_1:13;
A28:
x in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e }
by A24, NFCONT_1:4;
then
x in dom f
by A23;
then
x in dom (I * (g * (proj (1,1))))
by A1, RELAT_1:36;
then
I . (g . ((proj (1,1)) . x)) = (I * (g * (proj (1,1)))) . x
by A27, FUNCT_1:12;
then
I . (g . ((proj (1,1)) . x)) = f . x
by A1, RELAT_1:36;
then A29:
I . (g . ((proj (1,1)) . x)) = f /. x
by A23, A28, PARTFUN1:def 6;
let y be
Point of
(REAL-NS 1);
( y in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e } implies (f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x)) )
assume A30:
y in { z where z is Point of (REAL-NS 1) : ||.(z - x).|| < e }
;
(f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x))
reconsider y0 =
(proj (1,1)) . y as
Element of
REAL by XREAL_0:def 1;
reconsider y0x0 =
y0 - x0 as
Element of
REAL by XREAL_0:def 1;
reconsider gy0 =
g . y0,
gx0 =
g . x0,
g0 =
g . 0 as
Element of
REAL by XREAL_0:def 1;
reconsider L0y0x0 =
L0 . y0x0 as
Element of
REAL by XREAL_0:def 1;
reconsider R0y0x0 =
R0 . y0x0,
Jyx =
(proj (1,1)) . (y - x) as
Element of
REAL by XREAL_0:def 1;
reconsider gJy =
g . ((proj (1,1)) . y),
gJx =
g . ((proj (1,1)) . x) as
Element of
REAL by XREAL_0:def 1;
reconsider R0Jyx =
R0 . Jyx,
L0Jyx =
L0 . Jyx as
Element of
REAL by XREAL_0:def 1;
reconsider p1 =
I . gy0,
p2 =
I . gx0,
q1 =
I . L0y0x0,
q2 =
I . R0y0x0 as
VECTOR of
(REAL-NS 1) by REAL_NS1:def 4;
A31:
(proj (1,1)) . x = x0
by A2, Lm1;
y in the
carrier of
(REAL-NS 1)
;
then
y in REAL 1
by REAL_NS1:def 4;
then
I . ((g . y0) - (g . x0)) = I . ((L0 . (y0 - x0)) + (R0 . (y0 - x0)))
by A10, A25, A30, FUNCT_2:35;
then
p1 - p2 = I . ((L0 . (y0 - x0)) + (R0 . (y0 - x0)))
by Th3;
then
p1 - p2 = q1 + q2
by Th3;
then
(I . gy0) - (I . gx0) = q1 + q2
by REAL_NS1:5;
then
(I . gJy) - (I . gJx) = (I . L0y0x0) + (I . R0y0x0)
by A31, REAL_NS1:2;
then
(I . gJy) - (I . gJx) = (I . L0Jyx) + (I . R0y0x0)
by A31, Th4;
then A32:
(I . gJy) - (I . gJx) = (I . L0Jyx) + (I . R0Jyx)
by A31, Th4;
dom L = the
carrier of
(REAL-NS 1)
by FUNCT_2:def 1;
then
y - x in dom ((I * L0) * (proj (1,1)))
;
then A33:
y - x in dom (I * (L0 * (proj (1,1))))
by RELAT_1:36;
y - x in the
carrier of
(REAL-NS 1)
;
then A34:
y - x in dom (proj (1,1))
by Lm1, REAL_NS1:def 4;
then A35:
I . (R0 . ((proj (1,1)) . (y - x))) = I . ((R0 * (proj (1,1))) . (y - x))
by FUNCT_1:13;
R is
total
by NDIFF_1:def 5;
then A36:
dom ((I * R0) * (proj (1,1))) = the
carrier of
(REAL-NS 1)
by PARTFUN1:def 2;
then
y - x in dom ((I * R0) * (proj (1,1)))
;
then
y - x in dom (I * (R0 * (proj (1,1))))
by RELAT_1:36;
then
I . (R0 . ((proj (1,1)) . (y - x))) = (I * (R0 * (proj (1,1)))) . (y - x)
by A35, FUNCT_1:12;
then
I . (R0 . ((proj (1,1)) . (y - x))) = ((I * R0) * (proj (1,1))) . (y - x)
by RELAT_1:36;
then A37:
I . (R0 . ((proj (1,1)) . (y - x))) = R /. (y - x)
by A36, PARTFUN1:def 6;
y in the
carrier of
(REAL-NS 1)
;
then
y in dom (proj (1,1))
by Lm1, REAL_NS1:def 4;
then A38:
I . (g . ((proj (1,1)) . y)) = I . ((g * (proj (1,1))) . y)
by FUNCT_1:13;
I . (L0 . ((proj (1,1)) . (y - x))) = I . ((L0 * (proj (1,1))) . (y - x))
by A34, FUNCT_1:13;
then
I . (L0 . ((proj (1,1)) . (y - x))) = (I * (L0 * (proj (1,1)))) . (y - x)
by A33, FUNCT_1:12;
then A39:
I . (L0 . ((proj (1,1)) . (y - x))) = L . (y - x)
by RELAT_1:36;
y in dom f
by A23, A30;
then
y in dom (I * (g * (proj (1,1))))
by A1, RELAT_1:36;
then
I . (g . ((proj (1,1)) . y)) = (I * (g * (proj (1,1)))) . y
by A38, FUNCT_1:12;
then
I . (g . ((proj (1,1)) . y)) = f . y
by A1, RELAT_1:36;
then
I . (g . ((proj (1,1)) . y)) = f /. y
by A23, A30, PARTFUN1:def 6;
then
(I . gJy) - (I . gJx) = (f /. y) - (f /. x)
by A29, REAL_NS1:5;
hence
(f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x))
by A32, A37, A39, REAL_NS1:2;
verum
end;
L0 is total
by FDIFF_1:def 3;
then A40:
dom L0 = REAL
by PARTFUN1:def 2;
A41:
L is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))
by LOPBAN_1:def 9;
then
f is_differentiable_in x
by A24, A23, A26, NDIFF_1:def 6;
then
diff (f,x) = (I * L0) * (proj (1,1))
by A24, A23, A41, A26, NDIFF_1:def 7;
then
(diff (f,x)) . <*1*> = ((I * L0) * (proj (1,1))) . (I . 1)
by Lm1;
then
(diff (f,x)) . <*jj*> = (I * L0) . ((proj (1,1)) . (I . jj))
by Lm1, FUNCT_1:13;
then
(diff (f,x)) . <*jj*> = I . (L0 . ((proj (1,1)) . (I . jj)))
by A40, FUNCT_1:13;
then
(diff (f,x)) . <*1*> = I . (L0 . 1)
by Lm1, FUNCT_1:35;
hence
( f is_differentiable_in x & (diff (f,x)) . <*1*> = <*(diff (g,y))*> )
by A24, A23, A9, A41, A26, Lm1, NDIFF_1:def 6; verum