let a1, c, a2, d be Real; ( c > 0 & d > 0 & a1 < a2 implies (((AffineMap ((d / c),(- ((d / c) * (a1 - c))))) | [.(a1 - c),a1.]) +* ((AffineMap (0,d)) | [.a1,a2.])) +* ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))) | [.a2,(a2 + c).]) = (d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)))) | ['(a1 - c),(a2 + c)'] )
assume A1:
( c > 0 & d > 0 & a1 < a2 )
; (((AffineMap ((d / c),(- ((d / c) * (a1 - c))))) | [.(a1 - c),a1.]) +* ((AffineMap (0,d)) | [.a1,a2.])) +* ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))) | [.a2,(a2 + c).]) = (d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)))) | ['(a1 - c),(a2 + c)']
then AB:
( a1 - c < a1 - 0 & a2 + 0 < a2 + c )
by XREAL_1:15, XREAL_1:8;
then AC:
a1 - c < a2
by XXREAL_0:2, A1;
set dT = d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)));
set F = (((AffineMap ((d / c),(- ((d / c) * (a1 - c))))) | [.(a1 - c),a1.]) +* ((AffineMap (0,d)) | [.a1,a2.])) +* ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))) | [.a2,(a2 + c).]);
A2: (AffineMap ((d / c),(- ((d / c) * (a1 - c))))) | [.(a1 - c),a1.] =
(AffineMap ((d * (1 / c)),((- ((d * 1) / c)) * (a1 - c)))) | [.(a1 - c),a1.]
by XCMPLX_1:99
.=
(AffineMap ((d * (1 / c)),((- (d * (1 / c))) * (a1 - c)))) | [.(a1 - c),a1.]
by XCMPLX_1:99
.=
(AffineMap ((d * (1 / c)),(d * (- ((1 / c) * (a1 - c)))))) | [.(a1 - c),a1.]
.=
(d (#) (AffineMap ((1 / c),(- ((1 / c) * (a1 - c)))))) | [.(a1 - c),a1.]
by Th28
.=
(d (#) (AffineMap ((1 / (a1 - (a1 - c))),(- ((a1 - c) / (a1 - (a1 - c))))))) | [.(a1 - c),a1.]
by XCMPLX_1:99
;
A3: (AffineMap ((- (d / c)),((d / c) * (a2 + c)))) | [.a2,(a2 + c).] =
(AffineMap ((- (d * (1 / c))),((d / c) * (a2 + c)))) | [.a2,(a2 + c).]
by XCMPLX_1:99
.=
(AffineMap ((d * (- (1 / c))),(d * ((a2 + c) / c)))) | [.a2,(a2 + c).]
by XCMPLX_1:75
.=
(d (#) (AffineMap ((- (1 / ((a2 + c) - a2))),((a2 + c) / ((a2 + c) - a2))))) | [.a2,(a2 + c).]
by Th28
;
(((AffineMap ((d / c),(- ((d / c) * (a1 - c))))) | [.(a1 - c),a1.]) +* ((AffineMap (0,d)) | [.a1,a2.])) +* ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))) | [.a2,(a2 + c).]) =
(((d (#) (AffineMap ((1 / (a1 - (a1 - c))),(- ((a1 - c) / (a1 - (a1 - c))))))) | [.(a1 - c),a1.]) +* ((AffineMap ((d * 0),(d * 1))) | [.a1,a2.])) +* ((d (#) (AffineMap ((- (1 / ((a2 + c) - a2))),((a2 + c) / ((a2 + c) - a2))))) | [.a2,(a2 + c).])
by A3, A2
.=
(((d (#) (AffineMap ((1 / (a1 - (a1 - c))),(- ((a1 - c) / (a1 - (a1 - c))))))) | [.(a1 - c),a1.]) +* ((d (#) (AffineMap (0,1))) | [.a1,a2.])) +* ((d (#) (AffineMap ((- (1 / ((a2 + c) - a2))),((a2 + c) / ((a2 + c) - a2))))) | [.a2,(a2 + c).])
by Th28
.=
(d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)))) | [.(a1 - c),(a2 + c).]
by A1, AB, LmSymTrape4
;
hence
(((AffineMap ((d / c),(- ((d / c) * (a1 - c))))) | [.(a1 - c),a1.]) +* ((AffineMap (0,d)) | [.a1,a2.])) +* ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))) | [.a2,(a2 + c).]) = (d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)))) | ['(a1 - c),(a2 + c)']
by INTEGRA5:def 3, AC, XXREAL_0:2, AB; verum