let X be non empty set ; :: thesis: for f, g being PartFunc of X,REAL holds ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)
let f, g be PartFunc of X,REAL; :: thesis: ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)
A1: dom (max+ (f + g)) = dom (f + g) by RFUNCT_3:def 10;
A2: dom (max+ g) = dom g by RFUNCT_3:def 10;
A3: dom (max+ f) = dom f by RFUNCT_3:def 10;
A4: dom (max- f) = dom f by RFUNCT_3:def 11;
A5: dom (max- g) = dom g by RFUNCT_3:def 11;
A6: dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom ((max+ (f + g)) + (max- f))) /\ (dom (max- g)) by VALUED_1:def 1
.= ((dom (f + g)) /\ (dom f)) /\ (dom g) by A1, A4, A5, VALUED_1:def 1 ;
then A7: dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom (f + g)) /\ ((dom f) /\ (dom g)) by XBOOLE_1:16;
A8: dom (max- (f + g)) = dom (f + g) by RFUNCT_3:def 11;
A9: for x being object st x in dom (((max+ (f + g)) + (max- f)) + (max- g)) holds
(((max+ (f + g)) + (max- f)) + (max- g)) . x = (((max- (f + g)) + (max+ f)) + (max+ g)) . x
proof
let x be object ; :: thesis: ( x in dom (((max+ (f + g)) + (max- f)) + (max- g)) implies (((max+ (f + g)) + (max- f)) + (max- g)) . x = (((max- (f + g)) + (max+ f)) + (max+ g)) . x )
assume A10: x in dom (((max+ (f + g)) + (max- f)) + (max- g)) ; :: thesis: (((max+ (f + g)) + (max- f)) + (max- g)) . x = (((max- (f + g)) + (max+ f)) + (max+ g)) . x
then A11: x in dom g by A6, XBOOLE_0:def 4;
then A12: (max+ g) . x = max+ (g . x) by A2, RFUNCT_3:def 10;
A13: (max- g) . x = max- (g . x) by A5, A11, RFUNCT_3:def 11;
A14: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
then A15: (max+ (f + g)) . x = max+ ((f + g) . x) by A1, A7, A10, RFUNCT_3:def 10
.= max (((f . x) + (g . x)),0) by A7, A10, A14, VALUED_1:def 1 ;
A16: x in dom f by A7, A10, A14, XBOOLE_0:def 4;
then A17: (max+ f) . x = max+ (f . x) by A3, RFUNCT_3:def 10;
A18: (max- (f + g)) . x = max- ((f + g) . x) by A8, A7, A10, A14, RFUNCT_3:def 11
.= max ((- ((f . x) + (g . x))),0) by A7, A10, A14, VALUED_1:def 1 ;
A19: (max- f) . x = max- (f . x) by A4, A16, RFUNCT_3:def 11;
A20: now :: thesis: ( 0 <= f . x implies (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) )
assume A21: 0 <= f . x ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then A22: (max- f) . x = 0 by A19, XXREAL_0:def 10;
A23: now :: thesis: ( g . x < 0 implies (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) )
assume A24: g . x < 0 ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then A25: (max- g) . x = - (g . x) by A13, XXREAL_0:def 10;
A26: (max+ g) . x = 0 by A12, A24, XXREAL_0:def 10;
A27: now :: thesis: ( (f . x) + (g . x) < 0 implies (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) )
assume A28: (f . x) + (g . x) < 0 ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then (max- (f + g)) . x = - ((f . x) + (g . x)) by A18, XXREAL_0:def 10;
then (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((- ((f . x) + (g . x))) + (f . x)) + 0 by A17, A21, A26, XXREAL_0:def 10;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A15, A22, A25, A28, XXREAL_0:def 10; :: thesis: verum
end;
now :: thesis: ( 0 <= (f . x) + (g . x) implies (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) )
assume 0 <= (f . x) + (g . x) ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then ( (max- (f + g)) . x = 0 & (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((f . x) + (g . x)) + 0) + (- (g . x)) ) by A15, A18, A22, A25, XXREAL_0:def 10;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A17, A21, A26, XXREAL_0:def 10; :: thesis: verum
end;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A27; :: thesis: verum
end;
now :: thesis: ( 0 <= g . x implies (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) )
assume A29: 0 <= g . x ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then (max- g) . x = 0 by A13, XXREAL_0:def 10;
then A30: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (f . x) + (g . x) by A15, A21, A22, A29, XXREAL_0:def 10;
( (max- (f + g)) . x = 0 & (max+ g) . x = g . x ) by A18, A12, A21, A29, XXREAL_0:def 10;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A17, A21, A30, XXREAL_0:def 10; :: thesis: verum
end;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A23; :: thesis: verum
end;
A31: now :: thesis: ( f . x < 0 implies (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) )
assume A32: f . x < 0 ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then A33: (max- f) . x = - (f . x) by A19, XXREAL_0:def 10;
A34: now :: thesis: ( 0 <= g . x implies (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) )
assume A35: 0 <= g . x ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then A36: (max- g) . x = 0 by A13, XXREAL_0:def 10;
A37: (max+ g) . x = g . x by A12, A35, XXREAL_0:def 10;
A38: now :: thesis: ( (f . x) + (g . x) < 0 implies (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) )
assume A39: (f . x) + (g . x) < 0 ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then (max- (f + g)) . x = - ((f . x) + (g . x)) by A18, XXREAL_0:def 10;
then (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((- ((f . x) + (g . x))) + 0) + (g . x) by A17, A32, A37, XXREAL_0:def 10
.= (- (f . x)) + ((- (g . x)) + (g . x)) ;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A15, A33, A36, A39, XXREAL_0:def 10; :: thesis: verum
end;
now :: thesis: ( 0 <= (f . x) + (g . x) implies (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) )
assume 0 <= (f . x) + (g . x) ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then ( (max- (f + g)) . x = 0 & (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((f . x) + (g . x)) + (- (f . x))) + 0 ) by A15, A18, A33, A36, XXREAL_0:def 10;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A17, A32, A37, XXREAL_0:def 10; :: thesis: verum
end;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A38; :: thesis: verum
end;
now :: thesis: ( g . x < 0 implies (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) )
assume A40: g . x < 0 ; :: thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
then ( (max- (f + g)) . x = - ((f . x) + (g . x)) & (max+ g) . x = 0 ) by A18, A12, A32, XXREAL_0:def 10;
then A41: (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((- ((f . x) + (g . x))) + 0) + 0 by A17, A32, XXREAL_0:def 10;
(max- g) . x = - (g . x) by A13, A40, XXREAL_0:def 10;
then (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (0 + (- (f . x))) + (- (g . x)) by A15, A32, A33, A40, XXREAL_0:def 10;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A41; :: thesis: verum
end;
hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A34; :: thesis: verum
end;
x in (dom f) /\ (dom g) by A10, Th62;
then x in dom (((max- (f + g)) + (max+ f)) + (max+ g)) by Th62;
then (((max- (f + g)) + (max+ f)) + (max+ g)) . x = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by Th60;
hence (((max+ (f + g)) + (max- f)) + (max- g)) . x = (((max- (f + g)) + (max+ f)) + (max+ g)) . x by A10, A20, A31, Th60; :: thesis: verum
end;
dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) by Th62;
then dom (((max+ (f + g)) + (max- f)) + (max- g)) = dom (((max- (f + g)) + (max+ f)) + (max+ g)) by Th62;
hence ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g) by A9, FUNCT_1:2; :: thesis: verum