let X, Y be ComplexNormSpace; :: thesis: for f being Point of (C_NormSpace_of_BoundedLinearOperators (X,Y))

for g being Lipschitzian LinearOperator of X,Y st g = f holds

for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||

let f be Point of (C_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: for g being Lipschitzian LinearOperator of X,Y st g = f holds

for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||

let g be Lipschitzian LinearOperator of X,Y; :: thesis: ( g = f implies for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.|| )

assume A1: g = f ; :: thesis: for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||

A2: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th26;

for g being Lipschitzian LinearOperator of X,Y st g = f holds

for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||

let f be Point of (C_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: for g being Lipschitzian LinearOperator of X,Y st g = f holds

for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||

let g be Lipschitzian LinearOperator of X,Y; :: thesis: ( g = f implies for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.|| )

assume A1: g = f ; :: thesis: for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||

A2: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th26;

now :: thesis: for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||

hence
for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||
; :: thesis: verumlet t be VECTOR of X; :: thesis: ||.(g . t).|| <= ||.f.|| * ||.t.||

end;now :: thesis: ( ( t = 0. X & ||.(g . t).|| <= ||.f.|| * ||.t.|| ) or ( t <> 0. X & ||.(g . t).|| <= ||.f.|| * ||.t.|| ) )end;

hence
||.(g . t).|| <= ||.f.|| * ||.t.||
; :: thesis: verumper cases
( t = 0. X or t <> 0. X )
;

end;

case A3:
t = 0. X
; :: thesis: ||.(g . t).|| <= ||.f.|| * ||.t.||

then A4:
||.t.|| = 0
by NORMSP_0:def 6;

g . t = g . (0c * (0. X)) by A3, CLVECT_1:1

.= 0c * (g . (0. X)) by Def3

.= 0. Y by CLVECT_1:1 ;

hence ||.(g . t).|| <= ||.f.|| * ||.t.|| by A4, NORMSP_0:def 6; :: thesis: verum

end;g . t = g . (0c * (0. X)) by A3, CLVECT_1:1

.= 0c * (g . (0. X)) by Def3

.= 0. Y by CLVECT_1:1 ;

hence ||.(g . t).|| <= ||.f.|| * ||.t.|| by A4, NORMSP_0:def 6; :: thesis: verum

case A5:
t <> 0. X
; :: thesis: ||.(g . t).|| <= ||.f.|| * ||.t.||

reconsider t0 = (||.t.|| ") + (0 * <i>) as Element of COMPLEX by XCMPLX_0:def 2;

reconsider t1 = t0 * t as VECTOR of X ;

A6: ||.t.|| <> 0 by A5, NORMSP_0:def 5;

then A7: ||.t.|| > 0 by CLVECT_1:105;

A8: |.t0.| = |.(1 * (||.t.|| ")).|

.= |.(1 / ||.t.||).| by XCMPLX_0:def 9

.= 1 / |.||.t.||.| by ABSVALUE:7

.= 1 / ||.t.|| by A7, ABSVALUE:def 1

.= 1 * (||.t.|| ") by XCMPLX_0:def 9

.= ||.t.|| " ;

then A9: ||.(g . t).|| / ||.t.|| = ||.(g . t).|| * |.t0.| by XCMPLX_0:def 9

.= ||.(t0 * (g . t)).|| by CLVECT_1:def 13

.= ||.(g . t1).|| by Def3 ;

||.t1.|| = |.t0.| * ||.t.|| by CLVECT_1:def 13

.= 1 by A6, A8, XCMPLX_0:def 7 ;

then ||.(g . t).|| / ||.t.|| in { ||.(g . s).|| where s is VECTOR of X : ||.s.|| <= 1 } by A9;

then ||.(g . t).|| / ||.t.|| <= upper_bound (PreNorms g) by A2, SEQ_4:def 1;

then ||.(g . t).|| / ||.t.|| <= (BoundedLinearOperatorsNorm (X,Y)) . g by Th29;

then A10: ||.(g . t).|| / ||.t.|| <= ||.f.|| by A1;

(||.(g . t).|| / ||.t.||) * ||.t.|| = (||.(g . t).|| * (||.t.|| ")) * ||.t.|| by XCMPLX_0:def 9

.= ||.(g . t).|| * ((||.t.|| ") * ||.t.||)

.= ||.(g . t).|| * 1 by A6, XCMPLX_0:def 7

.= ||.(g . t).|| ;

hence ||.(g . t).|| <= ||.f.|| * ||.t.|| by A7, A10, XREAL_1:64; :: thesis: verum

end;reconsider t1 = t0 * t as VECTOR of X ;

A6: ||.t.|| <> 0 by A5, NORMSP_0:def 5;

then A7: ||.t.|| > 0 by CLVECT_1:105;

A8: |.t0.| = |.(1 * (||.t.|| ")).|

.= |.(1 / ||.t.||).| by XCMPLX_0:def 9

.= 1 / |.||.t.||.| by ABSVALUE:7

.= 1 / ||.t.|| by A7, ABSVALUE:def 1

.= 1 * (||.t.|| ") by XCMPLX_0:def 9

.= ||.t.|| " ;

then A9: ||.(g . t).|| / ||.t.|| = ||.(g . t).|| * |.t0.| by XCMPLX_0:def 9

.= ||.(t0 * (g . t)).|| by CLVECT_1:def 13

.= ||.(g . t1).|| by Def3 ;

||.t1.|| = |.t0.| * ||.t.|| by CLVECT_1:def 13

.= 1 by A6, A8, XCMPLX_0:def 7 ;

then ||.(g . t).|| / ||.t.|| in { ||.(g . s).|| where s is VECTOR of X : ||.s.|| <= 1 } by A9;

then ||.(g . t).|| / ||.t.|| <= upper_bound (PreNorms g) by A2, SEQ_4:def 1;

then ||.(g . t).|| / ||.t.|| <= (BoundedLinearOperatorsNorm (X,Y)) . g by Th29;

then A10: ||.(g . t).|| / ||.t.|| <= ||.f.|| by A1;

(||.(g . t).|| / ||.t.||) * ||.t.|| = (||.(g . t).|| * (||.t.|| ")) * ||.t.|| by XCMPLX_0:def 9

.= ||.(g . t).|| * ((||.t.|| ") * ||.t.||)

.= ||.(g . t).|| * 1 by A6, XCMPLX_0:def 7

.= ||.(g . t).|| ;

hence ||.(g . t).|| <= ||.f.|| * ||.t.|| by A7, A10, XREAL_1:64; :: thesis: verum