:: 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 b1 being LinearOperator of [:X,Y:],(product <*X,Y*>) st
for x being Point of X
for y being Point of Y holds b1 . (x,y) = <*x,y*>
proof end;
uniqueness
for b1, b2 being LinearOperator of [:X,Y:],(product <*X,Y*>) st ( for x being Point of X
for y being Point of Y holds b1 . (x,y) = <*x,y*> ) & ( for x being Point of X
for y being Point of Y holds b2 . (x,y) = <*x,y*> ) holds
b1 = b2
proof end;
end;

:: deftheorem defISO defines IsoCPRLSP LOPBAN12:def 1 :
for X, Y being RealLinearSpace
for b3 being LinearOperator of [:X,Y:],(product <*X,Y*>) holds
( b3 = IsoCPRLSP (X,Y) iff for x being Point of X
for y being Point of Y holds b3 . (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 b1 being LinearOperator of [:X,Y:],(product <*X,Y*>) st b1 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 b1 being LinearOperator of (product <*X,Y*>),[:X,Y:] st b1 = f " holds
b1 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 b1 being LinearOperator of (product <*X,Y*>),[:X,Y:] st b1 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;