let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for V, W being VectSp of K

for f being bilinear-Form of V,W holds

( leftker (QForm f) = leftker (RQForm (LQForm f)) & rightker (QForm f) = rightker (RQForm (LQForm f)) & leftker (QForm f) = leftker (LQForm (RQForm f)) & rightker (QForm f) = rightker (LQForm (RQForm f)) )

let V, W be VectSp of K; :: thesis: for f being bilinear-Form of V,W holds

( leftker (QForm f) = leftker (RQForm (LQForm f)) & rightker (QForm f) = rightker (RQForm (LQForm f)) & leftker (QForm f) = leftker (LQForm (RQForm f)) & rightker (QForm f) = rightker (LQForm (RQForm f)) )

let f be bilinear-Form of V,W; :: thesis: ( leftker (QForm f) = leftker (RQForm (LQForm f)) & rightker (QForm f) = rightker (RQForm (LQForm f)) & leftker (QForm f) = leftker (LQForm (RQForm f)) & rightker (QForm f) = rightker (LQForm (RQForm f)) )

set vq = VectQuot (V,(LKer f));

set wq = VectQuot (W,(RKer f));

set wqr = VectQuot (W,(RKer (LQForm f)));

set vql = VectQuot (V,(LKer (RQForm f)));

set rlf = RQForm (LQForm f);

set qf = QForm f;

set lrf = LQForm (RQForm f);

thus leftker (QForm f) c= leftker (RQForm (LQForm f)) :: according to XBOOLE_0:def 10 :: thesis: ( leftker (RQForm (LQForm f)) c= leftker (QForm f) & rightker (QForm f) = rightker (RQForm (LQForm f)) & leftker (QForm f) = leftker (LQForm (RQForm f)) & rightker (QForm f) = rightker (LQForm (RQForm f)) )

assume x in rightker (LQForm (RQForm f)) ; :: thesis: x in rightker (QForm f)

then consider ww being Vector of (VectQuot (W,(RKer f))) such that

A15: x = ww and

A16: for vv being Vector of (VectQuot (V,(LKer (RQForm f)))) holds (LQForm (RQForm f)) . (vv,ww) = 0. K ;

for f being bilinear-Form of V,W holds

( leftker (QForm f) = leftker (RQForm (LQForm f)) & rightker (QForm f) = rightker (RQForm (LQForm f)) & leftker (QForm f) = leftker (LQForm (RQForm f)) & rightker (QForm f) = rightker (LQForm (RQForm f)) )

let V, W be VectSp of K; :: thesis: for f being bilinear-Form of V,W holds

( leftker (QForm f) = leftker (RQForm (LQForm f)) & rightker (QForm f) = rightker (RQForm (LQForm f)) & leftker (QForm f) = leftker (LQForm (RQForm f)) & rightker (QForm f) = rightker (LQForm (RQForm f)) )

let f be bilinear-Form of V,W; :: thesis: ( leftker (QForm f) = leftker (RQForm (LQForm f)) & rightker (QForm f) = rightker (RQForm (LQForm f)) & leftker (QForm f) = leftker (LQForm (RQForm f)) & rightker (QForm f) = rightker (LQForm (RQForm f)) )

set vq = VectQuot (V,(LKer f));

set wq = VectQuot (W,(RKer f));

set wqr = VectQuot (W,(RKer (LQForm f)));

set vql = VectQuot (V,(LKer (RQForm f)));

set rlf = RQForm (LQForm f);

set qf = QForm f;

set lrf = LQForm (RQForm f);

thus leftker (QForm f) c= leftker (RQForm (LQForm f)) :: according to XBOOLE_0:def 10 :: thesis: ( leftker (RQForm (LQForm f)) c= leftker (QForm f) & rightker (QForm f) = rightker (RQForm (LQForm f)) & leftker (QForm f) = leftker (LQForm (RQForm f)) & rightker (QForm f) = rightker (LQForm (RQForm f)) )

proof

thus
leftker (RQForm (LQForm f)) c= leftker (QForm f)
:: thesis: ( rightker (QForm f) = rightker (RQForm (LQForm f)) & leftker (QForm f) = leftker (LQForm (RQForm f)) & rightker (QForm f) = rightker (LQForm (RQForm f)) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker (QForm f) or x in leftker (RQForm (LQForm f)) )

assume x in leftker (QForm f) ; :: thesis: x in leftker (RQForm (LQForm f))

then consider vv being Vector of (VectQuot (V,(LKer f))) such that

A1: x = vv and

