let n be Element of NAT ; :: thesis: for f1, f2 being PartFunc of REAL ,(REAL n)
for i being Element of NAT st i in Seg n holds
( (proj i,n) * (f1 + f2) = ((proj i,n) * f1) + ((proj i,n) * f2) & (proj i,n) * (f1 - f2) = ((proj i,n) * f1) - ((proj i,n) * f2) )
let f1, f2 be PartFunc of REAL ,(REAL n); :: thesis: for i being Element of NAT st i in Seg n holds
( (proj i,n) * (f1 + f2) = ((proj i,n) * f1) + ((proj i,n) * f2) & (proj i,n) * (f1 - f2) = ((proj i,n) * f1) - ((proj i,n) * f2) )
let i be Element of NAT ; :: thesis: ( i in Seg n implies ( (proj i,n) * (f1 + f2) = ((proj i,n) * f1) + ((proj i,n) * f2) & (proj i,n) * (f1 - f2) = ((proj i,n) * f1) - ((proj i,n) * f2) ) )
assume
i in Seg n
; :: thesis: ( (proj i,n) * (f1 + f2) = ((proj i,n) * f1) + ((proj i,n) * f2) & (proj i,n) * (f1 - f2) = ((proj i,n) * f1) - ((proj i,n) * f2) )
S0:
dom (f1 + f2) = (dom f1) /\ (dom f2)
by Def1;
L1:
dom (proj i,n) = REAL n
by FUNCT_2:def 1;
then
rng f1 c= dom (proj i,n)
;
then L2:
dom ((proj i,n) * f1) = dom f1
by RELAT_1:46;
rng f2 c= dom (proj i,n)
by L1;
then L3:
dom ((proj i,n) * f2) = dom f2
by RELAT_1:46;
L4:
rng (f1 + f2) c= dom (proj i,n)
by L1;
then L5:
dom ((proj i,n) * (f1 + f2)) = dom (f1 + f2)
by RELAT_1:46;
P1:
dom ((proj i,n) * (f1 + f2)) = dom (((proj i,n) * f1) + ((proj i,n) * f2))
by S0, L5, L2, L3, VALUED_1:def 1;
for z being Element of REAL st z in dom ((proj i,n) * (f1 + f2)) holds
((proj i,n) * (f1 + f2)) . z = (((proj i,n) * f1) + ((proj i,n) * f2)) . z
proof
let z be
Element of
REAL ;
:: thesis: ( z in dom ((proj i,n) * (f1 + f2)) implies ((proj i,n) * (f1 + f2)) . z = (((proj i,n) * f1) + ((proj i,n) * f2)) . z )
assume A1:
z in dom ((proj i,n) * (f1 + f2))
;
:: thesis: ((proj i,n) * (f1 + f2)) . z = (((proj i,n) * f1) + ((proj i,n) * f2)) . z
then A2:
z in dom (f1 + f2)
by L4, RELAT_1:46;
then
(proj i,n) . ((f1 + f2) . z) = (proj i,n) . ((f1 + f2) /. z)
by PARTFUN1:def 8;
then
(proj i,n) . ((f1 + f2) . z) = (proj i,n) . ((f1 /. z) + (f2 /. z))
by A2, Def1;
then A3:
(proj i,n) . ((f1 + f2) . z) = ((f1 /. z) + (f2 /. z)) . i
by PDIFF_1:def 1;
reconsider f1z =
f1 /. z as
Element of
n -tuples_on REAL ;
reconsider f2z =
f2 /. z as
Element of
n -tuples_on REAL ;
F1:
(proj i,n) . ((f1 + f2) . z) = (f1z . i) + (f2z . i)
by A3, RVSUM_1:27;
A4:
z in dom (((proj i,n) * f1) + ((proj i,n) * f2))
by A1, S0, L5, L2, L3, VALUED_1:def 1;
z in (dom ((proj i,n) * f1)) /\ (dom ((proj i,n) * f2))
by A1, Def1, L5, L2, L3;
then A5:
(
z in dom ((proj i,n) * f1) &
z in dom ((proj i,n) * f2) )
by XBOOLE_0:def 4;
then A51:
((proj i,n) * f1) . z = (proj i,n) . (f1 . z)
by FUNCT_1:22;
A52:
((proj i,n) * f2) . z = (proj i,n) . (f2 . z)
by A5, FUNCT_1:22;
z in (dom f1) /\ (dom f2)
by A2, Def1;
then A6:
(
z in dom f1 &
z in dom f2 )
by XBOOLE_0:def 4;
then A61:
f1 . z = f1z
by PARTFUN1:def 8;
A62:
f2 . z = f2z
by A6, PARTFUN1:def 8;
A7:
((proj i,n) * f1) . z = f1z . i
by A51, A61, PDIFF_1:def 1;
((proj i,n) * f2) . z = f2z . i
by A52, A62, PDIFF_1:def 1;
then
(((proj i,n) * f1) + ((proj i,n) * f2)) . z = (f1z . i) + (f2z . i)
by A4, VALUED_1:def 1, A7;
hence
((proj i,n) * (f1 + f2)) . z = (((proj i,n) * f1) + ((proj i,n) * f2)) . z
by F1, A1, FUNCT_1:22;
:: thesis: verum
end;
hence
(proj i,n) * (f1 + f2) = ((proj i,n) * f1) + ((proj i,n) * f2)
by PARTFUN1:34, P1; :: thesis: (proj i,n) * (f1 - f2) = ((proj i,n) * f1) - ((proj i,n) * f2)
S0P:
dom (f1 - f2) = (dom f1) /\ (dom f2)
by Def2;
L4P:
rng (f1 - f2) c= dom (proj i,n)
by L1;
then L5P:
dom ((proj i,n) * (f1 - f2)) = dom (f1 - f2)
by RELAT_1:46;
P1P:
dom ((proj i,n) * (f1 - f2)) = dom (((proj i,n) * f1) - ((proj i,n) * f2))
by S0P, L5P, L2, L3, VALUED_1:12;
for z being Element of REAL st z in dom ((proj i,n) * (f1 - f2)) holds
((proj i,n) * (f1 - f2)) . z = (((proj i,n) * f1) - ((proj i,n) * f2)) . z
proof
let z be
Element of
REAL ;
:: thesis: ( z in dom ((proj i,n) * (f1 - f2)) implies ((proj i,n) * (f1 - f2)) . z = (((proj i,n) * f1) - ((proj i,n) * f2)) . z )
assume A1:
z in dom ((proj i,n) * (f1 - f2))
;
:: thesis: ((proj i,n) * (f1 - f2)) . z = (((proj i,n) * f1) - ((proj i,n) * f2)) . z
then A2:
z in dom (f1 - f2)
by L4P, RELAT_1:46;
then
(proj i,n) . ((f1 - f2) . z) = (proj i,n) . ((f1 - f2) /. z)
by PARTFUN1:def 8;
then
(proj i,n) . ((f1 - f2) . z) = (proj i,n) . ((f1 /. z) - (f2 /. z))
by A2, Def2;
then A3:
(proj i,n) . ((f1 - f2) . z) = ((f1 /. z) - (f2 /. z)) . i
by PDIFF_1:def 1;
reconsider f1z =
f1 /. z as
Element of
n -tuples_on REAL ;
reconsider f2z =
f2 /. z as
Element of
n -tuples_on REAL ;
F1:
(proj i,n) . ((f1 - f2) . z) = (f1z . i) - (f2z . i)
by A3, RVSUM_1:48;
A4:
(((proj i,n) * f1) - ((proj i,n) * f2)) . z = (((proj i,n) * f1) . z) - (((proj i,n) * f2) . z)
by A1, P1P, VALUED_1:13;
A5:
(
z in dom ((proj i,n) * f1) &
z in dom ((proj i,n) * f2) )
by A1, S0P, L5P, L2, L3, XBOOLE_0:def 4;
then A51:
((proj i,n) * f1) . z = (proj i,n) . (f1 . z)
by FUNCT_1:22;
A52:
((proj i,n) * f2) . z = (proj i,n) . (f2 . z)
by A5, FUNCT_1:22;
z in (dom f1) /\ (dom f2)
by A2, Def2;
then A6:
(
z in dom f1 &
z in dom f2 )
by XBOOLE_0:def 4;
then A61:
f1 . z = f1z
by PARTFUN1:def 8;
A62:
f2 . z = f2z
by A6, PARTFUN1:def 8;
A7:
((proj i,n) * f1) . z = f1z . i
by A51, A61, PDIFF_1:def 1;
((proj i,n) * f2) . z = f2z . i
by A52, A62, PDIFF_1:def 1;
hence
((proj i,n) * (f1 - f2)) . z = (((proj i,n) * f1) - ((proj i,n) * f2)) . z
by F1, A1, FUNCT_1:22, A4, A7;
:: thesis: verum
end;
hence
(proj i,n) * (f1 - f2) = ((proj i,n) * f1) - ((proj i,n) * f2)
by PARTFUN1:34, P1P; :: thesis: verum