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 open iff I .: Z is open )
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 open iff I .: Z is open )
let Z be Subset of S; :: thesis: ( I is one-to-one & I is onto & I is isometric implies ( Z is open iff I .: Z is open ) )
assume that
A1: ( I is one-to-one & I is onto ) and
A2: I is isometric ; :: thesis: ( Z is open iff I .: Z is open )
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;
Q2: I = J " by P2, A1, FUNCT_1:43;
Q3: J " Z = (J ") .: Z by P2, FUNCT_1:85
.= I .: Z by A1, P2, FUNCT_1:43 ;
A3: I .: (Z `) = J " (Z `) by Q2, P2, FUNCT_1:85
.= (I .: Z) ` by Q3, FUNCT_2:100 ;
thus ( Z is open iff I .: Z is open ) :: thesis: verum

proof

hereby :: thesis: ( I .: Z is open implies Z is open )

assume Z is open ; :: thesis: I .: Z is open
then Z ` is closed by NFCONT_1:def 4;
then (I .: Z) ` is closed by A1, A2, A3, LM024;
hence I .: Z is open by NFCONT_1:def 4; :: thesis: verum

end;

assume I .: Z is open ; :: thesis: Z is open
then I .: (Z `) is closed by A3, NFCONT_1:def 4;
then Z ` is closed by A1, A2, LM024;
hence Z is open by NFCONT_1:def 4; :: thesis: verum

end;