set L = LKer f;
set vq = VectQuot V,(LKer f);
set Cv = CosetSet V,(LKer f);
set aCv = addCoset V,(LKer f);
set mCv = lmultCoset V,(LKer f);
set R = RKer f;
set wq = VectQuot W,(RKer f);
set Cw = CosetSet W,(RKer f);
set aCw = addCoset W,(RKer f);
set mCw = lmultCoset W,(RKer f);
defpred S1[ set , set , set ] means for v being Vector of V
for w being Vector of W st $1 = v + (LKer f) & $2 = w + (RKer f) holds
$3 = f . v,w;
A1:
now let A be
Vector of
(VectQuot V,(LKer f));
for B being Vector of (VectQuot W,(RKer f)) ex y being Element of the carrier of K st S1[A,B,y]let B be
Vector of
(VectQuot W,(RKer f));
ex y being Element of the carrier of K st S1[A,B,y]consider a being
Vector of
V such that A2:
A = a + (LKer f)
by VECTSP10:23;
consider b being
Vector of
W such that A3:
B = b + (RKer f)
by VECTSP10:23;
take y =
f . a,
b;
S1[A,B,y]now let a1 be
Vector of
V;
for b1 being Vector of W st A = a1 + (LKer f) & B = b1 + (RKer f) holds
y = f . a1,b1let b1 be
Vector of
W;
( A = a1 + (LKer f) & B = b1 + (RKer f) implies y = f . a1,b1 )assume
A = a1 + (LKer f)
;
( B = b1 + (RKer f) implies y = f . a1,b1 )then
a in a1 + (LKer f)
by A2, VECTSP_4:59;
then consider vv being
Vector of
V such that A4:
vv in LKer f
and A5:
a = a1 + vv
by VECTSP_4:57;
vv in the
carrier of
(LKer f)
by A4, STRUCT_0:def 5;
then
vv in leftker f
by Def19;
then A6:
ex
aa being
Vector of
V st
(
aa = vv & ( for
w0 being
Vector of
W holds
f . aa,
w0 = 0. K ) )
;
assume
B = b1 + (RKer f)
;
y = f . a1,b1then
b in b1 + (RKer f)
by A3, VECTSP_4:59;
then consider ww being
Vector of
W such that A7:
ww in RKer f
and A8:
b = b1 + ww
by VECTSP_4:57;
ww in the
carrier of
(RKer f)
by A7, STRUCT_0:def 5;
then
ww in rightker f
by Def20;
then A9:
ex
bb being
Vector of
W st
(
bb = ww & ( for
v0 being
Vector of
V holds
f . v0,
bb = 0. K ) )
;
thus y =
((f . a1,b1) + (f . a1,ww)) + ((f . vv,b1) + (f . vv,ww))
by A5, A8, Th29
.=
((f . a1,b1) + (0. K)) + ((f . vv,b1) + (f . vv,ww))
by A9
.=
((f . a1,b1) + (0. K)) + ((0. K) + (f . vv,ww))
by A6
.=
(f . a1,b1) + ((0. K) + (f . vv,ww))
by RLVECT_1:def 7
.=
(f . a1,b1) + (f . vv,ww)
by RLVECT_1:10
.=
(f . a1,b1) + (0. K)
by A6
.=
f . a1,
b1
by RLVECT_1:def 7
;
verum end; hence
S1[
A,
B,
y]
;
verum end;
consider ff being Function of [:the carrier of (VectQuot V,(LKer f)),the carrier of (VectQuot W,(RKer f)):],the carrier of K such that
A10:
for A being Vector of (VectQuot V,(LKer f))
for B being Vector of (VectQuot W,(RKer f)) holds S1[A,B,ff . A,B]
from BINOP_1:sch 3(A1);
reconsider ff = ff as Form of (VectQuot V,(LKer f)),(VectQuot W,(RKer f)) ;
A11:
CosetSet V,(LKer f) = the carrier of (VectQuot V,(LKer f))
by VECTSP10:def 6;
A12:
now let ww be
Vector of
(VectQuot W,(RKer f));
FunctionalSAF ff,ww is homogeneous consider w being
Vector of
W such that A13:
ww = w + (RKer f)
by VECTSP10:23;
set ffw =
FunctionalSAF ff,
ww;
now let A be
Vector of
(VectQuot V,(LKer f));
for r being Element of K holds (FunctionalSAF ff,ww) . (r * A) = r * ((FunctionalSAF ff,ww) . A)let r be
Element of
K;
(FunctionalSAF ff,ww) . (r * A) = r * ((FunctionalSAF ff,ww) . A)consider a being
Vector of
V such that A14:
A = a + (LKer f)
by VECTSP10:23;
A15:
( the
lmult of
(VectQuot V,(LKer f)) = lmultCoset V,
(LKer f) &
(lmultCoset V,(LKer f)) . r,
A = (r * a) + (LKer f) )
by A11, A14, VECTSP10:def 5, VECTSP10:def 6;
thus (FunctionalSAF ff,ww) . (r * A) =
ff . (r * A),
ww
by Th10
.=
f . (r * a),
w
by A10, A13, A15, VECTSP_1:def 24
.=
r * (f . a,w)
by Th32
.=
r * (ff . A,ww)
by A10, A13, A14
.=
r * ((FunctionalSAF ff,ww) . A)
by Th10
;
verum end; hence
FunctionalSAF ff,
ww is
homogeneous
by HAHNBAN1:def 12;
verum end;
A16:
CosetSet W,(RKer f) = the carrier of (VectQuot W,(RKer f))
by VECTSP10:def 6;
A17:
now let vv be
Vector of
(VectQuot V,(LKer f));
FunctionalFAF ff,vv is homogeneous consider v being
Vector of
V such that A18:
vv = v + (LKer f)
by VECTSP10:23;
set ffv =
FunctionalFAF ff,
vv;
now let A be
Vector of
(VectQuot W,(RKer f));
for r being Element of K holds (FunctionalFAF ff,vv) . (r * A) = r * ((FunctionalFAF ff,vv) . A)let r be
Element of
K;
(FunctionalFAF ff,vv) . (r * A) = r * ((FunctionalFAF ff,vv) . A)consider a being
Vector of
W such that A19:
A = a + (RKer f)
by VECTSP10:23;
A20:
( the
lmult of
(VectQuot W,(RKer f)) = lmultCoset W,
(RKer f) &
(lmultCoset W,(RKer f)) . r,
A = (r * a) + (RKer f) )
by A16, A19, VECTSP10:def 5, VECTSP10:def 6;
thus (FunctionalFAF ff,vv) . (r * A) =
ff . vv,
(r * A)
by Th9
.=
f . v,
(r * a)
by A10, A18, A20, VECTSP_1:def 24
.=
r * (f . v,a)
by Th33
.=
r * (ff . vv,A)
by A10, A18, A19
.=
r * ((FunctionalFAF ff,vv) . A)
by Th9
;
verum end; hence
FunctionalFAF ff,
vv is
homogeneous
by HAHNBAN1:def 12;
verum end;
A21:
now let ww be
Vector of
(VectQuot W,(RKer f));
FunctionalSAF ff,ww is additive consider w being
Vector of
W such that A22:
ww = w + (RKer f)
by VECTSP10:23;
set ffw =
FunctionalSAF ff,
ww;
now let A,
B be
Vector of
(VectQuot V,(LKer f));
(FunctionalSAF ff,ww) . (A + B) = ((FunctionalSAF ff,ww) . A) + ((FunctionalSAF ff,ww) . B)consider a being
Vector of
V such that A23:
A = a + (LKer f)
by VECTSP10:23;
consider b being
Vector of
V such that A24:
B = b + (LKer f)
by VECTSP10:23;
A25:
( the
addF of
(VectQuot V,(LKer f)) = addCoset V,
(LKer f) &
(addCoset V,(LKer f)) . A,
B = (a + b) + (LKer f) )
by A11, A23, A24, VECTSP10:def 3, VECTSP10:def 6;
thus (FunctionalSAF ff,ww) . (A + B) =
ff . (A + B),
ww
by Th10
.=
f . (a + b),
w
by A10, A22, A25, RLVECT_1:5
.=
(f . a,w) + (f . b,w)
by Th27
.=
(ff . A,ww) + (f . b,w)
by A10, A22, A23
.=
(ff . A,ww) + (ff . B,ww)
by A10, A22, A24
.=
((FunctionalSAF ff,ww) . A) + (ff . B,ww)
by Th10
.=
((FunctionalSAF ff,ww) . A) + ((FunctionalSAF ff,ww) . B)
by Th10
;
verum end; hence
FunctionalSAF ff,
ww is
additive
by HAHNBAN1:def 11;
verum end;
now let vv be
Vector of
(VectQuot V,(LKer f));
FunctionalFAF ff,vv is additive consider v being
Vector of
V such that A26:
vv = v + (LKer f)
by VECTSP10:23;
set ffv =
FunctionalFAF ff,
vv;
now let A,
B be
Vector of
(VectQuot W,(RKer f));
(FunctionalFAF ff,vv) . (A + B) = ((FunctionalFAF ff,vv) . A) + ((FunctionalFAF ff,vv) . B)consider a being
Vector of
W such that A27:
A = a + (RKer f)
by VECTSP10:23;
consider b being
Vector of
W such that A28:
B = b + (RKer f)
by VECTSP10:23;
A29:
( the
addF of
(VectQuot W,(RKer f)) = addCoset W,
(RKer f) &
(addCoset W,(RKer f)) . A,
B = (a + b) + (RKer f) )
by A16, A27, A28, VECTSP10:def 3, VECTSP10:def 6;
thus (FunctionalFAF ff,vv) . (A + B) =
ff . vv,
(A + B)
by Th9
.=
f . v,
(a + b)
by A10, A26, A29, RLVECT_1:5
.=
(f . v,a) + (f . v,b)
by Th28
.=
(ff . vv,A) + (f . v,b)
by A10, A26, A27
.=
(ff . vv,A) + (ff . vv,B)
by A10, A26, A28
.=
((FunctionalFAF ff,vv) . A) + (ff . vv,B)
by Th9
.=
((FunctionalFAF ff,vv) . A) + ((FunctionalFAF ff,vv) . B)
by Th9
;
verum end; hence
FunctionalFAF ff,
vv is
additive
by HAHNBAN1:def 11;
verum end;
then reconsider ff = ff as bilinear-Form of (VectQuot V,(LKer f)),(VectQuot W,(RKer f)) by A21, A12, A17, Def12, Def13, Def14, Def15;
take
ff
; for A being Vector of (VectQuot V,(LKer f))
for B being Vector of (VectQuot W,(RKer f))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
ff . A,B = f . v,w
thus
for A being Vector of (VectQuot V,(LKer f))
for B being Vector of (VectQuot W,(RKer f))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
ff . A,B = f . v,w
by A10; verum