set K = F_Complex ;
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:
rightker f = rightker (f *' )
by Th58;
A2:
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 F_Complex st S1[A,B,y]let B be
Vector of
(VectQuot W,(RKer (f *' )));
ex y being Element of the carrier of F_Complex st S1[A,B,y]consider a being
Vector of
V such that A3:
A = a + (LKer f)
by VECTSP10:23;
consider b being
Vector of
W such that A4:
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 A3, VECTSP_4:59;
then consider vv being
Vector of
V such that A5:
vv in LKer f
and A6:
a = a1 + vv
by VECTSP_4:57;
vv in the
carrier of
(LKer f)
by A5, STRUCT_0:def 5;
then
vv in leftker f
by BILINEAR:def 19;
then A7:
ex
aa being
Vector of
V st
(
aa = vv & ( for
w0 being
Vector of
W holds
f . aa,
w0 = 0. F_Complex ) )
;
assume
B = b1 + (RKer (f *' ))
;
y = f . a1,b1then
b in b1 + (RKer (f *' ))
by A4, VECTSP_4:59;
then consider ww being
Vector of
W such that A8:
ww in RKer (f *' )
and A9:
b = b1 + ww
by VECTSP_4:57;
ww in the
carrier of
(RKer (f *' ))
by A8, STRUCT_0:def 5;
then
ww in rightker (f *' )
by BILINEAR:def 20;
then A10:
ex
bb being
Vector of
W st
(
bb = ww & ( for
v0 being
Vector of
V holds
f . v0,
bb = 0. F_Complex ) )
by A1;
thus y =
((f . a1,b1) + (f . a1,ww)) + ((f . vv,b1) + (f . vv,ww))
by A6, A9, BILINEAR:29
.=
((f . a1,b1) + (0. F_Complex )) + ((f . vv,b1) + (f . vv,ww))
by A10
.=
((f . a1,b1) + (0. F_Complex )) + ((0. F_Complex ) + (f . vv,ww))
by A7
.=
(f . a1,b1) + ((0. F_Complex ) + (f . vv,ww))
by RLVECT_1:def 7
.=
(f . a1,b1) + (f . vv,ww)
by RLVECT_1:10
.=
(f . a1,b1) + (0. F_Complex )
by A7
.=
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 F_Complex such that
A11:
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(A2);
reconsider ff = ff as Form of (VectQuot V,(LKer f)),(VectQuot W,(RKer (f *' ))) ;
A12:
CosetSet V,(LKer f) = the carrier of (VectQuot V,(LKer f))
by VECTSP10:def 6;
A13:
now let ww be
Vector of
(VectQuot W,(RKer (f *' )));
FunctionalSAF ff,ww is homogeneous consider w being
Vector of
W such that A14:
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 F_Complex holds (FunctionalSAF ff,ww) . (r * A) = r * ((FunctionalSAF ff,ww) . A)let r be
Element of
F_Complex ;
(FunctionalSAF ff,ww) . (r * A) = r * ((FunctionalSAF ff,ww) . A)consider a being
Vector of
V such that A15:
A = a + (LKer f)
by VECTSP10:23;
A16:
( the
lmult of
(VectQuot V,(LKer f)) = lmultCoset V,
(LKer f) &
(lmultCoset V,(LKer f)) . r,
A = (r * a) + (LKer f) )
by A12, A15, VECTSP10:def 5, VECTSP10:def 6;
thus (FunctionalSAF ff,ww) . (r * A) =
ff . (the lmult of (VectQuot V,(LKer f)) . r,A),
ww
by BILINEAR:10
.=
f . (r * a),
w
by A11, A14, A16
.=
r * (f . a,w)
by BILINEAR:32
.=
r * (ff . A,ww)
by A11, A14, A15
.=
r * ((FunctionalSAF ff,ww) . A)
by BILINEAR:10
;
verum end; hence
FunctionalSAF ff,
ww is
homogeneous
by HAHNBAN1:def 12;
verum end;
A17:
CosetSet W,(RKer (f *' )) = the carrier of (VectQuot W,(RKer (f *' )))
by VECTSP10:def 6;
A18:
now let vv be
Vector of
(VectQuot V,(LKer f));
FunctionalFAF ff,vv is cmplxhomogeneous consider v being
Vector of
V such that A19:
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 F_Complex holds (FunctionalFAF ff,vv) . (r * A) = (r *' ) * ((FunctionalFAF ff,vv) . A)let r be
Element of
F_Complex ;
(FunctionalFAF ff,vv) . (r * A) = (r *' ) * ((FunctionalFAF ff,vv) . A)consider a being
Vector of
W such that A20:
A = a + (RKer (f *' ))
by VECTSP10:23;
A21:
( the
lmult of
(VectQuot W,(RKer (f *' ))) = lmultCoset W,
(RKer (f *' )) &
(lmultCoset W,(RKer (f *' ))) . r,
A = (r * a) + (RKer (f *' )) )
by A17, A20, VECTSP10:def 5, VECTSP10:def 6;
thus (FunctionalFAF ff,vv) . (r * A) =
ff . vv,
(the lmult of (VectQuot W,(RKer (f *' ))) . r,A)
by BILINEAR:9
.=
f . v,
(r * a)
by A11, A19, A21
.=
(r *' ) * (f . v,a)
by Th30
.=
(r *' ) * (ff . vv,A)
by A11, A19, A20
.=
(r *' ) * ((FunctionalFAF ff,vv) . A)
by BILINEAR:9
;
verum end; hence
FunctionalFAF ff,
vv is
cmplxhomogeneous
by Def1;
verum end;
A22:
now let ww be
Vector of
(VectQuot W,(RKer (f *' )));
FunctionalSAF ff,ww is additive consider w being
Vector of
W such that A23:
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 A24:
A = a + (LKer f)
by VECTSP10:23;
consider b being
Vector of
V such that A25:
B = b + (LKer f)
by VECTSP10:23;
A26:
( the
addF of
(VectQuot V,(LKer f)) = addCoset V,
(LKer f) &
(addCoset V,(LKer f)) . A,
B = (a + b) + (LKer f) )
by A12, A24, A25, VECTSP10:def 3, VECTSP10:def 6;
thus (FunctionalSAF ff,ww) . (A + B) =
ff . (the addF of (VectQuot V,(LKer f)) . A,B),
ww
by BILINEAR:10
.=
f . (a + b),
w
by A11, A23, A26
.=
(f . a,w) + (f . b,w)
by BILINEAR:27
.=
(ff . A,ww) + (f . b,w)
by A11, A23, A24
.=
(ff . A,ww) + (ff . B,ww)
by A11, A23, A25
.=
((FunctionalSAF ff,ww) . A) + (ff . B,ww)
by BILINEAR:10
.=
((FunctionalSAF ff,ww) . A) + ((FunctionalSAF ff,ww) . B)
by BILINEAR:10
;
verum end; hence
FunctionalSAF ff,
ww is
additive
by GRCAT_1:def 13;
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 A27:
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 A28:
A = a + (RKer (f *' ))
by VECTSP10:23;
consider b being
Vector of
W such that A29:
B = b + (RKer (f *' ))
by VECTSP10:23;
A30:
( the
addF of
(VectQuot W,(RKer (f *' ))) = addCoset W,
(RKer (f *' )) &
(addCoset W,(RKer (f *' ))) . A,
B = (a + b) + (RKer (f *' )) )
by A17, A28, A29, VECTSP10:def 3, VECTSP10:def 6;
thus (FunctionalFAF ff,vv) . (A + B) =
ff . vv,
(the addF of (VectQuot W,(RKer (f *' ))) . A,B)
by BILINEAR:9
.=
f . v,
(a + b)
by A11, A27, A30
.=
(f . v,a) + (f . v,b)
by BILINEAR:28
.=
(ff . vv,A) + (f . v,b)
by A11, A27, A28
.=
(ff . vv,A) + (ff . vv,B)
by A11, A27, A29
.=
((FunctionalFAF ff,vv) . A) + (ff . vv,B)
by BILINEAR:9
.=
((FunctionalFAF ff,vv) . A) + ((FunctionalFAF ff,vv) . B)
by BILINEAR:9
;
verum end; hence
FunctionalFAF ff,
vv is
additive
by GRCAT_1:def 13;
verum end;
then reconsider ff = ff as sesquilinear-Form of (VectQuot V,(LKer f)),(VectQuot W,(RKer (f *' ))) by A22, A13, A18, Def4, BILINEAR:def 12, BILINEAR:def 13, BILINEAR:def 15;
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 A11; verum