:: Bilinear Functionals in Vector Spaces
:: by Jaros{\l}aw Kotowicz
::
:: Received November 5, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


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;
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 1
[: the carrier of V, the carrier of W:] --> (0. K);
coherence
 [: the carrier of V, the carrier of W:] --> (0. K) is Form of V,W ;
end;

:: deftheorem  defines NulForm BILINEAR:def_1_:_
 for K being non empty ZeroStr
for V, W being VectSpStr over K holds NulForm (V,W) = [: the carrier of V, the carrier of W:] --> (0. K);

definition
let K be non empty addLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be Form of V,W;
funcf + g ->  Form of V,W means :Def2: :: BILINEAR:def 2
 for v being Vector of V
for w being Vector of W holds it . (v,w) = (f . (v,w)) + (g . (v,w));
existence
 ex b1 being Form of V,W st
for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . (v,w)) + (g . (v,w))
proofend;
uniqueness
 for b1, b2 being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . (v,w)) + (g . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = (f . (v,w)) + (g . (v,w)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines + BILINEAR:def_2_:_
 for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f, g, b6 being Form of V,W holds
( b6 = f + g iff for v being Vector of V
for w being Vector of W holds b6 . (v,w) = (f . (v,w)) + (g . (v,w)) );

definition
let K be non empty multMagma ;
let V, W be non empty VectSpStr over K;
let f be Form of V,W;
let a be Element of K;
funca * f ->  Form of V,W means :Def3: :: BILINEAR:def 3
 for v being Vector of V
for w being Vector of W holds it . (v,w) = a * (f . (v,w));
existence
 ex b1 being Form of V,W st
for v being Vector of V
for w being Vector of W holds b1 . (v,w) = a * (f . (v,w))
proofend;
uniqueness
 for b1, b2 being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . (v,w) = a * (f . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = a * (f . (v,w)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines * BILINEAR:def_3_:_
 for K being non empty multMagma
for V, W being non empty VectSpStr over K
for f being Form of V,W
for a being Element of K
for b6 being Form of V,W holds
( b6 = a * f iff for v being Vector of V
for w being Vector of W holds b6 . (v,w) = a * (f . (v,w)) );

definition
let K be non empty addLoopStr ;
let V, W be non empty VectSpStr over K;
let f be Form of V,W;
func - f ->  Form of V,W means :Def4: :: BILINEAR:def 4
 for v being Vector of V
for w being Vector of W holds it . (v,w) = - (f . (v,w));
existence
 ex b1 being Form of V,W st
for v being Vector of V
for w being Vector of W holds b1 . (v,w) = - (f . (v,w))
proofend;
uniqueness
 for b1, b2 being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . (v,w) = - (f . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = - (f . (v,w)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines - BILINEAR:def_4_:_
 for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f, b5 being Form of V,W holds
( b5 = - f iff for v being Vector of V
for w being Vector of W holds b5 . (v,w) = - (f . (v,w)) );

definition
let K be non empty right_complementable add-associative right_zeroed left-distributive left_unital doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be Form of V,W;
redefine func - f equals :: BILINEAR:def 5
(- (1. K)) * f;
compatibility
 for b1 being Form of V,W holds
( b1 = - f iff b1 = (- (1. K)) * f )
proofend;
end;

:: deftheorem  defines - BILINEAR:def_5_:_
 for K being non empty right_complementable add-associative right_zeroed left-distributive left_unital doubleLoopStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds - f = (- (1. K)) * f;

definition
let K be non empty addLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be Form of V,W;
funcf - g ->  Form of V,W equals :: BILINEAR:def 6
f + (- g);
correctness
coherence
f + (- g) is Form of V,W;
;
end;

:: deftheorem  defines - BILINEAR:def_6_:_
 for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f, g being Form of V,W holds f - g = f + (- g);

definition
let K be non empty addLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be Form of V,W;
redefine func f - g means :Def7: :: BILINEAR:def 7
 for v being Vector of V
for w being Vector of W holds it . (v,w) = (f . (v,w)) - (g . (v,w));
compatibility
 for b1 being Form of V,W holds
( b1 = f - g iff for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . (v,w)) - (g . (v,w)) )
proofend;
end;

:: deftheorem Def7 defines - BILINEAR:def_7_:_
 for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f, g, b6 being Form of V,W holds
( b6 = f - g iff for v being Vector of V
for w being Vector of W holds b6 . (v,w) = (f . (v,w)) - (g . (v,w)) );

definition
let K be non empty Abelian addLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be Form of V,W;
:: original:+
redefine funcf + g ->  Form of V,W;
commutativity
 for f, g being Form of V,W holds f + g = g + f
proofend;
end;

theorem :: BILINEAR:1
for K being non empty right_zeroed addLoopStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds f + (NulForm (V,W)) = f
proofend;

theorem :: BILINEAR:2
for K being non empty add-associative addLoopStr
for V, W being non empty VectSpStr over K
for f, g, h being Form of V,W holds (f + g) + h = f + (g + h)
proofend;

theorem :: BILINEAR:3
for K being non empty right_complementable add-associative right_zeroed addLoopStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds f - f = NulForm (V,W)
proofend;

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

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

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

theorem :: BILINEAR:7
for K being non empty left_unital doubleLoopStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds (1. K) * f = f
proofend;

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;
let v be Vector of V;
func FunctionalFAF (f,v) ->  Functional of W equals :: BILINEAR:def 8
(curry f) . v;
correctness
coherence
(curry f) . v is Functional of W;
;
end;

:: deftheorem  defines FunctionalFAF BILINEAR:def_8_:_
 for K being non empty 1-sorted
for V, W being non empty VectSpStr over K
for f being Form of V,W
for v being Vector of V holds FunctionalFAF (f,v) = (curry f) . v;

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

:: deftheorem  defines FunctionalSAF BILINEAR:def_9_:_
 for K being non empty 1-sorted
for V, W being non empty VectSpStr over K
for f being Form of V,W
for w being Vector of W holds FunctionalSAF (f,w) = (curry' f) . w;

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

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

theorem Th10: :: BILINEAR:10
for K being non empty ZeroStr
for V, W being non empty VectSpStr over K
for v being Vector of V holds FunctionalFAF ((NulForm (V,W)),v) = 0Functional W
proofend;

theorem Th11: :: BILINEAR:11
for K being non empty ZeroStr
for V, W being non empty VectSpStr over K
for w being Vector of W holds FunctionalSAF ((NulForm (V,W)),w) = 0Functional V
proofend;

theorem Th12: :: BILINEAR:12
for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f, g being Form of V,W
for w being Vector of W holds FunctionalSAF ((f + g),w) = (FunctionalSAF (f,w)) + (FunctionalSAF (g,w))
proofend;

theorem Th13: :: BILINEAR:13
for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f, g being Form of V,W
for v being Vector of V holds FunctionalFAF ((f + g),v) = (FunctionalFAF (f,v)) + (FunctionalFAF (g,v))
proofend;

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

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

theorem Th16: :: BILINEAR:16
for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f being Form of V,W
for w being Vector of W holds FunctionalSAF ((- f),w) = - (FunctionalSAF (f,w))
proofend;

theorem Th17: :: BILINEAR:17
for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f being Form of V,W
for v being Vector of V holds FunctionalFAF ((- f),v) = - (FunctionalFAF (f,v))
proofend;

theorem :: BILINEAR:18
for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f, g being Form of V,W
for w being Vector of W holds FunctionalSAF ((f - g),w) = (FunctionalSAF (f,w)) - (FunctionalSAF (g,w))
proofend;

theorem :: BILINEAR:19
for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f, g being Form of V,W
for v being Vector of V holds FunctionalFAF ((f - g),v) = (FunctionalFAF (f,v)) - (FunctionalFAF (g,v))
proofend;

begin

:: Two Form generated by Functionals.
definition
let K be non empty multMagma ;
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 :Def10: :: BILINEAR:def 10
 for v being Vector of V
for w being Vector of W holds it . (v,w) = (f . v) * (g . w);
existence
 ex b1 being Form of V,W st
for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . v) * (g . w)
proofend;
uniqueness
 for b1, b2 being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . v) * (g . w) ) & ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = (f . v) * (g . w) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines FormFunctional BILINEAR:def_10_:_
 for K being non empty multMagma
for V, W being non empty VectSpStr over K
for f being Functional of V
for g being Functional of W
for b6 being Form of V,W holds
( b6 = FormFunctional (f,g) iff for v being Vector of V
for w being Vector of W holds b6 . (v,w) = (f . v) * (g . w) );

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

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

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

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

theorem Th24: :: BILINEAR:24
for K being non empty multMagma
for V, W being non empty VectSpStr over K
for f being Functional of V
for g being Functional of W
for v being Vector of V holds FunctionalFAF ((FormFunctional (f,g)),v) = (f . v) * g
proofend;

theorem Th25: :: BILINEAR:25
for K being non empty commutative multMagma
for V, W being non empty VectSpStr over K
for f being Functional of V
for g being Functional of W
for w being Vector of W holds FunctionalSAF ((FormFunctional (f,g)),w) = (g . w) * f
proofend;

begin

::Bilinear Forms and Their Properties
definition
let K be non empty addLoopStr ;
let V, W be non empty VectSpStr over K;
let f be Form of V,W;
attrf is additiveFAF  means :Def11: :: BILINEAR:def 11
 for v being Vector of V holds FunctionalFAF (f,v) is additive ;
attrf is additiveSAF  means :Def12: :: BILINEAR:def 12
 for w being Vector of W holds FunctionalSAF (f,w) is additive ;
end;

:: deftheorem Def11 defines additiveFAF BILINEAR:def_11_:_
 for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds
( f is additiveFAF iff for v being Vector of V holds FunctionalFAF (f,v) is additive );

:: deftheorem Def12 defines additiveSAF BILINEAR:def_12_:_
 for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds
( f is additiveSAF iff for w being Vector of W holds FunctionalSAF (f,w) is additive );

definition
let K be non empty multMagma ;
let V, W be non empty VectSpStr over K;
let f be Form of V,W;
attrf is homogeneousFAF  means :Def13: :: BILINEAR:def 13
 for v being Vector of V holds FunctionalFAF (f,v) is homogeneous ;
attrf is homogeneousSAF  means :Def14: :: BILINEAR:def 14
 for w being Vector of W holds FunctionalSAF (f,w) is homogeneous ;
end;

:: deftheorem Def13 defines homogeneousFAF BILINEAR:def_13_:_
 for K being non empty multMagma
for V, W being non empty VectSpStr over K
for f being Form of V,W holds
( f is homogeneousFAF iff for v being Vector of V holds FunctionalFAF (f,v) is homogeneous );

:: deftheorem Def14 defines homogeneousSAF BILINEAR:def_14_:_
 for K being non empty multMagma
for V, W being non empty VectSpStr over K
for f being Form of V,W holds
( f is homogeneousSAF iff for w being Vector of W holds FunctionalSAF (f,w) is homogeneous );

registration
let K be non empty right_zeroed addLoopStr ;
let V, W be non empty VectSpStr over K;
cluster NulForm (V,W) ->  additiveFAF ;
coherence
 NulForm (V,W) is additiveFAF
proofend;
cluster NulForm (V,W) ->  additiveSAF ;
coherence
 NulForm (V,W) is additiveSAF
proofend;
end;

registration
let K be non empty right_zeroed addLoopStr ;
let V, W be non empty VectSpStr over K;
cluster non empty Relation-like [: the carrier of V, the carrier of W:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of W:]) V21([: the carrier of V, the carrier of W:], the carrier of K) additiveFAF additiveSAF for Element of bool [:[: the carrier of V, the carrier of W:], the carrier of K:];
existence
 ex b1 being Form of V,W st
( b1 is additiveFAF & b1 is additiveSAF )
proofend;
end;

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

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
cluster non empty Relation-like [: the carrier of V, the carrier of W:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of W:]) V21([: the carrier of V, the carrier of W:], the carrier of K) additiveFAF additiveSAF homogeneousFAF homogeneousSAF for Element of bool [:[: the carrier of V, the carrier of W:], the carrier of K:];
existence
 ex b1 being Form of V,W st
( b1 is additiveFAF & b1 is homogeneousFAF & b1 is additiveSAF & b1 is homogeneousSAF )
proofend;
end;

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

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

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

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

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

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

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

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

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

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

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

registration
let K be Field;
let V, W be non trivial VectSp of K;
let f be V17() 0-preserving Functional of V;
let g be V17() 0-preserving Functional of W;
cluster FormFunctional (f,g) ->  non constant ;
coherence
 not FormFunctional (f,g) is constant
proofend;
end;

registration
let K be Field;
let V, W be non trivial VectSp of K;
cluster non empty non trivial Relation-like [: the carrier of V, the carrier of W:] -defined the carrier of K -valued Function-like non constant V20([: the carrier of V, the carrier of W:]) V21([: the carrier of V, the carrier of W:], the carrier of K) additiveFAF additiveSAF homogeneousFAF homogeneousSAF for Element of bool [:[: the carrier of V, the carrier of W:], the carrier of K:];
existence
 ex b1 being Form of V,W st
( not b1 is trivial & not b1 is constant & b1 is additiveFAF & b1 is homogeneousFAF & b1 is additiveSAF & b1 is homogeneousSAF )
proofend;
end;

registration
let K be non empty Abelian add-associative right_zeroed addLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be additiveSAF Form of V,W;
clusterf + g ->  additiveSAF ;
correctness
coherence
f + g is additiveSAF ;
proofend;
end;

registration
let K be non empty Abelian add-associative right_zeroed addLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be additiveFAF Form of V,W;
clusterf + g ->  additiveFAF ;
correctness
coherence
f + g is additiveFAF ;
proofend;
end;

registration
let K be non empty right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be additiveSAF Form of V,W;
let a be Element of K;
clustera * f ->  additiveSAF ;
correctness
coherence
a * f is additiveSAF ;
proofend;
end;

registration
let K be non empty right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be additiveFAF Form of V,W;
let a be Element of K;
clustera * f ->  additiveFAF ;
correctness
coherence
a * f is additiveFAF ;
proofend;
end;

registration
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;
let V, W be non empty VectSpStr over K;
let f be additiveSAF Form of V,W;
cluster - f ->  additiveSAF ;
correctness
coherence
- f is additiveSAF ;
proofend;
end;

registration
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;
let V, W be non empty VectSpStr over K;
let f be additiveFAF Form of V,W;
cluster - f ->  additiveFAF ;
correctness
coherence
- f is additiveFAF ;
proofend;
end;

registration
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be additiveSAF Form of V,W;
clusterf - g ->  additiveSAF ;
correctness
coherence
f - g is additiveSAF ;
;
end;

registration
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be additiveFAF Form of V,W;
clusterf - g ->  additiveFAF ;
correctness
coherence
f - g is additiveFAF ;
;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be homogeneousSAF Form of V,W;
clusterf + g ->  homogeneousSAF ;
correctness
coherence
f + g is homogeneousSAF ;
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be homogeneousFAF Form of V,W;
clusterf + g ->  homogeneousFAF ;
correctness
coherence
f + g is homogeneousFAF ;
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed associative commutative right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be homogeneousSAF Form of V,W;
let a be Element of K;
clustera * f ->  homogeneousSAF ;
correctness
coherence
a * f is homogeneousSAF ;
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed associative commutative right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be homogeneousFAF Form of V,W;
let a be Element of K;
clustera * f ->  homogeneousFAF ;
correctness
coherence
a * f is homogeneousFAF ;
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be homogeneousSAF Form of V,W;
cluster - f ->  homogeneousSAF ;
correctness
coherence
- f is homogeneousSAF ;
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be homogeneousFAF Form of V,W;
cluster - f ->  homogeneousFAF ;
correctness
coherence
- f is homogeneousFAF ;
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be homogeneousSAF Form of V,W;
clusterf - g ->  homogeneousSAF ;
correctness
coherence
f - g is homogeneousSAF ;
;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be homogeneousFAF Form of V,W;
clusterf - g ->  homogeneousFAF ;
correctness
coherence
f - g is homogeneousFAF ;
;
end;

theorem Th26: :: BILINEAR:26
for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for v, u being Vector of V
for w being Vector of W
for f being Form of V,W st f is additiveSAF holds
f . ((v + u),w) = (f . (v,w)) + (f . (u,w))
proofend;

theorem Th27: :: BILINEAR:27
for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for v being Vector of V
for u, w being Vector of W
for f being Form of V,W st f is additiveFAF holds
f . (v,(u + w)) = (f . (v,u)) + (f . (v,w))
proofend;

theorem Th28: :: BILINEAR:28
for K being non empty right_zeroed addLoopStr
for V, W being non empty VectSpStr over K
for v, u being Vector of V
for w, t being Vector of W
for f being additiveFAF additiveSAF Form of V,W holds f . ((v + u),(w + t)) = ((f . (v,w)) + (f . (v,t))) + ((f . (u,w)) + (f . (u,t)))
proofend;

theorem Th29: :: BILINEAR:29
for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for V, W being non empty right_zeroed VectSpStr over K
for f being additiveFAF Form of V,W
for v being Vector of V holds f . (v,(0. W)) = 0. K
proofend;

theorem Th30: :: BILINEAR:30
for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for V, W being non empty right_zeroed VectSpStr over K
for f being additiveSAF Form of V,W
for w being Vector of W holds f . ((0. V),w) = 0. K
proofend;

theorem Th31: :: BILINEAR:31
for K being non empty multMagma
for V, W being non empty VectSpStr over K
for v being Vector of V
for w being Vector of W
for a being Element of K
for f being Form of V,W st f is homogeneousSAF holds
f . ((a * v),w) = a * (f . (v,w))
proofend;

theorem Th32: :: BILINEAR:32
for K being non empty multMagma
for V, W being non empty VectSpStr over K
for v being Vector of V
for w being Vector of W
for a being Element of K
for f being Form of V,W st f is homogeneousFAF holds
f . (v,(a * w)) = a * (f . (v,w))
proofend;

theorem Th33: :: BILINEAR:33
for K being non empty right_complementable add-associative right_zeroed associative distributive left_unital doubleLoopStr
for V, W being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
for f being homogeneousSAF Form of V,W
for w being Vector of W holds f . ((0. V),w) = 0. K
proofend;

theorem Th34: :: BILINEAR:34
for K being non empty right_complementable add-associative right_zeroed associative distributive left_unital doubleLoopStr
for V, W being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
for f being homogeneousFAF Form of V,W
for v being Vector of V holds f . (v,(0. W)) = 0. K
proofend;

theorem Th35: :: BILINEAR:35
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V, W being VectSp of K
for v, u being Vector of V
for w being Vector of W
for f being additiveSAF homogeneousSAF Form of V,W holds f . ((v - u),w) = (f . (v,w)) - (f . (u,w))
proofend;

theorem Th36: :: BILINEAR:36
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V, W being VectSp of K
for v being Vector of V
for w, t being Vector of W
for f being additiveFAF homogeneousFAF Form of V,W holds f . (v,(w - t)) = (f . (v,w)) - (f . (v,t))
proofend;

theorem Th37: :: BILINEAR:37
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V, W being VectSp of K
for v, u being Vector of V
for w, t being Vector of W
for f being bilinear-Form of V,W holds f . ((v - u),(w - t)) = ((f . (v,w)) - (f . (v,t))) - ((f . (u,w)) - (f . (u,t)))
proofend;

theorem :: BILINEAR:38
for K being non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V, W being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
for v, u being Vector of V
for w, t being Vector of W
for a, b being Element of K
for f being 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)))))
proofend;

