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

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

definition

let K be 1-sorted ;
let V, W be ModuleStr 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 ModuleStr 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 ModuleStr 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 ModuleStr over K;
let f, g be Form of V,W;

func f + 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 b₁ being Form of V,W st
for v being Vector of V
for w being Vector of W holds b₁ . (v,w) = (f . (v,w)) + (g . (v,w))

proof end;

uniqueness
for b₁, b₂ being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b₁ . (v,w) = (f . (v,w)) + (g . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds b₂ . (v,w) = (f . (v,w)) + (g . (v,w)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines + BILINEAR:def 2 :
for K being non empty addLoopStr
for V, W being non empty ModuleStr over K
for f, g, b₆ being Form of V,W holds
( b₆ = f + g iff for v being Vector of V
for w being Vector of W holds b₆ . (v,w) = (f . (v,w)) + (g . (v,w)) );

definition

let K be non empty multMagma ;
let V, W be non empty ModuleStr over K;
let f be Form of V,W;
let a be Element of K;

func a * 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 b₁ being Form of V,W st
for v being Vector of V
for w being Vector of W holds b₁ . (v,w) = a * (f . (v,w))

proof end;

uniqueness
for b₁, b₂ being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b₁ . (v,w) = a * (f . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds b₂ . (v,w) = a * (f . (v,w)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines * BILINEAR:def 3 :
for K being non empty multMagma
for V, W being non empty ModuleStr over K
for f being Form of V,W
for a being Element of K
for b₆ being Form of V,W holds
( b₆ = a * f iff for v being Vector of V
for w being Vector of W holds b₆ . (v,w) = a * (f . (v,w)) );

definition

let K be non empty addLoopStr ;
let V, W be non empty ModuleStr 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 b₁ being Form of V,W st
for v being Vector of V
for w being Vector of W holds b₁ . (v,w) = - (f . (v,w))

proof end;

uniqueness
for b₁, b₂ being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b₁ . (v,w) = - (f . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds b₂ . (v,w) = - (f . (v,w)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines - BILINEAR:def 4 :
for K being non empty addLoopStr
for V, W being non empty ModuleStr over K
for f, b₅ being Form of V,W holds
( b₅ = - f iff for v being Vector of V
for w being Vector of W holds b₅ . (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 ModuleStr over K;
let f be Form of V,W;

redefine func - f equals :: BILINEAR:def 5
(- (1. K)) * f;

compatibility
for b₁ being Form of V,W holds
( b₁ = - f iff b₁ = (- (1. K)) * f )

proof end;

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 ModuleStr 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 ModuleStr over K;
let f, g be Form of V,W;

func f - 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 ModuleStr 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 ModuleStr 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 b₁ being Form of V,W holds
( b₁ = f - g iff for v being Vector of V
for w being Vector of W holds b₁ . (v,w) = (f . (v,w)) - (g . (v,w)) )

proof end;

end;

:: deftheorem Def7 defines - BILINEAR:def 7 :
for K being non empty addLoopStr
for V, W being non empty ModuleStr over K
for f, g, b₆ being Form of V,W holds
( b₆ = f - g iff for v being Vector of V
for w being Vector of W holds b₆ . (v,w) = (f . (v,w)) - (g . (v,w)) );

definition

let K be non empty Abelian addLoopStr ;
let V, W be non empty ModuleStr over K;
let f, g be Form of V,W;
:: original: +
redefine func f + g -> Form of V,W;
commutativity
for f, g being Form of V,W holds f + g = g + f

proof end;

end;

theorem :: BILINEAR:1

for K being non empty right_zeroed addLoopStr
for V, W being non empty ModuleStr over K
for f being Form of V,W holds f + (NulForm (V,W)) = f

proof end;

theorem :: BILINEAR:2

for K being non empty add-associative addLoopStr
for V, W being non empty ModuleStr over K
for f, g, h being Form of V,W holds (f + g) + h = f + (g + h)

proof end;

theorem :: BILINEAR:3

for K being non empty right_complementable add-associative right_zeroed addLoopStr
for V, W being non empty ModuleStr over K
for f being Form of V,W holds f - f = NulForm (V,W)

proof end;

theorem :: BILINEAR:4

for K being non empty right-distributive doubleLoopStr
for V, W being non empty ModuleStr over K
for a being Element of K
for f, g being Form of V,W holds a * (f + g) = (a * f) + (a * g)

proof end;

theorem :: BILINEAR:5

for K being non empty left-distributive doubleLoopStr
for V, W being non empty ModuleStr over K
for a, b being Element of K
for f being Form of V,W holds (a + b) * f = (a * f) + (b * f)

proof end;

theorem :: BILINEAR:6

for K being non empty associative doubleLoopStr
for V, W being non empty ModuleStr over K
for a, b being Element of K
for f being Form of V,W holds (a * b) * f = a * (b * f)

proof end;

theorem :: BILINEAR:7

for K being non empty left_unital doubleLoopStr
for V, W being non empty ModuleStr over K
for f being Form of V,W holds (1. K) * f = f

proof end;

:: 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 ModuleStr 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 ModuleStr 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 ModuleStr 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 ModuleStr 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 ModuleStr 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) ) )

proof end;

theorem Th9: :: BILINEAR:9

for K being non empty 1-sorted
for V, W being non empty ModuleStr 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) ) )

proof end;

theorem Th10: :: BILINEAR:10

for K being non empty ZeroStr
for V, W being non empty ModuleStr over K
for v being Vector of V holds FunctionalFAF ((NulForm (V,W)),v) = 0Functional W

proof end;

theorem Th11: :: BILINEAR:11

for K being non empty ZeroStr
for V, W being non empty ModuleStr over K
for w being Vector of W holds FunctionalSAF ((NulForm (V,W)),w) = 0Functional V

proof end;

theorem Th12: :: BILINEAR:12

for K being non empty addLoopStr
for V, W being non empty ModuleStr 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))

