let K be non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; :: thesis: for V being non empty VectSpStr of K
for W being VectSp of K
for f being Functional of V
for g being linear-Functional of W st f <> 0Functional V holds
( RKer (FormFunctional f,g) = Ker g & RQForm (FormFunctional f,g) = FormFunctional f,(CQFunctional g) )
let V be non empty VectSpStr of K; :: thesis: for W being VectSp of K
for f being Functional of V
for g being linear-Functional of W st f <> 0Functional V holds
( RKer (FormFunctional f,g) = Ker g & RQForm (FormFunctional f,g) = FormFunctional f,(CQFunctional g) )
let W be VectSp of K; :: thesis: for f being Functional of V
for g being linear-Functional of W st f <> 0Functional V holds
( RKer (FormFunctional f,g) = Ker g & RQForm (FormFunctional f,g) = FormFunctional f,(CQFunctional g) )
let f be Functional of V; :: thesis: for g being linear-Functional of W st f <> 0Functional V holds
( RKer (FormFunctional f,g) = Ker g & RQForm (FormFunctional f,g) = FormFunctional f,(CQFunctional g) )
let g be linear-Functional of W; :: thesis: ( f <> 0Functional V implies ( RKer (FormFunctional f,g) = Ker g & RQForm (FormFunctional f,g) = FormFunctional f,(CQFunctional g) ) )
assume A1:
f <> 0Functional V
; :: thesis: ( RKer (FormFunctional f,g) = Ker g & RQForm (FormFunctional f,g) = FormFunctional f,(CQFunctional g) )
set fg = FormFunctional f,g;
set cg = CQFunctional g;
set fcfg = FormFunctional f,(CQFunctional g);
set wqr = VectQuot W,(RKer (FormFunctional f,g));
set wq = VectQuot W,(Ker g);
A2:
the carrier of (RKer (FormFunctional f,g)) = rightker (FormFunctional f,g)
by Def20;
rightker (FormFunctional f,g) = ker g
by A1, Th54;
hence A3:
RKer (FormFunctional f,g) = Ker g
by A2, VECTSP10:def 11; :: thesis: RQForm (FormFunctional f,g) = FormFunctional f,(CQFunctional g)
A4:
dom (RQForm (FormFunctional f,g)) = [:the carrier of V,the carrier of (VectQuot W,(RKer (FormFunctional f,g))):]
by FUNCT_2:def 1;
A5:
dom (FormFunctional f,(CQFunctional g)) = [:the carrier of V,the carrier of (VectQuot W,(Ker g)):]
by FUNCT_2:def 1;
now let x be
set ;
:: thesis: ( x in dom (FormFunctional f,(CQFunctional g)) implies (FormFunctional f,(CQFunctional g)) . x = (RQForm (FormFunctional f,g)) . x )assume
x in dom (FormFunctional f,(CQFunctional g))
;
:: thesis: (FormFunctional f,(CQFunctional g)) . x = (RQForm (FormFunctional f,g)) . xthen consider A being
Vector of
V,
B being
Vector of
(VectQuot W,(Ker g)) such that A6:
x = [A,B]
by DOMAIN_1:9;
consider w being
Vector of
W such that A7:
B = w + (Ker g)
by VECTSP10:23;
thus (FormFunctional f,(CQFunctional g)) . x =
(FormFunctional f,(CQFunctional g)) . A,
B
by A6
.=
(f . A) * ((CQFunctional g) . B)
by Def11
.=
(f . A) * (g . w)
by A7, VECTSP10:36
.=
(FormFunctional f,g) . A,
w
by Def11
.=
(RQForm (FormFunctional f,g)) . A,
B
by A3, A7, Def22
.=
(RQForm (FormFunctional f,g)) . x
by A6
;
:: thesis: verum end;
hence
RQForm (FormFunctional f,g) = FormFunctional f,(CQFunctional g)
by A3, A4, A5, FUNCT_1:9; :: thesis: verum