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 i being Nat st 1 <= i & i <= n holds
( Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) & (BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n)) <= 1 )
let s be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))); :: thesis: for i being Nat st 1 <= i & i <= n holds
( Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) & (BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n)) <= 1 )
let i be Nat; :: thesis: ( 1 <= i & i <= n implies ( Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) & (BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n)) <= 1 ) )
assume A1: ( 1 <= i & i <= n ) ; :: thesis: ( Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) & (BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n)) <= 1 )
A2: for y being Point of (REAL-NS n)
for r being Real holds (Proj (i,n)) . (r * y) = r * ((Proj (i,n)) . y) by PDIFF_6:27;
for y1, y2 being Point of (REAL-NS n) holds (Proj (i,n)) . (y1 + y2) = ((Proj (i,n)) . y1) + ((Proj (i,n)) . y2) by PDIFF_6:26;
hence A3: Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) by A2, LOPBAN_1:def 5, VECTSP_1:def 20; :: thesis: (BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n)) <= 1
deffunc H1( Nat, Nat) -> Element of K10(K11((BoundedLinearOperators ((REAL-NS $1),(REAL-NS $2))),REAL)) = BoundedLinearOperatorsNorm ((REAL-NS $1),(REAL-NS $2));
A4: Proj (i,n) in BoundedLinearOperators ((REAL-NS n),(REAL-NS 1)) by A3, LOPBAN_1:def 9;
set s0 = modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1));
upper_bound (PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1)))) <= 1
proof
A5: for x being Real st x in PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))) holds
x <= 1
proof
let x be Real; :: thesis: ( x in PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))) implies x <= 1 )
assume x in PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))) ; :: thesis: x <= 1
then consider y being VECTOR of (REAL-NS n) such that
A6: ( x = ||.((modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))) . y).|| & ||.y.|| <= 1 ) ;
A7: ||.((Proj (i,n)) . y).|| <= ||.y.|| by A1, Th3;
Proj (i,n) = modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1)) by A3, LOPBAN_1:29;
hence x <= 1 by A6, A7, XXREAL_0:2; :: thesis: verum
end;
A8: PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))) is bounded_above
proof
for x being ExtReal st x in PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))) holds
x <= 1 by A5;
then 1 is UpperBound of PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))) by XXREAL_2:def 1;
hence PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))) is bounded_above by XXREAL_2:def 10; :: thesis: verum
end;
assume A9: upper_bound (PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1)))) > 1 ; :: thesis: contradiction
set dif = (upper_bound (PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))))) - 1;
A10: (upper_bound (PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))))) - 1 > 0 by A9, XREAL_1:50;
ex w being Real st
( w in PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))) & (upper_bound (PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))))) - ((upper_bound (PreNorms (modetrans ((Proj (i,n)),(REAL-NS n),(REAL-NS 1))))) - 1) < w ) by A10, A8, SEQ_4:def 1;
hence contradiction by A5; :: thesis: verum
end;
hence (BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (i,n)) <= 1 by A4, LOPBAN_1:def 13; :: thesis: verum