let n, m be non empty Element of NAT ; :: thesis: for i being Element of NAT
for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds
( (f1 + f2) * (reproj i,x) = (f1 * (reproj i,x)) + (f2 * (reproj i,x)) & (f1 - f2) * (reproj i,x) = (f1 * (reproj i,x)) - (f2 * (reproj i,x)) )
let i be Element of NAT ; :: thesis: for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds
( (f1 + f2) * (reproj i,x) = (f1 * (reproj i,x)) + (f2 * (reproj i,x)) & (f1 - f2) * (reproj i,x) = (f1 * (reproj i,x)) - (f2 * (reproj i,x)) )
let f1, f2 be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: for x being Point of (REAL-NS m) holds
( (f1 + f2) * (reproj i,x) = (f1 * (reproj i,x)) + (f2 * (reproj i,x)) & (f1 - f2) * (reproj i,x) = (f1 * (reproj i,x)) - (f2 * (reproj i,x)) )
let x be Point of (REAL-NS m); :: thesis: ( (f1 + f2) * (reproj i,x) = (f1 * (reproj i,x)) + (f2 * (reproj i,x)) & (f1 - f2) * (reproj i,x) = (f1 * (reproj i,x)) - (f2 * (reproj i,x)) )
A1:
dom (f1 + f2) = (dom f1) /\ (dom f2)
by VFUNCT_1:def 1;
A2:
dom (f1 - f2) = (dom f1) /\ (dom f2)
by VFUNCT_1:def 2;
A3:
dom (reproj i,x) = the carrier of (REAL-NS 1)
by FUNCT_2:def 1;
A4:
for s being Element of (REAL-NS 1) holds
( s in dom ((f1 + f2) * (reproj i,x)) iff s in dom ((f1 * (reproj i,x)) + (f2 * (reproj i,x))) )
proof
let s be
Element of
(REAL-NS 1);
:: thesis: ( s in dom ((f1 + f2) * (reproj i,x)) iff s in dom ((f1 * (reproj i,x)) + (f2 * (reproj i,x))) )
(
s in dom ((f1 + f2) * (reproj i,x)) iff
(reproj i,x) . s in (dom f1) /\ (dom f2) )
by A1, A3, FUNCT_1:21;
then
(
s in dom ((f1 + f2) * (reproj i,x)) iff (
(reproj i,x) . s in dom f1 &
(reproj i,x) . s in dom f2 ) )
by XBOOLE_0:def 4;
then
(
s in dom ((f1 + f2) * (reproj i,x)) iff (
s in dom (f1 * (reproj i,x)) &
s in dom (f2 * (reproj i,x)) ) )
by A3, FUNCT_1:21;
then
(
s in dom ((f1 + f2) * (reproj i,x)) iff
s in (dom (f1 * (reproj i,x))) /\ (dom (f2 * (reproj i,x))) )
by XBOOLE_0:def 4;
hence
(
s in dom ((f1 + f2) * (reproj i,x)) iff
s in dom ((f1 * (reproj i,x)) + (f2 * (reproj i,x))) )
by VFUNCT_1:def 1;
:: thesis: verum
end;
A5:
for s being Element of (REAL-NS 1) holds
( s in dom ((f1 - f2) * (reproj i,x)) iff s in dom ((f1 * (reproj i,x)) - (f2 * (reproj i,x))) )
proof
let s be
Element of
(REAL-NS 1);
:: thesis: ( s in dom ((f1 - f2) * (reproj i,x)) iff s in dom ((f1 * (reproj i,x)) - (f2 * (reproj i,x))) )
(
s in dom ((f1 - f2) * (reproj i,x)) iff
(reproj i,x) . s in (dom f1) /\ (dom f2) )
by A2, A3, FUNCT_1:21;
then
(
s in dom ((f1 - f2) * (reproj i,x)) iff (
(reproj i,x) . s in dom f1 &
(reproj i,x) . s in dom f2 ) )
by XBOOLE_0:def 4;
then
(
s in dom ((f1 - f2) * (reproj i,x)) iff (
s in dom (f1 * (reproj i,x)) &
s in dom (f2 * (reproj i,x)) ) )
by A3, FUNCT_1:21;
then
(
s in dom ((f1 - f2) * (reproj i,x)) iff
s in (dom (f1 * (reproj i,x))) /\ (dom (f2 * (reproj i,x))) )
by XBOOLE_0:def 4;
hence
(
s in dom ((f1 - f2) * (reproj i,x)) iff
s in dom ((f1 * (reproj i,x)) - (f2 * (reproj i,x))) )
by VFUNCT_1:def 2;
:: thesis: verum
end;
for s being set holds
( s in dom ((f1 + f2) * (reproj i,x)) iff s in dom ((f1 * (reproj i,x)) + (f2 * (reproj i,x))) )
by A4;
then A6:
dom ((f1 + f2) * (reproj i,x)) = dom ((f1 * (reproj i,x)) + (f2 * (reproj i,x)))
by TARSKI:2;
for s being set holds
( s in dom ((f1 - f2) * (reproj i,x)) iff s in dom ((f1 * (reproj i,x)) - (f2 * (reproj i,x))) )
by A5;
then A7:
dom ((f1 - f2) * (reproj i,x)) = dom ((f1 * (reproj i,x)) - (f2 * (reproj i,x)))
by TARSKI:2;
A8:
for z being Element of (REAL-NS 1) st z in dom ((f1 + f2) * (reproj i,x)) holds
((f1 + f2) * (reproj i,x)) . z = ((f1 * (reproj i,x)) + (f2 * (reproj i,x))) . z
proof
let z be
Element of
(REAL-NS 1);
:: thesis: ( z in dom ((f1 + f2) * (reproj i,x)) implies ((f1 + f2) * (reproj i,x)) . z = ((f1 * (reproj i,x)) + (f2 * (reproj i,x))) . z )
assume A9:
z in dom ((f1 + f2) * (reproj i,x))
;
:: thesis: ((f1 + f2) * (reproj i,x)) . z = ((f1 * (reproj i,x)) + (f2 * (reproj i,x))) . z
then
(reproj i,x) . z in (dom f1) /\ (dom f2)
by A1, FUNCT_1:21;
then A10:
(
(reproj i,x) . z in dom f1 &
(reproj i,x) . z in dom f2 )
by XBOOLE_0:def 4;
then A11:
(
z in dom (f1 * (reproj i,x)) &
z in dom (f2 * (reproj i,x)) )
by A3, FUNCT_1:21;
A12:
f1 /. ((reproj i,x) . z) =
f1 . ((reproj i,x) . z)
by A10, PARTFUN1:def 8
.=
(f1 * (reproj i,x)) . z
by A11, FUNCT_1:22
.=
(f1 * (reproj i,x)) /. z
by A11, PARTFUN1:def 8
;
A13:
f2 /. ((reproj i,x) . z) =
f2 . ((reproj i,x) . z)
by A10, PARTFUN1:def 8
.=
(f2 * (reproj i,x)) . z
by A11, FUNCT_1:22
.=
(f2 * (reproj i,x)) /. z
by A11, PARTFUN1:def 8
;
A14:
(reproj i,x) . z in dom (f1 + f2)
by A9, FUNCT_1:21;
((f1 + f2) * (reproj i,x)) . z =
(f1 + f2) . ((reproj i,x) . z)
by A9, FUNCT_1:22
.=
(f1 + f2) /. ((reproj i,x) . z)
by A14, PARTFUN1:def 8
.=
(f1 /. ((reproj i,x) . z)) + (f2 /. ((reproj i,x) . z))
by A14, VFUNCT_1:def 1
.=
((f1 * (reproj i,x)) + (f2 * (reproj i,x))) /. z
by A6, A9, A12, A13, VFUNCT_1:def 1
;
hence
((f1 + f2) * (reproj i,x)) . z = ((f1 * (reproj i,x)) + (f2 * (reproj i,x))) . z
by A6, A9, PARTFUN1:def 8;
:: thesis: verum
end;
for z being Element of (REAL-NS 1) st z in dom ((f1 - f2) * (reproj i,x)) holds
((f1 - f2) * (reproj i,x)) . z = ((f1 * (reproj i,x)) - (f2 * (reproj i,x))) . z
proof
let z be
Element of
(REAL-NS 1);
:: thesis: ( z in dom ((f1 - f2) * (reproj i,x)) implies ((f1 - f2) * (reproj i,x)) . z = ((f1 * (reproj i,x)) - (f2 * (reproj i,x))) . z )
assume A15:
z in dom ((f1 - f2) * (reproj i,x))
;
:: thesis: ((f1 - f2) * (reproj i,x)) . z = ((f1 * (reproj i,x)) - (f2 * (reproj i,x))) . z
then
(reproj i,x) . z in (dom f1) /\ (dom f2)
by A2, FUNCT_1:21;
then A16:
(
(reproj i,x) . z in dom f1 &
(reproj i,x) . z in dom f2 )
by XBOOLE_0:def 4;
then A17:
(
z in dom (f1 * (reproj i,x)) &
z in dom (f2 * (reproj i,x)) )
by A3, FUNCT_1:21;
A18:
f1 /. ((reproj i,x) . z) =
f1 . ((reproj i,x) . z)
by A16, PARTFUN1:def 8
.=
(f1 * (reproj i,x)) . z
by A17, FUNCT_1:22
.=
(f1 * (reproj i,x)) /. z
by A17, PARTFUN1:def 8
;
A19:
f2 /. ((reproj i,x) . z) =
f2 . ((reproj i,x) . z)
by A16, PARTFUN1:def 8
.=
(f2 * (reproj i,x)) . z
by A17, FUNCT_1:22
.=
(f2 * (reproj i,x)) /. z
by A17, PARTFUN1:def 8
;
A20:
(reproj i,x) . z in dom (f1 - f2)
by A15, FUNCT_1:21;
thus ((f1 - f2) * (reproj i,x)) . z =
(f1 - f2) . ((reproj i,x) . z)
by A15, FUNCT_1:22
.=
(f1 - f2) /. ((reproj i,x) . z)
by A20, PARTFUN1:def 8
.=
(f1 /. ((reproj i,x) . z)) - (f2 /. ((reproj i,x) . z))
by A20, VFUNCT_1:def 2
.=
((f1 * (reproj i,x)) - (f2 * (reproj i,x))) /. z
by A7, A15, A18, A19, VFUNCT_1:def 2
.=
((f1 * (reproj i,x)) - (f2 * (reproj i,x))) . z
by A7, A15, PARTFUN1:def 8
;
:: thesis: verum
end;
hence
( (f1 + f2) * (reproj i,x) = (f1 * (reproj i,x)) + (f2 * (reproj i,x)) & (f1 - f2) * (reproj i,x) = (f1 * (reproj i,x)) - (f2 * (reproj i,x)) )
by A6, A7, A8, PARTFUN1:34; :: thesis: verum