set lf = LQForm f;
thus
LQForm f is additiveFAF
LQForm f is homogeneousFAF proof
let A be
Vector of
(VectQuot (V,(LKer f)));
BILINEAR:def 11 FunctionalFAF ((LQForm f),A) is additive
set flf =
FunctionalFAF (
(LQForm f),
A);
consider v being
Vector of
V such that A1:
A = v + (LKer f)
by VECTSP10:22;
let w,
t be
Vector of
W;
VECTSP_1:def 19 (FunctionalFAF ((LQForm f),A)) . (w + t) = ((FunctionalFAF ((LQForm f),A)) . w) + ((FunctionalFAF ((LQForm f),A)) . t)
thus (FunctionalFAF ((LQForm f),A)) . (w + t) =
(LQForm f) . (
A,
(w + t))
by Th8
.=
f . (
v,
(w + t))
by A1, Def20
.=
(f . (v,w)) + (f . (v,t))
by Th27
.=
((LQForm f) . (A,w)) + (f . (v,t))
by A1, Def20
.=
((LQForm f) . (A,w)) + ((LQForm f) . (A,t))
by A1, Def20
.=
((FunctionalFAF ((LQForm f),A)) . w) + ((LQForm f) . (A,t))
by Th8
.=
((FunctionalFAF ((LQForm f),A)) . w) + ((FunctionalFAF ((LQForm f),A)) . t)
by Th8
;
verum
end;
let A be Vector of (VectQuot (V,(LKer f))); BILINEAR:def 13 FunctionalFAF ((LQForm f),A) is homogeneous
set flf = FunctionalFAF ((LQForm f),A);
consider v being Vector of V such that
A2:
A = v + (LKer f)
by VECTSP10:22;
let w be Vector of W; HAHNBAN1:def 8 for b1 being Element of the carrier of K holds (FunctionalFAF ((LQForm f),A)) . (b1 * w) = b1 * ((FunctionalFAF ((LQForm f),A)) . w)
let r be Scalar of ; (FunctionalFAF ((LQForm f),A)) . (r * w) = r * ((FunctionalFAF ((LQForm f),A)) . w)
thus (FunctionalFAF ((LQForm f),A)) . (r * w) =
(LQForm f) . (A,(r * w))
by Th8
.=
f . (v,(r * w))
by A2, Def20
.=
r * (f . (v,w))
by Th32
.=
r * ((LQForm f) . (A,w))
by A2, Def20
.=
r * ((FunctionalFAF ((LQForm f),A)) . w)
by Th8
; verum