let E, F, G be RealNormSpace; for L being Point of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) ex L1 being Point of (R_NormSpace_of_BoundedLinearOperators (E,G)) ex L2 being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st
( ( for x being Point of E
for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y) ) & ( for x being Point of E holds L1 . x = L . [x,(0. F)] ) & ( for y being Point of F holds L2 . y = L . [(0. E),y] ) & ||.L.|| <= ||.L1.|| + ||.L2.|| & ||.L1.|| <= ||.L.|| & ||.L2.|| <= ||.L.|| )
let LP be Point of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)); ex L1 being Point of (R_NormSpace_of_BoundedLinearOperators (E,G)) ex L2 being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st
( ( for x being Point of E
for y being Point of F holds LP . [x,y] = (L1 . x) + (L2 . y) ) & ( for x being Point of E holds L1 . x = LP . [x,(0. F)] ) & ( for y being Point of F holds L2 . y = LP . [(0. E),y] ) & ||.LP.|| <= ||.L1.|| + ||.L2.|| & ||.L1.|| <= ||.LP.|| & ||.L2.|| <= ||.LP.|| )
reconsider L = LP as Lipschitzian LinearOperator of [:E,F:],G by LOPBAN_1:def 9;
consider L1 being Lipschitzian LinearOperator of E,G, L2 being Lipschitzian LinearOperator of F,G such that
A1:
for x being Point of E
for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y)
and
A2:
for x being Point of E holds L1 . x = L /. [x,(0. F)]
and
A3:
for y being Point of F holds L2 . y = L /. [(0. E),y]
by Th2;
reconsider LP1 = L1 as Point of (R_NormSpace_of_BoundedLinearOperators (E,G)) by LOPBAN_1:def 9;
reconsider LP2 = L2 as Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) by LOPBAN_1:def 9;
take
LP1
; ex L2 being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st
( ( for x being Point of E
for y being Point of F holds LP . [x,y] = (LP1 . x) + (L2 . y) ) & ( for x being Point of E holds LP1 . x = LP . [x,(0. F)] ) & ( for y being Point of F holds L2 . y = LP . [(0. E),y] ) & ||.LP.|| <= ||.LP1.|| + ||.L2.|| & ||.LP1.|| <= ||.LP.|| & ||.L2.|| <= ||.LP.|| )
take
LP2
; ( ( for x being Point of E
for y being Point of F holds LP . [x,y] = (LP1 . x) + (LP2 . y) ) & ( for x being Point of E holds LP1 . x = LP . [x,(0. F)] ) & ( for y being Point of F holds LP2 . y = LP . [(0. E),y] ) & ||.LP.|| <= ||.LP1.|| + ||.LP2.|| & ||.LP1.|| <= ||.LP.|| & ||.LP2.|| <= ||.LP.|| )
thus
for x being Point of E
for y being Point of F holds LP . [x,y] = (LP1 . x) + (LP2 . y)
by A1; ( ( for x being Point of E holds LP1 . x = LP . [x,(0. F)] ) & ( for y being Point of F holds LP2 . y = LP . [(0. E),y] ) & ||.LP.|| <= ||.LP1.|| + ||.LP2.|| & ||.LP1.|| <= ||.LP.|| & ||.LP2.|| <= ||.LP.|| )
thus
for x being Point of E holds LP1 . x = LP . [x,(0. F)]
( ( for y being Point of F holds LP2 . y = LP . [(0. E),y] ) & ||.LP.|| <= ||.LP1.|| + ||.LP2.|| & ||.LP1.|| <= ||.LP.|| & ||.LP2.|| <= ||.LP.|| )
thus
for y being Point of F holds LP2 . y = LP . [(0. E),y]
( ||.LP.|| <= ||.LP1.|| + ||.LP2.|| & ||.LP1.|| <= ||.LP.|| & ||.LP2.|| <= ||.LP.|| )
A7: ||.LP.|| =
upper_bound (PreNorms (modetrans (LP,[:E,F:],G)))
by LOPBAN_1:def 13
.=
upper_bound (PreNorms L)
by LOPBAN_1:29
;
for t being Real st t in PreNorms L holds
t <= ||.LP1.|| + ||.LP2.||
proof
let t be
Real;
( t in PreNorms L implies t <= ||.LP1.|| + ||.LP2.|| )
assume
t in PreNorms L
;
t <= ||.LP1.|| + ||.LP2.||
then consider w being
Point of
[:E,F:] such that A8:
(
t = ||.(L . w).|| &
||.w.|| <= 1 )
;
consider x being
Point of
E,
y being
Point of
F such that A9:
w = [x,y]
by PRVECT_3:18;
||.x.|| <= ||.w.||
by A9, NDIFF_8:21;
then A10:
||.x.|| <= 1
by A8, XXREAL_0:2;
||.y.|| <= ||.w.||
by A9, NDIFF_8:21;
then A11:
||.y.|| <= 1
by A8, XXREAL_0:2;
L . w = (L1 . x) + (L2 . y)
by A1, A9;
then A12:
||.(L . w).|| <= ||.(L1 . x).|| + ||.(L2 . y).||
by NORMSP_1:def 1;
A13:
||.(L1 . x).|| <= ||.LP1.|| * ||.x.||
by LOPBAN_1:32;
||.LP1.|| * ||.x.|| <= ||.LP1.|| * 1
by A10, XREAL_1:64;
then A14:
||.(L1 . x).|| <= ||.LP1.||
by A13, XXREAL_0:2;
A15:
||.(L2 . y).|| <= ||.LP2.|| * ||.y.||
by LOPBAN_1:32;
||.LP2.|| * ||.y.|| <= ||.LP2.|| * 1
by A11, XREAL_1:64;
then
||.(L2 . y).|| <= ||.LP2.||
by A15, XXREAL_0:2;
then
||.(L1 . x).|| + ||.(L2 . y).|| <= ||.LP1.|| + ||.LP2.||
by A14, XREAL_1:7;
hence
t <= ||.LP1.|| + ||.LP2.||
by A8, A12, XXREAL_0:2;
verum
end;
hence
||.LP.|| <= ||.LP1.|| + ||.LP2.||
by A7, SEQ_4:45; ( ||.LP1.|| <= ||.LP.|| & ||.LP2.|| <= ||.LP.|| )
A17: ||.LP1.|| =
upper_bound (PreNorms (modetrans (LP1,E,G)))
by LOPBAN_1:def 13
.=
upper_bound (PreNorms L1)
by LOPBAN_1:29
;
for t being Real st t in PreNorms L1 holds
t <= ||.LP.||
hence
||.LP1.|| <= ||.LP.||
by A17, SEQ_4:45; ||.LP2.|| <= ||.LP.||
A23: ||.LP2.|| =
upper_bound (PreNorms (modetrans (LP2,F,G)))
by LOPBAN_1:def 13
.=
upper_bound (PreNorms L2)
by LOPBAN_1:29
;
for t being Real st t in PreNorms L2 holds
t <= ||.LP.||
hence
||.LP2.|| <= ||.LP.||
by A23, SEQ_4:45; verum