let Z be set ; for n, i being Element of NAT
for f1, f2 being PartFunc of Z,(REAL 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 n, i be Element of NAT ; for f1, f2 being PartFunc of Z,(REAL 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 Z,(REAL n); ( (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) )
A1:
dom (proj (i,n)) = REAL n
by FUNCT_2:def 1;
then
rng f1 c= dom (proj (i,n))
;
then A2:
dom ((proj (i,n)) * f1) = dom f1
by RELAT_1:27;
A3:
rng (f1 + f2) c= dom (proj (i,n))
by A1;
then A4:
dom ((proj (i,n)) * (f1 + f2)) = dom (f1 + f2)
by RELAT_1:27;
rng f2 c= dom (proj (i,n))
by A1;
then A5:
dom ((proj (i,n)) * f2) = dom f2
by RELAT_1:27;
A6:
dom (f1 + f2) = (dom f1) /\ (dom f2)
by VALUED_2:def 45;
A7:
for z being Element of Z 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
Z;
( z in dom ((proj (i,n)) * (f1 + f2)) implies ((proj (i,n)) * (f1 + f2)) . z = (((proj (i,n)) * f1) + ((proj (i,n)) * f2)) . z )
reconsider f1z =
f1 /. z as
Element of
n -tuples_on REAL ;
reconsider f2z =
f2 /. z as
Element of
n -tuples_on REAL ;
assume A8:
z in dom ((proj (i,n)) * (f1 + f2))
;
((proj (i,n)) * (f1 + f2)) . z = (((proj (i,n)) * f1) + ((proj (i,n)) * f2)) . z
then A9:
z in dom (f1 + f2)
by A3, RELAT_1:27;
then A10:
z in (dom f1) /\ (dom f2)
by VALUED_2:def 45;
then
z in dom f1
by XBOOLE_0:def 4;
then A11:
f1 . z = f1z
by PARTFUN1:def 6;
z in dom f2
by A10, XBOOLE_0:def 4;
then A12:
f2 . z = f2z
by PARTFUN1:def 6;
(proj (i,n)) . ((f1 + f2) . z) = (proj (i,n)) . ((f1 . z) + (f2 . z))
by A9, VALUED_2:def 45;
then
(proj (i,n)) . ((f1 + f2) . z) = ((f1 /. z) + (f2 /. z)) . i
by A11, A12, PDIFF_1:def 1;
then A13:
(proj (i,n)) . ((f1 + f2) . z) = (f1z . i) + (f2z . i)
by RVSUM_1:11;
A14:
z in (dom ((proj (i,n)) * f1)) /\ (dom ((proj (i,n)) * f2))
by A2, A5, A4, A8, VALUED_2:def 45;
then
z in dom ((proj (i,n)) * f1)
by XBOOLE_0:def 4;
then
((proj (i,n)) * f1) . z = (proj (i,n)) . (f1 . z)
by FUNCT_1:12;
then A15:
((proj (i,n)) * f1) . z = f1z . i
by A11, PDIFF_1:def 1;
z in dom ((proj (i,n)) * f2)
by A14, XBOOLE_0:def 4;
then
((proj (i,n)) * f2) . z = (proj (i,n)) . (f2 . z)
by FUNCT_1:12;
then A16:
((proj (i,n)) * f2) . z = f2z . i
by A12, PDIFF_1:def 1;
z in dom (((proj (i,n)) * f1) + ((proj (i,n)) * f2))
by A6, A2, A5, A4, A8, VALUED_1:def 1;
then
(((proj (i,n)) * f1) + ((proj (i,n)) * f2)) . z = (f1z . i) + (f2z . i)
by A15, A16, VALUED_1:def 1;
hence
((proj (i,n)) * (f1 + f2)) . z = (((proj (i,n)) * f1) + ((proj (i,n)) * f2)) . z
by A8, A13, FUNCT_1:12;
verum
end;
dom ((proj (i,n)) * (f1 + f2)) = dom (((proj (i,n)) * f1) + ((proj (i,n)) * f2))
by A6, A2, A5, A4, VALUED_1:def 1;
hence
(proj (i,n)) * (f1 + f2) = ((proj (i,n)) * f1) + ((proj (i,n)) * f2)
by A7, PARTFUN1:5; (proj (i,n)) * (f1 - f2) = ((proj (i,n)) * f1) - ((proj (i,n)) * f2)
A17:
rng (f1 - f2) c= dom (proj (i,n))
by A1;
then A18:
dom ((proj (i,n)) * (f1 - f2)) = dom (f1 - f2)
by RELAT_1:27;
A19:
dom (f1 - f2) = (dom f1) /\ (dom f2)
by VALUED_2:def 46;
then A20:
dom ((proj (i,n)) * (f1 - f2)) = dom (((proj (i,n)) * f1) - ((proj (i,n)) * f2))
by A2, A5, A18, VALUED_1:12;
for z being Element of Z 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
Z;
( z in dom ((proj (i,n)) * (f1 - f2)) implies ((proj (i,n)) * (f1 - f2)) . z = (((proj (i,n)) * f1) - ((proj (i,n)) * f2)) . z )
reconsider f1z =
f1 /. z as
Element of
n -tuples_on REAL ;
reconsider f2z =
f2 /. z as
Element of
n -tuples_on REAL ;
assume A21:
z in dom ((proj (i,n)) * (f1 - f2))
;
((proj (i,n)) * (f1 - f2)) . z = (((proj (i,n)) * f1) - ((proj (i,n)) * f2)) . z
then A22:
z in dom (f1 - f2)
by A17, RELAT_1:27;
then A23:
z in (dom f1) /\ (dom f2)
by VALUED_2:def 46;
then
z in dom f1
by XBOOLE_0:def 4;
then A24:
f1 . z = f1z
by PARTFUN1:def 6;
z in dom f2
by A23, XBOOLE_0:def 4;
then A25:
f2 . z = f2z
by PARTFUN1:def 6;
z in dom ((proj (i,n)) * f2)
by A5, A19, A18, A21, XBOOLE_0:def 4;
then
((proj (i,n)) * f2) . z = (proj (i,n)) . (f2 . z)
by FUNCT_1:12;
then A26:
((proj (i,n)) * f2) . z = f2z . i
by A25, PDIFF_1:def 1;
(proj (i,n)) . ((f1 - f2) . z) = (proj (i,n)) . ((f1 . z) - (f2 . z))
by A22, VALUED_2:def 46;
then
(proj (i,n)) . ((f1 - f2) . z) = ((f1 /. z) - (f2 /. z)) . i
by A24, A25, PDIFF_1:def 1;
then A27:
(proj (i,n)) . ((f1 - f2) . z) = (f1z . i) - (f2z . i)
by RVSUM_1:27;
z in dom ((proj (i,n)) * f1)
by A2, A19, A18, A21, XBOOLE_0:def 4;
then
((proj (i,n)) * f1) . z = (proj (i,n)) . (f1 . z)
by FUNCT_1:12;
then A28:
((proj (i,n)) * f1) . z = f1z . i
by A24, PDIFF_1:def 1;
(((proj (i,n)) * f1) - ((proj (i,n)) * f2)) . z = (((proj (i,n)) * f1) . z) - (((proj (i,n)) * f2) . z)
by A20, A21, VALUED_1:13;
hence
((proj (i,n)) * (f1 - f2)) . z = (((proj (i,n)) * f1) - ((proj (i,n)) * f2)) . z
by A21, A27, A28, A26, FUNCT_1:12;
verum
end;
hence
(proj (i,n)) * (f1 - f2) = ((proj (i,n)) * f1) - ((proj (i,n)) * f2)
by A20, PARTFUN1:5; verum