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