A1:
[#] REAL = dom (exp_R * (AffineMap (- 1),0 ))
by FUNCT_2:def 1;
A2:
[#] REAL = dom (AffineMap (- 1),0 )
by FUNCT_2:def 1;
A3:
for x being Real st x in REAL holds
(AffineMap (- 1),0 ) . x = ((- 1) * x) + 0
by JORDAN16:def 3;
then A4:
( AffineMap (- 1),0 is_differentiable_on REAL & ( for x being Real st x in [#] REAL holds
((AffineMap (- 1),0 ) `| REAL ) . x = - 1 ) )
by A2, FDIFF_1:31;
for x being Real st x in REAL holds
exp_R * (AffineMap (- 1),0 ) is_differentiable_in x
then A5:
exp_R * (AffineMap (- 1),0 ) is_differentiable_on REAL
by A1, FDIFF_1:16;
for x being Real st x in REAL holds
((- (exp_R * (AffineMap (- 1),0 ))) `| REAL ) . x = exp_R (- x)
proof
let x be
Real;
:: thesis: ( x in REAL implies ((- (exp_R * (AffineMap (- 1),0 ))) `| REAL ) . x = exp_R (- x) )
assume
x in REAL
;
:: thesis: ((- (exp_R * (AffineMap (- 1),0 ))) `| REAL ) . x = exp_R (- x)
A6:
AffineMap (- 1),
0 is_differentiable_in x
by A4, FDIFF_1:16;
((- (exp_R * (AffineMap (- 1),0 ))) `| REAL ) . x =
(- 1) * (diff (exp_R * (AffineMap (- 1),0 )),x)
by Lm1, A5, FDIFF_1:28
.=
(- 1) * ((exp_R . ((AffineMap (- 1),0 ) . x)) * (diff (AffineMap (- 1),0 ),x))
by A6, TAYLOR_1:19
.=
(- 1) * ((exp_R . ((AffineMap (- 1),0 ) . x)) * (((AffineMap (- 1),0 ) `| REAL ) . x))
by A4, FDIFF_1:def 8
.=
(- 1) * ((exp_R . ((AffineMap (- 1),0 ) . x)) * (- 1))
by A2, A3, FDIFF_1:31
.=
(- 1) * ((exp_R . (((- 1) * x) + 0 )) * (- 1))
by JORDAN16:def 3
.=
exp_R (- x)
;
hence
((- (exp_R * (AffineMap (- 1),0 ))) `| REAL ) . x = exp_R (- x)
;
:: thesis: verum
end;
hence
( - (exp_R * (AffineMap (- 1),0 )) is_differentiable_on REAL & ( for x being Real holds ((- (exp_R * (AffineMap (- 1),0 ))) `| REAL ) . x = exp_R (- x) ) )
by A5, Lm1, FDIFF_1:28; :: thesis: verum