:: by Jaros{\l}aw Kotowicz

::

:: Received November 5, 2002

:: Copyright (c) 2002-2018 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;
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;

definition

let K be non empty ZeroStr ;

let V, W be ModuleStr over K;

[: the carrier of V, the carrier of W:] --> (0. K) is Form of V,W ;

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

[: the carrier of V, the carrier of W:] --> (0. K) is Form of V,W ;

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

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;

ex b_{1} being Form of V,W st

for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = (f . (v,w)) + (g . (v,w))

for b_{1}, b_{2} being Form of V,W st ( for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = (f . (v,w)) + (g . (v,w)) ) & ( for v being Vector of V

for w being Vector of W holds b_{2} . (v,w) = (f . (v,w)) + (g . (v,w)) ) holds

b_{1} = b_{2}

end;
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 for v being Vector of V

for w being Vector of W holds it . (v,w) = (f . (v,w)) + (g . (v,w));

ex b

for v being Vector of V

for w being Vector of W holds b

proof end;

uniqueness for b

for w being Vector of W holds b

for w being Vector of W holds b

b

proof 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_{6} being Form of V,W holds

( b_{6} = f + g iff for v being Vector of V

for w being Vector of W holds b_{6} . (v,w) = (f . (v,w)) + (g . (v,w)) );

for K being non empty addLoopStr

for V, W being non empty ModuleStr over K

for f, g, b