theorem :: BILINEAR:39
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V, W being VectSp of K
for v, u being Vector of V
for w, t being Vector of W
for a, b being Element of K
for f being 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)))))
proofend;

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

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 15
 {  v where v is Vector of V : for w being Vector of W holds f . (v,w) = 0. K  }  ;
correctness
coherence
{  v where v is Vector of V : for w being Vector of W holds f . (v,w) = 0. K  }  is Subset of V;
proofend;
end;

:: deftheorem  defines leftker BILINEAR:def_15_:_
 for K being ZeroStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds leftker f =  {  v where v is Vector of V : for w being Vector of W holds f . (v,w) = 0. K  }  ;

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 16
 {  w where w is Vector of W : for v being Vector of V holds f . (v,w) = 0. K  }  ;
correctness
coherence
{  w where w is Vector of W : for v being Vector of V holds f . (v,w) = 0. K  }  is Subset of W;
proofend;
end;

:: deftheorem  defines rightker BILINEAR:def_16_:_
 for K being ZeroStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds rightker f =  {  w where w is Vector of W : for v being Vector of V holds f . (v,w) = 0. K  }  ;

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 17
 {  v where v is Vector of V : f . (v,v) = 0. K  }  ;
correctness
coherence
{  v where v is Vector of V : f . (v,v) = 0. K  }  is Subset of V;
proofend;
end;

