:: Isomorphisms from the Space of Multilinear Operators
:: by Kazuhisa Nakasho
::
:: Received May 27, 2019
:: Copyright (c) 2019-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies LOPBAN12, LOPBAN10, NUMBERS, REAL_1, ZFMISC_1, NORMSP_1,
PRE_TOPC, FUNCT_1, SUBSET_1, RELAT_1, LOPBAN_1, ARYTM_3, GROUP_2,
FUNCT_4, VECTMETR, FUNCT_2, SUPINF_2, FCONT_1, STRUCT_0, CARD_1, SEQ_4,
MONOID_0, XXREAL_0, FINSEQ_1, RLVECT_1, NDIFF_7, PRVECT_1, PRVECT_2,
CARD_3, PDIFF_1, LOPBAN_8, LOPBAN_9;
notations TARSKI, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_7,
BINOP_1, NUMBERS, MONOID_0, XCMPLX_0, XXREAL_0, XREAL_0, CARD_3,
FINSEQ_1, SEQ_4, STRUCT_0, PRE_TOPC, RLVECT_1, NORMSP_0, NORMSP_1,
MAZURULM, RVSUM_1, LOPBAN_1, PRVECT_1, PRVECT_2, PRVECT_3, NDIFF_5,
NDIFF_7, LOPBAN_8, LOPBAN_9, LOPBAN10;
constructors SEQ_4, RELSET_1, RSSPACE3, NDIFF_5, DOMAIN_1, ABIAN, NDIFF_7,
MONOID_0, LOPBAN_9, LOPBAN10;
registrations RELSET_1, STRUCT_0, XREAL_0, MEMBERED, FUNCT_1, FINSEQ_1,
NUMBERS, XBOOLE_0, NDIFF_5, LOPBAN_1, PRVECT_2, PRVECT_3, NDIFF_7,
CARD_3, MONOID_0, FUNCT_7, LOPBAN_9, LOPBAN10, FUNCT_2, PRVECT_1;
requirements SUBSET, BOOLE, NUMERALS, ARITHM;
definitions MONOID_0;
equalities NORMSP_0, BINOP_1, PRVECT_3, LOPBAN_9, LOPBAN10, STRUCT_0;
expansions FUNCT_2;
theorems TARSKI, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, LOPBAN_1,
VECTSP_1, PRVECT_3, NDIFF_5, NDIFF_7, BINOP_1, RVSUM_1, LOPBAN_2,
LOPBAN_8, PRVECT_2, FUNCT_7, LOPBAN_9, LOPBAN10;
schemes FUNCT_2;
begin :: Plain Isomorphisms from the Space of Multilinear Operators
reserve X,Y,Z,E,F,G,S,T for RealLinearSpace;
registration
let G be RealLinearSpace-Sequence;
cluster product G -> constituted-FinSeqs;
coherence
proof
let a be Element of product G;
product G = RLSStruct(# product carr G,
zeros G, [:(addop G):],[:(multop G):] #) by PRVECT_2:def 9;
hence thesis by NDIFF_5:9;
end;
end;
theorem LemmaA:
for s being Element of product <*E,F*>,
i being Element of dom <*E,F*>,
x1 being object holds
len(s +* (i,x1)) = 2
proof
let s be Element of product <*E,F*>,
i be Element of dom <*E,F*>,
x1 be object;
consider x be Point of E, y be Point of F such that
A3: s = <*x,y*> by PRVECT_3:14;
A1: len s = 2 by A3,FINSEQ_1:44;
dom(s +* (i,x1)) = dom s by FUNCT_7:30
.= Seg 2 by A1,FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 3;
end;
theorem NDIFF5def4:
for G be RealLinearSpace-Sequence,
i be Element of dom G,
x be Element of product G holds
for r being Element of (G.i) holds
reproj (i,x) . r = x +* (i,r)
proof
let G be RealLinearSpace-Sequence,
i be Element of dom G,
x be Element of product G;
ex x0 being Element of product carr G st
x0 = x & reproj(i,x) = reproj(i,x0) by LOPBAN10:def 2;
hence thesis by LOPBAN10:def 1;
end;
definition
let X, Y be RealLinearSpace;
func IsoCPRLSP(X,Y) -> LinearOperator of [:X,Y:],product <*X,Y*> means
:defISO:
for x be Point of X, y be Point of Y holds it.(x,y) = <*x,y*>;
existence
proof
consider I be Function of [:X,Y:], product <*X,Y*> such that
I is one-to-one onto and
A1: for x be Point of X, y be Point of Y holds I.(x,y) = <*x,y*> and
A2: for v,w be Point of [:X,Y:] holds I.(v+w) = I.v + I.w and
A3: for v be Point of [:X,Y:], r be Real holds I.(r*v) = r*(I.v) and
0. product <*X,Y*> = I.(0.[:X,Y:]) by PRVECT_3:12;
reconsider I as LinearOperator of [:X,Y:], product <*X,Y*>
by A2,A3,LOPBAN_1:def 5,VECTSP_1:def 20;
take I;
thus thesis by A1;
end;
uniqueness
proof
let I1, I2 be LinearOperator of [:X,Y:],product <*X,Y*>;
assume that
A4: for x be Point of X, y be Point of Y holds I1.(x,y) = <*x,y*> and
A5: for x be Point of X, y be Point of Y holds I2.(x,y) = <*x,y*>;
for x,y be set st x in the carrier of X & y in the carrier of Y
holds I1.(x,y) = I2.(x,y)
proof
let x,y be set;
assume x in the carrier of X;
then reconsider x1 = x as Point of X;
assume y in the carrier of Y;
then reconsider y1 = y as Point of Y;
thus I1.(x,y) = <*x1,y1*> by A4
.= I2.(x,y) by A5;
end;
hence I1 = I2 by BINOP_1:def 21;
end;
end;
theorem ZeZe:
for X, Y be RealLinearSpace holds
0.product <*X,Y*> = IsoCPRLSP(X,Y).(0.[:X,Y:])
proof
let X, Y be RealLinearSpace;
consider I be Function of [:X,Y:], product <*X,Y*> such that
I is one-to-one onto and
A1: for x be Point of X, y be Point of Y holds I.(x,y) = <*x,y*> and
A2: for v,w be Point of [:X,Y:] holds I.(v+w) = I.v + I.w and
A3: for v be Point of [:X,Y:], r be Real holds I.(r*v) = r*(I.v) and
A4: 0. product <*X,Y*> = I.(0.[:X,Y:]) by PRVECT_3:12;
reconsider I as LinearOperator of [:X,Y:], product <*X,Y*>
by A2,A3,LOPBAN_1:def 5,VECTSP_1:def 20;
for a being Element of X,
b being Element of Y holds I.(a,b) = IsoCPRLSP(X,Y).(a,b)
by A1,defISO;
hence thesis by A4,BINOP_1:2;
end;
registration
let X, Y be RealLinearSpace;
cluster IsoCPRLSP(X,Y) -> bijective;
correctness
proof
consider I be Function of [:X,Y:], product <*X,Y*> such that
A1: I is one-to-one onto and
A2: for x be Point of X, y be Point of Y holds I.(x,y) = <*x,y*> and
A3: for v,w be Point of [:X,Y:] holds I.(v+w) = I.v + I.w and
A4: for v be Point of [:X,Y:], r be Real holds I.(r*v) = r*(I.v) and
0. product <*X,Y*> = I.(0.[:X,Y:]) by PRVECT_3:12;
reconsider I as LinearOperator of [:X,Y:], product <*X,Y*>
by A3,A4,VECTSP_1:def 20,LOPBAN_1:def 5;
for a being Element of X,
b being Element of Y holds
I.(a,b) = IsoCPRLSP(X,Y).(a,b) by defISO,A2;
hence thesis by A1,BINOP_1:2;
end;
end;
registration
let X, Y be RealLinearSpace;
cluster bijective for LinearOperator of [:X,Y:],product <*X,Y*>;
correctness
proof
take IsoCPRLSP(X,Y);
thus thesis;
end;
end;
theorem LM020:
for I be LinearOperator of S, T st I is bijective holds
ex J be LinearOperator of T, S st J = I" & J is bijective
proof
let I be LinearOperator of S, T;
assume
A1: I is bijective; then
a1: I is one-to-one onto; then
A2: rng I = the carrier of T & dom I = the carrier of S by FUNCT_2:def 1;
A3: rng I = dom(I") & dom I = rng(I") by A1,FUNCT_1:33; then
reconsider J = I" as Function of T,S by A2,FUNCT_2:1;
A4: for v, w be Point of T holds J.(v+w) = J.v + J.w
proof
let v, w be Point of T;
consider t be Point of S such that
A5: v = I.t by FUNCT_2:113,a1;
consider s be Point of S such that
A6: w = I.s by FUNCT_2:113,a1;
A7: J.(v+w) = J.(I.(t+s)) by A5,A6,VECTSP_1:def 20
.= t+s by A1,A2,FUNCT_1:34;
J.w = s by A1,A2,A6,FUNCT_1:34;
hence thesis by A1,A2,A5,A7,FUNCT_1:34;
end;
for v be Point of T, r be Real holds J.(r*v) = r*(J.v)
proof
let v be Point of T,r be Real;
consider t be Point of S such that
A9: v = I.t by FUNCT_2:113,a1;
J.(r*v) = J.(I.(r*t)) by A9,LOPBAN_1:def 5
.= r*t by A1,A2,FUNCT_1:34;
hence thesis by A1,A2,A9,FUNCT_1:34;
end;
then reconsider J as LinearOperator of T,S
by A4,LOPBAN_1:def 5,VECTSP_1:def 20;
take J;
thus J = I";
J is one-to-one onto by A1,A3,FUNCT_2:def 1;
hence J is bijective;
end;
definition
let X, Y be RealLinearSpace;
let f be bijective LinearOperator of [:X,Y:],product <*X,Y*>;
redefine func f" -> LinearOperator of product <*X,Y*>,[:X,Y:]; :: redefines " (FUNCT_1, definition)
correctness
proof
ex J be LinearOperator of product <*X,Y*>,[:X,Y:] st
J = f" & J is bijective by LM020;
hence thesis;
end;
end;
registration
let X, Y be RealLinearSpace;
let f be bijective LinearOperator of [:X,Y:],product <*X,Y*>;
cluster f" -> bijective for LinearOperator of product <*X,Y*>,[:X,Y:];
correctness
proof
ex J be LinearOperator of product <*X,Y*>,[:X,Y:] st
J = f" & J is bijective by LM020;
hence thesis;
end;
end;
registration
let X, Y be RealLinearSpace;
cluster bijective for LinearOperator of product <*X,Y*>,[:X,Y:];
correctness
proof
take IsoCPRLSP(X,Y)";
thus thesis;
end;
end;
theorem defISOA1:
for X, Y be RealLinearSpace,
x be Point of X, y be Point of Y holds
(IsoCPRLSP(X,Y)").<*x,y*> = [x,y]
proof
let X, Y be RealLinearSpace;
set I = IsoCPRLSP(X,Y);
set J = I";
A1: dom I = the carrier of [:X,Y:] by FUNCT_2:def 1;
let x be Point of X, y be Point of Y;
A2: I.(x,y) = <*x,y*> by defISO;
reconsider z = [x,y] as Point of [:X,Y:];
J.(I.z) = z by A1,FUNCT_1:34;
hence thesis by A2;
end;
theorem
for X, Y be RealLinearSpace holds
(IsoCPRLSP(X,Y)").(0. product <*X,Y*>) = 0.[:X,Y:]
proof
let X, Y be RealLinearSpace;
set I = IsoCPRLSP(X,Y);
set J = I";
A1: dom I = the carrier of [:X,Y:] by FUNCT_2:def 1;
J.(0. product <*X,Y*>) = J.(I.(0.[:X,Y:])) by ZeZe;
hence thesis by A1,FUNCT_1:34;
end;
theorem IS01:
for u be MultilinearOperator of <*E,F*>,G
holds u * (IsoCPRLSP (E,F)) is BilinearOperator of E,F,G
proof
let u be MultilinearOperator of <*E,F*>,G;
reconsider L = u * (IsoCPRLSP (E,F)) as Function of [:E,F:],G;
dom <*E,F*> = Seg len <*E,F*> by FINSEQ_1:def 3; then
dom <*E,F*> = {1,2} by FINSEQ_1:2,44; then
reconsider i1 = 1, i2 = 2 as Element of dom <*E,F*> by TARSKI:def 2;
A2: for x1,x2 be Point of E, y be Point of F
holds L. (x1+x2,y) = L. (x1,y) + L. (x2,y)
proof
let x1,x2 be Point of E, y be Point of F;
set x = x1;
reconsider xy = <*x,y*> as Point of product <*E,F*> by PRVECT_3:14;
reconsider L1 = u * reproj(i1,xy)
as LinearOperator of E,G by LOPBAN10:def 3;
A5: dom reproj(i1,xy) = the carrier of <*E,F*>.i1 by FUNCT_2:def 1
.= the carrier of E;
len xy = 2 by FINSEQ_1:44; then
dom xy = {1,2} by FINSEQ_1:2,def 3; then
A7: i1 in dom xy by TARSKI:def 2; then
A14: (xy +* (i1,x1)).1 = x1 by FUNCT_7:31;
A8: len (xy +* (i1,x1+x2)) = 2 by LemmaA;
A9: (xy +* (i1,x1+x2)).1 = x1+x2 by A7,FUNCT_7:31;
A10: (xy +* (i1,x1+x2)).2 = xy.i2 by FUNCT_7:32
.= y;
reconsider x1x2 = x1 + x2 as Element of <*E,F*>.i1;
A12: reproj(i1,xy).x1x2 = xy +* (i1,x1+x2) by NDIFF5def4
.= <*x1+x2,y*> by A8,A9,A10,FINSEQ_1:44;
A13: len (xy +* (i1,x1)) = 2 by LemmaA;
A15: (xy +* (i1,x1)).2 = xy.i2 by FUNCT_7:32
.= y;
A17:reproj(i1,xy).x1 = xy +* (i1,x1) by NDIFF5def4
.= <*x1,y*> by A13,A14,A15,FINSEQ_1:44;
A18: len (xy +* (i1,x2)) = 2 by LemmaA;
A19: (xy +* (i1,x2)).1 = x2 by A7,FUNCT_7:31;
A20: (xy +* (i1,x2)).2 = xy.i2 by FUNCT_7:32
.= y;
A22:reproj(i1,xy).(x2) = xy +* (i1,x2) by NDIFF5def4
.= <*x2,y*> by A18,A19,A20,FINSEQ_1:44;
A4: [x1+x2,y] is Point of [:E,F:] & [x1,y] is Point of [:E,F:]
& [x2,y] is Point of [:E,F:]; then
A23: L.(x1+x2,y) = u.((IsoCPRLSP (E,F)).(x1+x2,y)) by FUNCT_2:15
.= u.(reproj(i1,xy).(x1+x2)) by A12,defISO
.= L1.(x1+x2) by A5,FUNCT_1:13;
A24: L.(x1,y) = u.((IsoCPRLSP (E,F)).(x1,y)) by A4,FUNCT_2:15
.= u.(reproj(i1,xy).x1) by A17,defISO
.= L1.x1 by A5,FUNCT_1:13;
L. (x2,y) = u.((IsoCPRLSP (E,F)).(x2,y)) by A4,FUNCT_2:15
.= u.(reproj(i1,xy).x2) by A22,defISO
.= L1.x2 by A5,FUNCT_1:13;
hence L.(x1+x2,y) = L.(x1,y) + L.(x2,y) by A23,A24,VECTSP_1:def 20;
end;
A26: for x be Point of E, y be Point of F, a be Real
holds L.(a * x, y) = a * L.(x,y)
proof
let x be Point of E, y be Point of F, a be Real;
reconsider xy = <*x,y*> as Point of product <*E,F*> by PRVECT_3:14;
reconsider L1 = u * reproj(i1,xy)
as LinearOperator of E,G by LOPBAN10:def 3;
A29: dom reproj(i1,xy) = the carrier of <*E,F*>.i1 by FUNCT_2:def 1
.= the carrier of E;
len xy = 2 by FINSEQ_1:44; then
dom xy = {1,2} by FINSEQ_1:2,def 3; then
A31: i1 in dom xy by TARSKI:def 2;
A32: len(xy +* (i1,a*x)) = 2 by LemmaA;
A33: (xy +* (i1,a*x)).1 = a*x by A31,FUNCT_7:31;
A34: (xy +* (i1,a*x)).2 = xy.i2 by FUNCT_7:32
.= y;
reconsider x1x2 = a*x as Element of <*E,F*> .i1;
A36: reproj(i1,xy).x1x2 = xy +* (i1,a*x) by NDIFF5def4
.= <* a*x, y *> by A32,A33,A34,FINSEQ_1:44;
A37: len (xy +* (i1,x)) = 2 by LemmaA;
A38: (xy +* (i1,x)).1 = x by A31,FUNCT_7:31;
A39: (xy +* (i1,x)).2 = xy.i2 by FUNCT_7:32
.= y;
A41:reproj(i1,xy).x = xy +* (i1,x) by NDIFF5def4
.= <*x,y*> by A37,A38,A39,FINSEQ_1:44;
A28: [x,y] is Point of [:E,F:] & [a*x,y] is Point of [:E,F:]; then
A42: L.(a*x,y) = u.((IsoCPRLSP(E,F)).(a*x,y)) by FUNCT_2:15
.= u.(reproj(i1,xy).(a*x)) by A36,defISO
.= L1.(a*x) by A29,FUNCT_1:13;
L.(x,y) = u.((IsoCPRLSP (E,F)).(x,y)) by A28,FUNCT_2:15
.= u.(reproj(i1,xy).x) by A41,defISO
.= L1.x by A29,FUNCT_1:13;
hence L.(a*x, y) = a* L.(x,y) by A42,LOPBAN_1:def 5;
end;
A44: for x be Point of E, y1,y2 be Point of F
holds L.(x,y1+y2) = L.(x,y1) + L.(x,y2)
proof
let x be Point of E, y1,y2 be Point of F;
reconsider xy = <*x,y1*> as Point of product <*E,F*> by PRVECT_3:14;
reconsider L1= u * reproj(i2,xy)
as LinearOperator of F,G by LOPBAN10:def 3;
A47: dom reproj(i2,xy) = the carrier of <*E,F*>.i2 by FUNCT_2:def 1
.= the carrier of F;
len xy = 2 by FINSEQ_1:44; then
dom xy = {1,2} by FINSEQ_1:2,def 3; then
A49: i2 in dom xy by TARSKI:def 2;
A50: len (xy +* (i2,y1+y2)) = 2 by LemmaA;
A51: (xy +* (i2,y1+y2)).1 = xy.i1 by FUNCT_7:32
.= x;
A52: (xy +* (i2,y1+y2)).2 = y1+y2 by A49,FUNCT_7:31;
reconsider x1x2 = y1+y2 as Element of <*E,F*>.i2;
A54: reproj(i2,xy).x1x2 = xy +* (i2,y1+y2) by NDIFF5def4
.= <*x,y1+y2*> by A50,A51,A52,FINSEQ_1:44;
A55: len(xy +* (i2,y1)) = 2 by LemmaA;
A56: (xy +* (i2,y1)).1 = xy.i1 by FUNCT_7:32
.= x;
A57: (xy +* (i2,y1)).2 = y1 by A49,FUNCT_7:31;
A59:reproj(i2,xy).y1 = xy +* (i2,y1) by NDIFF5def4
.= <*x,y1*> by A55,A56,A57,FINSEQ_1:44;
A60: len (xy +* (i2,y2)) = 2 by LemmaA;
A61: (xy +* (i2,y2)).1 = xy.i1 by FUNCT_7:32
.= x;
A62: (xy +* (i2,y2)).2 = y2 by A49,FUNCT_7:31;
A64:reproj(i2,xy).y2 = xy +* (i2,y2) by NDIFF5def4
.= <*x,y2*> by A60,A61,A62,FINSEQ_1:44;
A46: [x,y1+y2] is Point of [:E,F:]
& [x,y1] is Point of [:E,F:]
& [x,y2] is Point of [:E,F:]; then
A65: L.(x,y1+y2) = u.((IsoCPRLSP (E,F)).(x,y1+y2)) by FUNCT_2:15
.= u.(reproj(i2,xy).(y1+y2)) by A54,defISO
.= L1.(y1+y2) by A47,FUNCT_1:13;
A66: L. (x,y1) = u.((IsoCPRLSP (E,F)).(x,y1)) by A46,FUNCT_2:15
.= u.(reproj(i2,xy).y1) by A59,defISO
.= L1.y1 by A47,FUNCT_1:13;
L. (x,y2) = u.((IsoCPRLSP (E,F)).(x,y2)) by A46,FUNCT_2:15
.= u.(reproj(i2,xy).y2) by A64,defISO
.= L1.y2 by A47,FUNCT_1:13;
hence L.(x,y1+y2) = L.(x,y1) + L.(x,y2) by A65,A66,VECTSP_1:def 20;
end;
for x be Point of E, y be Point of F, a be Real
holds L.(x,a*y) = a * L.(x,y)
proof
let x be Point of E, y be Point of F, a be Real;
reconsider xy = <*x,y*> as Point of product <*E,F*> by PRVECT_3:14;
reconsider L1 = u * reproj(i2,xy)
as LinearOperator of F,G by LOPBAN10:def 3;
A70: dom reproj(i2,xy) = the carrier of <*E,F*>.i2 by FUNCT_2:def 1
.= the carrier of F;
len xy = 2 by FINSEQ_1:44; then
dom xy = {1,2} by FINSEQ_1:2,def 3; then
A72: i2 in dom xy by TARSKI:def 2; then
A80: (xy +* (i2,y)).2 = y by FUNCT_7:31;
A73: len(xy +* (i2,a*y)) = 2 by LemmaA;
A74: (xy +* (i2,a*y)).1 = xy.i1 by FUNCT_7:32
.= x;
A75: (xy +* (i2,a*y)).2 = a*y by A72,FUNCT_7:31;
reconsider x1x2 = a*y as Element of <*E,F*> .i2;
A77: reproj(i2,xy).x1x2 = xy +* (i2,a*y) by NDIFF5def4
.= <*x,a*y*> by A73,A74,A75,FINSEQ_1:44;
A78: len (xy +* (i2,y)) = 2 by LemmaA;
A79: (xy +* (i2,y)).1 = xy.i1 by FUNCT_7:32
.= x;
A82: reproj(i2,xy).y = xy +* (i2,y) by NDIFF5def4
.= <*x,y*> by A78,A79,A80,FINSEQ_1:44;
A69: [x,y] is Point of [:E,F:] & [x,a*y] is Point of [:E,F:]; then
A83: L.(x,a*y) = u.((IsoCPRLSP(E,F)).(x,a*y)) by FUNCT_2:15
.= u.(reproj(i2,xy).(a*y)) by A77,defISO
.= L1.(a*y) by A70,FUNCT_1:13;
L. (x,y) = u.((IsoCPRLSP (E,F)).(x,y)) by A69,FUNCT_2:15
.= u.(reproj(i2,xy).y) by A82,defISO
.= L1.y by A70,FUNCT_1:13;
hence L.(x,a*y) = a * L.(x,y) by A83,LOPBAN_1:def 5;
end;
hence thesis by A2,A26,A44,LOPBAN_8:11;
end;
theorem IS02:
for u be BilinearOperator of E,F,G
holds u * (IsoCPRLSP (E,F))" is MultilinearOperator of <*E,F*>,G
proof
let u be BilinearOperator of E,F,G;
reconsider M = u * (IsoCPRLSP (E,F))" as Function of product <*E,F*>,G;
A1: dom <*E,F*> = Seg len <*E,F*> by FINSEQ_1:def 3
.= {1,2} by FINSEQ_1:2,44;
then
reconsider i1 = 1, i2 = 2 as Element of dom <*E,F*> by TARSKI:def 2;
for i be Element of dom <*E,F*>, s be Element of product <*E,F*>
holds M * reproj(i,s) is LinearOperator of <*E,F*>.i,G
proof
let i be Element of dom <*E,F*>,
s be Element of product <*E,F*>;
consider x be Point of E, y be Point of F such that
A3: s = <*x,y*> by PRVECT_3:14;
len s = 2 by A3,FINSEQ_1:44; then
A5: dom s = {1,2} by FINSEQ_1:2,def 3;
per cases by A1,TARSKI:def 2;
suppose
A6: i = 1; then
A7: <*E,F*>.i = E; then
reconsider L = M * reproj(i,s) as Function of E,G;
A8: dom reproj(i,s) = the carrier of <*E,F*>.i by FUNCT_2:def 1
.= the carrier of E by A6;
A9: for z be Point of E holds reproj(i,s).z = <*z,y*>
proof
let x1 be Point of E;
A10: len (s +* (i,x1)) = 2 by LemmaA;
A11: (s +* (i,x1)).1 = x1 by A1,A5,A6,FUNCT_7:31;
A12: (s +* (i,x1)).2 = s.2 by A6,FUNCT_7:32
.= y by A3;
thus reproj(i,s).x1 = s +* (i,x1) by A7,NDIFF5def4
.= <*x1,y*> by A10,A11,A12,FINSEQ_1:44;
end;
A14: for x1,x2 be Point of E holds L.(x1+x2) = L.x1 + L.x2
proof
let x1,x2 be Point of E;
reconsider x1y = <*x1,y*>, x2y = <*x2,y*>, x12y = <*x1+x2,y*>
as Point of product <*E,F*> by PRVECT_3:14;
A18: L.x1 = M.((reproj(i,s)).x1) by A8,FUNCT_1:13
.= (u * (IsoCPRLSP (E,F))").(<*x1,y*>) by A9
.= u.((IsoCPRLSP (E,F))" .x1y) by FUNCT_2:15
.= u.(x1,y) by defISOA1;
A19: L.x2 = M.((reproj(i,s)).x2) by A8,FUNCT_1:13
.= (u * (IsoCPRLSP(E,F))").(<*x2,y*>) by A9
.= u.((IsoCPRLSP (E,F))" .x2y) by FUNCT_2:15
.= u.(x2,y) by defISOA1;
L.(x1+x2) = M.((reproj (i,s)).(x1+x2)) by A8,FUNCT_1:13
.= (u * (IsoCPRLSP(E,F))") .(<*(x1+x2),y*>) by A9
.= u.((IsoCPRLSP(E,F))" .(x12y)) by FUNCT_2:15
.= u.(x1+x2,y) by defISOA1;
hence L.(x1+x2) = L.x1 + L.x2 by A18,A19,LOPBAN_8:11;
end;
for x1 be Point of E, a be Real holds L.(a*x1) = a * L.x1
proof
let x1 be Point of E, a be Real;
reconsider ax1y = <*a*x1,y*>, x1y = <*x1,y*>
as Point of product <*E,F*> by PRVECT_3:14;
A23: L.x1 = M.((reproj(i,s)).x1) by A8,FUNCT_1:13
.= (u * (IsoCPRLSP(E,F))").(<*x1,y*>) by A9
.= u.((IsoCPRLSP(E,F))" .x1y) by FUNCT_2:15
.= u.(x1,y) by defISOA1;
L.(a*x1) = M.((reproj (i,s)).(a*x1)) by A8,FUNCT_1:13
.= (u *(IsoCPRLSP(E,F))").(<*a*x1,y*>) by A9
.= u.((IsoCPRLSP(E,F))" .ax1y) by FUNCT_2:15
.= u.(a*x1,y) by defISOA1;
hence L.(a*x1) = a * L.x1 by A23,LOPBAN_8:11;
end;
hence M * reproj(i,s) is LinearOperator of <*E,F*>.i,G
by A7,A14,LOPBAN_1:def 5,VECTSP_1:def 20;
end;
suppose
A25: i = 2; then
A26: <*E,F*>.i = F; then
reconsider L = M * reproj(i,s) as Function of F,G;
A27: dom reproj(i,s) = the carrier of <*E,F*>.i by FUNCT_2:def 1
.= the carrier of F by A25;
A28: for z be Point of F holds reproj(i,s).z = <*x,z*>
proof
let y1 be Point of F;
A29: len(s +* (i,y1)) = 2 by LemmaA;
A30: (s +* (i,y1)).2 = y1 by A1,A5,A25,FUNCT_7:31;
A31: (s +* (i,y1)).1 = s.1 by A25,FUNCT_7:32
.= x by A3;
thus reproj(i,s).y1 = s +* (i,y1) by A26,NDIFF5def4
.= <*x,y1*> by A29,A30,A31,FINSEQ_1:44;
end;
A33: for y1,y2 be Point of F holds L.(y1+y2) = L.y1 + L.y2
proof
let y1,y2 be Point of F;
reconsider y1y = <*x,y1*>, y2y = <*x,y2*>, y12y = <*x,y1+y2*>
as Point of product <*E,F*> by PRVECT_3:14;
A37: L.y1 = M.((reproj(i,s)).y1) by A27,FUNCT_1:13
.= (u *(IsoCPRLSP(E,F))").(<*x,y1*>) by A28
.= u.((IsoCPRLSP(E,F))" .(y1y)) by FUNCT_2:15
.= u.(x,y1) by defISOA1;
A38: L.y2 = M.((reproj(i,s)).y2) by A27,FUNCT_1:13
.= (u * (IsoCPRLSP(E,F))").(<*x,y2*>) by A28
.= u.((IsoCPRLSP(E,F))" .(y2y)) by FUNCT_2:15
.= u.(x,y2) by defISOA1;
L.(y1+y2) = M.((reproj(i,s)).(y1+y2)) by A27,FUNCT_1:13
.= (u * (IsoCPRLSP(E,F))").(<*x,(y1+y2)*>) by A28
.= u.((IsoCPRLSP(E,F))" .(y12y)) by FUNCT_2:15
.= u.(x,y1+y2) by defISOA1;
hence L.(y1+y2) = L.y1 + L.y2 by A37,A38,LOPBAN_8:11;
end;
for y1 be Point of F, a be Real holds L.(a*y1) = a * L.y1
proof
let y1 be Point of F, a be Real;
reconsider ax1y = <* x, a*y1 *>, x1y = <*x,y1*>
as Point of product <*E,F*> by PRVECT_3:14;
A42: L.y1 = M.((reproj (i,s)).y1) by A27,FUNCT_1:13
.= (u * (IsoCPRLSP(E,F))").(<*x,y1*>) by A28
.= u.((IsoCPRLSP(E,F))" .x1y) by FUNCT_2:15
.= u.(x,y1) by defISOA1;
L.(a*y1) = M.((reproj(i,s)).(a*y1)) by A27,FUNCT_1:13
.= (u * (IsoCPRLSP(E,F))").(<*x,a*y1*>) by A28
.= u.((IsoCPRLSP (E,F))" .(ax1y)) by FUNCT_2:15
.= u.(x, a*y1) by defISOA1;
hence L.(a*y1) = a * L.y1 by A42,LOPBAN_8:11;
end;
hence M * reproj(i,s) is LinearOperator of <*E,F*>.i,G
by A26,A33,LOPBAN_1:def 5,VECTSP_1:def 20;
end;
end;
hence thesis by LOPBAN10:def 3;
end;
theorem IS03:
ex I be LinearOperator of
R_VectorSpace_of_BilinearOperators(X,Y,Z),
R_VectorSpace_of_MultilinearOperators(<*X,Y*>,Z)
st I is bijective
& for u be Point of R_VectorSpace_of_BilinearOperators(X,Y,Z)
holds I.u = u * (IsoCPRLSP(X,Y))"
proof
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 P1[Function,Function] means
$2 = $1 * (IsoCPRLSP(X,Y))";
A1: for x being Element of F1 ex y being Element of F2 st P1[x,y]
proof
let x be Element of F1;
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 F2 by LOPBAN10:def 4;
take v;
thus thesis;
end;
consider I being Function of F1,F2 such that
A2: for x being Element of F1 holds P1[x, I.x] from FUNCT_2:sch 3(A1);
A3: for x1, x2 being object st x1 in F1 & x2 in F1 & I.x1 = I.x2
holds x1 = x2
proof
let x1, x2 be object;
assume
A4: x1 in F1 & x2 in F1 & I.x1 = I.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 thesis by A6,A7,FUNCT_2:17;
end;
A9: for y being object st y in F2 holds
ex x being object st x in F1 & y = I.x
proof
let y be object;
assume y in F2; 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;
thus v in F1;
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;
end;
A12: for x,y be 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);
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 be VECTOR of product <*X,Y*> holds h.xy = f.xy + g.xy
proof
let xy be VECTOR of product <*X,Y*>;
consider p be Point of X, q be 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;
end;
hence thesis by LOPBAN10:11;
end;
for x be Point of R_VectorSpace_of_BilinearOperators(X,Y,Z),
a be Real holds I.(a*x) = a * I.x
proof
let x be Point of R_VectorSpace_of_BilinearOperators(X,Y,Z),
a be Real;
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 be VECTOR of product <*X,Y*> holds g.xy = a * f.xy
proof
let xy be VECTOR of product <*X,Y*>;
consider p be Point of X, q be 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;
end;
hence thesis by LOPBAN10:12;
end; then
reconsider 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 one-to-one onto by A3,A9,FUNCT_2:10,19;
hence thesis by A2;
end;
theorem
ex I be LinearOperator of R_VectorSpace_of_LinearOperators
(X,R_VectorSpace_of_LinearOperators(Y,Z)),
R_VectorSpace_of_MultilinearOperators(<*X,Y*>,Z)
st I is bijective
& for u be Point of R_VectorSpace_of_LinearOperators(X,
R_VectorSpace_of_LinearOperators(Y,Z)) holds
for x be Point of X,y be Point of Y holds (I.u).<*x,y*> = (u.x).y
proof
consider I be LinearOperator of
R_VectorSpace_of_LinearOperators(X,R_VectorSpace_of_LinearOperators(Y,Z)),
R_VectorSpace_of_BilinearOperators(X,Y,Z) such that
A1: I is bijective
& for u be Point of R_VectorSpace_of_LinearOperators(X,
R_VectorSpace_of_LinearOperators(Y,Z)) holds
for x be Point of X,y be Point of Y holds
(I.u).(x,y) = (u.x).y by LOPBAN_9:26;
consider J be LinearOperator of
R_VectorSpace_of_BilinearOperators(X,Y,Z),
R_VectorSpace_of_MultilinearOperators(<*X,Y*>,Z) such that
A2: J is bijective
& for u be Point of R_VectorSpace_of_BilinearOperators(X,Y,Z)
holds J.u = u * (IsoCPRLSP(X,Y))" by IS03;
reconsider K = J*I as LinearOperator of
R_VectorSpace_of_LinearOperators(X,
R_VectorSpace_of_LinearOperators(Y,Z)),
R_VectorSpace_of_MultilinearOperators(<*X,Y*>,Z) by LOPBAN_2:1;
take K;
thus K is bijective by A1,A2,FUNCT_2:27;
let u be Point of R_VectorSpace_of_LinearOperators(X,
R_VectorSpace_of_LinearOperators(Y,Z));
let x be Point of X, y be Point of Y;
A3: K.u = J.(I.u) by FUNCT_2:15;
reconsider xy = <*x,y*> as Point of product <*X,Y*> by PRVECT_3:14;
thus (K.u).<*x,y*> = ((I.u) * (IsoCPRLSP(X,Y))").xy by A2,A3
.= (I.u).((IsoCPRLSP (X,Y))" .xy) by FUNCT_2:15
.= (I.u).(x,y) by defISOA1
.= (u.x).y by A1;
end;
begin :: Extensions to Isometric Isomorphism from the Normed Space of
:: Multilinear Operators
reserve X,Y,Z,E,F,G for RealNormSpace;
reserve S,T for RealNormSpace-Sequence;
theorem LemmaA:
for s being Point of product <*E,F*>,
i being Element of dom <*E,F*>,
x1 being object holds
len(s +* (i,x1)) = 2
proof
let s be Point of product <*E,F*>,
i be Element of dom <*E,F*>,
x1 be object;
consider x be Point of E, y be Point of F such that
A3: s = <*x,y*> by PRVECT_3:19;
A1: len s = 2 by FINSEQ_1:44,A3;
dom(s +* (i,x1)) = dom s by FUNCT_7:30
.= Seg 2 by A1,FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 3;
end;
theorem IS01A:
for u be Lipschitzian MultilinearOperator of <*E,F*>,G holds
u * (IsoCPNrSP(E,F)) is Lipschitzian BilinearOperator of E,F,G
proof
let u be Lipschitzian MultilinearOperator of <*E,F*>,G;
reconsider L = u * (IsoCPNrSP(E,F)) as Function of [:E,F:],G;
dom <*E,F*> = Seg len <*E,F*> by FINSEQ_1:def 3
.= {1,2} by FINSEQ_1:2,44; then
reconsider i1 = 1, i2 = 2 as Element of dom <*E,F*> by TARSKI:def 2;
A2: for x1,x2 be Point of E, y be Point of F
holds L.(x1+x2,y) = L.(x1,y) + L.(x2,y)
proof
let x1,x2 be Point of E, y be Point of F;
reconsider xy = <*x1,y*> as Point of product <*E,F*> by PRVECT_3:19;
reconsider L1 = u * reproj(i1,xy)
as LinearOperator of E,G by LOPBAN10:def 6;
A5: dom reproj(i1,xy) = the carrier of <*E,F*>.i1 by FUNCT_2:def 1
.= the carrier of E;
len xy = 2 by FINSEQ_1:44; then
dom xy = {1,2} by FINSEQ_1:2,def 3; then
A7: i1 in dom xy by TARSKI:def 2;
A8: len(xy +* (i1,x1+x2)) = 2 by LemmaA;
A9: (xy +* (i1,x1+x2)).1 = x1+x2 by A7,FUNCT_7:31;
A10: (xy +* (i1,x1+x2)).2 = xy.i2 by FUNCT_7:32
.= y;
reconsider x1x2 = x1+x2 as Element of <*E,F*>.i1;
A12: reproj(i1,xy).x1x2 = xy +* (i1,x1+x2) by NDIFF_5:def 4
.= <*x1+x2, y*> by A8,A9,A10,FINSEQ_1:44;
A13: len(xy +* (i1,x1)) = 2 by LemmaA;
A14: (xy +* (i1,x1)).1 = x1 by A7,FUNCT_7:31;
A15: (xy +* (i1,x1)).2 = xy.i2 by FUNCT_7:32
.= y;
A17:reproj(i1,xy).x1 = xy +* (i1,x1) by NDIFF_5:def 4
.= <*x1,y*> by A13,A14,A15,FINSEQ_1:44;
A18: len(xy +* (i1,x2)) = 2 by LemmaA;
A19: (xy +* (i1,x2)).1 = x2 by A7,FUNCT_7:31;
A20: (xy +* (i1,x2)).2 = xy.i2 by FUNCT_7:32
.= y;
A22: reproj(i1,xy).x2 = xy +* (i1,x2) by NDIFF_5:def 4
.= <*x2,y*> by A18,A19,A20,FINSEQ_1:44;
A4: [x1+x2,y] is Point of [:E,F:]
& [x1,y] is Point of [:E,F:] & [x2,y] is Point of [:E,F:]; then
A23: L.(x1+x2,y) = u.((IsoCPNrSP(E,F)).(x1+x2,y)) by FUNCT_2:15
.= u.(reproj(i1,xy).(x1+x2)) by A12,NDIFF_7:def 3
.= L1.(x1+x2) by A5,FUNCT_1:13;
A24: L.(x1,y) = u.((IsoCPNrSP(E,F)).(x1,y)) by A4,FUNCT_2:15
.= u.(reproj(i1,xy).x1) by A17,NDIFF_7:def 3
.= L1.x1 by A5,FUNCT_1:13;
L.(x2,y) = u.((IsoCPNrSP(E,F)).(x2,y)) by A4,FUNCT_2:15
.= u.(reproj(i1,xy).x2) by A22,NDIFF_7:def 3
.= L1.x2 by A5,FUNCT_1:13;
hence L.(x1+x2,y) = L.(x1,y) + L.(x2,y) by A23,A24,VECTSP_1:def 20;
end;
A26: for x be Point of E, y be Point of F, a be Real
holds L.(a*x, y) = a * L.(x,y)
proof
let x be Point of E, y be Point of F, a be Real;
reconsider xy = <*x,y*> as Point of product <*E,F*> by PRVECT_3:19;
reconsider L1 = u * reproj(i1,xy)
as LinearOperator of E,G by LOPBAN10:def 6;
A29: dom reproj(i1,xy) = the carrier of <*E,F*>.i1 by FUNCT_2:def 1
.= the carrier of E;
len xy = 2 by FINSEQ_1:44; then
dom xy = {1,2} by FINSEQ_1:2,def 3; then
A31: i1 in dom xy by TARSKI:def 2;
A32: len(xy +* (i1,a*x)) = 2 by LemmaA;
A33: (xy +* (i1,a*x)).1 = a*x by A31,FUNCT_7:31;
A34: (xy +* (i1,a*x)).2 = xy.i2 by FUNCT_7:32
.= y;
reconsider x1x2 = a*x as Element of <*E,F*>.i1;
A36: reproj(i1,xy).x1x2 = xy +* (i1,a*x) by NDIFF_5:def 4
.= <*a*x,y*> by A32,A33,A34,FINSEQ_1:44;
A37: len (xy +* (i1,x)) = 2 by LemmaA;
A38: (xy +* (i1,x)).1 = x by A31,FUNCT_7:31;
A39: (xy +* (i1,x)).2 = xy.i2 by FUNCT_7:32
.= y;
A41: reproj(i1,xy).x = xy +* (i1,x) by NDIFF_5:def 4
.= <*x,y*> by A37,A38,A39,FINSEQ_1:44;
A28: [x,y] is Point of [:E,F:] & [a*x,y] is Point of [:E,F:]; then
A42: L.(a*x,y) = u.((IsoCPNrSP(E,F)).(a*x,y)) by FUNCT_2:15
.= u.(reproj(i1,xy).(a*x)) by A36,NDIFF_7:def 3
.= L1.(a*x) by A29,FUNCT_1:13;
L.(x,y) = u.((IsoCPNrSP(E,F)).(x,y)) by A28,FUNCT_2:15
.= u.(reproj(i1,xy).x) by A41,NDIFF_7:def 3
.= L1.x by A29,FUNCT_1:13;
hence L.(a*x, y) = a * L.(x,y) by A42,LOPBAN_1:def 5;
end;
A44: for x be Point of E, y1,y2 be Point of F
holds L.(x,y1+y2) = L.(x,y1) + L.(x,y2)
proof
let x be Point of E, y1,y2 be Point of F;
reconsider xy = <*x,y1*> as Point of product <*E,F*> by PRVECT_3:19;
reconsider L1 = u * reproj(i2,xy)
as LinearOperator of F,G by LOPBAN10:def 6;
A47: dom reproj(i2,xy) = the carrier of <*E,F*>.i2 by FUNCT_2:def 1
.= the carrier of F;
len xy = 2 by FINSEQ_1:44; then
dom xy = {1,2} by FINSEQ_1:2,def 3; then
A49: i2 in dom xy by TARSKI:def 2;
A50: len (xy +* (i2,y1+y2)) = 2 by LemmaA;
A51: (xy +* (i2,y1+y2)).1 = xy.i1 by FUNCT_7:32
.= x;
A52: (xy +* (i2,y1+y2)).2 = y1+y2 by A49,FUNCT_7:31;
reconsider x1x2 = y1+y2 as Element of <*E,F*>.i2;
A54: reproj(i2,xy).x1x2 = xy +* (i2,y1+y2) by NDIFF_5:def 4
.= <*x,y1+y2*> by A50,A51,A52,FINSEQ_1:44;
A55: len(xy +* (i2,y1)) = 2 by LemmaA;
A56: (xy +* (i2,y1)).1 = xy.i1 by FUNCT_7:32
.= x;
A57: (xy +* (i2,y1)).2 = y1 by A49,FUNCT_7:31;
A59:reproj(i2,xy).y1 = xy +* (i2,y1) by NDIFF_5:def 4
.= <*x,y1*> by A55,A56,A57,FINSEQ_1:44;
A60: len (xy +* (i2,y2)) = 2 by LemmaA;
A61: (xy +* (i2,y2)).1 = xy.i1 by FUNCT_7:32
.= x;
A62: (xy +* (i2,y2)).2 = y2 by A49,FUNCT_7:31;
A64: reproj(i2,xy).y2 = xy +* (i2,y2) by NDIFF_5:def 4
.= <*x,y2*> by A60,A61,A62,FINSEQ_1:44;
A46: [x,y1+y2] is Point of [:E,F:] & [x,y1] is Point of [:E,F:]
& [x,y2] is Point of [:E,F:]; then
A65: L.(x,y1+y2) = u.((IsoCPNrSP (E,F)).(x,y1+y2)) by FUNCT_2:15
.= u.(reproj(i2,xy).(y1+y2)) by A54,NDIFF_7:def 3
.= L1.(y1+y2) by A47,FUNCT_1:13;
A66: L.(x,y1) = u.((IsoCPNrSP (E,F)).(x,y1)) by A46,FUNCT_2:15
.= u.(reproj(i2,xy).y1) by A59,NDIFF_7:def 3
.= L1.y1 by A47,FUNCT_1:13;
L.(x,y2) = u.((IsoCPNrSP (E,F)).(x,y2)) by A46,FUNCT_2:15
.= u.(reproj(i2,xy).y2) by A64,NDIFF_7:def 3
.= L1.y2 by A47,FUNCT_1:13;
hence L.(x,y1+y2) = L.(x,y1) + L.(x,y2) by A65,A66,VECTSP_1:def 20;
end;
for x be Point of E, y be Point of F, a be Real
holds L.(x, a*y) = a * L.(x,y)
proof
let x be Point of E, y be Point of F, a be Real;
reconsider xy = <*x,y*> as Point of product <*E,F*> by PRVECT_3:19;
reconsider L1 = u * reproj(i2,xy)
as LinearOperator of F,G by LOPBAN10:def 6;
A70: dom reproj(i2,xy) = the carrier of <*E,F*>.i2 by FUNCT_2:def 1
.= the carrier of F;
len xy = 2 by FINSEQ_1:44; then
dom xy = {1,2} by FINSEQ_1:2,def 3; then
A72: i2 in dom xy by TARSKI:def 2; then
A75: (xy +* (i2, a*y)).2 = a * y by FUNCT_7:31;
A73: len(xy +* (i2,a*y)) = 2 by LemmaA;
A74: (xy +* (i2,a*y)).1 = xy.i1 by FUNCT_7:32
.= x;
reconsider x1x2 = a * y as Element of <*E,F*>.i2;
A77:reproj(i2,xy).x1x2 = xy +* (i2,a*y) by NDIFF_5:def 4
.= <*x, a*y*> by A73,A74,A75,FINSEQ_1:44;
A78: len(xy +* (i2,y)) = 2 by LemmaA;
A79: (xy +* (i2,y)).1 = xy.i1 by FUNCT_7:32
.= x;
A80: (xy +* (i2,y)).2 = y by A72,FUNCT_7:31;
A82:reproj(i2,xy).y = xy +* (i2,y) by NDIFF_5:def 4
.= <*x,y*> by A78,A79,A80,FINSEQ_1:44;
A69: [x,y] is Point of [:E,F:] & [x,a*y] is Point of [:E,F:]; then
A83: L.(x, a*y) = u.((IsoCPNrSP(E,F)).(x,a*y)) by FUNCT_2:15
.= u.(reproj(i2,xy).(a*y)) by A77,NDIFF_7:def 3
.= L1.(a*y) by A70,FUNCT_1:13;
L.(x,y) = u.((IsoCPNrSP(E,F)).(x,y)) by A69,FUNCT_2:15
.= u.(reproj(i2,xy).y) by A82,NDIFF_7:def 3
.= L1.y by A70,FUNCT_1:13;
hence L.(x,a*y) = a * L.(x,y) by A83,LOPBAN_1:def 5;
end; then
reconsider L as BilinearOperator of E,F,G by A2,A26,A44,LOPBAN_8:12;
ex K being Real
st 0 <= K
& for x being VECTOR of E, y being VECTOR of F
holds ||. L.(x,y) .|| <= K * ||. x .|| * ||. y .||
proof
consider K being Real such that
A85: 0 <= K
& for s being Point of product <*E,F*>
holds ||. u.s .|| <= K * NrProduct s by LOPBAN10:def 10;
take K;
thus 0 <= K by A85;
let x be VECTOR of E, y be VECTOR of F;
reconsider xy = <*x,y*> as Point of product <*E,F*> by PRVECT_3:19;
[x,y] is Point of [:E,F:]; then
A87: L.(x,y) = u.((IsoCPNrSP(E,F)).(x,y)) by FUNCT_2:15
.= u.(<*x,y*>) by NDIFF_7:def 3;
reconsider s = <*x,y*> as Point of product <*E,F*> by PRVECT_3:19;
consider Nx be FinSequence of REAL such that
A88: dom Nx = dom <*E,F*>
& (for i be Element of dom <*E,F*> holds Nx.i = ||.s.i.||)
& NrProduct s = Product Nx by LOPBAN10:def 9;
dom Nx = Seg len <*E,F*> by A88,FINSEQ_1:def 3
.= Seg 2 by FINSEQ_1:44; then
A89: len Nx = 2 by FINSEQ_1:def 3;
A91: Nx.1 = ||.s.i1.|| by A88
.= ||.x.||;
Nx.2 = ||.s.i2.|| by A88
.= ||.y.||; then
Nx = <* ||.x.||, ||.y.|| *> by A89,A91,FINSEQ_1:44; then
Product Nx = ||.x.|| * ||.y.|| by RVSUM_1:99; then
||.L.(x,y).|| <= K * (||.x.|| * ||.y.||) by A85,A87,A88;
hence thesis;
end;
hence thesis by LOPBAN_9:def 3;
end;
theorem IS02A:
for u be Lipschitzian BilinearOperator of E,F,G
holds u * (IsoCPNrSP(E,F))" is Lipschitzian MultilinearOperator of <*E,F*>,G
proof
let u be Lipschitzian BilinearOperator of E,F,G;
reconsider M = u * (IsoCPNrSP(E,F))"
as Function of product <*E,F*>,G;
A1: dom <*E,F*> = Seg len <*E,F*> by FINSEQ_1:def 3
.= {1,2} by FINSEQ_1:2,44;
then reconsider i1=1, i2=2 as Element of dom <*E,F*> by TARSKI:def 2;
for i be Element of dom <*E,F*>,
s be Element of product <*E,F*> holds
M * reproj(i,s) is LinearOperator of <*E,F*>.i,G
proof
let i be Element of dom <*E,F*>,
s be Element of product <*E,F*>;
consider x be Point of E, y be Point of F such that
A3: s = <*x,y*> by PRVECT_3:19;
len s = 2 by A3,FINSEQ_1:44; then
A5: dom s = {1,2} by FINSEQ_1:2,def 3;
per cases by A1,TARSKI:def 2;
suppose
A6: i = 1; then
A7: <*E,F*>.i = E; then
reconsider L = M * reproj(i,s) as Function of E,G;
A8: dom reproj(i,s) = the carrier of <*E,F*>.i by FUNCT_2:def 1
.= the carrier of E by A6;
A9: for z be Point of E holds reproj(i,s).z = <*z,y*>
proof
let x1 be Point of E;
A10: len (s +* (i,x1)) = 2 by LemmaA;
A11: (s +* (i,x1)).1 = x1 by A1,A5,A6,FUNCT_7:31;
A12: (s +* (i,x1)).2 = s.2 by A6,FUNCT_7:32
.= y by A3;
thus reproj(i,s).x1 = s +* (i,x1) by A7,NDIFF_5:def 4
.= <*x1,y*> by A10,A11,A12,FINSEQ_1:44;
end;
A14: for x1,x2 be Point of E holds L.(x1+x2) = L.x1 + L.x2
proof
let x1,x2 be Point of E;
reconsider x1y = <*x1,y*>, x2y = <*x2,y*>, x12y = <*x1+x2,y*>
as Point of product <*E,F*> by PRVECT_3:19;
A18: L.x1 = M.((reproj (i,s)).x1) by A8,FUNCT_1:13
.= (u * (IsoCPNrSP(E,F))").(<*x1,y*>) by A9
.= u.((IsoCPNrSP(E,F))" .(x1y)) by FUNCT_2:15
.= u.(x1,y) by NDIFF_7:18;
A19: L.x2 = M.((reproj(i,s)).x2) by A8,FUNCT_1:13
.= (u * (IsoCPNrSP(E,F))").(<*x2,y*>) by A9
.= u.((IsoCPNrSP(E,F))" .(x2y)) by FUNCT_2:15
.= u.(x2,y) by NDIFF_7:18;
L.(x1+x2) = M.((reproj(i,s)).(x1+x2)) by A8,FUNCT_1:13
.= (u * (IsoCPNrSP(E,F))").(<*(x1+x2),y*>) by A9
.= u.((IsoCPNrSP(E,F))" .(x12y)) by FUNCT_2:15
.= u.(x1+x2,y) by NDIFF_7:18;
hence L.(x1+x2) = L.x1 + L.x2 by A18,A19,LOPBAN_8:12;
end;
for x1 be Point of E, a be Real holds L.(a*x1) = a * L.x1
proof
let x1 be Point of E, a be Real;
reconsider ax1y = <*a*x1,y*>, x1y = <*x1,y*>
as Point of product <*E,F*> by PRVECT_3:19;
A23: L.x1 = M.((reproj(i,s)).x1) by A8,FUNCT_1:13
.= (u * (IsoCPNrSP(E,F))").(<*x1,y*>) by A9
.= u.((IsoCPNrSP(E,F))" .x1y) by FUNCT_2:15
.= u.(x1,y) by NDIFF_7:18;
L.(a*x1) = M.((reproj(i,s)).(a*x1)) by A8,FUNCT_1:13
.= (u * (IsoCPNrSP(E,F))").(<*a*x1,y*>) by A9
.= u.((IsoCPNrSP(E,F))" .(ax1y)) by FUNCT_2:15
.= u.(a*x1,y) by NDIFF_7:18;
hence L.(a*x1) = a * L.x1 by A23,LOPBAN_8:12;
end;
hence M * reproj(i,s) is LinearOperator of <*E,F*>.i,G
by A7,A14,LOPBAN_1:def 5,VECTSP_1:def 20;
end;
suppose
A25: i = 2; then
A26: <*E,F*>.i = F; then
reconsider L = M * reproj(i,s) as Function of F,G;
A27: dom reproj(i,s) = the carrier of <*E,F*> .i by FUNCT_2:def 1
.= the carrier of F by A25;
A28: for z be Point of F holds reproj(i,s).z = <*x,z*>
proof
let y1 be Point of F;
A29: len (s +* (i,y1)) = 2 by LemmaA;
A30: (s +* (i,y1)).2 = y1 by A1,A5,A25,FUNCT_7:31;
A31: (s +* (i,y1)).1 = s.1 by A25,FUNCT_7:32
.= x by A3;
thus reproj(i,s).y1 = s +* (i,y1) by A26,NDIFF_5:def 4
.= <*x,y1*> by A29,A30,A31,FINSEQ_1:44;
end;
A33: for y1,y2 be Point of F holds L.(y1+y2) = L.y1 + L.y2
proof
let y1,y2 be Point of F;
reconsider y1y = <*x,y1*>, y2y = <*x,y2*>, y12y = <*x,y1+y2*>
as Point of product <*E,F*> by PRVECT_3:19;
A37: L.y1 = M.((reproj (i,s)).y1) by A27,FUNCT_1:13
.= (u * (IsoCPNrSP (E,F))").(<*x,y1*>) by A28
.= u.((IsoCPNrSP(E,F))" .(y1y)) by FUNCT_2:15
.= u.(x,y1) by NDIFF_7:18;
A38: L.y2 = M.((reproj(i,s)).y2) by A27,FUNCT_1:13
.= (u * (IsoCPNrSP(E,F))").(<*x,y2*>) by A28
.= u.((IsoCPNrSP(E,F))" .(y2y)) by FUNCT_2:15
.= u.(x,y2) by NDIFF_7:18;
L.(y1+y2) = M.((reproj(i,s)).(y1+y2)) by A27,FUNCT_1:13
.= (u * (IsoCPNrSP (E,F))").(<*x,(y1+y2)*>) by A28
.= u.((IsoCPNrSP(E,F))" .(y12y)) by FUNCT_2:15
.= u.(x,y1+y2) by NDIFF_7:18;
hence L.(y1+y2) = L.y1 + L.y2 by A37,A38,LOPBAN_8:12;
end;
for y1 be Point of F, a be Real holds L.(a*y1) = a * L.y1
proof
let y1 be Point of F, a be Real;
reconsider ax1y = <*x,a*y1*>, x1y = <*x,y1*>
as Point of product <*E,F*> by PRVECT_3:19;
A42: L.y1 = M.((reproj(i,s)).y1) by A27,FUNCT_1:13
.= (u * (IsoCPNrSP(E,F))").(<*x,y1*>) by A28
.= u.((IsoCPNrSP (E,F))" .x1y) by FUNCT_2:15
.= u.(x,y1) by NDIFF_7:18;
L.(a*y1) = M.((reproj (i,s)).(a*y1)) by A27,FUNCT_1:13
.= (u * (IsoCPNrSP (E,F))").(<*x,a*y1*>) by A28
.= u.((IsoCPNrSP(E,F))" .(ax1y)) by FUNCT_2:15
.= u.(x,a*y1) by NDIFF_7:18;
hence L.(a*y1) = a * L.y1 by A42,LOPBAN_8:12;
end;
hence M * reproj(i,s) is LinearOperator of <*E,F*>.i,G
by A26,A33,LOPBAN_1:def 5,VECTSP_1:def 20;
end;
end; then
reconsider M as MultilinearOperator of <*E,F*>,G by LOPBAN10:def 6;
ex K being Real st 0 <= K &
for s being Point of product <*E,F*> holds ||. M.s .|| <= K * NrProduct s
proof
consider K being Real such that
A44: 0 <= K
& for x be Point of E, y be Point of F
holds ||. u.(x,y) .|| <= K * ||.x.|| * ||.y.|| by LOPBAN_9:def 3;
take K;
thus 0 <= K by A44;
let xy be Point of product <*E,F*>;
consider x be Point of E, y be Point of F such that
A45: xy = <*x,y*> by PRVECT_3:19;
A46: M.xy = u.((IsoCPNrSP(E,F)").xy) by FUNCT_2:15
.= u.(x,y) by A45,NDIFF_7:18;
consider Nx be FinSequence of REAL such that
A47: dom Nx = dom <*E,F*>
& (for i be Element of dom <*E,F*> holds Nx.i = ||.xy.i.||)
& NrProduct xy = Product Nx by LOPBAN10:def 9;
dom Nx = Seg len <*E,F*> by A47,FINSEQ_1:def 3
.= Seg 2 by FINSEQ_1:44; then
A48: len Nx = 2 by FINSEQ_1:def 3;
A50: Nx.1 = ||.xy.i1.|| by A47
.= ||.x.|| by A45;
Nx.2 = ||.xy.i2.|| by A47
.= ||.y.|| by A45; then
Nx = <* ||.x.||,||.y.|| *> by A48,A50,FINSEQ_1:44; then
A51: NrProduct xy = ||.x.|| * ||.y.|| by A47,RVSUM_1:99;
||. u.(x,y) .|| <= K * ||.x.|| * ||.y.|| by A44;
hence thesis by A46,A51;
end;
hence thesis by LOPBAN10:def 10;
end;
theorem IS03A:
ex I be LinearOperator of
R_NormSpace_of_BoundedBilinearOperators(X,Y,Z),
R_NormSpace_of_BoundedMultilinearOperators(<*X,Y*>,Z)
st I is bijective isometric
& for u be Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
holds I.u = u * (IsoCPNrSP(X,Y))"
proof
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 P1[Function,Function] means $2 = $1 * (IsoCPNrSP(X,Y))";
A1: for x being Element of F1
ex y being Element of F2 st P1[x,y]
proof
let x be Element of F1;
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 F2
by LOPBAN10:def 11;
take v;
thus thesis;
end;
consider I being Function of F1,F2 such that
A2: for x being Element of F1 holds P1[x,I.x] from FUNCT_2:sch 3(A1);
A3: for x1, x2 being object st x1 in F1 & x2 in F1
& I.x1 = I.x2 holds x1 = x2
proof
let x1, x2 be object;
assume
A4: x1 in F1 & x2 in F1 & I.x1 = I.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 thesis by A6,A7,FUNCT_2:17;
end;
for y being object st y in F2 holds
ex x being object st x in F1 & y = I.x
proof
let y be object;
assume y in F2; 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;
thus v in F1;
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;
end; then
A9: I is onto by FUNCT_2:10;
A12: for x,y be 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);
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, g = I.y, h = I.(x+y);
for xy be VECTOR of product <*X,Y*> holds h.xy = f.xy + g.xy
proof
let xy be VECTOR of product <*X,Y*>;
consider p be Point of X, q be Point of Y such that
A16: xy = <*p,q*> by PRVECT_3:19;
A17: f.xy = x.((IsoCPNrSP (X,Y)").xy) by A13,FUNCT_2:15
.= x.(p,q) by A16,NDIFF_7:18;
A18: g.xy = y.((IsoCPNrSP(X,Y)").xy ) by A14,FUNCT_2:15
.= y.(p,q) by A16,NDIFF_7:18;
h.xy = (x+y).((IsoCPNrSP(X,Y)").xy) by A15,FUNCT_2:15
.= (x+y).(p,q) by A16,NDIFF_7:18;
hence h.xy = f.xy + g.xy by A17,A18,LOPBAN_9:19;
end;
hence thesis by LOPBAN10:48;
end;
for x be Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z),
a be Real holds I.(a*x) = a * I.x
proof
let x be Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z),
a be Real;
A20: I.x = x * (IsoCPNrSP (X,Y))" by A2;
A21: I.(a*x) = (a*x) * (IsoCPNrSP(X,Y))" by A2;
set f = I.x, g = I.(a*x);
for xy be VECTOR of product <*X,Y*> holds g.xy = a * f.xy
proof
let xy be VECTOR of product <*X,Y*>;
consider p be Point of X, q be Point of Y such that
A22: xy = <*p,q*> by PRVECT_3:19;
A23: f.xy = x.((IsoCPNrSP (X,Y)").xy) by A20,FUNCT_2:15
.= x.(p,q) by A22,NDIFF_7:18;
g.xy = (a*x).((IsoCPNrSP(X,Y)").xy) by A21,FUNCT_2:15
.= (a*x).(p,q) by A22,NDIFF_7:18;
hence g.xy = a * f.xy by A23,LOPBAN_9:20;
end;
hence thesis by LOPBAN10:49;
end; then
reconsider 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;
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);
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 be object holds z in PreNorms(u1) iff z in PreNorms(v1)
proof
let z be object;
hereby
assume z in PreNorms(u1); then
consider x be VECTOR of X,y be 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;
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 be Element of dom <*X,Y*> holds ||.s.i.|| <= 1
proof
let i be Element of dom <*X,Y*>;
i = 1 or i = 2 by FINSEQ_1:2,TARSKI:def 2,A35;
hence thesis by A28;
end;
hence z in PreNorms(v1) by A28,A30;
end;
assume z in PreNorms(v1); then
consider s be VECTOR of product <*X,Y*> such that
A31: z = ||. v1.s .||
& for i be Element of dom <*X,Y*> holds ||.s.i.|| <= 1;
consider x be Point of X, y be 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;
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;
hence z in PreNorms(u1) by A31,A33;
end;
hence thesis by A26,A27,TARSKI:2;
end;
hence thesis by A2,NDIFF_7:7,A3,A9,FUNCT_2:19;
end;
theorem IS04A:
ex I be LinearOperator of
R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedLinearOperators(Y,Z)),
R_NormSpace_of_BoundedMultilinearOperators(<*X,Y*>,Z)
st I is bijective isometric
& for u be Point of R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedLinearOperators(Y,Z))
holds ||.u.|| = ||. I.u .||
& for x be Point of X,y be Point of Y holds (I.u).<*x,y*> = (u.x).y
proof
consider I be LinearOperator of
R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedLinearOperators(Y,Z)),
R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) such that
A1: I is bijective
& for u be Point of R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedLinearOperators(Y,Z))
holds ||.u.|| = ||. I.u .||
& for x be Point of X,y be Point of Y holds
(I.u).(x,y) = (u.x).y by LOPBAN_9:27;
consider J be LinearOperator of
R_NormSpace_of_BoundedBilinearOperators(X,Y,Z),
R_NormSpace_of_BoundedMultilinearOperators(<*X,Y*>,Z) such that
A2: J is bijective isometric
& for u be Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
holds J.u = u * (IsoCPNrSP(X,Y))" by IS03A;
reconsider K = J*I as LinearOperator of
R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedLinearOperators(Y,Z)),
R_NormSpace_of_BoundedMultilinearOperators(<*X,Y*>,Z) by LOPBAN_2:1;
take K;
thus K is bijective by A1,A2,FUNCT_2:27;
A3: for x being Element of R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedLinearOperators(Y,Z))
holds ||.K. x.|| = ||.x.||
proof
let x be Element of R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedLinearOperators(Y,Z));
thus ||. K.x .|| = ||. J.(I.x) .|| by FUNCT_2:15
.= ||. I.x .|| by A2,NDIFF_7:7
.= ||.x.|| by A1;
end;
hence K is isometric by NDIFF_7:7;
let u be Point of R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedLinearOperators(Y,Z));
thus ||.K.u.|| = ||.u.|| by A3;
let x be Point of X,y be Point of Y;
A4: K.u = J.(I.u) by FUNCT_2:15;
reconsider xy = <*x,y*> as Point of product <*X,Y*> by PRVECT_3:19;
thus (K.u).<*x,y*> = ((I.u) * (IsoCPNrSP (X,Y))").xy by A2,A4
.= (I.u).((IsoCPNrSP(X,Y))" .xy) by FUNCT_2:15
.= (I.u).(x,y) by NDIFF_7:18
.= (u.x).y by A1;
end;
theorem
for X,Y being RealNormSpace-Sequence,
Z being RealNormSpace
ex I be LinearOperator of R_NormSpace_of_BoundedLinearOperators
(product X,R_NormSpace_of_BoundedLinearOperators(product Y,Z)),
R_NormSpace_of_BoundedMultilinearOperators(<*product X,product Y*>,Z)
st I is bijective isometric
& for u be Point of R_NormSpace_of_BoundedLinearOperators
(product X,R_NormSpace_of_BoundedLinearOperators(product Y,Z ))
holds ||.u.|| = ||. I.u .||
& for x be Point of product X,y be Point of product Y
holds (I.u).<*x,y*> = (u.x).y by IS04A;