set lf = LQForm f;
thus
LQForm f is additiveFAF
LQForm f is cmplxhomogeneousFAF 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 BILINEAR:8
.=
f . (
v,
(w + t))
by A1, BILINEAR:def 20
.=
(f . (v,w)) + (f . (v,t))
by BILINEAR:27
.=
((LQForm f) . (A,w)) + (f . (v,t))
by A1, BILINEAR:def 20
.=
((LQForm f) . (A,w)) + ((LQForm f) . (A,t))
by A1, BILINEAR:def 20
.=
((FunctionalFAF ((LQForm f),A)) . w) + ((LQForm f) . (A,t))
by BILINEAR:8
.=
((FunctionalFAF ((LQForm f),A)) . w) + ((FunctionalFAF ((LQForm f),A)) . t)
by BILINEAR:8
;
verum
end;
let A be Vector of (VectQuot (V,(LKer f))); HERMITAN:def 4 FunctionalFAF ((LQForm f),A) is cmplxhomogeneous
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; HERMITAN:def 1 for a being Scalar of holds (FunctionalFAF ((LQForm f),A)) . (a * w) = (a *') * ((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 BILINEAR:8
.=
f . (v,(r * w))
by A2, BILINEAR:def 20
.=
(r *') * (f . (v,w))
by Th27
.=
(r *') * ((LQForm f) . (A,w))
by A2, BILINEAR:def 20
.=
(r *') * ((FunctionalFAF ((LQForm f),A)) . w)
by BILINEAR:8
; verum