let a, b, c, d, r be Real; ( a < b & b < c & c < d implies (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) = (TrapezoidalFS (a,b,c,d)) | [.a,d.] )
assume that
Z1:
a < b
and
Z2:
b < c
and
Z3:
c < d
; (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) = (TrapezoidalFS (a,b,c,d)) | [.a,d.]
Z4:
a < c
by XXREAL_0:2, Z1, Z2;
set f1 = (AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.];
set f2 = (AffineMap (0,1)) | [.b,c.];
set f3 = (AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.];
D2: dom ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) =
(dom (((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.]))) \/ (dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))
by FUNCT_4:def 1
.=
((dom ((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.])) \/ (dom ((AffineMap (0,1)) | [.b,c.]))) \/ (dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))
by FUNCT_4:def 1
.=
([.a,b.] \/ (dom ((AffineMap (0,1)) | [.b,c.]))) \/ (dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))
by FUNCT_2:def 1
.=
([.a,b.] \/ [.b,c.]) \/ (dom ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]))
by FUNCT_2:def 1
.=
([.a,b.] \/ [.b,c.]) \/ [.c,d.]
by FUNCT_2:def 1
.=
[.a,c.] \/ [.c,d.]
by XXREAL_1:165, Z1, Z2
.=
[.a,d.]
by XXREAL_1:165, Z4, Z3
;
D1:
dom ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) = dom ((TrapezoidalFS (a,b,c,d)) | [.a,d.])
by FUNCT_2:def 1, D2;
for x being object st x in dom ((TrapezoidalFS (a,b,c,d)) | [.a,d.]) holds
((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) . x = ((TrapezoidalFS (a,b,c,d)) | [.a,d.]) . x
proof
let x be
object ;
( x in dom ((TrapezoidalFS (a,b,c,d)) | [.a,d.]) implies ((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) . x = ((TrapezoidalFS (a,b,c,d)) | [.a,d.]) . x )
assume A1a:
x in dom ((TrapezoidalFS (a,b,c,d)) | [.a,d.])
;
((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) . x = ((TrapezoidalFS (a,b,c,d)) | [.a,d.]) . x
then reconsider x =
x as
Real ;
((TrapezoidalFS (a,b,c,d)) | [.a,d.]) . x =
(TrapezoidalFS (a,b,c,d)) . x
by FUNCT_1:49, A1a
.=
(((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((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 FUZNUM_1:def 8, Z1, Z2, Z3
.=
((((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((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 FUNCT_4:14
.=
(((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* (((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 FUNCT_4:14
.=
(((AffineMap (0,0)) | (REAL \ ].a,d.[)) +* ((((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 FUNCT_4:14
.=
((((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 FUNCT_4:13, A1a, D2
;
hence
((((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.])) . x = ((TrapezoidalFS (a,b,c,d)) | [.a,d.]) . x
;
verum
end;
hence
(((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) = (TrapezoidalFS (a,b,c,d)) | [.a,d.]
by FUNCT_1:2, D1; verum