let V be RealNormSpace; :: thesis: for W being finite-dimensional RealLinearSpace
for b being OrdBasis of RLSp2RVSp W st V is finite-dimensional & dim V <> 0 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = RLSStruct(# the carrier of W, the ZeroF of W, the U5 of W, the Mult of W #) holds
ex k1, k2 being Real st
( 0 < k1 & 0 < k2 & ( for x being Point of V holds
( ||.x.|| <= k1 * ((max_norm (W,b)) . x) & (max_norm (W,b)) . x <= k2 * ||.x.|| ) ) )
let W be finite-dimensional RealLinearSpace; :: thesis: for b being OrdBasis of RLSp2RVSp W st V is finite-dimensional & dim V <> 0 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = RLSStruct(# the carrier of W, the ZeroF of W, the U5 of W, the Mult of W #) holds
ex k1, k2 being Real st
( 0 < k1 & 0 < k2 & ( for x being Point of V holds
( ||.x.|| <= k1 * ((max_norm (W,b)) . x) & (max_norm (W,b)) . x <= k2 * ||.x.|| ) ) )
let b be OrdBasis of RLSp2RVSp W; :: thesis: ( V is finite-dimensional & dim V <> 0 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = RLSStruct(# the carrier of W, the ZeroF of W, the U5 of W, the Mult of W #) implies ex k1, k2 being Real st
( 0 < k1 & 0 < k2 & ( for x being Point of V holds
( ||.x.|| <= k1 * ((max_norm (W,b)) . x) & (max_norm (W,b)) . x <= k2 * ||.x.|| ) ) ) )
assume that
A1: ( V is finite-dimensional & dim V <> 0 ) and
A2: RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = RLSStruct(# the carrier of W, the ZeroF of W, the U5 of W, the Mult of W #) ; :: thesis: ex k1, k2 being Real st
( 0 < k1 & 0 < k2 & ( for x being Point of V holds
( ||.x.|| <= k1 * ((max_norm (W,b)) . x) & (max_norm (W,b)) . x <= k2 * ||.x.|| ) ) )
A4: (Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) by RLSUB_1:def 4
.= (Omega). W by A2, RLSUB_1:def 4 ;
A5: dim V = dim ((Omega). V) by A1, RLVECT_5:30
.= dim W by A4, RLVECT_5:30 ;
reconsider e = b as FinSequence of W ;
reconsider e1 = e as FinSequence of V by A2;
deffunc H1( Nat) -> Element of REAL = In (||.(e1 /. $1).||,REAL);
consider k being FinSequence of REAL such that
A6: ( len k = len b & ( for i being Nat st i in dom k holds
k . i = H1(i) ) ) from FINSEQ_2:sch 1();
 set k1 = Sum k;
for i being Nat st i in dom k holds
0 <= k . i
proof
let i be Nat; :: thesis: ( i in dom k implies 0 <= k . i )
assume i in dom k ; :: thesis: 0 <= k . i
then k . i = In (||.(e1 /. i).||,REAL) by A6
.= ||.(e1 /. i).|| ;
hence 0 <= k . i ; :: thesis: verum
end;
then A7: 0 <= Sum k by RVSUM_1:84;
A8: for x being Point of V holds ||.x.|| <= ((Sum k) + 1) * ((max_norm (W,b)) . x)
proof
let x0 be Point of V; :: thesis: ||.x0.|| <= ((Sum k) + 1) * ((max_norm (W,b)) . x0)
reconsider x = x0 as Point of W by A2;
consider y being Element of (RLSp2RVSp W), z being Element of REAL (dim W) such that
A9: ( x = y & z = y |-- b & (max_norm (W,b)) . x = (max_norm (dim W)) . z ) by Def3;
reconsider yb = y |-- b as FinSequence of REAL ;
A10: now :: thesis: for i being Nat st i in dom yb holds
|.(yb /. i).| <= (max_norm (W,b)) . x
let i be Nat; :: thesis: ( i in dom yb implies |.(yb /. i).| <= (max_norm (W,b)) . x )
assume A11: i in dom yb ; :: thesis: |.(yb /. i).| <= (max_norm (W,b)) . x
then i in dom (abs z) by A9, VALUED_1:def 11;
then (abs z) . i = |.(z . i).| by VALUED_1:def 11
.= |.(yb /. i).| by A9, A11, PARTFUN1:def 6 ;
hence |.(yb /. i).| <= (max_norm (W,b)) . x by A1, A5, A9, A11, Def1; :: thesis: verum
end;
A12: len (y |-- b) = len b by MATRLIN:def 7;
then dom (y |-- b) = Seg (len b) by FINSEQ_1:def 3
.= dom b by FINSEQ_1:def 3 ;
then A13: dom (lmlt ((y |-- b),b)) = dom (y |-- b) by MATRLIN:12
.= Seg (len b) by A12, FINSEQ_1:def 3 ;
reconsider f = the Mult of W .: (yb,e) as FinSequence of the carrier of W ;
reconsider f1 = f as FinSequence of V by A2;
A14: x = Sum (lmlt ((y |-- b),b)) by A9, MATRLIN:35
.= Sum f1 by A2 ;
A15: len f = len b by A13, FINSEQ_1:def 3;
deffunc H2( Nat) -> Element of REAL = In (||.(f1 /. $1).||,REAL);
consider g being FinSequence of REAL such that
A16: ( len g = len f & ( for i being Nat st i in dom g holds
g . i = H2(i) ) ) from FINSEQ_2:sch 1();
 A17: for i being Element of NAT st i in dom f1 holds
g . i = ||.(f1 /. i).||
proof
let i be Element of NAT ; :: thesis: ( i in dom f1 implies g . i = ||.(f1 /. i).|| )
assume i in dom f1 ; :: thesis: g . i = ||.(f1 /. i).||
then i in Seg (len f) by FINSEQ_1:def 3;
then i in dom g by A16, FINSEQ_1:def 3;
then g . i = In (||.(f1 /. i).||,REAL) by A16;
hence g . i = ||.(f1 /. i).|| ; :: thesis: verum
end;
then A18: ||.x0.|| <= Sum g by NDIFF_5:7, A14, A16;
A19: for i being Nat st i in Seg (len b) holds
g . i <= (((max_norm (W,b)) . x) * k) . i
proof
let i be Nat; :: thesis: ( i in Seg (len b) implies g . i <= (((max_norm (W,b)) . x) * k) . i )
assume A20: i in Seg (len b) ; :: thesis: g . i <= (((max_norm (W,b)) . x) * k) . i
A21: dom e = Seg (len b) by FINSEQ_1:def 3;
A22: dom yb = Seg (len b) by A12, FINSEQ_1:def 3;
then A23: yb . i = yb /. i by PARTFUN1:def 6, A20;
f1 /. i = f1 . i by A13, A20, PARTFUN1:def 6
.= the Mult of W . ((yb . i),(e . i)) by A13, A20, FUNCOP_1:22
.= (yb /. i) * (e1 /. i) by A2, A20, A21, A23, PARTFUN1:def 6 ;
then A24: g . i = ||.((yb /. i) * (e1 /. i)).|| by A13, A20, A17
.= |.(yb /. i).| * ||.(e1 /. i).|| by NORMSP_1:def 1 ;
A25: |.(yb /. i).| * ||.(e1 /. i).|| <= ((max_norm (W,b)) . x) * ||.(e1 /. i).|| by XREAL_1:64, A10, A20, A22;
i in dom k by A6, A20, FINSEQ_1:def 3;
then k . i = In (||.(e1 /. i).||,REAL) by A6
.= ||.(e1 /. i).|| ;
hence g . i <= (((max_norm (W,b)) . x) * k) . i by A24, A25, RVSUM_1:45; :: thesis: verum
end;
A26: g is len b -element by A15, A16, CARD_1:def 7;
dom (((max_norm (W,b)) . x) * k) = dom k by VALUED_1:def 5
.= Seg (len b) by A6, FINSEQ_1:def 3 ;
then len (((max_norm (W,b)) . x) * k) = len b by FINSEQ_1:def 3;
then ((max_norm (W,b)) . x) * k is len b -element by CARD_1:def 7;
then Sum g <= Sum (((max_norm (W,b)) . x) * k) by A19, A26, RVSUM_1:82;
then Sum g <= ((max_norm (W,b)) . x) * (Sum k) by RVSUM_1:87;
then A27: ||.x0.|| <= (Sum k) * ((max_norm (W,b)) . x0) by A18, XXREAL_0:2;
A28: 0 <= (max_norm (W,b)) . x by A1, A5, Th19;
(Sum k) + 0 < (Sum k) + 1 by XREAL_1:8;
then (Sum k) * ((max_norm (W,b)) . x0) <= ((Sum k) + 1) * ((max_norm (W,b)) . x0) by A28, XREAL_1:64;
hence ||.x0.|| <= ((Sum k) + 1) * ((max_norm (W,b)) . x0) by A27, XXREAL_0:2; :: thesis: verum
end;
consider S0 being LinearOperator of W,(REAL-NS (dim W)) such that
A29: ( S0 is bijective & ( for x being Element of (RLSp2RVSp W) holds S0 . x = x |-- b ) ) by A1, A5, Th23;
reconsider S = S0 as Function of the carrier of V, the carrier of (REAL-NS (dim W)) by A2;
for x, y being Element of V holds S . (x + y) = (S . x) + (S . y)
proof
let x, y be Element of V; :: thesis: S . (x + y) = (S . x) + (S . y)
reconsider x0 = x, y0 = y as Element of W by A2;
A30: x + y = x0 + y0 by A2;
S0 is additive ;
hence S . (x + y) = (S . x) + (S . y) by A30; :: thesis: verum
end;
then A32: S is additive ;
for a being Real
for x being VECTOR of V holds S . (a * x) = a * (S . x)
proof
let a be Real; :: thesis: for x being VECTOR of V holds S . (a * x) = a * (S . x)
let x be VECTOR of V; :: thesis: S . (a * x) = a * (S . x)
reconsider x0 = x as Element of W by A2;
a * x = a * x0 by A2;
hence S . (a * x) = a * (S . x) by LOPBAN_1:def 5; :: thesis: verum
end;
then S is homogeneous ;
then reconsider S = S as LinearOperator of V,(REAL-NS (dim W)) by A32;
consider T being LinearOperator of (REAL-NS (dim W)),V such that
A34: ( T = S " & T is one-to-one & T is onto ) by A29, REAL_NS2:85;
A35: for x being Element of V holds ||.x.|| <= ((Sum k) + 1) * ||.(S . x).||
proof
let x0 be Element of V; :: thesis: ||.x0.|| <= ((Sum k) + 1) * ||.(S . x0).||
reconsider x = x0 as Element of W by A2;
reconsider Sx = S . x0 as Element of REAL (dim W) by REAL_NS1:def 4;
consider x1 being Element of (RLSp2RVSp W), z1 being Element of REAL (dim W) such that
A36: ( x = x1 & z1 = x1 |-- b & (euclid_norm (W,b)) . x = |.z1.| ) by Def5;
(euclid_norm (W,b)) . x = ||.(S . x0).|| by A29, A36, REAL_NS1:1;
then A38: ((Sum k) + 1) * ((max_norm (W,b)) . x) <= ((Sum k) + 1) * ||.(S . x0).|| by A1, A5, A7, Th22, XREAL_1:64;
||.x0.|| <= ((Sum k) + 1) * ((max_norm (W,b)) . x0) by A8;
hence ||.x0.|| <= ((Sum k) + 1) * ||.(S . x0).|| by A38, XXREAL_0:2; :: thesis: verum
end;
for y being Element of (REAL-NS (dim W)) holds ||.(T . y).|| <= ((Sum k) + 1) * ||.y.||
proof
let y be Element of (REAL-NS (dim W)); :: thesis: ||.(T . y).|| <= ((Sum k) + 1) * ||.y.||
the carrier of (REAL-NS (dim W)) = rng S by A29, FUNCT_2:def 3;
then consider x being Element of the carrier of V such that
A39: y = S . x by FUNCT_2:113;
T . y = x by A29, A34, A39, FUNCT_2:26;
hence ||.(T . y).|| <= ((Sum k) + 1) * ||.y.|| by A35, A39; :: thesis: verum
end;
then A41: T is Lipschitzian by A7;
set CW = { y where y is Element of V : (max_norm (W,b)) . y = 1 } ;
set CR = { x where x is Element of (REAL-NS (dim W)) : (max_norm (dim W)) . x = 1 } ;
for z being object st z in { y where y is Element of V : (max_norm (W,b)) . y = 1 } holds
z in the carrier of V
proof
let z be object ; :: thesis: ( z in { y where y is Element of V : (max_norm (W,b)) . y = 1 } implies z in the carrier of V )
assume z in { y where y is Element of V : (max_norm (W,b)) . y = 1 } ; :: thesis: z in the carrier of V
then ex y being Element of V st
( z = y & (max_norm (W,b)) . y = 1 ) ;
hence z in the carrier of V ; :: thesis: verum
end;
then reconsider CW = { y where y is Element of V : (max_norm (W,b)) . y = 1 } as Subset of V by TARSKI:def 3;
for z being object st z in { x where x is Element of (REAL-NS (dim W)) : (max_norm (dim W)) . x = 1 } holds
z in the carrier of (REAL-NS (dim W))
proof
let z be object ; :: thesis: ( z in { x where x is Element of (REAL-NS (dim W)) : (max_norm (dim W)) . x = 1 } implies z in the carrier of (REAL-NS (dim W)) )
assume z in { x where x is Element of (REAL-NS (dim W)) : (max_norm (dim W)) . x = 1 } ; :: thesis: z in the carrier of (REAL-NS (dim W))
then ex y being Element of (REAL-NS (dim W)) st
( z = y & (max_norm (dim W)) . y = 1 ) ;
hence z in the carrier of (REAL-NS (dim W)) ; :: thesis: verum
end;
then reconsider CR = { x where x is Element of (REAL-NS (dim W)) : (max_norm (dim W)) . x = 1 } as Subset of (REAL-NS (dim W)) by TARSKI:def 3;
not REAL-NS (dim W) is trivial by A1, A5;
then consider zn being Point of (REAL-NS (dim W)) such that
A42: zn <> 0. (REAL-NS (dim W)) ;
reconsider znn = zn as Element of REAL (dim W) by REAL_NS1:def 4;
zn <> 0* (dim W) by A42, REAL_NS1:def 4;
then A43: (max_norm (dim W)) . znn <> 0 by A1, A5, Th12;
then A44: 0 < (max_norm (dim W)) . zn by A1, A5, Th12;
set yn = (1 / ((max_norm (dim W)) . zn)) * zn;
set a = 1 / ((max_norm (dim W)) . zn);
A45: (max_norm (dim W)) . ((1 / ((max_norm (dim W)) . zn)) * zn) = (max_norm (dim W)) . ((1 / ((max_norm (dim W)) . zn)) * znn) by REAL_NS1:3
.= |.(1 / ((max_norm (dim W)) . zn)).| * ((max_norm (dim W)) . znn) by A1, A5, Th12 ;
|.(1 / ((max_norm (dim W)) . zn)).| * ((max_norm (dim W)) . znn) = (1 / ((max_norm (dim W)) . zn)) * ((max_norm (dim W)) . zn) by A44, COMPLEX1:43
.= 1 by XCMPLX_1:106, A43 ;
then A46: (1 / ((max_norm (dim W)) . zn)) * zn in CR by A45;
A47: for y being object holds
( y in T .: CR iff y in CW )
proof
let y be object ; :: thesis: ( y in T .: CR iff y in CW )
hereby :: thesis: ( y in CW implies y in T .: CR )
assume y in T .: CR ; :: thesis: y in CW
then consider x being object such that
A48: ( x in dom T & x in CR & y = T . x ) by FUNCT_1:def 6;
reconsider x = x as Element of (REAL-NS (dim W)) by A48;
A49: ex x0 being Element of (REAL-NS (dim W)) st
( x = x0 & (max_norm (dim W)) . x0 = 1 ) by A48;
consider w being Element of (RLSp2RVSp W), z being Element of REAL (dim W) such that
A50: ( T . x = w & z = w |-- b & (max_norm (W,b)) . (T . x) = (max_norm (dim W)) . z ) by A2, Def3;
w in the carrier of V by A50;
then A51: w in dom S by FUNCT_2:def 1;
S . w = z by A29, A50;
then A52: T . z = w by A29, A34, A51, FUNCT_1:34;
z in REAL (dim W) ;
then A53: z in the carrier of (REAL-NS (dim W)) by REAL_NS1:def 4;
dom T = the carrier of (REAL-NS (dim W)) by FUNCT_2:def 1;
then z = x by A34, A50, A52, A53, FUNCT_1:def 4;
hence y in CW by A48, A49, A50; :: thesis: verum
end;
assume A54: y in CW ; :: thesis: y in T .: CR
then reconsider y0 = y as Element of V ;
A55: ex y0 being Element of V st
( y = y0 & (max_norm (W,b)) . y0 = 1 ) by A54;
consider w being Element of (RLSp2RVSp W), z being Element of REAL (dim W) such that
A56: ( y0 = w & z = w |-- b & (max_norm (W,b)) . y0 = (max_norm (dim W)) . z ) by A2, Def3;
w in the carrier of V by A56;
then A57: w in dom S by FUNCT_2:def 1;
z in REAL (dim W) ;
then A58: z in the carrier of (REAL-NS (dim W)) by REAL_NS1:def 4;
then A59: z in dom T by FUNCT_2:def 1;
S . w = z by A29, A56;
then A60: T . z = w by A29, A34, A57, FUNCT_1:34;
z in CR by A56, A55, A58;
hence y in T .: CR by A56, A59, A60, FUNCT_1:def 6; :: thesis: verum
end;
the carrier of (REAL-NS (dim W)) = REAL (dim W) by REAL_NS1:def 4;
then reconsider g = max_norm (dim W) as Function of the carrier of (REAL-NS (dim W)),REAL ;
set D = the carrier of (REAL-NS (dim W));
A63: dom g = the carrier of (REAL-NS (dim W)) by FUNCT_2:def 1;
A64: |.(- 1).| = |.1.| by COMPLEX1:52
.= 1 by COMPLEX1:43 ;
for x0 being Point of (REAL-NS (dim W))
for r being Real st x0 in the carrier of (REAL-NS (dim W)) & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS (dim W)) st x1 in the carrier of (REAL-NS (dim W)) & ||.(x1 - x0).|| < s holds
|.((g /. x1) - (g /. x0)).| < r ) )
proof
let x0 be Point of (REAL-NS (dim W)); :: thesis: for r being Real st x0 in the carrier of (REAL-NS (dim W)) & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS (dim W)) st x1 in the carrier of (REAL-NS (dim W)) & ||.(x1 - x0).|| < s holds
|.((g /. x1) - (g /. x0)).| < r ) )
let r be Real; :: thesis: ( x0 in the carrier of (REAL-NS (dim W)) & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS (dim W)) st x1 in the carrier of (REAL-NS (dim W)) & ||.(x1 - x0).|| < s holds
|.((g /. x1) - (g /. x0)).| < r ) ) )
assume A65: ( x0 in the carrier of (REAL-NS (dim W)) & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS (dim W)) st x1 in the carrier of (REAL-NS (dim W)) & ||.(x1 - x0).|| < s holds
|.((g /. x1) - (g /. x0)).| < r ) )
set s = r;
take r ; :: thesis: ( 0 < r & ( for x1 being Point of (REAL-NS (dim W)) st x1 in the carrier of (REAL-NS (dim W)) & ||.(x1 - x0).|| < r holds
|.((g /. x1) - (g /. x0)).| < r ) )
thus 0 < r by A65; :: thesis: for x1 being Point of (REAL-NS (dim W)) st x1 in the carrier of (REAL-NS (dim W)) & ||.(x1 - x0).|| < r holds
|.((g /. x1) - (g /. x0)).| < r
let x1 be Point of (REAL-NS (dim W)); :: thesis: ( x1 in the carrier of (REAL-NS (dim W)) & ||.(x1 - x0).|| < r implies |.((g /. x1) - (g /. x0)).| < r )
assume A66: ( x1 in the carrier of (REAL-NS (dim W)) & ||.(x1 - x0).|| < r ) ; :: thesis: |.((g /. x1) - (g /. x0)).| < r
A67: dom g = the carrier of (REAL-NS (dim W)) by FUNCT_2:def 1;
reconsider y0 = x0 as Element of REAL (dim W) by REAL_NS1:def 4;
reconsider y1 = x1 as Element of REAL (dim W) by REAL_NS1:def 4;
A68: ||.(x1 - x0).|| = |.(y1 - y0).| by REAL_NS1:1, REAL_NS1:5;
A69: (max_norm (dim W)) . (y1 - y0) <= |.(y1 - y0).| by A1, A5, Th14;
A70: x1 - x0 = y1 - y0 by REAL_NS1:5;
then A71: y0 + (y1 - y0) = x0 + (x1 - x0) by REAL_NS1:2
.= y1 by RLVECT_4:1 ;
A72: x0 - x1 = y0 - y1 by REAL_NS1:5;
then A73: y1 + (y0 - y1) = x1 + (x0 - x1) by REAL_NS1:2
.= y0 by RLVECT_4:1 ;
y0 - y1 = - (x1 - x0) by A72, RLVECT_1:33
.= (- 1) * (x1 - x0) by RLVECT_1:16
.= (- 1) * (y1 - y0) by A70, REAL_NS1:3 ;
then A74: (max_norm (dim W)) . (y0 - y1) = |.(- 1).| * ((max_norm (dim W)) . (y1 - y0)) by Th12, A1, A5
.= (max_norm (dim W)) . (y1 - y0) by A64 ;
A75: g . (y1 - y0) = g /. (y1 - y0) by A67, A70, PARTFUN1:def 6;
A76: g /. y1 = g . y1 by A67, PARTFUN1:def 6;
A77: g /. y0 = g . y0 by A67, PARTFUN1:def 6;
A78: ((max_norm (dim W)) . y1) - ((max_norm (dim W)) . y0) <= (((max_norm (dim W)) . y0) + ((max_norm (dim W)) . (y1 - y0))) - ((max_norm (dim W)) . y0) by A1, A5, A71, Th12, XREAL_1:9;
((max_norm (dim W)) . y1) - (((max_norm (dim W)) . y1) + ((max_norm (dim W)) . (y0 - y1))) <= ((max_norm (dim W)) . y1) - ((max_norm (dim W)) . y0) by A1, A5, A73, Th12, XREAL_1:10;
then - ((max_norm (dim W)) . (y1 - y0)) <= ((max_norm (dim W)) . y1) - ((max_norm (dim W)) . y0) by A74;
then |.((g /. y1) - (g /. y0)).| <= g /. (y1 - y0) by A75, A76, A77, A78, ABSVALUE:5;
then |.((g /. x1) - (g /. x0)).| <= ||.(x1 - x0).|| by A68, A69, A75, XXREAL_0:2;
hence |.((g /. x1) - (g /. x0)).| < r by A66, XXREAL_0:2; :: thesis: verum
end;
then A79: g is_continuous_on the carrier of (REAL-NS (dim W)) by A63, NFCONT_1:20;
for s1 being sequence of (REAL-NS (dim W)) st rng s1 c= CR & s1 is convergent holds
lim s1 in CR
proof
let s1 be sequence of (REAL-NS (dim W)); :: thesis: ( rng s1 c= CR & s1 is convergent implies lim s1 in CR )
assume A80: ( rng s1 c= CR & s1 is convergent ) ; :: thesis: lim s1 in CR
set D = the carrier of (REAL-NS (dim W));
A82: g is_continuous_in lim s1 by A79;
A83: dom s1 = NAT by FUNCT_2:def 1;
A81: the carrier of (REAL-NS (dim W)) = dom g by FUNCT_2:def 1;
then A84: rng s1 c= dom g ;
then A85: g /* s1 = g * s1 by FUNCT_2:def 11;
then A86: dom (g /* s1) = dom s1 by A84, RELAT_1:27;
for x, y being object st x in dom (g /* s1) & y in dom (g /* s1) holds
(g /* s1) . x = (g /* s1) . y
proof
let x, y be object ; :: thesis: ( x in dom (g /* s1) & y in dom (g /* s1) implies (g /* s1) . x = (g /* s1) . y )
assume A87: ( x in dom (g /* s1) & y in dom (g /* s1) ) ; :: thesis: (g /* s1) . x = (g /* s1) . y
then reconsider i = x, j = y as Element of NAT ;
i in dom s1 by A84, A85, A87, RELAT_1:27;
then s1 . i in rng s1 by FUNCT_1:3;
then s1 . i in CR by A80;
then ex x being Element of (REAL-NS (dim W)) st
( s1 . i = x & (max_norm (dim W)) . x = 1 ) ;
then A88: (g /* s1) . x = 1 by A84, FUNCT_2:108;
j in dom s1 by A87, A85, A84, RELAT_1:27;
then s1 . j in rng s1 by FUNCT_1:3;
then s1 . j in CR by A80;
then ex x being Element of (REAL-NS (dim W)) st
( s1 . j = x & (max_norm (dim W)) . x = 1 ) ;
hence (g /* s1) . x = (g /* s1) . y by A84, FUNCT_2:108, A88; :: thesis: verum
end;
then A89: g /* s1 is constant by FUNCT_1:def 10;
A90: ( (g /* s1) . 1 in rng (g /* s1) & (g /* s1) . 1 = g . (s1 . 1) ) by A83, A84, A86, FUNCT_1:3, FUNCT_2:108;
s1 . 1 in rng s1 by A83, FUNCT_1:3;
then s1 . 1 in CR by A80;
then A92: ex x being Element of (REAL-NS (dim W)) st
( s1 . 1 = x & (max_norm (dim W)) . x = 1 ) ;
(max_norm (dim W)) . (lim s1) = lim (g /* s1) by A80, A81, A82
.= 1 by A89, A90, A92, SEQ_4:25 ;
hence lim s1 in CR ; :: thesis: verum
end;
then A93: CR is closed ;
A95: 0 + (dim W) < 1 + (dim W) by XREAL_1:8;
A94: ex r being Real st
for y being Point of (REAL-NS (dim W)) st y in CR holds
||.y.|| < r
proof
set r = 1 + (dim W);
take 1 + (dim W) ; :: thesis: for y being Point of (REAL-NS (dim W)) st y in CR holds
||.y.|| < 1 + (dim W)
let y be Point of (REAL-NS (dim W)); :: thesis: ( y in CR implies ||.y.|| < 1 + (dim W) )
assume y in CR ; :: thesis: ||.y.|| < 1 + (dim W)
then A96: ex z being Element of (REAL-NS (dim W)) st
( y = z & (max_norm (dim W)) . z = 1 ) ;
reconsider y0 = y as Element of REAL (dim W) by REAL_NS1:def 4;
( (sum_norm (dim W)) . y0 <= (dim W) * ((max_norm (dim W)) . y0) & (max_norm (dim W)) . y0 <= |.y0.| & |.y0.| <= (sum_norm (dim W)) . y0 ) by A1, A5, Th14;
then |.y0.| <= (dim W) * ((max_norm (dim W)) . y0) by XXREAL_0:2;
then ||.y.|| <= dim W by A96, REAL_NS1:1;
hence ||.y.|| < 1 + (dim W) by A95, XXREAL_0:2; :: thesis: verum
end;
A97: T is_continuous_on CR by A41, LOPBAN_5:4, NFCONT_1:23;
CW = T .: CR by A47, TARSKI:2;
then A98: CW is compact by A93, A94, A97, Lm3, NFCONT_1:32;
reconsider f = id CW as PartFunc of V,V ;
dom f = CW ;
then A99: f is_continuous_on CW by NFCONT_1:50;
dom T = the carrier of (REAL-NS (dim W)) by FUNCT_2:def 1;
then A100: CW <> {} by A47, TARSKI:2, A46;
A101: dom f = dom ||.f.|| by NORMSP_0:def 3;
then A102: rng ||.f.|| is compact by A98, A99, NFCONT_1:28, NFCONT_1:31;
rng ||.f.|| <> {} by A101, A100, RELAT_1:42;
then consider y0 being Element of V such that
A104: ( y0 in dom ||.f.|| & lower_bound (rng ||.f.||) = ||.f.|| . y0 ) by A102, PARTFUN1:3, RCOMP_1:14;
A107: ||.f.|| . y0 = ||.(f /. y0).|| by A104, NORMSP_0:def 3;
rng ||.f.|| is real-bounded by A102, RCOMP_1:10;
then rng ||.f.|| is bounded_below by XXREAL_2:def 11;
then A105: for r being Real st r in rng ||.f.|| holds
||.f.|| . y0 <= r by A104, SEQ_4:def 2;
set k2 = ||.(f /. y0).||;
A108: for x being Element of V st x in CW holds
||.(f /. y0).|| <= ||.x.||
proof
let x be Element of V; :: thesis: ( x in CW implies ||.(f /. y0).|| <= ||.x.|| )
assume A109: x in CW ; :: thesis: ||.(f /. y0).|| <= ||.x.||
then f /. x = f . x by A101, PARTFUN1:def 6
.= x by A109, FUNCT_1:18 ;
then ||.f.|| . x = ||.x.|| by A101, A109, NORMSP_0:def 3;
hence ||.(f /. y0).|| <= ||.x.|| by A101, A105, A107, A109, FUNCT_1:3; :: thesis: verum
end;
A113: ||.(f /. y0).|| <> 0
proof
assume ||.(f /. y0).|| = 0 ; :: thesis: contradiction
then consider x being Element of V such that
A114: ( x in dom ||.f.|| & 0 = ||.f.|| . x ) by A104, A107;
||.f.|| . x = ||.(f /. x).|| by NORMSP_0:def 3, A114;
then f /. x = 0. V by A114, NORMSP_0:def 5;
then f . x = 0. V by A101, A114, PARTFUN1:def 6;
then 0. V in CW by A101, A114, FUNCT_1:18;
then A115: ex y being Element of V st
( y = 0. V & (max_norm (W,b)) . y = 1 ) ;
(max_norm (W,b)) . (0. V) = (max_norm (W,b)) . (0. W) by A2
.= 0 by A1, A5, Th19 ;
hence contradiction by A115; :: thesis: verum
end;
then A116: 0 < 1 / ||.(f /. y0).|| by XREAL_1:139;
for x being Point of V holds (max_norm (W,b)) . x <= (1 / ||.(f /. y0).||) * ||.x.||
proof
let x be Element of V; :: thesis: (max_norm (W,b)) . x <= (1 / ||.(f /. y0).||) * ||.x.||
reconsider xn = x as Element of W by A2;
per cases ( x = 0. V or x <> 0. V ) ;
suppose x = 0. V ; :: thesis: (max_norm (W,b)) . x <= (1 / ||.(f /. y0).||) * ||.x.||
then (max_norm (W,b)) . x = (max_norm (W,b)) . (0. W) by A2
.= 0 by A1, A5, Th19 ;
hence (max_norm (W,b)) . x <= (1 / ||.(f /. y0).||) * ||.x.|| ; :: thesis: verum
end;
suppose x <> 0. V ; :: thesis: (max_norm (W,b)) . x <= (1 / ||.(f /. y0).||) * ||.x.||
then xn <> 0. W by A2;
then A118: (max_norm (W,b)) . xn <> 0 by A1, A5, Th19;
then A119: 0 < (max_norm (W,b)) . xn by A1, A5, Th19;
set y = (1 / ((max_norm (W,b)) . x)) * x;
set a = 1 / ((max_norm (W,b)) . x);
(1 / ((max_norm (W,b)) . x)) * x = (1 / ((max_norm (W,b)) . x)) * xn by A2;
then A120: (max_norm (W,b)) . ((1 / ((max_norm (W,b)) . x)) * x) = |.(1 / ((max_norm (W,b)) . x)).| * ((max_norm (W,b)) . xn) by A1, A5, Th19;
|.(1 / ((max_norm (W,b)) . x)).| * ((max_norm (W,b)) . xn) = (1 / ((max_norm (W,b)) . x)) * ((max_norm (W,b)) . xn) by A119, COMPLEX1:43
.= 1 by A118, XCMPLX_1:106 ;
then (1 / ((max_norm (W,b)) . x)) * x in CW by A120;
then A123: ||.(f /. y0).|| * ((max_norm (W,b)) . x) <= ||.((1 / ((max_norm (W,b)) . x)) * x).|| * ((max_norm (W,b)) . x) by A108, XREAL_1:64, A119;
||.((1 / ((max_norm (W,b)) . x)) * x).|| = |.(1 / ((max_norm (W,b)) . x)).| * ||.x.|| by NORMSP_1:def 1
.= (1 / ((max_norm (W,b)) . x)) * ||.x.|| by A119, COMPLEX1:43 ;
then ||.((1 / ((max_norm (W,b)) . x)) * x).|| * ((max_norm (W,b)) . x) = ((1 / ((max_norm (W,b)) . x)) * ((max_norm (W,b)) . x)) * ||.x.||
.= 1 * ||.x.|| by A118, XCMPLX_1:106
.= ||.x.|| ;
then (1 / ||.(f /. y0).||) * (||.(f /. y0).|| * ((max_norm (W,b)) . x)) <= (1 / ||.(f /. y0).||) * ||.x.|| by A123, XREAL_1:64;
then ((1 / ||.(f /. y0).||) * ||.(f /. y0).||) * ((max_norm (W,b)) . x) <= (1 / ||.(f /. y0).||) * ||.x.|| ;
then 1 * ((max_norm (W,b)) . x) <= (1 / ||.(f /. y0).||) * ||.x.|| by A113, XCMPLX_1:106;
hence (max_norm (W,b)) . x <= (1 / ||.(f /. y0).||) * ||.x.|| ; :: thesis: verum
end;
end;
end;
hence ex k1, k2 being Real st
( 0 < k1 & 0 < k2 & ( for x being Point of V holds
( ||.x.|| <= k1 * ((max_norm (W,b)) . x) & (max_norm (W,b)) . x <= k2 * ||.x.|| ) ) ) by A7, A8, A116; :: thesis: verum