let V, W be RealNormSpace; :: thesis: for L being LinearOperator of V,W st L is one-to-one & L is onto & L is isometric-like holds
ex K being LinearOperator of W,V st
( K = L " & K is one-to-one & K is onto & K is isometric-like )
let L be LinearOperator of V,W; :: thesis: ( L is one-to-one & L is onto & L is isometric-like implies ex K being LinearOperator of W,V st
( K = L " & K is one-to-one & K is onto & K is isometric-like ) )
assume A1: ( L is one-to-one & L is onto & L is isometric-like ) ; :: thesis: ex K being LinearOperator of W,V st
( K = L " & K is one-to-one & K is onto & K is isometric-like )
consider K being LinearOperator of W,V such that
A2: ( K = L " & K is one-to-one & K is onto ) by A1, REAL_NS2:85;
take K ; :: thesis: ( K = L " & K is one-to-one & K is onto & K is isometric-like )
thus K = L " by A2; :: thesis: ( K is one-to-one & K is onto & K is isometric-like )
thus ( K is one-to-one & K is onto ) by A2; :: thesis: K is isometric-like
consider k1, k2 being Real such that
A3: ( 0 <= k1 & 0 <= k2 & ( for x being Element of V holds
( ||.(L . x).|| <= k1 * ||.x.|| & ||.x.|| <= k2 * ||.(L . x).|| ) ) ) by A1;
for y being Element of W holds
( ||.(K . y).|| <= k2 * ||.y.|| & ||.y.|| <= k1 * ||.(K . y).|| )
proof
let y be Element of W; :: thesis: ( ||.(K . y).|| <= k2 * ||.y.|| & ||.y.|| <= k1 * ||.(K . y).|| )
the carrier of W = rng L by A1, FUNCT_2:def 3;
then consider x being Element of the carrier of V such that
A4: y = L . x by FUNCT_2:113;
A5: K . y = x by A1, A2, A4, FUNCT_2:26;
hence ||.(K . y).|| <= k2 * ||.y.|| by A3, A4; :: thesis: ||.y.|| <= k1 * ||.(K . y).||
thus ||.y.|| <= k1 * ||.(K . y).|| by A3, A4, A5; :: thesis: verum
end;
hence K is isometric-like by A3; :: thesis: verum