:: deftheorem  defines diagker BILINEAR:def_17_:_
 for K being ZeroStr
for V being non empty VectSpStr over K
for f being Form of V,V holds diagker f =  {  v where v is Vector of V : f . (v,v) = 0. K  }  ;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty right_zeroed VectSpStr over K;
let W be non empty VectSpStr over K;
let f be additiveSAF Form of V,W;
cluster leftker f ->  non empty ;
coherence
 not leftker f is empty
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K;
let W be non empty VectSpStr over K;
let f be homogeneousSAF Form of V,W;
cluster leftker f ->  non empty ;
coherence
 not leftker f is empty
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty VectSpStr over K;
let W be non empty right_zeroed VectSpStr over K;
let f be additiveFAF Form of V,W;
cluster rightker f ->  non empty ;
coherence
 not rightker f is empty
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be non empty VectSpStr over K;
let W be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K;
let f be homogeneousFAF Form of V,W;
cluster rightker f ->  non empty ;
coherence
 not rightker f is empty
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let V be non empty right_zeroed VectSpStr over K;
let f be additiveFAF Form of V,V;
cluster diagker f ->  non empty ;
coherence
 not diagker f is empty
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let V be non empty right_zeroed VectSpStr over K;
let f be additiveSAF Form of V,V;
cluster diagker f ->  non empty ;
coherence
 not diagker f is empty
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K;
let f be homogeneousFAF Form of V,V;
cluster diagker f ->  non empty ;
coherence
 not diagker f is empty
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K;
let f be homogeneousSAF Form of V,V;
cluster diagker f ->  non empty ;
coherence
 not diagker f is empty
