let a, b, c, d, r, s be Real; ( a < b & b < c & c < d & r >= 0 & s >= 0 & r = s implies for x being Real holds (r (#) (TrapezoidalFS (a,b,c,d))) . x = max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x) )
assume A1:
( a < b & b < c & c < d )
; ( not r >= 0 or not s >= 0 or not r = s or for x being Real holds (r (#) (TrapezoidalFS (a,b,c,d))) . x = max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x) )
assume A2:
( r >= 0 & s >= 0 )
; ( not r = s or for x being Real holds (r (#) (TrapezoidalFS (a,b,c,d))) . x = max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x) )
assume A3:
r = s
; for x being Real holds (r (#) (TrapezoidalFS (a,b,c,d))) . x = max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x)
set fab = AffineMap ((r / (b - a)),(- ((a * r) / (b - a))));
set fbc = AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))));
set fcd = AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))));
set T = TrapezoidalFS (a,b,c,d);
A5: AffineMap ((r / (b - a)),(- ((a * r) / (b - a)))) =
AffineMap ((r * (1 / (b - a))),(- ((a * r) / (b - a))))
by XCMPLX_1:99
.=
AffineMap ((r * (1 / (b - a))),((- (r * a)) / (b - a)))
by XCMPLX_1:187
.=
AffineMap ((r * (1 / (b - a))),((r * (- a)) / (b - a)))
.=
AffineMap ((r * (1 / (b - a))),(r * ((- a) / (b - a))))
by XCMPLX_1:74
.=
AffineMap ((r * (1 / (b - a))),(r * (- (a / (b - a)))))
by XCMPLX_1:187
.=
r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))
by FUZZY_7:13
;
A7: AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c)))) =
AffineMap (((- r) / (d - c)),((- (d * (- r))) / (d - c)))
by XCMPLX_1:187, A3
.=
AffineMap ((r / (- (d - c))),((d * r) / (d - c)))
by XCMPLX_1:192
.=
AffineMap ((r * (1 / (- (d - c)))),((d * r) / (d - c)))
by XCMPLX_1:99
.=
AffineMap ((r * ((- 1) / (d - c))),((d * r) / (d - c)))
by XCMPLX_1:192
.=
AffineMap ((r * (- (1 / (d - c)))),((d * r) / (d - c)))
by XCMPLX_1:187
.=
AffineMap ((r * (- (1 / (d - c)))),(r * (d / (d - c))))
by XCMPLX_1:74
.=
r (#) (AffineMap ((- (1 / (d - c))),(d / (d - c))))
by FUZZY_7:13
;
A6: AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b)))) =
AffineMap ((r * 0),(r * 1))
by A3
.=
r (#) (AffineMap (0,1))
by FUZZY_7:13
;
for x being Real holds (r (#) (TrapezoidalFS (a,b,c,d))) . x = max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x)
proof
let x be
Real;
(r (#) (TrapezoidalFS (a,b,c,d))) . x = max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x)
A4:
(r (#) (TrapezoidalFS (a,b,c,d))) . x =
r * ((TrapezoidalFS (a,b,c,d)) . x)
by VALUED_1:6
.=
r * ((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((TrapezoidalFS (a,b,c,d)) | [.a,d.])) . x)
by FUZZY_7:45, A1
;
per cases
( x in [.a,d.] or not x in [.a,d.] )
;
suppose B1:
x in [.a,d.]
;
(r (#) (TrapezoidalFS (a,b,c,d))) . x = max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x)then XX:
x in dom ((TrapezoidalFS (a,b,c,d)) | [.a,d.])
by FUNCT_2:def 1;
B11:
((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x >= 0
by Lm2, A1, B1, A2;
B12:
max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x) =
max (
0,
(((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x))
by RFUNCT_3:def 1
.=
((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x
by XXREAL_0:def 10, B11
;
per cases
( x < b or b <= x )
;
suppose D1:
x < b
;
(r (#) (TrapezoidalFS (a,b,c,d))) . x = max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x)then Dc1:
x < c
by XXREAL_0:2, A1;
then D12:
not
x in dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])
by XXREAL_1:1;
D14:
not
x in dom ((AffineMap (0,1)) | [.b,c.])
by XXREAL_1:1, D1;
a <= x
by B1, XXREAL_1:1;
then
x in [.a,b.]
by D1;
then D15:
x in dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])
by FUNCT_2:def 1;
D13:
r * (((TrapezoidalFS (a,b,c,d)) | [.a,d.]) . x) =
r * (((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) . x)
by FUZZY_7:44, A1
.=
r * ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) . x)
by FUNCT_4:11, D12
.=
r * (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) . x)
by FUNCT_4:11, D14
.=
r * ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) . x)
by FUNCT_1:47, D15
.=
(AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) . x
by A5, VALUED_1:6
;
D16:
not
x in dom ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)
by XXREAL_1:236, Dc1;
D17:
not
x in dom ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])
by XXREAL_1:1, D1;
x in ].-infty,b.]
by D1, XXREAL_1:234;
then D18:
x in dom ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.])
by FUNCT_2:def 1;
((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x =
(((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) . x
by FUNCT_4:11, D16
.=
((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) . x
by FUNCT_4:11, D17
.=
(AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) . x
by FUNCT_1:47, D18
;
hence
(r (#) (TrapezoidalFS (a,b,c,d))) . x = max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x)
by D13, B12, FUNCT_4:13, A4, XX;
verum end; suppose D2:
b <= x
;
(r (#) (TrapezoidalFS (a,b,c,d))) . x = max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x)per cases
( x < c or c <= x )
;
suppose D3:
x < c
;
(r (#) (TrapezoidalFS (a,b,c,d))) . x = max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x)then D33:
not
x in dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])
by XXREAL_1:1;
D39:
x in [.b,c.]
by D3, D2;
then D32:
x in dom ((AffineMap (0,1)) | [.b,c.])
by FUNCT_2:def 1;
D31:
r * (((TrapezoidalFS (a,b,c,d)) | [.a,d.]) . x) =
r * (((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) . x)
by FUZZY_7:44, A1
.=
r * ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) . x)
by FUNCT_4:11, D33
.=
r * (((AffineMap (0,1)) | [.b,c.]) . x)
by FUNCT_4:13, D32
.=
r * ((AffineMap (0,1)) . x)
by FUNCT_1:47, D32
.=
(AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) . x
by A6, VALUED_1:6
;
D34:
not
x in dom ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)
by D3, XXREAL_1:236;
D35:
x in dom ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])
by FUNCT_2:def 1, D39;
((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x =
(((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) . x
by FUNCT_4:11, D34
.=
((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.]) . x
by FUNCT_4:13, D35
.=
(AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) . x
by FUNCT_1:47, D35
;
hence
(r (#) (TrapezoidalFS (a,b,c,d))) . x = max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x)
by D31, FUNCT_4:13, A4, XX, B12;
verum end; suppose D4:
c <= x
;
(r (#) (TrapezoidalFS (a,b,c,d))) . x = max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x)
x <= d
by B1, XXREAL_1:1;
then
x in [.c,d.]
by D4;
then D42:
x in dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])
by FUNCT_2:def 1;
D41:
r * (((TrapezoidalFS (a,b,c,d)) | [.a,d.]) . x) =
r * (((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) . x)
by FUZZY_7:44, A1
.=
r * (((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) . x)
by FUNCT_4:13, D42
.=
r * ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) . x)
by FUNCT_1:47, D42
.=
(AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) . x
by A7, VALUED_1:6
;
x in [.c,+infty.[
by D4, XXREAL_1:236;
then D43:
x in dom ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)
by FUNCT_2:def 1;
((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x =
((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[) . x
by FUNCT_4:13, D43
.=
(AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) . x
by FUNCT_1:47, D43
;
hence
(r (#) (TrapezoidalFS (a,b,c,d))) . x = max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x)
by D41, FUNCT_4:13, A4, XX, B12;
verum end; end; suppose C1:
not
x in [.a,d.]
;
(r (#) (TrapezoidalFS (a,b,c,d))) . x = max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x)then C2:
(
x < a or
d < x )
;
then C3:
((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x <= 0
by Lm1, A1, A2;
C6:
max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x) =
max (
0,
(((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x))
by RFUNCT_3:def 1
.=
0
by XXREAL_0:def 10, C3
;
C4:
not
x in dom ((TrapezoidalFS (a,b,c,d)) | [.a,d.])
by C1;
C8:
x in REAL
by XREAL_0:def 1;
not
x in ].a,d.[
by XXREAL_1:4, C2;
then C5:
x in REAL \ ].a,d.[
by XBOOLE_0:def 5, C8;
(r (#) (TrapezoidalFS (a,b,c,d))) . x =
r * (((AffineMap (0,0)) | (REAL \ ].a,d.[)) . x)
by C4, FUNCT_4:11, A4
.=
r * ((AffineMap (0,0)) . x)
by FUNCT_1:49, C5
.=
r * ((0 * x) + 0)
by FCONT_1:def 4
;
hence
(r (#) (TrapezoidalFS (a,b,c,d))) . x = max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x)
by C6;
verum end;
end;
hence
for x being Real holds (r (#) (TrapezoidalFS (a,b,c,d))) . x = max+ (((((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | ].-infty,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,+infty.[)) . x)
; verum