let F be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; for V being VectSp of F
for W being Subspace of V
for f being linear-Functional of V st the carrier of W c= ker f holds
QFunctional f,W is homogeneous
let V be VectSp of F; for W being Subspace of V
for f being linear-Functional of V st the carrier of W c= ker f holds
QFunctional f,W is homogeneous
let W be Subspace of V; for f being linear-Functional of V st the carrier of W c= ker f holds
QFunctional f,W is homogeneous
let f be linear-Functional of V; ( the carrier of W c= ker f implies QFunctional f,W is homogeneous )
set qf = QFunctional f,W;
set vq = VectQuot V,W;
assume A1:
the carrier of W c= ker f
; QFunctional f,W is homogeneous
now 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)A2:
CosetSet V,
W = the
carrier of
(VectQuot V,W)
by Def6;
then
A in CosetSet V,
W
;
then consider aa being
Coset of
W such that A3:
A = aa
;
consider a being
Vector of
V such that A4:
aa = a + W
by VECTSP_4:def 6;
r * A =
the
lmult of
(VectQuot V,W) . r,
A
by VECTSP_1:def 24
.=
(lmultCoset V,W) . r,
A
by Def6
.=
(r * a) + W
by A2, A3, A4, Def5
;
hence (QFunctional f,W) . (r * A) =
f . (r * a)
by A1, Def12
.=
r * (f . a)
by HAHNBAN1:def 12
.=
r * ((QFunctional f,W) . A)
by A1, A3, A4, Def12
;
verum end;
hence
QFunctional f,W is homogeneous
by HAHNBAN1:def 12; verum