proofend;
end;

theorem :: BILINEAR:41
for K being ZeroStr
for V being non empty VectSpStr over K
for f being Form of V,V holds
( leftker f c= diagker f & rightker f c= diagker f )
proofend;

theorem Th42: :: BILINEAR:42
for K being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for V, W being non empty VectSpStr over K
for f being additiveSAF homogeneousSAF Form of V,W holds leftker f is linearly-closed
proofend;

theorem Th43: :: BILINEAR:43
for K being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for V, W being non empty VectSpStr over K
for f being additiveFAF homogeneousFAF Form of V,W holds rightker f is linearly-closed
proofend;

definition
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be VectSp of K;
let W be non empty VectSpStr over K;
let f be additiveSAF homogeneousSAF Form of V,W;
func LKer f ->  non empty strict Subspace of V means :Def18: :: BILINEAR:def 18
 the carrier of it = leftker f;
existence
 ex b1 being non empty strict Subspace of V st the carrier of b1 = leftker f by Th42, VECTSP_4:34;
uniqueness
 for b1, b2 being non empty strict Subspace of V st the carrier of b1 = leftker f & the carrier of b2 = leftker f holds
b1 = b2 by VECTSP_4:29;
end;

:: deftheorem Def18 defines LKer BILINEAR:def_18_:_
 for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being non empty VectSpStr over K