( b

for w being Vector of W holds b

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;

ex b_{1} being Form of V,W st

for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = a * (f . (v,w))

for b_{1}, b_{2} being Form of V,W st ( for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = a * (f . (v,w)) ) & ( for v being Vector of V

for w being Vector of W holds b_{2} . (v,w) = a * (f . (v,w)) ) holds

b_{1} = b_{2}

end;
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 for v being Vector of V

for w being Vector of W holds it . (v,w) = a * (f . (v,w));

ex b

for v being Vector of V

for w being Vector of W holds b

proof end;

uniqueness for b

for w being Vector of W holds b

for w being Vector of W holds b

b

proof 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_{6} being Form of V,W holds

( b_{6} = a * f iff for v being Vector of V

for w being Vector of W holds b_{6} . (v,w) = a * (f . (v,w)) );

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

( b

for w being Vector of W holds b

definition

let K be non empty addLoopStr ;

let V, W be non empty ModuleStr over K;

let f be Form of V,W;

ex b_{1} being Form of V,W st

for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = - (f . (v,w))

for b_{1}, b_{2} being Form of V,W st ( for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = - (f . (v,w)) ) & ( for v being Vector of V

for w being Vector of W holds b_{2} . (v,w) = - (f . (v,w)) ) holds

b_{1} = b_{2}

end;
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 for v being Vector of V

for w being Vector of W holds it . (v,w) = - (f . (v,w));

ex b

for v being Vector of V

for w being Vector of W holds b

proof end;

uniqueness for b

for w being Vector of W holds b

for w being Vector of W holds b

b

proof 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_{5} being Form of V,W holds

( b_{5} = - f iff for v being Vector of V

for w being Vector of W holds b_{5} . (v,w) = - (f . (v,w)) );

for K being non empty addLoopStr

for V, W being non empty ModuleStr over K

for f, b

( b

for w being Vector of W holds b

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;

compatibility

for b_{1} being Form of V,W holds

( b_{1} = - f iff b_{1} = (- (1. K)) * f )

end;
let V, W be non empty ModuleStr over K;

let f be Form of V,W;

compatibility

for b

( b

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

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;

correctness

coherence

f + (- g) is Form of V,W;

;

end;
let V, W be non empty ModuleStr over K;

let f, g be Form of V,W;

correctness

coherence

f + (- g) is Form of V,W;

;

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

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;

for b_{1} being Form of V,W holds

( b_{1} = f - g iff for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = (f . (v,w)) - (g . (v,w)) )

end;
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 v being Vector of V

for w being Vector of W holds it . (v,w) = (f . (v,w)) - (g . (v,w));

for b

( b

for w being Vector of W holds b

proof 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_{6} being Form of V,W holds

( b_{6} = f - g iff for v being Vector of V

for w being Vector of W holds b_{6} . (v,w) = (f . (v,w)) - (g . (v,w)) );

for K being non empty addLoopStr

for V, W being non empty ModuleStr over K

for f, g, b

( b

for w being Vector of W holds b

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

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

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

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)

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)

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)

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)

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)

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

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;

correctness

coherence

(curry f) . v is Functional of W;

;

end;
let V, W be non empty ModuleStr over K;

let f be Form of V,W;

let v be Vector of V;

correctness

coherence

(curry f) . v is Functional of W;

;

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

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;

correctness

coherence

(curry' f) . w is Functional of V;

;

end;
let V, W be non empty ModuleStr over K;

let f be Form of V,W;

let w be Vector of W;

correctness

coherence

(curry' f) . w is Functional of V;

;

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

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

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

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

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

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

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

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

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

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

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

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

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

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;

ex b_{1} being Form of V,W st

for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = (f . v) * (g . w)

for b_{1}, b_{2} being Form of V,W st ( for v being Vector of V

for w being Vector of W holds b_{1} . (v,w) = (f . v) * (g . w) ) & ( for v being Vector of V

for w being Vector of W holds b_{2} . (v,w) = (f . v) * (g . w) ) holds

b_{1} = b_{2}

end;
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 for v being Vector of V

for w being Vector of W holds it . (v,w) = (f . v) * (g . w);

ex b

for v being Vector of V

for w being Vector of W holds b

proof end;

uniqueness for b

for w being Vector of W holds b

for w being Vector of W holds b

b

proof 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_{6} being Form of V,W holds

( b_{6} = FormFunctional (f,g) iff for v being Vector of V

for w being Vector of W holds b_{6} . (v,w) = (f . v) * (g . w) );

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

( b

for w being Vector of W holds b

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

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

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)

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)

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

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

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;

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

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 ;

for w being Vector of W holds FunctionalSAF (f,w) is additive ;

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

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

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;

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

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 ;

for w being Vector of W holds FunctionalSAF (f,w) is homogeneous ;

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

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

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;

coherence

NulForm (V,W) is additiveFAF

NulForm (V,W) is additiveSAF

end;
let V, W be non empty ModuleStr over K;

coherence

NulForm (V,W) is additiveFAF

proof end;

coherence NulForm (V,W) is additiveSAF

proof end;

registration

let K be non empty right_zeroed addLoopStr ;

let V, W be non empty ModuleStr over K;

ex b_{1} being Form of V,W st

( b_{1} is additiveFAF & b_{1} is additiveSAF )

end;
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 Form of ,;

existence ex b

( b

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

coherence

NulForm (V,W) is homogeneousFAF

NulForm (V,W) is homogeneousSAF

end;
let V, W be non empty ModuleStr over K;

coherence

NulForm (V,W) is homogeneousFAF

proof end;

coherence NulForm (V,W) is homogeneousSAF

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

ex b_{1} being Form of V,W st

( b_{1} is additiveFAF & b_{1} is homogeneousFAF & b_{1} is additiveSAF & b_{1} is homogeneousSAF )

end;
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 Form of ,;

existence ex b

( b

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

mode bilinear-Form of V,W is additiveFAF additiveSAF homogeneousFAF homogeneousSAF Form of V,W;

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;

coherence

FunctionalFAF (f,v) is additive by Def11;

end;
let V, W be non empty ModuleStr over K;

let f be additiveFAF Form of V,W;

let v be Vector of V;

coherence

FunctionalFAF (f,v) is additive by Def11;

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;

coherence

FunctionalSAF (f,w) is additive by Def12;

end;
let V, W be non empty ModuleStr over K;

let f be additiveSAF Form of V,W;

let w be Vector of W;

coherence

FunctionalSAF (f,w) is additive by Def12;

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;

coherence

FunctionalFAF (f,v) is homogeneous by Def13;

end;
let V, W be non empty ModuleStr over K;

let f be homogeneousFAF Form of V,W;

let v be Vector of V;

coherence

FunctionalFAF (f,v) is homogeneous by Def13;

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;

coherence

FunctionalSAF (f,w) is homogeneous by Def14;

end;
let V, W be non empty ModuleStr over K;

let f be homogeneousSAF Form of V,W;

let w be Vector of W;

coherence

FunctionalSAF (f,w) is homogeneous by Def14;

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;

coherence

FormFunctional (f,g) is additiveFAF

end;
let V, W be non empty ModuleStr over K;

let f be Functional of V;

let g be additive Functional of W;

coherence

FormFunctional (f,g) is additiveFAF

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

coherence

FormFunctional (f,g) is additiveSAF

end;
let V, W be non empty ModuleStr over K;

let f be additive Functional of V;

let g be Functional of W;

coherence

FormFunctional (f,g) is additiveSAF

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

coherence

FormFunctional (f,g) is homogeneousFAF

end;
let V, W be non empty ModuleStr over K;

let f be Functional of V;

let g be homogeneous Functional of W;

coherence

FormFunctional (f,g) is homogeneousFAF

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

coherence

FormFunctional (f,g) is homogeneousSAF

end;
let V, W be non empty ModuleStr over K;

let f be homogeneous Functional of V;

let g be Functional of W;

coherence

FormFunctional (f,g) is homogeneousSAF

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

coherence

not FormFunctional (f,g) is trivial

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

coherence

not FormFunctional (f,g) is trivial

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

coherence

not FormFunctional (f,g) is trivial

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

coherence

not FormFunctional (f,g) is trivial

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

coherence

not FormFunctional (f,g) is constant

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

coherence

not FormFunctional (f,g) is constant

proof end;

registration

let K be Field;

let V, W be non trivial VectSp of K;

ex b_{1} being Form of V,W st

( not b_{1} is trivial & not b_{1} is constant & b_{1} is additiveFAF & b_{1} is homogeneousFAF & b_{1} is additiveSAF & b_{1} is homogeneousSAF )

end;
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 Form of ,;

existence ex b

( not b

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

correctness

coherence

f + g is additiveSAF ;

end;
let V, W be non empty ModuleStr over K;

let f, g be additiveSAF Form of V,W;

correctness

coherence

f + g is additiveSAF ;

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

correctness

coherence

f + g is additiveFAF ;

end;
let V, W be non empty ModuleStr over K;

let f, g be additiveFAF Form of V,W;

correctness

coherence

f + g is additiveFAF ;

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

correctness

coherence

a * f is additiveSAF ;

end;
let V, W be non empty ModuleStr over K;

let f be additiveSAF Form of V,W;

let a be Element of K;

correctness

coherence

a * f is additiveSAF ;

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

correctness

coherence

a * f is additiveFAF ;

end;
let V, W be non empty ModuleStr over K;

let f be additiveFAF Form of V,W;

let a be Element of K;

correctness

coherence

a * f is additiveFAF ;

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

correctness

coherence

- f is additiveSAF ;

end;
let V, W be non empty ModuleStr over K;

let f be additiveSAF Form of V,W;

correctness

coherence

- f is additiveSAF ;

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

correctness

coherence

- f is additiveFAF ;

end;
let V, W be non empty ModuleStr over K;

let f be additiveFAF Form of V,W;

correctness

coherence

- f is additiveFAF ;

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

correctness

coherence

f - g is additiveSAF ;

;

end;
let V, W be non empty ModuleStr over K;

let f, g be additiveSAF Form of V,W;

correctness

coherence

f - g is additiveSAF ;

;

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;

correctness

coherence

f - g is additiveFAF ;

;

end;
let V, W be non empty ModuleStr over K;

let f, g be additiveFAF Form of V,W;

correctness

coherence

f - g is additiveFAF ;

;

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;

correctness

coherence

f + g is homogeneousSAF ;

end;
let V, W be non empty ModuleStr over K;

let f, g be homogeneousSAF Form of V,W;

correctness

coherence

f + g is homogeneousSAF ;

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

correctness

coherence

f + g is homogeneousFAF ;

end;
let V, W be non empty ModuleStr over K;

let f, g be homogeneousFAF Form of V,W;

correctness

coherence

f + g is homogeneousFAF ;

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

correctness

coherence

a * f is homogeneousSAF ;

end;
let V, W be non empty ModuleStr over K;

let f be homogeneousSAF Form of V,W;

let a be Element of K;

correctness

coherence

a * f is homogeneousSAF ;

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

correctness

coherence

a * f is homogeneousFAF ;

end;
let V, W be non empty ModuleStr over K;

let f be homogeneousFAF Form of V,W;

let a be Element of K;

correctness

coherence

a * f is homogeneousFAF ;

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

correctness

coherence

- f is homogeneousSAF ;

end;
let V, W be non empty ModuleStr over K;

let f be homogeneousSAF Form of V,W;

correctness

coherence

- f is homogeneousSAF ;

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

correctness

coherence

- f is homogeneousFAF ;

end;
let V, W be non empty ModuleStr over K;

let f be homogeneousFAF Form of V,W;

correctness

coherence

- f is homogeneousFAF ;

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

correctness

coherence

f - g is homogeneousSAF ;

;

end;
let V, W be non empty ModuleStr over K;

let f, g be homogeneousSAF Form of V,W;

correctness

coherence

f - g is homogeneousSAF ;

;

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;

correctness

coherence

f - g is homogeneousFAF ;

;

end;
let V, W be non empty ModuleStr over K;

let f, g be homogeneousFAF Form of V,W;

correctness

coherence

f - g is homogeneousFAF ;

;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 )

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;

coherence

{ v where v is Vector of V : for w being Vector of W holds f . (v,w) = 0. K } is Subset of V;

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

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;

:: 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 } ;

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;

coherence

{ w where w is Vector of W : for v being Vector of V holds f . (v,w) = 0. K } is Subset of W;

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

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;

:: 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 } ;

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;

coherence

{ v where v is Vector of V : f . (v,v) = 0. K } is Subset of V;

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

coherence

{ v where v is Vector of V : f . (v,v) = 0. K } is Subset of V;

proof 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 } ;

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;

coherence

not leftker f is empty

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

coherence

not leftker f is empty

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

coherence

not leftker f is empty

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

coherence

not leftker f is empty

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

coherence

not rightker f is empty

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

coherence

not rightker f is empty

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

coherence

not rightker f is empty

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

coherence

not rightker f is empty

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

coherence

not diagker f is empty

end;
let V be non empty right_zeroed ModuleStr over K;

let f be additiveFAF Form of V,V;

coherence

not diagker f is empty

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

coherence

not diagker f is empty

end;
let V be non empty right_zeroed ModuleStr over K;

let f be additiveSAF Form of V,V;

coherence

not diagker f is empty

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

coherence

not diagker f is empty

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

coherence

not diagker f is empty

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

coherence

not diagker f is empty

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

coherence

not diagker f is empty

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

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

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

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;

ex b_{1} being non empty strict Subspace of V st the carrier of b_{1} = leftker f
by Th42, VECTSP_4:34;

uniqueness

for b_{1}, b_{2} being non empty strict Subspace of V st the carrier of b_{1} = leftker f & the carrier of b_{2} = leftker f holds

b_{1} = b_{2}
by VECTSP_4:29;

end;
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 the carrier of it = leftker f;

ex b

uniqueness

for b

b

:: 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_{5} being non empty strict Subspace of V holds

( b_{5} = LKer f iff the carrier of b_{5} = leftker f );

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

( b

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;

ex b_{1} being non empty strict Subspace of W st the carrier of b_{1} = rightker f
by Th43, VECTSP_4:34;

uniqueness

for b_{1}, b_{2} being non empty strict Subspace of W st the carrier of b_{1} = rightker f & the carrier of b_{2} = rightker f holds

b_{1} = b_{2}
by VECTSP_4:29;

end;
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 the carrier of it = rightker f;

ex b

uniqueness

for b

b

:: 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_{5} being non empty strict Subspace of W holds

( b_{5} = RKer f iff the carrier of b_{5} = rightker f );

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

( b

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;

ex b_{1} 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_{1} . (A,w) = f . (v,w)

for b_{1}, b_{2} 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_{1} . (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_{2} . (A,w) = f . (v,w) ) holds

b_{1} = b_{2}

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

ex b

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

proof end;

uniqueness for b

for w being Vector of W

for v being Vector of V st A = v + (LKer f) holds

b

for w being Vector of W

for v being Vector of V st A = v + (LKer f) holds

b

b

proof 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_{5} being additiveSAF homogeneousSAF Form of (VectQuot (V,(LKer f))),W holds

( b_{5} = 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_{5} . (A,w) = f . (v,w) );

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

( b

for w being Vector of W

for v being Vector of V st A = v + (LKer f) holds

b

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;

ex b_{1} 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_{1} . (v,A) = f . (v,w)

for b_{1}, b_{2} 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_{1} . (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_{2} . (v,A) = f . (v,w) ) holds

b_{1} = b_{2}

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

ex b

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

proof end;

uniqueness for b

for v being Vector of V

for w being Vector of W st A = w + (RKer f) holds

b

for v being Vector of V

for w being Vector of W st A = w + (RKer f) holds

b

b

proof 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_{5} being additiveFAF homogeneousFAF Form of V,(VectQuot (W,(RKer f))) holds

( b_{5} = 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_{5} . (v,A) = f . (v,w) );

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

( b

for v being Vector of V

for w being Vector of W st A = w + (RKer f) holds

b

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;

coherence

( LQForm f is additiveFAF & LQForm f is homogeneousFAF )

( RQForm f is additiveSAF & RQForm f is homogeneousSAF )

end;
let V, W be VectSp of K;

let f be bilinear-Form of V,W;

coherence

( LQForm f is additiveFAF & LQForm f is homogeneousFAF )

proof end;

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

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

ex b_{1} 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_{1} . (A,B) = f . (v,w)

for b_{1}, b_{2} 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_{1} . (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_{2} . (A,B) = f . (v,w) ) holds

b_{1} = b_{2}

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

ex b

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

proof end;

uniqueness for b

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

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

b

proof 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_{5} being bilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer f))) holds

( b_{5} = 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_{5} . (A,B) = f . (v,w) );

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

( b

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

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)

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)

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)

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)

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

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

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

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

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

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

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

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

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

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;