A2: for ww being Vector of (VectQuot (W,(RKer f))) holds (QForm f) . (vv,ww) = 0. K ;

end;assume x in leftker (QForm f) ; :: thesis: x in leftker (RQForm (LQForm f))

then consider vv being Vector of (VectQuot (V,(LKer f))) such that

A1: x = vv and

A2: for ww being Vector of (VectQuot (W,(RKer f))) holds (QForm f) . (vv,ww) = 0. K ;

now :: thesis: for ww being Vector of (VectQuot (W,(RKer (LQForm f)))) holds (RQForm (LQForm f)) . (vv,ww) = 0. K

hence
x in leftker (RQForm (LQForm f))
by A1; :: thesis: verumlet ww be Vector of (VectQuot (W,(RKer (LQForm f)))); :: thesis: (RQForm (LQForm f)) . (vv,ww) = 0. K

reconsider w = ww as Vector of (VectQuot (W,(RKer f))) by Th46;

thus (RQForm (LQForm f)) . (vv,ww) = (QForm f) . (vv,w) by Th48

.= 0. K by A2 ; :: thesis: verum

end;reconsider w = ww as Vector of (VectQuot (W,(RKer f))) by Th46;

thus (RQForm (LQForm f)) . (vv,ww) = (QForm f) . (vv,w) by Th48

.= 0. K by A2 ; :: thesis: verum

proof

thus
rightker (QForm f) c= rightker (RQForm (LQForm f))
:: according to XBOOLE_0:def 10 :: thesis: ( rightker (RQForm (LQForm f)) c= rightker (QForm f) & leftker (QForm f) = leftker (LQForm (RQForm f)) & rightker (QForm f) = rightker (LQForm (RQForm f)) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker (RQForm (LQForm f)) or x in leftker (QForm f) )

assume x in leftker (RQForm (LQForm f)) ; :: thesis: x in leftker (QForm f)

then consider vv being Vector of (VectQuot (V,(LKer f))) such that

A3: x = vv and

A4: for ww being Vector of (VectQuot (W,(RKer (LQForm f)))) holds (RQForm (LQForm f)) . (vv,ww) = 0. K ;

end;assume x in leftker (RQForm (LQForm f)) ; :: thesis: x in leftker (QForm f)

then consider vv being Vector of (VectQuot (V,(LKer f))) such that

A3: x = vv and

A4: for ww being Vector of (VectQuot (W,(RKer (LQForm f)))) holds (RQForm (LQForm f)) . (vv,ww) = 0. K ;

now :: thesis: for ww being Vector of (VectQuot (W,(RKer f))) holds (QForm f) . (vv,ww) = 0. K

hence
x in leftker (QForm f)
by A3; :: thesis: verumlet ww be Vector of (VectQuot (W,(RKer f))); :: thesis: (QForm f) . (vv,ww) = 0. K

reconsider w = ww as Vector of (VectQuot (W,(RKer (LQForm f)))) by Th46;

thus (QForm f) . (vv,ww) = (RQForm (LQForm f)) . (vv,w) by Th48

.= 0. K by A4 ; :: thesis: verum

end;reconsider w = ww as Vector of (VectQuot (W,(RKer (LQForm f)))) by Th46;

thus (QForm f) . (vv,ww) = (RQForm (LQForm f)) . (vv,w) by Th48

.= 0. K by A4 ; :: thesis: verum

proof

thus
rightker (RQForm (LQForm f)) c= rightker (QForm f)
:: thesis: ( leftker (QForm f) = leftker (LQForm (RQForm f)) & rightker (QForm f) = rightker (LQForm (RQForm f)) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rightker (QForm f) or x in rightker (RQForm (LQForm f)) )

assume x in rightker (QForm f) ; :: thesis: x in rightker (RQForm (LQForm f))

then consider ww being Vector of (VectQuot (W,(RKer f))) such that

A5: x = ww and

A6: for vv being Vector of (VectQuot (V,(LKer f))) holds (QForm f) . (vv,ww) = 0. K ;

reconsider w = ww as Vector of (VectQuot (W,(RKer (LQForm f)))) by Th46;

end;assume x in rightker (QForm f) ; :: thesis: x in rightker (RQForm (LQForm f))

then consider ww being Vector of (VectQuot (W,(RKer f))) such that

A5: x = ww and

A6: for vv being Vector of (VectQuot (V,(LKer f))) holds (QForm f) . (vv,ww) = 0. K ;

reconsider w = ww as Vector of (VectQuot (W,(RKer (LQForm f)))) by Th46;

