let X, Y be non trivial RealBanachSpace; :: thesis: for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds
ex K, s being Real st
( 0 <= K & 0 < s & ( for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.du.|| < s holds
( u + du is invertible & ||.(((Inv (u + du)) - (Inv u)) - (- (((Inv u) * du) * (Inv u)))).|| <= K * (||.du.|| * ||.du.||) ) ) )
let u be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( u is invertible implies ex K, s being Real st
( 0 <= K & 0 < s & ( for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.du.|| < s holds
( u + du is invertible & ||.(((Inv (u + du)) - (Inv u)) - (- (((Inv u) * du) * (Inv u)))).|| <= K * (||.du.|| * ||.du.||) ) ) ) )
assume A1: u is invertible ; :: thesis: ex K, s being Real st
( 0 <= K & 0 < s & ( for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.du.|| < s holds
( u + du is invertible & ||.(((Inv (u + du)) - (Inv u)) - (- (((Inv u) * du) * (Inv u)))).|| <= K * (||.du.|| * ||.du.||) ) ) )
set s1 = 1 / ||.(Inv u).||;
set AG = R_Normed_Algebra_of_BoundedLinearOperators X;
A3: 0 < ||.(Inv u).|| by A1, LOPBAN13:12;
set s2 = (1 / 2) / ||.(Inv u).||;
A5: 0 < (1 / 2) / ||.(Inv u).|| by A3, XREAL_1:139;
set s12 = min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||));
A7: ( 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 A3, A5, XXREAL_0:15, XXREAL_0:17;
set K = ((2 * ||.(Inv u).||) * ||.(Inv u).||) * ||.(Inv u).||;
take ((2 * ||.(Inv u).||) * ||.(Inv u).||) * ||.(Inv u).|| ; :: thesis: ex s being Real st
( 0 <= ((2 * ||.(Inv u).||) * ||.(Inv u).||) * ||.(Inv u).|| & 0 < s & ( for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.du.|| < s holds
( u + du is invertible & ||.(((Inv (u + du)) - (Inv u)) - (- (((Inv u) * du) * (Inv u)))).|| <= (((2 * ||.(Inv u).||) * ||.(Inv u).||) * ||.(Inv u).||) * (||.du.|| * ||.du.||) ) ) )
take min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||)) ; :: thesis: ( 0 <= ((2 * ||.(Inv u).||) * ||.(Inv u).||) * ||.(Inv u).|| & 0 < min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||)) & ( for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.du.|| < min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||)) holds
( u + du is invertible & ||.(((Inv (u + du)) - (Inv u)) - (- (((Inv u) * du) * (Inv u)))).|| <= (((2 * ||.(Inv u).||) * ||.(Inv u).||) * ||.(Inv u).||) * (||.du.|| * ||.du.||) ) ) )
thus ( 0 <= ((2 * ||.(Inv u).||) * ||.(Inv u).||) * ||.(Inv u).|| & 0 < min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||)) ) by A3, A5, XXREAL_0:15; :: thesis: for du being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.du.|| < min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||)) holds
( u + du is invertible & ||.(((Inv (u + du)) - (Inv u)) - (- (((Inv u) * du) * (Inv u)))).|| <= (((2 * ||.(Inv u).||) * ||.(Inv u).||) * ||.(Inv u).||) * (||.du.|| * ||.du.||) )
let du be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( ||.du.|| < min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||)) implies ( u + du is invertible & ||.(((Inv (u + du)) - (Inv u)) - (- (((Inv u) * du) * (Inv u)))).|| <= (((2 * ||.(Inv u).||) * ||.(Inv u).||) * ||.(Inv u).||) * (||.du.|| * ||.du.||) ) )
assume A8: ||.du.|| < min ((1 / ||.(Inv u).||),((1 / 2) / ||.(Inv u).||)) ; :: thesis: ( u + du is invertible & ||.(((Inv (u + du)) - (Inv u)) - (- (((Inv u) * du) * (Inv u)))).|| <= (((2 * ||.(Inv u).||) * ||.(Inv u).||) * ||.(Inv u).||) * (||.du.|| * ||.du.||) )
then A9: ||.du.|| < 1 / ||.(Inv u).|| by A7, XXREAL_0:2;
hence u + du is invertible by A1, LOPBAN13:13; :: thesis: ||.(((Inv (u + du)) - (Inv u)) - (- (((Inv u) * du) * (Inv u)))).|| <= (((2 * ||.(Inv u).||) * ||.(Inv u).||) * ||.(Inv u).||) * (||.du.|| * ||.du.||)
consider w being Point of (R_Normed_Algebra_of_BoundedLinearOperators X), s, I being Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) such that
A11: ( w = (Inv u) * du & 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 (u + du) = (Inv (I + s)) * (Inv u) ) by A1, A9, LOPBAN13:13;
reconsider sA = s as Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ;
A13: I * (Inv u) = (id the carrier of X) * (modetrans ((Inv u),Y,X)) by A11, 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)) ;
set L = ((Inv u) * du) * (Inv u);
A14: ((Inv (u + du)) - (Inv u)) - (- (((Inv u) * du) * (Inv u))) = (((Inv (I + s)) * (Inv u)) - IIu) + (((Inv u) * du) * (Inv u)) by A11, A13, RLVECT_1:17
.= (((Inv (I + s)) - I) * (Inv u)) + (((Inv u) * du) * (Inv u)) by LOPBAN13:20 ;
A15: (Inv (I + s)) * (I + s) = I by A11, LOPBAN13:22;
(Inv (I + s)) * I = (modetrans ((Inv (I + s)),X,X)) * (id the carrier of X) by A11, LOPBAN_1:def 11
.= modetrans ((Inv (I + s)),X,X) by FUNCT_2:17
.= Inv (I + s) by LOPBAN_1:def 11 ;
then A17: (Inv (I + s)) - I = (Inv (I + s)) * (I - (I + s)) by A15, LOPBAN13:19
.= (Inv (I + s)) * (- ((Inv u) * du)) by A11, LOPBAN13:21 ;
then A19: ((Inv (I + s)) - I) * (Inv u) = (- ((Inv (I + s)) * ((Inv u) * du))) * (Inv u) by LOPBAN13:26
.= - (((Inv (I + s)) * ((Inv u) * du)) * (Inv u)) by LOPBAN13:26
.= - ((Inv (I + s)) * (((Inv u) * du) * (Inv u))) by LOPBAN13:10 ;
I * (((Inv u) * du) * (Inv u)) = (id the carrier of X) * (modetrans ((((Inv u) * du) * (Inv u)),Y,X)) by A11, LOPBAN_1:def 11
.= modetrans ((((Inv u) * du) * (Inv u)),Y,X) by FUNCT_2:17
.= ((Inv u) * du) * (Inv u) by LOPBAN_1:def 11 ;
then (- ((Inv (I + s)) * (((Inv u) * du) * (Inv u)))) + (((Inv u) * du) * (Inv u)) = (I * (((Inv u) * du) * (Inv u))) - ((Inv (I + s)) * (((Inv u) * du) * (Inv u)))
.= (I - (Inv (I + s))) * (((Inv u) * du) * (Inv u)) by LOPBAN13:20
.= (- ((Inv (I + s)) - I)) * (((Inv u) * du) * (Inv u)) by RLVECT_1:33
.= - (((Inv (I + s)) * (- ((Inv u) * du))) * (((Inv u) * du) * (Inv u))) by A17, LOPBAN13:26 ;
then ((Inv (u + du)) - (Inv u)) - (- (((Inv u) * du) * (Inv u))) = - ((- ((Inv (I + s)) * ((Inv u) * du))) * (((Inv u) * du) * (Inv u))) by A14, A19, LOPBAN13:26
.= - (- (((Inv (I + s)) * ((Inv u) * du)) * (((Inv u) * du) * (Inv u)))) by LOPBAN13:26
.= ((Inv (I + s)) * ((Inv u) * du)) * (((Inv u) * du) * (Inv u)) by RLVECT_1:17 ;
then A22: ||.(((Inv (u + du)) - (Inv u)) - (- (((Inv u) * du) * (Inv u)))).|| <= ||.((Inv (I + s)) * ((Inv u) * du)).|| * ||.(((Inv u) * du) * (Inv u)).|| by LOPBAN13:18;
A23: ||.((Inv (I + s)) * ((Inv u) * du)).|| <= ||.(Inv (I + s)).|| * ||.((Inv u) * du).|| by LOPBAN13:18;
||.(Inv (I + s)).|| * ||.((Inv u) * du).|| <= ||.(Inv (I + s)).|| * (||.(Inv u).|| * ||.du.||) by LOPBAN13:18, XREAL_1:64;
then A25: ||.((Inv (I + s)) * ((Inv u) * du)).|| <= ||.(Inv (I + s)).|| * (||.(Inv u).|| * ||.du.||) by A23, XXREAL_0:2;
A26: ||.((Inv u) * du).|| * ||.(Inv u).|| <= (||.(Inv u).|| * ||.du.||) * ||.(Inv u).|| by LOPBAN13:18, XREAL_1:64;
||.(((Inv u) * du) * (Inv u)).|| <= ||.((Inv u) * du).|| * ||.(Inv u).|| by LOPBAN13:18;
then ||.(((Inv u) * du) * (Inv u)).|| <= (||.(Inv u).|| * ||.du.||) * ||.(Inv u).|| by A26, XXREAL_0:2;
then ||.((Inv (I + s)) * ((Inv u) * du)).|| * ||.(((Inv u) * du) * (Inv u)).|| <= (||.(Inv (I + s)).|| * (||.(Inv u).|| * ||.du.||)) * ((||.(Inv u).|| * ||.du.||) * ||.(Inv u).||) by A25, XREAL_1:66;
then A28: ||.(((Inv (u + du)) - (Inv u)) - (- (((Inv u) * du) * (Inv u)))).|| <= (||.(Inv (I + s)).|| * (||.(Inv u).|| * ||.du.||)) * ((||.(Inv u).|| * ||.du.||) * ||.(Inv u).||) by A22, XXREAL_0:2;
A29: ||.s.|| <= ||.(Inv u).|| * ||.du.|| by A11, LOPBAN13:18;
||.du.|| < (1 / 2) / ||.(Inv u).|| by A7, A8, XXREAL_0:2;
then ||.(Inv u).|| * ||.du.|| <= ||.(Inv u).|| * ((1 / 2) / ||.(Inv u).||) by XREAL_1:64;
then ||.(Inv u).|| * ||.du.|| <= 1 / 2 by A3, XCMPLX_1:87;
then ||.s.|| <= 1 / 2 by A29, 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 ||.(Inv (I + s)).|| <= 2 by A11, XXREAL_0:2;
then ||.(Inv (I + s)).|| * ((||.(Inv u).|| * ||.du.||) * ((||.(Inv u).|| * ||.du.||) * ||.(Inv u).||)) <= 2 * ((||.(Inv u).|| * ||.du.||) * ((||.(Inv u).|| * ||.du.||) * ||.(Inv u).||)) by XREAL_1:64;
hence ||.(((Inv (u + du)) - (Inv u)) - (- (((Inv u) * du) * (Inv u)))).|| <= (((2 * ||.(Inv u).||) * ||.(Inv u).||) * ||.(Inv u).||) * (||.du.|| * ||.du.||) by A28, XXREAL_0:2; :: thesis: verum