let J be Function of (REAL 1),REAL; :: thesis: for x0 being Element of REAL 1 st J = proj (1,1) holds
( J is_differentiable_in x0 & diff (J,x0) = J )
let x0 be Element of REAL 1; :: thesis: ( J = proj (1,1) implies ( J is_differentiable_in x0 & diff (J,x0) = J ) )
assume A1: J = proj (1,1) ; :: thesis: ( J is_differentiable_in x0 & diff (J,x0) = J )
A2: 1 in Seg 1 ;
set R = (REAL 1) --> (0* 1);
set L = <>* J;
rng J = dom ((proj (1,1)) ") by A1, A2, PDIFF_1:1, PDIFF_1:2;
then A3: dom (<>* J) = dom J by RELAT_1:27
.= REAL 1 by A1, A2, PDIFF_1:1 ;
reconsider L = <>* J as Function of (REAL 1),(REAL 1) by PDIFF_1:2;
set f = <>* J;
A4: L = id (dom J) by A1, FUNCT_1:39
.= id (REAL 1) by A1, A2, PDIFF_1:1 ;
A5: for x, y being Element of REAL 1 holds L . (x + y) = (L . x) + (L . y) by A4;
A6: for x being Element of REAL 1
for r being Real holds L . (r * x) = r * (L . x) by A4;
then A7: L is LinearOperator of 1,1 by A5, PDIFF_6:def 1, PDIFF_6:def 2;
reconsider r0 = 1 as Real ;
A8: { y where y is Element of REAL 1 : |.(y - x0).| < r0 } c= dom (<>* J)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { y where y is Element of REAL 1 : |.(y - x0).| < r0 } or x in dom (<>* J) )
assume x in { y where y is Element of REAL 1 : |.(y - x0).| < r0 } ; :: thesis: x in dom (<>* J)
then ex y being Element of REAL 1 st
( x = y & |.(y - x0).| < r0 ) ;
hence x in dom (<>* J) by A3; :: thesis: verum
end;
A9: for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds
(|.z.| ") * |.w.| < r ) )
proof
let r be Real; :: thesis: ( r > 0 implies ex d being Real st
( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds
(|.z.| ") * |.w.| < r ) ) )
assume A10: r > 0 ; :: thesis: ex d being Real st
( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds
(|.z.| ") * |.w.| < r ) )
take d = r; :: thesis: ( d > 0 & ( for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds
(|.z.| ") * |.w.| < r ) )
thus 0 < d by A10; :: thesis: for z, w being Element of REAL 1 st z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z holds
(|.z.| ") * |.w.| < r
let z, w be Element of REAL 1; :: thesis: ( z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z implies (|.z.| ") * |.w.| < r )
assume A11: ( z <> 0* 1 & |.z.| < d & w = ((REAL 1) --> (0* 1)) . z ) ; :: thesis: (|.z.| ") * |.w.| < r
w = 0* 1 by A11, FUNCOP_1:7;
then |.w.| = 0 by EUCLID:7;
hence (|.z.| ") * |.w.| < r by A10; :: thesis: verum
end;
A12: for x being Element of REAL 1 st |.(x - x0).| < r0 holds
((<>* J) /. x) - ((<>* J) /. x0) = (L . (x - x0)) + (((REAL 1) --> (0* 1)) . (x - x0))
proof
let x be Element of REAL 1; :: thesis: ( |.(x - x0).| < r0 implies ((<>* J) /. x) - ((<>* J) /. x0) = (L . (x - x0)) + (((REAL 1) --> (0* 1)) . (x - x0)) )
assume |.(x - x0).| < r0 ; :: thesis: ((<>* J) /. x) - ((<>* J) /. x0) = (L . (x - x0)) + (((REAL 1) --> (0* 1)) . (x - x0))
thus ((<>* J) /. x) - ((<>* J) /. x0) = (L /. x) - (L /. x0)
.= (L /. x) + (L /. ((- 1) * x0)) by A6
.= L . (x - x0) by A5
.= (L . (x - x0)) + (0* 1) by RVSUM_1:16
.= (L . (x - x0)) + (((REAL 1) --> (0* 1)) . (x - x0)) by FUNCOP_1:7 ; :: thesis: verum
end;
then ( <>* J is_differentiable_in x0 & diff ((<>* J),x0) = L ) by A7, A8, A9, PDIFF_6:24;
hence J is_differentiable_in x0 ; :: thesis: diff (J,x0) = J
A13: rng J c= REAL ;
thus diff (J,x0) = (proj (1,1)) * L by A12, A7, A8, A9, PDIFF_6:24
.= ((proj (1,1)) * ((proj (1,1)) ")) * J by RELAT_1:36
.= (id (rng (proj (1,1)))) * J by FUNCT_1:39
.= (id REAL) * J by A2, PDIFF_1:1
.= J by A13, RELAT_1:53 ; :: thesis: verum