let V be VectSp of F_Complex ; :: thesis: for f being diagReR+0valued hermitan-Form of V
for A, B being Vector of (VectQuot (V,(LKer f)))
for v, w being Vector of V st A = v + (LKer f) & B = w + (LKer f) holds
(ScalarForm f) . (A,B) = f . (v,w)
let f be diagReR+0valued hermitan-Form of V; :: thesis: for A, B being Vector of (VectQuot (V,(LKer f)))
for v, w being Vector of V st A = v + (LKer f) & B = w + (LKer f) holds
(ScalarForm f) . (A,B) = f . (v,w)
set vq = VectQuot (V,(LKer f));
set vr = VectQuot (V,(RKer (f *')));
let A, B be Vector of (VectQuot (V,(LKer f))); :: thesis: for v, w being Vector of V st A = v + (LKer f) & B = w + (LKer f) holds
(ScalarForm f) . (A,B) = f . (v,w)
let v, w be Vector of V; :: thesis: ( A = v + (LKer f) & B = w + (LKer f) implies (ScalarForm f) . (A,B) = f . (v,w) )
reconsider W = B as Vector of (VectQuot (V,(RKer (f *')))) by Th56;
assume that
A1: A = v + (LKer f) and
A2: B = w + (LKer f) ; :: thesis: (ScalarForm f) . (A,B) = f . (v,w)
W = w + (RKer (f *')) by A2, Th56;
hence (ScalarForm f) . (A,B) = f . (v,w) by A1, Def12; :: thesis: verum