let V, W be RealNormSpace; for L being Lipschitzian LinearOperator of V,W ex QL being Lipschitzian LinearOperator of (NVectQuot (V,(Ker L))),(Im L) ex PQL being Point of (R_NormSpace_of_BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))) ex PL being Point of (R_NormSpace_of_BoundedLinearOperators (V,W)) st
( QL is onto & QL is one-to-one & L = PL & QL = PQL & ||.PL.|| = ||.PQL.|| & ( for z being Point of (NVectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
QL . z = L . v ) )
let L be Lipschitzian LinearOperator of V,W; ex QL being Lipschitzian LinearOperator of (NVectQuot (V,(Ker L))),(Im L) ex PQL being Point of (R_NormSpace_of_BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))) ex PL being Point of (R_NormSpace_of_BoundedLinearOperators (V,W)) st
( QL is onto & QL is one-to-one & L = PL & QL = PQL & ||.PL.|| = ||.PQL.|| & ( for z being Point of (NVectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
QL . z = L . v ) )
A1:
( the carrier of (Ker L) = L " {(0. W)} & L " {(0. W)} is closed )
by KERCL01, KLXY1, LCL1, LOPBAN_7:6;
reconsider V1 = V as RealLinearSpace ;
reconsider W1 = W as RealLinearSpace ;
reconsider L1 = L as LinearOperator of V1,W1 ;
A2:
( RLSStruct(# the carrier of (NVectQuot (V,(Ker L))), the ZeroF of (NVectQuot (V,(Ker L))), the addF of (NVectQuot (V,(Ker L))), the Mult of (NVectQuot (V,(Ker L))) #) = VectQuot (V,(Ker L)) & the normF of (NVectQuot (V,(Ker L))) = NormCoset (V,(Ker L)) )
by A1, defQuotN;
A3:
the carrier of (VectQuot (V,(Ker L))) = CosetSet (V,(Ker L))
by LMQ06;
consider QL1 being LinearOperator of (VectQuot (V1,(Ker L1))),(Im L1) such that
A4:
( QL1 is isomorphism & ( for z being Point of (VectQuot (V1,(Ker L1)))
for v being VECTOR of V1 st z = v + (Ker L1) holds
QL1 . z = L1 . v ) )
by LMQ21;
reconsider KL1 = Ker L1 as Subspace of V ;
A5:
RLSStruct(# the carrier of (NVectQuot (V,(Ker L))), the ZeroF of (NVectQuot (V,(Ker L))), the addF of (NVectQuot (V,(Ker L))), the Mult of (NVectQuot (V,(Ker L))) #) = VectQuot (V,KL1)
by A1, defQuotN;
reconsider QL = QL1 as Function of (NVectQuot (V,(Ker L))),(Im L) by A5;
A6:
for v, w being Element of (NVectQuot (V,(Ker L))) holds QL . (v + w) = (QL . v) + (QL . w)
for v being VECTOR of (NVectQuot (V,(Ker L)))
for r being Real holds QL . (r * v) = r * (QL . v)
then
( QL is additive & QL is homogeneous )
by A6, LOPBAN_1:def 5;
then reconsider QL = QL as LinearOperator of (NVectQuot (V,(Ker L))),(Im L) ;
A7:
R_NormSpace_of_BoundedLinearOperators (V,W) = NORMSTR(# (BoundedLinearOperators (V,W)),(Zero_ ((BoundedLinearOperators (V,W)),(R_VectorSpace_of_LinearOperators (V,W)))),(Add_ ((BoundedLinearOperators (V,W)),(R_VectorSpace_of_LinearOperators (V,W)))),(Mult_ ((BoundedLinearOperators (V,W)),(R_VectorSpace_of_LinearOperators (V,W)))),(BoundedLinearOperatorsNorm (V,W)) #)
by LOPBAN_1:def 14;
reconsider PL = L as Point of (R_NormSpace_of_BoundedLinearOperators (V,W)) by A7, LOPBAN_1:def 9;
A8:
for v being Point of (NVectQuot (V,(Ker L))) holds ||.(QL . v).|| <= ||.PL.|| * ||.v.||
reconsider QL = QL as Lipschitzian LinearOperator of (NVectQuot (V,(Ker L))),(Im L) by A8, LOPBAN_1:def 8;
take
QL
; ex PQL being Point of (R_NormSpace_of_BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))) ex PL being Point of (R_NormSpace_of_BoundedLinearOperators (V,W)) st
( QL is onto & QL is one-to-one & L = PL & QL = PQL & ||.PL.|| = ||.PQL.|| & ( for z being Point of (NVectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
QL . z = L . v ) )
A19:
R_NormSpace_of_BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L)) = NORMSTR(# (BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))),(Zero_ ((BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))),(R_VectorSpace_of_LinearOperators ((NVectQuot (V,(Ker L))),(Im L))))),(Add_ ((BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))),(R_VectorSpace_of_LinearOperators ((NVectQuot (V,(Ker L))),(Im L))))),(Mult_ ((BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))),(R_VectorSpace_of_LinearOperators ((NVectQuot (V,(Ker L))),(Im L))))),(BoundedLinearOperatorsNorm ((NVectQuot (V,(Ker L))),(Im L))) #)
by LOPBAN_1:def 14;
then reconsider PQL = QL as Point of (R_NormSpace_of_BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))) by LOPBAN_1:def 9;
A20:
PreNorms QL = { ||.(QL . t).|| where t is VECTOR of (NVectQuot (V,(Ker L))) : ||.t.|| <= 1 }
by LOPBAN_1:def 12;
then
upper_bound (PreNorms QL) <= ||.PL.||
by SEQ_4:45;
then A24:
||.PQL.|| <= ||.PL.||
by A19, LOPBAN_1:30;
R_NormSpace_of_BoundedLinearOperators (V,W) = NORMSTR(# (BoundedLinearOperators (V,W)),(Zero_ ((BoundedLinearOperators (V,W)),(R_VectorSpace_of_LinearOperators (V,W)))),(Add_ ((BoundedLinearOperators (V,W)),(R_VectorSpace_of_LinearOperators (V,W)))),(Mult_ ((BoundedLinearOperators (V,W)),(R_VectorSpace_of_LinearOperators (V,W)))),(BoundedLinearOperatorsNorm (V,W)) #)
by LOPBAN_1:def 14;
then A26:
||.PL.|| = upper_bound (PreNorms L)
by LOPBAN_1:30;
A27:
( not PreNorms L is empty & PreNorms L is bounded_above )
by LOPBAN_1:27;
A28:
PreNorms L = { ||.(L . t).|| where t is VECTOR of V : ||.t.|| <= 1 }
by LOPBAN_1:def 12;
now for s being Real st 0 < s holds
||.PL.|| <= ||.PQL.|| + (1 * s)let s be
Real;
( 0 < s implies ||.PL.|| <= ||.PQL.|| + (1 * s) )assume
0 < s
;
||.PL.|| <= ||.PQL.|| + (1 * s)then consider p being
Real such that A29:
(
p in PreNorms L &
||.PL.|| - s < p )
by A26, A27, SEQ_4:def 1;
consider vv1 being
VECTOR of
V such that A30:
p = ||.(L . vv1).||
and A31:
||.vv1.|| <= 1
by A28, A29;
A32:
lower_bound (NormVSets (V,(Ker L),vv1)) <= ||.vv1.||
by LMQ23;
reconsider v =
vv1 + (Ker L) as
Point of
(NVectQuot (V,(Ker L))) by A2, LMQ07;
||.v.|| = lower_bound (NormVSets (V,(Ker L),vv1))
by A2, DeNorm;
then A33:
||.v.|| <= 1
by A31, A32, XXREAL_0:2;
QL . v = L . vv1
by A4, A5;
then A34:
||.(QL . v).|| = ||.(L . vv1).||
by SUBTH0;
A35:
||.(QL . v).|| <= ||.PQL.|| * ||.v.||
by LOPBAN_1:32;
||.PQL.|| * ||.v.|| <= ||.PQL.|| * 1
by A33, XREAL_1:64;
then
||.(QL . v).|| <= ||.PQL.||
by A35, XXREAL_0:2;
then
||.PL.|| - s <= ||.PQL.||
by A29, A30, A34, XXREAL_0:2;
then
(||.PL.|| - s) + s <= ||.PQL.|| + s
by XREAL_1:6;
hence
||.PL.|| <= ||.PQL.|| + (1 * s)
;
verum end;
then
||.PL.|| <= ||.PQL.||
by LMINEQ;
hence
ex PQL being Point of (R_NormSpace_of_BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))) ex PL being Point of (R_NormSpace_of_BoundedLinearOperators (V,W)) st
( QL is onto & QL is one-to-one & L = PL & QL = PQL & ||.PL.|| = ||.PQL.|| & ( for z being Point of (NVectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
QL . z = L . v ) )
by A4, A5, A24, XXREAL_0:1; verum