let T be LinearOperator of X,Y; :: thesis: ( T is closed implies T is Lipschitzian )

assume A1: T is closed ; :: thesis: T is Lipschitzian

defpred S_{1}[ object , object ] means X = [Y,(T . Y)];

A2: for z being object st z in the carrier of (graphNSP T) holds

ex x being object st

( x in the carrier of X & S_{1}[z,x] )

A5: for z being object st z in the carrier of (graphNSP T) holds

S_{1}[z,J . z]
from FUNCT_2:sch 1(A2);

A6: graphNSP T is complete by Th11, A1;

A7: ( graphNSP T is Subspace of [:X,Y:] & the normF of (graphNSP T) = the normF of [:X,Y:] | the carrier of (graphNSP T) ) by Th9;

A8: for x being VECTOR of (graphNSP T)

for r being Real holds J . (r * x) = r * (J . x)

J is Lipschitzian

for y being object holds

( y in rng J iff y in the carrier of X )

then reconsider L = J " as Lipschitzian LinearOperator of X,(graphNSP T) by A17, Th7, A6;

consider K being Real such that

A19: ( 0 <= K & ( for x being VECTOR of X holds ||.(L . x).|| <= K * ||.x.|| ) ) by LOPBAN_1:def 8;

assume A1: T is closed ; :: thesis: T is Lipschitzian

defpred S

A2: for z being object st z in the carrier of (graphNSP T) holds

ex x being object st

