let X1, X2 be non empty set ; for x being Element of X1
for y being Element of X2
for f1, f2 being PartFunc of [:X1,X2:],ExtREAL holds
( ProjPMap1 ((f1 + f2),x) = (ProjPMap1 (f1,x)) + (ProjPMap1 (f2,x)) & ProjPMap1 ((f1 - f2),x) = (ProjPMap1 (f1,x)) - (ProjPMap1 (f2,x)) & ProjPMap2 ((f1 + f2),y) = (ProjPMap2 (f1,y)) + (ProjPMap2 (f2,y)) & ProjPMap2 ((f1 - f2),y) = (ProjPMap2 (f1,y)) - (ProjPMap2 (f2,y)) )
let x be Element of X1; for y being Element of X2
for f1, f2 being PartFunc of [:X1,X2:],ExtREAL holds
( ProjPMap1 ((f1 + f2),x) = (ProjPMap1 (f1,x)) + (ProjPMap1 (f2,x)) & ProjPMap1 ((f1 - f2),x) = (ProjPMap1 (f1,x)) - (ProjPMap1 (f2,x)) & ProjPMap2 ((f1 + f2),y) = (ProjPMap2 (f1,y)) + (ProjPMap2 (f2,y)) & ProjPMap2 ((f1 - f2),y) = (ProjPMap2 (f1,y)) - (ProjPMap2 (f2,y)) )
let y be Element of X2; for f1, f2 being PartFunc of [:X1,X2:],ExtREAL holds
( ProjPMap1 ((f1 + f2),x) = (ProjPMap1 (f1,x)) + (ProjPMap1 (f2,x)) & ProjPMap1 ((f1 - f2),x) = (ProjPMap1 (f1,x)) - (ProjPMap1 (f2,x)) & ProjPMap2 ((f1 + f2),y) = (ProjPMap2 (f1,y)) + (ProjPMap2 (f2,y)) & ProjPMap2 ((f1 - f2),y) = (ProjPMap2 (f1,y)) - (ProjPMap2 (f2,y)) )
let f1, f2 be PartFunc of [:X1,X2:],ExtREAL; ( ProjPMap1 ((f1 + f2),x) = (ProjPMap1 (f1,x)) + (ProjPMap1 (f2,x)) & ProjPMap1 ((f1 - f2),x) = (ProjPMap1 (f1,x)) - (ProjPMap1 (f2,x)) & ProjPMap2 ((f1 + f2),y) = (ProjPMap2 (f1,y)) + (ProjPMap2 (f2,y)) & ProjPMap2 ((f1 - f2),y) = (ProjPMap2 (f1,y)) - (ProjPMap2 (f2,y)) )
A1:
dom (f1 + f2) = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty})))
by MESFUNC1:def 3;
B1:
dom (f1 - f2) = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty})))
by MESFUNC1:def 4;
A2:
( dom (ProjPMap1 (f1,x)) = X-section ((dom f1),x) & dom (ProjPMap1 (f2,x)) = X-section ((dom f2),x) & dom (ProjPMap2 (f1,y)) = Y-section ((dom f1),y) & dom (ProjPMap2 (f2,y)) = Y-section ((dom f2),y) )
by Def3, Def4;
A3:
( X-section ((f1 " {-infty}),x) = (ProjPMap1 (f1,x)) " {-infty} & X-section ((f1 " {+infty}),x) = (ProjPMap1 (f1,x)) " {+infty} & X-section ((f2 " {-infty}),x) = (ProjPMap1 (f2,x)) " {-infty} & X-section ((f2 " {+infty}),x) = (ProjPMap1 (f2,x)) " {+infty} & Y-section ((f1 " {-infty}),y) = (ProjPMap2 (f1,y)) " {-infty} & Y-section ((f1 " {+infty}),y) = (ProjPMap2 (f1,y)) " {+infty} & Y-section ((f2 " {-infty}),y) = (ProjPMap2 (f2,y)) " {-infty} & Y-section ((f2 " {+infty}),y) = (ProjPMap2 (f2,y)) " {+infty} )
by Th42, Th41;
A4: dom (ProjPMap1 ((f1 + f2),x)) =
X-section ((dom (f1 + f2)),x)
by Def3
.=
(X-section (((dom f1) /\ (dom f2)),x)) \ (X-section ((((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))),x))
by A1, Th43
.=
((X-section ((dom f1),x)) /\ (X-section ((dom f2),x))) \ (X-section ((((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))),x))
by MEASUR11:27
.=
((dom (ProjPMap1 (f1,x))) /\ (dom (ProjPMap1 (f2,x)))) \ ((X-section (((f1 " {-infty}) /\ (f2 " {+infty})),x)) \/ (X-section (((f1 " {+infty}) /\ (f2 " {-infty})),x)))
by A2, MEASUR11:26
;
then A5: dom (ProjPMap1 ((f1 + f2),x)) =
((dom (ProjPMap1 (f1,x))) /\ (dom (ProjPMap1 (f2,x)))) \ (((X-section ((f1 " {-infty}),x)) /\ (X-section ((f2 " {+infty}),x))) \/ (X-section (((f1 " {+infty}) /\ (f2 " {-infty})),x)))
by MEASUR11:27
.=
((dom (ProjPMap1 (f1,x))) /\ (dom (ProjPMap1 (f2,x)))) \ ((((ProjPMap1 (f1,x)) " {-infty}) /\ ((ProjPMap1 (f2,x)) " {+infty})) \/ ((X-section ((f1 " {+infty}),x)) /\ (X-section ((f2 " {-infty}),x))))
by A3, MEASUR11:27
.=
dom ((ProjPMap1 (f1,x)) + (ProjPMap1 (f2,x)))
by A3, MESFUNC1:def 3
;
for y being Element of X2 st y in dom (ProjPMap1 ((f1 + f2),x)) holds
(ProjPMap1 ((f1 + f2),x)) . y = ((ProjPMap1 (f1,x)) + (ProjPMap1 (f2,x))) . y
proof
let y be
Element of
X2;
( y in dom (ProjPMap1 ((f1 + f2),x)) implies (ProjPMap1 ((f1 + f2),x)) . y = ((ProjPMap1 (f1,x)) + (ProjPMap1 (f2,x))) . y )
assume A6:
y in dom (ProjPMap1 ((f1 + f2),x))
;
(ProjPMap1 ((f1 + f2),x)) . y = ((ProjPMap1 (f1,x)) + (ProjPMap1 (f2,x))) . y
reconsider z =
[x,y] as
Element of
[:X1,X2:] by ZFMISC_1:def 2;
A7:
(ProjPMap1 ((f1 + f2),x)) . y = (f1 + f2) . (
x,
y)
by A6, Th26;
then
[x,y] in dom (f1 + f2)
by A6, Th40;
then A8:
(ProjPMap1 ((f1 + f2),x)) . y = (f1 . z) + (f2 . z)
by A7, MESFUNC1:def 3;
y in (dom (ProjPMap1 (f1,x))) /\ (dom (ProjPMap1 (f2,x)))
by A4, A6, XBOOLE_0:def 5;
then
(
y in dom (ProjPMap1 (f1,x)) &
y in dom (ProjPMap1 (f2,x)) )
by XBOOLE_0:def 4;
then
(
(ProjPMap1 (f1,x)) . y = f1 . (
x,
y) &
(ProjPMap1 (f2,x)) . y = f2 . (
x,
y) )
by Th26;
hence
(ProjPMap1 ((f1 + f2),x)) . y = ((ProjPMap1 (f1,x)) + (ProjPMap1 (f2,x))) . y
by A8, A5, A6, MESFUNC1:def 3;
verum
end;
hence
ProjPMap1 ((f1 + f2),x) = (ProjPMap1 (f1,x)) + (ProjPMap1 (f2,x))
by A5, PARTFUN1:5; ( ProjPMap1 ((f1 - f2),x) = (ProjPMap1 (f1,x)) - (ProjPMap1 (f2,x)) & ProjPMap2 ((f1 + f2),y) = (ProjPMap2 (f1,y)) + (ProjPMap2 (f2,y)) & ProjPMap2 ((f1 - f2),y) = (ProjPMap2 (f1,y)) - (ProjPMap2 (f2,y)) )
B4: dom (ProjPMap1 ((f1 - f2),x)) =
X-section ((dom (f1 - f2)),x)
by Def3
.=
(X-section (((dom f1) /\ (dom f2)),x)) \ (X-section ((((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))),x))
by B1, Th43
.=
((X-section ((dom f1),x)) /\ (X-section ((dom f2),x))) \ (X-section ((((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))),x))
by MEASUR11:27
.=
((dom (ProjPMap1 (f1,x))) /\ (dom (ProjPMap1 (f2,x)))) \ ((X-section (((f1 " {+infty}) /\ (f2 " {+infty})),x)) \/ (X-section (((f1 " {-infty}) /\ (f2 " {-infty})),x)))
by A2, MEASUR11:26
;
then B5: dom (ProjPMap1 ((f1 - f2),x)) =
((dom (ProjPMap1 (f1,x))) /\ (dom (ProjPMap1 (f2,x)))) \ (((X-section ((f1 " {+infty}),x)) /\ (X-section ((f2 " {+infty}),x))) \/ (X-section (((f1 " {-infty}) /\ (f2 " {-infty})),x)))
by MEASUR11:27
.=
((dom (ProjPMap1 (f1,x))) /\ (dom (ProjPMap1 (f2,x)))) \ ((((ProjPMap1 (f1,x)) " {+infty}) /\ ((ProjPMap1 (f2,x)) " {+infty})) \/ ((X-section ((f1 " {-infty}),x)) /\ (X-section ((f2 " {-infty}),x))))
by A3, MEASUR11:27
.=
dom ((ProjPMap1 (f1,x)) - (ProjPMap1 (f2,x)))
by A3, MESFUNC1:def 4
;
for y being Element of X2 st y in dom (ProjPMap1 ((f1 - f2),x)) holds
(ProjPMap1 ((f1 - f2),x)) . y = ((ProjPMap1 (f1,x)) - (ProjPMap1 (f2,x))) . y
proof
let y be
Element of
X2;
( y in dom (ProjPMap1 ((f1 - f2),x)) implies (ProjPMap1 ((f1 - f2),x)) . y = ((ProjPMap1 (f1,x)) - (ProjPMap1 (f2,x))) . y )
assume A6:
y in dom (ProjPMap1 ((f1 - f2),x))
;
(ProjPMap1 ((f1 - f2),x)) . y = ((ProjPMap1 (f1,x)) - (ProjPMap1 (f2,x))) . y
reconsider z =
[x,y] as
Element of
[:X1,X2:] by ZFMISC_1:def 2;
A7:
(ProjPMap1 ((f1 - f2),x)) . y = (f1 - f2) . (
x,
y)
by A6, Th26;
then
[x,y] in dom (f1 - f2)
by A6, Th40;
then A8:
(ProjPMap1 ((f1 - f2),x)) . y = (f1 . z) - (f2 . z)
by A7, MESFUNC1:def 4;
y in (dom (ProjPMap1 (f1,x))) /\ (dom (ProjPMap1 (f2,x)))
by B4, A6, XBOOLE_0:def 5;
then
(
y in dom (ProjPMap1 (f1,x)) &
y in dom (ProjPMap1 (f2,x)) )
by XBOOLE_0:def 4;
then
(
(ProjPMap1 (f1,x)) . y = f1 . (
x,
y) &
(ProjPMap1 (f2,x)) . y = f2 . (
x,
y) )
by Th26;
hence
(ProjPMap1 ((f1 - f2),x)) . y = ((ProjPMap1 (f1,x)) - (ProjPMap1 (f2,x))) . y
by A8, B5, A6, MESFUNC1:def 4;
verum
end;
hence
ProjPMap1 ((f1 - f2),x) = (ProjPMap1 (f1,x)) - (ProjPMap1 (f2,x))
by B5, PARTFUN1:5; ( ProjPMap2 ((f1 + f2),y) = (ProjPMap2 (f1,y)) + (ProjPMap2 (f2,y)) & ProjPMap2 ((f1 - f2),y) = (ProjPMap2 (f1,y)) - (ProjPMap2 (f2,y)) )
C4: dom (ProjPMap2 ((f1 + f2),y)) =
Y-section ((dom (f1 + f2)),y)
by Def4
.=
(Y-section (((dom f1) /\ (dom f2)),y)) \ (Y-section ((((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))),y))
by A1, Th43
.=
((Y-section ((dom f1),y)) /\ (Y-section ((dom f2),y))) \ (Y-section ((((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))),y))
by MEASUR11:27
.=
((dom (ProjPMap2 (f1,y))) /\ (dom (ProjPMap2 (f2,y)))) \ ((Y-section (((f1 " {-infty}) /\ (f2 " {+infty})),y)) \/ (Y-section (((f1 " {+infty}) /\ (f2 " {-infty})),y)))
by A2, MEASUR11:26
;
then C5: dom (ProjPMap2 ((f1 + f2),y)) =
((dom (ProjPMap2 (f1,y))) /\ (dom (ProjPMap2 (f2,y)))) \ (((Y-section ((f1 " {-infty}),y)) /\ (Y-section ((f2 " {+infty}),y))) \/ (Y-section (((f1 " {+infty}) /\ (f2 " {-infty})),y)))
by MEASUR11:27
.=
((dom (ProjPMap2 (f1,y))) /\ (dom (ProjPMap2 (f2,y)))) \ ((((ProjPMap2 (f1,y)) " {-infty}) /\ ((ProjPMap2 (f2,y)) " {+infty})) \/ ((Y-section ((f1 " {+infty}),y)) /\ (Y-section ((f2 " {-infty}),y))))
by A3, MEASUR11:27
.=
dom ((ProjPMap2 (f1,y)) + (ProjPMap2 (f2,y)))
by A3, MESFUNC1:def 3
;
for x being Element of X1 st x in dom (ProjPMap2 ((f1 + f2),y)) holds
(ProjPMap2 ((f1 + f2),y)) . x = ((ProjPMap2 (f1,y)) + (ProjPMap2 (f2,y))) . x
proof
let x be
Element of
X1;
( x in dom (ProjPMap2 ((f1 + f2),y)) implies (ProjPMap2 ((f1 + f2),y)) . x = ((ProjPMap2 (f1,y)) + (ProjPMap2 (f2,y))) . x )
assume C6:
x in dom (ProjPMap2 ((f1 + f2),y))
;
(ProjPMap2 ((f1 + f2),y)) . x = ((ProjPMap2 (f1,y)) + (ProjPMap2 (f2,y))) . x
reconsider z =
[x,y] as
Element of
[:X1,X2:] by ZFMISC_1:def 2;
C7:
(ProjPMap2 ((f1 + f2),y)) . x = (f1 + f2) . (
x,
y)
by C6, Th26;
then
[x,y] in dom (f1 + f2)
by C6, Th40;
then C8:
(ProjPMap2 ((f1 + f2),y)) . x = (f1 . z) + (f2 . z)
by C7, MESFUNC1:def 3;
x in (dom (ProjPMap2 (f1,y))) /\ (dom (ProjPMap2 (f2,y)))
by C4, C6, XBOOLE_0:def 5;
then
(
x in dom (ProjPMap2 (f1,y)) &
x in dom (ProjPMap2 (f2,y)) )
by XBOOLE_0:def 4;
then
(
(ProjPMap2 (f1,y)) . x = f1 . (
x,
y) &
(ProjPMap2 (f2,y)) . x = f2 . (
x,
y) )
by Th26;
hence
(ProjPMap2 ((f1 + f2),y)) . x = ((ProjPMap2 (f1,y)) + (ProjPMap2 (f2,y))) . x
by C8, C5, C6, MESFUNC1:def 3;
verum
end;
hence
ProjPMap2 ((f1 + f2),y) = (ProjPMap2 (f1,y)) + (ProjPMap2 (f2,y))
by C5, PARTFUN1:5; ProjPMap2 ((f1 - f2),y) = (ProjPMap2 (f1,y)) - (ProjPMap2 (f2,y))
D4: dom (ProjPMap2 ((f1 - f2),y)) =
Y-section ((dom (f1 - f2)),y)
by Def4
.=
(Y-section (((dom f1) /\ (dom f2)),y)) \ (Y-section ((((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))),y))
by B1, Th43
.=
((Y-section ((dom f1),y)) /\ (Y-section ((dom f2),y))) \ (Y-section ((((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))),y))
by MEASUR11:27
.=
((dom (ProjPMap2 (f1,y))) /\ (dom (ProjPMap2 (f2,y)))) \ ((Y-section (((f1 " {+infty}) /\ (f2 " {+infty})),y)) \/ (Y-section (((f1 " {-infty}) /\ (f2 " {-infty})),y)))
by A2, MEASUR11:26
;
then D5: dom (ProjPMap2 ((f1 - f2),y)) =
((dom (ProjPMap2 (f1,y))) /\ (dom (ProjPMap2 (f2,y)))) \ (((Y-section ((f1 " {+infty}),y)) /\ (Y-section ((f2 " {+infty}),y))) \/ (Y-section (((f1 " {-infty}) /\ (f2 " {-infty})),y)))
by MEASUR11:27
.=
((dom (ProjPMap2 (f1,y))) /\ (dom (ProjPMap2 (f2,y)))) \ ((((ProjPMap2 (f1,y)) " {+infty}) /\ ((ProjPMap2 (f2,y)) " {+infty})) \/ ((Y-section ((f1 " {-infty}),y)) /\ (Y-section ((f2 " {-infty}),y))))
by A3, MEASUR11:27
.=
dom ((ProjPMap2 (f1,y)) - (ProjPMap2 (f2,y)))
by A3, MESFUNC1:def 4
;
for x being Element of X1 st x in dom (ProjPMap2 ((f1 - f2),y)) holds
(ProjPMap2 ((f1 - f2),y)) . x = ((ProjPMap2 (f1,y)) - (ProjPMap2 (f2,y))) . x
proof
let x be
Element of
X1;
( x in dom (ProjPMap2 ((f1 - f2),y)) implies (ProjPMap2 ((f1 - f2),y)) . x = ((ProjPMap2 (f1,y)) - (ProjPMap2 (f2,y))) . x )
assume D6:
x in dom (ProjPMap2 ((f1 - f2),y))
;
(ProjPMap2 ((f1 - f2),y)) . x = ((ProjPMap2 (f1,y)) - (ProjPMap2 (f2,y))) . x
reconsider z =
[x,y] as
Element of
[:X1,X2:] by ZFMISC_1:def 2;
D7:
(ProjPMap2 ((f1 - f2),y)) . x = (f1 - f2) . (
x,
y)
by D6, Th26;
then
[x,y] in dom (f1 - f2)
by D6, Th40;
then D8:
(ProjPMap2 ((f1 - f2),y)) . x = (f1 . z) - (f2 . z)
by D7, MESFUNC1:def 4;
x in (dom (ProjPMap2 (f1,y))) /\ (dom (ProjPMap2 (f2,y)))
by D4, D6, XBOOLE_0:def 5;
then
(
x in dom (ProjPMap2 (f1,y)) &
x in dom (ProjPMap2 (f2,y)) )
by XBOOLE_0:def 4;
then
(
(ProjPMap2 (f1,y)) . x = f1 . (
x,
y) &
(ProjPMap2 (f2,y)) . x = f2 . (
x,
y) )
by Th26;
hence
(ProjPMap2 ((f1 - f2),y)) . x = ((ProjPMap2 (f1,y)) - (ProjPMap2 (f2,y))) . x
by D8, D5, D6, MESFUNC1:def 4;
verum
end;
hence
ProjPMap2 ((f1 - f2),y) = (ProjPMap2 (f1,y)) - (ProjPMap2 (f2,y))
by D5, PARTFUN1:5; verum