proof end;

theorem Th13: :: BILINEAR:13

for K being non empty addLoopStr
for V, W being non empty ModuleStr 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))

proof end;

theorem Th14: :: BILINEAR:14

for K being non empty doubleLoopStr
for V, W being non empty ModuleStr 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))

proof end;

theorem Th15: :: BILINEAR:15

for K being non empty doubleLoopStr
for V, W being non empty ModuleStr 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))

proof end;

theorem Th16: :: BILINEAR:16

for K being non empty addLoopStr
for V, W being non empty ModuleStr over K
for f being Form of V,W
for w being Vector of W holds FunctionalSAF ((- f),w) = - (FunctionalSAF (f,w))

proof end;

theorem Th17: :: BILINEAR:17

for K being non empty addLoopStr
for V, W being non empty ModuleStr over K
for f being Form of V,W
for v being Vector of V holds FunctionalFAF ((- f),v) = - (FunctionalFAF (f,v))

proof end;

theorem :: BILINEAR:18

for K being non empty addLoopStr
for V, W being non empty ModuleStr 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))

proof end;

theorem :: BILINEAR:19

for K being non empty addLoopStr
for V, W being non empty ModuleStr 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))

proof end;

:: Two Form generated by Functionals.

definition

let K be non empty multMagma ;
let V, W be non empty ModuleStr 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 b₁ being Form of V,W st
for v being Vector of V
for w being Vector of W holds b₁ . (v,w) = (f . v) * (g . w)

proof end;

