let G be non-trivial RealNormSpace-Sequence; for F being non trivial RealNormSpace
for f1, f2 being PartFunc of (product G),F
for x being Point of (product G)
for i being set st i in dom G holds
( (f1 + f2) * (reproj ((modetrans (G,i)),x)) = (f1 * (reproj ((modetrans (G,i)),x))) + (f2 * (reproj ((modetrans (G,i)),x))) & (f1 - f2) * (reproj ((modetrans (G,i)),x)) = (f1 * (reproj ((modetrans (G,i)),x))) - (f2 * (reproj ((modetrans (G,i)),x))) )
let F be non trivial RealNormSpace; for f1, f2 being PartFunc of (product G),F
for x being Point of (product G)
for i being set st i in dom G holds
( (f1 + f2) * (reproj ((modetrans (G,i)),x)) = (f1 * (reproj ((modetrans (G,i)),x))) + (f2 * (reproj ((modetrans (G,i)),x))) & (f1 - f2) * (reproj ((modetrans (G,i)),x)) = (f1 * (reproj ((modetrans (G,i)),x))) - (f2 * (reproj ((modetrans (G,i)),x))) )
let f1, f2 be PartFunc of (product G),F; for x being Point of (product G)
for i being set st i in dom G holds
( (f1 + f2) * (reproj ((modetrans (G,i)),x)) = (f1 * (reproj ((modetrans (G,i)),x))) + (f2 * (reproj ((modetrans (G,i)),x))) & (f1 - f2) * (reproj ((modetrans (G,i)),x)) = (f1 * (reproj ((modetrans (G,i)),x))) - (f2 * (reproj ((modetrans (G,i)),x))) )
let x be Point of (product G); for i being set st i in dom G holds
( (f1 + f2) * (reproj ((modetrans (G,i)),x)) = (f1 * (reproj ((modetrans (G,i)),x))) + (f2 * (reproj ((modetrans (G,i)),x))) & (f1 - f2) * (reproj ((modetrans (G,i)),x)) = (f1 * (reproj ((modetrans (G,i)),x))) - (f2 * (reproj ((modetrans (G,i)),x))) )
let i0 be set ; ( i0 in dom G implies ( (f1 + f2) * (reproj ((modetrans (G,i0)),x)) = (f1 * (reproj ((modetrans (G,i0)),x))) + (f2 * (reproj ((modetrans (G,i0)),x))) & (f1 - f2) * (reproj ((modetrans (G,i0)),x)) = (f1 * (reproj ((modetrans (G,i0)),x))) - (f2 * (reproj ((modetrans (G,i0)),x))) ) )
assume
i0 in dom G
; ( (f1 + f2) * (reproj ((modetrans (G,i0)),x)) = (f1 * (reproj ((modetrans (G,i0)),x))) + (f2 * (reproj ((modetrans (G,i0)),x))) & (f1 - f2) * (reproj ((modetrans (G,i0)),x)) = (f1 * (reproj ((modetrans (G,i0)),x))) - (f2 * (reproj ((modetrans (G,i0)),x))) )
set i = modetrans (G,i0);
A1:
dom (reproj ((modetrans (G,i0)),x)) = the carrier of (G . (modetrans (G,i0)))
by FUNCT_2:def 1;
A2:
dom (f1 + f2) = (dom f1) /\ (dom f2)
by VFUNCT_1:def 1;
for s being Element of (G . (modetrans (G,i0))) holds
( s in dom ((f1 + f2) * (reproj ((modetrans (G,i0)),x))) iff s in dom ((f1 * (reproj ((modetrans (G,i0)),x))) + (f2 * (reproj ((modetrans (G,i0)),x)))) )
proof
let s be
Element of
(G . (modetrans (G,i0)));
( s in dom ((f1 + f2) * (reproj ((modetrans (G,i0)),x))) iff s in dom ((f1 * (reproj ((modetrans (G,i0)),x))) + (f2 * (reproj ((modetrans (G,i0)),x)))) )
(
s in dom ((f1 + f2) * (reproj ((modetrans (G,i0)),x))) iff
(reproj ((modetrans (G,i0)),x)) . s in (dom f1) /\ (dom f2) )
by A2, A1, FUNCT_1:11;
then
(
s in dom ((f1 + f2) * (reproj ((modetrans (G,i0)),x))) iff (
(reproj ((modetrans (G,i0)),x)) . s in dom f1 &
(reproj ((modetrans (G,i0)),x)) . s in dom f2 ) )
by XBOOLE_0:def 4;
then
(
s in dom ((f1 + f2) * (reproj ((modetrans (G,i0)),x))) iff (
s in dom (f1 * (reproj ((modetrans (G,i0)),x))) &
s in dom (f2 * (reproj ((modetrans (G,i0)),x))) ) )
by A1, FUNCT_1:11;
then
(
s in dom ((f1 + f2) * (reproj ((modetrans (G,i0)),x))) iff
s in (dom (f1 * (reproj ((modetrans (G,i0)),x)))) /\ (dom (f2 * (reproj ((modetrans (G,i0)),x)))) )
by XBOOLE_0:def 4;
hence
(
s in dom ((f1 + f2) * (reproj ((modetrans (G,i0)),x))) iff
s in dom ((f1 * (reproj ((modetrans (G,i0)),x))) + (f2 * (reproj ((modetrans (G,i0)),x)))) )
by VFUNCT_1:def 1;
verum
end;
then
for s being set holds
( s in dom ((f1 + f2) * (reproj ((modetrans (G,i0)),x))) iff s in dom ((f1 * (reproj ((modetrans (G,i0)),x))) + (f2 * (reproj ((modetrans (G,i0)),x)))) )
;
then A3:
dom ((f1 + f2) * (reproj ((modetrans (G,i0)),x))) = dom ((f1 * (reproj ((modetrans (G,i0)),x))) + (f2 * (reproj ((modetrans (G,i0)),x))))
by TARSKI:1;
A4:
for z being Element of (G . (modetrans (G,i0))) st z in dom ((f1 + f2) * (reproj ((modetrans (G,i0)),x))) holds
((f1 + f2) * (reproj ((modetrans (G,i0)),x))) . z = ((f1 * (reproj ((modetrans (G,i0)),x))) + (f2 * (reproj ((modetrans (G,i0)),x)))) . z
proof
let z be
Element of
(G . (modetrans (G,i0)));
( z in dom ((f1 + f2) * (reproj ((modetrans (G,i0)),x))) implies ((f1 + f2) * (reproj ((modetrans (G,i0)),x))) . z = ((f1 * (reproj ((modetrans (G,i0)),x))) + (f2 * (reproj ((modetrans (G,i0)),x)))) . z )
assume A5:
z in dom ((f1 + f2) * (reproj ((modetrans (G,i0)),x)))
;
((f1 + f2) * (reproj ((modetrans (G,i0)),x))) . z = ((f1 * (reproj ((modetrans (G,i0)),x))) + (f2 * (reproj ((modetrans (G,i0)),x)))) . z
then A6:
(reproj ((modetrans (G,i0)),x)) . z in dom (f1 + f2)
by FUNCT_1:11;
z in (dom (f1 * (reproj ((modetrans (G,i0)),x)))) /\ (dom (f2 * (reproj ((modetrans (G,i0)),x))))
by A3, A5, VFUNCT_1:def 1;
then A9:
(
z in dom (f1 * (reproj ((modetrans (G,i0)),x))) &
z in dom (f2 * (reproj ((modetrans (G,i0)),x))) )
by XBOOLE_0:def 4;
A7:
(reproj ((modetrans (G,i0)),x)) . z in (dom f1) /\ (dom f2)
by A2, A5, FUNCT_1:11;
then
(reproj ((modetrans (G,i0)),x)) . z in dom f1
by XBOOLE_0:def 4;
then A13:
f1 /. ((reproj ((modetrans (G,i0)),x)) . z) =
f1 . ((reproj ((modetrans (G,i0)),x)) . z)
by PARTFUN1:def 6
.=
(f1 * (reproj ((modetrans (G,i0)),x))) . z
by A9, FUNCT_1:12
.=
(f1 * (reproj ((modetrans (G,i0)),x))) /. z
by A9, PARTFUN1:def 6
;
(reproj ((modetrans (G,i0)),x)) . z in dom f2
by A7, XBOOLE_0:def 4;
then A12:
f2 /. ((reproj ((modetrans (G,i0)),x)) . z) =
f2 . ((reproj ((modetrans (G,i0)),x)) . z)
by PARTFUN1:def 6
.=
(f2 * (reproj ((modetrans (G,i0)),x))) . z
by A9, FUNCT_1:12
.=
(f2 * (reproj ((modetrans (G,i0)),x))) /. z
by A9, PARTFUN1:def 6
;
((f1 + f2) * (reproj ((modetrans (G,i0)),x))) . z =
(f1 + f2) . ((reproj ((modetrans (G,i0)),x)) . z)
by A5, FUNCT_1:12
.=
(f1 + f2) /. ((reproj ((modetrans (G,i0)),x)) . z)
by A6, PARTFUN1:def 6
.=
(f1 /. ((reproj ((modetrans (G,i0)),x)) . z)) + (f2 /. ((reproj ((modetrans (G,i0)),x)) . z))
by A6, VFUNCT_1:def 1
.=
((f1 * (reproj ((modetrans (G,i0)),x))) + (f2 * (reproj ((modetrans (G,i0)),x)))) /. z
by A3, A5, A13, A12, VFUNCT_1:def 1
;
hence
((f1 + f2) * (reproj ((modetrans (G,i0)),x))) . z = ((f1 * (reproj ((modetrans (G,i0)),x))) + (f2 * (reproj ((modetrans (G,i0)),x)))) . z
by A3, A5, PARTFUN1:def 6;
verum
end;
A14:
dom (f1 - f2) = (dom f1) /\ (dom f2)
by VFUNCT_1:def 2;
for s being Element of (G . (modetrans (G,i0))) holds
( s in dom ((f1 - f2) * (reproj ((modetrans (G,i0)),x))) iff s in dom ((f1 * (reproj ((modetrans (G,i0)),x))) - (f2 * (reproj ((modetrans (G,i0)),x)))) )
proof
let s be
Element of
(G . (modetrans (G,i0)));
( s in dom ((f1 - f2) * (reproj ((modetrans (G,i0)),x))) iff s in dom ((f1 * (reproj ((modetrans (G,i0)),x))) - (f2 * (reproj ((modetrans (G,i0)),x)))) )
(
s in dom ((f1 - f2) * (reproj ((modetrans (G,i0)),x))) iff
(reproj ((modetrans (G,i0)),x)) . s in (dom f1) /\ (dom f2) )
by A14, A1, FUNCT_1:11;
then
(
s in dom ((f1 - f2) * (reproj ((modetrans (G,i0)),x))) iff (
(reproj ((modetrans (G,i0)),x)) . s in dom f1 &
(reproj ((modetrans (G,i0)),x)) . s in dom f2 ) )
by XBOOLE_0:def 4;
then
(
s in dom ((f1 - f2) * (reproj ((modetrans (G,i0)),x))) iff (
s in dom (f1 * (reproj ((modetrans (G,i0)),x))) &
s in dom (f2 * (reproj ((modetrans (G,i0)),x))) ) )
by A1, FUNCT_1:11;
then
(
s in dom ((f1 - f2) * (reproj ((modetrans (G,i0)),x))) iff
s in (dom (f1 * (reproj ((modetrans (G,i0)),x)))) /\ (dom (f2 * (reproj ((modetrans (G,i0)),x)))) )
by XBOOLE_0:def 4;
hence
(
s in dom ((f1 - f2) * (reproj ((modetrans (G,i0)),x))) iff
s in dom ((f1 * (reproj ((modetrans (G,i0)),x))) - (f2 * (reproj ((modetrans (G,i0)),x)))) )
by VFUNCT_1:def 2;
verum
end;
then
for s being set holds
( s in dom ((f1 - f2) * (reproj ((modetrans (G,i0)),x))) iff s in dom ((f1 * (reproj ((modetrans (G,i0)),x))) - (f2 * (reproj ((modetrans (G,i0)),x)))) )
;
then A15:
dom ((f1 - f2) * (reproj ((modetrans (G,i0)),x))) = dom ((f1 * (reproj ((modetrans (G,i0)),x))) - (f2 * (reproj ((modetrans (G,i0)),x))))
by TARSKI:1;
for z being Element of (G . (modetrans (G,i0))) st z in dom ((f1 - f2) * (reproj ((modetrans (G,i0)),x))) holds
((f1 - f2) * (reproj ((modetrans (G,i0)),x))) . z = ((f1 * (reproj ((modetrans (G,i0)),x))) - (f2 * (reproj ((modetrans (G,i0)),x)))) . z
proof
let z be
Element of
(G . (modetrans (G,i0)));
( z in dom ((f1 - f2) * (reproj ((modetrans (G,i0)),x))) implies ((f1 - f2) * (reproj ((modetrans (G,i0)),x))) . z = ((f1 * (reproj ((modetrans (G,i0)),x))) - (f2 * (reproj ((modetrans (G,i0)),x)))) . z )
assume A16:
z in dom ((f1 - f2) * (reproj ((modetrans (G,i0)),x)))
;
((f1 - f2) * (reproj ((modetrans (G,i0)),x))) . z = ((f1 * (reproj ((modetrans (G,i0)),x))) - (f2 * (reproj ((modetrans (G,i0)),x)))) . z
then A17:
(reproj ((modetrans (G,i0)),x)) . z in dom (f1 - f2)
by FUNCT_1:11;
z in (dom (f1 * (reproj ((modetrans (G,i0)),x)))) /\ (dom (f2 * (reproj ((modetrans (G,i0)),x))))
by A15, A16, VFUNCT_1:def 2;
then A20:
(
z in dom (f1 * (reproj ((modetrans (G,i0)),x))) &
z in dom (f2 * (reproj ((modetrans (G,i0)),x))) )
by XBOOLE_0:def 4;
A18:
(reproj ((modetrans (G,i0)),x)) . z in (dom f1) /\ (dom f2)
by A14, A16, FUNCT_1:11;
then
(reproj ((modetrans (G,i0)),x)) . z in dom f1
by XBOOLE_0:def 4;
then A24:
f1 /. ((reproj ((modetrans (G,i0)),x)) . z) =
f1 . ((reproj ((modetrans (G,i0)),x)) . z)
by PARTFUN1:def 6
.=
(f1 * (reproj ((modetrans (G,i0)),x))) . z
by A20, FUNCT_1:12
.=
(f1 * (reproj ((modetrans (G,i0)),x))) /. z
by A20, PARTFUN1:def 6
;
(reproj ((modetrans (G,i0)),x)) . z in dom f2
by A18, XBOOLE_0:def 4;
then A23:
f2 /. ((reproj ((modetrans (G,i0)),x)) . z) =
f2 . ((reproj ((modetrans (G,i0)),x)) . z)
by PARTFUN1:def 6
.=
(f2 * (reproj ((modetrans (G,i0)),x))) . z
by A20, FUNCT_1:12
.=
(f2 * (reproj ((modetrans (G,i0)),x))) /. z
by A20, PARTFUN1:def 6
;
thus ((f1 - f2) * (reproj ((modetrans (G,i0)),x))) . z =
(f1 - f2) . ((reproj ((modetrans (G,i0)),x)) . z)
by A16, FUNCT_1:12
.=
(f1 - f2) /. ((reproj ((modetrans (G,i0)),x)) . z)
by A17, PARTFUN1:def 6
.=
(f1 /. ((reproj ((modetrans (G,i0)),x)) . z)) - (f2 /. ((reproj ((modetrans (G,i0)),x)) . z))
by A17, VFUNCT_1:def 2
.=
((f1 * (reproj ((modetrans (G,i0)),x))) - (f2 * (reproj ((modetrans (G,i0)),x)))) /. z
by A15, A16, A24, A23, VFUNCT_1:def 2
.=
((f1 * (reproj ((modetrans (G,i0)),x))) - (f2 * (reproj ((modetrans (G,i0)),x)))) . z
by A15, A16, PARTFUN1:def 6
;
verum
end;
hence
( (f1 + f2) * (reproj ((modetrans (G,i0)),x)) = (f1 * (reproj ((modetrans (G,i0)),x))) + (f2 * (reproj ((modetrans (G,i0)),x))) & (f1 - f2) * (reproj ((modetrans (G,i0)),x)) = (f1 * (reproj ((modetrans (G,i0)),x))) - (f2 * (reproj ((modetrans (G,i0)),x))) )
by A3, A15, A4, PARTFUN1:5; verum