:: 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)} );

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

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;

coherence

not LQForm f is degenerated-on-left

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

coherence

not LQForm f is degenerated-on-left

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

coherence

not RQForm f is degenerated-on-right

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

coherence

not RQForm f is degenerated-on-right

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

coherence

( not QForm f is degenerated-on-left & not QForm f is degenerated-on-right )

end;
let V, W be VectSp of K;

let f be bilinear-Form of V,W;

coherence

( not QForm f is degenerated-on-left & not QForm f is degenerated-on-right )

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

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

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

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

registration

let K be Field;

let V, W be non trivial VectSp of K;

let f be non constant bilinear-Form of V,W;

coherence

not QForm f is constant

end;
let V, W be non trivial VectSp of K;

let f be non constant bilinear-Form of V,W;

coherence

not QForm f is constant

proof end;

:: Bilinear Symmetric and Alternating Forms

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

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;

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

for v being Vector of V holds f . (v,v) = 0. K;

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

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;

coherence

NulForm (V,V) is symmetric

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

end;
let V be non empty ModuleStr over K;

coherence

NulForm (V,V) is symmetric

proof end;

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

registration

let K be non empty ZeroStr ;

let V be non empty ModuleStr over K;

ex b_{1} being Form of V,V st b_{1} is symmetric