uniqueness
for b₁, b₂ being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b₁ . (v,w) = (f . v) * (g . w) ) & ( for v being Vector of V
for w being Vector of W holds b₂ . (v,w) = (f . v) * (g . w) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines FormFunctional BILINEAR:def 10 :
for K being non empty multMagma
for V, W being non empty ModuleStr over K
for f being Functional of V
for g being Functional of W
for b₆ being Form of V,W holds
( b₆ = FormFunctional (f,g) iff for v being Vector of V
for w being Vector of W holds b₆ . (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 ModuleStr 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

proof end;

theorem Th21: :: BILINEAR:21

for K being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for V, W being non empty ModuleStr 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

proof end;

theorem :: BILINEAR:22

for K being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for V, W being non empty ModuleStr over K
for f being Functional of V holds FormFunctional (f,(0Functional W)) = NulForm (V,W)

proof end;

theorem :: BILINEAR:23

for K being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for V, W being non empty ModuleStr over K
for g being Functional of W holds FormFunctional ((0Functional V),g) = NulForm (V,W)

proof end;

theorem Th24: :: BILINEAR:24

for K being non empty multMagma
for V, W being non empty ModuleStr 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

proof end;

theorem Th25: :: BILINEAR:25

for K being non empty commutative multMagma
for V, W being non empty ModuleStr 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

proof end;

::Bilinear Forms and Their Properties

definition

let K be non empty addLoopStr ;
let V, W be non empty ModuleStr over K;
let f be Form of V,W;

attr f is additiveFAF means :Def11: :: BILINEAR:def 11
for v being Vector of V holds FunctionalFAF (f,v) is additive ;

attr f 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 ModuleStr 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 ModuleStr 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 ModuleStr over K;
let f be Form of V,W;

attr f is homogeneousFAF means :Def13: :: BILINEAR:def 13
for v being Vector of V holds FunctionalFAF (f,v) is homogeneous ;

attr f 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 ModuleStr 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 ModuleStr 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 ModuleStr over K;

cluster NulForm (V,W) -> additiveFAF ;

coherence
NulForm (V,W) is additiveFAF

proof end;

cluster NulForm (V,W) -> additiveSAF ;

coherence
NulForm (V,W) is additiveSAF

proof end;

end;

registration

let K be non empty right_zeroed addLoopStr ;
let V, W be non empty ModuleStr 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 b₁ being Form of V,W st
( b₁ is additiveFAF & b₁ is additiveSAF )

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty ModuleStr over K;

cluster NulForm (V,W) -> homogeneousFAF ;

coherence
NulForm (V,W) is homogeneousFAF

proof end;

cluster NulForm (V,W) -> homogeneousSAF ;

coherence
NulForm (V,W) is homogeneousSAF

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty ModuleStr 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 b₁ being Form of V,W st
( b₁ is additiveFAF & b₁ is homogeneousFAF & b₁ is additiveSAF & b₁ is homogeneousSAF )

proof end;

end;

definition

let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty ModuleStr 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 ModuleStr 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 ModuleStr 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 ModuleStr 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 ModuleStr 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 ModuleStr 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

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive commutative doubleLoopStr ;
let V, W be non empty ModuleStr 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

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive associative commutative doubleLoopStr ;
let V, W be non empty ModuleStr 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

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive associative commutative doubleLoopStr ;
let V, W be non empty ModuleStr 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

proof end;

end;

registration

let K be non empty non degenerated doubleLoopStr ;
let V be non trivial ModuleStr over K;
let W be non empty ModuleStr 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

proof end;

end;

registration

let K be non empty non degenerated doubleLoopStr ;
let V be non empty ModuleStr over K;
let W be non trivial ModuleStr 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

proof end;

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

proof end;

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 b₁ being Form of V,W st
( not b₁ is trivial & not b₁ is constant & b₁ is additiveFAF & b₁ is homogeneousFAF & b₁ is additiveSAF & b₁ is homogeneousSAF )

proof end;

end;

registration

let K be non empty Abelian add-associative right_zeroed addLoopStr ;
let V, W be non empty ModuleStr over K;
let f, g be additiveSAF Form of V,W;

cluster f + g -> additiveSAF ;

correctness
coherence
f + g is additiveSAF ;

proof end;

end;

registration

let K be non empty Abelian add-associative right_zeroed addLoopStr ;
let V, W be non empty ModuleStr over K;
let f, g be additiveFAF Form of V,W;

cluster f + g -> additiveFAF ;

correctness
coherence
f + g is additiveFAF ;

proof end;

end;

registration

let K be non empty right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty ModuleStr over K;
let f be additiveSAF Form of V,W;
let a be Element of K;

cluster a * f -> additiveSAF ;

correctness
coherence
a * f is additiveSAF ;

proof end;

end;

registration

let K be non empty right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty ModuleStr over K;
let f be additiveFAF Form of V,W;
let a be Element of K;

cluster a * f -> additiveFAF ;

correctness
coherence
a * f is additiveFAF ;

proof end;

end;

registration

let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;
let V, W be non empty ModuleStr over K;
let f be additiveSAF Form of V,W;

cluster - f -> additiveSAF ;

correctness
coherence
- f is additiveSAF ;

proof end;

end;

registration

let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;
let V, W be non empty ModuleStr over K;
let f be additiveFAF Form of V,W;

cluster - f -> additiveFAF ;

correctness
coherence
- f is additiveFAF ;

proof end;

end;

registration

let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;
let V, W be non empty ModuleStr over K;
let f, g be additiveSAF Form of V,W;

cluster f - 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 ModuleStr over K;
let f, g be additiveFAF Form of V,W;

cluster f - 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 ModuleStr over K;
let f, g be homogeneousSAF Form of V,W;

cluster f + g -> homogeneousSAF ;

correctness
coherence
f + g is homogeneousSAF ;

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty ModuleStr over K;
let f, g be homogeneousFAF Form of V,W;

cluster f + g -> homogeneousFAF ;

correctness
coherence
f + g is homogeneousFAF ;

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive associative commutative doubleLoopStr ;
let V, W be non empty ModuleStr over K;
let f be homogeneousSAF Form of V,W;
let a be Element of K;

cluster a * f -> homogeneousSAF ;

correctness
coherence
a * f is homogeneousSAF ;

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive associative commutative doubleLoopStr ;
let V, W be non empty ModuleStr over K;
let f be homogeneousFAF Form of V,W;
let a be Element of K;

cluster a * f -> homogeneousFAF ;

correctness
coherence
a * f is homogeneousFAF ;

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty ModuleStr over K;
let f be homogeneousSAF Form of V,W;

cluster - f -> homogeneousSAF ;

correctness
coherence
- f is homogeneousSAF ;

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty ModuleStr over K;
let f be homogeneousFAF Form of V,W;

cluster - f -> homogeneousFAF ;

correctness
coherence
- f is homogeneousFAF ;

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty ModuleStr over K;
let f, g be homogeneousSAF Form of V,W;

cluster f - 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 ModuleStr over K;
let f, g be homogeneousFAF Form of V,W;

cluster f - 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 ModuleStr 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))

proof end;

theorem Th27: :: BILINEAR:27

for K being non empty addLoopStr
for V, W being non empty ModuleStr 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))

