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))); :: according to BILINEAR:def 14 :: thesis: FunctionalSAF (sc,w) is homogeneous
set fg = FunctionalSAF (sc,w);
let v be Vector of (VectQuot (V,(LKer f))); :: according to HAHNBAN1:def 8 :: thesis: 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 ; :: thesis: (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 ; :: thesis: verum
end;
A5: sc is additiveSAF
proof
let w be Vector of (VectQuot (V,(LKer f))); :: according to BILINEAR:def 12 :: thesis: FunctionalSAF (sc,w) is additive
set fg = FunctionalSAF (sc,w);
let v1, v2 be Vector of (VectQuot (V,(LKer f))); :: according to VECTSP_1:def 19 :: thesis: (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 ; :: thesis: verum
end;
A10: sc is hermitan
proof
let v, w be Vector of (VectQuot (V,(LKer f))); :: according to HERMITAN:def 5 :: thesis: 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 ; :: thesis: verum
end;
sc is diagReR+0valued
proof
let v be Vector of (VectQuot (V,(LKer f))); :: according to HERMITAN:def 7 :: thesis: 0 <= Re (sc . (v,v))
reconsider A = v as Vector of (VectQuot (V,(RKer (f *')))) by Th56;
consider va being Vector of V such that
A15: v = va + (LKer f) by VECTSP10:22;
A = va + (RKer (f *')) by A15, Th56;
then sc . (v,v) = f . (va,va) by A15, Def12;
hence 0 <= Re (sc . (v,v)) by Def7; :: thesis: verum
end;
hence Q*Form f is diagReR+0valued hermitan-Form of (VectQuot (V,(LKer f))) by A1, A5, A10; :: thesis: verum