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

begin

definition

let K be 1-sorted ;
let V, W be VectSpStr of 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 of K;
canceled;
func NulForm (V,W) -> Form of V,W equals :: BILINEAR:def 2
[: 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 BILINEAR:def 1 :
canceled;

:: deftheorem defines NulForm BILINEAR:def 2 :
for K being non empty ZeroStr
for V, W being VectSpStr of 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 of K;
let f, g be Form of V,W;
func f + g -> 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) = (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 Def3 defines + BILINEAR:def 3 :
for K being non empty addLoopStr
for V, W being non empty VectSpStr of 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 VectSpStr of K;
let f be Form of V,W;
let a be Element of K;
func a * 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) = 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 Def4 defines * BILINEAR:def 4 :
for K being non empty multMagma
for V, W being non empty VectSpStr of 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 VectSpStr of K;
let f be Form of V,W;
func - f -> Form of V,W means :Def5: :: BILINEAR:def 5
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 Def5 defines - BILINEAR:def 5 :
for K being non empty addLoopStr
for V, W being non empty VectSpStr of 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 VectSpStr of K;
let f be Form of V,W;
redefine func - f equals :: BILINEAR:def 6
(- (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 6 :
for K being non empty right_complementable add-associative right_zeroed left-distributive left_unital doubleLoopStr
for V, W being non empty VectSpStr of 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 of K;
let f, g be Form of V,W;
func f - g -> Form of V,W equals :: BILINEAR:def 7
f + (- g);
correctness
coherence
f + (- g) is Form of V,W;
;

end;

:: deftheorem defines - BILINEAR:def 7 :
for K being non empty addLoopStr
for V, W being non empty VectSpStr of 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 of K;
let f, g be Form of V,W;
redefine func f - g means :Def8: :: BILINEAR:def 8
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 Def8 defines - BILINEAR:def 8 :
for K being non empty addLoopStr
for V, W being non empty VectSpStr of 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 VectSpStr of 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

canceled;

theorem :: BILINEAR:2

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

proof end;

theorem :: BILINEAR:3

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

proof end;

theorem :: BILINEAR:4

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

proof end;

theorem :: BILINEAR:5

for K being non empty right-distributive doubleLoopStr
for V, W being non empty VectSpStr of 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:6

for K being non empty left-distributive doubleLoopStr
for V, W being non empty VectSpStr of 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:7

for K being non empty associative doubleLoopStr
for V, W being non empty VectSpStr of 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:8

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

proof end;

Lm1: now

let K be non empty 1-sorted ; :: thesis: for V, W being non empty VectSpStr of K
for f being Form of V,W
for v being Element of the carrier of V
for y being Element of W holds
( (curry f) . v is Functional of W & (curry' f) . y is Functional of V )
let V, W be non empty VectSpStr of K; :: thesis: for f being Form of V,W
for v being Element of the carrier of V
for y being Element of W holds
( (curry f) . v is Functional of W & (curry' f) . y is Functional of V )
let f be Form of V,W; :: thesis: for v being Element of the carrier of V
for y being Element of W holds
( (curry f) . v is Functional of W & (curry' f) . y is Functional of V )
let v be Element of the carrier of V; :: thesis: for y being Element of W holds
( (curry f) . v is Functional of W & (curry' f) . y is Functional of V )
let y be Element of W; :: thesis: ( (curry f) . v is Functional of W & (curry' f) . y is Functional of V )
A1: dom f = [: the carrier of V, the carrier of W:] by FUNCT_2:def 1;
then consider g being Function such that
A2: (curry f) . v = g and
A3: ( dom g = the carrier of W & rng g c= rng f ) and
for y being set st y in the carrier of W holds
g . y = f . (v,y) by FUNCT_5:36;
reconsider g = g as Function of the carrier of W, the carrier of K by A3, FUNCT_2:4, XBOOLE_1:1;
g = (curry f) . v by A2;
hence (curry f) . v is Functional of W ; :: thesis: (curry' f) . y is Functional of V
consider h being Function such that
A4: (curry' f) . y = h and
A5: ( dom h = the carrier of V & rng h c= rng f ) and
for x being set st x in the carrier of V holds
h . x = f . (x,y) by A1, FUNCT_5:39;
reconsider h = h as Function of the carrier of V, the carrier of K by A5, FUNCT_2:4, XBOOLE_1:1;
h = (curry' f) . y by A4;
hence (curry' f) . y is Functional of V ; :: thesis: verum

end;

begin

definition

let K be non empty 1-sorted ;
let V, W be non empty VectSpStr of K;
let f be Form of V,W;
let v be Vector of V;
func FunctionalFAF (f,v) -> Functional of W equals :: BILINEAR:def 9
(curry f) . v;
correctness
coherence
(curry f) . v is Functional of W;
by Lm1;

end;

:: deftheorem defines FunctionalFAF BILINEAR:def 9 :
for K being non empty 1-sorted
for V, W being non empty VectSpStr of 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 of K;
let f be Form of V,W;
let w be Vector of W;
func FunctionalSAF (f,w) -> Functional of V equals :: BILINEAR:def 10
(curry' f) . w;
correctness
coherence
(curry' f) . w is Functional of V;
by Lm1;

end;

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

theorem Th9: :: BILINEAR:9

for K being non empty 1-sorted
for V, W being non empty VectSpStr of 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 Th10: :: BILINEAR:10

for K being non empty 1-sorted
for V, W being non empty VectSpStr of 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 Th11: :: BILINEAR:11

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

proof end;

theorem Th12: :: BILINEAR:12

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

proof end;

theorem Th13: :: BILINEAR:13

for K being non empty addLoopStr
for V, W being non empty VectSpStr of 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 Th14: :: BILINEAR:14

for K being non empty addLoopStr
for V, W being non empty VectSpStr of 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 Th15: :: BILINEAR:15

for K being non empty doubleLoopStr
for V, W being non empty VectSpStr of 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 Th16: :: BILINEAR:16

for K being non empty doubleLoopStr
for V, W being non empty VectSpStr of 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 Th17: :: BILINEAR:17

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

proof end;

theorem Th18: :: BILINEAR:18

for K being non empty addLoopStr
for V, W being non empty VectSpStr of 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:19

for K being non empty addLoopStr
for V, W being non empty VectSpStr of 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:20

for K being non empty addLoopStr
for V, W being non empty VectSpStr of 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;

begin

definition

let K be non empty multMagma ;
let V, W be non empty VectSpStr of K;
let f be Functional of V;
let g be Functional of W;
func FormFunctional (f,g) -> Form of V,W means :Def11: :: BILINEAR:def 11
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 Def11 defines FormFunctional BILINEAR:def 11 :
for K being non empty multMagma
for V, W being non empty VectSpStr of 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 Th21: :: BILINEAR:21

for K being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for V, W being non empty VectSpStr of 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 Th22: :: BILINEAR:22

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

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

proof end;

theorem :: BILINEAR:24

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

proof end;

theorem Th25: :: BILINEAR:25

for K being non empty multMagma
for V, W being non empty VectSpStr of 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 Th26: :: BILINEAR:26

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

begin

definition

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

end;

:: deftheorem Def12 defines additiveFAF BILINEAR:def 12 :
for K being non empty addLoopStr
for V, W being non empty VectSpStr of 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 Def13 defines additiveSAF BILINEAR:def 13 :
for K being non empty addLoopStr
for V, W being non empty VectSpStr of 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 of K;
let f be Form of V,W;
attr f is homogeneousFAF means :Def14: :: BILINEAR:def 14
for v being Vector of V holds FunctionalFAF (f,v) is homogeneous ;
attr f is homogeneousSAF means :Def15: :: BILINEAR:def 15
for w being Vector of W holds FunctionalSAF (f,w) is homogeneous ;

end;

:: deftheorem Def14 defines homogeneousFAF BILINEAR:def 14 :
for K being non empty multMagma
for V, W being non empty VectSpStr of 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 Def15 defines homogeneousSAF BILINEAR:def 15 :
for K being non empty multMagma
for V, W being non empty VectSpStr of 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 of 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 VectSpStr of K;
cluster non empty Relation-like [: the carrier of V, the carrier of W:] -defined the carrier of K -valued Function-like V17([: the carrier of V, the carrier of W:]) V18([: the carrier of V, the carrier of W:], the carrier of K) additiveFAF additiveSAF 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 VectSpStr of 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 VectSpStr of K;
cluster non empty Relation-like [: the carrier of V, the carrier of W:] -defined the carrier of K -valued Function-like V17([: the carrier of V, the carrier of W:]) V18([: the carrier of V, the carrier of W:], the carrier of K) additiveFAF additiveSAF homogeneousFAF homogeneousSAF 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 VectSpStr of 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 of 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 Def12;

end;

registration

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

end;

registration

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

end;

registration

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

end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr of 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 commutative right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr of 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 associative commutative right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr of 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 associative commutative right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr of 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 empty non trivial VectSpStr of K;
let W be non empty VectSpStr of 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 VectSpStr of K;
let W be non empty non trivial VectSpStr of 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 non constant 0-preserving Functional of V;
let g be non constant 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 V17([: the carrier of V, the carrier of W:]) V18([: the carrier of V, the carrier of W:], the carrier of K) additiveFAF additiveSAF homogeneousFAF homogeneousSAF 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 VectSpStr of 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 VectSpStr of 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 VectSpStr of 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 VectSpStr of 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 VectSpStr of 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 VectSpStr of 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 VectSpStr of 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 VectSpStr of 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 VectSpStr of 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 VectSpStr of 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 associative commutative right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr of 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 associative commutative right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr of 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 VectSpStr of 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 VectSpStr of 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 VectSpStr of 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 VectSpStr of K;
let f, g be homogeneousFAF Form of V,W;
cluster f - g -> homogeneousFAF ;
correctness
coherence
f - g is homogeneousFAF ;
;

end;

theorem Th27: :: BILINEAR:27

for K being non empty addLoopStr
for V, W being non empty VectSpStr of 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 Th28: :: BILINEAR:28

for K being non empty addLoopStr
for V, W being non empty VectSpStr of 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 Th29: :: BILINEAR:29

for K being non empty right_zeroed addLoopStr
for V, W being non empty VectSpStr of 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 Th30: :: BILINEAR:30

for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for V, W being non empty right_zeroed VectSpStr of 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 Th31: :: BILINEAR:31

for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for V, W being non empty right_zeroed VectSpStr of 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 Th32: :: BILINEAR:32

for K being non empty multMagma
for V, W being non empty VectSpStr of 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 Th33: :: BILINEAR:33

for K being non empty multMagma
for V, W being non empty VectSpStr of 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 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 of 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 Th35: :: BILINEAR:35

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 of 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 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, 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 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 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 Th38: :: BILINEAR:38

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

proof end;

theorem :: BILINEAR:39

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 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 :: BILINEAR:40

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

proof end;

theorem Th41: :: BILINEAR:41

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

begin

definition

let K be ZeroStr ;
let V, W be non empty VectSpStr of K;
let f be Form of V,W;
func leftker f -> Subset of V equals :: BILINEAR:def 16
{ v where v is Vector of V : for w 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 16 :
for K being ZeroStr
for V, W being non empty VectSpStr of 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 of K;
let f be Form of V,W;
func rightker f -> Subset of W equals :: BILINEAR:def 17
{ w where w is Vector of W : for v 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 17 :
for K being ZeroStr
for V, W being non empty VectSpStr of 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 of K;
let f be Form of V,V;
func diagker f -> Subset of V equals :: BILINEAR:def 18
{ v where v is Vector of V : f . (v,v) = 0. K } ;
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 18 :
for K being ZeroStr
for V being non empty VectSpStr of 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 of K;
let W be non empty VectSpStr of 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 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 of K;
let W be non empty VectSpStr of 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 VectSpStr of K;
let W be non empty right_zeroed VectSpStr of 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 associative well-unital distributive doubleLoopStr ;
let V be non empty VectSpStr of K;
let W be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr of 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 VectSpStr of 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 VectSpStr of 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 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 of 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 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 of 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:42

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

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 VectSpStr of K
for f being additiveSAF homogeneousSAF Form of V,W holds leftker f is linearly-closed

proof end;

theorem Th44: :: BILINEAR:44

for K being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for V, W being non empty VectSpStr of 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 associative well-unital distributive doubleLoopStr ;
let V be VectSp of K;
let W be non empty VectSpStr of K;
let f be additiveSAF homogeneousSAF Form of V,W;
func LKer f -> non empty strict Subspace of V means :Def19: :: BILINEAR:def 19
the carrier of it = leftker f;
existence
ex b₁ being non empty strict Subspace of V st the carrier of b₁ = leftker f by Th43, VECTSP_4:42;
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:37;

end;

:: deftheorem Def19 defines LKer BILINEAR:def 19 :
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 of 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 associative well-unital distributive doubleLoopStr ;
let V be non empty VectSpStr of 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 :Def20: :: BILINEAR:def 20
the carrier of it = rightker f;
existence
ex b₁ being non empty strict Subspace of W st the carrier of b₁ = rightker f by Th44, VECTSP_4:42;
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:37;

end;

:: deftheorem Def20 defines RKer BILINEAR:def 20 :
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being non empty VectSpStr of 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 associative well-unital distributive doubleLoopStr ;
let V be VectSp of K;
let W be non empty VectSpStr of K;
let f be additiveSAF homogeneousSAF Form of V,W;
func LQForm f -> additiveSAF homogeneousSAF Form of (VectQuot (V,(LKer f))),W means :Def21: :: BILINEAR:def 21
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 Def21 defines LQForm BILINEAR:def 21 :
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 of 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 associative well-unital distributive doubleLoopStr ;
let V be non empty VectSpStr of 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 :Def22: :: BILINEAR:def 22
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 Def22 defines RQForm BILINEAR:def 22 :
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being non empty VectSpStr of 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 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 )

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 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 :Def23: :: BILINEAR:def 23
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 Def23 defines QForm BILINEAR:def 23 :
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 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 Th45: :: BILINEAR:45

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 of K
for f being additiveSAF homogeneousSAF Form of V,W holds rightker f = rightker (LQForm f)

proof end;

theorem Th46: :: BILINEAR:46

for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being non empty VectSpStr of 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 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 RKer f = RKer (LQForm f)

proof end;

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 LKer f = LKer (RQForm f)

proof end;

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
( QForm f = RQForm (LQForm f) & QForm f = LQForm (RQForm f) )

proof end;

theorem Th50: :: BILINEAR:50

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

proof end;

theorem Th51: :: BILINEAR:51

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

proof end;

theorem Th52: :: BILINEAR:52

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 of 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 Th53: :: BILINEAR:53

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

proof end;

theorem Th54: :: BILINEAR:54

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 of 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 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 VectSp of K
for W being non empty VectSpStr of 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 Th56: :: BILINEAR:56

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 of K
for W being VectSp of K
for f being Functional of V
for g being linear-Functional of W st f <> 0Functional V holds
( RKer (FormFunctional (f,g)) = Ker g & RQForm (FormFunctional (f,g)) = FormFunctional (f,(CQFunctional g)) )

proof end;

theorem :: BILINEAR:57

for K being Field
for V, W being non trivial VectSp of K
for f being V14() linear-Functional of V
for g being V14() 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 VectSpStr of K;
let f be Form of V,W;
attr f is degenerated-on-left means :Def24: :: BILINEAR:def 24
leftker f <> {(0. V)};
attr f is degenerated-on-right means :Def25: :: BILINEAR:def 25
rightker f <> {(0. W)};

end;

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

:: deftheorem Def25 defines degenerated-on-right BILINEAR:def 25 :
for K being ZeroStr
for V, W being non empty VectSpStr of 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 of 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 associative well-unital distributive doubleLoopStr ;
let V be non empty right_zeroed VectSpStr of 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 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 & not QForm f is degenerated-on-right )

proof end;

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 & 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;

begin

definition

let K be 1-sorted ;
let V be VectSpStr of K;
let f be Form of V,V;
attr f is symmetric means :Def26: :: BILINEAR:def 26
for v, w being Vector of V holds f . (v,w) = f . (w,v);

end;

:: deftheorem Def26 defines symmetric BILINEAR:def 26 :
for K being 1-sorted
for V being VectSpStr of 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 of K;
let f be Form of V,V;
attr f is alternating means :Def27: :: BILINEAR:def 27
for v being Vector of V holds f . (v,v) = 0. K;

end;

:: deftheorem Def27 defines alternating BILINEAR:def 27 :
for K being ZeroStr
for V being VectSpStr of 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 of 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

proof end;

end;

registration

let K be non empty ZeroStr ;
let V be non empty VectSpStr of K;
cluster non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of K -valued Function-like V17([: the carrier of V, the carrier of V:]) V18([: the carrier of V, the carrier of V:], the carrier of K) symmetric 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 V17([: the carrier of V, the carrier of V:]) V18([: the carrier of V, the carrier of V:], the carrier of K) alternating 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 VectSpStr of K;
cluster non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of K -valued Function-like V17([: the carrier of V, the carrier of V:]) V18([: the carrier of V, the carrier of V:], the carrier of K) additiveFAF additiveSAF homogeneousFAF homogeneousSAF symmetric 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 V17([: the carrier of V, the carrier of V:]) V18([: the carrier of V, the carrier of V:], the carrier of K) additiveFAF additiveSAF homogeneousFAF homogeneousSAF alternating 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 V17([: the carrier of V, the carrier of V:]) V18([: the carrier of V, the carrier of V:], the carrier of K) additiveFAF additiveSAF homogeneousFAF homogeneousSAF symmetric 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 VectSpStr of K;
cluster non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of K -valued Function-like V17([: the carrier of V, the carrier of V:]) V18([: the carrier of V, the carrier of V:], the carrier of K) additiveFAF additiveSAF alternating 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 VectSpStr of 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 VectSpStr of 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 VectSpStr of 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 VectSpStr of 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 VectSpStr of 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 VectSpStr of 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 VectSpStr of 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 VectSpStr of K;
let f, g be alternating Form of V,V;
cluster f - g -> alternating ;
coherence
f - g is alternating ;

end;

theorem :: BILINEAR:58

for K being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for V being non empty VectSpStr of K
for f being symmetric bilinear-Form of V,V holds leftker f = rightker f

proof end;

theorem Th59: :: BILINEAR:59

for K being non empty right_complementable add-associative right_zeroed addLoopStr
for V being non empty VectSpStr of 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 VectSpStr of K;
let f be additiveFAF additiveSAF Form of V,V;
redefine attr f is alternating means :: BILINEAR:def 28
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 28 :
for K being Fanoian Field
for V being non empty VectSpStr of 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:60

for K being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for V being non empty VectSpStr of K
for f being alternating bilinear-Form of V,V holds leftker f = rightker f

proof end;