let a, b, p, q be Real; ( a > 0 & p > 0 & (1 - b) / a < (1 - q) / (- p) implies for x being Real holds (TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) )
assume AA:
a > 0
; ( not p > 0 or not (1 - b) / a < (1 - q) / (- p) or for x being Real holds (TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) )
assume PP:
p > 0
; ( not (1 - b) / a < (1 - q) / (- p) or for x being Real holds (TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) )
assume A5:
(1 - b) / a < (1 - q) / (- p)
; for x being Real holds (TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
( 0 + (- q) < 1 + (- q) & - p < 0 )
by PP, XREAL_1:8;
then A6:
(1 - q) / (- p) < (- q) / (- p)
by XREAL_1:75;
0 + (- b) < 1 + (- b)
by XREAL_1:8;
then A0:
( (- b) / a < (1 - b) / a & (1 - b) / a < (1 - q) / (- p) & (1 - q) / (- p) < q / p )
by XREAL_1:74, AA, A5, A6, XCMPLX_1:191;
then A00:
(1 - b) / a < q / p
by XXREAL_0:2;
set f0 = (AffineMap (0,0)) | (REAL \ ].((- b) / a),(q / p).[);
set f1 = (AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).];
set f2 = (AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).];
set f3 = (AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).];
set f4 = (AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[;
set f5 = (AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[;
D2:
dom ((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).]) = [.((1 - b) / a),((1 - q) / (- p)).]
by FUNCT_2:def 1;
D3:
dom ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).]) = [.((1 - q) / (- p)),(q / p).]
by FUNCT_2:def 1;
D5:
dom ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[) = [.((q - b) / (a + p)),+infty.[
by FUNCT_2:def 1;
for x being Real holds (TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
proof
let x be
Real;
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
B170:
dom (((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).]) +* ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).])) =
(dom ((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).])) \/ (dom ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).]))
by FUNCT_4:def 1
.=
[.((1 - b) / a),((1 - q) / (- p)).] \/ (dom ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).]))
by FUNCT_2:def 1
.=
[.((1 - b) / a),((1 - q) / (- p)).] \/ [.((1 - q) / (- p)),(q / p).]
by FUNCT_2:def 1
.=
[.((1 - b) / a),(q / p).]
by XXREAL_1:165, A0
;
B17:
dom (((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).]) +* (((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).]) +* ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).]))) =
(dom ((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).])) \/ (dom (((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).]) +* ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).])))
by FUNCT_4:def 1
.=
[.((- b) / a),((1 - b) / a).] \/ (dom (((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).]) +* ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).])))
by FUNCT_2:def 1
.=
[.((- b) / a),(q / p).]
by XXREAL_1:165, A0, A00, B170
;
F1:
(AffineMap ((1 / (((1 - b) / a) + (- ((- b) / a)))),(- (((- b) / a) / (((1 - b) / a) + (- ((- b) / a))))))) . x =
(AffineMap ((1 / (((1 - b) / a) + (- ((- b) / a)))),(- (((- b) / a) / (((1 - b) / a) + (b / a)))))) . x
by XCMPLX_1:190
.=
(AffineMap ((1 / (((1 - b) / a) + (b / a))),(- (((- b) / a) / (((1 - b) / a) + (b / a)))))) . x
by XCMPLX_1:190
.=
(AffineMap ((1 / (((1 - b) / a) + (b / a))),(- (((- b) / a) / (((1 - b) + b) / a))))) . x
by XCMPLX_1:62
.=
(AffineMap ((1 / (((1 - b) + b) / a)),(- (((- b) / a) / (1 / a))))) . x
by XCMPLX_1:62
.=
(AffineMap ((1 / (1 / a)),(- (((- b) / a) * a)))) . x
by XCMPLX_1:100
.=
(AffineMap ((a * (1 / 1)),(- (((- b) / a) * a)))) . x
by XCMPLX_1:81
.=
(AffineMap (a,(- ((a / a) * (- b))))) . x
by XCMPLX_1:75
.=
(AffineMap (a,(- (1 * (- b))))) . x
by XCMPLX_1:60, AA
.=
(AffineMap (a,b)) . x
;
F3:
(AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) . x =
(AffineMap ((- (1 / ((q / p) + ((1 - q) / p)))),((q / p) / ((q / p) + (- ((1 - q) / (- p))))))) . x
by XCMPLX_1:189
.=
(AffineMap ((- (1 / ((q / p) + ((1 - q) / p)))),((q / p) / ((q / p) + ((1 - q) / p))))) . x
by XCMPLX_1:189
.=
(AffineMap ((- (1 / ((q + (1 - q)) / p))),((q / p) / ((q / p) + ((1 - q) / p))))) . x
by XCMPLX_1:62
.=
(AffineMap ((- (1 / (1 / p))),((q / p) / ((q + (1 - q)) / p)))) . x
by XCMPLX_1:62
.=
(AffineMap ((- p),((q / p) / (1 / p)))) . x
by XCMPLX_1:56
.=
(AffineMap ((- p),((q / p) * p))) . x
by XCMPLX_1:100
.=
(AffineMap ((- p),q)) . x
by XCMPLX_1:87, PP
.=
((- p) * x) + q
by FCONT_1:def 4
;
per cases
( x <= (- b) / a or (- b) / a < x )
;
suppose B1:
x <= (- b) / a
;
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))then
x * a <= ((- b) / a) * a
by XREAL_1:64, AA;
then
x * a <= (a / a) * (- b)
by XCMPLX_1:75;
then
x * a <= 1
* (- b)
by XCMPLX_1:60, AA;
then B14:
(a * x) + b <= (- b) + b
by XREAL_1:6;
0 + ((- b) / a) < (1 / a) + ((- b) / a)
by XREAL_1:6, AA;
then MM:
(- b) / a < (1 + (- b)) / a
by XCMPLX_1:62;
(1 - b) / a < (q - b) / (a + p)
by asymTT4, A5, AA, PP;
then
(- b) / a < (q - b) / (a + p)
by MM, XXREAL_0:2;
then B15:
x < (q - b) / (a + p)
by B1, XXREAL_0:2;
B11:
max (
0,
(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) =
max (
0,
(min (1,(((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) . x))))
by FUNCT_4:11, D5, XXREAL_1:236, B15
.=
max (
0,
(min (1,((AffineMap (a,b)) . x))))
by FUNCT_1:49, B15, XXREAL_1:233
.=
max (
0,
(min (1,((a * x) + b))))
by FCONT_1:def 4
.=
max (
0,
((a * x) + b))
by XXREAL_0:def 9, B14
.=
0
by XXREAL_0:def 10, B14
;
per cases
( x = (- b) / a or x <> (- b) / a )
;
suppose E1:
x = (- b) / a
;
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = 0
by TrZoi1, A0, E1;
hence
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (
0,
(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
by B11;
verum end; suppose E2:
x <> (- b) / a
;
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
( not
x in ].((- b) / a),(q / p).[ &
x in REAL )
by B1, XREAL_0:def 1, XXREAL_1:4;
then B14:
x in REAL \ ].((- b) / a),(q / p).[
by XBOOLE_0:def 5;
x < (- b) / a
by B1, E2, XXREAL_0:1;
then E21:
not
x in dom (((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).]) +* (((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).]) +* ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).])))
by XXREAL_1:1, B17;
(((((AffineMap (0,0)) | (REAL \ ].((- b) / a),(q / p).[)) +* ((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).])) +* ((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).])) +* ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).])) . x =
((((AffineMap (0,0)) | (REAL \ ].((- b) / a),(q / p).[)) +* ((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).])) +* (((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).]) +* ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).]))) . x
by FUNCT_4:14
.=
(((AffineMap (0,0)) | (REAL \ ].((- b) / a),(q / p).[)) +* (((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).]) +* (((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).]) +* ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).])))) . x
by FUNCT_4:14
.=
((AffineMap (0,0)) | (REAL \ ].((- b) / a),(q / p).[)) . x
by FUNCT_4:11, E21
.=
(AffineMap (0,0)) . x
by FUNCT_1:49, B14
.=
(0 * x) + 0
by FCONT_1:def 4
.=
0
;
hence
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (
0,
(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
by B11, FUZNUM_1:def 8, A0;
verum end; suppose B2:
(- b) / a < x
;
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))then
x * a > ((- b) / a) * a
by XREAL_1:68, AA;
then
x * a > (a / a) * (- b)
by XCMPLX_1:75;
then
x * a > 1
* (- b)
by XCMPLX_1:60, AA;
then B21:
(a * x) + b > (- b) + b
by XREAL_1:6;
per cases
( x <= (1 - b) / a or (1 - b) / a < x )
;
suppose B3:
x <= (1 - b) / a
;
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
x * a <= ((1 - b) / a) * a
by XREAL_1:64, B3, AA;
then
x * a <= (a / a) * (1 - b)
by XCMPLX_1:75;
then
x * a <= 1
* (1 - b)
by XCMPLX_1:60, AA;
then B33:
(x * a) + b <= (1 - b) + b
by XREAL_1:6;
(1 - b) / a < (q - b) / (a + p)
by asymTT4, AA, PP, A5;
then B31:
x < (q - b) / (a + p)
by B3, XXREAL_0:2;
B61:
max (
0,
(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) =
max (
0,
(min (1,(((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) . x))))
by FUNCT_4:11, D5, XXREAL_1:236, B31
.=
max (
0,
(min (1,((AffineMap (a,b)) . x))))
by FUNCT_1:49, B31, XXREAL_1:233
.=
max (
0,
(min (1,((a * x) + b))))
by FCONT_1:def 4
.=
max (
0,
((a * x) + b))
by XXREAL_0:def 9, B33
;
B34:
x in [.((- b) / a),((1 - b) / a).]
by B2, B3;
then B35:
x in dom ((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).])
by FUNCT_2:def 1;
per cases
( x = (1 - b) / a or x <> (1 - b) / a )
;
suppose E1B3:
x = (1 - b) / a
;
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))then E1B31:
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = 1
by TrZoi1, A0;
max (
0,
(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) =
max (
0,
(((a / a) * (1 - b)) + b))
by XCMPLX_1:75, E1B3, B61
.=
max (
0,
((1 * (1 - b)) + b))
by XCMPLX_1:60, AA
.=
1
by XXREAL_0:def 10
;
hence
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (
0,
(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
by E1B31;
verum end; suppose
x <> (1 - b) / a
;
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))then
( not
(1 - b) / a <= x or not
x <= q / p )
by B3, XXREAL_0:1;
then B36:
not
x in dom (((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).]) +* ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).]))
by B170, XXREAL_1:1;
(((((AffineMap (0,0)) | (REAL \ ].((- b) / a),(q / p).[)) +* ((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).])) +* ((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).])) +* ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).])) . x =
((((AffineMap (0,0)) | (REAL \ ].((- b) / a),(q / p).[)) +* ((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).])) +* (((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).]) +* ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).]))) . x
by FUNCT_4:14
.=
(((AffineMap (0,0)) | (REAL \ ].((- b) / a),(q / p).[)) +* ((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).])) . x
by FUNCT_4:11, B36
.=
((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).]) . x
by FUNCT_4:13, B35
.=
(AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) . x
by FUNCT_1:49, B34
.=
(a * x) + b
by FCONT_1:def 4, F1
.=
max (
0,
((a * x) + b))
by XXREAL_0:def 10, B21
;
hence
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (
0,
(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
by B61, FUZNUM_1:def 8, A0;
verum end; end; suppose B4:
(1 - b) / a < x
;
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))then
x * a > ((1 - b) / a) * a
by XREAL_1:68, AA;
then
x * a > (a / a) * (1 - b)
by XCMPLX_1:75;
then
x * a > 1
* (1 - b)
by XCMPLX_1:60, AA;
then B41:
(x * a) + b > (1 - b) + b
by XREAL_1:6;
per cases
( x <= (1 - q) / (- p) or (1 - q) / (- p) < x )
;
suppose B5:
x <= (1 - q) / (- p)
;
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))per cases
( x = (1 - q) / (- p) or x <> (1 - q) / (- p) )
;
suppose B5E:
x = (1 - q) / (- p)
;
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))then AS:
(q - b) / (a + p) < x
by asymTT4, A5, AA, PP;
B5E3:
max (
0,
(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) =
max (
0,
(min (1,(((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[) . x))))
by FUNCT_4:13, D5, AS, XXREAL_1:236
.=
max (
0,
(min (1,((AffineMap ((- p),q)) . x))))
by FUNCT_1:49, AS, XXREAL_1:236
.=
max (
0,
(min (1,(((- p) * x) + q))))
by FCONT_1:def 4
.=
max (
0,
(min (1,((((- p) / (- p)) * (1 - q)) + q))))
by XCMPLX_1:75, B5E
.=
max (
0,
(min (1,((1 * (1 - q)) + q))))
by XCMPLX_1:60, PP
.=
1
by XXREAL_0:def 10
;
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = 1
by TrZoi1, A0, B5E;
hence
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (
0,
(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
by B5E3;
verum end; suppose B5N:
x <> (1 - q) / (- p)
;
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))then B5N5:
x < (1 - q) / (- p)
by B5, XXREAL_0:1;
( not
(1 - q) / (- p) <= x or not
x <= q / p )
by B5, XXREAL_0:1, B5N;
then B5N1:
not
x in dom ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).])
by D3, XXREAL_1:1;
((1 - q) / (- p)) * (- p) < x * (- p)
by XREAL_1:69, PP, B5N5;
then
((- p) / (- p)) * (1 - q) < x * (- p)
by XCMPLX_1:75;
then
1
* (1 - q) < x * (- p)
by XCMPLX_1:60, PP;
then BB:
((- p) * x) + q > (1 - q) + q
by XREAL_1:6;
B5N3:
x in [.((1 - b) / a),((1 - q) / (- p)).]
by B4, B5;
B5N2:
x in dom ((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).])
by D2, B4, B5;
B5N4:
(((((AffineMap (0,0)) | (REAL \ ].((- b) / a),(q / p).[)) +* ((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).])) +* ((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).])) +* ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).])) . x =
((((AffineMap (0,0)) | (REAL \ ].((- b) / a),(q / p).[)) +* ((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).])) +* ((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).])) . x
by FUNCT_4:11, B5N1
.=
((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).]) . x
by FUNCT_4:13, B5N2
.=
(AffineMap (0,1)) . x
by FUNCT_1:49, B5N3
.=
(0 * x) + 1
by FCONT_1:def 4
.=
1
;
per cases
( x < (q - b) / (a + p) or (q - b) / (a + p) <= x )
;
suppose B9:
x < (q - b) / (a + p)
;
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))then max (
0,
(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) =
max (
0,
(min (1,(((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) . x))))
by FUNCT_4:11, D5, XXREAL_1:236
.=
max (
0,
(min (1,((AffineMap (a,b)) . x))))
by FUNCT_1:49, B9, XXREAL_1:233
.=
max (
0,
(min (1,((a * x) + b))))
by FCONT_1:def 4
.=
max (
0,1)
by XXREAL_0:def 9, B41
.=
1
by XXREAL_0:def 10
;
hence
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (
0,
(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
by B5N4, FUZNUM_1:def 8, A0;
verum end; suppose B10:
(q - b) / (a + p) <= x
;
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))then max (
0,
(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) =
max (
0,
(min (1,(((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[) . x))))
by FUNCT_4:13, D5, XXREAL_1:236
.=
max (
0,
(min (1,((AffineMap ((- p),q)) . x))))
by FUNCT_1:49, B10, XXREAL_1:236
.=
max (
0,
(min (1,(((- p) * x) + q))))
by FCONT_1:def 4
.=
max (
0,1)
by XXREAL_0:def 9, BB
.=
1
by XXREAL_0:def 10
;
hence
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (
0,
(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
by B5N4, FUZNUM_1:def 8, A0;
verum end; end; suppose B6:
(1 - q) / (- p) < x
;
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))then
((1 - q) / (- p)) * (- p) > x * (- p)
by XREAL_1:69, PP;
then
((- p) / (- p)) * (1 - q) > x * (- p)
by XCMPLX_1:75;
then
1
* (1 - q) > x * (- p)
by XCMPLX_1:60, PP;
then B63:
((- p) * x) + q < (1 - q) + q
by XREAL_1:6;
AZ:
(q - b) / (a + p) < (1 - q) / (- p)
by asymTT4, A5, AA, PP;
B62:
x in [.((q - b) / (a + p)),+infty.[
by XXREAL_1:236, AZ, B6, XXREAL_0:2;
x in dom ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)
by D5, AZ, B6, XXREAL_0:2, XXREAL_1:236;
then B61:
max (
0,
(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) =
max (
0,
(min (1,(((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[) . x))))
by FUNCT_4:13
.=
max (
0,
(min (1,((AffineMap ((- p),q)) . x))))
by FUNCT_1:49, B62
.=
max (
0,
(min (1,(((- p) * x) + q))))
by FCONT_1:def 4
.=
max (
0,
(((- p) * x) + q))
by XXREAL_0:def 9, B63
;
per cases
( x <= q / p or q / p < x )
;
suppose B7:
x <= q / p
;
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))then B71:
x in [.((1 - q) / (- p)),(q / p).]
by B6;
B72:
x in dom ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).])
by D3, B7, B6;
x * p <= (q / p) * p
by XREAL_1:64, PP, B7;
then
x * p <= (p / p) * q
by XCMPLX_1:75;
then
x * p <= 1
* q
by XCMPLX_1:60, PP;
then B73:
(x * p) - (x * p) <= q - (p * x)
by XREAL_1:9;
(((((AffineMap (0,0)) | (REAL \ ].((- b) / a),(q / p).[)) +* ((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).])) +* ((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).])) +* ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).])) . x =
((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).]) . x
by FUNCT_4:13, B72
.=
(AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) . x
by FUNCT_1:49, B71
.=
max (
0,
(((- p) * x) + q))
by XXREAL_0:def 10, B73, F3
;
hence
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (
0,
(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
by FUZNUM_1:def 8, A0, B61;
verum end; suppose B8:
q / p < x
;
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))then
( not
x in ].((- b) / a),(q / p).[ &
x in REAL )
by XREAL_0:def 1, XXREAL_1:4;
then B81:
x in REAL \ ].((- b) / a),(q / p).[
by XBOOLE_0:def 5;
E21:
not
x in dom (((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).]) +* (((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).]) +* ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).])))
by XXREAL_1:1, B17, B8;
B82:
(((((AffineMap (0,0)) | (REAL \ ].((- b) / a),(q / p).[)) +* ((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).])) +* ((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).])) +* ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).])) . x =
((((AffineMap (0,0)) | (REAL \ ].((- b) / a),(q / p).[)) +* ((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).])) +* (((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).]) +* ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).]))) . x
by FUNCT_4:14
.=
(((AffineMap (0,0)) | (REAL \ ].((- b) / a),(q / p).[)) +* (((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).]) +* (((AffineMap (0,1)) | [.((1 - b) / a),((1 - q) / (- p)).]) +* ((AffineMap ((- (1 / ((q / p) - ((1 - q) / (- p))))),((q / p) / ((q / p) - ((1 - q) / (- p)))))) | [.((1 - q) / (- p)),(q / p).])))) . x
by FUNCT_4:14
.=
((AffineMap (0,0)) | (REAL \ ].((- b) / a),(q / p).[)) . x
by FUNCT_4:11, E21
.=
(AffineMap (0,0)) . x
by FUNCT_1:49, B81
.=
(0 * x) + 0
by FCONT_1:def 4
.=
0
;
x * p > (q / p) * p
by XREAL_1:68, PP, B8;
then
x * p > (p / p) * q
by XCMPLX_1:75;
then
x * p > 1
* q
by XCMPLX_1:60, PP;
then B83:
(x * p) - (x * p) > q - (p * x)
by XREAL_1:9;
max (
0,
(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
= 0
by XXREAL_0:def 10, B83, B61;
hence
(TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (
0,
(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
by B82, FUZNUM_1:def 8, A0;
verum end; end; end; end;
end;
hence
for x being Real holds (TrapezoidalFS (((- b) / a),((1 - b) / a),((1 - q) / (- p)),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
; verum