proof end;

theorem Th28: :: BILINEAR:28

for K being non empty right_zeroed addLoopStr
for V, W being non empty ModuleStr 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)))

proof end;

theorem Th29: :: BILINEAR:29

for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for V, W being non empty right_zeroed ModuleStr over K
for f being additiveFAF Form of V,W
for v being Vector of V holds f . (v,(0. W)) = 0. K

proof end;

theorem Th30: :: BILINEAR:30

for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for V, W being non empty right_zeroed ModuleStr over K
for f being additiveSAF Form of V,W
for w being Vector of W holds f . ((0. V),w) = 0. K

proof end;

theorem Th31: :: BILINEAR:31

for K being non empty multMagma
for V, W being non empty ModuleStr 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))

proof end;

theorem Th32: :: BILINEAR:32

for K being non empty multMagma
for V, W being non empty ModuleStr 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))

proof end;

theorem Th33: :: BILINEAR:33

for K being non empty right_complementable add-associative right_zeroed distributive left_unital associative doubleLoopStr
for V, W being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over K
for f being homogeneousSAF Form of V,W
for w being Vector of W holds f . ((0. V),w) = 0. K

proof end;

theorem Th34: :: BILINEAR:34

for K being non empty right_complementable add-associative right_zeroed distributive left_unital associative doubleLoopStr
for V, W being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over K
for f being homogeneousFAF Form of V,W
for v being Vector of V holds f . (v,(0. W)) = 0. K

proof end;

theorem Th35: :: BILINEAR:35

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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))

proof end;

theorem Th36: :: BILINEAR:36

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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))

proof end;

theorem Th37: :: BILINEAR:37

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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)))

proof end;

theorem :: BILINEAR:38

for K being non empty right_complementable add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V, W being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr 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)))))

proof end;

