let a, b, p, q be Real; ( a > 0 & p > 0 & (- b) / a < q / p & (1 - b) / a = (1 - q) / (- p) implies for x being Real holds (TriangularFS (((- b) / a),((1 - b) / a),(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 A2:
a > 0
; ( not p > 0 or not (- b) / a < q / p or not (1 - b) / a = (1 - q) / (- p) or for x being Real holds (TriangularFS (((- b) / a),((1 - b) / a),(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 A3:
p > 0
; ( not (- b) / a < q / p or not (1 - b) / a = (1 - q) / (- p) or for x being Real holds (TriangularFS (((- b) / a),((1 - b) / a),(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 A4:
(- b) / a < q / p
; ( not (1 - b) / a = (1 - q) / (- p) or for x being Real holds (TriangularFS (((- b) / a),((1 - b) / a),(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 (TriangularFS (((- b) / a),((1 - b) / a),(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 A3, 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 < q / p )
by XREAL_1:74, A2, A5, A6, XCMPLX_1:191;
set f1 = (AffineMap (0,0)) | (REAL \ ].((- b) / a),(q / p).[);
set f2 = (AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).];
set f3 = (AffineMap ((- (1 / ((q / p) - ((1 - b) / a)))),((q / p) / ((q / p) - ((1 - b) / a))))) | [.((1 - b) / a),(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 ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).]) = [.((- b) / a),((1 - b) / a).]
by FUNCT_2:def 1;
D3:
dom ((AffineMap ((- (1 / ((q / p) - ((1 - b) / a)))),((q / p) / ((q / p) - ((1 - b) / a))))) | [.((1 - b) / a),(q / p).]) = [.((1 - b) / a),(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 (TriangularFS (((- b) / a),((1 - b) / a),(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;
(TriangularFS (((- b) / a),((1 - b) / a),(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 <= (- b) / a or (- b) / a < x )
;
suppose B1:
x <= (- b) / a
;
(TriangularFS (((- b) / a),((1 - b) / a),(q / p))) . x = max (0,(min (1,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x))))
(- b) / a < (q - b) / (a + p)
by asymTT2, A2, A3, A4;
then B15:
x < (q - b) / (a + p)
by B1, XXREAL_0:2;
per cases
( x = (- b) / a or x <> (- b) / a )
;
suppose N2:
x = (- b) / a
;
(TriangularFS (((- b) / a),((1 - b) / a),(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 N3:
(TriangularFS (((- b) / a),((1 - b) / a),(q / p))) . x = 0
by TrAng1, A0;
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, XXREAL_1:233, B15
.=
max (
0,
(min (1,((a * x) + b))))
by FCONT_1:def 4
.=
max (
0,
(min (1,(((a / a) * (- b)) + b))))
by XCMPLX_1:75, N2
.=
max (
0,
(min (1,((1 * (- b)) + b))))
by XCMPLX_1:60, A2
.=
0
by XXREAL_0:36
;
hence
(TriangularFS (((- b) / a),((1 - b) / a),(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 N3;
verum end; suppose N1:
x <> (- b) / a
;
(TriangularFS (((- b) / a),((1 - b) / a),(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;
B17:
dom (((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).]) +* ((AffineMap ((- (1 / ((q / p) - ((1 - b) / a)))),((q / p) / ((q / p) - ((1 - b) / a))))) | [.((1 - b) / a),(q / p).])) =
(dom ((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).])) \/ (dom ((AffineMap ((- (1 / ((q / p) - ((1 - b) / a)))),((q / p) / ((q / p) - ((1 - b) / a))))) | [.((1 - b) / a),(q / p).]))
by FUNCT_4:def 1
.=
[.((- b) / a),((1 - b) / a).] \/ (dom ((AffineMap ((- (1 / ((q / p) - ((1 - b) / a)))),((q / p) / ((q / p) - ((1 - b) / a))))) | [.((1 - b) / a),(q / p).]))
by FUNCT_2:def 1
.=
[.((- b) / a),((1 - b) / a).] \/ [.((1 - b) / a),(q / p).]
by FUNCT_2:def 1
.=
[.((- b) / a),(q / p).]
by XXREAL_1:165, A0
;
B16:
x < (- b) / a
by B1, N1, XXREAL_0:1;
then B11:
not
x in dom (((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).]) +* ((AffineMap ((- (1 / ((q / p) - ((1 - b) / a)))),((q / p) / ((q / p) - ((1 - b) / a))))) | [.((1 - b) / a),(q / p).]))
by XXREAL_1:1, B17;
x * a < ((- b) / a) * a
by XREAL_1:68, A2, B16;
then
x * a < (a / a) * (- b)
by XCMPLX_1:75;
then
x * a < 1
* (- b)
by XCMPLX_1:60, A2;
then B150a:
(x * a) + b < (- b) + b
by XREAL_1:6;
B10:
((((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 ((- (1 / ((q / p) - ((1 - b) / a)))),((q / p) / ((q / p) - ((1 - b) / a))))) | [.((1 - b) / a),(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 ((- (1 / ((q / p) - ((1 - b) / a)))),((q / p) / ((q / p) - ((1 - b) / a))))) | [.((1 - b) / a),(q / p).]))) . x
by FUNCT_4:14
.=
((AffineMap (0,0)) | (REAL \ ].((- b) / a),(q / p).[)) . x
by FUNCT_4:11, B11
.=
(AffineMap (0,0)) . x
by FUNCT_1:49, B14
.=
(0 * x) + 0
by FCONT_1:def 4
.=
0
;
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, XXREAL_1:233, B15
.=
max (
0,
(min (1,((a * x) + b))))
by FCONT_1:def 4
.=
max (
0,
((a * x) + b))
by B150a, XXREAL_0:def 9
.=
0
by B150a, XXREAL_0:def 10
;
hence
(TriangularFS (((- b) / a),((1 - b) / a),(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 B10, FUZNUM_1:def 7, A0;
verum end; suppose B2:
(- b) / a < x
;
(TriangularFS (((- b) / a),((1 - b) / a),(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
((- b) / a) * a < x * a
by XREAL_1:68, A2;
then
(a / a) * (- b) < x * a
by XCMPLX_1:75;
then
1
* (- b) < x * a
by XCMPLX_1:60, A2;
then B2Xa:
(- b) + b < (x * a) + b
by XREAL_1:6;
per cases
( x < (1 - b) / a or (1 - b) / a <= x )
;
suppose B3:
x < (1 - b) / a
;
(TriangularFS (((- b) / a),((1 - b) / a),(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, A2;
then
x * a < (a / a) * (1 - b)
by XCMPLX_1:75;
then
x * a < 1
* (1 - b)
by XCMPLX_1:60, A2;
then B3Xa:
(x * a) + b < (1 - b) + b
by XREAL_1:6;
B33:
x in [.((- b) / a),((1 - b) / a).]
by B3, B2;
B32:
x in dom ((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).])
by D2, B3, B2;
B31:
not
x in dom ((AffineMap ((- (1 / ((q / p) - ((1 - b) / a)))),((q / p) / ((q / p) - ((1 - b) / a))))) | [.((1 - b) / a),(q / p).])
by D3, XXREAL_1:1, B3;
B34:
(TriangularFS (((- b) / a),((1 - b) / a),(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 ((- (1 / ((q / p) - ((1 - b) / a)))),((q / p) / ((q / p) - ((1 - b) / a))))) | [.((1 - b) / a),(q / p).])) . x
by FUZNUM_1:def 7, A0
.=
(((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, B31
.=
((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).]) . x
by FUNCT_4:13, B32
.=
(AffineMap ((1 / (((1 - b) / a) + (- ((- b) / a)))),(- (((- b) / a) / (((1 - b) / a) + (- ((- b) / a))))))) . x
by FUNCT_1:49, B33
.=
(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, A2
.=
(AffineMap (a,b)) . x
;
B38:
x < (q - b) / (a + p)
by B3, asymTT3, A2, A3, A5;
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, B38
.=
max (
0,
(min (1,((AffineMap (a,b)) . x))))
by FUNCT_1:49, B38, 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, B3Xa
.=
(a * x) + b
by XXREAL_0:def 10, B2Xa
;
hence
(TriangularFS (((- b) / a),((1 - b) / a),(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 FCONT_1:def 4, B34;
verum end; suppose B4:
(1 - b) / a <= x
;
(TriangularFS (((- b) / a),((1 - b) / a),(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 B41a:
(q - b) / (a + p) <= x
by asymTT3, A2, A3, A5;
((1 - q) / (- p)) * (- p) >= x * (- p)
by XREAL_1:65, A3, B4, A5;
then
((- p) / (- p)) * (1 - q) >= x * (- p)
by XCMPLX_1:75;
then
1
* (1 - q) >= x * (- p)
by XCMPLX_1:60, A3;
then B43a:
((- p) * x) + q <= (1 - q) + q
by XREAL_1:6;
B44:
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, B41a, XXREAL_1:236
.=
max (
0,
(min (1,((AffineMap ((- p),q)) . x))))
by FUNCT_1:49, B41a, XXREAL_1:236
.=
max (
0,
(min (1,(((- p) * x) + q))))
by FCONT_1:def 4
.=
max (
0,
(((- p) * x) + q))
by XXREAL_0:def 9, B43a
;
per cases
( x < q / p or q / p <= x )
;
suppose B5:
x < q / p
;
(TriangularFS (((- b) / a),((1 - b) / a),(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 B53:
x in [.((1 - b) / a),(q / p).]
by B4;
x * p < (q / p) * p
by XREAL_1:68, A3, B5;
then
x * p < (p / p) * q
by XCMPLX_1:75;
then
x * p < 1
* q
by XCMPLX_1:60, A3;
then B54a:
(x * p) - (x * p) < q - (p * x)
by XREAL_1:9;
(TriangularFS (((- b) / a),((1 - b) / a),(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 ((- (1 / ((q / p) - ((1 - b) / a)))),((q / p) / ((q / p) - ((1 - b) / a))))) | [.((1 - b) / a),(q / p).])) . x
by FUZNUM_1:def 7, A0
.=
((AffineMap ((- (1 / ((q / p) - ((1 - b) / a)))),((q / p) / ((q / p) - ((1 - b) / a))))) | [.((1 - b) / a),(q / p).]) . x
by FUNCT_4:13, B53, D3
.=
(AffineMap ((- (1 / ((q / p) - ((1 - b) / a)))),((q / p) / ((q / p) - ((1 - b) / a))))) . x
by FUNCT_1:49, B53
.=
(AffineMap ((- (1 / ((q / p) + ((1 - q) / p)))),((q / p) / ((q / p) + (- ((1 - q) / (- p))))))) . x
by XCMPLX_1:189, A5
.=
(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, A3
.=
((- p) * x) + q
by FCONT_1:def 4
.=
max (
0,
(((- p) * x) + q))
by XXREAL_0:def 10, B54a
;
hence
(TriangularFS (((- b) / a),((1 - b) / a),(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 B44;
verum end; suppose B6:
q / p <= x
;
(TriangularFS (((- b) / a),((1 - b) / a),(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 B14:
x in REAL \ ].((- b) / a),(q / p).[
by XBOOLE_0:def 5;
B17:
dom (((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).]) +* ((AffineMap ((- (1 / ((q / p) - ((1 - b) / a)))),((q / p) / ((q / p) - ((1 - b) / a))))) | [.((1 - b) / a),(q / p).])) =
(dom ((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).])) \/ (dom ((AffineMap ((- (1 / ((q / p) - ((1 - b) / a)))),((q / p) / ((q / p) - ((1 - b) / a))))) | [.((1 - b) / a),(q / p).]))
by FUNCT_4:def 1
.=
[.((- b) / a),((1 - b) / a).] \/ (dom ((AffineMap ((- (1 / ((q / p) - ((1 - b) / a)))),((q / p) / ((q / p) - ((1 - b) / a))))) | [.((1 - b) / a),(q / p).]))
by FUNCT_2:def 1
.=
[.((- b) / a),((1 - b) / a).] \/ [.((1 - b) / a),(q / p).]
by FUNCT_2:def 1
.=
[.((- b) / a),(q / p).]
by XXREAL_1:165, A0
;
TT2:
(q - b) / (a + p) < q / p
by asymTT2, A2, A3, A4;
then B62:
x in [.((q - b) / (a + p)),+infty.[
by XXREAL_1:236, B6, XXREAL_0:2;
B61:
x in dom ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)
by D5, XXREAL_1:236, B6, XXREAL_0:2, TT2;
per cases
( x = q / p or x <> q / p )
;
suppose N3:
x = q / p
;
(TriangularFS (((- b) / a),((1 - b) / a),(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 B66:
(TriangularFS (((- b) / a),((1 - b) / a),(q / p))) . x = 0
by TrAng1, A0;
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, B61
.=
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,
(min (1,((- (p * (q / p))) + q))))
by N3
.=
max (
0,
(min (1,((- ((p * q) / p)) + q))))
by XCMPLX_1:74
.=
max (
0,
(min (1,((- q) + q))))
by XCMPLX_1:89, A3
.=
max (
0,
0)
by XXREAL_0:def 9
.=
0
;
hence
(TriangularFS (((- b) / a),((1 - b) / a),(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 B66;
verum end; suppose N4:
x <> q / p
;
(TriangularFS (((- b) / a),((1 - b) / a),(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
(- b) / a <= x or not
x <= q / p )
by B6, XXREAL_0:1;
then B11:
not
x in dom (((AffineMap ((1 / (((1 - b) / a) - ((- b) / a))),(- (((- b) / a) / (((1 - b) / a) - ((- b) / a)))))) | [.((- b) / a),((1 - b) / a).]) +* ((AffineMap ((- (1 / ((q / p) - ((1 - b) / a)))),((q / p) / ((q / p) - ((1 - b) / a))))) | [.((1 - b) / a),(q / p).]))
by XXREAL_1:1, B17;
x > q / p
by B6, N4, XXREAL_0:1;
then
x * p > (q / p) * p
by XREAL_1:68, A3;
then
x * p > (p / p) * q
by XCMPLX_1:75;
then
x * p > 1
* q
by XCMPLX_1:60, A3;
then B63a:
(x * p) - (x * p) > q - (p * x)
by XREAL_1:9;
B60:
((((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 ((- (1 / ((q / p) - ((1 - b) / a)))),((q / p) / ((q / p) - ((1 - b) / a))))) | [.((1 - b) / a),(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 ((- (1 / ((q / p) - ((1 - b) / a)))),((q / p) / ((q / p) - ((1 - b) / a))))) | [.((1 - b) / a),(q / p).]))) . x
by FUNCT_4:14
.=
((AffineMap (0,0)) | (REAL \ ].((- b) / a),(q / p).[)) . x
by FUNCT_4:11, B11
.=
(AffineMap (0,0)) . x
by FUNCT_1:49, B14
.=
(0 * x) + 0
by FCONT_1:def 4
.=
0
;
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, B61
.=
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 B63a, XXREAL_0:def 9
.=
0
by B63a, XXREAL_0:def 10
;
hence
(TriangularFS (((- b) / a),((1 - b) / a),(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 B60, FUZNUM_1:def 7, A0;
verum end; end; end; end;
end;
hence
for x being Real holds (TriangularFS (((- b) / a),((1 - b) / a),(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