let E, F, G be RealNormSpace; for u being Lipschitzian MultilinearOperator of <*E,F*>,G holds u * (IsoCPNrSP (E,F)) is Lipschitzian BilinearOperator of E,F,G
let u be Lipschitzian MultilinearOperator of <*E,F*>,G; u * (IsoCPNrSP (E,F)) is Lipschitzian BilinearOperator of E,F,G
reconsider L = u * (IsoCPNrSP (E,F)) as Function of [:E,F:],G ;
dom <*E,F*> =
Seg (len <*E,F*>)
by FINSEQ_1:def 3
.=
{1,2}
by FINSEQ_1:2, FINSEQ_1:44
;
then reconsider i1 = 1, i2 = 2 as Element of dom <*E,F*> by TARSKI:def 2;
A2:
for x1, x2 being Point of E
for y being Point of F holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))
proof
let x1,
x2 be
Point of
E;
for y being Point of F holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))let y be
Point of
F;
L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))
reconsider xy =
<*x1,y*> as
Point of
(product <*E,F*>) by PRVECT_3:19;
A3:
<*E,F*> . i1 = E
by FINSEQ_1:44;
then reconsider L1 =
u * (reproj (i1,xy)) as
LinearOperator of
E,
G by LOPBAN10:def 6;
A5:
dom (reproj (i1,xy)) =
the
carrier of
(<*E,F*> . i1)
by FUNCT_2:def 1
.=
the
carrier of
E
by FINSEQ_1:44
;
len xy = 2
by FINSEQ_1:44;
then
dom xy = {1,2}
by FINSEQ_1:2, FINSEQ_1:def 3;
then A7:
i1 in dom xy
by TARSKI:def 2;
A8:
len (xy +* (i1,(x1 + x2))) = 2
by LemmaA;
A9:
(xy +* (i1,(x1 + x2))) . 1
= x1 + x2
by A7, FUNCT_7:31;
A10:
(xy +* (i1,(x1 + x2))) . 2 =
xy . i2
by FUNCT_7:32
.=
y
by FINSEQ_1:44
;
reconsider x1x2 =
x1 + x2 as
Element of
(<*E,F*> . i1) by FINSEQ_1:44;
A12:
(reproj (i1,xy)) . x1x2 =
xy +* (
i1,
(x1 + x2))
by NDIFF_5:def 4
.=
<*(x1 + x2),y*>
by A8, A9, A10, FINSEQ_1:44
;
A13:
len (xy +* (i1,x1)) = 2
by LemmaA;
A14:
(xy +* (i1,x1)) . 1
= x1
by A7, FUNCT_7:31;
A15:
(xy +* (i1,x1)) . 2 =
xy . i2
by FUNCT_7:32
.=
y
by FINSEQ_1:44
;
A17:
(reproj (i1,xy)) . x1 =
xy +* (
i1,
x1)
by A3, NDIFF_5:def 4
.=
<*x1,y*>
by A13, A14, A15, FINSEQ_1:44
;
A18:
len (xy +* (i1,x2)) = 2
by LemmaA;
A19:
(xy +* (i1,x2)) . 1
= x2
by A7, FUNCT_7:31;
A20:
(xy +* (i1,x2)) . 2 =
xy . i2
by FUNCT_7:32
.=
y
by FINSEQ_1:44
;
A22:
(reproj (i1,xy)) . x2 =
xy +* (
i1,
x2)
by A3, NDIFF_5:def 4
.=
<*x2,y*>
by A18, A19, A20, FINSEQ_1:44
;
A4:
(
[(x1 + x2),y] is
Point of
[:E,F:] &
[x1,y] is
Point of
[:E,F:] &
[x2,y] is
Point of
[:E,F:] )
;
then A23:
L . (
(x1 + x2),
y) =
u . ((IsoCPNrSP (E,F)) . ((x1 + x2),y))
by FUNCT_2:15
.=
u . ((reproj (i1,xy)) . (x1 + x2))
by A12, NDIFF_7:def 3
.=
L1 . (x1 + x2)
by A5, FUNCT_1:13
;
A24:
L . (
x1,
y) =
u . ((IsoCPNrSP (E,F)) . (x1,y))
by A4, FUNCT_2:15
.=
u . ((reproj (i1,xy)) . x1)
by A17, NDIFF_7:def 3
.=
L1 . x1
by A5, FUNCT_1:13
;
L . (
x2,
y) =
u . ((IsoCPNrSP (E,F)) . (x2,y))
by A4, FUNCT_2:15
.=
u . ((reproj (i1,xy)) . x2)
by A22, NDIFF_7:def 3
.=
L1 . x2
by A5, FUNCT_1:13
;
hence
L . (
(x1 + x2),
y)
= (L . (x1,y)) + (L . (x2,y))
by A23, A24, VECTSP_1:def 20;
verum
end;
A26:
for x being Point of E
for y being Point of F
for a being Real holds L . ((a * x),y) = a * (L . (x,y))
proof
let x be
Point of
E;
for y being Point of F
for a being Real holds L . ((a * x),y) = a * (L . (x,y))let y be
Point of
F;
for a being Real holds L . ((a * x),y) = a * (L . (x,y))let a be
Real;
L . ((a * x),y) = a * (L . (x,y))
reconsider xy =
<*x,y*> as
Point of
(product <*E,F*>) by PRVECT_3:19;
A27:
<*E,F*> . i1 = E
by FINSEQ_1:44;
then reconsider L1 =
u * (reproj (i1,xy)) as
LinearOperator of
E,
G by LOPBAN10:def 6;
A29:
dom (reproj (i1,xy)) =
the
carrier of
(<*E,F*> . i1)
by FUNCT_2:def 1
.=
the
carrier of
E
by FINSEQ_1:44
;
len xy = 2
by FINSEQ_1:44;
then
dom xy = {1,2}
by FINSEQ_1:2, FINSEQ_1:def 3;
then A31:
i1 in dom xy
by TARSKI:def 2;
A32:
len (xy +* (i1,(a * x))) = 2
by LemmaA;
A33:
(xy +* (i1,(a * x))) . 1
= a * x
by A31, FUNCT_7:31;
A34:
(xy +* (i1,(a * x))) . 2 =
xy . i2
by FUNCT_7:32
.=
y
by FINSEQ_1:44
;
reconsider x1x2 =
a * x as
Element of
(<*E,F*> . i1) by FINSEQ_1:44;
A36:
(reproj (i1,xy)) . x1x2 =
xy +* (
i1,
(a * x))
by NDIFF_5:def 4
.=
<*(a * x),y*>
by A32, A33, A34, FINSEQ_1:44
;
A37:
len (xy +* (i1,x)) = 2
by LemmaA;
A38:
(xy +* (i1,x)) . 1
= x
by A31, FUNCT_7:31;
A39:
(xy +* (i1,x)) . 2 =
xy . i2
by FUNCT_7:32
.=
y
by FINSEQ_1:44
;
A41:
(reproj (i1,xy)) . x =
xy +* (
i1,
x)
by A27, NDIFF_5:def 4
.=
<*x,y*>
by A37, A38, A39, FINSEQ_1:44
;
A28:
(
[x,y] is
Point of
[:E,F:] &
[(a * x),y] is
Point of
[:E,F:] )
;
then A42:
L . (
(a * x),
y) =
u . ((IsoCPNrSP (E,F)) . ((a * x),y))
by FUNCT_2:15
.=
u . ((reproj (i1,xy)) . (a * x))
by A36, NDIFF_7:def 3
.=
L1 . (a * x)
by A29, FUNCT_1:13
;
L . (
x,
y) =
u . ((IsoCPNrSP (E,F)) . (x,y))
by A28, FUNCT_2:15
.=
u . ((reproj (i1,xy)) . x)
by A41, NDIFF_7:def 3
.=
L1 . x
by A29, FUNCT_1:13
;
hence
L . (
(a * x),
y)
= a * (L . (x,y))
by A42, LOPBAN_1:def 5;
verum
end;
A44:
for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))
proof
let x be
Point of
E;
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))let y1,
y2 be
Point of
F;
L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))
reconsider xy =
<*x,y1*> as
Point of
(product <*E,F*>) by PRVECT_3:19;
A45:
<*E,F*> . i2 = F
by FINSEQ_1:44;
then reconsider L1 =
u * (reproj (i2,xy)) as
LinearOperator of
F,
G by LOPBAN10:def 6;
A47:
dom (reproj (i2,xy)) =
the
carrier of
(<*E,F*> . i2)
by FUNCT_2:def 1
.=
the
carrier of
F
by FINSEQ_1:44
;
len xy = 2
by FINSEQ_1:44;
then
dom xy = {1,2}
by FINSEQ_1:2, FINSEQ_1:def 3;
then A49:
i2 in dom xy
by TARSKI:def 2;
A50:
len (xy +* (i2,(y1 + y2))) = 2
by LemmaA;
A51:
(xy +* (i2,(y1 + y2))) . 1 =
xy . i1
by FUNCT_7:32
.=
x
by FINSEQ_1:44
;
A52:
(xy +* (i2,(y1 + y2))) . 2
= y1 + y2
by A49, FUNCT_7:31;
reconsider x1x2 =
y1 + y2 as
Element of
(<*E,F*> . i2) by FINSEQ_1:44;
A54:
(reproj (i2,xy)) . x1x2 =
xy +* (
i2,
(y1 + y2))
by NDIFF_5:def 4
.=
<*x,(y1 + y2)*>
by A50, A51, A52, FINSEQ_1:44
;
A55:
len (xy +* (i2,y1)) = 2
by LemmaA;
A56:
(xy +* (i2,y1)) . 1 =
xy . i1
by FUNCT_7:32
.=
x
by FINSEQ_1:44
;
A57:
(xy +* (i2,y1)) . 2
= y1
by A49, FUNCT_7:31;
A59:
(reproj (i2,xy)) . y1 =
xy +* (
i2,
y1)
by A45, NDIFF_5:def 4
.=
<*x,y1*>
by A55, A56, A57, FINSEQ_1:44
;
A60:
len (xy +* (i2,y2)) = 2
by LemmaA;
A61:
(xy +* (i2,y2)) . 1 =
xy . i1
by FUNCT_7:32
.=
x
by FINSEQ_1:44
;
A62:
(xy +* (i2,y2)) . 2
= y2
by A49, FUNCT_7:31;
A64:
(reproj (i2,xy)) . y2 =
xy +* (
i2,
y2)
by A45, NDIFF_5:def 4
.=
<*x,y2*>
by A60, A61, A62, FINSEQ_1:44
;
A46:
(
[x,(y1 + y2)] is
Point of
[:E,F:] &
[x,y1] is
Point of
[:E,F:] &
[x,y2] is
Point of
[:E,F:] )
;
then A65:
L . (
x,
(y1 + y2)) =
u . ((IsoCPNrSP (E,F)) . (x,(y1 + y2)))
by FUNCT_2:15
.=
u . ((reproj (i2,xy)) . (y1 + y2))
by A54, NDIFF_7:def 3
.=
L1 . (y1 + y2)
by A47, FUNCT_1:13
;
A66:
L . (
x,
y1) =
u . ((IsoCPNrSP (E,F)) . (x,y1))
by A46, FUNCT_2:15
.=
u . ((reproj (i2,xy)) . y1)
by A59, NDIFF_7:def 3
.=
L1 . y1
by A47, FUNCT_1:13
;
L . (
x,
y2) =
u . ((IsoCPNrSP (E,F)) . (x,y2))
by A46, FUNCT_2:15
.=
u . ((reproj (i2,xy)) . y2)
by A64, NDIFF_7:def 3
.=
L1 . y2
by A47, FUNCT_1:13
;
hence
L . (
x,
(y1 + y2))
= (L . (x,y1)) + (L . (x,y2))
by A65, A66, VECTSP_1:def 20;
verum
end;
for x being Point of E
for y being Point of F
for a being Real holds L . (x,(a * y)) = a * (L . (x,y))
proof
let x be
Point of
E;
for y being Point of F
for a being Real holds L . (x,(a * y)) = a * (L . (x,y))let y be
Point of
F;
for a being Real holds L . (x,(a * y)) = a * (L . (x,y))let a be
Real;
L . (x,(a * y)) = a * (L . (x,y))
reconsider xy =
<*x,y*> as
Point of
(product <*E,F*>) by PRVECT_3:19;
A68:
<*E,F*> . i2 = F
by FINSEQ_1:44;
then reconsider L1 =
u * (reproj (i2,xy)) as
LinearOperator of
F,
G by LOPBAN10:def 6;
A70:
dom (reproj (i2,xy)) =
the
carrier of
(<*E,F*> . i2)
by FUNCT_2:def 1
.=
the
carrier of
F
by FINSEQ_1:44
;
len xy = 2
by FINSEQ_1:44;
then
dom xy = {1,2}
by FINSEQ_1:2, FINSEQ_1:def 3;
then A72:
i2 in dom xy
by TARSKI:def 2;
then A75:
(xy +* (i2,(a * y))) . 2
= a * y
by FUNCT_7:31;
A73:
len (xy +* (i2,(a * y))) = 2
by LemmaA;
A74:
(xy +* (i2,(a * y))) . 1 =
xy . i1
by FUNCT_7:32
.=
x
by FINSEQ_1:44
;
reconsider x1x2 =
a * y as
Element of
(<*E,F*> . i2) by FINSEQ_1:44;
A77:
(reproj (i2,xy)) . x1x2 =
xy +* (
i2,
(a * y))
by NDIFF_5:def 4
.=
<*x,(a * y)*>
by A73, A74, A75, FINSEQ_1:44
;
A78:
len (xy +* (i2,y)) = 2
by LemmaA;
A79:
(xy +* (i2,y)) . 1 =
xy . i1
by FUNCT_7:32
.=
x
by FINSEQ_1:44
;
A80:
(xy +* (i2,y)) . 2
= y
by A72, FUNCT_7:31;
A82:
(reproj (i2,xy)) . y =
xy +* (
i2,
y)
by A68, NDIFF_5:def 4
.=
<*x,y*>
by A78, A79, A80, FINSEQ_1:44
;
A69:
(
[x,y] is
Point of
[:E,F:] &
[x,(a * y)] is
Point of
[:E,F:] )
;
then A83:
L . (
x,
(a * y)) =
u . ((IsoCPNrSP (E,F)) . (x,(a * y)))
by FUNCT_2:15
.=
u . ((reproj (i2,xy)) . (a * y))
by A77, NDIFF_7:def 3
.=
L1 . (a * y)
by A70, FUNCT_1:13
;
L . (
x,
y) =
u . ((IsoCPNrSP (E,F)) . (x,y))
by A69, FUNCT_2:15
.=
u . ((reproj (i2,xy)) . y)
by A82, NDIFF_7:def 3
.=
L1 . y
by A70, FUNCT_1:13
;
hence
L . (
x,
(a * y))
= a * (L . (x,y))
by A83, LOPBAN_1:def 5;
verum
end;
then reconsider L = L as BilinearOperator of E,F,G by A2, A26, A44, LOPBAN_8:12;
ex K being Real st
( 0 <= K & ( for x being VECTOR of E
for y being VECTOR of F holds ||.(L . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) )
proof
consider K being
Real such that A85:
(
0 <= K & ( for
s being
Point of
(product <*E,F*>) holds
||.(u . s).|| <= K * (NrProduct s) ) )
by LOPBAN10:def 10;
take
K
;
( 0 <= K & ( for x being VECTOR of E
for y being VECTOR of F holds ||.(L . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) )
thus
0 <= K
by A85;
for x being VECTOR of E
for y being VECTOR of F holds ||.(L . (x,y)).|| <= (K * ||.x.||) * ||.y.||
let x be
VECTOR of
E;
for y being VECTOR of F holds ||.(L . (x,y)).|| <= (K * ||.x.||) * ||.y.||let y be
VECTOR of
F;
||.(L . (x,y)).|| <= (K * ||.x.||) * ||.y.||
reconsider xy =
<*x,y*> as
Point of
(product <*E,F*>) by PRVECT_3:19;
[x,y] is
Point of
[:E,F:]
;
then A87:
L . (
x,
y) =
u . ((IsoCPNrSP (E,F)) . (x,y))
by FUNCT_2:15
.=
u . <*x,y*>
by NDIFF_7:def 3
;
reconsider s =
<*x,y*> as
Point of
(product <*E,F*>) by PRVECT_3:19;
consider Nx being
FinSequence of
REAL such that A88:
(
dom Nx = dom <*E,F*> & ( for
i being
Element of
dom <*E,F*> holds
Nx . i = ||.(s . i).|| ) &
NrProduct s = Product Nx )
by LOPBAN10:def 9;
dom Nx =
Seg (len <*E,F*>)
by A88, FINSEQ_1:def 3
.=
Seg 2
by FINSEQ_1:44
;
then A89:
len Nx = 2
by FINSEQ_1:def 3;
A90:
(
<*E,F*> . i1 = E &
<*E,F*> . i2 = F )
by FINSEQ_1:44;
A91:
Nx . 1 =
||.(s . i1).||
by A88
.=
||.x.||
by A90, FINSEQ_1:44
;
Nx . 2 =
||.(s . i2).||
by A88
.=
||.y.||
by A90, FINSEQ_1:44
;
then
Nx = <*||.x.||,||.y.||*>
by A89, A91, FINSEQ_1:44;
then
Product Nx = ||.x.|| * ||.y.||
by RVSUM_1:99;
then
||.(L . (x,y)).|| <= K * (||.x.|| * ||.y.||)
by A85, A87, A88;
hence
||.(L . (x,y)).|| <= (K * ||.x.||) * ||.y.||
;
verum
end;
hence
u * (IsoCPNrSP (E,F)) is Lipschitzian BilinearOperator of E,F,G
by LOPBAN_9:def 3; verum