let a, b be Real; ( 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
; for x being Real holds (TriangularFS ((a - b),a,(a + b))) . x = max (0,(1 - |.((x - a) / b).|))
let x be Real; (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).[))
;
((((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
;
((((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;
verum end; suppose X2:
x <> a + b
;
((((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
;
((((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;
verum end; suppose
x <> a - b
;
((((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;
verum end; end; suppose P710:
x in dom ((AffineMap ((1 / (a - (a - b))),(- ((a - b) / (a - (a - b)))))) | [.(a - b),a.])
;
((((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
;
((((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;
verum end; suppose M1:
x <> a
;
((((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;
verum end; end; suppose P810:
x in dom ((AffineMap ((- (1 / ((a + b) - a))),((a + b) / ((a + b) - a)))) | [.a,(a + b).])
;
((((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;
verum end;
end;
hence
(TriangularFS ((a - b),a,(a + b))) . x = max (0,(1 - |.((x - a) / b).|))
by FUZNUM_1:def 7, A2; verum