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)
by MESFUNC2:def 2
.=
dom f
by MESFUNC1:def 6
.=
dom (max+ f)
by MESFUNC2:def 2
.=
dom (c (#) (max+ f))
by MESFUNC1:def 6
;
A3: dom (max- (c (#) f)) =
dom (c (#) f)
by MESFUNC2:def 3
.=
dom f
by MESFUNC1:def 6
.=
dom (max- f)
by MESFUNC2:def 3
.=
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;
:: thesis: ( x in dom (max+ (c (#) f)) implies (max+ (c (#) f)) . x = (c (#) (max+ f)) . x )
assume A4:
x in dom (max+ (c (#) f))
;
:: thesis: (max+ (c (#) f)) . x = (c (#) (max+ f)) . x
then A5:
x in dom (c (#) f)
by MESFUNC2:def 2;
then
x in dom f
by MESFUNC1:def 6;
then A6:
x in dom (max+ f)
by MESFUNC2:def 2;
A7:
(max+ (c (#) f)) . x =
max ((c (#) f) . x),
0
by A4, MESFUNC2:def 2
.=
max ((R_EAL c) * (f . x)),
0
by A5, MESFUNC1:def 6
;
(c (#) (max+ f)) . x =
(R_EAL c) * ((max+ f) . x)
by A2, A4, MESFUNC1:def 6
.=
c * (max (f . x),0 )
by A6, MESFUNC2:def 2
.=
max (c * (f . x)),
(c * 0 )
by A1, Th11
;
hence
(max+ (c (#) f)) . x = (c (#) (max+ f)) . x
by A7;
:: thesis: verum
end;
hence
max+ (c (#) f) = c (#) (max+ f)
by A2, 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:
x in dom (c (#) f)
by MESFUNC2:def 3;
then
x in dom f
by MESFUNC1:def 6;
then A10:
x in dom (max- f)
by MESFUNC2:def 3;
A11:
(max- (c (#) f)) . x =
max (- ((c (#) f) . x)),
0
by A8, MESFUNC2:def 3
.=
max (- ((R_EAL c) * (f . x))),
0
by A9, MESFUNC1:def 6
;
(c (#) (max- f)) . x =
(R_EAL c) * ((max- f) . x)
by A3, A8, MESFUNC1:def 6
.=
c * (max (- (f . x)),0 )
by A10, MESFUNC2:def 3
.=
max (c * (- (f . x))),
(c * 0 )
by A1, Th11
.=
max (- (c * (f . x))),
(c * 0 )
by XXREAL_3:103
;
hence
(max- (c (#) f)) . x = (c (#) (max- f)) . x
by A11;
:: thesis: verum
end;
hence
max- (c (#) f) = c (#) (max- f)
by A3, PARTFUN1:34; :: thesis: verum