let V be RealNormSpace; ( V is finite-dimensional & dim V <> 0 implies ex k1, k2 being Real ex S being LinearOperator of V,(REAL-NS (dim V)) st
( S is bijective & 0 <= k1 & 0 <= k2 & ( for x being Element of V holds
( ||.(S . x).|| <= k1 * ||.x.|| & ||.x.|| <= k2 * ||.(S . x).|| ) ) ) )
assume A1:
( V is finite-dimensional & dim V <> 0 )
; ex k1, k2 being Real ex S being LinearOperator of V,(REAL-NS (dim V)) st
( S is bijective & 0 <= k1 & 0 <= k2 & ( for x being Element of V holds
( ||.(S . x).|| <= k1 * ||.x.|| & ||.x.|| <= k2 * ||.(S . x).|| ) ) )
then consider S being LinearOperator of V,(REAL-NS (dim V)), W being finite-dimensional VectSp of F_Real , b being OrdBasis of W such that
A2:
( W = RLSp2RVSp V & S is bijective & ( for x being Element of W holds S . x = x |-- b ) )
by Th24;
reconsider V0 = V as finite-dimensional RealLinearSpace by A1;
reconsider b0 = b as OrdBasis of RLSp2RVSp V0 by A2;
RLSStruct(# the carrier of V0, the ZeroF of V0, the U5 of V0, the Mult of V0 #) = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #)
;
then consider k1, k2 being Real such that
A4:
( 0 < k1 & 0 < k2 & ( for x being Point of V holds
( ||.x.|| <= k1 * ((max_norm (V0,b0)) . x) & (max_norm (V0,b0)) . x <= k2 * ||.x.|| ) ) )
by Th25, A1;
A5:
now for x being Element of V holds
( ||.(S . x).|| <= ((dim V0) * k2) * ||.x.|| & ||.x.|| <= k1 * ||.(S . x).|| )let x be
Element of
V;
( ||.(S . x).|| <= ((dim V0) * k2) * ||.x.|| & ||.x.|| <= k1 * ||.(S . x).|| )reconsider Sx =
S . x as
Element of
REAL (dim V) by REAL_NS1:def 4;
consider x1 being
Element of
(RLSp2RVSp V0),
z1 being
Element of
REAL (dim V0) such that A6:
(
x = x1 &
z1 = x1 |-- b0 &
(euclid_norm (V0,b0)) . x = |.z1.| )
by Def5;
A8:
(euclid_norm (V0,b0)) . x = ||.(S . x).||
by A2, A6, REAL_NS1:1;
(
(sum_norm (V0,b0)) . x <= (dim V) * ((max_norm (V0,b0)) . x) &
(max_norm (V0,b0)) . x <= (euclid_norm (V0,b0)) . x &
(euclid_norm (V0,b0)) . x <= (sum_norm (V0,b0)) . x )
by Th22, A1;
then A9:
||.(S . x).|| <= (dim V0) * ((max_norm (V0,b0)) . x)
by A8, XXREAL_0:2;
(dim V0) * ((max_norm (V0,b0)) . x) <= (dim V0) * (k2 * ||.x.||)
by A4, XREAL_1:64;
hence
||.(S . x).|| <= ((dim V0) * k2) * ||.x.||
by A9, XXREAL_0:2;
||.x.|| <= k1 * ||.(S . x).||A10:
k1 * ((max_norm (V0,b0)) . x) <= k1 * ||.(S . x).||
by A1, A4, A8, Th22, XREAL_1:64;
||.x.|| <= k1 * ((max_norm (V0,b0)) . x)
by A4;
hence
||.x.|| <= k1 * ||.(S . x).||
by A10, XXREAL_0:2;
verum end;
set h1 = (dim V0) * k2;
take
(dim V0) * k2
; ex k2 being Real ex S being LinearOperator of V,(REAL-NS (dim V)) st
( S is bijective & 0 <= (dim V0) * k2 & 0 <= k2 & ( for x being Element of V holds
( ||.(S . x).|| <= ((dim V0) * k2) * ||.x.|| & ||.x.|| <= k2 * ||.(S . x).|| ) ) )
take
k1
; ex S being LinearOperator of V,(REAL-NS (dim V)) st
( S is bijective & 0 <= (dim V0) * k2 & 0 <= k1 & ( for x being Element of V holds
( ||.(S . x).|| <= ((dim V0) * k2) * ||.x.|| & ||.x.|| <= k1 * ||.(S . x).|| ) ) )
take
S
; ( S is bijective & 0 <= (dim V0) * k2 & 0 <= k1 & ( for x being Element of V holds
( ||.(S . x).|| <= ((dim V0) * k2) * ||.x.|| & ||.x.|| <= k1 * ||.(S . x).|| ) ) )
thus
S is bijective
by A2; ( 0 <= (dim V0) * k2 & 0 <= k1 & ( for x being Element of V holds
( ||.(S . x).|| <= ((dim V0) * k2) * ||.x.|| & ||.x.|| <= k1 * ||.(S . x).|| ) ) )
thus
( 0 <= (dim V0) * k2 & 0 <= k1 )
by A4; for x being Element of V holds
( ||.(S . x).|| <= ((dim V0) * k2) * ||.x.|| & ||.x.|| <= k1 * ||.(S . x).|| )
thus
for x being Element of V holds
( ||.(S . x).|| <= ((dim V0) * k2) * ||.x.|| & ||.x.|| <= k1 * ||.(S . x).|| )
by A5; verum