deffunc H_{1}( 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 ; :: thesis: 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 H_{1}(m,n); :: thesis: 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; :: thesis: ( ( 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 H_{1}(m,1) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds

||.si.|| <= K ; :: thesis: ||.s.|| <= n * K

reconsider s0 = s as Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def 9;

A13: for y being ExtReal st y in PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) holds

y <= n * K

not upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n)))) > n * K

hence ||.s.|| <= n * K by LOPBAN_1:30; :: thesis: verum

let m, n be non zero Element of NAT ; :: thesis: 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 H

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; :: thesis: ( ( 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 H

||.si.|| <= K ; :: thesis: ||.s.|| <= n * K

reconsider s0 = s as Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def 9;

A2: now :: thesis: for x being Point of (REAL-NS m) st ||.x.|| <= 1 holds

||.(s0 . x).|| <= n * K

set PreNormS = PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n)));||.(s0 . x).|| <= n * K

let x be Point of (REAL-NS m); :: thesis: ( ||.x.|| <= 1 implies ||.(s0 . x).|| <= n * K )

assume A3: ||.x.|| <= 1 ; :: thesis: ||.(s0 . x).|| <= n * K

A11: ( 1 <= 1 & 1 <= n ) by NAT_1:14;

then reconsider s1 = (Proj (1,n)) * s as Point of H_{1}(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; :: thesis: verum

end;assume A3: ||.x.|| <= 1 ; :: thesis: ||.(s0 . x).|| <= n * K

now :: thesis: for i being Element of NAT st 1 <= i & i <= n holds

||.((Proj (i,n)) . (s . x)).|| <= K * ||.x.||

then A10:
||.(s . x).|| <= n * (K * ||.x.||)
by Th16;||.((Proj (i,n)) . (s . x)).|| <= K * ||.x.||

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= n implies ||.((Proj (i,n)) . (s . x)).|| <= K * ||.x.|| )

assume A4: ( 1 <= i & i <= n ) ; :: thesis: ||.((Proj (i,n)) . (s . x)).|| <= K * ||.x.||

set si = (Proj (i,n)) * s;

reconsider si = (Proj (i,n)) * s as Point of H_{1}(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; :: thesis: verum

end;assume A4: ( 1 <= i & i <= n ) ; :: thesis: ||.((Proj (i,n)) . (s . x)).|| <= K * ||.x.||

set si = (Proj (i,n)) * s;

reconsider si = (Proj (i,n)) * s as Point of H

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; :: thesis: verum

A11: ( 1 <= 1 & 1 <= n ) by NAT_1:14;

then reconsider s1 = (Proj (1,n)) * s as Point of H

||.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; :: thesis: verum

A13: for y being ExtReal st y in PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) holds

y <= n * K

proof

A16:
PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) is bounded_above
let y be ExtReal; :: thesis: ( y in PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) implies y <= n * K )

assume A14: y in PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) ; :: thesis: y <= n * K

consider x being VECTOR of (REAL-NS m) such that

A15: ( y = ||.((modetrans (s,(REAL-NS m),(REAL-NS n))) . x).|| & ||.x.|| <= 1 ) by A14;

y = ||.(s0 . x).|| by A15, LOPBAN_1:29;

hence y <= n * K by A2, A15; :: thesis: verum

end;assume A14: y in PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) ; :: thesis: y <= n * K

consider x being VECTOR of (REAL-NS m) such that

A15: ( y = ||.((modetrans (s,(REAL-NS m),(REAL-NS n))) . x).|| & ||.x.|| <= 1 ) by A14;

y = ||.(s0 . x).|| by A15, LOPBAN_1:29;

hence y <= n * K by A2, A15; :: thesis: verum

proof

set UBPreNormS = upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))));
n * K is UpperBound of PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n)))
by A13, XXREAL_2:def 1;

hence PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) is bounded_above by XXREAL_2:def 10; :: thesis: verum

end;hence PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) is bounded_above by XXREAL_2:def 10; :: thesis: verum

not upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n)))) > n * K

proof

then
upper_bound (PreNorms s0) <= n * K
by LOPBAN_1:def 11;
assume A17:
upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n)))) > n * K
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

hence ||.s.|| <= n * K by LOPBAN_1:30; :: thesis: verum