theorem :: BILINEAR:39

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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)))))

proof end;

theorem Th40: :: BILINEAR:40

for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for V, W being non empty right_zeroed ModuleStr 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 )

proof end;

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

definition

let K be ZeroStr ;
let V, W be non empty ModuleStr 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;

proof end;

end;

:: deftheorem defines leftker BILINEAR:def 15 :
for K being ZeroStr
for V, W being non empty ModuleStr 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 ModuleStr 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;

proof end;

end;

:: deftheorem defines rightker BILINEAR:def 16 :
for K being ZeroStr
for V, W being non empty ModuleStr 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 ModuleStr 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;

proof end;

end;

:: deftheorem defines diagker BILINEAR:def 17 :
for K being ZeroStr
for V being non empty ModuleStr 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 ModuleStr over K;
let W be non empty ModuleStr over K;
let f be additiveSAF Form of V,W;

cluster leftker f -> non empty ;

coherence
not leftker f is empty

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed well-unital distributive associative doubleLoopStr ;
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over K;
let W be non empty ModuleStr over K;
let f be homogeneousSAF Form of V,W;

cluster leftker f -> non empty ;

coherence
not leftker f is empty

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty ModuleStr over K;
let W be non empty right_zeroed ModuleStr over K;
let f be additiveFAF Form of V,W;

cluster rightker f -> non empty ;

coherence
not rightker f is empty

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed well-unital distributive associative doubleLoopStr ;
let V be non empty ModuleStr over K;
let W be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over K;
let f be homogeneousFAF Form of V,W;

cluster rightker f -> non empty ;

coherence
not rightker f is empty

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let V be non empty right_zeroed ModuleStr over K;
let f be additiveFAF Form of V,V;

cluster diagker f -> non empty ;

coherence
not diagker f is empty

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let V be non empty right_zeroed ModuleStr over K;
let f be additiveSAF Form of V,V;

cluster diagker f -> non empty ;

coherence
not diagker f is empty

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed well-unital distributive associative doubleLoopStr ;
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over K;
let f be homogeneousFAF Form of V,V;

cluster diagker f -> non empty ;

coherence
not diagker f is empty

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed well-unital distributive associative doubleLoopStr ;
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over K;
let f be homogeneousSAF Form of V,V;

cluster diagker f -> non empty ;

coherence
not diagker f is empty

proof end;

end;

theorem :: BILINEAR:41

for K being ZeroStr
for V being non empty ModuleStr over K
for f being Form of V,V holds
( leftker f c= diagker f & rightker f c= diagker f )

proof end;

theorem Th42: :: BILINEAR:42

for K being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for V, W being non empty ModuleStr over K
for f being additiveSAF homogeneousSAF Form of V,W holds leftker f is linearly-closed

proof end;

theorem Th43: :: BILINEAR:43

for K being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for V, W being non empty ModuleStr over K
for f being additiveFAF homogeneousFAF Form of V,W holds rightker f is linearly-closed

proof end;

definition

let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ;
let V be VectSp of K;
let W be non empty ModuleStr 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 b₁ being non empty strict Subspace of V st the carrier of b₁ = leftker f by Th42, VECTSP_4:34;
uniqueness
for b₁, b₂ being non empty strict Subspace of V st the carrier of b₁ = leftker f & the carrier of b₂ = leftker f holds
b₁ = b₂ by VECTSP_4:29;

end;

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

definition

let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ;
let V be non empty ModuleStr 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 b₁ being non empty strict Subspace of W st the carrier of b₁ = rightker f by Th43, VECTSP_4:34;
uniqueness
for b₁, b₂ being non empty strict Subspace of W st the carrier of b₁ = rightker f & the carrier of b₂ = rightker f holds
b₁ = b₂ by VECTSP_4:29;

end;

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

definition

let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ;
let V be VectSp of K;
let W be non empty ModuleStr 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 b₁ 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
b₁ . (A,w) = f . (v,w)

proof end;