for f being additiveSAF homogeneousSAF Form of V,W
for b5 being non empty strict Subspace of V holds
( b5 = LKer f iff the carrier of b5 = leftker f );

definition
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be non empty VectSpStr over K;
let W be VectSp of K;
let f be additiveFAF homogeneousFAF Form of V,W;
func RKer f ->  non empty strict Subspace of W means :Def19: :: BILINEAR:def 19
 the carrier of it = rightker f;
existence
 ex b1 being non empty strict Subspace of W st the carrier of b1 = rightker f by Th43, VECTSP_4:34;
uniqueness
 for b1, b2 being non empty strict Subspace of W st the carrier of b1 = rightker f & the carrier of b2 = rightker f holds
b1 = b2 by VECTSP_4:29;
end;

:: deftheorem Def19 defines RKer BILINEAR:def_19_:_
 for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being non empty VectSpStr over K
for W being VectSp of K
for f being additiveFAF homogeneousFAF Form of V,W
for b5 being non empty strict Subspace of W holds
( b5 = RKer f iff the carrier of b5 = rightker f );

definition
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be VectSp of K;
let 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 :Def20: :: BILINEAR:def 20
 for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
it . (A,w) = f . (v,w);
existence
 ex b1 being additiveSAF homogeneousSAF Form of (VectQuot (V,(LKer f))),W st
