let r be Real; ( r <> 0 implies ( (1 / r) (#) (exp_R * (AffineMap (r,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x ) ) )
assume A1:
r <> 0
; ( (1 / r) (#) (exp_R * (AffineMap (r,0))) is_differentiable_on REAL & ( for x being Real holds (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x ) )
A2:
[#] REAL = dom (exp_R * (AffineMap (r,0)))
by FUNCT_2:def 1;
A3:
[#] REAL = dom (AffineMap (r,0))
by FUNCT_2:def 1;
A4:
for x being Real st x in REAL holds
(AffineMap (r,0)) . x = (r * x) + 0
by FCONT_1:def 4;
then A5:
AffineMap (r,0) is_differentiable_on REAL
by A3, FDIFF_1:23;
for x being Real st x in REAL holds
exp_R * (AffineMap (r,0)) is_differentiable_in x
then A6:
( [#] REAL = dom ((1 / r) (#) (exp_R * (AffineMap (r,0)))) & exp_R * (AffineMap (r,0)) is_differentiable_on REAL )
by A2, FDIFF_1:9, FUNCT_2:def 1;
hence
(1 / r) (#) (exp_R * (AffineMap (r,0))) is_differentiable_on REAL
by FDIFF_1:20; for x being Real holds (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x
A7:
for x being Real st x in REAL holds
(((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x
proof
let x be
Real;
( x in REAL implies (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x )
assume A8:
x in REAL
;
(((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x
then A9:
AffineMap (
r,
0)
is_differentiable_in x
by A3, A5, FDIFF_1:9;
(((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x =
(1 / r) * (diff ((exp_R * (AffineMap (r,0))),x))
by A6, FDIFF_1:20, A8
.=
(1 / r) * ((exp_R . ((AffineMap (r,0)) . x)) * (diff ((AffineMap (r,0)),x)))
by A9, TAYLOR_1:19
.=
(1 / r) * ((exp_R . ((AffineMap (r,0)) . x)) * (((AffineMap (r,0)) `| REAL) . x))
by A5, FDIFF_1:def 7, A8
.=
(1 / r) * ((exp_R . ((AffineMap (r,0)) . x)) * r)
by A3, A4, FDIFF_1:23, A8
.=
(r * (1 / r)) * (exp_R . ((AffineMap (r,0)) . x))
.=
(r / r) * (exp_R . ((AffineMap (r,0)) . x))
by XCMPLX_1:99
.=
1
* (exp_R . ((AffineMap (r,0)) . x))
by A1, XCMPLX_1:60
.=
(exp_R * (AffineMap (r,0))) . x
by A2, FUNCT_1:12, A8
;
hence
(((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x
;
verum
end;
let x be Real; (((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x
x in REAL
by XREAL_0:def 1;
hence
(((1 / r) (#) (exp_R * (AffineMap (r,0)))) `| REAL) . x = (exp_R * (AffineMap (r,0))) . x
by A7; verum