now :: thesis: for vv being Vector of (VectQuot (V,(LKer f))) holds (RQForm (LQForm f)) . (vv,w) = 0. K

hence
x in rightker (RQForm (LQForm f))
by A5; :: thesis: verumlet vv be Vector of (VectQuot (V,(LKer f))); :: thesis: (RQForm (LQForm f)) . (vv,w) = 0. K

thus (RQForm (LQForm f)) . (vv,w) = (QForm f) . (vv,ww) by Th48

.= 0. K by A6 ; :: thesis: verum

end;thus (RQForm (LQForm f)) . (vv,w) = (QForm f) . (vv,ww) by Th48

.= 0. K by A6 ; :: thesis: verum

proof

thus
leftker (QForm f) c= leftker (LQForm (RQForm f))
:: according to XBOOLE_0:def 10 :: thesis: ( leftker (LQForm (RQForm f)) c= leftker (QForm f) & rightker (QForm f) = rightker (LQForm (RQForm f)) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rightker (RQForm (LQForm f)) or x in rightker (QForm f) )

assume x in rightker (RQForm (LQForm f)) ; :: thesis: x in rightker (QForm f)

then consider ww being Vector of (VectQuot (W,(RKer (LQForm f)))) such that

A7: x = ww and

A8: for vv being Vector of (VectQuot (V,(LKer f))) holds (RQForm (LQForm f)) . (vv,ww) = 0. K ;

reconsider w = ww as Vector of (VectQuot (W,(RKer f))) by Th46;

end;assume x in rightker (RQForm (LQForm f)) ; :: thesis: x in rightker (QForm f)

then consider ww being Vector of (VectQuot (W,(RKer (LQForm f)))) such that

A7: x = ww and

A8: for vv being Vector of (VectQuot (V,(LKer f))) holds (RQForm (LQForm f)) . (vv,ww) = 0. K ;

reconsider w = ww as Vector of (VectQuot (W,(RKer f))) by Th46;

now :: thesis: for vv being Vector of (VectQuot (V,(LKer f))) holds (QForm f) . (vv,w) = 0. K

hence
x in rightker (QForm f)
by A7; :: thesis: verumlet vv be Vector of (VectQuot (V,(LKer f))); :: thesis: (QForm f) . (vv,w) = 0. K

thus (QForm f) . (vv,w) = (RQForm (LQForm f)) . (vv,ww) by Th48

.= 0. K by A8 ; :: thesis: verum

end;thus (QForm f) . (vv,w) = (RQForm (LQForm f)) . (vv,ww) by Th48

.= 0. K by A8 ; :: thesis: verum

proof

thus
leftker (LQForm (RQForm f)) c= leftker (QForm f)
:: thesis: rightker (QForm f) = rightker (LQForm (RQForm f))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker (QForm f) or x in leftker (LQForm (RQForm f)) )

assume x in leftker (QForm f) ; :: thesis: x in leftker (LQForm (RQForm f))

then consider vv being Vector of (VectQuot (V,(LKer f))) such that

A9: x = vv and

A10: for ww being Vector of (VectQuot (W,(RKer f))) holds (QForm f) . (vv,ww) = 0. K ;

reconsider v = vv as Vector of (VectQuot (V,(LKer (RQForm f)))) by Th47;

end;assume x in leftker (QForm f) ; :: thesis: x in leftker (LQForm (RQForm f))

then consider vv being Vector of (VectQuot (V,(LKer f))) such that

A9: x = vv and

A10: for ww being Vector of (VectQuot (W,(RKer f))) holds (QForm f) . (vv,ww) = 0. K ;

reconsider v = vv as Vector of (VectQuot (V,(LKer (RQForm f)))) by Th47;

now :: thesis: for ww being Vector of (VectQuot (W,(RKer f))) holds (LQForm (RQForm f)) . (v,ww) = 0. K

hence
x in leftker (LQForm (RQForm f))
by A9; :: thesis: verumlet ww be Vector of (VectQuot (W,(RKer f))); :: thesis: (LQForm (RQForm f)) . (v,ww) = 0. K

thus (LQForm (RQForm f)) . (v,ww) = (QForm f) . (vv,ww) by Th48

.= 0. K by A10 ; :: thesis: verum

end;thus (LQForm (RQForm f)) . (v,ww) = (QForm f) . (vv,ww) by Th48

.= 0. K by A10 ; :: thesis: verum

proof

thus
rightker (QForm f) c= rightker (LQForm (RQForm f))
:: according to XBOOLE_0:def 10 :: thesis: rightker (LQForm (RQForm f)) c= rightker (QForm f)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker (LQForm (RQForm f)) or x in leftker (QForm f) )