for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
b1 . (A,w) = f . (v,w)
proofend;
uniqueness
 for b1, b2 being additiveSAF homogeneousSAF Form of (VectQuot (V,(LKer f))),W st ( for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
b1 . (A,w) = f . (v,w) ) & ( for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
b2 . (A,w) = f . (v,w) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def20 defines LQForm BILINEAR:def_20_:_
 for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being non empty VectSpStr over K
for f being additiveSAF homogeneousSAF Form of V,W
for b5 being additiveSAF homogeneousSAF Form of (VectQuot (V,(LKer f))),W holds
( b5 = LQForm f iff for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
b5 . (A,w) = f . (v,w) );

definition
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be non empty VectSpStr over K;
let 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 :Def21: :: BILINEAR:def 21
 for A being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
it . (v,A) = f . (v,w);
existence
 ex b1 being additiveFAF homogeneousFAF Form of V,(VectQuot (W,(RKer f))) st
for A being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
b1 . (v,A) = f . (v,w)
proofend;
uniqueness
 for b1, b2 being additiveFAF homogeneousFAF Form of V,(VectQuot (W,(RKer f))) st ( for A being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
b1 . (v,A) = f . (v,w) ) & ( for A being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
b2 . (v,A) = f . (v,w) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def21 defines RQForm BILINEAR:def_21_:_
 for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being non empty VectSpStr over K
for W being VectSp of K
for f being additiveFAF homogeneousFAF Form of V,W
for b5 being additiveFAF homogeneousFAF Form of V,(VectQuot (W,(RKer f))) holds
( b5 = RQForm f iff for A being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
b5 . (v,A) = f . (v,w) );

registration
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V, W be VectSp of K;
let f be bilinear-Form of V,W;
cluster LQForm f ->  additiveFAF additiveSAF homogeneousFAF homogeneousSAF ;
coherence
 ( LQForm f is additiveFAF & LQForm f is homogeneousFAF )
proofend;
cluster RQForm f ->  additiveFAF additiveSAF homogeneousFAF homogeneousSAF ;
coherence
 ( RQForm f is additiveSAF & RQForm f is homogeneousSAF )
proofend;
end;

definition
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive 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 :Def22: :: BILINEAR:def 22
 for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
it . (A,B) = f . (v,w);
existence
 ex b1 being bilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer f))) st
for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
b1 . (A,B) = f . (v,w)
proofend;
uniqueness
 for b1, b2 being bilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer f))) st ( for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
b1 . (A,B) = f . (v,w) ) & ( for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
b2 . (A,B) = f . (v,w) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def22 defines QForm BILINEAR:def_22_:_
 for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V, W being VectSp of K
for f being bilinear-Form of V,W
for b5 being bilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer f))) holds
( b5 = QForm f iff for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
b5 . (A,B) = f . (v,w) );

theorem Th44: :: BILINEAR:44
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being non empty VectSpStr over K
for f being additiveSAF homogeneousSAF Form of V,W holds rightker f = rightker (LQForm f)
proofend;

theorem Th45: :: BILINEAR:45
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being non empty VectSpStr over K
for W being VectSp of K
for f being additiveFAF homogeneousFAF Form of V,W holds leftker f = leftker (RQForm f)
proofend;

