:: Isomorphisms from the Space of Multilinear Operators
:: by Kazuhisa Nakasho
::
:: Received May 27, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users

registration

let G be RealLinearSpace-Sequence;

cluster product G -> constituted-FinSeqs ;

coherence
product G is constituted-FinSeqs

proof end;

end;

theorem LemmaA: :: LOPBAN12:1

for E, F being RealLinearSpace
for s being Element of (product <*E,F*>)
for i being Element of dom <*E,F*>
for x1 being object holds len (s +* (i,x1)) = 2

proof end;

theorem NDIFF5def4: :: LOPBAN12:2

for G being RealLinearSpace-Sequence
for i being Element of dom G
for x being Element of (product G)
for r being Element of (G . i) holds (reproj (i,x)) . r = x +* (i,r)

proof end;

definition

let X, Y be RealLinearSpace;

func IsoCPRLSP (X,Y) -> LinearOperator of [:X,Y:],(product <*X,Y*>) means :defISO: :: LOPBAN12:def 1
for x being Point of X
for y being Point of Y holds it . (x,y) = <*x,y*>;

existence
ex b₁ being LinearOperator of [:X,Y:],(product <*X,Y*>) st
for x being Point of X
for y being Point of Y holds b₁ . (x,y) = <*x,y*>

proof end;

uniqueness
for b₁, b₂ being LinearOperator of [:X,Y:],(product <*X,Y*>) st ( for x being Point of X
for y being Point of Y holds b₁ . (x,y) = <*x,y*> ) & ( for x being Point of X
for y being Point of Y holds b₂ . (x,y) = <*x,y*> ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defISO defines IsoCPRLSP LOPBAN12:def 1 :
for X, Y being RealLinearSpace
for b₃ being LinearOperator of [:X,Y:],(product <*X,Y*>) holds
( b₃ = IsoCPRLSP (X,Y) iff for x being Point of X
for y being Point of Y holds b₃ . (x,y) = <*x,y*> );

theorem ZeZe: :: LOPBAN12:3

for X, Y being RealLinearSpace holds 0. (product <*X,Y*>) = (IsoCPRLSP (X,Y)) . (0. [:X,Y:])

proof end;

registration

let X, Y be RealLinearSpace;

cluster IsoCPRLSP (X,Y) -> bijective ;

correctness
coherence
IsoCPRLSP (X,Y) is bijective ;

proof end;

end;

registration

let X, Y be RealLinearSpace;

cluster Relation-like the carrier of [:X,Y:] -defined the carrier of (product <*X,Y*>) -valued Function-like V11() V14( the carrier of [:X,Y:]) quasi_total bijective V166([:X,Y:], product <*X,Y*>) V167([:X,Y:], product <*X,Y*>) for Element of K19(K20( the carrier of [:X,Y:], the carrier of (product <*X,Y*>)));

correctness
existence
ex b₁ being LinearOperator of [:X,Y:],(product <*X,Y*>) st b₁ is bijective ;

proof end;

end;

theorem LM020: :: LOPBAN12:4

for S, T being RealLinearSpace
for I being LinearOperator of S,T st I is bijective holds
ex J being LinearOperator of T,S st
( J = I " & J is bijective )

proof end;

definition

let X, Y be RealLinearSpace;
let f be bijective LinearOperator of [:X,Y:],(product <*X,Y*>);
:: original: "
redefine func f " -> LinearOperator of (product <*X,Y*>),[:X,Y:];
correctness
coherence
f " is LinearOperator of (product <*X,Y*>),[:X,Y:];

proof 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
coherence
for b₁ being LinearOperator of (product <*X,Y*>),[:X,Y:] st b₁ = f " holds
b₁ is bijective ;

proof end;

end;

registration

let X, Y be RealLinearSpace;

cluster Relation-like the carrier of (product <*X,Y*>) -defined the carrier of [:X,Y:] -valued Function-like V11() V14( the carrier of (product <*X,Y*>)) quasi_total bijective V166( product <*X,Y*>,[:X,Y:]) V167( product <*X,Y*>,[:X,Y:]) for Element of K19(K20( the carrier of (product <*X,Y*>), the carrier of [:X,Y:]));

correctness
existence
ex b₁ being LinearOperator of (product <*X,Y*>),[:X,Y:] st b₁ is bijective ;

proof end;

end;

theorem defISOA1: :: LOPBAN12:5

for X, Y being RealLinearSpace
for x being Point of X
for y being Point of Y holds ((IsoCPRLSP (X,Y)) ") . <*x,y*> = [x,y]

proof end;

theorem :: LOPBAN12:6

for X, Y being RealLinearSpace holds ((IsoCPRLSP (X,Y)) ") . (0. (product <*X,Y*>)) = 0. [:X,Y:]

proof end;

theorem IS01: :: LOPBAN12:7

for E, F, G being RealLinearSpace
for u being MultilinearOperator of <*E,F*>,G holds u * (IsoCPRLSP (E,F)) is BilinearOperator of E,F,G

proof end;

theorem IS02: :: LOPBAN12:8

for E, F, G being RealLinearSpace
for u being BilinearOperator of E,F,G holds u * ((IsoCPRLSP (E,F)) ") is MultilinearOperator of <*E,F*>,G

proof end;

theorem IS03: :: LOPBAN12:9

for X, Y, Z being 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)) ") ) )

proof end;

theorem :: LOPBAN12:10

for X, Y, Z being RealLinearSpace ex I being 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 being Point of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z))))
for x being Point of X
for y being Point of Y holds (I . u) . <*x,y*> = (u . x) . y ) )

proof end;

theorem LemmaA: :: LOPBAN12:11

for E, F being RealNormSpace
for s being Point of (product <*E,F*>)
for i being Element of dom <*E,F*>
for x1 being object holds len (s +* (i,x1)) = 2

proof end;

theorem IS01A: :: LOPBAN12:12

for E, F, G being RealNormSpace
for u being Lipschitzian MultilinearOperator of <*E,F*>,G holds u * (IsoCPNrSP (E,F)) is Lipschitzian BilinearOperator of E,F,G

proof end;

theorem IS02A: :: LOPBAN12:13

for E, F, G being RealNormSpace
for u being Lipschitzian BilinearOperator of E,F,G holds u * ((IsoCPNrSP (E,F)) ") is Lipschitzian MultilinearOperator of <*E,F*>,G

proof end;

theorem IS03A: :: LOPBAN12:14

for X, Y, Z being 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)) ") ) )

proof end;

theorem IS04A: :: LOPBAN12:15

for X, Y, Z being RealNormSpace ex I being LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))),(R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z)) st
( I is bijective & I is isometric & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds
( ||.u.|| = ||.(I . u).|| & ( for x being Point of X
for y being Point of Y holds (I . u) . <*x,y*> = (u . x) . y ) ) ) )

proof end;

theorem :: LOPBAN12:16

for X, Y being RealNormSpace-Sequence
for Z being RealNormSpace ex I being 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 & I is isometric & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators ((product X),(R_NormSpace_of_BoundedLinearOperators ((product Y),Z)))) holds
( ||.u.|| = ||.(I . u).|| & ( for x being Point of (product X)
for y being Point of (product Y) holds (I . u) . <*x,y*> = (u . x) . y ) ) ) ) by IS04A;