let C be non empty set ; for f being PartFunc of C,ExtREAL
for c being Real st 0 <= c holds
( max+ ((- c) (#) f) = c (#) (max- f) & max- ((- c) (#) f) = c (#) (max+ f) )
let f be PartFunc of C,ExtREAL; for c being Real st 0 <= c holds
( max+ ((- c) (#) f) = c (#) (max- f) & max- ((- c) (#) f) = c (#) (max+ f) )
let c be Real; ( 0 <= c implies ( max+ ((- c) (#) f) = c (#) (max- f) & max- ((- c) (#) f) = c (#) (max+ f) ) )
assume A1:
0 <= c
; ( max+ ((- c) (#) f) = c (#) (max- f) & max- ((- c) (#) f) = c (#) (max+ f) )
A2:
dom (max+ ((- c) (#) f)) = dom ((- c) (#) f)
by MESFUNC2:def 2;
then
dom (max+ ((- c) (#) f)) = dom f
by MESFUNC1:def 6;
then A3:
dom (max+ ((- c) (#) f)) = dom (max- f)
by MESFUNC2:def 3;
then A4:
dom (max+ ((- c) (#) f)) = dom (c (#) (max- f))
by MESFUNC1:def 6;
for x being Element of C st x in dom (max+ ((- c) (#) f)) holds
(max+ ((- c) (#) f)) . x = (c (#) (max- f)) . x
proof
let x be
Element of
C;
( x in dom (max+ ((- c) (#) f)) implies (max+ ((- c) (#) f)) . x = (c (#) (max- f)) . x )
assume A5:
x in dom (max+ ((- c) (#) f))
;
(max+ ((- c) (#) f)) . x = (c (#) (max- f)) . x
then A6:
(max+ ((- c) (#) f)) . x =
max (
(((- c) (#) f) . x),
0)
by MESFUNC2:def 2
.=
max (
((- c) * (f . x)),
0)
by A2, A5, MESFUNC1:def 6
.=
max (
(- (c * (f . x))),
0)
by XXREAL_3:92
;
(c (#) (max- f)) . x =
c * ((max- f) . x)
by A4, A5, MESFUNC1:def 6
.=
c * (max ((- (f . x)),0))
by A3, A5, MESFUNC2:def 3
.=
max (
(c * (- (f . x))),
(c * 0))
by A1, Th6
.=
max (
(- (c * (f . x))),
(c * 0))
by XXREAL_3:92
;
hence
(max+ ((- c) (#) f)) . x = (c (#) (max- f)) . x
by A6;
verum
end;
hence
max+ ((- c) (#) f) = c (#) (max- f)
by A4, PARTFUN1:5; max- ((- c) (#) f) = c (#) (max+ f)
A7:
dom (max- ((- c) (#) f)) = dom ((- c) (#) f)
by MESFUNC2:def 3;
then
dom (max- ((- c) (#) f)) = dom f
by MESFUNC1:def 6;
then A8:
dom (max- ((- c) (#) f)) = dom (max+ f)
by MESFUNC2:def 2;
then A9:
dom (max- ((- c) (#) f)) = dom (c (#) (max+ f))
by MESFUNC1:def 6;
for x being Element of C st x in dom (max- ((- c) (#) f)) holds
(max- ((- c) (#) f)) . x = (c (#) (max+ f)) . x
proof
let x be
Element of
C;
( x in dom (max- ((- c) (#) f)) implies (max- ((- c) (#) f)) . x = (c (#) (max+ f)) . x )
assume A10:
x in dom (max- ((- c) (#) f))
;
(max- ((- c) (#) f)) . x = (c (#) (max+ f)) . x
then A11:
(max- ((- c) (#) f)) . x =
max (
(- (((- c) (#) f) . x)),
0)
by MESFUNC2:def 3
.=
max (
(- ((- c) * (f . x))),
0)
by A7, A10, MESFUNC1:def 6
.=
max (
((- (- c)) * (f . x)),
0)
by XXREAL_3:92
;
(c (#) (max+ f)) . x =
c * ((max+ f) . x)
by A9, A10, MESFUNC1:def 6
.=
c * (max ((f . x),0))
by A8, A10, MESFUNC2:def 2
.=
max (
(c * (f . x)),
(c * 0))
by A1, Th6
;
hence
(max- ((- c) (#) f)) . x = (c (#) (max+ f)) . x
by A11;
verum
end;
hence
max- ((- c) (#) f) = c (#) (max+ f)
by A9, PARTFUN1:5; verum