theorem Th46: :: BILINEAR:46
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V, W being VectSp of K
for f being bilinear-Form of V,W holds RKer f = RKer (LQForm f)
proofend;

theorem Th47: :: BILINEAR:47
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V, W being VectSp of K
for f being bilinear-Form of V,W holds LKer f = LKer (RQForm f)
proofend;

theorem Th48: :: BILINEAR:48
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V, W being VectSp of K
for f being bilinear-Form of V,W holds
( QForm f = RQForm (LQForm f) & QForm f = LQForm (RQForm f) )
proofend;

theorem Th49: :: BILINEAR:49
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
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)) )
proofend;

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

theorem Th51: :: BILINEAR:51
for K being non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for V, W being non empty VectSpStr over K
for f being Functional of V
for g being Functional of W st g <> 0Functional W holds
leftker (FormFunctional (f,g)) = ker f
proofend;

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

theorem Th53: :: BILINEAR:53
for K being non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for V, W being non empty VectSpStr over K
for f being Functional of V
for g being Functional of W st f <> 0Functional V holds
rightker (FormFunctional (f,g)) = ker g
proofend;

theorem Th54: :: BILINEAR:54
for K being non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being non empty VectSpStr over K
for f being linear-Functional of V
for g being Functional of W st g <> 0Functional W holds
( LKer (FormFunctional (f,g)) = Ker f &amp; LQForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),g) )
proofend;

theorem Th55: :: BILINEAR:55
for K being non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for V being non empty VectSpStr over 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 &amp; RQForm (FormFunctional (f,g)) = FormFunctional (f,(CQFunctional g)) )
proofend;

theorem :: BILINEAR:56
for K being Field
for V, W being non trivial VectSp of K
for f being V17() linear-Functional of V
for g being V17() linear-Functional of W holds QForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),(CQFunctional g))
proofend;

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

:: deftheorem Def23 defines degenerated-on-left BILINEAR:def_23_:_
 for K being ZeroStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds
( f is degenerated-on-left iff leftker f <> {(0. V)} );

:: deftheorem Def24 defines degenerated-on-right BILINEAR:def_24_:_
 for K being ZeroStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds
( f is degenerated-on-right iff rightker f <> {(0. W)} );

registration
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be VectSp of K;
let W be non empty right_zeroed VectSpStr over K;
let f be additiveSAF homogeneousSAF Form of V,W;
cluster LQForm f ->  additiveSAF homogeneousSAF non degenerated-on-left ;
coherence
 not LQForm f is degenerated-on-left
proofend;
end;

registration
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be non empty right_zeroed VectSpStr over K;
let W be VectSp of K;
let f be additiveFAF homogeneousFAF Form of V,W;
cluster RQForm f ->  additiveFAF homogeneousFAF non degenerated-on-right ;
coherence
 not RQForm f is degenerated-on-right
proofend;
end;

registration
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive 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 ;
coherence
 ( not QForm f is degenerated-on-left &amp; not QForm f is degenerated-on-right )
proofend;
end;

registration
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V, W be VectSp of K;
let f be bilinear-Form of V,W;
cluster RQForm (LQForm f) ->  additiveFAF homogeneousFAF non degenerated-on-left non degenerated-on-right ;
coherence
 ( not RQForm (LQForm f) is degenerated-on-left &amp; not RQForm (LQForm f) is degenerated-on-right )
proofend;
cluster LQForm (RQForm f) ->  additiveSAF homogeneousSAF non degenerated-on-left non degenerated-on-right ;
coherence
 ( not LQForm (RQForm f) is degenerated-on-left &amp; not LQForm (RQForm f) is degenerated-on-right )
proofend;
end;

registration
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 ;
coherence
 not QForm f is constant
proofend;
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;
attrf is symmetric  means :Def25: :: BILINEAR:def 25
 for v, w being Vector of V holds f . (v,w) = f . (w,v);
end;

:: deftheorem Def25 defines symmetric BILINEAR:def_25_:_
 for K being 1-sorted
for V being VectSpStr over K
for f being Form of V,V holds
( f is symmetric iff for v, w being Vector of V holds f . (v,w) = f . (w,v) );

definition
let K be ZeroStr ;
let V be VectSpStr over K;
let f be Form of V,V;
attrf is alternating  means :Def26: :: BILINEAR:def 26
 for v being Vector of V holds f . (v,v) = 0. K;
end;

:: deftheorem Def26 defines alternating BILINEAR:def_26_:_
 for K being ZeroStr
for V being VectSpStr over K
for f being Form of V,V holds
( f is alternating iff for v being Vector of V holds f . (v,v) = 0. K );

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

registration
let K be non empty ZeroStr ;
let V be non empty VectSpStr over K;
cluster non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of V:]) V21([: the carrier of V, the carrier of V:], the carrier of K) symmetric for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of K:];
existence
 ex b1 being Form of V,V st b1 is symmetric