ex b_{1} being Form of V,V st b_{1} is alternating

end;
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 Form of ,;

existence ex b

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 Form of ,;

existence ex b

proof end;

registration

let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;

let V be non empty ModuleStr over K;

ex b_{1} being Form of V,V st

( b_{1} is symmetric & b_{1} is additiveFAF & b_{1} is homogeneousFAF & b_{1} is additiveSAF & b_{1} is homogeneousSAF )

ex b_{1} being Form of V,V st

( b_{1} is alternating & b_{1} is additiveFAF & b_{1} is homogeneousFAF & b_{1} is additiveSAF & b_{1} is homogeneousSAF )

end;
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 Form of ,;

existence ex b

( b

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 Form of ,;

existence ex b

( b

proof end;

registration

let K be Field;

let V be non trivial VectSp of K;

ex b_{1} being Form of V,V st

( b_{1} is symmetric & not b_{1} is trivial & not b_{1} is constant & b_{1} is additiveFAF & b_{1} is homogeneousFAF & b_{1} is additiveSAF & b_{1} is homogeneousSAF )

end;
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 Form of ,;

existence ex b

( b

proof end;

registration

let K be non empty right_complementable add-associative right_zeroed addLoopStr ;

let V be non empty ModuleStr over K;

ex b_{1} being Form of V,V st

( b_{1} is alternating & b_{1} is additiveFAF & b_{1} is additiveSAF )

end;
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 Form of ,;

existence ex b

( b

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

coherence

f + g is symmetric

end;
let V be non empty ModuleStr over K;

let f, g be symmetric Form of V,V;

coherence

f + g is symmetric

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

coherence

a * f is symmetric

end;
let V be non empty ModuleStr over K;

let f be symmetric Form of V,V;

let a be Element of K;

coherence

a * f is symmetric

proof end;

registration

let K be non empty addLoopStr ;

let V be non empty ModuleStr over K;

let f be symmetric Form of V,V;

coherence

- f is symmetric

end;
let V be non empty ModuleStr over K;

let f be symmetric Form of V,V;

coherence

- f is symmetric

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

coherence

f - g is symmetric ;

end;
let V be non empty ModuleStr over K;

let f, g be symmetric Form of V,V;

coherence

f - g is symmetric ;

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;

coherence

f + g is alternating

end;
let V be non empty ModuleStr over K;

let f, g be alternating Form of V,V;

coherence

f + g is alternating

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

coherence

a * f is alternating

end;
let V be non empty ModuleStr over K;

let f be alternating Form of V,V;

let a be Scalar of K;

coherence

a * f is alternating

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

coherence

- f is alternating

end;
let V be non empty ModuleStr over K;

let f be alternating Form of V,V;

coherence

- f is alternating

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

coherence

f - g is alternating ;

end;
let V be non empty ModuleStr over K;

let f, g be alternating Form of V,V;

coherence

f - g is alternating ;

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

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

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;

( f is alternating iff for v, w being Vector of V holds f . (v,w) = - (f . (w,v)) )

end;
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 for v, w being Vector of V holds f . (v,w) = - (f . (w,v));

( f is alternating iff for v, w being Vector of V holds f . (v,w) = - (f . (w,v)) )

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

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

for V being non empty ModuleStr over K

for f being alternating bilinear-Form of V,V holds leftker f = rightker f

proof end;