let X, Y be non trivial RealBanachSpace; :: thesis: for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.(v - u).|| < s holds
||.((Inv v) - (Inv u)).|| < r ) )
let u be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( u is invertible implies for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.(v - u).|| < s holds
||.((Inv v) - (Inv u)).|| < r ) ) )
assume A1: u is invertible ; :: thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.(v - u).|| < s holds
||.((Inv v) - (Inv u)).|| < r ) )
let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.(v - u).|| < s holds
||.((Inv v) - (Inv u)).|| < r ) ) )
assume A2: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.(v - u).|| < s holds
||.((Inv v) - (Inv u)).|| < r ) )
set r0 = r / 2;
A3: ( 0 < r / 2 & r / 2 < r ) by A2, XREAL_1:215, XREAL_1:216;
set s1 = 1 / ||.(Inv u).||;
set AG = R_Normed_Algebra_of_BoundedLinearOperators X;
A5: 0 < ||.(Inv u).|| by A1, LM50;
then A6: 0 < 1 / ||.(Inv u).|| by XREAL_1:139;
set s2 = (1 / 2) / ||.(Inv u).||;
A7: 0 < (1 / 2) / ||.(Inv u).|| by A5, XREAL_1:139;
A8: 0 < ||.(Inv u).|| * ||.(Inv u).|| by A5, XREAL_1:129;
A9: 0 < (r / 2) / 2 by A3, XREAL_1:215;
set s3 = ((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||);
A10: 0 < ((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||) by A8, A9, XREAL_1:139;
set s4 = min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||));
A11: ( 0 < min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||)) & min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||)) <= 1 / ||.(Inv u).|| & min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||)) <= (1 / 2) / ||.(Inv u).|| ) by A6, A7, XXREAL_0:15, XXREAL_0:17;
set s = min ((min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||))),(((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||)));
B11: ( 0 < min ((min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||))),(((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||))) & min ((min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||))),(((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||))) <= min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||)) & min ((min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||))),(((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||))) <= ((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||) ) by A10, A11, XXREAL_0:15, XXREAL_0:17;
then A12: ( 0 < min ((min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||))),(((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||))) & min ((min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||))),(((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||))) <= 1 / ||.(Inv u).|| & min ((min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||))),(((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||))) <= (1 / 2) / ||.(Inv u).|| & min ((min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||))),(((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||))) <= ((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||) ) by A11, XXREAL_0:2;
take min ((min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||))),(((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||))) ; :: thesis: ( 0 < min ((min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||))),(((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||))) & ( for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.(v - u).|| < min ((min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||))),(((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||))) holds
||.((Inv v) - (Inv u)).|| < r ) )
thus 0 < min ((min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||))),(((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||))) by A10, A11, XXREAL_0:15; :: thesis: for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.(v - u).|| < min ((min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||))),(((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||))) holds
||.((Inv v) - (Inv u)).|| < r
let v be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( ||.(v - u).|| < min ((min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||))),(((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||))) implies ||.((Inv v) - (Inv u)).|| < r )
assume A13: ||.(v - u).|| < min ((min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||))),(((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||))) ; :: thesis: ||.((Inv v) - (Inv u)).|| < r
then ||.(v - u).|| < 1 / ||.(Inv u).|| by A12, XXREAL_0:2;
then consider w being Point of (R_Normed_Algebra_of_BoundedLinearOperators X), s, I being Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) such that
A14: ( w = (Inv u) * (v - u) & s = w & I = id X & ||.s.|| < 1 & (- w) GeoSeq is norm_summable & I + s is invertible & ||.(Inv (I + s)).|| <= 1 / (1 - ||.s.||) & Inv (I + s) = Sum ((- w) GeoSeq) & Inv v = (Inv (I + s)) * (Inv u) ) by A1, LMTh2;
reconsider sA = s as Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ;
A16: I * (Inv u) = (id X) * (modetrans ((Inv u),Y,X)) by A14, LOPBAN_1:def 11
.= modetrans ((Inv u),Y,X) by FUNCT_2:17
.= Inv u by LOPBAN_1:def 11 ;
reconsider IIu = I * (Inv u) as Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) ;
(Inv v) - (Inv u) = ((Inv (I + s)) - I) * (Inv u) by A14, A16, LM200;
then A18: ||.((Inv v) - (Inv u)).|| <= ||.((Inv (I + s)) - I).|| * ||.(Inv u).|| by NRM;
A19: (Inv (I + s)) * (I + s) = I by A14, LM400;
(Inv (I + s)) * I = (modetrans ((Inv (I + s)),X,X)) * (id X) by A14, LOPBAN_1:def 11
.= modetrans ((Inv (I + s)),X,X) by FUNCT_2:17
.= Inv (I + s) by LOPBAN_1:def 11 ;
then (Inv (I + s)) - I = (Inv (I + s)) * (I - (I + s)) by A19, LM100
.= (Inv (I + s)) * (- s) by LM300 ;
then ||.((Inv (I + s)) - I).|| <= ||.(Inv (I + s)).|| * ||.(- s).|| by NRM;
then A23: ||.((Inv (I + s)) - I).|| <= ||.(Inv (I + s)).|| * ||.s.|| by NORMSP_1:2;
A24: ||.s.|| <= ||.(Inv u).|| * ||.(v - u).|| by A14, NRM;
||.(Inv (I + s)).|| * ||.s.|| <= ||.(Inv (I + s)).|| * (||.(Inv u).|| * ||.(v - u).||) by A14, NRM, XREAL_1:64;
then A25: ||.((Inv (I + s)) - I).|| <= (||.(Inv (I + s)).|| * ||.(Inv u).||) * ||.(v - u).|| by A23, XXREAL_0:2;
||.(Inv (I + s)).|| * (||.(Inv u).|| * ||.(v - u).||) <= (1 / (1 - ||.s.||)) * (||.(Inv u).|| * ||.(v - u).||) by A14, XREAL_1:64;
then ||.((Inv (I + s)) - I).|| <= ((1 / (1 - ||.s.||)) * ||.(Inv u).||) * ||.(v - u).|| by A25, XXREAL_0:2;
then ||.((Inv (I + s)) - I).|| * ||.(Inv u).|| <= (((1 / (1 - ||.s.||)) * ||.(Inv u).||) * ||.(v - u).||) * ||.(Inv u).|| by XREAL_1:64;
then A29: ||.((Inv v) - (Inv u)).|| <= (((1 / (1 - ||.s.||)) * ||.(Inv u).||) * ||.(v - u).||) * ||.(Inv u).|| by A18, XXREAL_0:2;
||.(v - u).|| < (1 / 2) / ||.(Inv u).|| by A12, A13, XXREAL_0:2;
then ||.(Inv u).|| * ||.(v - u).|| <= ||.(Inv u).|| * ((1 / 2) / ||.(Inv u).||) by XREAL_1:64;
then ||.(Inv u).|| * ||.(v - u).|| <= 1 / 2 by A5, XCMPLX_1:87;
then ||.s.|| <= 1 / 2 by A24, XXREAL_0:2;
then 1 - (1 / 2) <= 1 - ||.s.|| by XREAL_1:10;
then 1 / (1 - ||.s.||) <= 1 / (1 / 2) by XREAL_1:118;
then A32: (1 / (1 - ||.s.||)) * ((||.(Inv u).|| * ||.(Inv u).||) * ||.(v - u).||) <= 2 * ((||.(Inv u).|| * ||.(Inv u).||) * ||.(v - u).||) by XREAL_1:64;
||.(v - u).|| < ((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||) by B11, A13, XXREAL_0:2;
then ||.(v - u).|| * (||.(Inv u).|| * ||.(Inv u).||) <= (((r / 2) / 2) / (||.(Inv u).|| * ||.(Inv u).||)) * (||.(Inv u).|| * ||.(Inv u).||) by XREAL_1:64;
then ||.(v - u).|| * (||.(Inv u).|| * ||.(Inv u).||) <= (r / 2) / 2 by A8, XCMPLX_1:87;
then 2 * (||.(Inv u).|| * (||.(Inv u).|| * ||.(v - u).||)) <= ((r / 2) / 2) * 2 by XREAL_1:64;
then (1 / (1 - ||.s.||)) * ((||.(Inv u).|| * ||.(Inv u).||) * ||.(v - u).||) <= r / 2 by A32, XXREAL_0:2;
then ||.((Inv v) - (Inv u)).|| <= r / 2 by A29, XXREAL_0:2;
hence ||.((Inv v) - (Inv u)).|| < r by A3, XXREAL_0:2; :: thesis: verum