Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

### Bilinear Functionals in Vector Spaces

by
Jaroslaw Kotowicz

Received November 5, 2002

MML identifier: BILINEAR
[ Mizar article, MML identifier index ]

```environ

vocabulary RLVECT_1, VECTSP_1, ARYTM_1, HAHNBAN, FUNCT_1, SUBSET_1, FUNCOP_1,
GRCAT_1, UNIALG_1, BINOP_1, LATTICES, RELAT_1, HAHNBAN1, FUNCT_5,
RLSUB_1, ALGSTR_2, REALSET1, BOOLE, SEQM_3, GROUP_6, VECTSP10, BILINEAR,
RELAT_2, SPPOL_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, DOMAIN_1, FUNCT_1,
RELAT_1, PRE_TOPC, REALSET1, RLVECT_1, BINOP_1, VECTSP_1, RELSET_1,
FUNCT_2, SEQM_3, FUNCT_5, VECTSP_4, BORSUK_1, HAHNBAN1, VECTSP10;
constructors DOMAIN_1, NATTRA_1, BORSUK_1, VECTSP10;
clusters STRUCT_0, SUBSET_1, RELSET_1, VECTSP_1, HAHNBAN1, VECTSP_4, VECTSP10,
XBOOLE_0;
requirements SUBSET, BOOLE;

begin
:: Two Form on Vector Spaces and Operations on Them.

definition
let K be 1-sorted;
let V,W be VectSpStr over K;
mode Form of V,W is Function of [:the carrier of V,the carrier of W:],
the carrier of K;
canceled;
end;

definition
let K be non empty ZeroStr;
let V,W be VectSpStr over K;
func NulForm(V,W) -> Form of V,W equals
:: BILINEAR:def 2
[:the carrier of V,the carrier of W:] --> 0.K;
end;

definition
let K be non empty LoopStr;
let V,W be non empty VectSpStr over K;
let f,g be Form of V,W;
func f+g -> Form of V,W means
:: BILINEAR:def 3
for v be Vector of V, w be Vector of W holds it.[v,w] = f.[v,w]+g.[v,w];
end;

definition
let K be non empty HGrStr;
let V,W be non empty VectSpStr over K;
let f be Form of V,W;
let a be Element of K;
func a*f -> Form of V,W means
:: BILINEAR:def 4
for v be Vector of V, w be Vector of W holds it.[v,w] = a*f.[v,w];
end;

definition
let K be non empty LoopStr;
let V,W be non empty VectSpStr over K;
let f be Form of V,W;
func -f -> Form of V,W means
:: BILINEAR:def 5
for v be Vector of V, w be Vector of W holds it.[v,w] = -f.[v,w];
end;

definition
let K be add-associative right_zeroed right_complementable
left-distributive left_unital (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
let f be Form of V,W;
redefine func -f -> Form of V,W equals
:: BILINEAR:def 6
(- 1_ K) *f;
end;

definition
let K be non empty LoopStr;
let V,W be non empty VectSpStr over K;
let f,g be Form of V,W;
func f-g -> Form of V,W equals
:: BILINEAR:def 7
f + -g;
end;

definition
let K be non empty LoopStr;
let V,W be non empty VectSpStr over K;
let f,g be Form of V,W;
redefine func f - g -> Form of V,W means
:: BILINEAR:def 8
for v be Vector of V, w be Vector of W holds it.[v,w] = f.[v,w] - g.[v,w];
end;

definition
let K be Abelian (non empty LoopStr);
let V,W be non empty VectSpStr over K;
let f,g be Form of V,W;
redefine func f+g;
commutativity;
end;

theorem :: BILINEAR:1
for K be non empty ZeroStr
for V,W be non empty VectSpStr over K
for v be Vector of V,w be Vector of W holds NulForm(V,W).[v,w] = 0.K;

theorem :: BILINEAR:2
for K be right_zeroed (non empty LoopStr)
for V,W be non empty VectSpStr over K
for f be Form of V,W holds f + NulForm(V,W) = f;

theorem :: BILINEAR:3
for K be add-associative (non empty LoopStr)
for V,W be non empty VectSpStr over K
for f,g,h be Form of V,W holds f+g+h = f+(g+h);

theorem :: BILINEAR:4
for K be add-associative right_zeroed right_complementable (non empty LoopStr
)
for V,W be non empty VectSpStr over K
for f be Form of V,W holds f - f = NulForm(V,W);

theorem :: BILINEAR:5
for K be right-distributive (non empty doubleLoopStr)
for V,W be non empty VectSpStr over K, a be Element of K
for f,g be Form of V,W holds a*(f+g) = a*f+a*g;

theorem :: BILINEAR:6
for K be left-distributive (non empty doubleLoopStr)
for V,W be non empty VectSpStr over K
for a,b be Element of K
for f be Form of V,W holds (a+b)*f = a*f+b*f;

theorem :: BILINEAR:7
for K be associative (non empty doubleLoopStr)
for V,W be non empty VectSpStr over K
for a,b be Element of K
for f be Form of V,W holds (a*b)*f = a*(b*f);

theorem :: BILINEAR:8
for K be left_unital (non empty doubleLoopStr)
for V,W be non empty VectSpStr over K
for f be Form of V,W holds (1_ K)*f = f;

begin
:: Functional generated by Two Form when the One of Arguments is Fixed.

definition
let K be non empty 1-sorted;
let V,W be non empty VectSpStr over K;
let f be Form of V,W, v be Vector of V;
func FunctionalFAF(f,v) -> Functional of W equals
:: BILINEAR:def 9
(curry f).v;
end;

definition
let K be non empty 1-sorted;
let V,W be non empty VectSpStr over K;
let f be Form of V,W, w be Vector of W;
func FunctionalSAF(f,w) -> Functional of V equals
:: BILINEAR:def 10
(curry' f).w;
end;

theorem :: BILINEAR:9
for K be non empty 1-sorted
for V,W be non empty VectSpStr over K
for f be Form of V,W, v be Vector of V holds
dom (FunctionalFAF(f,v)) = the carrier of W &
rng (FunctionalFAF(f,v)) c= the carrier of K &
for w be Vector of W holds (FunctionalFAF(f,v)).w = f.[v,w];

theorem :: BILINEAR:10
for K be non empty 1-sorted
for V,W be non empty VectSpStr over K
for f be Form of V,W, w be Vector of W holds
dom (FunctionalSAF(f,w)) = the carrier of V &
rng (FunctionalSAF(f,w)) c= the carrier of K &
for v be Vector of V holds (FunctionalSAF(f,w)).v = f.[v,w];

theorem :: BILINEAR:11
for K be non empty ZeroStr
for V,W be non empty VectSpStr over K
for f be Form of V,W, v be Vector of V holds
FunctionalFAF(NulForm(V,W),v) = 0Functional(W);

theorem :: BILINEAR:12
for K be non empty ZeroStr
for V,W be non empty VectSpStr over K
for f be Form of V,W, w be Vector of W holds
FunctionalSAF(NulForm(V,W),w) = 0Functional(V);

theorem :: BILINEAR:13
for K be non empty LoopStr
for V,W be non empty VectSpStr over K
for f,g be Form of V,W, w be Vector of W holds
FunctionalSAF(f+g,w) = FunctionalSAF(f,w) + FunctionalSAF(g,w);

theorem :: BILINEAR:14
for K be non empty LoopStr
for V,W be non empty VectSpStr over K
for f,g be Form of V,W, v be Vector of V holds
FunctionalFAF(f+g,v) = FunctionalFAF(f,v) + FunctionalFAF(g,v);

theorem :: BILINEAR:15
for K be non empty doubleLoopStr
for V,W be non empty VectSpStr over K
for f be Form of V,W, a be Element of K, w be Vector of W holds
FunctionalSAF(a*f,w) = a*FunctionalSAF(f,w);

theorem :: BILINEAR:16
for K be non empty doubleLoopStr
for V,W be non empty VectSpStr over K
for f be Form of V,W, a be Element of K, v be Vector of V holds
FunctionalFAF(a*f,v) = a*FunctionalFAF(f,v);

theorem :: BILINEAR:17
for K be non empty LoopStr
for V,W be non empty VectSpStr over K
for f be Form of V,W, w be Vector of W holds
FunctionalSAF(-f,w) = - FunctionalSAF(f,w);

theorem :: BILINEAR:18
for K be non empty LoopStr
for V,W be non empty VectSpStr over K
for f be Form of V,W, v be Vector of V holds
FunctionalFAF(-f,v) = -FunctionalFAF(f,v);

theorem :: BILINEAR:19
for K be non empty LoopStr
for V,W be non empty VectSpStr over K
for f,g be Form of V,W, w be Vector of W holds
FunctionalSAF(f-g,w) = FunctionalSAF(f,w) - FunctionalSAF(g,w);

theorem :: BILINEAR:20
for K be non empty LoopStr
for V,W be non empty VectSpStr over K
for f,g be Form of V,W, v be Vector of V holds
FunctionalFAF(f-g,v) = FunctionalFAF(f,v) - FunctionalFAF(g,v);

begin
:: Two Form generated by Functionals.

definition
let K be non empty HGrStr;
let V,W be non empty VectSpStr over K;
let f be Functional of V; let g be Functional of W;
func FormFunctional(f,g) -> Form of V,W means
:: BILINEAR:def 11
for v be Vector of V, w be Vector of W holds it.[v,w]= f.v * g.w;
end;

theorem :: BILINEAR:21
for K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr)
for V,W be non empty VectSpStr over K
for f be Functional of V ,v be Vector of V, w be Vector of W holds
FormFunctional(f,0Functional(W)).[v,w] = 0.K;

theorem :: BILINEAR:22
for K be add-associative right_zeroed right_complementable
left-distributive (non empty doubleLoopStr)
for V,W be non empty VectSpStr over K
for g be Functional of W, v be Vector of V, w be Vector of W holds
FormFunctional(0Functional(V),g).[v,w] = 0.K;

theorem :: BILINEAR:23
for K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr)
for V,W be non empty VectSpStr over K
for f be Functional of V holds FormFunctional(f,0Functional(W)) = NulForm(V,W)
;

theorem :: BILINEAR:24
for K be add-associative right_zeroed right_complementable
left-distributive (non empty doubleLoopStr)
for V,W be non empty VectSpStr over K
for g be Functional of W holds FormFunctional(0Functional(V),g) = NulForm(V,W)
;

theorem :: BILINEAR:25
for K be non empty HGrStr
for V,W be non empty VectSpStr over K
for f be Functional of V, g be Functional of W, v be Vector of V holds
FunctionalFAF(FormFunctional(f,g),v) = f.v * g;

theorem :: BILINEAR:26
for K be commutative (non empty HGrStr)
for V,W be non empty VectSpStr over K
for f be Functional of V, g be Functional of W, w be Vector of W holds
FunctionalSAF(FormFunctional(f,g),w) = g.w * f;

begin
::Bilinear Forms and Their Properties

definition
let K be non empty LoopStr;
let V,W be non empty VectSpStr over K;
let f be Form of V,W;
attr f is additiveFAF means
:: BILINEAR:def 12
for v be Vector of V holds FunctionalFAF(f,v) is additive;
attr f is additiveSAF means
:: BILINEAR:def 13
for w be Vector of W holds FunctionalSAF(f,w) is additive;
end;

definition
let K be non empty HGrStr;
let V,W be non empty VectSpStr over K;
let f be Form of V,W;
attr f is homogeneousFAF means
:: BILINEAR:def 14
for v be Vector of V holds FunctionalFAF(f,v) is homogeneous;
attr f is homogeneousSAF means
:: BILINEAR:def 15
for w be Vector of W holds FunctionalSAF(f,w) is homogeneous;
end;

definition
let K be right_zeroed (non empty LoopStr);
let V,W be non empty VectSpStr over K;
cluster NulForm(V,W) -> additiveFAF;
cluster NulForm(V,W) -> additiveSAF;
end;

definition
let K be right_zeroed (non empty LoopStr);
let V,W be non empty VectSpStr over K;
end;

definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
cluster NulForm(V,W) -> homogeneousFAF;
cluster NulForm(V,W) -> homogeneousSAF;
end;

definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
cluster additiveFAF homogeneousFAF additiveSAF homogeneousSAF Form of V,W;
end;

definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
mode bilinear-Form of V,W is additiveSAF homogeneousSAF
additiveFAF homogeneousFAF Form of V,W;
end;

definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
let f be additiveFAF Form of V,W, v be Vector of V;
cluster FunctionalFAF(f,v) -> additive;
end;

definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
let f be additiveSAF Form of V,W, w be Vector of W;
cluster FunctionalSAF(f,w) -> additive;
end;

definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
let f be homogeneousFAF Form of V,W, v be Vector of V;
cluster FunctionalFAF(f,v) -> homogeneous;
end;

definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
let f be homogeneousSAF Form of V,W, w be Vector of W;
cluster FunctionalSAF(f,w) -> homogeneous;
end;

definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
let f be Functional of V, g be additive Functional of W;
cluster FormFunctional(f,g) -> additiveFAF;
end;

definition
let K be add-associative right_zeroed right_complementable
commutative right-distributive (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
let f be additive Functional of V, g be Functional of W;
cluster FormFunctional(f,g) -> additiveSAF;
end;

definition
let K be add-associative right_zeroed right_complementable commutative
associative right-distributive (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
let f be Functional of V, g be homogeneous Functional of W;
cluster FormFunctional(f,g) -> homogeneousFAF;
end;

definition
let K be add-associative right_zeroed right_complementable commutative
associative right-distributive (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
let f be homogeneous Functional of V, g be Functional of W;
cluster FormFunctional(f,g) -> homogeneousSAF;
end;

definition
let K be non degenerated (non empty doubleLoopStr);
let V be non trivial (non empty VectSpStr over K),
W be non empty VectSpStr over K;
let f be Functional of V, g be Functional of W;
cluster FormFunctional(f,g) -> non trivial;
end;

definition
let K be non degenerated (non empty doubleLoopStr);
let V be non empty VectSpStr over K,
W be non trivial (non empty VectSpStr over K);
let f be Functional of V, g be Functional of W;
cluster FormFunctional(f,g) -> non trivial;
end;

definition
let K be Field;
let V,W be non trivial VectSp of K;
let f be non constant 0-preserving Functional of V,
g be non constant 0-preserving Functional of W;
cluster FormFunctional(f,g) -> non constant;
end;

definition
let K be Field;
let V,W be non trivial VectSp of K;
cluster non trivial non constant
additiveFAF homogeneousFAF additiveSAF homogeneousSAF Form of V,W;
end;

definition
let K be Abelian add-associative right_zeroed (non empty LoopStr);
let V,W be non empty VectSpStr over K;
let f,g be additiveSAF Form of V,W;
cluster f+g -> additiveSAF;
end;

definition
let K be Abelian add-associative right_zeroed (non empty LoopStr);
let V,W be non empty VectSpStr over K;
let f,g be additiveFAF Form of V,W;
cluster f+g -> additiveFAF;
end;

definition
let K be right-distributive right_zeroed (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
let f be additiveSAF Form of V,W;
let a be Element of K;
cluster a*f -> additiveSAF;
end;

definition
let K be right-distributive right_zeroed (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
let f be additiveFAF Form of V,W;
let a be Element of K;
cluster a*f -> additiveFAF;
end;

definition
let K be Abelian add-associative right_zeroed right_complementable
(non empty LoopStr);
let V,W be non empty VectSpStr over K;
let f be additiveSAF Form of V,W;
cluster -f -> additiveSAF;
end;

definition
let K be Abelian add-associative right_zeroed right_complementable
(non empty LoopStr);
let V,W be non empty VectSpStr over K;
let f be additiveFAF Form of V,W;
cluster -f -> additiveFAF;
end;

definition
let K be Abelian add-associative right_zeroed right_complementable
(non empty LoopStr);
let V,W be non empty VectSpStr over K;
let f,g be additiveSAF Form of V,W;
cluster f-g -> additiveSAF;
end;

definition
let K be Abelian add-associative right_zeroed right_complementable
(non empty LoopStr);
let V,W be non empty VectSpStr over K;
let f,g be additiveFAF Form of V,W;
cluster f-g -> additiveFAF;
end;

definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
let f,g be homogeneousSAF Form of V,W;
cluster f+g -> homogeneousSAF;
end;

definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
let f,g be homogeneousFAF Form of V,W;
cluster f+g -> homogeneousFAF;
end;

definition
let K be add-associative right_zeroed right_complementable
associative commutative right-distributive (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
let f be homogeneousSAF Form of V,W;
let a be Element of K;
cluster a*f -> homogeneousSAF;
end;

definition
let K be add-associative right_zeroed right_complementable
associative commutative right-distributive (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
let f be homogeneousFAF Form of V,W;
let a be Element of K;
cluster a*f -> homogeneousFAF;
end;

definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
let f be homogeneousSAF Form of V,W;
cluster -f -> homogeneousSAF;
end;

definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
let f be homogeneousFAF Form of V,W;
cluster -f -> homogeneousFAF;
end;

definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
let f,g be homogeneousSAF Form of V,W;
cluster f-g -> homogeneousSAF;
end;

definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V,W be non empty VectSpStr over K;
let f,g be homogeneousFAF Form of V,W;
cluster f-g -> homogeneousFAF;
end;

theorem :: BILINEAR:27
for K be non empty LoopStr
for V,W be non empty VectSpStr over K
for v,u be Vector of V, w be Vector of W, f be Form of V,W
st f is additiveSAF holds f.[v+u,w] = f.[v,w] + f.[u,w];

theorem :: BILINEAR:28
for K be non empty LoopStr
for V,W be non empty VectSpStr over K
for v be Vector of V, u,w be Vector of W, f be Form of V,W
st f is additiveFAF holds f.[v,u+w] = f.[v,u] + f.[v,w];

theorem :: BILINEAR:29
for K be right_zeroed (non empty LoopStr)
for V,W be non empty VectSpStr over K
for v,u be Vector of V, w,t be Vector of W,
f be additiveSAF additiveFAF Form of V,W holds
f.[v+u,w+t] = f.[v,w] + f.[v,t] + (f.[u,w] + f.[u,t]);

theorem :: BILINEAR:30
for K be add-associative right_zeroed right_complementable
(non empty doubleLoopStr)
for V,W be right_zeroed (non empty VectSpStr over K)
for f be additiveFAF Form of V,W, v be Vector of V holds f.[v,0.W] = 0.K;

theorem :: BILINEAR:31
for K be add-associative right_zeroed right_complementable
(non empty doubleLoopStr)
for V,W be right_zeroed (non empty VectSpStr over K)
for f be additiveSAF Form of V,W, w be Vector of W holds f.[0.V,w] = 0.K;

theorem :: BILINEAR:32
for K be non empty HGrStr
for V,W be non empty VectSpStr over K
for v be Vector of V, w be Vector of W, a be Element of K
for f be Form of V,W st f is homogeneousSAF holds f.[a*v,w] = a*f.[v,w];

theorem :: BILINEAR:33
for K be non empty HGrStr
for V,W be non empty VectSpStr over K
for v be Vector of V, w be Vector of W, a be Element of K
for f be Form of V,W st f is homogeneousFAF holds f.[v,a*w] = a*f.[v,w];

theorem :: BILINEAR:34
for K be add-associative right_zeroed right_complementable
associative left_unital distributive (non empty doubleLoopStr)
for V,W be add-associative right_zeroed right_complementable VectSp-like
(non empty VectSpStr over K)
for f be homogeneousSAF Form of V,W, w be Vector of W holds f.[0.V,w] = 0.K;

theorem :: BILINEAR:35
for K be add-associative right_zeroed right_complementable
associative left_unital distributive (non empty doubleLoopStr)
for V,W be add-associative right_zeroed right_complementable
VectSp-like (non empty VectSpStr over K)
for f be homogeneousFAF Form of V,W, v be Vector of V holds f.[v,0.W] = 0.K;

theorem :: BILINEAR:36
for K be add-associative right_zeroed right_complementable Abelian
associative left_unital distributive (non empty doubleLoopStr)
for V,W be VectSp of K
for v,u be Vector of V, w be Vector of W,
f be additiveSAF homogeneousSAF Form of V,W holds
f.[v-u,w] = f.[v,w] - f.[u,w];

theorem :: BILINEAR:37
for K be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr)
for V,W be VectSp of K
for v be Vector of V, w,t be Vector of W,
f be additiveFAF homogeneousFAF Form of V,W holds
f.[v,w-t] = f.[v,w] - f.[v,t];

theorem :: BILINEAR:38
for K be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr)
for V,W be VectSp of K
for v,u be Vector of V, w,t be Vector of W, f be bilinear-Form of V,W
holds f.[v-u,w-t] = f.[v,w] - f.[v,t] -(f.[u,w] - f.[u,t]);

theorem :: BILINEAR:39
for K be add-associative right_zeroed right_complementable
associative left_unital distributive (non empty doubleLoopStr)
for V,W be add-associative right_zeroed right_complementable VectSp-like
(non empty VectSpStr over K)
for v,u be Vector of V, w,t be Vector of W, a,b be Element of K
for f be bilinear-Form of V,W
holds
f.[v+a*u,w+b*t] = f.[v,w] + b*f.[v,t] + (a*f.[u,w] + a*(b*f.[u,t]));

theorem :: BILINEAR:40
for K be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr)
for V,W be VectSp of K
for v,u be Vector of V, w,t be Vector of W, a,b be Element of K
for f be bilinear-Form of V,W
holds f.[v-a*u,w-b*t] = f.[v,w] - b*f.[v,t] - (a*f.[u,w] - a*(b*f.[u,t]));

theorem :: BILINEAR:41
for K be add-associative right_zeroed right_complementable
(non empty doubleLoopStr), V,W be right_zeroed (non empty VectSpStr over K),
f be Form of V,W
st f is additiveFAF or f is additiveSAF holds
f is constant iff for v be Vector of V, w be Vector of W holds f.[v,w]=0.K;

begin
:: Left and Right Kernel of Form. "Diagonal" Kernel of Form

definition
let K be ZeroStr;
let V,W be non empty VectSpStr over K;
let f be Form of V,W;
func leftker f ->
Subset of V equals
:: BILINEAR:def 16
{v where v is Vector of V : for w be Vector of W holds f.[v,w] = 0.K};
end;

definition
let K be ZeroStr;
let V,W be non empty VectSpStr over K;
let f be Form of V,W;
func rightker f ->
Subset of W equals
:: BILINEAR:def 17
{w where w is Vector of W : for v be Vector of V holds f.[v,w] = 0.K};
end;

definition
let K be ZeroStr;
let V be non empty VectSpStr over K;
let f be Form of V,V;
func diagker f -> Subset of V equals
:: BILINEAR:def 18
{v where v is Vector of V : f.[v,v] = 0.K};
end;

definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V be right_zeroed (non empty VectSpStr over K);
let W be non empty VectSpStr over K;
let f be additiveSAF Form of V,W;
cluster leftker f -> non empty;
end;

definition
let K be add-associative right_zeroed right_complementable
associative left_unital distributive (non empty doubleLoopStr);
let V be add-associative right_zeroed right_complementable
VectSp-like (non empty VectSpStr over K);
let W be non empty VectSpStr over K;
let f be homogeneousSAF Form of V,W;
cluster leftker f -> non empty;
end;

definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V be non empty VectSpStr over K;
let W be right_zeroed (non empty VectSpStr over K);
let f be additiveFAF Form of V,W;
cluster rightker f -> non empty;
end;

definition
let K be add-associative right_zeroed right_complementable
associative left_unital distributive (non empty doubleLoopStr);
let V be non empty VectSpStr over K;
let W be add-associative right_zeroed right_complementable
VectSp-like (non empty VectSpStr over K);
let f be homogeneousFAF Form of V,W;
cluster rightker f -> non empty;
end;

definition
let K be add-associative right_zeroed right_complementable
(non empty doubleLoopStr);
let V be right_zeroed (non empty VectSpStr over K);
let f be additiveFAF Form of V,V;
cluster diagker f -> non empty;
end;

definition
let K be add-associative right_zeroed right_complementable
(non empty doubleLoopStr);
let V be right_zeroed (non empty VectSpStr over K);
let f be additiveSAF Form of V,V;
cluster diagker f -> non empty;
end;

definition
let K be add-associative right_zeroed right_complementable
associative left_unital distributive (non empty doubleLoopStr);
let V be add-associative right_zeroed right_complementable
VectSp-like (non empty VectSpStr over K);
let f be homogeneousFAF Form of V,V;
cluster diagker f -> non empty;
end;

definition
let K be add-associative right_zeroed right_complementable
associative left_unital distributive (non empty doubleLoopStr);
let V be add-associative right_zeroed right_complementable
VectSp-like (non empty VectSpStr over K);
let f be homogeneousSAF Form of V,V;
cluster diagker f -> non empty;
end;

theorem :: BILINEAR:42
for K be ZeroStr, V be non empty VectSpStr over K
for f be Form of V,V holds
leftker f c= diagker f & rightker f c= diagker f;

theorem :: BILINEAR:43
for K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr)
for V,W be non empty VectSpStr over K
for f be additiveSAF homogeneousSAF Form of V,W
holds leftker f is lineary-closed;

theorem :: BILINEAR:44
for K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr)
for V,W be non empty VectSpStr over K
for f be additiveFAF homogeneousFAF Form of V,W
holds rightker f is lineary-closed;

definition
let K be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr);
let V be VectSp of K, W be non empty VectSpStr over K;
let f be additiveSAF homogeneousSAF Form of V,W;
func LKer f -> strict non empty Subspace of V means
:: BILINEAR:def 19
the carrier of it = leftker f;
end;

definition
let K be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr);
let V be non empty VectSpStr over K, W be VectSp of K;
let f be additiveFAF homogeneousFAF Form of V,W;
func RKer f -> strict non empty Subspace of W means
:: BILINEAR:def 20
the carrier of it = rightker f;
end;

definition
let K be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr);
let V be VectSp of K, W be non empty VectSpStr over K;
let f be additiveSAF homogeneousSAF Form of V,W;
func LQForm(f) -> additiveSAF homogeneousSAF Form of VectQuot(V,LKer f),W means
:: BILINEAR:def 21

for A be Vector of VectQuot(V,LKer(f)), w be Vector of W, v be Vector of V
st A = v + LKer(f) holds it.[A,w] = f.[v,w];
end;

definition
let K be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr);
let V be non empty VectSpStr over K, W be VectSp of K;
let f be additiveFAF homogeneousFAF Form of V,W;
func RQForm(f) -> additiveFAF homogeneousFAF Form of V,VectQuot(W,RKer f) means
:: BILINEAR:def 22

for A be Vector of VectQuot(W,RKer(f)), v be Vector of V, w be Vector of W
st A = w + RKer(f) holds it.[v,A] = f.[v,w];
end;

definition
let K be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr);
let V,W be VectSp of K;
let f be bilinear-Form of V,W;
cluster LQForm(f) -> additiveFAF homogeneousFAF;
cluster RQForm(f) -> additiveSAF homogeneousSAF;
end;

definition
let K be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr);
let V,W be VectSp of K;
let f be bilinear-Form of V,W;
func QForm(f) -> bilinear-Form of VectQuot(V,LKer(f)),VectQuot(W,RKer(f)) means
:: BILINEAR:def 23

for A be Vector of VectQuot(V,LKer f), B be Vector of VectQuot(W, RKer(f))
for v be Vector of V, w be Vector of W
st A = v + LKer f & B = w + RKer f holds it.[A,B]= f.[v,w];
end;

theorem :: BILINEAR:45
for K be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr)
for V be VectSp of K, W be non empty VectSpStr over K
for f be additiveSAF homogeneousSAF Form of V,W holds
rightker f = rightker (LQForm f);

theorem :: BILINEAR:46
for K be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr)
for V be non empty VectSpStr over K, W be VectSp of K
for f be additiveFAF homogeneousFAF Form of V,W holds
leftker f = leftker (RQForm f);

theorem :: BILINEAR:47
for K be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr)
for V,W be VectSp of K, f be bilinear-Form of V,W holds
RKer f = RKer (LQForm f);

theorem :: BILINEAR:48
for K be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr)
for V,W be VectSp of K, f be bilinear-Form of V,W holds
LKer f = LKer (RQForm f);

theorem :: BILINEAR:49
for K be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr)
for V,W be VectSp of K, f be bilinear-Form of V,W
holds QForm(f) = RQForm(LQForm(f)) & QForm(f) = LQForm(RQForm(f));

theorem :: BILINEAR:50
for K be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr)
for V,W be VectSp of K, f be 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)));

theorem :: BILINEAR:51
for K be add-associative right_zeroed right_complementable
distributive (non empty doubleLoopStr)
for V,W be non empty VectSpStr over K
for f be Functional of V, g be Functional of W
holds ker f c= leftker FormFunctional(f,g);

theorem :: BILINEAR:52
for K be add-associative right_zeroed right_complementable associative
commutative left_unital Field-like distributive (non empty doubleLoopStr)
for V, W be non empty VectSpStr over K
for f be Functional of V, g be Functional of W
st g <> 0Functional(W) holds leftker FormFunctional(f,g) = ker f;

theorem :: BILINEAR:53
for K be add-associative right_zeroed right_complementable distributive
(non empty doubleLoopStr)
for V,W be non empty VectSpStr over K
for f be Functional of V, g be Functional of W
holds ker g c= rightker FormFunctional(f,g);

theorem :: BILINEAR:54
for K be add-associative right_zeroed right_complementable associative
commutative left_unital Field-like distributive (non empty doubleLoopStr)
for V, W be non empty VectSpStr over K
for f be Functional of V, g be Functional of W
st f <> 0Functional(V) holds rightker FormFunctional(f,g) = ker g;

theorem :: BILINEAR:55
for K be add-associative right_zeroed right_complementable commutative Abelian
associative left_unital distributive Field-like (non empty doubleLoopStr)
for V be VectSp of K, W be non empty VectSpStr over K
for f be linear-Functional of V, g be Functional of W
st g <> 0Functional(W) holds
LKer FormFunctional(f,g) = Ker f &
LQForm(FormFunctional(f,g)) = FormFunctional(CQFunctional(f),g);

theorem :: BILINEAR:56
for K be add-associative right_zeroed right_complementable commutative Abelian
associative left_unital distributive Field-like (non empty doubleLoopStr)
for V be non empty VectSpStr over K, W be VectSp of K
for f be Functional of V, g be linear-Functional of W
st f <> 0Functional(V) holds
RKer FormFunctional(f,g) = Ker g &
RQForm(FormFunctional(f,g)) = FormFunctional(f,CQFunctional(g));

theorem :: BILINEAR:57
for K be Field, V,W be non trivial VectSp of K
for f be non constant linear-Functional of V,
g be non constant linear-Functional of W holds
QForm(FormFunctional(f,g)) = FormFunctional(CQFunctional(f),CQFunctional(g));

definition
let K be ZeroStr;
let V,W be non empty VectSpStr over K;
let f be Form of V,W;
attr f is degenerated-on-left means
:: BILINEAR:def 24
leftker f <> {0.V};
attr f is degenerated-on-right means
:: BILINEAR:def 25
rightker f <> {0.W};
end;

definition
let K be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr);
let V be VectSp of K, W be right_zeroed (non empty VectSpStr over K);
let f be additiveSAF homogeneousSAF Form of V,W;
cluster LQForm(f) -> non degenerated-on-left;
end;

definition
let K be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr);
let V be right_zeroed (non empty VectSpStr over K), W be VectSp of K;
let f be additiveFAF homogeneousFAF Form of V,W;
cluster RQForm(f) -> non degenerated-on-right;
end;

definition
let K be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr);
let V,W be VectSp of K;
let f be bilinear-Form of V,W;
cluster QForm(f) -> non degenerated-on-left non degenerated-on-right;
end;

definition
let K be add-associative right_zeroed right_complementable
Abelian associative left_unital distributive (non empty doubleLoopStr);
let V,W be VectSp of K;
let f be bilinear-Form of V,W;
cluster RQForm(LQForm(f)) -> non degenerated-on-left non degenerated-on-right;
cluster LQForm(RQForm(f)) -> non degenerated-on-left non degenerated-on-right;
end;

definition
let K be Field;
let V,W be non trivial VectSp of K;
let f be non constant bilinear-Form of V,W;
cluster QForm(f) -> non constant;
end;

begin
:: Bilinear Symmetric and Alternating Forms

definition
let K be 1-sorted;
let V be VectSpStr over K;
let f be Form of V,V;
attr f is symmetric means
:: BILINEAR:def 26
for v,w be Vector of V holds f.[v,w] = f.[w,v];
end;

definition
let K be ZeroStr;
let V be VectSpStr over K;
let f be Form of V,V;
attr f is alternating means
:: BILINEAR:def 27
for v be Vector of V holds f.[v,v] = 0.K;
end;

definition
let K be non empty ZeroStr;
let V be non empty VectSpStr over K;
cluster NulForm(V,V) -> symmetric;
cluster NulForm(V,V) -> alternating;
end;

definition
let K be non empty ZeroStr;
let V be non empty VectSpStr over K;
cluster symmetric Form of V,V;
cluster alternating Form of V,V;
end;

definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V be non empty VectSpStr over K;
cluster symmetric
additiveFAF homogeneousFAF additiveSAF homogeneousSAF Form of V,V;
cluster alternating
additiveFAF homogeneousFAF additiveSAF homogeneousSAF Form of V,V;
end;

definition
let K be Field;
let V be non trivial VectSp of K;
cluster symmetric non trivial non constant
additiveFAF homogeneousFAF additiveSAF homogeneousSAF Form of V,V;
end;

definition
let K be add-associative right_zeroed right_complementable
(non empty LoopStr);
let V be non empty VectSpStr over K;
cluster alternating additiveFAF additiveSAF Form of V,V;
end;

definition
let K be non empty LoopStr;
let V be non empty VectSpStr over K;
let f,g be symmetric Form of V,V;
cluster f+g -> symmetric;
end;

definition
let K be non empty doubleLoopStr;
let V be non empty VectSpStr over K;
let f be symmetric Form of V,V;
let a be Element of K;
cluster a*f -> symmetric;
end;

definition
let K be non empty LoopStr;
let V be non empty VectSpStr over K;
let f be symmetric Form of V,V;
cluster -f -> symmetric;
end;

definition
let K be non empty LoopStr;
let V be non empty VectSpStr over K;
let f,g be symmetric Form of V,V;
cluster f-g -> symmetric;
end;

definition
let K be right_zeroed (non empty LoopStr);
let V be non empty VectSpStr over K;
let f,g be alternating Form of V,V;
cluster f+g -> alternating;
end;

definition
let K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr);
let V be non empty VectSpStr over K;
let f be alternating Form of V,V;
let a be Scalar of K;
cluster a*f -> alternating;
end;

definition
let K be add-associative right_zeroed right_complementable
(non empty LoopStr);
let V be non empty VectSpStr over K;
let f be alternating Form of V,V;
cluster -f -> alternating;
end;

definition
let K be add-associative right_zeroed right_complementable
(non empty LoopStr);
let V be non empty VectSpStr over K;
let f,g be alternating Form of V,V;
cluster f-g -> alternating;
end;

theorem :: BILINEAR:58
for K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr)
for V be non empty VectSpStr over K
for f be symmetric bilinear-Form of V,V holds
leftker f = rightker f;

theorem :: BILINEAR:59
for K be add-associative right_zeroed right_complementable
(non empty LoopStr)
for V be non empty VectSpStr over K
for f be alternating additiveSAF additiveFAF Form of V,V
for v,w be Vector of V holds f.[v,w]=-f.[w,v];

definition
let K be Fanoian Field;
let V be non empty VectSpStr over K;
let f be additiveSAF additiveFAF Form of V,V;
redefine attr f is alternating means
:: BILINEAR:def 28
for v,w be Vector of V holds f.[v,w] = -f.[w,v];
end;

theorem :: BILINEAR:60
for K be add-associative right_zeroed right_complementable
right-distributive (non empty doubleLoopStr)
for V be non empty VectSpStr over K
for f be alternating bilinear-Form of V,V holds
leftker f = rightker f;
```