assume x in leftker (LQForm (RQForm f)) ; :: thesis: x in leftker (QForm f)

then consider vv being Vector of (VectQuot (V,(LKer (RQForm f)))) such that

A11: x = vv and

A12: for ww being Vector of (VectQuot (W,(RKer f))) holds (LQForm (RQForm f)) . (vv,ww) = 0. K ;

reconsider v = vv as Vector of (VectQuot (V,(LKer f))) by Th47;

end;assume x in leftker (LQForm (RQForm f)) ; :: thesis: x in leftker (QForm f)

then consider vv being Vector of (VectQuot (V,(LKer (RQForm f)))) such that

A11: x = vv and

A12: for ww being Vector of (VectQuot (W,(RKer f))) holds (LQForm (RQForm f)) . (vv,ww) = 0. K ;

reconsider v = vv as Vector of (VectQuot (V,(LKer f))) by Th47;

now :: thesis: for ww being Vector of (VectQuot (W,(RKer f))) holds (QForm f) . (v,ww) = 0. K

hence
x in leftker (QForm f)
by A11; :: thesis: verumlet ww be Vector of (VectQuot (W,(RKer f))); :: thesis: (QForm f) . (v,ww) = 0. K

thus (QForm f) . (v,ww) = (LQForm (RQForm f)) . (vv,ww) by Th48

.= 0. K by A12 ; :: thesis: verum

end;thus (QForm f) . (v,ww) = (LQForm (RQForm f)) . (vv,ww) by Th48

.= 0. K by A12 ; :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rightker (LQForm (RQForm f)) or x in rightker (QForm f) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rightker (QForm f) or x in rightker (LQForm (RQForm f)) )

assume x in rightker (QForm f) ; :: thesis: x in rightker (LQForm (RQForm f))

then consider ww being Vector of (VectQuot (W,(RKer f))) such that

A13: x = ww and

A14: for vv being Vector of (VectQuot (V,(LKer f))) holds (QForm f) . (vv,ww) = 0. K ;

end;assume x in rightker (QForm f) ; :: thesis: x in rightker (LQForm (RQForm f))

then consider ww being Vector of (VectQuot (W,(RKer f))) such that

A13: x = ww and

A14: for vv being Vector of (VectQuot (V,(LKer f))) holds (QForm f) . (vv,ww) = 0. K ;

now :: thesis: for vv being Vector of (VectQuot (V,(LKer (RQForm f)))) holds (LQForm (RQForm f)) . (vv,ww) = 0. K

hence
x in rightker (LQForm (RQForm f))
by A13; :: thesis: verumlet vv be Vector of (VectQuot (V,(LKer (RQForm f)))); :: thesis: (LQForm (RQForm f)) . (vv,ww) = 0. K

reconsider v = vv as Vector of (VectQuot (V,(LKer f))) by Th47;

thus (LQForm (RQForm f)) . (vv,ww) = (QForm f) . (v,ww) by Th48

.= 0. K by A14 ; :: thesis: verum

end;reconsider v = vv as Vector of (VectQuot (V,(LKer f))) by Th47;

thus (LQForm (RQForm f)) . (vv,ww) = (QForm f) . (v,ww) by Th48

.= 0. K by A14 ; :: thesis: verum

assume x in rightker (LQForm (RQForm f)) ; :: thesis: x in rightker (QForm f)

then consider ww being Vector of (VectQuot (W,(RKer f))) such that

A15: x = ww and

A16: for vv being Vector of (VectQuot (V,(LKer (RQForm f)))) holds (LQForm (RQForm f)) . (vv,ww) = 0. K ;

now :: thesis: for vv being Vector of (VectQuot (V,(LKer f))) holds (QForm f) . (vv,ww) = 0. K

hence
x in rightker (QForm f)
by A15; :: thesis: verumlet vv be Vector of (VectQuot (V,(LKer f))); :: thesis: (QForm f) . (vv,ww) = 0. K

reconsider v = vv as Vector of (VectQuot (V,(LKer (RQForm f)))) by Th47;

thus (QForm f) . (vv,ww) = (LQForm (RQForm f)) . (v,ww) by Th48

.= 0. K by A16 ; :: thesis: verum

end;reconsider v = vv as Vector of (VectQuot (V,(LKer (RQForm f)))) by Th47;

thus (QForm f) . (vv,ww) = (LQForm (RQForm f)) . (v,ww) by Th48

.= 0. K by A16 ; :: thesis: verum