:: Isomorphisms from the Space of Multilinear Operators
::  by Kazuhisa Nakasho
:: 
:: Received May 27, 2019
:: Copyright (c) 2019-2021 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;


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;
end;

theorem :: LOPBAN12:1
  for s being Element of product <*E,F*>,
      i being Element of dom <*E,F*>,
      x1 being object holds
  len(s +* (i,x1)) = 2;

theorem :: LOPBAN12:2
  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);

definition
  let X, Y be RealLinearSpace;
  func IsoCPRLSP(X,Y) -> LinearOperator of [:X,Y:],product <*X,Y*> means
:: LOPBAN12:def 1

  for x be Point of X, y be Point of Y holds it.(x,y) = <*x,y*>;
end;

theorem :: LOPBAN12:3
  for X, Y be RealLinearSpace holds
    0.product <*X,Y*> = IsoCPRLSP(X,Y).(0.[:X,Y:]);

registration
  let X, Y be RealLinearSpace;
  cluster IsoCPRLSP(X,Y) -> bijective;
end;

registration
  let X, Y be RealLinearSpace;
  cluster bijective for LinearOperator of [:X,Y:],product <*X,Y*>;
end;

theorem :: LOPBAN12:4
  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;

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:];
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:];
end;

registration
  let X, Y be RealLinearSpace;
  cluster bijective for LinearOperator of product <*X,Y*>,[:X,Y:];
end;

theorem :: LOPBAN12:5
  for X, Y be RealLinearSpace,
      x be Point of X, y be Point of Y holds
    (IsoCPRLSP(X,Y)").<*x,y*> = [x,y];

theorem :: LOPBAN12:6
  for X, Y be RealLinearSpace holds
    (IsoCPRLSP(X,Y)").(0. product <*X,Y*>) = 0.[:X,Y:];

theorem :: LOPBAN12:7
  for u be MultilinearOperator of <*E,F*>,G
  holds u * (IsoCPRLSP (E,F)) is BilinearOperator of E,F,G;

theorem :: LOPBAN12:8
  for u be BilinearOperator of E,F,G
  holds u * (IsoCPRLSP (E,F))" is MultilinearOperator of <*E,F*>,G;

theorem :: LOPBAN12:9
  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))";

theorem :: LOPBAN12:10
  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;

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 :: LOPBAN12:11
  for s being Point of product <*E,F*>,
      i being Element of dom <*E,F*>,
      x1 being object holds
  len(s +* (i,x1)) = 2;

theorem :: LOPBAN12:12
  for u be Lipschitzian MultilinearOperator of <*E,F*>,G holds
  u * (IsoCPNrSP(E,F)) is Lipschitzian BilinearOperator of E,F,G;

theorem :: LOPBAN12:13
  for u be Lipschitzian BilinearOperator of E,F,G
  holds u * (IsoCPNrSP(E,F))" is Lipschitzian MultilinearOperator of <*E,F*>,G;

theorem :: LOPBAN12:14
  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))";

theorem :: LOPBAN12:15
  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;

theorem :: LOPBAN12:16
  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;