let a, b, c be Real; for f being Function of REAL,REAL st b > 0 & c > 0 & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) holds
f | ['(a - c),(a + c)'] = ((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(lower_bound ['(a - c),(a + c)']),(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))).]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))),(upper_bound ['(a - c),(a + c)']).])
let f be Function of REAL,REAL; ( b > 0 & c > 0 & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) implies f | ['(a - c),(a + c)'] = ((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(lower_bound ['(a - c),(a + c)']),(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))).]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))),(upper_bound ['(a - c),(a + c)']).]) )
assume that
A1:
b > 0
and
A2:
c > 0
and
A3:
for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|))
; f | ['(a - c),(a + c)'] = ((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(lower_bound ['(a - c),(a + c)']),(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))).]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))),(upper_bound ['(a - c),(a + c)']).])
set s = b / c;
set d = b - ((a * b) / c);
set p = - (b / c);
set q = b + ((a * b) / c);
set C = ['(a - c),(a + c)'];
A7: ((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c))) =
(((b + ((a * b) / c)) - b) + ((a * b) / c)) / ((b / c) + (b / c))
.=
(((a * b) / c) + (a * (b / c))) / ((b / c) + (b / c))
by XCMPLX_1:74
.=
((a * (b / c)) + (a * (b / c))) / ((b / c) + (b / c))
by XCMPLX_1:74
.=
(a * ((b / c) + (b / c))) / ((b / c) + (b / c))
.=
a * (((b / c) + (b / c)) / ((b / c) + (b / c)))
by XCMPLX_1:74
.=
a
by XCMPLX_1:88, A1, A2
;
A10:
( a - c <= a & a <= a + c )
by XREAL_1:43, XREAL_1:29, A2;
A8:
( [.(lower_bound ['(a - c),(a + c)']),(upper_bound ['(a - c),(a + c)']).] = ['(a - c),(a + c)'] & ['(a - c),(a + c)'] = [.(a - c),(a + c).] )
by XXREAL_0:2, A10, INTEGRA5:def 3, INTEGRA1:4;
set G = ((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[);
((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[) = ((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.[) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)
by FUZZY_6:35;
then reconsider G = ((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[) as Function of REAL,REAL by FUZZY_6:18;
set g = ((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(lower_bound ['(a - c),(a + c)']),(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))).]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))),(upper_bound ['(a - c),(a + c)']).]);
GI: ((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(lower_bound ['(a - c),(a + c)']),(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))).]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))),(upper_bound ['(a - c),(a + c)']).]) =
((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(lower_bound ['(a - c),(a + c)']),a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,(a + c).])
by A8, INTEGRA1:5, A7
.=
((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(a - c),a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,(a + c).])
by A8, INTEGRA1:5
.=
(((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) | [.(a - c),(a + c).]
by Th4, A1, A2
;
B4: dom (f | ['(a - c),(a + c)']) =
['(a - c),(a + c)']
by FUNCT_2:def 1
.=
[.(a - c),(a + c).]
by XXREAL_0:2, A10, INTEGRA5:def 3
.=
dom (G | [.(a - c),(a + c).])
by FUNCT_2:def 1
.=
dom (((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(lower_bound ['(a - c),(a + c)']),(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))).]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))),(upper_bound ['(a - c),(a + c)']).]))
by GI
;
for x being object st x in dom (f | ['(a - c),(a + c)']) holds
(f | ['(a - c),(a + c)']) . x = (((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(lower_bound ['(a - c),(a + c)']),(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))).]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))),(upper_bound ['(a - c),(a + c)']).])) . x
proof
let x be
object ;
( x in dom (f | ['(a - c),(a + c)']) implies (f | ['(a - c),(a + c)']) . x = (((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(lower_bound ['(a - c),(a + c)']),(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))).]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))),(upper_bound ['(a - c),(a + c)']).])) . x )
assume B1:
x in dom (f | ['(a - c),(a + c)'])
;
(f | ['(a - c),(a + c)']) . x = (((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(lower_bound ['(a - c),(a + c)']),(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))).]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))),(upper_bound ['(a - c),(a + c)']).])) . x
then C1:
x in ['(a - c),(a + c)']
;
reconsider x =
x as
Real by B1;
C2:
x in [.(a - c),(a + c).]
by XXREAL_0:2, A10, INTEGRA5:def 3, C1;
C3:
0 <= b - |.((b * (x - a)) / c).|
by Lm16, A1, A2, B1;
(((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(lower_bound ['(a - c),(a + c)']),(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))).]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))),(upper_bound ['(a - c),(a + c)']).])) . x =
(((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) . x
by FUNCT_1:49, C2, GI
.=
b - |.((b * (x - a)) / c).|
by Th1, A1, A2
.=
max (
0,
(b - |.((b * (x - a)) / c).|))
by C3, XXREAL_0:def 10
.=
f . x
by A3
;
hence
(f | ['(a - c),(a + c)']) . x = (((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(lower_bound ['(a - c),(a + c)']),(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))).]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))),(upper_bound ['(a - c),(a + c)']).])) . x
by FUNCT_1:49, B1;
verum
end;
hence
f | ['(a - c),(a + c)'] = ((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(lower_bound ['(a - c),(a + c)']),(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))).]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))),(upper_bound ['(a - c),(a + c)']).])
by B4, FUNCT_1:def 11; verum