let b, c be Real; ( c - b > 0 implies rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) = [.0,1.] )
set f = AffineMap ((- (1 / (c - b))),(c / (c - b)));
set g = (AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.];
assume A0:
c - b > 0
; rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) = [.0,1.]
thus
rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) c= [.0,1.]
XBOOLE_0:def 10 [.0,1.] c= rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])proof
let y be
object ;
TARSKI:def 3 ( not y in rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) or y in [.0,1.] )
assume Y0:
y in rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])
;
y in [.0,1.]
then consider x being
object such that A1:
x in dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])
and A2:
y = ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . x
by FUNCT_1:def 3;
Y1:
x in [.b,c.]
by A1, RELAT_1:57;
reconsider xx =
x as
Real by A1;
reconsider yy =
y as
Real by Y0;
S4:
y = (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . xx
by FUNCT_1:47, A1, A2;
A4:
b <= xx
by Y1, XXREAL_1:1;
S2:
(AffineMap ((- (1 / (c - b))),(c / (c - b)))) . b = 1
by Cb1, A0;
S5:
(AffineMap ((- (1 / (c - b))),(c / (c - b)))) . b >= (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . xx
by A4, FCONT_1:54, A0;
xx <= c
by Y1, XXREAL_1:1;
then S6:
(AffineMap ((- (1 / (c - b))),(c / (c - b)))) . xx >= (AffineMap ((- (1 / (c - b))),(c / (c - b)))) . c
by A0, FCONT_1:54;
(AffineMap ((- (1 / (c - b))),(c / (c - b)))) . c = 0
by Cb2;
hence
y in [.0,1.]
by S4, S2, S5, S6;
verum
end;
let y be object ; TARSKI:def 3 ( not y in [.0,1.] or y in rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) )
assume V1:
y in [.0,1.]
; y in rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])
then reconsider yy = y as Real ;
set A = - (1 / (c - b));
set B = c / (c - b);
L2:
(AffineMap ((- (1 / (c - b))),(c / (c - b)))) " = AffineMap (((- (1 / (c - b))) "),(- ((c / (c - b)) / (- (1 / (c - b))))))
by FCONT_1:56, A0;
then L3: ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) ") . 0 =
(((- (1 / (c - b))) ") * 0) + (- ((c / (c - b)) / (- (1 / (c - b)))))
by FCONT_1:def 4
.=
- ((c / (c - b)) / ((- 1) / (c - b)))
by XCMPLX_1:187
.=
- (c / (- 1))
by XCMPLX_1:55, A0
.=
c
;
X1: - ((c / (c - b)) / (- (1 / (c - b)))) =
- ((c / (c - b)) / ((- 1) / (c - b)))
by XCMPLX_1:187
.=
- (c / (- 1))
by XCMPLX_1:55, A0
.=
c
;
L4: ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) ") . 1 =
(((- (1 / (c - b))) ") * 1) + (- ((c / (c - b)) / (- (1 / (c - b)))))
by FCONT_1:def 4, L2
.=
(1 / (- (1 / (c - b)))) + (- ((c / (c - b)) / (- (1 / (c - b)))))
by XCMPLX_1:215
.=
(1 / ((- 1) / (c - b))) + c
by XCMPLX_1:187, X1
.=
((c - b) / (- 1)) + c
by XCMPLX_1:57
.=
b
;
set x = ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) ") . yy;
reconsider xx = ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) ") . yy as Real by L2;
J2:
( 0 <= yy & yy <= 1 )
by XXREAL_1:1, V1;
then J3:
c >= xx
by FCONT_1:54, L2, A0, L3;
xx >= b
by FCONT_1:54, L2, A0, J2, L4;
then J4:
((AffineMap ((- (1 / (c - b))),(c / (c - b)))) ") . yy in [.b,c.]
by J3;
jj:
dom (AffineMap ((- (1 / (c - b))),(c / (c - b)))) = REAL
by FUNCT_2:def 1;
T1:
((AffineMap ((- (1 / (c - b))),(c / (c - b)))) ") . yy in dom ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])
by J4, jj, RELAT_1:57;
rng (AffineMap ((- (1 / (c - b))),(c / (c - b)))) = REAL
by FCONT_1:55, A0;
then S2:
yy in rng (AffineMap ((- (1 / (c - b))),(c / (c - b))))
by XREAL_0:def 1;
set ff = (AffineMap ((- (1 / (c - b))),(c / (c - b)))) " ;
((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.]) . (((AffineMap ((- (1 / (c - b))),(c / (c - b)))) ") . yy) =
(AffineMap ((- (1 / (c - b))),(c / (c - b)))) . (((AffineMap ((- (1 / (c - b))),(c / (c - b)))) ") . yy)
by FUNCT_1:49, J4
.=
yy
by A0, S2, FUNCT_1:35
;
hence
y in rng ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | [.b,c.])
by T1, FUNCT_1:def 3; verum