let a, b be Real; :: thesis: ( b > 0 implies for x being Real holds (TriangularFS ((a - b),a,(a + b))) . x = max (0,(1 - |.((x - a) / b).|)) )
assume A1: b > 0 ; :: thesis: for x being Real holds (TriangularFS ((a - b),a,(a + b))) . x = max (0,(1 - |.((x - a) / b).|))
let x be Real; :: thesis: (TriangularFS ((a - b),a,(a + b))) . x = max (0,(1 - |.((x - a) / b).|))
A2A: 0 + a < b + a by XREAL_1:29, A1;
then A2: ( a - b < (a + b) - b & a < a + b ) by XREAL_1:14;
set f1 = (AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[);
set f2 = (AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.];
set f3 = (AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).];
set F = (((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).]);
P1: dom ((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) = REAL \ ].(a - b),(a + b).[ by FUNCT_2:def 1;
P2: dom ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.]) = [.(a - b),a.] by FUNCT_2:def 1;
P3: dom ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).]) = [.a,(a + b).] by FUNCT_2:def 1;
dom ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) = dom (TriangularFS ((a - b),a,(a + b))) by FUZNUM_1:def 7, A2
.= REAL by FUNCT_2:def 1 ;
then P66: ( x in dom (((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) or x in dom ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).]) ) by FUNCT_4:12, XREAL_0:def 1;
((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = max (0,(1 - |.((x - a) / b).|))
proof
per cases ( x in dom ((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) or x in dom ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.]) or x in dom ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).]) ) by P66, FUNCT_4:12;
suppose P610: x in dom ((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) ; :: thesis: ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = max (0,(1 - |.((x - a) / b).|))
then ( x in REAL & not x in ].(a - b),(a + b).[ ) by XBOOLE_0:def 5, P1;
then P613: ( x <= a - b or a + b <= x ) ;
per cases ( x = a + b or x <> a + b ) ;
suppose X0: x = a + b ; :: thesis: ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = max (0,(1 - |.((x - a) / b).|))
then X2B: a <= x by A1, XREAL_1:29;
X3: ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).]) . x by FUNCT_4:13, P3, X2B, X0, XXREAL_1:1
.= (AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) . x by FUNCT_1:47, X2B, X0, XXREAL_1:1, P3
.= ((- (1 / ((a + b) - a))) * x) + ((a + b) / ((a + b) - a)) by FCONT_1:def 4
.= (- ((a + b) * (1 / ((a + b) - a)))) + ((a + b) / ((a + b) - a)) by X0
.= (- ((1 * (a + b)) / ((a + b) - a))) + ((a + b) / ((a + b) - a)) by XCMPLX_1:74
.= 0 ;
1 - |.((x - a) / b).| = 1 - |.1.| by A1, XCMPLX_1:60, X0
.= 1 - 1 by ABSVALUE:def 1 ;
hence ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = max (0,(1 - |.((x - a) / b).|)) by X3; :: thesis: verum
end;
suppose X2: x <> a + b ; :: thesis: ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = max (0,(1 - |.((x - a) / b).|))
( not a <= x or not x <= a + b ) by A2, P613, XXREAL_0:1, XXREAL_0:2, X2;
then not x in dom ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).]) by P3, XXREAL_1:1;
then P614: ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = (((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) . x by FUNCT_4:11;
per cases ( x = a - b or x <> a - b ) ;
suppose X0: x = a - b ; :: thesis: ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = max (0,(1 - |.((x - a) / b).|))
x in [.(a - b),a.] by A2, X0;
then X2: x in dom ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.]) by FUNCT_2:def 1;
then X3: ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.]) . x by P614, FUNCT_4:13
.= (AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) . x by FUNCT_1:47, X2
.= ((1 / (a - (a - b))) * x) + (- ((a - b) / (a - (a - b)))) by FCONT_1:def 4
.= ((1 / (a - (a - b))) * (a - b)) - ((a - b) / (a - (a - b))) by X0
.= (((a - b) * 1) / (a - (a - b))) - ((a - b) / (a - (a - b))) by XCMPLX_1:74
.= 0 ;
1 - |.((x - a) / b).| = 1 - |.((- b) / b).| by X0
.= 1 - |.(- (b / b)).| by XCMPLX_1:187
.= 1 - |.(- 1).| by A1, XCMPLX_1:60
.= 1 - |.1.| by COMPLEX1:52
.= 1 - 1 by ABSVALUE:def 1 ;
hence ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = max (0,(1 - |.((x - a) / b).|)) by X3; :: thesis: verum
end;
suppose x <> a - b ; :: thesis: ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = max (0,(1 - |.((x - a) / b).|))
then ( x < a - b or a < x ) by A2A, P613, XXREAL_0:2, XXREAL_0:1;
then not x in [.(a - b),a.] by XXREAL_1:1;
then not x in dom ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.]) by FUNCT_2:def 1;
then P616: ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = ((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) . x by P614, FUNCT_4:11
.= (AffineMap (0,0)) . x by FUNCT_1:47, P610
.= (0 * x) + 0 by FCONT_1:def 4
.= 0 ;
( x - a <= (a - b) - a or (a + b) - a <= x - a ) by P613, XREAL_1:13;
then P617: ( (x - a) / b <= ((a - b) - a) / b or ((a + b) - a) / b <= (x - a) / b ) by A1, XREAL_1:72;
((a - b) - a) / b = (- b) / b
.= - (b / b) by XCMPLX_1:187
.= - 1 by A1, XCMPLX_1:60 ;
then ( (x - a) / b <= - 1 or 1 <= (x - a) / b ) by P617, A1, XCMPLX_1:60;
then 1 <= |.((x - a) / b).| by LmABS;
hence ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = max (0,(1 - |.((x - a) / b).|)) by P616, XXREAL_0:def 10, XREAL_1:47; :: thesis: verum
end;
end;
end;
end;
end;
suppose P710: x in dom ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.]) ; :: thesis: ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = max (0,(1 - |.((x - a) / b).|))
then P711: ( a - b <= x & x <= a ) by P2, XXREAL_1:1;
per cases ( x = a or x <> a ) ;
suppose P713: x = a ; :: thesis: ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = max (0,(1 - |.((x - a) / b).|))
a <= a + b by P713, P711, XREAL_1:20;
then P714: x in dom ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).]) by P713, P3;
P715: ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).]) . x by FUNCT_4:13, P714
.= (AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) . x by FUNCT_1:47, P714
.= ((- (1 / ((a + b) - a))) * x) + ((a + b) / ((a + b) - a)) by FCONT_1:def 4
.= (- ((1 / b) * a)) + ((a + b) / b) by P713
.= (- ((a * 1) / b)) + ((a + b) / b) by XCMPLX_1:74
.= ((a + b) / b) - (a / b)
.= ((a + b) - a) / b by XCMPLX_1:120
.= 1 by XCMPLX_1:60, A1 ;
1 - |.((x - a) / b).| = 1 - 0 by ABSVALUE:def 1, P713;
then max (0,(1 - |.((x - a) / b).|)) = 1 by XXREAL_0:def 10;
hence ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = max (0,(1 - |.((x - a) / b).|)) by P715; :: thesis: verum
end;
suppose M1: x <> a ; :: thesis: ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = max (0,(1 - |.((x - a) / b).|))
then P716: x < a by P711, XXREAL_0:1;
( x < a or a + b < x ) by M1, P711, XXREAL_0:1;
then not x in [.a,(a + b).] by XXREAL_1:1;
then not x in dom ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).]) by FUNCT_2:def 1;
then P777: ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = (((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) . x by FUNCT_4:11
.= ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.]) . x by P710, FUNCT_4:13
.= (AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) . x by FUNCT_1:49, P710, P2
.= ((1 / (a - (a - b))) * x) + (- ((a - b) / (a - (a - b)))) by FCONT_1:def 4
.= ((x * 1) / (a - (a - b))) + (- ((a - b) / (a - (a - b)))) by XCMPLX_1:74
.= ((x * 1) / ((a - a) + b)) - ((a - b) / ((a - a) + b))
.= (x - (a - b)) / b by XCMPLX_1:120 ;
x - a < a - a by XREAL_1:9, P716;
then P77: 1 - |.((x - a) / b).| = 1 - (- ((x - a) / b)) by ABSVALUE:def 1, A1
.= 1 + ((x - a) / b)
.= (b / b) + ((x - a) / b) by XCMPLX_1:60, A1
.= (b + (x - a)) / b by XCMPLX_1:62
.= (x - (a - b)) / b ;
a - b <= x by P710, P2, XXREAL_1:1;
then (a - b) - (a - b) <= x - (a - b) by XREAL_1:9;
then max (0,(1 - |.((x - a) / b).|)) = (x - (a - b)) / b by XXREAL_0:def 10, P77, A1;
hence ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = max (0,(1 - |.((x - a) / b).|)) by P777; :: thesis: verum
end;
end;
end;
suppose P810: x in dom ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).]) ; :: thesis: ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = max (0,(1 - |.((x - a) / b).|))
then P811: ( a <= x & x <= a + b ) by XXREAL_1:1, P3;
P812: x in dom (((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.]) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) by FUNCT_4:12, P810;
P888: ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = (((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* (((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.]) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).]))) . x by FUNCT_4:14
.= (((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.]) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x by FUNCT_4:13, P812
.= ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).]) . x by FUNCT_4:13, P810
.= (AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) . x by FUNCT_1:49, P810, P3
.= ((- (1 / ((a + b) - a))) * x) + ((a + b) / ((a + b) - a)) by FCONT_1:def 4
.= (- ((1 / ((a + b) - a)) * x)) + ((a + b) / ((a + b) - a))
.= (- ((x * 1) / ((a + b) - a))) + ((a + b) / ((a + b) - a)) by XCMPLX_1:74
.= ((a + b) / b) - (x / b)
.= ((a + b) - x) / b by XCMPLX_1:120 ;
x - a >= a - a by XREAL_1:9, P811;
then P88: 1 - |.((x - a) / b).| = 1 - ((x - a) / b) by ABSVALUE:def 1, A1
.= (b / b) - ((x - a) / b) by XCMPLX_1:60, A1
.= (b - (x - a)) / b by XCMPLX_1:120
.= ((b - x) + a) / b ;
x - x <= (a + b) - x by XREAL_1:9, P811;
then max (0,(1 - |.((x - a) / b).|)) = ((b - x) + a) / b by XXREAL_0:def 10, P88, A1;
hence ((((AffineMap (0,0)) | (REAL \ ].(a - b),(a + b).[)) +* ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])) +* ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])) . x = max (0,(1 - |.((x - a) / b).|)) by P888; :: thesis: verum
end;
end;
end;
hence (TriangularFS ((a - b),a,(a + b))) . x = max (0,(1 - |.((x - a) / b).|)) by FUZNUM_1:def 7, A2; :: thesis: verum