let X be non empty set ; for f, g being PartFunc of X,ExtREAL st f is () & f is () & g is () & g is () holds
((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)
let f, g be PartFunc of X,ExtREAL; ( f is () & f is () & g is () & g is () implies ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g) )
assume that
A1:
f is ()
and
A2:
f is ()
and
A3:
g is ()
and
A4:
g is ()
; ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)
A5:
dom (max- (f + g)) = dom (f + g)
by MESFUNC2:def 3;
for x being object st x in dom (max- g) holds
0 <= (max- g) . x
by MESFUNC2:13;
then A6:
max- g is nonnegative
by SUPINF_2:52;
for x being object st x in dom (max+ g) holds
0 <= (max+ g) . x
by MESFUNC2:12;
then A7:
max+ g is nonnegative
by SUPINF_2:52;
A8:
dom (max- f) = dom f
by MESFUNC2:def 3;
for x being object st x in dom (max+ (f + g)) holds
0 <= (max+ (f + g)) . x
by MESFUNC2:12;
then A9:
max+ (f + g) is nonnegative
by SUPINF_2:52;
for x being object st x in dom (max+ f) holds
0 <= (max+ f) . x
by MESFUNC2:12;
then A10:
max+ f is nonnegative
by SUPINF_2:52;
A11:
dom (max+ f) = dom f
by MESFUNC2:def 2;
A12:
dom (max+ g) = dom g
by MESFUNC2:def 2;
A13:
dom (max- g) = dom g
by MESFUNC2:def 3;
for x being object st x in dom (max- f) holds
0 <= (max- f) . x
by MESFUNC2:13;
then A14:
max- f is nonnegative
by SUPINF_2:52;
A15:
dom (max+ (f + g)) = dom (f + g)
by MESFUNC2:def 2;
then A16:
dom (((max+ (f + g)) + (max- f)) + (max- g)) = ((dom (f + g)) /\ (dom f)) /\ (dom g)
by A8, A13, A9, A14, A6, Th23;
then A17:
dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom (f + g)) /\ ((dom f) /\ (dom g))
by XBOOLE_1:16;
for x being object st x in dom (max- (f + g)) holds
0 <= (max- (f + g)) . x
by MESFUNC2:13;
then A18:
max- (f + g) is nonnegative
by SUPINF_2:52;
A19:
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 A20:
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 A21:
x in dom g
by A16, XBOOLE_0:def 4;
then A22:
(max+ g) . x = max (
(g . x),
0)
by A12, MESFUNC2:def 2;
A23:
g . x <> +infty
by A4;
A24:
dom (f + g) = (dom f) /\ (dom g)
by A1, A3, Th16;
then A25:
(max+ (f + g)) . x =
max (
((f + g) . x),
0)
by A15, A17, A20, MESFUNC2:def 2
.=
max (
((f . x) + (g . x)),
0)
by A17, A20, A24, MESFUNC1:def 3
;
A26:
x in dom f
by A17, A20, A24, XBOOLE_0:def 4;
then A27:
(max+ f) . x = max (
(f . x),
0)
by A11, MESFUNC2:def 2;
A28:
(max- (f + g)) . x =
max (
(- ((f + g) . x)),
0)
by A5, A17, A20, A24, MESFUNC2:def 3
.=
max (
(- ((f . x) + (g . x))),
0)
by A17, A20, A24, MESFUNC1:def 3
;
A29:
f . x <> -infty
by A1;
then A30:
- (f . x) <> +infty
by XXREAL_3:23;
A31:
f . x <> +infty
by A2;
A32:
(max- f) . x = max (
(- (f . x)),
0)
by A8, A26, MESFUNC2:def 3;
A33:
(max- g) . x = max (
(- (g . x)),
0)
by A13, A21, MESFUNC2:def 3;
A34:
g . x <> -infty
by A3;
then A35:
- (g . x) <> +infty
by XXREAL_3:23;
A36:
now (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)per cases
( 0 <= f . x or f . x < 0 )
;
suppose A37:
0 <= f . x
;
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)then A38:
(max- f) . x = 0
by A32, XXREAL_0:def 10;
per cases
( 0 <= g . x or g . x < 0 )
;
suppose A39:
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 A33, XXREAL_0:def 10;
then A40:
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) =
(((f . x) + (g . x)) + 0) + 0
by A25, A37, A38, A39, XXREAL_0:def 10
.=
((f . x) + (g . x)) + 0
by XXREAL_3:4
.=
(f . x) + (g . x)
by XXREAL_3:4
;
A41:
(max+ g) . x = g . x
by A22, A39, XXREAL_0:def 10;
(max- (f + g)) . x = 0
by A28, A37, A39, XXREAL_0:def 10;
then
(((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = (0 + (f . x)) + (g . x)
by A27, A37, A41, 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 A40, XXREAL_3:4;
verum end; suppose A42:
g . x < 0
;
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)then A43:
(max+ g) . x = 0
by A22, XXREAL_0:def 10;
A44:
(max- g) . x = - (g . x)
by A33, A42, XXREAL_0:def 10;
per cases
( 0 <= (f . x) + (g . x) or (f . x) + (g . x) < 0 )
;
suppose A45:
0 <= (f . x) + (g . x)
;
(((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
by A28, XXREAL_0:def 10;
then A46:
(((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = (0 + (f . x)) + 0
by A27, A37, A43, XXREAL_0:def 10;
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) =
(((f . x) + (g . x)) + 0) + (- (g . x))
by A25, A38, A44, A45, XXREAL_0:def 10
.=
((f . x) + (g . x)) - (g . x)
by XXREAL_3:4
.=
(f . x) + ((g . x) - (g . x))
by A23, A34, XXREAL_3:30
.=
(f . x) + 0
by XXREAL_3:7
;
hence
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
by A46, XXREAL_3:4;
verum end; suppose A47:
(f . x) + (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 = 0
by A25, XXREAL_0:def 10;
then
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (0 + 0) + (- (g . x))
by A38, A44;
then A48:
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = 0 + (- (g . x))
;
(max- (f + g)) . x = - ((f . x) + (g . x))
by A28, A47, XXREAL_0:def 10;
then (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) =
((- ((f . x) + (g . x))) + (f . x)) + 0
by A27, A37, A43, XXREAL_0:def 10
.=
(- ((f . x) + (g . x))) + (f . x)
by XXREAL_3:4
.=
((- (g . x)) - (f . x)) + (f . x)
by XXREAL_3:25
.=
(- (g . x)) + ((- (f . x)) + (f . x))
by A31, A30, A35, XXREAL_3:29
;
hence
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
by A48, XXREAL_3:7;
verum end; end; end; suppose A49:
f . x < 0
;
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)then A50:
(max- f) . x = - (f . x)
by A32, XXREAL_0:def 10;
per cases
( 0 <= g . x or g . x < 0 )
;
suppose A51:
0 <= g . x
;
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)then A52:
(max+ g) . x = g . x
by A22, XXREAL_0:def 10;
A53:
(max- g) . x = 0
by A33, A51, XXREAL_0:def 10;
per cases
( 0 <= (f . x) + (g . x) or (f . x) + (g . x) < 0 )
;
suppose A54:
0 <= (f . x) + (g . x)
;
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)then A55:
(max- (f + g)) . x = 0
by A28, XXREAL_0:def 10;
(max+ f) . x = 0
by A27, A49, XXREAL_0:def 10;
then A56:
(((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = (0 + 0) + (g . x)
by A52, A55;
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) =
(((f . x) + (g . x)) + (- (f . x))) + 0
by A25, A50, A53, A54, XXREAL_0:def 10
.=
((f . x) + (g . x)) + (- (f . x))
by XXREAL_3:4
.=
(g . x) + ((f . x) - (f . x))
by A31, A29, A23, A34, XXREAL_3:29
.=
(g . x) + 0
by XXREAL_3:7
;
hence
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
by A56;
verum end; suppose A57:
(f . x) + (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))
by A28, XXREAL_0:def 10;
then A58:
(((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) =
((- ((f . x) + (g . x))) + 0) + (g . x)
by A27, A49, A52, XXREAL_0:def 10
.=
(- ((f . x) + (g . x))) + (g . x)
by XXREAL_3:4
.=
((- (f . x)) - (g . x)) + (g . x)
by XXREAL_3:25
.=
(- (f . x)) + ((- (g . x)) + (g . x))
by A23, A30, A35, XXREAL_3:29
;
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) =
(0 + (- (f . x))) + 0
by A25, A50, A53, A57, XXREAL_0:def 10
.=
0 + (- (f . x))
by XXREAL_3:4
;
hence
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
by A58, XXREAL_3:7;
verum end; end; suppose A59:
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- g) . x = - (g . x)
by A33, XXREAL_0:def 10;
then A60:
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) =
(0 + (- (f . x))) + (- (g . x))
by A25, A49, A50, A59, XXREAL_0:def 10
.=
(- (f . x)) - (g . x)
by XXREAL_3:4
;
A61:
(max+ g) . x = 0
by A22, A59, XXREAL_0:def 10;
(max- (f + g)) . x = - ((f . x) + (g . x))
by A28, A49, A59, XXREAL_0:def 10;
then (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) =
((- ((f . x) + (g . x))) + 0) + 0
by A27, A49, A61, XXREAL_0:def 10
.=
(- ((f . x) + (g . x))) + 0
by XXREAL_3:4
.=
- ((f . x) + (g . x))
by XXREAL_3:4
;
hence
(((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
by A60, XXREAL_3:25;
verum end; end;
A62:
dom (((max+ (f + g)) + (max- f)) + (max- g)) = ((dom (max+ (f + g))) /\ (dom (max- f))) /\ (dom (max- g))
by A9, A14, A6, Th23;
(((max- (f + g)) + (max+ f)) + (max+ g)) . x = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x)
by A5, A11, A12, A18, A10, A7, A16, A20, Th23;
hence
(((max+ (f + g)) + (max- f)) + (max- g)) . x = (((max- (f + g)) + (max+ f)) + (max+ g)) . x
by A9, A14, A6, A20, A62, A36, Th23;
verum
end;
dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g)
by A1, A3, Th24;
then
dom (((max+ (f + g)) + (max- f)) + (max- g)) = dom (((max- (f + g)) + (max+ f)) + (max+ g))
by A1, A3, Th24;
hence
((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)
by A19, FUNCT_1:2; verum