let L be INTegral Z_Lattice; InnerProduct L is bilinear-Form of L,L
X1:
dom (InnerProduct L) = [: the carrier of L, the carrier of L:]
by FUNCT_2:def 1;
for z being object st z in [: the carrier of L, the carrier of L:] holds
(InnerProduct L) . z in the carrier of INT.Ring
then reconsider f = InnerProduct L as Form of L,L by X1, FUNCT_2:3;
for v being Vector of L holds FunctionalSAF (f,v) is additive
proof
let v be
Vector of
L;
FunctionalSAF (f,v) is additive
for
x,
y being
Vector of
L holds
(FunctionalSAF (f,v)) . (x + y) = ((FunctionalSAF (f,v)) . x) + ((FunctionalSAF (f,v)) . y)
proof
let x,
y be
Vector of
L;
(FunctionalSAF (f,v)) . (x + y) = ((FunctionalSAF (f,v)) . x) + ((FunctionalSAF (f,v)) . y)
thus (FunctionalSAF (f,v)) . (x + y) =
f . (
(x + y),
v)
by FUNCT_5:70
.=
<;(x + y),v;>
.=
<;v,(x + y);>
by defZLattice
.=
<;v,x;> + <;v,y;>
by ThSc2
.=
<;x,v;> + <;v,y;>
by defZLattice
.=
<;x,v;> + <;y,v;>
by defZLattice
.=
(f . (x,v)) + (f . (y,v))
.=
(((curry' f) . v) . x) + (f . (y,v))
by FUNCT_5:70
.=
((FunctionalSAF (f,v)) . x) + ((FunctionalSAF (f,v)) . y)
by FUNCT_5:70
;
verum
end;
hence
FunctionalSAF (
f,
v) is
additive
;
verum
end;
then X1:
f is additiveSAF
;
for v being Vector of L holds FunctionalSAF (f,v) is homogeneous
proof
let v be
Vector of
L;
FunctionalSAF (f,v) is homogeneous
for
x being
Vector of
L for
i being
Element of
INT.Ring holds
(FunctionalSAF (f,v)) . (i * x) = i * ((FunctionalSAF (f,v)) . x)
proof
let x be
Vector of
L;
for i being Element of INT.Ring holds (FunctionalSAF (f,v)) . (i * x) = i * ((FunctionalSAF (f,v)) . x)let i be
Element of
INT.Ring;
(FunctionalSAF (f,v)) . (i * x) = i * ((FunctionalSAF (f,v)) . x)
thus (FunctionalSAF (f,v)) . (i * x) =
f . (
(i * x),
v)
by FUNCT_5:70
.=
<;(i * x),v;>
.=
<;v,(i * x);>
by defZLattice
.=
i * <;v,x;>
by ThSc3
.=
i * <;x,v;>
by defZLattice
.=
i * (f . (x,v))
.=
i * ((FunctionalSAF (f,v)) . x)
by FUNCT_5:70
;
verum
end;
hence
FunctionalSAF (
f,
v) is
homogeneous
;
verum
end;
then X2:
f is homogeneousSAF
;
for v being Vector of L holds FunctionalFAF (f,v) is additive
proof
let v be
Vector of
L;
FunctionalFAF (f,v) is additive
for
x,
y being
Vector of
L holds
(FunctionalFAF (f,v)) . (x + y) = ((FunctionalFAF (f,v)) . x) + ((FunctionalFAF (f,v)) . y)
proof
let x,
y be
Vector of
L;
(FunctionalFAF (f,v)) . (x + y) = ((FunctionalFAF (f,v)) . x) + ((FunctionalFAF (f,v)) . y)
thus (FunctionalFAF (f,v)) . (x + y) =
f . (
v,
(x + y))
by FUNCT_5:69
.=
<;v,(x + y);>
.=
<;v,x;> + <;v,y;>
by ThSc2
.=
(f . (v,x)) + (f . (v,y))
.=
(((curry f) . v) . x) + (f . (v,y))
by FUNCT_5:69
.=
((FunctionalFAF (f,v)) . x) + ((FunctionalFAF (f,v)) . y)
by FUNCT_5:69
;
verum
end;
hence
FunctionalFAF (
f,
v) is
additive
;
verum
end;
then X3:
f is additiveFAF
;
for v being Vector of L holds FunctionalFAF (f,v) is homogeneous
proof
let v be
Vector of
L;
FunctionalFAF (f,v) is homogeneous
for
x being
Vector of
L for
i being
Element of
INT.Ring holds
(FunctionalFAF (f,v)) . (i * x) = i * ((FunctionalFAF (f,v)) . x)
proof
let x be
Vector of
L;
for i being Element of INT.Ring holds (FunctionalFAF (f,v)) . (i * x) = i * ((FunctionalFAF (f,v)) . x)let i be
Element of
INT.Ring;
(FunctionalFAF (f,v)) . (i * x) = i * ((FunctionalFAF (f,v)) . x)
thus (FunctionalFAF (f,v)) . (i * x) =
f . (
v,
(i * x))
by FUNCT_5:69
.=
<;v,(i * x);>
.=
i * <;v,x;>
by ThSc3
.=
i * (f . (v,x))
.=
i * ((FunctionalFAF (f,v)) . x)
by FUNCT_5:69
;
verum
end;
hence
FunctionalFAF (
f,
v) is
homogeneous
;
verum
end;
then
f is homogeneousFAF
;
hence
InnerProduct L is bilinear-Form of L,L
by X1, X2, X3; verum