let C be non empty set ; :: thesis: 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 ; :: thesis: for c being Real st 0 <= c holds
( max+ ((- c) (#) f) = c (#) (max- f) & max- ((- c) (#) f) = c (#) (max+ f) )
let c be Real; :: thesis: ( 0 <= c implies ( max+ ((- c) (#) f) = c (#) (max- f) & max- ((- c) (#) f) = c (#) (max+ f) ) )
assume A1:
0 <= c
; :: thesis: ( max+ ((- c) (#) f) = c (#) (max- f) & max- ((- c) (#) f) = c (#) (max+ f) )
A2:
( dom (max+ ((- c) (#) f)) = dom ((- c) (#) f) & dom (max- ((- c) (#) f)) = dom ((- c) (#) f) )
by MESFUNC2:def 2, MESFUNC2:def 3;
then
( dom (max+ ((- c) (#) f)) = dom f & dom (max- ((- c) (#) f)) = dom f )
by MESFUNC1:def 6;
then A3:
( dom (max+ ((- c) (#) f)) = dom (max- f) & dom (max- ((- c) (#) f)) = dom (max+ f) )
by MESFUNC2:def 2, MESFUNC2:def 3;
then A4:
( dom (max+ ((- c) (#) f)) = dom (c (#) (max- f)) & dom (max- ((- c) (#) f)) = dom (c (#) (max+ f)) )
by MESFUNC1:def 6;
A5:
- (R_EAL c) = - c
by SUPINF_2:3;
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;
:: thesis: ( x in dom (max+ ((- c) (#) f)) implies (max+ ((- c) (#) f)) . x = (c (#) (max- f)) . x )
assume A6:
x in dom (max+ ((- c) (#) f))
;
:: thesis: (max+ ((- c) (#) f)) . x = (c (#) (max- f)) . x
then A7:
(max+ ((- c) (#) f)) . x =
max (((- c) (#) f) . x),
0
by MESFUNC2:def 2
.=
max ((R_EAL (- c)) * (f . x)),
0
by A2, A6, MESFUNC1:def 6
.=
max (- ((R_EAL c) * (f . x))),
0
by A5, XXREAL_3:103
;
(c (#) (max- f)) . x =
(R_EAL c) * ((max- f) . x)
by A4, A6, MESFUNC1:def 6
.=
(R_EAL c) * (max (- (f . x)),(R_EAL 0 ))
by A3, A6, MESFUNC2:def 3
.=
max ((R_EAL c) * (- (f . x))),
((R_EAL c) * (R_EAL 0 ))
by A1, Th11
.=
max (- ((R_EAL c) * (f . x))),
(c * 0 )
by XXREAL_3:103
;
hence
(max+ ((- c) (#) f)) . x = (c (#) (max- f)) . x
by A7;
:: thesis: verum
end;
hence
max+ ((- c) (#) f) = c (#) (max- f)
by A4, PARTFUN1:34; :: thesis: max- ((- c) (#) f) = c (#) (max+ f)
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;
:: thesis: ( x in dom (max- ((- c) (#) f)) implies (max- ((- c) (#) f)) . x = (c (#) (max+ f)) . x )
assume A8:
x in dom (max- ((- c) (#) f))
;
:: thesis: (max- ((- c) (#) f)) . x = (c (#) (max+ f)) . x
then A9:
(max- ((- c) (#) f)) . x =
max (- (((- c) (#) f) . x)),
0
by MESFUNC2:def 3
.=
max (- ((R_EAL (- c)) * (f . x))),
0
by A2, A8, MESFUNC1:def 6
.=
max ((- (- (R_EAL c))) * (f . x)),
0
by A5, XXREAL_3:103
;
(c (#) (max+ f)) . x =
(R_EAL c) * ((max+ f) . x)
by A4, A8, MESFUNC1:def 6
.=
(R_EAL c) * (max (f . x),(R_EAL 0 ))
by A3, A8, MESFUNC2:def 2
.=
max ((R_EAL c) * (f . x)),
(c * 0 )
by A1, Th11
;
hence
(max- ((- c) (#) f)) . x = (c (#) (max+ f)) . x
by A9;
:: thesis: verum
end;
hence
max- ((- c) (#) f) = c (#) (max+ f)
by A4, PARTFUN1:34; :: thesis: verum