let X, Y, Z be RealNormSpace; ex I being LinearOperator of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)),(R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z)) st
( I is bijective & I is isometric & ( for u being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds I . u = u * ((IsoCPNrSP (X,Y)) ") ) )
set F1 = the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));
set F2 = the carrier of (R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z));
defpred S1[ Function, Function] means $2 = $1 * ((IsoCPNrSP (X,Y)) ");
A1:
for x being Element of the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ex y being Element of the carrier of (R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z)) st S1[x,y]
proof
let x be
Element of the
carrier of
(R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));
ex y being Element of the carrier of (R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z)) st S1[x,y]
reconsider u =
x as
Lipschitzian BilinearOperator of
X,
Y,
Z by LOPBAN_9:def 4;
u * ((IsoCPNrSP (X,Y)) ") is
Lipschitzian MultilinearOperator of
<*X,Y*>,
Z
by IS02A;
then reconsider v =
u * ((IsoCPNrSP (X,Y)) ") as
Element of the
carrier of
(R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z)) by LOPBAN10:def 11;
take
v
;
S1[x,v]
thus
S1[
x,
v]
;
verum
end;
consider I being Function of the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)), the carrier of (R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z)) such that
A2:
for x being Element of the carrier of (R_NormSpace_of_BoundedBilinearOperators (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_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) & x2 in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) & I . x1 = I . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) & x2 in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) & I . x1 = I . x2 implies x1 = x2 )
assume A4:
(
x1 in the
carrier of
(R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) &
x2 in the
carrier of
(R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) &
I . x1 = I . x2 )
;
x1 = x2
then reconsider u1 =
x1,
u2 =
x2 as
Point of
(R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ;
reconsider v1 =
u1,
v2 =
u2 as
Lipschitzian BilinearOperator of
X,
Y,
Z by LOPBAN_9:def 4;
I . v1 = v1 * ((IsoCPNrSP (X,Y)) ")
by A2;
then
v1 * ((IsoCPNrSP (X,Y)) ") = v2 * ((IsoCPNrSP (X,Y)) ")
by A2, A4;
then
v1 * (((IsoCPNrSP (X,Y)) ") * (IsoCPNrSP (X,Y))) = (v2 * ((IsoCPNrSP (X,Y)) ")) * (IsoCPNrSP (X,Y))
by RELAT_1:36;
then A6:
v1 * (((IsoCPNrSP (X,Y)) ") * (IsoCPNrSP (X,Y))) = v2 * (((IsoCPNrSP (X,Y)) ") * (IsoCPNrSP (X,Y)))
by RELAT_1:36;
(
IsoCPNrSP (
X,
Y) is
one-to-one &
rng (IsoCPNrSP (X,Y)) = the
carrier of
(product <*X,Y*>) )
by FUNCT_2:def 3;
then A7:
((IsoCPNrSP (X,Y)) ") * (IsoCPNrSP (X,Y)) = id [:X,Y:]
by FUNCT_2:29;
then
v1 * (((IsoCPNrSP (X,Y)) ") * (IsoCPNrSP (X,Y))) = v1
by FUNCT_2:17;
hence
x1 = x2
by A6, A7, FUNCT_2:17;
verum
end;
for y being object st y in the carrier of (R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z)) holds
ex x being object st
( x in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) & y = I . x )
proof
let y be
object ;
( y in the carrier of (R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z)) implies ex x being object st
( x in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) & y = I . x ) )
assume
y in the
carrier of
(R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z))
;
ex x being object st
( x in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) & y = I . x )
then reconsider u =
y as
Point of
(R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z)) ;
reconsider u1 =
u as
Lipschitzian MultilinearOperator of
<*X,Y*>,
Z by LOPBAN10:def 11;
reconsider v1 =
u1 * (IsoCPNrSP (X,Y)) as
Lipschitzian BilinearOperator of
X,
Y,
Z by IS01A;
reconsider v =
v1 as
Point of
(R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by LOPBAN_9:def 4;
take
v
;
( v in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) & y = I . v )
thus
v in the
carrier of
(R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))
;
y = I . v
(
IsoCPNrSP (
X,
Y) is
one-to-one &
rng (IsoCPNrSP (X,Y)) = the
carrier of
(product <*X,Y*>) )
by FUNCT_2:def 3;
then A10:
(IsoCPNrSP (X,Y)) * ((IsoCPNrSP (X,Y)) ") = id (product <*X,Y*>)
by FUNCT_2:29;
thus I . v =
(u1 * (IsoCPNrSP (X,Y))) * ((IsoCPNrSP (X,Y)) ")
by A2
.=
u1 * ((IsoCPNrSP (X,Y)) * ((IsoCPNrSP (X,Y)) "))
by RELAT_1:36
.=
y
by A10, FUNCT_2:17
;
verum
end;
then A9:
I is onto
by FUNCT_2:10;
A12:
for x, y being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds I . (x + y) = (I . x) + (I . y)
proof
let x,
y be
Point of
(R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));
I . (x + y) = (I . x) + (I . y)
A13:
I . x = x * ((IsoCPNrSP (X,Y)) ")
by A2;
A14:
I . y = y * ((IsoCPNrSP (X,Y)) ")
by A2;
A15:
I . (x + y) = (x + y) * ((IsoCPNrSP (X,Y)) ")
by A2;
set f =
I . x;
set g =
I . y;
set h =
I . (x + y);
for
xy being
VECTOR of
(product <*X,Y*>) holds
(I . (x + y)) . xy = ((I . x) . xy) + ((I . y) . xy)
proof
let xy be
VECTOR of
(product <*X,Y*>);
(I . (x + y)) . xy = ((I . x) . xy) + ((I . y) . xy)
consider p being
Point of
X,
q being
Point of
Y such that A16:
xy = <*p,q*>
by PRVECT_3:19;
A17:
(I . x) . xy =
x . (((IsoCPNrSP (X,Y)) ") . xy)
by A13, FUNCT_2:15
.=
x . (
p,
q)
by A16, NDIFF_7:18
;
A18:
(I . y) . xy =
y . (((IsoCPNrSP (X,Y)) ") . xy)
by A14, FUNCT_2:15
.=
y . (
p,
q)
by A16, NDIFF_7:18
;
(I . (x + y)) . xy =
(x + y) . (((IsoCPNrSP (X,Y)) ") . xy)
by A15, FUNCT_2:15
.=
(x + y) . (
p,
q)
by A16, NDIFF_7:18
;
hence
(I . (x + y)) . xy = ((I . x) . xy) + ((I . y) . xy)
by A17, A18, LOPBAN_9:19;
verum
end;
hence
I . (x + y) = (I . x) + (I . y)
by LOPBAN10:48;
verum
end;
for x being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))
for a being Real holds I . (a * x) = a * (I . x)
proof
let x be
Point of
(R_NormSpace_of_BoundedBilinearOperators (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 * ((IsoCPNrSP (X,Y)) ")
by A2;
A21:
I . (a * x) = (a * x) * ((IsoCPNrSP (X,Y)) ")
by A2;
set f =
I . x;
set g =
I . (a * x);
for
xy being
VECTOR of
(product <*X,Y*>) holds
(I . (a * x)) . xy = a * ((I . x) . xy)
proof
let xy be
VECTOR of
(product <*X,Y*>);
(I . (a * x)) . xy = a * ((I . x) . xy)
consider p being
Point of
X,
q being
Point of
Y such that A22:
xy = <*p,q*>
by PRVECT_3:19;
A23:
(I . x) . xy =
x . (((IsoCPNrSP (X,Y)) ") . xy)
by A20, FUNCT_2:15
.=
x . (
p,
q)
by A22, NDIFF_7:18
;
(I . (a * x)) . xy =
(a * x) . (((IsoCPNrSP (X,Y)) ") . xy)
by A21, FUNCT_2:15
.=
(a * x) . (
p,
q)
by A22, NDIFF_7:18
;
hence
(I . (a * x)) . xy = a * ((I . x) . xy)
by A23, LOPBAN_9:20;
verum
end;
hence
I . (a * x) = a * (I . x)
by LOPBAN10:49;
verum
end;
then reconsider I = I as LinearOperator of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)),(R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z)) by A12, LOPBAN_1:def 5, VECTSP_1:def 20;
take
I
; ( I is bijective & I is isometric & ( for u being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds I . u = u * ((IsoCPNrSP (X,Y)) ") ) )
A35: dom <*X,Y*> =
Seg (len <*X,Y*>)
by FINSEQ_1:def 3
.=
Seg 2
by FINSEQ_1:44
;
for u being Element of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds ||.(I . u).|| = ||.u.||
proof
let u be
Point of
(R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));
||.(I . u).|| = ||.u.||
reconsider u1 =
u as
Lipschitzian BilinearOperator of
X,
Y,
Z by LOPBAN_9:def 4;
reconsider v1 =
I . u as
Lipschitzian MultilinearOperator of
<*X,Y*>,
Z by LOPBAN10:def 11;
A26:
||.u.|| =
upper_bound (PreNorms (modetrans (u,X,Y,Z)))
by LOPBAN_9:def 8
.=
upper_bound (PreNorms u1)
;
A27:
||.(I . u).|| =
upper_bound (PreNorms (modetrans (v1,<*X,Y*>,Z)))
by LOPBAN10:def 15
.=
upper_bound (PreNorms v1)
;
for
z being
object holds
(
z in PreNorms u1 iff
z in PreNorms v1 )
proof
let z be
object ;
( z in PreNorms u1 iff z in PreNorms v1 )
hereby ( z in PreNorms v1 implies z in PreNorms u1 )
assume
z in PreNorms u1
;
z in PreNorms v1then consider x being
VECTOR of
X,
y being
VECTOR of
Y such that A28:
(
z = ||.(u1 . (x,y)).|| &
||.x.|| <= 1 &
||.y.|| <= 1 )
;
reconsider s =
<*x,y*> as
Point of
(product <*X,Y*>) by PRVECT_3:19;
A29:
(
<*X,Y*> . 1
= X &
<*X,Y*> . 2
= Y )
by FINSEQ_1:44;
A30:
v1 . s =
(u * ((IsoCPNrSP (X,Y)) ")) . s
by A2
.=
u . (((IsoCPNrSP (X,Y)) ") . s)
by FUNCT_2:15
.=
u1 . (
x,
y)
by NDIFF_7:18
;
for
i being
Element of
dom <*X,Y*> holds
||.(s . i).|| <= 1
hence
z in PreNorms v1
by A28, A30;
verum
end;
assume
z in PreNorms v1
;
z in PreNorms u1
then consider s being
VECTOR of
(product <*X,Y*>) such that A31:
(
z = ||.(v1 . s).|| & ( for
i being
Element of
dom <*X,Y*> holds
||.(s . i).|| <= 1 ) )
;
consider x being
Point of
X,
y being
Point of
Y such that A32:
s = <*x,y*>
by PRVECT_3:19;
A33:
v1 . s =
(u * ((IsoCPNrSP (X,Y)) ")) . s
by A2
.=
u . (((IsoCPNrSP (X,Y)) ") . s)
by FUNCT_2:15
.=
u1 . (
x,
y)
by A32, NDIFF_7:18
;
A34:
(
<*X,Y*> . 1
= X &
<*X,Y*> . 2
= Y )
by FINSEQ_1:44;
reconsider i1 = 1,
i2 = 2 as
Element of
dom <*X,Y*> by A35, FINSEQ_1:2, TARSKI:def 2;
(
||.(s . i1).|| <= 1 &
||.(s . i2).|| <= 1 )
by A31;
then
(
||.x.|| <= 1 &
||.y.|| <= 1 )
by A32, A34, FINSEQ_1:44;
hence
z in PreNorms u1
by A31, A33;
verum
end;
hence
||.(I . u).|| = ||.u.||
by A26, A27, TARSKI:2;
verum
end;
hence
( I is bijective & I is isometric & ( for u being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds I . u = u * ((IsoCPNrSP (X,Y)) ") ) )
by A2, NDIFF_7:7, A3, A9, FUNCT_2:19; verum