set vq = VectQuot (V,(LKer f));
set vr = VectQuot (V,(RKer (f *')));
VectQuot (V,(RKer (f *'))) = VectQuot (V,(LKer f))
by Th56;
then reconsider sc = Q*Form f as Form of (VectQuot (V,(LKer f))),(VectQuot (V,(LKer f))) ;
A1:
sc is homogeneousSAF
proof
let w be
Vector of
(VectQuot (V,(LKer f)));
BILINEAR:def 14 FunctionalSAF (sc,w) is homogeneous
set fg =
FunctionalSAF (
sc,
w);
let v be
Vector of
(VectQuot (V,(LKer f)));
HAHNBAN1:def 8 for b1 being Element of the carrier of F_Complex holds (FunctionalSAF (sc,w)) . (b1 * v) = b1 * ((FunctionalSAF (sc,w)) . v)let r be
Scalar of ;
(FunctionalSAF (sc,w)) . (r * v) = r * ((FunctionalSAF (sc,w)) . v)
consider va being
Vector of
V such that A2:
v = va + (LKer f)
by VECTSP10:22;
A3:
r * v = (r * va) + (LKer f)
by A2, VECTSP10:25;
reconsider A =
w as
Vector of
(VectQuot (V,(RKer (f *')))) by Th56;
consider wa being
Vector of
V such that A4:
A = wa + (RKer (f *'))
by VECTSP10:22;
thus (FunctionalSAF (sc,w)) . (r * v) =
(Q*Form f) . (
(r * v),
w)
by BILINEAR:9
.=
f . (
(r * va),
wa)
by A4, A3, Def12
.=
r * (f . (va,wa))
by BILINEAR:31
.=
r * (sc . (v,w))
by A4, A2, Def12
.=
r * ((FunctionalSAF (sc,w)) . v)
by BILINEAR:9
;
verum
end;
A5:
sc is additiveSAF
proof
let w be
Vector of
(VectQuot (V,(LKer f)));
BILINEAR:def 12 FunctionalSAF (sc,w) is additive
set fg =
FunctionalSAF (
sc,
w);
let v1,
v2 be
Vector of
(VectQuot (V,(LKer f)));
VECTSP_1:def 19 (FunctionalSAF (sc,w)) . (v1 + v2) = ((FunctionalSAF (sc,w)) . v1) + ((FunctionalSAF (sc,w)) . v2)
consider va being
Vector of
V such that A6:
v1 = va + (LKer f)
by VECTSP10:22;
consider vb being
Vector of
V such that A7:
v2 = vb + (LKer f)
by VECTSP10:22;
reconsider A =
w as
Vector of
(VectQuot (V,(RKer (f *')))) by Th56;
consider wa being
Vector of
V such that A8:
A = wa + (RKer (f *'))
by VECTSP10:22;
A9:
v1 + v2 = (va + vb) + (LKer f)
by A6, A7, VECTSP10:26;
thus (FunctionalSAF (sc,w)) . (v1 + v2) =
(Q*Form f) . (
(v1 + v2),
w)
by BILINEAR:9
.=
f . (
(va + vb),
wa)
by A8, A9, Def12
.=
(f . (va,wa)) + (f . (vb,wa))
by BILINEAR:26
.=
(sc . (v1,w)) + (f . (vb,wa))
by A8, A6, Def12
.=
(sc . (v1,w)) + (sc . (v2,w))
by A8, A7, Def12
.=
((FunctionalSAF (sc,w)) . v1) + (sc . (v2,w))
by BILINEAR:9
.=
((FunctionalSAF (sc,w)) . v1) + ((FunctionalSAF (sc,w)) . v2)
by BILINEAR:9
;
verum
end;
A10:
sc is hermitan
proof
let v,
w be
Vector of
(VectQuot (V,(LKer f)));
HERMITAN:def 5 sc . (v,w) = (sc . (w,v)) *'
reconsider A =
w as
Vector of
(VectQuot (V,(RKer (f *')))) by Th56;
consider wa being
Vector of
V such that A11:
A = wa + (RKer (f *'))
by VECTSP10:22;
A12:
w = wa + (LKer f)
by A11, Th56;
reconsider B =
v as
Vector of
(VectQuot (V,(RKer (f *')))) by Th56;
consider va being
Vector of
V such that A13:
v = va + (LKer f)
by VECTSP10:22;
A14:
B = va + (RKer (f *'))
by A13, Th56;
thus sc . (
v,
w) =
f . (
va,
wa)
by A11, A13, Def12
.=
(f . (wa,va)) *'
by Def5
.=
(sc . (w,v)) *'
by A14, A12, Def12
;
verum
end;
sc is diagReR+0valued
hence
Q*Form f is diagReR+0valued hermitan-Form of (VectQuot (V,(LKer f)))
by A1, A5, A10; verum