let X be non empty set ; 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; ((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 ;
( 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))
;
(((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 ( 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
;
(((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;
now ( 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
;
(((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;
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;
verum end;
A31:
now ( 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
;
(((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;
now ( 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
;
(((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;
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;
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;
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; verum