let X, Y, Z be RealLinearSpace; ex I being LinearOperator of (R_VectorSpace_of_BilinearOperators (X,Y,Z)),(R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) st
( I is bijective & ( for u being Point of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) holds I . u = u * ((IsoCPRLSP (X,Y)) ") ) )
set F1 = the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z));
set F2 = the carrier of (R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z));
defpred S1[ Function, Function] means $2 = $1 * ((IsoCPRLSP (X,Y)) ");
A1:
for x being Element of the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) ex y being Element of the carrier of (R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) st S1[x,y]
proof
let x be
Element of the
carrier of
(R_VectorSpace_of_BilinearOperators (X,Y,Z));
ex y being Element of the carrier of (R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) st S1[x,y]
reconsider u =
x as
BilinearOperator of
X,
Y,
Z by LOPBAN_9:def 1;
u * ((IsoCPRLSP (X,Y)) ") is
MultilinearOperator of
<*X,Y*>,
Z
by IS02;
then reconsider v =
u * ((IsoCPRLSP (X,Y)) ") as
Element of the
carrier of
(R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) by LOPBAN10:def 4;
take
v
;
S1[x,v]
thus
S1[
x,
v]
;
verum
end;
consider I being Function of the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)), the carrier of (R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) such that
A2:
for x being Element of the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) holds S1[x,I . x]
from FUNCT_2:sch 3(A1);
A3:
for x1, x2 being object st x1 in the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) & x2 in the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) & I . x1 = I . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) & x2 in the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) & I . x1 = I . x2 implies x1 = x2 )
assume A4:
(
x1 in the
carrier of
(R_VectorSpace_of_BilinearOperators (X,Y,Z)) &
x2 in the
carrier of
(R_VectorSpace_of_BilinearOperators (X,Y,Z)) &
I . x1 = I . x2 )
;
x1 = x2
then reconsider u1 =
x1,
u2 =
x2 as
Point of
(R_VectorSpace_of_BilinearOperators (X,Y,Z)) ;
reconsider v1 =
u1,
v2 =
u2 as
BilinearOperator of
X,
Y,
Z by LOPBAN_9:def 1;
I . v1 = v1 * ((IsoCPRLSP (X,Y)) ")
by A2;
then
v1 * ((IsoCPRLSP (X,Y)) ") = v2 * ((IsoCPRLSP (X,Y)) ")
by A2, A4;
then
v1 * (((IsoCPRLSP (X,Y)) ") * (IsoCPRLSP (X,Y))) = (v2 * ((IsoCPRLSP (X,Y)) ")) * (IsoCPRLSP (X,Y))
by RELAT_1:36;
then A6:
v1 * (((IsoCPRLSP (X,Y)) ") * (IsoCPRLSP (X,Y))) = v2 * (((IsoCPRLSP (X,Y)) ") * (IsoCPRLSP (X,Y)))
by RELAT_1:36;
(
IsoCPRLSP (
X,
Y) is
one-to-one &
rng (IsoCPRLSP (X,Y)) = the
carrier of
(product <*X,Y*>) )
by FUNCT_2:def 3;
then A7:
((IsoCPRLSP (X,Y)) ") * (IsoCPRLSP (X,Y)) = id [:X,Y:]
by FUNCT_2:29;
then
v1 * (((IsoCPRLSP (X,Y)) ") * (IsoCPRLSP (X,Y))) = v1
by FUNCT_2:17;
hence
x1 = x2
by A6, A7, FUNCT_2:17;
verum
end;
A9:
for y being object st y in the carrier of (R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) holds
ex x being object st
( x in the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) & y = I . x )
proof
let y be
object ;
( y in the carrier of (R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) implies ex x being object st
( x in the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) & y = I . x ) )
assume
y in the
carrier of
(R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z))
;
ex x being object st
( x in the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) & y = I . x )
then reconsider u =
y as
Point of
(R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) ;
reconsider u1 =
u as
MultilinearOperator of
<*X,Y*>,
Z by LOPBAN10:def 4;
reconsider v1 =
u1 * (IsoCPRLSP (X,Y)) as
BilinearOperator of
X,
Y,
Z by IS01;
reconsider v =
v1 as
Point of
(R_VectorSpace_of_BilinearOperators (X,Y,Z)) by LOPBAN_9:def 1;
take
v
;
( v in the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) & y = I . v )
thus
v in the
carrier of
(R_VectorSpace_of_BilinearOperators (X,Y,Z))
;
y = I . v
(
IsoCPRLSP (
X,
Y) is
one-to-one &
rng (IsoCPRLSP (X,Y)) = the
carrier of
(product <*X,Y*>) )
by FUNCT_2:def 3;
then A10:
(IsoCPRLSP (X,Y)) * ((IsoCPRLSP (X,Y)) ") = id (product <*X,Y*>)
by FUNCT_2:29;
thus I . v =
(u1 * (IsoCPRLSP (X,Y))) * ((IsoCPRLSP (X,Y)) ")
by A2
.=
u1 * ((IsoCPRLSP (X,Y)) * ((IsoCPRLSP (X,Y)) "))
by RELAT_1:36
.=
y
by A10, FUNCT_2:17
;
verum
end;
A12:
for x, y being Point of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) holds I . (x + y) = (I . x) + (I . y)
proof
let x,
y be
Point of
(R_VectorSpace_of_BilinearOperators (X,Y,Z));
I . (x + y) = (I . x) + (I . y)
A13:
I . x = x * ((IsoCPRLSP (X,Y)) ")
by A2;
A14:
I . y = y * ((IsoCPRLSP (X,Y)) ")
by A2;
A15:
I . (x + y) = (x + y) * ((IsoCPRLSP (X,Y)) ")
by A2;
reconsider f =
I . x,
g =
I . y,
h =
I . (x + y) as
Point of
(R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) ;
for
xy being
VECTOR of
(product <*X,Y*>) holds
h . xy = (f . xy) + (g . xy)
proof
let xy be
VECTOR of
(product <*X,Y*>);
h . xy = (f . xy) + (g . xy)
consider p being
Point of
X,
q being
Point of
Y such that A16:
xy = <*p,q*>
by PRVECT_3:14;
A17:
f . xy =
x . (((IsoCPRLSP (X,Y)) ") . xy)
by A13, FUNCT_2:15
.=
x . (
p,
q)
by A16, defISOA1
;
A18:
g . xy =
y . (((IsoCPRLSP (X,Y)) ") . xy)
by A14, FUNCT_2:15
.=
y . (
p,
q)
by A16, defISOA1
;
h . xy =
(x + y) . (((IsoCPRLSP (X,Y)) ") . xy)
by A15, FUNCT_2:15
.=
(x + y) . (
p,
q)
by A16, defISOA1
;
hence
h . xy = (f . xy) + (g . xy)
by A17, A18, LOPBAN_9:2;
verum
end;
hence
I . (x + y) = (I . x) + (I . y)
by LOPBAN10:11;
verum
end;
for x being Point of (R_VectorSpace_of_BilinearOperators (X,Y,Z))
for a being Real holds I . (a * x) = a * (I . x)
proof
let x be
Point of
(R_VectorSpace_of_BilinearOperators (X,Y,Z));
for a being Real holds I . (a * x) = a * (I . x)let a be
Real;
I . (a * x) = a * (I . x)
A20:
I . x = x * ((IsoCPRLSP (X,Y)) ")
by A2;
A21:
I . (a * x) = (a * x) * ((IsoCPRLSP (X,Y)) ")
by A2;
reconsider f =
I . x,
g =
I . (a * x) as
Point of
(R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) ;
for
xy being
VECTOR of
(product <*X,Y*>) holds
g . xy = a * (f . xy)
proof
let xy be
VECTOR of
(product <*X,Y*>);
g . xy = a * (f . xy)
consider p being
Point of
X,
q being
Point of
Y such that A22:
xy = <*p,q*>
by PRVECT_3:14;
A23:
f . xy =
x . (((IsoCPRLSP (X,Y)) ") . xy)
by A20, FUNCT_2:15
.=
x . (
p,
q)
by A22, defISOA1
;
g . xy =
(a * x) . (((IsoCPRLSP (X,Y)) ") . xy)
by A21, FUNCT_2:15
.=
(a * x) . (
p,
q)
by A22, defISOA1
;
hence
g . xy = a * (f . xy)
by A23, LOPBAN_9:3;
verum
end;
hence
I . (a * x) = a * (I . x)
by LOPBAN10:12;
verum
end;
then reconsider I = I as LinearOperator of (R_VectorSpace_of_BilinearOperators (X,Y,Z)),(R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) by A12, LOPBAN_1:def 5, VECTSP_1:def 20;
take
I
; ( I is bijective & ( for u being Point of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) holds I . u = u * ((IsoCPRLSP (X,Y)) ") ) )
( I is one-to-one & I is onto )
by A3, A9, FUNCT_2:10, FUNCT_2:19;
hence
( I is bijective & ( for u being Point of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) holds I . u = u * ((IsoCPRLSP (X,Y)) ") ) )
by A2; verum