let E, F, G be RealLinearSpace; for L being Function of [: the carrier of E, the carrier of F:], the carrier of G holds
( L is Bilinear iff ( ( for x1, x2 being Point of E
for y being Point of F holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y)) ) & ( 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)) ) & ( for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2)) ) & ( 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)) ) ) )
let L be Function of [: the carrier of E, the carrier of F:], the carrier of G; ( L is Bilinear iff ( ( for x1, x2 being Point of E
for y being Point of F holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y)) ) & ( 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)) ) & ( for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2)) ) & ( 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)) ) ) )
A1:
( dom (curry L) = the carrier of E & dom (curry' L) = the carrier of F )
by FUNCT_2:def 1;
hereby ( ( for x1, x2 being Point of E
for y being Point of F holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y)) ) & ( 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)) ) & ( for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2)) ) & ( 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)) ) implies L is Bilinear )
assume A2:
L is
Bilinear
;
( ( for x1, x2 being Point of E
for y being Point of F holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y)) ) & ( 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)) ) & ( for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2)) ) & ( 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)) ) )thus
for
x1,
x2 being
Point of
E for
y being
Point of
F holds
L . (
(x1 + x2),
y)
= (L . (x1,y)) + (L . (x2,y))
( ( 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)) ) & ( for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2)) ) & ( 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 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 Ly =
(curry' L) . y as
additive homogeneous Function of
E,
G by A1, A2;
A5:
Ly . x1 = L . (
x1,
y)
by LM5;
A6:
Ly . x2 = L . (
x2,
y)
by LM5;
thus L . (
(x1 + x2),
y) =
Ly . (x1 + x2)
by LM5
.=
(L . (x1,y)) + (L . (x2,y))
by A5, A6, VECTSP_1:def 20
;
verum
end; thus
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))
( ( for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2)) ) & ( 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 . ((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 Ly =
(curry' L) . y as
additive homogeneous Function of
E,
G by A1, A2;
thus L . (
(a * x),
y) =
Ly . (a * x)
by LM5
.=
a * (Ly . x)
by LOPBAN_1:def 5
.=
a * (L . (x,y))
by LM5
;
verum
end; thus
for
x being
Point of
E for
y1,
y2 being
Point of
F holds
L . (
x,
(y1 + y2))
= (L . (x,y1)) + (L . (x,y2))
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 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 Lx =
(curry L) . x as
additive homogeneous Function of
F,
G by A1, A2;
A8:
Lx . y1 = L . (
x,
y1)
by LM4;
A9:
Lx . y2 = L . (
x,
y2)
by LM4;
thus L . (
x,
(y1 + y2)) =
Lx . (y1 + y2)
by LM4
.=
(L . (x,y1)) + (L . (x,y2))
by A8, A9, VECTSP_1:def 20
;
verum
end; thus
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))
verumproof
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 Lx =
(curry L) . x as
additive homogeneous Function of
F,
G by A1, A2;
A10:
Lx . y = L . (
x,
y)
by LM4;
thus L . (
x,
(a * y)) =
Lx . (a * y)
by LM4
.=
a * (L . (x,y))
by A10, LOPBAN_1:def 5
;
verum
end;
end;
assume that
A11:
for x1, x2 being Point of E
for y being Point of F holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))
and
A12:
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))
and
A13:
for x being Point of E
for y1, y2 being Point of F holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))
and
A14:
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))
; L is Bilinear
A15:
for x being Point of E st x in dom (curry L) holds
(curry L) . x is additive homogeneous Function of F,G
proof
let x be
Point of
E;
( x in dom (curry L) implies (curry L) . x is additive homogeneous Function of F,G )
assume
x in dom (curry L)
;
(curry L) . x is additive homogeneous Function of F,G
reconsider Lx =
(curry L) . x as
Function of
F,
G ;
A16:
for
y1,
y2 being
Point of
F holds
Lx . (y1 + y2) = (Lx . y1) + (Lx . y2)
proof
let y1,
y2 be
Point of
F;
Lx . (y1 + y2) = (Lx . y1) + (Lx . y2)
A17:
L . (
x,
y1)
= Lx . y1
by LM4;
thus Lx . (y1 + y2) =
L . (
x,
(y1 + y2))
by LM4
.=
(L . (x,y1)) + (L . (x,y2))
by A13
.=
(Lx . y1) + (Lx . y2)
by A17, LM4
;
verum
end;
for
y being
Point of
F for
a being
Real holds
Lx . (a * y) = a * (Lx . y)
hence
(curry L) . x is
additive homogeneous Function of
F,
G
by A16, LOPBAN_1:def 5, VECTSP_1:def 20;
verum
end;
for y being Point of F st y in dom (curry' L) holds
(curry' L) . y is additive homogeneous Function of E,G
proof
let y be
Point of
F;
( y in dom (curry' L) implies (curry' L) . y is additive homogeneous Function of E,G )
assume
y in dom (curry' L)
;
(curry' L) . y is additive homogeneous Function of E,G
reconsider Ly =
(curry' L) . y as
Function of
E,
G ;
A22:
for
x1,
x2 being
Point of
E holds
Ly . (x1 + x2) = (Ly . x1) + (Ly . x2)
proof
let x1,
x2 be
Point of
E;
Ly . (x1 + x2) = (Ly . x1) + (Ly . x2)
A23:
L . (
x1,
y)
= Ly . x1
by LM5;
thus Ly . (x1 + x2) =
L . (
(x1 + x2),
y)
by LM5
.=
(L . (x1,y)) + (L . (x2,y))
by A11
.=
(Ly . x1) + (Ly . x2)
by A23, LM5
;
verum
end;
for
x being
Point of
E for
a being
Real holds
Ly . (a * x) = a * (Ly . x)
hence
(curry' L) . y is
additive homogeneous Function of
E,
G
by A22, LOPBAN_1:def 5, VECTSP_1:def 20;
verum
end;
hence
L is Bilinear
by A15; verum