let a, b be Real; ( a > 0 implies (AffineMap (a,b)) .: [.0,1.] = [.b,(a + b).] )
assume A1:
a > 0
; (AffineMap (a,b)) .: [.0,1.] = [.b,(a + b).]
thus
(AffineMap (a,b)) .: [.0,1.] c= [.b,(a + b).]
XBOOLE_0:def 10 [.b,(a + b).] c= (AffineMap (a,b)) .: [.0,1.]proof
A2:
(AffineMap (a,b)) . 1
= a + b
by Th49;
let u be
object ;
TARSKI:def 3 ( not u in (AffineMap (a,b)) .: [.0,1.] or u in [.b,(a + b).] )
assume
u in (AffineMap (a,b)) .: [.0,1.]
;
u in [.b,(a + b).]
then consider r being
Element of
REAL such that A3:
r in [.0,1.]
and A4:
u = (AffineMap (a,b)) . r
by FUNCT_2:65;
reconsider s =
u as
Real by A4;
r <= 1
by A3, XXREAL_1:1;
then A5:
s <= a + b
by A1, A4, A2, Th53;
A6:
(AffineMap (a,b)) . 0 = b
by Th48;
0 <= r
by A3, XXREAL_1:1;
then
b <= s
by A1, A4, A6, Th53;
hence
u in [.b,(a + b).]
by A5, XXREAL_1:1;
verum
end;
let u be object ; TARSKI:def 3 ( not u in [.b,(a + b).] or u in (AffineMap (a,b)) .: [.0,1.] )
assume A7:
u in [.b,(a + b).]
; u in (AffineMap (a,b)) .: [.0,1.]
then reconsider r = u as Element of REAL ;
set s = (r - b) / a;
A8: (AffineMap (a,b)) . ((r - b) / a) =
(a * ((r - b) / a)) + b
by Def4
.=
(r - b) + b
by A1, XCMPLX_1:87
.=
r
;
r <= a + b
by A7, XXREAL_1:1;
then
r - b <= a
by XREAL_1:20;
then
(r - b) / a <= a / a
by A1, XREAL_1:72;
then A9:
(r - b) / a <= 1
by A1, XCMPLX_1:60;
b <= r
by A7, XXREAL_1:1;
then
0 <= r - b
by XREAL_1:48;
then
(r - b) / a in [.0,1.]
by A1, A9, XXREAL_1:1;
hence
u in (AffineMap (a,b)) .: [.0,1.]
by A8, FUNCT_2:35; verum