let C be non empty set ; :: thesis: for f being PartFunc of C,ExtREAL
for c being Real st c <= 0 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 c <= 0 holds
( max+ (c (#) f) = (- c) (#) (max- f) & max- (c (#) f) = (- c) (#) (max+ f) )
let c be Real; :: thesis: ( c <= 0 implies ( max+ (c (#) f) = (- c) (#) (max- f) & max- (c (#) f) = (- c) (#) (max+ f) ) )
assume A1: c <= 0 ; :: 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 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 A3: x in dom (max+ (c (#) f)) ; :: thesis: (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x
then A4: x in dom (c (#) f) by MESFUNC2:def 2;
then x in dom f by MESFUNC1:def 6;
then A5: x in dom (max- f) by MESFUNC2:def 3;
A6: (max+ (c (#) f)) . x = max (((c (#) f) . x),0) by A3, MESFUNC2:def 2
.= max ((c * (f . x)),0) by A4, MESFUNC1:def 6 ;
B1: ((- c) (#) (max- f)) . x = (- c) * ((max- f) . x) by A2, A3, MESFUNC1:def 6
.= (- c) * (max ((- (f . x)),0)) by A5, MESFUNC2:def 3 ;
per cases ( f . x >= 0 or f . x < 0 ) ;
suppose f . x >= 0 ; :: thesis: (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x
then ( (max+ (c (#) f)) . x = 0 & max ((- (f . x)),0) = 0 ) by A1, A6, XXREAL_0:def 10;
hence (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x by B1; :: thesis: verum
end;
suppose D1: f . x < 0 ; :: thesis: (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x
then B2: ( (max+ (c (#) f)) . x = c * (f . x) & max ((- (f . x)),0) = - (f . x) ) by A1, A6, XXREAL_0:def 10;
per cases ( f . x = -infty or f . x in REAL ) by D1, XXREAL_0:14;
suppose E1: f . x = -infty ; :: thesis: (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x
per cases ( c = 0 or c < 0 ) by A1;
suppose c = 0 ; :: thesis: (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x
then ( (max+ (c (#) f)) . x = 0 & ((- c) (#) (max- f)) . x = 0 ) by B1, A6, XXREAL_0:def 10;
hence (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x ; :: thesis: verum
end;
suppose F1: c < 0 ; :: thesis: (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x
then (- c) * (- (f . x)) = +infty by E1, XXREAL_3:5, XXREAL_3:def 5;
hence (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x by B1, B2, E1, F1, XXREAL_3:def 5; :: thesis: verum
end;
end;
end;
suppose f . x in REAL ; :: thesis: (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x
then reconsider a = f . x as Real ;
(- c) * (- a) = (- c) * (- (f . x)) ;
then (- c) * (- (f . x)) = c * a
.= c * (f . x) ;
hence (max+ (c (#) f)) . x = ((- c) (#) (max- f)) . x by B1, B2; :: thesis: verum
end;
end;
end;
end;
end;
hence max+ (c (#) f) = (- c) (#) (max- f) by A2, PARTFUN1:5; :: thesis: max- (c (#) f) = (- c) (#) (max+ f)
A7: dom (max- (c (#) f)) = dom (c (#) f) by MESFUNC2:def 3
.= dom f by MESFUNC1:def 6
.= dom (max+ f) by MESFUNC2:def 2
.= 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 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 2;
A11: (max- (c (#) f)) . x = max ((- ((c (#) f) . x)),0) by A8, MESFUNC2:def 3
.= max ((- (c * (f . x))),0) by A9, MESFUNC1:def 6 ;
A12: ((- c) (#) (max+ f)) . x = (- c) * ((max+ f) . x) by A7, A8, MESFUNC1:def 6
.= (- c) * (max ((f . x),0)) by A10, MESFUNC2:def 2
.= max (((- c) * (f . x)),((- c) * 0)) by A1, MESFUNC5:6
.= max (((- c) * (f . x)),0) ;
- (c * (f . x)) = (- c) * (f . x)
proof
per cases ( f . x = +infty or f . x = -infty or f . x in REAL ) by XXREAL_0:14;
suppose E1: f . x = +infty ; :: thesis: - (c * (f . x)) = (- c) * (f . x)
per cases ( c = 0 or c < 0 ) by A1;
suppose c = 0 ; :: thesis: - (c * (f . x)) = (- c) * (f . x)
then ( c * (f . x) = 0 & (- c) * (f . x) = 0 ) ;
hence - (c * (f . x)) = (- c) * (f . x) ; :: thesis: verum
end;
suppose E2: c < 0 ; :: thesis: - (c * (f . x)) = (- c) * (f . x)
then c * (f . x) = -infty by E1, XXREAL_3:def 5;
hence - (c * (f . x)) = (- c) * (f . x) by E1, E2, XXREAL_3:5, XXREAL_3:def 5; :: thesis: verum
end;
end;
end;
suppose E1: f . x = -infty ; :: thesis: - (c * (f . x)) = (- c) * (f . x)
per cases ( c = 0 or c < 0 ) by A1;
suppose c = 0 ; :: thesis: - (c * (f . x)) = (- c) * (f . x)
then ( c * (f . x) = 0 & (- c) * (f . x) = 0 ) ;
hence - (c * (f . x)) = (- c) * (f . x) ; :: thesis: verum
end;
suppose E2: c < 0 ; :: thesis: - (c * (f . x)) = (- c) * (f . x)
then c * (f . x) = +infty by E1, XXREAL_3:def 5;
hence - (c * (f . x)) = (- c) * (f . x) by E1, E2, XXREAL_3:6, XXREAL_3:def 5; :: thesis: verum
end;
end;
end;
suppose f . x in REAL ; :: thesis: - (c * (f . x)) = (- c) * (f . x)
then reconsider a = f . x as Real ;
(- c) * a = (- c) * (f . x) ;
then (- c) * (f . x) = - (c * a) ;
hence - (c * (f . x)) = (- c) * (f . x) ; :: thesis: verum
end;
end;
end;
hence (max- (c (#) f)) . x = ((- c) (#) (max+ f)) . x by A11, A12; :: thesis: verum
end;
hence max- (c (#) f) = (- c) (#) (max+ f) by A7, PARTFUN1:5; :: thesis: verum