let V be VectSp of F_Complex ; for W being Subspace of V
for f being antilinear-Functional of V st the carrier of W c= ker (f *') holds
QFunctional (f,W) is cmplxhomogeneous
let W be Subspace of V; for f being antilinear-Functional of V st the carrier of W c= ker (f *') holds
QFunctional (f,W) is cmplxhomogeneous
let f be antilinear-Functional of V; ( the carrier of W c= ker (f *') implies QFunctional (f,W) is cmplxhomogeneous )
assume A1:
the carrier of W c= ker (f *')
; QFunctional (f,W) is cmplxhomogeneous
set vq = VectQuot (V,W);
set qf = QFunctional (f,W);
A2:
ker (f *') = ker f
by Th23;
now for A being Vector of (VectQuot (V,W))
for r being Scalar of holds (QFunctional (f,W)) . (r * A) = (r *') * ((QFunctional (f,W)) . A)set C =
CosetSet (
V,
W);
let A be
Vector of
(VectQuot (V,W));
for r being Scalar of holds (QFunctional (f,W)) . (r * A) = (r *') * ((QFunctional (f,W)) . A)let r be
Scalar of ;
(QFunctional (f,W)) . (r * A) = (r *') * ((QFunctional (f,W)) . A)A3:
CosetSet (
V,
W)
= the
carrier of
(VectQuot (V,W))
by VECTSP10:def 6;
then
A in CosetSet (
V,
W)
;
then consider aa being
Coset of
W such that A4:
A = aa
;
consider a being
Vector of
V such that A5:
aa = a + W
by VECTSP_4:def 6;
r * A =
(lmultCoset (V,W)) . (
r,
A)
by VECTSP10:def 6
.=
(r * a) + W
by A3, A4, A5, VECTSP10:def 5
;
hence (QFunctional (f,W)) . (r * A) =
f . (r * a)
by A1, A2, VECTSP10:def 12
.=
(r *') * (f . a)
by Def1
.=
(r *') * ((QFunctional (f,W)) . A)
by A1, A2, A4, A5, VECTSP10:def 12
;
verum end;
hence
QFunctional (f,W) is cmplxhomogeneous
; verum