( x in the carrier of X & S

proof

consider J being Function of (graphNSP T),X such that
let z be object ; :: thesis: ( z in the carrier of (graphNSP T) implies ex x being object st

( x in the carrier of X & S_{1}[z,x] ) )

assume A3: z in the carrier of (graphNSP T) ; :: thesis: ex x being object st

( x in the carrier of X & S_{1}[z,x] )

then consider x, y being object such that

A4: z = [x,y] by RELAT_1:def 1;

( x in dom T & y = T . x ) by FUNCT_1:1, A4, A3;

hence ex x being object st

( x in the carrier of X & S_{1}[z,x] )
by A4; :: thesis: verum

end;( x in the carrier of X & S

assume A3: z in the carrier of (graphNSP T) ; :: thesis: ex x being object st

( x in the carrier of X & S

then consider x, y being object such that

A4: z = [x,y] by RELAT_1:def 1;

( x in dom T & y = T . x ) by FUNCT_1:1, A4, A3;

hence ex x being object st

( x in the carrier of X & S

A5: for z being object st z in the carrier of (graphNSP T) holds

S

A6: graphNSP T is complete by Th11, A1;

A7: ( graphNSP T is Subspace of [:X,Y:] & the normF of (graphNSP T) = the normF of [:X,Y:] | the carrier of (graphNSP T) ) by Th9;

A8: for x being VECTOR of (graphNSP T)

for r being Real holds J . (r * x) = r * (J . x)

proof

for x, y being VECTOR of (graphNSP T) holds J . (x + y) = (J . x) + (J . y)
let x be VECTOR of (graphNSP T); :: thesis: for r being Real holds J . (r * x) = r * (J . x)

let r be Real; :: thesis: J . (r * x) = r * (J . x)

A9: x = [(J . x),(T . (J . x))] by A5;

A10: r * x = [(J . (r * x)),(T . (J . (r * x)))] by A5;

x in graph T ;

then reconsider x1 = x as Point of [:X,Y:] ;

r * x1 = r * x by A7, RLSUB_1:14;

then r * x = [(r * (J . x)),(r * (T . (J . x)))] by PRVECT_3:18, A9;

hence J . (r * x) = r * (J . x) by A10, XTUPLE_0:1; :: thesis: verum

end;let r be Real; :: thesis: J . (r * x) = r * (J . x)

A9: x = [(J . x),(T . (J . x))] by A5;

A10: r * x = [(J . (r * x)),(T . (J . (r * x)))] by A5;

x in graph T ;

then reconsider x1 = x as Point of [:X,Y:] ;

r * x1 = r * x by A7, RLSUB_1:14;

then r * x = [(r * (J . x)),(r * (T . (J . x)))] by PRVECT_3:18, A9;

hence J . (r * x) = r * (J . x) by A10, XTUPLE_0:1; :: thesis: verum

proof

then reconsider J = J as LinearOperator of (graphNSP T),X by A8, LOPBAN_1:def 5, VECTSP_1:def 20;
let x, y be VECTOR of (graphNSP T); :: thesis: J . (x + y) = (J . x) + (J . y)

A11: x = [(J . x),(T . (J . x))] by A5;

A12: y = [(J . y),(T . (J . y))] by A5;

A13: x + y = [(J . (x + y)),(T . (J . (x + y)))] by A5;

( x in graph T & y in graph T ) ;

then reconsider x1 = x, y1 = y as Point of [:X,Y:] ;

x1 + y1 = x + y by A7, RLSUB_1:13;

then x + y = [((J . x) + (J . y)),((T . (J . x)) + (T . (J . y)))] by PRVECT_3:18, A11, A12;

hence J . (x + y) = (J . x) + (J . y) by A13, XTUPLE_0:1; :: thesis: verum

end;A11: x = [(J . x),(T . (J . x))] by A5;

A12: y = [(J . y),(T . (J . y))] by A5;

A13: x + y = [(J . (x + y)),(T . (J . (x + y)))] by A5;

( x in graph T & y in graph T ) ;

then reconsider x1 = x, y1 = y as Point of [:X,Y:] ;

x1 + y1 = x + y by A7, RLSUB_1:13;

then x + y = [((J . x) + (J . y)),((T . (J . x)) + (T . (J . y)))] by PRVECT_3:18, A11, A12;

hence J . (x + y) = (J . x) + (J . y) by A13, XTUPLE_0:1; :: thesis: verum

J is Lipschitzian

proof
_{1} being Element of the carrier of (graphNSP T) holds ||.(J . b_{1}).|| <= 1 * ||.b_{1}.|| ) )

thus ( 0 <= 1 & ( for b_{1} being Element of the carrier of (graphNSP T) holds ||.(J . b_{1}).|| <= 1 * ||.b_{1}.|| ) )
by A14; :: thesis: verum

end;

then reconsider J = J as Lipschitzian LinearOperator of (graphNSP T),X ;A14: now :: thesis: for x being Point of (graphNSP T) holds ||.(J . x).|| <= 1 * ||.x.||

take
1
; :: according to LOPBAN_1:def 8 :: thesis: ( 0 <= 1 & ( for blet x be Point of (graphNSP T); :: thesis: ||.(J . x).|| <= 1 * ||.x.||

x in graph T ;

then reconsider x1 = x as Point of [:X,Y:] ;

A15: x1 = [(J . x),(T . (J . x))] by A5;

||.(J . x).|| <= ||.x1.|| by A15, Th15;

hence ||.(J . x).|| <= 1 * ||.x.|| by FUNCT_1:49; :: thesis: verum

end;x in graph T ;

then reconsider x1 = x as Point of [:X,Y:] ;

A15: x1 = [(J . x),(T . (J . x))] by A5;

||.(J . x).|| <= ||.x1.|| by A15, Th15;

hence ||.(J . x).|| <= 1 * ||.x.|| by FUNCT_1:49; :: thesis: verum

thus ( 0 <= 1 & ( for b

now :: thesis: for x, y being object st x in the carrier of (graphNSP T) & y in the carrier of (graphNSP T) & J . x = J . y holds

x = y

then A17:
J is one-to-one
by FUNCT_2:19;x = y

let x, y be object ; :: thesis: ( x in the carrier of (graphNSP T) & y in the carrier of (graphNSP T) & J . x = J . y implies x = y )

assume A16: ( x in the carrier of (graphNSP T) & y in the carrier of (graphNSP T) & J . x = J . y ) ; :: thesis: x = y

then reconsider x1 = x as Point of (graphNSP T) ;

x1 = [(J . x1),(T . (J . x1))] by A5;

hence x = y by A5, A16; :: thesis: verum

end;assume A16: ( x in the carrier of (graphNSP T) & y in the carrier of (graphNSP T) & J . x = J . y ) ; :: thesis: x = y

then reconsider x1 = x as Point of (graphNSP T) ;

x1 = [(J . x1),(T . (J . x1))] by A5;

hence x = y by A5, A16; :: thesis: verum

for y being object holds

( y in rng J iff y in the carrier of X )

proof

then
J is onto
by TARSKI:2;
let y be object ; :: thesis: ( y in rng J iff y in the carrier of X )

end;now :: thesis: ( y in the carrier of X implies y in rng J )

hence
( y in rng J iff y in the carrier of X )
; :: thesis: verumassume A18:
y in the carrier of X
; :: thesis: y in rng J

then reconsider y1 = y as Point of X ;

y1 in dom T by A18, FUNCT_2:def 1;

then reconsider x = [y1,(T . y1)] as Point of (graphNSP T) by FUNCT_1:1;

x = [(J . x),(T . (J . x))] by A5;

then y1 = J . x by XTUPLE_0:1;

hence y in rng J by FUNCT_2:112; :: thesis: verum

end;then reconsider y1 = y as Point of X ;

y1 in dom T by A18, FUNCT_2:def 1;

then reconsider x = [y1,(T . y1)] as Point of (graphNSP T) by FUNCT_1:1;

x = [(J . x),(T . (J . x))] by A5;

then y1 = J . x by XTUPLE_0:1;

hence y in rng J by FUNCT_2:112; :: thesis: verum

then reconsider L = J " as Lipschitzian LinearOperator of X,(graphNSP T) by A17, Th7, A6;

consider K being Real such that

A19: ( 0 <= K & ( for x being VECTOR of X holds ||.(L . x).|| <= K * ||.x.|| ) ) by LOPBAN_1:def 8;

now :: thesis: for y being Point of X holds ||.(T . y).|| <= K * ||.y.||

hence
T is Lipschitzian
by A19; :: thesis: verumlet y be Point of X; :: thesis: ||.(T . y).|| <= K * ||.y.||

y in the carrier of X ;

then y in dom T by FUNCT_2:def 1;

then reconsider x = [y,(T . y)] as Point of (graphNSP T) by FUNCT_1:1;

A20: x = [(J . x),(T . (J . x))] by A5;

A21: ||.(L . y).|| <= K * ||.y.|| by A19;

x in the carrier of (graphNSP T) ;

then A22: x in dom J by FUNCT_2:def 1;

A23: L . y = L . (J . x) by XTUPLE_0:1, A20

.= x by FUNCT_1:34, A17, A22 ;

reconsider x1 = x as Point of [:X,Y:] ;

||.x1.|| = ||.x.|| by FUNCT_1:49;

then ||.(T . y).|| <= ||.(L . y).|| by A23, Th15;

hence ||.(T . y).|| <= K * ||.y.|| by A21, XXREAL_0:2; :: thesis: verum

end;y in the carrier of X ;

then y in dom T by FUNCT_2:def 1;

then reconsider x = [y,(T . y)] as Point of (graphNSP T) by FUNCT_1:1;

A20: x = [(J . x),(T . (J . x))] by A5;

A21: ||.(L . y).|| <= K * ||.y.|| by A19;

x in the carrier of (graphNSP T) ;

then A22: x in dom J by FUNCT_2:def 1;

A23: L . y = L . (J . x) by XTUPLE_0:1, A20

.= x by FUNCT_1:34, A17, A22 ;

reconsider x1 = x as Point of [:X,Y:] ;

||.x1.|| = ||.x.|| by FUNCT_1:49;

then ||.(T . y).|| <= ||.(L . y).|| by A23, Th15;

hence ||.(T . y).|| <= K * ||.y.|| by A21, XXREAL_0:2; :: thesis: verum