uniqueness
for b₁, b₂ 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
b₁ . (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
b₂ . (A,w) = f . (v,w) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def20 defines LQForm BILINEAR:def 20 :
for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V being VectSp of K
for W being non empty ModuleStr over K
for f being additiveSAF homogeneousSAF Form of V,W
for b₅ being additiveSAF homogeneousSAF Form of (VectQuot (V,(LKer f))),W holds
( b₅ = 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
b₅ . (A,w) = f . (v,w) );

definition

let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ;
let V be non empty ModuleStr 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 b₁ 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
b₁ . (v,A) = f . (v,w)

proof end;

uniqueness
for b₁, b₂ 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
b₁ . (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
b₂ . (v,A) = f . (v,w) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def21 defines RQForm BILINEAR:def 21 :
for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V being non empty ModuleStr over K
for W being VectSp of K
for f being additiveFAF homogeneousFAF Form of V,W
for b₅ being additiveFAF homogeneousFAF Form of V,(VectQuot (W,(RKer f))) holds
( b₅ = 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
b₅ . (v,A) = f . (v,w) );

registration

let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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 )

proof end;

cluster RQForm f -> additiveFAF additiveSAF homogeneousFAF homogeneousSAF ;

coherence
( RQForm f is additiveSAF & RQForm f is homogeneousSAF )

proof end;

end;

definition

let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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 b₁ 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
b₁ . (A,B) = f . (v,w)

proof end;

uniqueness
for b₁, b₂ 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
b₁ . (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
b₂ . (A,B) = f . (v,w) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def22 defines QForm BILINEAR:def 22 :
for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V, W being VectSp of K
for f being bilinear-Form of V,W
for b₅ being bilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer f))) holds
( b₅ = 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
b₅ . (A,B) = f . (v,w) );

theorem Th44: :: BILINEAR:44

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V being VectSp of K
for W being non empty ModuleStr over K
for f being additiveSAF homogeneousSAF Form of V,W holds rightker f = rightker (LQForm f)

proof end;

theorem Th45: :: BILINEAR:45

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V being non empty ModuleStr over K
for W being VectSp of K
for f being additiveFAF homogeneousFAF Form of V,W holds leftker f = leftker (RQForm f)

proof end;

theorem Th46: :: BILINEAR:46

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

proof end;

theorem Th47: :: BILINEAR:47

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

proof end;

theorem Th48: :: BILINEAR:48

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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) )

proof end;

theorem Th49: :: BILINEAR:49

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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)) )

proof end;

theorem Th50: :: BILINEAR:50

for K being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for V, W being non empty ModuleStr over K
for f being Functional of V
for g being Functional of W holds ker f c= leftker (FormFunctional (f,g))

proof end;

theorem Th51: :: BILINEAR:51

for K being non empty right_complementable almost_left_invertible add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr
for V, W being non empty ModuleStr 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

proof end;

theorem Th52: :: BILINEAR:52

for K being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for V, W being non empty ModuleStr over K
for f being Functional of V
for g being Functional of W holds ker g c= rightker (FormFunctional (f,g))

proof end;

theorem Th53: :: BILINEAR:53

for K being non empty right_complementable almost_left_invertible add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr
for V, W being non empty ModuleStr 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

proof end;

theorem Th54: :: BILINEAR:54

for K being non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr
for V being VectSp of K
for W being non empty ModuleStr 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 & LQForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),g) )

proof end;

theorem Th55: :: BILINEAR:55

for K being non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr
for V being non empty ModuleStr 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 & RQForm (FormFunctional (f,g)) = FormFunctional (f,(CQFunctional g)) )

proof end;

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))

proof end;

definition

let K be ZeroStr ;
let V, W be non empty ModuleStr over K;
let f be Form of V,W;

attr f is degenerated-on-left means :Def23: :: BILINEAR:def 23
leftker f <> {(0. V)};

attr f 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 ModuleStr 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 ModuleStr 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 well-unital distributive associative doubleLoopStr ;
let V be VectSp of K;
let W be non empty right_zeroed ModuleStr 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

proof end;

end;

registration

let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ;
let V be non empty right_zeroed ModuleStr 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

proof end;

end;

registration

let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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 & not QForm f is degenerated-on-right )

proof end;

end;

registration

let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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 & not RQForm (LQForm f) is degenerated-on-right )

proof end;

