let X, Y, Z be RealLinearSpace; BilinearOperators (X,Y,Z) is linearly-closed
set W = BilinearOperators (X,Y,Z);
A1:
for v, u being VECTOR of (RealVectSpace ( the carrier of [:X,Y:],Z)) st v in BilinearOperators (X,Y,Z) & u in BilinearOperators (X,Y,Z) holds
v + u in BilinearOperators (X,Y,Z)
proof
let v,
u be
VECTOR of
(RealVectSpace ( the carrier of [:X,Y:],Z));
( v in BilinearOperators (X,Y,Z) & u in BilinearOperators (X,Y,Z) implies v + u in BilinearOperators (X,Y,Z) )
assume that A2:
v in BilinearOperators (
X,
Y,
Z)
and A3:
u in BilinearOperators (
X,
Y,
Z)
;
v + u in BilinearOperators (X,Y,Z)
reconsider u1 =
u as
BilinearOperator of
X,
Y,
Z by A3, Def6;
reconsider v1 =
v as
BilinearOperator of
X,
Y,
Z by A2, Def6;
v + u is
BilinearOperator of
X,
Y,
Z
proof
reconsider L =
v + u as
Function of
[:X,Y:],
Z by FUNCT_2:66;
A4:
for
x1,
x2 being
Point of
X for
y being
Point of
Y holds
L . (
(x1 + x2),
y)
= (L . (x1,y)) + (L . (x2,y))
proof
let x1,
x2 be
Point of
X;
for y being Point of Y holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))let y be
Point of
Y;
L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))
A5:
(
[x1,y] is
Element of
[:X,Y:] &
[x2,y] is
Element of
[:X,Y:] &
[(x1 + x2),y] is
Element of
[:X,Y:] )
;
hence L . (
(x1 + x2),
y) =
(v1 . ((x1 + x2),y)) + (u1 . ((x1 + x2),y))
by LOPBAN_1:1
.=
((v1 . (x1,y)) + (v1 . (x2,y))) + (u1 . ((x1 + x2),y))
by LOPBAN_8:11
.=
((v1 . (x1,y)) + (v1 . (x2,y))) + ((u1 . (x1,y)) + (u1 . (x2,y)))
by LOPBAN_8:11
.=
((v1 . (x1,y)) + (u1 . (x1,y))) + ((v1 . (x2,y)) + (u1 . (x2,y)))
by LM14
.=
(L . (x1,y)) + ((v1 . (x2,y)) + (u1 . (x2,y)))
by A5, LOPBAN_1:1
.=
(L . (x1,y)) + (L . (x2,y))
by A5, LOPBAN_1:1
;
verum
end;
A6:
for
x being
Point of
X for
y being
Point of
Y for
a being
Real holds
L . (
(a * x),
y)
= a * (L . (x,y))
proof
let x be
Point of
X;
for y being Point of Y
for a being Real holds L . ((a * x),y) = a * (L . (x,y))let y be
Point of
Y;
for a being Real holds L . ((a * x),y) = a * (L . (x,y))let a be
Real;
L . ((a * x),y) = a * (L . (x,y))
A7:
(
[x,y] is
Element of
[:X,Y:] &
[(a * x),y] is
Element of
[:X,Y:] )
;
hence L . (
(a * x),
y) =
(v1 . ((a * x),y)) + (u1 . ((a * x),y))
by LOPBAN_1:1
.=
(a * (v1 . (x,y))) + (u1 . ((a * x),y))
by LOPBAN_8:11
.=
(a * (v1 . (x,y))) + (a * (u1 . (x,y)))
by LOPBAN_8:11
.=
a * ((v1 . (x,y)) + (u1 . (x,y)))
by RLVECT_1:def 5
.=
a * (L . (x,y))
by A7, LOPBAN_1:1
;
verum
end;
A8:
for
x being
Point of
X for
y1,
y2 being
Point of
Y holds
L . (
x,
(y1 + y2))
= (L . (x,y1)) + (L . (x,y2))
proof
let x be
Point of
X;
for y1, y2 being Point of Y holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))let y1,
y2 be
Point of
Y;
L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))
A9:
(
[x,y1] is
Element of
[:X,Y:] &
[x,y2] is
Element of
[:X,Y:] &
[x,(y1 + y2)] is
Element of
[:X,Y:] )
;
hence L . (
x,
(y1 + y2)) =
(v1 . (x,(y1 + y2))) + (u1 . (x,(y1 + y2)))
by LOPBAN_1:1
.=
((v1 . (x,y1)) + (v1 . (x,y2))) + (u1 . (x,(y1 + y2)))
by LOPBAN_8:11
.=
((v1 . (x,y1)) + (v1 . (x,y2))) + ((u1 . (x,y1)) + (u1 . (x,y2)))
by LOPBAN_8:11
.=
((v1 . (x,y1)) + (u1 . (x,y1))) + ((v1 . (x,y2)) + (u1 . (x,y2)))
by LM14
.=
(L . (x,y1)) + ((v1 . (x,y2)) + (u1 . (x,y2)))
by A9, LOPBAN_1:1
.=
(L . (x,y1)) + (L . (x,y2))
by A9, LOPBAN_1:1
;
verum
end;
for
x being
Point of
X for
y being
Point of
Y for
a being
Real holds
L . (
x,
(a * y))
= a * (L . (x,y))
proof
let x be
Point of
X;
for y being Point of Y
for a being Real holds L . (x,(a * y)) = a * (L . (x,y))let y be
Point of
Y;
for a being Real holds L . (x,(a * y)) = a * (L . (x,y))let a be
Real;
L . (x,(a * y)) = a * (L . (x,y))
A10:
(
[x,y] is
Element of
[:X,Y:] &
[x,(a * y)] is
Element of
[:X,Y:] )
;
hence L . (
x,
(a * y)) =
(v1 . (x,(a * y))) + (u1 . (x,(a * y)))
by LOPBAN_1:1
.=
(a * (v1 . (x,y))) + (u1 . (x,(a * y)))
by LOPBAN_8:11
.=
(a * (v1 . (x,y))) + (a * (u1 . (x,y)))
by LOPBAN_8:11
.=
a * ((v1 . (x,y)) + (u1 . (x,y)))
by RLVECT_1:def 5
.=
a * (L . (x,y))
by A10, LOPBAN_1:1
;
verum
end;
hence
v + u is
BilinearOperator of
X,
Y,
Z
by A4, A6, A8, LOPBAN_8:11;
verum
end;
hence
v + u in BilinearOperators (
X,
Y,
Z)
by Def6;
verum
end;
for b being Real
for v being VECTOR of (RealVectSpace ( the carrier of [:X,Y:],Z)) st v in BilinearOperators (X,Y,Z) holds
b * v in BilinearOperators (X,Y,Z)
proof
let b be
Real;
for v being VECTOR of (RealVectSpace ( the carrier of [:X,Y:],Z)) st v in BilinearOperators (X,Y,Z) holds
b * v in BilinearOperators (X,Y,Z)let v be
VECTOR of
(RealVectSpace ( the carrier of [:X,Y:],Z));
( v in BilinearOperators (X,Y,Z) implies b * v in BilinearOperators (X,Y,Z) )
assume A11:
v in BilinearOperators (
X,
Y,
Z)
;
b * v in BilinearOperators (X,Y,Z)
reconsider v1 =
v as
BilinearOperator of
X,
Y,
Z by A11, Def6;
b * v is
BilinearOperator of
X,
Y,
Z
proof
reconsider L =
b * v as
Function of
[:X,Y:],
Z by FUNCT_2:66;
A12:
for
x1,
x2 being
Point of
X for
y being
Point of
Y holds
L . (
(x1 + x2),
y)
= (L . (x1,y)) + (L . (x2,y))
proof
let x1,
x2 be
Point of
X;
for y being Point of Y holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))let y be
Point of
Y;
L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))
A13:
(
[x1,y] is
Element of
[:X,Y:] &
[x2,y] is
Element of
[:X,Y:] &
[(x1 + x2),y] is
Element of
[:X,Y:] )
;
hence L . (
(x1 + x2),
y) =
b * (v1 . ((x1 + x2),y))
by LOPBAN_1:2
.=
b * ((v1 . (x1,y)) + (v1 . (x2,y)))
by LOPBAN_8:11
.=
(b * (v1 . (x1,y))) + (b * (v1 . (x2,y)))
by RLVECT_1:def 5
.=
(L . (x1,y)) + (b * (v1 . (x2,y)))
by A13, LOPBAN_1:2
.=
(L . (x1,y)) + (L . (x2,y))
by A13, LOPBAN_1:2
;
verum
end;
A14:
for
x being
Point of
X for
y being
Point of
Y for
a being
Real holds
L . (
(a * x),
y)
= a * (L . (x,y))
proof
let x be
Point of
X;
for y being Point of Y
for a being Real holds L . ((a * x),y) = a * (L . (x,y))let y be
Point of
Y;
for a being Real holds L . ((a * x),y) = a * (L . (x,y))let a be
Real;
L . ((a * x),y) = a * (L . (x,y))
A15:
(
[x,y] is
Element of
[:X,Y:] &
[(a * x),y] is
Element of
[:X,Y:] )
;
hence L . (
(a * x),
y) =
b * (v1 . ((a * x),y))
by LOPBAN_1:2
.=
b * (a * (v1 . (x,y)))
by LOPBAN_8:11
.=
(b * a) * (v1 . (x,y))
by RLVECT_1:def 7
.=
a * (b * (v1 . (x,y)))
by RLVECT_1:def 7
.=
a * (L . (x,y))
by A15, LOPBAN_1:2
;
verum
end;
A16:
for
x being
Point of
X for
y1,
y2 being
Point of
Y holds
L . (
x,
(y1 + y2))
= (L . (x,y1)) + (L . (x,y2))
proof
let x be
Point of
X;
for y1, y2 being Point of Y holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))let y1,
y2 be
Point of
Y;
L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))
A17:
(
[x,y1] is
Element of
[:X,Y:] &
[x,y2] is
Element of
[:X,Y:] &
[x,(y1 + y2)] is
Element of
[:X,Y:] )
;
hence L . (
x,
(y1 + y2)) =
b * (v1 . (x,(y1 + y2)))
by LOPBAN_1:2
.=
b * ((v1 . (x,y1)) + (v1 . (x,y2)))
by LOPBAN_8:11
.=
(b * (v1 . (x,y1))) + (b * (v1 . (x,y2)))
by RLVECT_1:def 5
.=
(L . (x,y1)) + (b * (v1 . (x,y2)))
by A17, LOPBAN_1:2
.=
(L . (x,y1)) + (L . (x,y2))
by A17, LOPBAN_1:2
;
verum
end;
for
x being
Point of
X for
y being
Point of
Y for
a being
Real holds
L . (
x,
(a * y))
= a * (L . (x,y))
proof
let x be
Point of
X;
for y being Point of Y
for a being Real holds L . (x,(a * y)) = a * (L . (x,y))let y be
Point of
Y;
for a being Real holds L . (x,(a * y)) = a * (L . (x,y))let a be
Real;
L . (x,(a * y)) = a * (L . (x,y))
A18:
(
[x,y] is
Element of
[:X,Y:] &
[x,(a * y)] is
Element of
[:X,Y:] )
;
hence L . (
x,
(a * y)) =
b * (v1 . (x,(a * y)))
by LOPBAN_1:2
.=
b * (a * (v1 . (x,y)))
by LOPBAN_8:11
.=
(b * a) * (v1 . (x,y))
by RLVECT_1:def 7
.=
a * (b * (v1 . (x,y)))
by RLVECT_1:def 7
.=
a * (L . (x,y))
by A18, LOPBAN_1:2
;
verum
end;
hence
b * v is
BilinearOperator of
X,
Y,
Z
by A12, A14, A16, LOPBAN_8:11;
verum
end;
hence
b * v in BilinearOperators (
X,
Y,
Z)
by Def6;
verum
end;
hence
BilinearOperators (X,Y,Z) is linearly-closed
by A1, RLSUB_1:def 1; verum