let S, T be RealNormSpace; :: thesis: for I being LinearOperator of S,T
for Z being Subset of S st I is one-to-one & I is onto & I is isometric holds
( Z is compact iff I .: Z is compact )
let I be LinearOperator of S,T; :: thesis: for Z being Subset of S st I is one-to-one & I is onto & I is isometric holds
( Z is compact iff I .: Z is compact )
let Z be Subset of S; :: thesis: ( I is one-to-one & I is onto & I is isometric implies ( Z is compact iff I .: Z is compact ) )
assume that
A1: ( I is one-to-one & I is onto ) and
A2: I is isometric ; :: thesis: ( Z is compact iff I .: Z is compact )
consider J being LinearOperator of T,S such that
P2: ( J = I " & J is one-to-one & J is onto & J is isometric ) by A1, A2, LM020;
P1: dom I = the carrier of S by FUNCT_2:def 1;
thus ( Z is compact implies I .: Z is compact ) by LM026, A2; :: thesis: ( I .: Z is compact implies Z is compact )
thus ( I .: Z is compact implies Z is compact ) :: thesis: verum

proof

assume X2: I .: Z is compact ; :: thesis: Z is compact
J .: (I .: Z) = I " (I .: Z) by A1, P2, FUNCT_1:85
.= Z by FUNCT_1:94, P1, A1 ;
hence Z is compact by P2, X2, LM026; :: thesis: verum

end;