let X, Y, Z be RealNormSpace; :: thesis: for f being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))
for g being Lipschitzian BilinearOperator of X,Y,Z st g = f holds
for t being VECTOR of X
for s being VECTOR of Y holds ||.(g . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.||
let f be Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)); :: thesis: for g being Lipschitzian BilinearOperator of X,Y,Z st g = f holds
for t being VECTOR of X
for s being VECTOR of Y holds ||.(g . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.||
let g be Lipschitzian BilinearOperator of X,Y,Z; :: thesis: ( g = f implies for t being VECTOR of X
for s being VECTOR of Y holds ||.(g . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.|| )
assume A1: g = f ; :: thesis: for t being VECTOR of X
for s being VECTOR of Y holds ||.(g . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.||
now :: thesis: for t being VECTOR of X
for s being VECTOR of Y holds ||.(g . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.||
let t be VECTOR of X; :: thesis: for s being VECTOR of Y holds ||.(g . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.||
let s be VECTOR of Y; :: thesis: ||.(g . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.||
now :: thesis: ( ( ( t = 0. X or s = 0. Y ) & ||.(g . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.|| ) or ( t <> 0. X & s <> 0. Y & ||.(g . (t,s)).|| <= ||.f.|| * (||.t.|| * ||.s.||) ) )
per cases ( t = 0. X or s = 0. Y or ( t <> 0. X & s <> 0. Y ) ) ;
case A3: ( t = 0. X or s = 0. Y ) ; :: thesis: ||.(g . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.||
then A4: ( ||.t.|| = 0 or ||.s.|| = 0 ) ;
( t = 0 * t or s = 0 * s ) by A3;
then g . (t,s) = 0 * (g . (t,s)) by LOPBAN_8:12
.= 0. Z by RLVECT_1:10 ;
hence ||.(g . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.|| by A4; :: thesis: verum
end;
case A5: ( t <> 0. X & s <> 0. Y ) ; :: thesis: ||.(g . (t,s)).|| <= ||.f.|| * (||.t.|| * ||.s.||)
reconsider t1 = (||.t.|| ") * t as VECTOR of X ;
reconsider s1 = (||.s.|| ") * s as VECTOR of Y ;
A6: ( ||.t.|| <> 0 & ||.s.|| <> 0 ) by A5, NORMSP_0:def 5;
then A7: ||.t.|| * ||.s.|| <> 0 by XCMPLX_1:6;
A8: |.(||.t.|| ").| = |.(1 * (||.t.|| ")).|
.= |.(1 / ||.t.||).| by XCMPLX_0:def 9
.= 1 / ||.t.|| by ABSVALUE:def 1
.= 1 * (||.t.|| ") by XCMPLX_0:def 9
.= ||.t.|| " ;
A9: |.(||.s.|| ").| = |.(1 * (||.s.|| ")).|
.= |.(1 / ||.s.||).| by XCMPLX_0:def 9
.= 1 / ||.s.|| by ABSVALUE:def 1
.= 1 * (||.s.|| ") by XCMPLX_0:def 9
.= ||.s.|| " ;
A10: |.((||.t.|| * ||.s.||) ").| = |.((||.t.|| ") * (||.s.|| ")).| by XCMPLX_1:204
.= (||.t.|| ") * (||.s.|| ") by A8, A9, COMPLEX1:65
.= (||.t.|| * ||.s.||) " by XCMPLX_1:204 ;
A11: ||.t1.|| = |.(||.t.|| ").| * ||.t.|| by NORMSP_1:def 1
.= 1 by A6, A8, XCMPLX_0:def 7 ;
A12: ||.s1.|| = |.(||.s.|| ").| * ||.s.|| by NORMSP_1:def 1
.= 1 by A6, A9, XCMPLX_0:def 7 ;
||.(g . (t,s)).|| / (||.t.|| * ||.s.||) = ||.(g . (t,s)).|| * ((||.t.|| * ||.s.||) ") by XCMPLX_0:def 9
.= ||.(((||.t.|| * ||.s.||) ") * (g . (t,s))).|| by A10, NORMSP_1:def 1
.= ||.(((||.t.|| ") * (||.s.|| ")) * (g . (t,s))).|| by XCMPLX_1:204
.= ||.((||.t.|| ") * ((||.s.|| ") * (g . (t,s)))).|| by RLVECT_1:def 7
.= ||.((||.t.|| ") * (g . (t,s1))).|| by LOPBAN_8:12
.= ||.(g . (t1,s1)).|| by LOPBAN_8:12 ;
then ||.(g . (t,s)).|| / (||.t.|| * ||.s.||) in { ||.(g . (t,s)).|| where t is VECTOR of X, s is VECTOR of Y : ( ||.t.|| <= 1 & ||.s.|| <= 1 ) } by A11, A12;
then ||.(g . (t,s)).|| / (||.t.|| * ||.s.||) <= upper_bound (PreNorms g) by SEQ_4:def 1;
then A13: ||.(g . (t,s)).|| / (||.t.|| * ||.s.||) <= ||.f.|| by A1, Th30;
(||.(g . (t,s)).|| / (||.t.|| * ||.s.||)) * (||.t.|| * ||.s.||) = (||.(g . (t,s)).|| * ((||.t.|| * ||.s.||) ")) * (||.t.|| * ||.s.||) by XCMPLX_0:def 9
.= ||.(g . (t,s)).|| * (((||.t.|| * ||.s.||) ") * (||.t.|| * ||.s.||))
.= ||.(g . (t,s)).|| * 1 by A7, XCMPLX_0:def 7
.= ||.(g . (t,s)).|| ;
hence ||.(g . (t,s)).|| <= ||.f.|| * (||.t.|| * ||.s.||) by A13, XREAL_1:64; :: thesis: verum
end;
end;
end;
hence ||.(g . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.|| ; :: thesis: verum
end;
hence for t being VECTOR of X
for s being VECTOR of Y holds ||.(g . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.|| ; :: thesis: verum