set L = RKer f;
set vq = VectQuot (W,(RKer f));
set C = CosetSet (W,(RKer f));
set aC = addCoset (W,(RKer f));
set mC = lmultCoset (W,(RKer f));
defpred S1[ set , set , set ] means for w being Vector of W st $2 = w + (RKer f) holds
$3 = f . ($1,w);
A1:
now let v0 be
Vector of
V;
for A being Vector of (VectQuot (W,(RKer f))) ex y being Element of the carrier of K st S1[v0,A,y]let A be
Vector of
(VectQuot (W,(RKer f)));
ex y being Element of the carrier of K st S1[v0,A,y]consider a being
Vector of
W such that A2:
A = a + (RKer f)
by VECTSP10:23;
take y =
f . (
v0,
a);
S1[v0,A,y]now let a1 be
Vector of
W;
( A = a1 + (RKer f) implies y = f . (v0,a1) )assume
A = a1 + (RKer f)
;
y = f . (v0,a1)then
a in a1 + (RKer f)
by A2, VECTSP_4:59;
then consider w being
Vector of
W such that A3:
w in RKer f
and A4:
a = a1 + w
by VECTSP_4:57;
w in the
carrier of
(RKer f)
by A3, STRUCT_0:def 5;
then
w in rightker f
by Def20;
then A5:
ex
aa being
Vector of
W st
(
aa = w & ( for
vv being
Vector of
V holds
f . (
vv,
aa)
= 0. K ) )
;
thus y =
(f . (v0,a1)) + (f . (v0,w))
by A4, Th28
.=
(f . (v0,a1)) + (0. K)
by A5
.=
f . (
v0,
a1)
by RLVECT_1:def 7
;
verum end; hence
S1[
v0,
A,
y]
;
verum end;
consider ff being Function of [: the carrier of V, the carrier of (VectQuot (W,(RKer f))):], the carrier of K such that
A6:
for v being Vector of V
for A being Vector of (VectQuot (W,(RKer f))) holds S1[v,A,ff . (v,A)]
from BINOP_1:sch 3(A1);
reconsider ff = ff as Form of V,(VectQuot (W,(RKer f))) ;
A7:
CosetSet (W,(RKer f)) = the carrier of (VectQuot (W,(RKer f)))
by VECTSP10:def 6;
now let v be
Vector of
V;
FunctionalFAF (ff,v) is additive set ffw =
FunctionalFAF (
ff,
v);
now let A,
B be
Vector of
(VectQuot (W,(RKer f)));
(FunctionalFAF (ff,v)) . (A + B) = ((FunctionalFAF (ff,v)) . A) + ((FunctionalFAF (ff,v)) . B)consider a being
Vector of
W such that A8:
A = a + (RKer f)
by VECTSP10:23;
consider b being
Vector of
W such that A9:
B = b + (RKer f)
by VECTSP10:23;
A10:
( the
addF of
(VectQuot (W,(RKer f))) = addCoset (
W,
(RKer f)) &
(addCoset (W,(RKer f))) . (
A,
B)
= (a + b) + (RKer f) )
by A7, A8, A9, VECTSP10:def 3, VECTSP10:def 6;
thus (FunctionalFAF (ff,v)) . (A + B) =
ff . (
v,
(A + B))
by Th9
.=
f . (
v,
(a + b))
by A6, A10, RLVECT_1:5
.=
(f . (v,a)) + (f . (v,b))
by Th28
.=
(ff . (v,A)) + (f . (v,b))
by A6, A8
.=
(ff . (v,A)) + (ff . (v,B))
by A6, A9
.=
((FunctionalFAF (ff,v)) . A) + (ff . (v,B))
by Th9
.=
((FunctionalFAF (ff,v)) . A) + ((FunctionalFAF (ff,v)) . B)
by Th9
;
verum end; hence
FunctionalFAF (
ff,
v) is
additive
by GRCAT_1:def 13;
verum end;
then reconsider ff = ff as additiveFAF Form of V,(VectQuot (W,(RKer f))) by Def12;
now let v be
Vector of
V;
FunctionalFAF (ff,v) is homogeneous set ffw =
FunctionalFAF (
ff,
v);
now let A be
Vector of
(VectQuot (W,(RKer f)));
for r being Element of K holds (FunctionalFAF (ff,v)) . (r * A) = r * ((FunctionalFAF (ff,v)) . A)let r be
Element of
K;
(FunctionalFAF (ff,v)) . (r * A) = r * ((FunctionalFAF (ff,v)) . A)consider a being
Vector of
W such that A11:
A = a + (RKer f)
by VECTSP10:23;
A12:
( the
lmult of
(VectQuot (W,(RKer f))) = lmultCoset (
W,
(RKer f)) &
(lmultCoset (W,(RKer f))) . (
r,
A)
= (r * a) + (RKer f) )
by A7, A11, VECTSP10:def 5, VECTSP10:def 6;
thus (FunctionalFAF (ff,v)) . (r * A) =
ff . (
v,
(r * A))
by Th9
.=
f . (
v,
(r * a))
by A6, A12, VECTSP_1:def 24
.=
r * (f . (v,a))
by Th33
.=
r * (ff . (v,A))
by A6, A11
.=
r * ((FunctionalFAF (ff,v)) . A)
by Th9
;
verum end; hence
FunctionalFAF (
ff,
v) is
homogeneous
by HAHNBAN1:def 12;
verum end;
then reconsider ff = ff as additiveFAF homogeneousFAF Form of V,(VectQuot (W,(RKer f))) by Def14;
take
ff
; for A being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
ff . (v,A) = f . (v,w)
thus
for A being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
ff . (v,A) = f . (v,w)
by A6; verum