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