let E, F, G be RealLinearSpace; for u being BilinearOperator of E,F,G holds u * ((IsoCPRLSP (E,F)) ") is MultilinearOperator of <*E,F*>,G
let u be BilinearOperator of E,F,G; u * ((IsoCPRLSP (E,F)) ") is MultilinearOperator of <*E,F*>,G
reconsider M = u * ((IsoCPRLSP (E,F)) ") as Function of (product <*E,F*>),G ;
A1: 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;
for i being Element of dom <*E,F*>
for s being Element of (product <*E,F*>) holds M * (reproj (i,s)) is LinearOperator of (<*E,F*> . i),G
proof
let i be
Element of
dom <*E,F*>;
for s being Element of (product <*E,F*>) holds M * (reproj (i,s)) is LinearOperator of (<*E,F*> . i),Glet s be
Element of
(product <*E,F*>);
M * (reproj (i,s)) is LinearOperator of (<*E,F*> . i),G
consider x being
Point of
E,
y being
Point of
F such that A3:
s = <*x,y*>
by PRVECT_3:14;
len s = 2
by A3, FINSEQ_1:44;
then A5:
dom s = {1,2}
by FINSEQ_1:2, FINSEQ_1:def 3;
per cases
( i = 1 or i = 2 )
by A1, TARSKI:def 2;
suppose A6:
i = 1
;
M * (reproj (i,s)) is LinearOperator of (<*E,F*> . i),Gthen A7:
<*E,F*> . i = E
;
then reconsider L =
M * (reproj (i,s)) as
Function of
E,
G ;
A8:
dom (reproj (i,s)) =
the
carrier of
(<*E,F*> . i)
by FUNCT_2:def 1
.=
the
carrier of
E
by A6
;
A9:
for
z being
Point of
E holds
(reproj (i,s)) . z = <*z,y*>
proof
let x1 be
Point of
E;
(reproj (i,s)) . x1 = <*x1,y*>
A10:
len (s +* (i,x1)) = 2
by LemmaA;
A11:
(s +* (i,x1)) . 1
= x1
by A1, A5, A6, FUNCT_7:31;
A12:
(s +* (i,x1)) . 2 =
s . 2
by A6, FUNCT_7:32
.=
y
by A3
;
thus (reproj (i,s)) . x1 =
s +* (
i,
x1)
by A7, NDIFF5def4
.=
<*x1,y*>
by A10, A11, A12, FINSEQ_1:44
;
verum
end; A14:
for
x1,
x2 being
Point of
E holds
L . (x1 + x2) = (L . x1) + (L . x2)
proof
let x1,
x2 be
Point of
E;
L . (x1 + x2) = (L . x1) + (L . x2)
reconsider x1y =
<*x1,y*>,
x2y =
<*x2,y*>,
x12y =
<*(x1 + x2),y*> as
Point of
(product <*E,F*>) by PRVECT_3:14;
A18:
L . x1 =
M . ((reproj (i,s)) . x1)
by A8, FUNCT_1:13
.=
(u * ((IsoCPRLSP (E,F)) ")) . <*x1,y*>
by A9
.=
u . (((IsoCPRLSP (E,F)) ") . x1y)
by FUNCT_2:15
.=
u . (
x1,
y)
by defISOA1
;
A19:
L . x2 =
M . ((reproj (i,s)) . x2)
by A8, FUNCT_1:13
.=
(u * ((IsoCPRLSP (E,F)) ")) . <*x2,y*>
by A9
.=
u . (((IsoCPRLSP (E,F)) ") . x2y)
by FUNCT_2:15
.=
u . (
x2,
y)
by defISOA1
;
L . (x1 + x2) =
M . ((reproj (i,s)) . (x1 + x2))
by A8, FUNCT_1:13
.=
(u * ((IsoCPRLSP (E,F)) ")) . <*(x1 + x2),y*>
by A9
.=
u . (((IsoCPRLSP (E,F)) ") . x12y)
by FUNCT_2:15
.=
u . (
(x1 + x2),
y)
by defISOA1
;
hence
L . (x1 + x2) = (L . x1) + (L . x2)
by A18, A19, LOPBAN_8:11;
verum
end;
for
x1 being
Point of
E for
a being
Real holds
L . (a * x1) = a * (L . x1)
proof
let x1 be
Point of
E;
for a being Real holds L . (a * x1) = a * (L . x1)let a be
Real;
L . (a * x1) = a * (L . x1)
reconsider ax1y =
<*(a * x1),y*>,
x1y =
<*x1,y*> as
Point of
(product <*E,F*>) by PRVECT_3:14;
A23:
L . x1 =
M . ((reproj (i,s)) . x1)
by A8, FUNCT_1:13
.=
(u * ((IsoCPRLSP (E,F)) ")) . <*x1,y*>
by A9
.=
u . (((IsoCPRLSP (E,F)) ") . x1y)
by FUNCT_2:15
.=
u . (
x1,
y)
by defISOA1
;
L . (a * x1) =
M . ((reproj (i,s)) . (a * x1))
by A8, FUNCT_1:13
.=
(u * ((IsoCPRLSP (E,F)) ")) . <*(a * x1),y*>
by A9
.=
u . (((IsoCPRLSP (E,F)) ") . ax1y)
by FUNCT_2:15
.=
u . (
(a * x1),
y)
by defISOA1
;
hence
L . (a * x1) = a * (L . x1)
by A23, LOPBAN_8:11;
verum
end; hence
M * (reproj (i,s)) is
LinearOperator of
(<*E,F*> . i),
G
by A7, A14, LOPBAN_1:def 5, VECTSP_1:def 20;
verum end; suppose A25:
i = 2
;
M * (reproj (i,s)) is LinearOperator of (<*E,F*> . i),Gthen A26:
<*E,F*> . i = F
;
then reconsider L =
M * (reproj (i,s)) as
Function of
F,
G ;
A27:
dom (reproj (i,s)) =
the
carrier of
(<*E,F*> . i)
by FUNCT_2:def 1
.=
the
carrier of
F
by A25
;
A28:
for
z being
Point of
F holds
(reproj (i,s)) . z = <*x,z*>
proof
let y1 be
Point of
F;
(reproj (i,s)) . y1 = <*x,y1*>
A29:
len (s +* (i,y1)) = 2
by LemmaA;
A30:
(s +* (i,y1)) . 2
= y1
by A1, A5, A25, FUNCT_7:31;
A31:
(s +* (i,y1)) . 1 =
s . 1
by A25, FUNCT_7:32
.=
x
by A3
;
thus (reproj (i,s)) . y1 =
s +* (
i,
y1)
by A26, NDIFF5def4
.=
<*x,y1*>
by A29, A30, A31, FINSEQ_1:44
;
verum
end; A33:
for
y1,
y2 being
Point of
F holds
L . (y1 + y2) = (L . y1) + (L . y2)
proof
let y1,
y2 be
Point of
F;
L . (y1 + y2) = (L . y1) + (L . y2)
reconsider y1y =
<*x,y1*>,
y2y =
<*x,y2*>,
y12y =
<*x,(y1 + y2)*> as
Point of
(product <*E,F*>) by PRVECT_3:14;
A37:
L . y1 =
M . ((reproj (i,s)) . y1)
by A27, FUNCT_1:13
.=
(u * ((IsoCPRLSP (E,F)) ")) . <*x,y1*>
by A28
.=
u . (((IsoCPRLSP (E,F)) ") . y1y)
by FUNCT_2:15
.=
u . (
x,
y1)
by defISOA1
;
A38:
L . y2 =
M . ((reproj (i,s)) . y2)
by A27, FUNCT_1:13
.=
(u * ((IsoCPRLSP (E,F)) ")) . <*x,y2*>
by A28
.=
u . (((IsoCPRLSP (E,F)) ") . y2y)
by FUNCT_2:15
.=
u . (
x,
y2)
by defISOA1
;
L . (y1 + y2) =
M . ((reproj (i,s)) . (y1 + y2))
by A27, FUNCT_1:13
.=
(u * ((IsoCPRLSP (E,F)) ")) . <*x,(y1 + y2)*>
by A28
.=
u . (((IsoCPRLSP (E,F)) ") . y12y)
by FUNCT_2:15
.=
u . (
x,
(y1 + y2))
by defISOA1
;
hence
L . (y1 + y2) = (L . y1) + (L . y2)
by A37, A38, LOPBAN_8:11;
verum
end;
for
y1 being
Point of
F for
a being
Real holds
L . (a * y1) = a * (L . y1)
proof
let y1 be
Point of
F;
for a being Real holds L . (a * y1) = a * (L . y1)let a be
Real;
L . (a * y1) = a * (L . y1)
reconsider ax1y =
<*x,(a * y1)*>,
x1y =
<*x,y1*> as
Point of
(product <*E,F*>) by PRVECT_3:14;
A42:
L . y1 =
M . ((reproj (i,s)) . y1)
by A27, FUNCT_1:13
.=
(u * ((IsoCPRLSP (E,F)) ")) . <*x,y1*>
by A28
.=
u . (((IsoCPRLSP (E,F)) ") . x1y)
by FUNCT_2:15
.=
u . (
x,
y1)
by defISOA1
;
L . (a * y1) =
M . ((reproj (i,s)) . (a * y1))
by A27, FUNCT_1:13
.=
(u * ((IsoCPRLSP (E,F)) ")) . <*x,(a * y1)*>
by A28
.=
u . (((IsoCPRLSP (E,F)) ") . ax1y)
by FUNCT_2:15
.=
u . (
x,
(a * y1))
by defISOA1
;
hence
L . (a * y1) = a * (L . y1)
by A42, LOPBAN_8:11;
verum
end; hence
M * (reproj (i,s)) is
LinearOperator of
(<*E,F*> . i),
G
by A26, A33, LOPBAN_1:def 5, VECTSP_1:def 20;
verum end;
end;
hence
u * ((IsoCPRLSP (E,F)) ") is MultilinearOperator of <*E,F*>,G
by LOPBAN10:def 3; verum