set W = MultilinearOperators (X,Y);
A1:
for v, u being VECTOR of (RealVectSpace ( the carrier of (product X),Y)) st v in MultilinearOperators (X,Y) & u in MultilinearOperators (X,Y) holds
v + u in MultilinearOperators (X,Y)
proof
let v,
u be
VECTOR of
(RealVectSpace ( the carrier of (product X),Y));
( v in MultilinearOperators (X,Y) & u in MultilinearOperators (X,Y) implies v + u in MultilinearOperators (X,Y) )
assume that A2:
v in MultilinearOperators (
X,
Y)
and A3:
u in MultilinearOperators (
X,
Y)
;
v + u in MultilinearOperators (X,Y)
reconsider u1 =
u as
MultilinearOperator of
X,
Y by A3, Def6;
reconsider v1 =
v as
MultilinearOperator of
X,
Y by A2, Def6;
v + u is
MultilinearOperator of
X,
Y
proof
reconsider L0 =
v + u as
Function of
(product X),
Y by FUNCT_2:66;
now for i being Element of dom X
for x being Point of (product X) holds L0 * (reproj (i,x)) is LinearOperator of (X . i),Ylet i be
Element of
dom X;
for x being Point of (product X) holds L0 * (reproj (i,x)) is LinearOperator of (X . i),Ylet x be
Point of
(product X);
L0 * (reproj (i,x)) is LinearOperator of (X . i),Yreconsider L =
L0 * (reproj (i,x)) as
Function of
(X . i),
Y ;
A4:
(
u1 * (reproj (i,x)) is
LinearOperator of
(X . i),
Y &
v1 * (reproj (i,x)) is
LinearOperator of
(X . i),
Y )
by Def3;
A5:
for
x1,
x2 being
Point of
(X . i) holds
L . (x1 + x2) = (L . x1) + (L . x2)
proof
let x1,
x2 be
Point of
(X . i);
L . (x1 + x2) = (L . x1) + (L . x2)
thus L . (x1 + x2) =
L0 . ((reproj (i,x)) . (x1 + x2))
by FUNCT_2:15
.=
(u1 . ((reproj (i,x)) . (x1 + x2))) + (v1 . ((reproj (i,x)) . (x1 + x2)))
by LOPBAN_1:1
.=
((u1 * (reproj (i,x))) . (x1 + x2)) + (v1 . ((reproj (i,x)) . (x1 + x2)))
by FUNCT_2:15
.=
((u1 * (reproj (i,x))) . (x1 + x2)) + ((v1 * (reproj (i,x))) . (x1 + x2))
by FUNCT_2:15
.=
(((u1 * (reproj (i,x))) . x1) + ((u1 * (reproj (i,x))) . x2)) + ((v1 * (reproj (i,x))) . (x1 + x2))
by A4, VECTSP_1:def 20
.=
(((u1 * (reproj (i,x))) . x1) + ((u1 * (reproj (i,x))) . x2)) + (((v1 * (reproj (i,x))) . x1) + ((v1 * (reproj (i,x))) . x2))
by A4, VECTSP_1:def 20
.=
(((u1 * (reproj (i,x))) . x1) + ((v1 * (reproj (i,x))) . x1)) + (((u1 * (reproj (i,x))) . x2) + ((v1 * (reproj (i,x))) . x2))
by LM14
.=
((u1 . ((reproj (i,x)) . x1)) + ((v1 * (reproj (i,x))) . x1)) + (((u1 * (reproj (i,x))) . x2) + ((v1 * (reproj (i,x))) . x2))
by FUNCT_2:15
.=
((u1 . ((reproj (i,x)) . x1)) + (v1 . ((reproj (i,x)) . x1))) + (((u1 * (reproj (i,x))) . x2) + ((v1 * (reproj (i,x))) . x2))
by FUNCT_2:15
.=
((u1 . ((reproj (i,x)) . x1)) + (v1 . ((reproj (i,x)) . x1))) + ((u1 . ((reproj (i,x)) . x2)) + ((v1 * (reproj (i,x))) . x2))
by FUNCT_2:15
.=
((u1 . ((reproj (i,x)) . x1)) + (v1 . ((reproj (i,x)) . x1))) + ((u1 . ((reproj (i,x)) . x2)) + (v1 . ((reproj (i,x)) . x2)))
by FUNCT_2:15
.=
(L0 . ((reproj (i,x)) . x1)) + ((u1 . ((reproj (i,x)) . x2)) + (v1 . ((reproj (i,x)) . x2)))
by LOPBAN_1:1
.=
(L0 . ((reproj (i,x)) . x1)) + (L0 . ((reproj (i,x)) . x2))
by LOPBAN_1:1
.=
(L . x1) + ((u + v) . ((reproj (i,x)) . x2))
by FUNCT_2:15
.=
(L . x1) + (L . x2)
by FUNCT_2:15
;
verum
end;
for
x being
Point of
(X . i) for
a being
Real holds
L . (a * x) = a * (L . x)
proof
let x1 be
Point of
(X . i);
for a being Real holds L . (a * x1) = a * (L . x1)let a be
Real;
L . (a * x1) = a * (L . x1)
thus L . (a * x1) =
L0 . ((reproj (i,x)) . (a * x1))
by FUNCT_2:15
.=
(u1 . ((reproj (i,x)) . (a * x1))) + (v1 . ((reproj (i,x)) . (a * x1)))
by LOPBAN_1:1
.=
((u1 * (reproj (i,x))) . (a * x1)) + (v1 . ((reproj (i,x)) . (a * x1)))
by FUNCT_2:15
.=
((u1 * (reproj (i,x))) . (a * x1)) + ((v1 * (reproj (i,x))) . (a * x1))
by FUNCT_2:15
.=
(a * ((u1 * (reproj (i,x))) . x1)) + ((v1 * (reproj (i,x))) . (a * x1))
by A4, LOPBAN_1:def 5
.=
(a * ((u1 * (reproj (i,x))) . x1)) + (a * ((v1 * (reproj (i,x))) . x1))
by A4, LOPBAN_1:def 5
.=
(a * (u1 . ((reproj (i,x)) . x1))) + (a * ((v1 * (reproj (i,x))) . x1))
by FUNCT_2:15
.=
(a * (u1 . ((reproj (i,x)) . x1))) + (a * (v1 . ((reproj (i,x)) . x1)))
by FUNCT_2:15
.=
a * ((u1 . ((reproj (i,x)) . x1)) + (v1 . ((reproj (i,x)) . x1)))
by RLVECT_1:def 5
.=
a * (L0 . ((reproj (i,x)) . x1))
by LOPBAN_1:1
.=
a * (L . x1)
by FUNCT_2:15
;
verum
end; hence
L0 * (reproj (i,x)) is
LinearOperator of
(X . i),
Y
by A5, LOPBAN_1:def 5, VECTSP_1:def 20;
verum end;
hence
v + u is
MultilinearOperator of
X,
Y
by Def3;
verum
end;
hence
v + u in MultilinearOperators (
X,
Y)
by Def6;
verum
end;
for b being Real
for v being VECTOR of (RealVectSpace ( the carrier of (product X),Y)) st v in MultilinearOperators (X,Y) holds
b * v in MultilinearOperators (X,Y)
proof
let b be
Real;
for v being VECTOR of (RealVectSpace ( the carrier of (product X),Y)) st v in MultilinearOperators (X,Y) holds
b * v in MultilinearOperators (X,Y)let v be
VECTOR of
(RealVectSpace ( the carrier of (product X),Y));
( v in MultilinearOperators (X,Y) implies b * v in MultilinearOperators (X,Y) )
assume A9:
v in MultilinearOperators (
X,
Y)
;
b * v in MultilinearOperators (X,Y)
reconsider v1 =
v as
MultilinearOperator of
X,
Y by A9, Def6;
b * v is
MultilinearOperator of
X,
Y
proof
reconsider L0 =
b * v as
Function of
(product X),
Y by FUNCT_2:66;
now for i being Element of dom X
for x being Point of (product X) holds L0 * (reproj (i,x)) is LinearOperator of (X . i),Ylet i be
Element of
dom X;
for x being Point of (product X) holds L0 * (reproj (i,x)) is LinearOperator of (X . i),Ylet x be
Point of
(product X);
L0 * (reproj (i,x)) is LinearOperator of (X . i),Yreconsider L =
L0 * (reproj (i,x)) as
Function of
(X . i),
Y ;
A10:
v1 * (reproj (i,x)) is
LinearOperator of
(X . i),
Y
by Def3;
A11:
for
x1,
x2 being
Point of
(X . i) holds
L . (x1 + x2) = (L . x1) + (L . x2)
proof
let x1,
x2 be
Point of
(X . i);
L . (x1 + x2) = (L . x1) + (L . x2)
thus L . (x1 + x2) =
L0 . ((reproj (i,x)) . (x1 + x2))
by FUNCT_2:15
.=
b * (v1 . ((reproj (i,x)) . (x1 + x2)))
by LOPBAN_1:2
.=
b * ((v1 * (reproj (i,x))) . (x1 + x2))
by FUNCT_2:15
.=
b * (((v1 * (reproj (i,x))) . x1) + ((v1 * (reproj (i,x))) . x2))
by A10, VECTSP_1:def 20
.=
(b * ((v1 * (reproj (i,x))) . x1)) + (b * ((v1 * (reproj (i,x))) . x2))
by RLVECT_1:def 5
.=
(b * (v1 . ((reproj (i,x)) . x1))) + (b * ((v1 * (reproj (i,x))) . x2))
by FUNCT_2:15
.=
(b * (v1 . ((reproj (i,x)) . x1))) + (b * (v1 . ((reproj (i,x)) . x2)))
by FUNCT_2:15
.=
(L0 . ((reproj (i,x)) . x1)) + (b * (v1 . ((reproj (i,x)) . x2)))
by LOPBAN_1:2
.=
(L0 . ((reproj (i,x)) . x1)) + (L0 . ((reproj (i,x)) . x2))
by LOPBAN_1:2
.=
(L . x1) + (L0 . ((reproj (i,x)) . x2))
by FUNCT_2:15
.=
(L . x1) + (L . x2)
by FUNCT_2:15
;
verum
end;
for
z being
Point of
(X . i) for
a being
Real holds
L . (a * z) = a * (L . z)
hence
L0 * (reproj (i,x)) is
LinearOperator of
(X . i),
Y
by A11, LOPBAN_1:def 5, VECTSP_1:def 20;
verum end;
hence
b * v is
MultilinearOperator of
X,
Y
by Def3;
verum
end;
hence
b * v in MultilinearOperators (
X,
Y)
by Def6;
verum
end;
hence
MultilinearOperators (X,Y) is linearly-closed
by A1, RLSUB_1:def 1; verum