:: by Kazuhisa Nakasho

::

:: Received May 27, 2019

:: Copyright (c) 2019 Association of Mizar Users

registration
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

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)

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;

ex b_{1} being LinearOperator of [:X,Y:],(product <*X,Y*>) st

for x being Point of X

for y being Point of Y holds b_{1} . (x,y) = <*x,y*>

for b_{1}, b_{2} being LinearOperator of [:X,Y:],(product <*X,Y*>) st ( for x being Point of X

for y being Point of Y holds b_{1} . (x,y) = <*x,y*> ) & ( for x being Point of X

for y being Point of Y holds b_{2} . (x,y) = <*x,y*> ) holds

b_{1} = b_{2}

end;
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 for x being Point of X

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

ex b

for x being Point of X

for y being Point of Y holds b

proof end;

uniqueness for b

for y being Point of Y holds b

for y being Point of Y holds b

b

proof end;

:: deftheorem defISO defines IsoCPRLSP LOPBAN12:def 1 :

for X, Y being RealLinearSpace

for b_{3} being LinearOperator of [:X,Y:],(product <*X,Y*>) holds

( b_{3} = IsoCPRLSP (X,Y) iff for x being Point of X

for y being Point of Y holds b_{3} . (x,y) = <*x,y*> );

for X, Y being RealLinearSpace

for b

( b

for y being Point of Y holds b

registration
end;

registration

let X, Y be RealLinearSpace;

existence

ex b_{1} being LinearOperator of [:X,Y:],(product <*X,Y*>) st b_{1} is bijective ;

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

proof 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 )

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

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

registration

let X, Y be RealLinearSpace;

let f be bijective LinearOperator of [:X,Y:],(product <*X,Y*>);

correctness

coherence

for b_{1} being LinearOperator of (product <*X,Y*>),[:X,Y:] st b_{1} = f " holds

b_{1} is bijective ;

end;
let f be bijective LinearOperator of [:X,Y:],(product <*X,Y*>);

correctness

coherence

for b

b

proof end;

registration

let X, Y be RealLinearSpace;

existence

ex b_{1} being LinearOperator of (product <*X,Y*>),[:X,Y:] st b_{1} is bijective ;

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

proof 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]

for x being Point of X

for y being Point of Y holds ((IsoCPRLSP (X,Y)) ") . <*x,y*> = [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

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

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)) ") ) )

( 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 ) )

( 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

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

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

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)) ") ) )

( 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 ) ) ) )

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

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;