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,a1then
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 HAHNBAN1:def 11;
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