proofend;
cluster non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of V:]) V21([: the carrier of V, the carrier of V:], the carrier of K) alternating for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of K:];
existence
 ex b1 being Form of V,V st b1 is alternating
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty VectSpStr over K;
cluster non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of V:]) V21([: the carrier of V, the carrier of V:], the carrier of K) additiveFAF additiveSAF homogeneousFAF homogeneousSAF symmetric for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of K:];
existence
 ex b1 being Form of V,V st
( b1 is symmetric &amp; b1 is additiveFAF &amp; b1 is homogeneousFAF &amp; b1 is additiveSAF &amp; b1 is homogeneousSAF )
proofend;
cluster non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of V:]) V21([: the carrier of V, the carrier of V:], the carrier of K) additiveFAF additiveSAF homogeneousFAF homogeneousSAF alternating for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of K:];
existence
 ex b1 being Form of V,V st
( b1 is alternating &amp; b1 is additiveFAF &amp; b1 is homogeneousFAF &amp; b1 is additiveSAF &amp; b1 is homogeneousSAF )
proofend;
end;

registration
let K be Field;
let V be non trivial VectSp of K;
cluster non empty non trivial Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of K -valued Function-like non constant V20([: the carrier of V, the carrier of V:]) V21([: the carrier of V, the carrier of V:], the carrier of K) additiveFAF additiveSAF homogeneousFAF homogeneousSAF symmetric for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of K:];
existence
 ex b1 being Form of V,V st
( b1 is symmetric &amp; not b1 is trivial &amp; not b1 is constant &amp; b1 is additiveFAF &amp; b1 is homogeneousFAF &amp; b1 is additiveSAF &amp; b1 is homogeneousSAF )
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed addLoopStr ;
let V be non empty VectSpStr over K;
cluster non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of V:]) V21([: the carrier of V, the carrier of V:], the carrier of K) additiveFAF additiveSAF alternating for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of K:];
existence
 ex b1 being Form of V,V st
( b1 is alternating &amp; b1 is additiveFAF &amp; b1 is additiveSAF )
proofend;
end;

registration
let K be non empty addLoopStr ;
let V be non empty VectSpStr over K;
let f, g be symmetric Form of V,V;
clusterf + g ->  symmetric ;
coherence
 f + g is symmetric
proofend;
end;

registration
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;
clustera * f ->  symmetric ;
coherence
 a * f is symmetric
proofend;
end;

registration
let K be non empty addLoopStr ;
let V be non empty VectSpStr over K;
let f be symmetric Form of V,V;
cluster - f ->  symmetric ;
coherence
 - f is symmetric
proofend;
end;

registration
let K be non empty addLoopStr ;
let V be non empty VectSpStr over K;
let f, g be symmetric Form of V,V;
clusterf - g ->  symmetric ;
coherence
 f - g is symmetric ;
end;

registration
let K be non empty right_zeroed addLoopStr ;
let V be non empty VectSpStr over K;
let f, g be alternating Form of V,V;
clusterf + g ->  alternating ;
coherence
 f + g is alternating
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty VectSpStr over K;
let f be alternating Form of V,V;
let a be Scalar of K;
clustera * f ->  alternating ;
coherence
 a * f is alternating
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed addLoopStr ;
let V be non empty VectSpStr over K;
let f be alternating Form of V,V;
cluster - f ->  alternating ;
coherence
 - f is alternating
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed addLoopStr ;
let V be non empty VectSpStr over K;
let f, g be alternating Form of V,V;
clusterf - g ->  alternating ;
coherence
 f - g is alternating ;
end;

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

theorem Th58: :: BILINEAR:58
for K being non empty right_complementable add-associative right_zeroed addLoopStr
for V being non empty VectSpStr over K
for f being additiveFAF additiveSAF alternating Form of V,V
for v, w being Vector of V holds f . (v,w) = - (f . (w,v))
proofend;

definition
let K be Fanoian Field;
let V be non empty VectSpStr over K;
let f be additiveFAF additiveSAF Form of V,V;
redefine attr f is alternating  means :: BILINEAR:def 27
 for v, w being Vector of V holds f . (v,w) = - (f . (w,v));
compatibility
 ( f is alternating iff for v, w being Vector of V holds f . (v,w) = - (f . (w,v)) )
proofend;
end;

:: deftheorem  defines alternating BILINEAR:def_27_:_
 for K being Fanoian Field
for V being non empty VectSpStr over K
for f being additiveFAF additiveSAF Form of V,V holds
( f is alternating iff for v, w being Vector of V holds f . (v,w) = - (f . (w,v)) );

theorem :: BILINEAR:59
for K being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for V being non empty VectSpStr over K
for f being alternating bilinear-Form of V,V holds leftker f = rightker f
proofend;