let E, F, G be RealLinearSpace; for u being MultilinearOperator of <*E,F*>,G holds u * (IsoCPRLSP (E,F)) is BilinearOperator of E,F,G
let u be MultilinearOperator of <*E,F*>,G; u * (IsoCPRLSP (E,F)) is BilinearOperator of E,F,G
reconsider L = u * (IsoCPRLSP (E,F)) as Function of [:E,F:],G ;
dom <*E,F*> = Seg (len <*E,F*>)
by FINSEQ_1:def 3;
then
dom <*E,F*> = {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))
set x =
x1;
reconsider xy =
<*x1,y*> as
Point of
(product <*E,F*>) by PRVECT_3:14;
A3:
<*E,F*> . i1 = E
by FINSEQ_1:44;
then reconsider L1 =
u * (reproj (i1,xy)) as
LinearOperator of
E,
G by LOPBAN10:def 3;
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;
then A14:
(xy +* (i1,x1)) . 1
= x1
by FUNCT_7:31;
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 NDIFF5def4
.=
<*(x1 + x2),y*>
by A8, A9, A10, FINSEQ_1:44
;
A13:
len (xy +* (i1,x1)) = 2
by LemmaA;
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, NDIFF5def4
.=
<*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, NDIFF5def4
.=
<*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 . ((IsoCPRLSP (E,F)) . ((x1 + x2),y))
by FUNCT_2:15
.=
u . ((reproj (i1,xy)) . (x1 + x2))
by A12, defISO
.=
L1 . (x1 + x2)
by A5, FUNCT_1:13
;
A24:
L . (
x1,
y) =
u . ((IsoCPRLSP (E,F)) . (x1,y))
by A4, FUNCT_2:15
.=
u . ((reproj (i1,xy)) . x1)
by A17, defISO
.=
L1 . x1
by A5, FUNCT_1:13
;
L . (
x2,
y) =
u . ((IsoCPRLSP (E,F)) . (x2,y))
by A4, FUNCT_2:15
.=
u . ((reproj (i1,xy)) . x2)
by A22, defISO
.=
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:14;
A27:
<*E,F*> . i1 = E
by FINSEQ_1:44;
then reconsider L1 =
u * (reproj (i1,xy)) as
LinearOperator of
E,
G by LOPBAN10:def 3;
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 NDIFF5def4
.=
<*(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, NDIFF5def4
.=
<*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 . ((IsoCPRLSP (E,F)) . ((a * x),y))
by FUNCT_2:15
.=
u . ((reproj (i1,xy)) . (a * x))
by A36, defISO
.=
L1 . (a * x)
by A29, FUNCT_1:13
;
L . (
x,
y) =
u . ((IsoCPRLSP (E,F)) . (x,y))
by A28, FUNCT_2:15
.=
u . ((reproj (i1,xy)) . x)
by A41, defISO
.=
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:14;
A45:
<*E,F*> . i2 = F
by FINSEQ_1:44;
then reconsider L1 =
u * (reproj (i2,xy)) as
LinearOperator of
F,
G by LOPBAN10:def 3;
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 NDIFF5def4
.=
<*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, NDIFF5def4
.=
<*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, NDIFF5def4
.=
<*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 . ((IsoCPRLSP (E,F)) . (x,(y1 + y2)))
by FUNCT_2:15
.=
u . ((reproj (i2,xy)) . (y1 + y2))
by A54, defISO
.=
L1 . (y1 + y2)
by A47, FUNCT_1:13
;
A66:
L . (
x,
y1) =
u . ((IsoCPRLSP (E,F)) . (x,y1))
by A46, FUNCT_2:15
.=
u . ((reproj (i2,xy)) . y1)
by A59, defISO
.=
L1 . y1
by A47, FUNCT_1:13
;
L . (
x,
y2) =
u . ((IsoCPRLSP (E,F)) . (x,y2))
by A46, FUNCT_2:15
.=
u . ((reproj (i2,xy)) . y2)
by A64, defISO
.=
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:14;
A68:
<*E,F*> . i2 = F
by FINSEQ_1:44;
then reconsider L1 =
u * (reproj (i2,xy)) as
LinearOperator of
F,
G by LOPBAN10:def 3;
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 A80:
(xy +* (i2,y)) . 2
= 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
;
A75:
(xy +* (i2,(a * y))) . 2
= a * y
by A72, FUNCT_7:31;
reconsider x1x2 =
a * y as
Element of
(<*E,F*> . i2) by FINSEQ_1:44;
A77:
(reproj (i2,xy)) . x1x2 =
xy +* (
i2,
(a * y))
by NDIFF5def4
.=
<*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
;
A82:
(reproj (i2,xy)) . y =
xy +* (
i2,
y)
by A68, NDIFF5def4
.=
<*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 . ((IsoCPRLSP (E,F)) . (x,(a * y)))
by FUNCT_2:15
.=
u . ((reproj (i2,xy)) . (a * y))
by A77, defISO
.=
L1 . (a * y)
by A70, FUNCT_1:13
;
L . (
x,
y) =
u . ((IsoCPRLSP (E,F)) . (x,y))
by A69, FUNCT_2:15
.=
u . ((reproj (i2,xy)) . y)
by A82, defISO
.=
L1 . y
by A70, FUNCT_1:13
;
hence
L . (
x,
(a * y))
= a * (L . (x,y))
by A83, LOPBAN_1:def 5;
verum
end;
hence
u * (IsoCPRLSP (E,F)) is BilinearOperator of E,F,G
by A2, A26, A44, LOPBAN_8:11; verum