cluster LQForm (RQForm f) -> additiveSAF homogeneousSAF non degenerated-on-left non degenerated-on-right ;

coherence
( not LQForm (RQForm f) is degenerated-on-left & not LQForm (RQForm f) is degenerated-on-right )

proof end;

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

proof end;

end;

:: Bilinear Symmetric and Alternating Forms

definition

let K be 1-sorted ;
let V be ModuleStr over K;
let f be Form of V,V;

attr f 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 ModuleStr 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 ModuleStr over K;
let f be Form of V,V;

attr f 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 ModuleStr 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 ModuleStr over K;

cluster NulForm (V,V) -> symmetric ;

coherence
NulForm (V,V) is symmetric

proof end;

cluster NulForm (V,V) -> alternating ;

coherence
NulForm (V,V) is alternating by FUNCOP_1:70;

end;

registration

let K be non empty ZeroStr ;
let V be non empty ModuleStr 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 b₁ being Form of V,V st b₁ is symmetric

proof end;

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 b₁ being Form of V,V st b₁ is alternating

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty ModuleStr 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 b₁ being Form of V,V st
( b₁ is symmetric & b₁ is additiveFAF & b₁ is homogeneousFAF & b₁ is additiveSAF & b₁ is homogeneousSAF )

proof end;

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 b₁ being Form of V,V st
( b₁ is alternating & b₁ is additiveFAF & b₁ is homogeneousFAF & b₁ is additiveSAF & b₁ is homogeneousSAF )

proof end;

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 b₁ being Form of V,V st
( b₁ is symmetric & not b₁ is trivial & not b₁ is constant & b₁ is additiveFAF & b₁ is homogeneousFAF & b₁ is additiveSAF & b₁ is homogeneousSAF )

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed addLoopStr ;
let V be non empty ModuleStr 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 b₁ being Form of V,V st
( b₁ is alternating & b₁ is additiveFAF & b₁ is additiveSAF )

proof end;

end;

registration

let K be non empty addLoopStr ;
let V be non empty ModuleStr over K;
let f, g be symmetric Form of V,V;

cluster f + g -> symmetric ;

coherence
f + g is symmetric

proof end;

end;

registration

let K be non empty doubleLoopStr ;
let V be non empty ModuleStr over K;
let f be symmetric Form of V,V;
let a be Element of K;

cluster a * f -> symmetric ;

coherence
a * f is symmetric

proof end;

end;

registration

let K be non empty addLoopStr ;
let V be non empty ModuleStr over K;
let f be symmetric Form of V,V;

cluster - f -> symmetric ;

coherence
- f is symmetric

proof end;

end;

registration

let K be non empty addLoopStr ;
let V be non empty ModuleStr over K;
let f, g be symmetric Form of V,V;

cluster f - g -> symmetric ;

coherence
f - g is symmetric ;

end;

registration

let K be non empty right_zeroed addLoopStr ;
let V be non empty ModuleStr over K;
let f, g be alternating Form of V,V;

cluster f + g -> alternating ;

coherence
f + g is alternating

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty ModuleStr over K;
let f be alternating Form of V,V;
let a be Scalar of K;

cluster a * f -> alternating ;

coherence
a * f is alternating

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed addLoopStr ;
let V be non empty ModuleStr over K;
let f be alternating Form of V,V;

cluster - f -> alternating ;

coherence
- f is alternating

proof end;

end;

registration

let K be non empty right_complementable add-associative right_zeroed addLoopStr ;
let V be non empty ModuleStr over K;
let f, g be alternating Form of V,V;

cluster f - 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 ModuleStr over K
for f being symmetric bilinear-Form of V,V holds leftker f = rightker f

proof end;

theorem Th58: :: BILINEAR:58

for K being non empty right_complementable add-associative right_zeroed addLoopStr
for V being non empty ModuleStr 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))

proof end;

definition

let K be Fanoian Field;
let V be non empty ModuleStr 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)) )

proof end;

end;

:: deftheorem defines alternating BILINEAR:def 27 :
for K being Fanoian Field
for V being non empty ModuleStr 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 ModuleStr over K
for f being alternating bilinear-Form of V,V holds leftker f = rightker f

proof end;