let F be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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 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)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)
.=
(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 8
.=
r * ((QFunctional (f,W)) . A)
by A1, A3, A4, Def12
;
verum end;
hence
QFunctional (f,W) is homogeneous
; verum