The abstract of the Mizar article:

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;
cluster additiveFAF additiveSAF 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;
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;