deffunc H1( non zero Nat, non zero Nat) -> L16() = R_NormSpace_of_BoundedLinearOperators ((REAL-NS $1),(REAL-NS $2));
let m, n be non zero Element of NAT ; for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for K being Real st ( for i being Element of NAT
for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= K ) holds
||.s.|| <= n * K
let s be Point of H1(m,n); for K being Real st ( for i being Element of NAT
for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= K ) holds
||.s.|| <= n * K
let K be Real; ( ( for i being Element of NAT
for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= K ) implies ||.s.|| <= n * K )
assume A1:
for i being Element of NAT
for si being Point of H1(m,1) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= K
; ||.s.|| <= n * K
reconsider s0 = s as Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def 9;
A2:
now for x being Point of (REAL-NS m) st ||.x.|| <= 1 holds
||.(s0 . x).|| <= n * Klet x be
Point of
(REAL-NS m);
( ||.x.|| <= 1 implies ||.(s0 . x).|| <= n * K )assume A3:
||.x.|| <= 1
;
||.(s0 . x).|| <= n * Know for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . (s . x)).|| <= K * ||.x.||let i be
Element of
NAT ;
( 1 <= i & i <= n implies ||.((Proj (i,n)) . (s . x)).|| <= K * ||.x.|| )assume A4:
( 1
<= i &
i <= n )
;
||.((Proj (i,n)) . (s . x)).|| <= K * ||.x.||set si =
(Proj (i,n)) * s;
reconsider si =
(Proj (i,n)) * s as
Point of
H1(
m,1)
by Th7, A4;
reconsider sii =
si as
Lipschitzian LinearOperator of
(REAL-NS m),
(REAL-NS 1) by LOPBAN_1:def 9;
A5:
||.(sii . x).|| <= ||.si.|| * ||.x.||
by LOPBAN_1:32;
A6:
the
carrier of
(REAL-NS m) = REAL m
by REAL_NS1:def 4;
A7:
Proj (
i,
n) is
Lipschitzian LinearOperator of
(REAL-NS n),
(REAL-NS 1)
by A4, Th6;
s is
Lipschitzian LinearOperator of
(REAL-NS m),
(REAL-NS n)
by LOPBAN_1:def 9;
then
(Proj (i,n)) * s is
LinearOperator of
(REAL-NS m),
(REAL-NS 1)
by A7, LOPBAN_2:1;
then
dom ((Proj (i,n)) * s) = REAL m
by A6, FUNCT_2:def 1;
then A8:
sii . x = (Proj (i,n)) . (s . x)
by A6, FUNCT_1:12;
A9:
0 <= ||.x.||
by NORMSP_1:4;
||.si.|| * ||.x.|| <= K * ||.x.||
by A4, A1, A9, XREAL_1:64;
hence
||.((Proj (i,n)) . (s . x)).|| <= K * ||.x.||
by A5, A8, XXREAL_0:2;
verum end; then A10:
||.(s . x).|| <= n * (K * ||.x.||)
by Th16;
A11:
( 1
<= 1 & 1
<= n )
by NAT_1:14;
then reconsider s1 =
(Proj (1,n)) * s as
Point of
H1(
m,1)
by Th7;
||.s1.|| <= K
by A11, A1;
then A12:
0 <= K
by NORMSP_1:4;
(n * K) * ||.x.|| <= (n * K) * 1
by A12, A3, XREAL_1:64;
hence
||.(s0 . x).|| <= n * K
by A10, XXREAL_0:2;
verum end;
set PreNormS = PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n)));
A13:
for y being ExtReal st y in PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) holds
y <= n * K
A16:
PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) is bounded_above
set UBPreNormS = upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))));
not upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n)))) > n * K
proof
assume A17:
upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n)))) > n * K
;
contradiction
set dif =
(upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))))) - (n * K);
A18:
(upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))))) - (n * K) > 0
by A17, XREAL_1:50;
consider w being
Real such that A19:
(
w in PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) &
(upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))))) - ((upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))))) - (n * K)) < w )
by A18, A16, SEQ_4:def 1;
thus
contradiction
by A19, A13;
verum
end;
then
upper_bound (PreNorms s0) <= n * K
by LOPBAN_1:def 11;
hence
||.s.|| <= n * K
by LOPBAN_1:30; verum