:: BILINEAR semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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 LoopStr ;
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 b1 being Form of V,W st
for v being Vector of V
for w being Vector of W holds b1 . [v,w] = (f . [v,w]) + (g . [v,w])
proof end;
uniqueness
for b1, b2 being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . [v,w] = (f . [v,w]) + (g . [v,w]) ) & ( for v being Vector of V
for w being Vector of W holds b2 . [v,w] = (f . [v,w]) + (g . [v,w]) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines + BILINEAR:def 3 :
for K being non empty LoopStr
for V, W being non empty VectSpStr of K
for f, g, b6 being Form of V,W holds
( b6 = f + g iff for v being Vector of V
for w being Vector of W holds b6 . [v,w] = (f . [v,w]) + (g . [v,w]) );

definition
let K be non empty HGrStr ;
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 b1 being Form of V,W st
for v being Vector of V
for w being Vector of W holds b1 . [v,w] = a * (f . [v,w])
proof end;
uniqueness
for b1, b2 being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . [v,w] = a * (f . [v,w]) ) & ( for v being Vector of V
for w being Vector of W holds b2 . [v,w] = a * (f . [v,w]) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines * BILINEAR:def 4 :
for K being non empty HGrStr
for V, W being non empty VectSpStr of K
for f being Form of V,W
for a being Element of K
for b6 being Form of V,W holds
( b6 = a * f iff for v being Vector of V
for w being Vector of W holds b6 . [v,w] = a * (f . [v,w]) );

definition
let K be non empty LoopStr ;
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 b1 being Form of V,W st
for v being Vector of V
for w being Vector of W holds b1 . [v,w] = - (f . [v,w])
proof end;
uniqueness
for b1, b2 being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . [v,w] = - (f . [v,w]) ) & ( for v being Vector of V
for w being Vector of W holds b2 . [v,w] = - (f . [v,w]) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines - BILINEAR:def 5 :
for K being non empty LoopStr
for V, W being non empty VectSpStr of K
for f, b5 being Form of V,W holds
( b5 = - f iff for v being Vector of V
for w being Vector of W holds b5 . [v,w] = - (f . [v,w]) );

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

:: deftheorem defines - BILINEAR:def 6 :
for K being non empty add-associative right_zeroed right_complementable 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 LoopStr ;
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 LoopStr
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 LoopStr ;
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 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]);
coherence
f - g is Form of V,W ;
compatibility
for b1 being Form of V,W holds
( b1 = f - g iff for v being Vector of V
for w being Vector of W holds b1 . [v,w] = (f . [v,w]) - (g . [v,w]) )
proof end;
end;

:: deftheorem Def8 defines - BILINEAR:def 8 :
for K being non empty LoopStr
for V, W being non empty VectSpStr of K
for f, g, b6 being Form of V,W holds
( b6 = f - g iff for v being Vector of V
for w being Vector of W holds b6 . [v,w] = (f . [v,w]) - (g . [v,w]) );

Lm1: now
let K be non empty Abelian LoopStr ; :: thesis: for V, W being non empty VectSpStr of K
for f, g being Form of V,W holds f + g = g + f
let V, W be non empty VectSpStr of K; :: thesis: for f, g being Form of V,W holds f + g = g + f
let f, g be Form of V,W; :: thesis: f + g = g + f
now
let v be Vector of V; :: thesis: for w being Vector of W holds (f + g) . [v,w] = (g + f) . [v,w]
let w be Vector of W; :: thesis: (f + g) . [v,w] = (g + f) . [v,w]
thus (f + g) . [v,w] = (f . [v,w]) + (g . [v,w]) by Def3
.= (g + f) . [v,w] by Def3 ; :: thesis: verum
end;
hence f + g = g + f by FUNCT_2:120; :: thesis: verum
end;

definition
let K be non empty Abelian LoopStr ;
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 by Lm1;
end;

theorem Th1: :: BILINEAR:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty ZeroStr
for V, W being non empty VectSpStr of K
for v being Vector of V
for w being Vector of W holds (NulForm V,W) . [v,w] = 0. K by FUNCOP_1:13;

theorem :: BILINEAR:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty right_zeroed LoopStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative LoopStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable LoopStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

Lm2: 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 & 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;
rng g c= the carrier of K by A2, XBOOLE_1:1;
then reconsider g = g as Function of the carrier of W,the carrier of K by A2, FUNCT_2:4;
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
A3: ( (curry' f) . y = h & 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;
rng h c= the carrier of K by A3, XBOOLE_1:1;
then reconsider h = h as Function of the carrier of V,the carrier of K by A3, FUNCT_2:4;
h = (curry' f) . y by A3;
hence (curry' f) . y is Functional of V ; :: thesis: verum
end;

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 Lm2;
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 Lm2;
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty LoopStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty LoopStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty LoopStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty LoopStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty LoopStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty LoopStr
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;

definition
let K be non empty HGrStr ;
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 b1 being Form of V,W st
for v being Vector of V
for w being Vector of W holds b1 . [v,w] = (f . v) * (g . w)
proof end;
uniqueness
for b1, b2 being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . [v,w] = (f . v) * (g . w) ) & ( for v being Vector of V
for w being Vector of W holds b2 . [v,w] = (f . v) * (g . w) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines FormFunctional BILINEAR:def 11 :
for K being non empty HGrStr
for V, W being non empty VectSpStr of K
for f being Functional of V
for g being Functional of W
for b6 being Form of V,W holds
( b6 = FormFunctional f,g iff for v being Vector of V
for w being Vector of W holds b6 . [v,w] = (f . v) * (g . w) );

theorem Th21: :: BILINEAR:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty HGrStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty commutative HGrStr
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;

definition
let K be non empty LoopStr ;
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 LoopStr
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 LoopStr
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 HGrStr ;
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 HGrStr
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 HGrStr
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 LoopStr ;
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 LoopStr ;
let V, W be non empty VectSpStr of K;
cluster additiveFAF additiveSAF Relation of [:the carrier of V,the carrier of W:],the carrier of K;
existence
ex b1 being Form of V,W st
( b1 is additiveFAF & b1 is additiveSAF )
proof end;
end;

registration
let K be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr of K;
cluster NulForm V,W -> additiveFAF additiveSAF homogeneousFAF ;
coherence
NulForm V,W is homogeneousFAF
proof end;
cluster NulForm V,W -> additiveFAF additiveSAF homogeneousSAF ;
coherence
NulForm V,W is homogeneousSAF
proof end;
end;

registration
let K be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr of K;
cluster additiveFAF additiveSAF homogeneousFAF homogeneousSAF Relation of [:the carrier of V,the carrier of W:],the carrier of K;
existence
ex b1 being Form of V,W st
( b1 is additiveFAF & b1 is homogeneousFAF & b1 is additiveSAF & b1 is homogeneousSAF )
proof end;
end;

definition
let K be non empty add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable 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 non trivial ;
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 constant non trivial additiveFAF additiveSAF homogeneousFAF homogeneousSAF Relation of [:the carrier of V,the carrier of W:],the carrier of K;
existence
ex b1 being Form of V,W st
( not b1 is trivial & not b1 is constant & b1 is additiveFAF & b1 is homogeneousFAF & b1 is additiveSAF & b1 is homogeneousSAF )
proof end;
end;

registration
let K be non empty Abelian add-associative right_zeroed LoopStr ;
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 LoopStr ;
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 Abelian add-associative right_zeroed right_complementable LoopStr ;
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 Abelian add-associative right_zeroed right_complementable LoopStr ;
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 Abelian add-associative right_zeroed right_complementable LoopStr ;
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 Abelian add-associative right_zeroed right_complementable LoopStr ;
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 add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty LoopStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty LoopStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty right_zeroed LoopStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty HGrStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty HGrStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V, W being non empty add-associative right_zeroed right_complementable VectSp-like 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V, W being non empty add-associative right_zeroed right_complementable VectSp-like 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V, W being non empty add-associative right_zeroed right_complementable VectSp-like 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable 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;

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 add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let V be non empty add-associative right_zeroed right_complementable VectSp-like 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 add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let V be non empty VectSpStr of K;
let W be non empty add-associative right_zeroed right_complementable VectSp-like 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 add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let V be non empty add-associative right_zeroed right_complementable VectSp-like 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 add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let V be non empty add-associative right_zeroed right_complementable VectSp-like 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable 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 lineary-closed
proof end;

theorem Th44: :: BILINEAR:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable 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 lineary-closed
proof end;

definition
let K be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 b1 being non empty strict Subspace of V st the carrier of b1 = leftker f
proof end;
uniqueness
for b1, b2 being non empty strict Subspace of V st the carrier of b1 = leftker f & the carrier of b2 = leftker f holds
b1 = b2 by VECTSP_4:37;
end;

:: deftheorem Def19 defines LKer BILINEAR:def 19 :
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 b5 being non empty strict Subspace of V holds
( b5 = LKer f iff the carrier of b5 = leftker f );

definition
let K be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 b1 being non empty strict Subspace of W st the carrier of b1 = rightker f
proof end;
uniqueness
for b1, b2 being non empty strict Subspace of W st the carrier of b1 = rightker f & the carrier of b2 = rightker f holds
b1 = b2 by VECTSP_4:37;
end;

:: deftheorem Def20 defines RKer BILINEAR:def 20 :
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 b5 being non empty strict Subspace of W holds
( b5 = RKer f iff the carrier of b5 = rightker f );

definition
let K be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 b1 being additiveSAF homogeneousSAF Form of (VectQuot V,(LKer f)),W st
for A being Vector of (VectQuot V,(LKer f))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
b1 . [A,w] = f . [v,w]
proof end;
uniqueness
for b1, b2 being additiveSAF homogeneousSAF Form of (VectQuot V,(LKer f)),W st ( for A being Vector of (VectQuot V,(LKer f))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
b1 . [A,w] = f . [v,w] ) & ( for A being Vector of (VectQuot V,(LKer f))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
b2 . [A,w] = f . [v,w] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def21 defines LQForm BILINEAR:def 21 :
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 b5 being additiveSAF homogeneousSAF Form of (VectQuot V,(LKer f)),W holds
( b5 = LQForm f iff for A being Vector of (VectQuot V,(LKer f))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
b5 . [A,w] = f . [v,w] );

definition
let K be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 b1 being additiveFAF homogeneousFAF Form of V,(VectQuot W,(RKer f)) st
for A being Vector of (VectQuot W,(RKer f))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
b1 . [v,A] = f . [v,w]
proof end;
uniqueness
for b1, b2 being additiveFAF homogeneousFAF Form of V,(VectQuot W,(RKer f)) st ( for A being Vector of (VectQuot W,(RKer f))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
b1 . [v,A] = f . [v,w] ) & ( for A being Vector of (VectQuot W,(RKer f))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
b2 . [v,A] = f . [v,w] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines RQForm BILINEAR:def 22 :
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 b5 being additiveFAF homogeneousFAF Form of V,(VectQuot W,(RKer f)) holds
( b5 = RQForm f iff for A being Vector of (VectQuot W,(RKer f))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
b5 . [v,A] = f . [v,w] );

registration
let K be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 b1 being bilinear-Form of (VectQuot V,(LKer f)),(VectQuot W,(RKer f)) st
for A being Vector of (VectQuot V,(LKer f))
for B being Vector of (VectQuot W,(RKer f))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
b1 . [A,B] = f . [v,w]
proof end;
uniqueness
for b1, b2 being bilinear-Form of (VectQuot V,(LKer f)),(VectQuot W,(RKer f)) st ( for A being Vector of (VectQuot V,(LKer f))
for B being Vector of (VectQuot W,(RKer f))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
b1 . [A,B] = f . [v,w] ) & ( for A being Vector of (VectQuot V,(LKer f))
for B being Vector of (VectQuot W,(RKer f))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
b2 . [A,B] = f . [v,w] ) holds
b1 = b2
proof end;
end;

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

theorem Th45: :: BILINEAR:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V, W being non trivial VectSp of K
for f being V126 linear-Functional of V
for g being V126 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 Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let V, W be VectSp of K;
let f be bilinear-Form of V,W;
cluster RQForm (LQForm f) -> additiveFAF additiveSAF homogeneousFAF homogeneousSAF 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) -> additiveFAF additiveSAF homogeneousFAF 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 non degenerated-on-left non degenerated-on-right ;
coherence
not QForm f is constant
proof end;
end;

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 symmetric Relation of [:the carrier of V,the carrier of V:],the carrier of K;
existence
ex b1 being Form of V,V st b1 is symmetric
proof end;
cluster alternating Relation of [:the carrier of V,the carrier of V:],the carrier of K;
existence
ex b1 being Form of V,V st b1 is alternating
proof end;
end;

registration
let K be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let V be non empty VectSpStr of K;
cluster additiveFAF additiveSAF homogeneousFAF homogeneousSAF symmetric Relation of [:the carrier of V,the carrier of V:],the carrier of K;
existence
ex b1 being Form of V,V st
( b1 is symmetric & b1 is additiveFAF & b1 is homogeneousFAF & b1 is additiveSAF & b1 is homogeneousSAF )
proof end;
cluster additiveFAF additiveSAF homogeneousFAF homogeneousSAF alternating Relation of [:the carrier of V,the carrier of V:],the carrier of K;
existence
ex b1 being Form of V,V st
( b1 is alternating & b1 is additiveFAF & b1 is homogeneousFAF & b1 is additiveSAF & b1 is homogeneousSAF )
proof end;
end;

registration
let K be Field;
let V be non trivial VectSp of K;
cluster non constant non trivial additiveFAF additiveSAF homogeneousFAF homogeneousSAF symmetric Relation of [:the carrier of V,the carrier of V:],the carrier of K;
existence
ex b1 being Form of V,V st
( b1 is symmetric & not b1 is trivial & not b1 is constant & b1 is additiveFAF & b1 is homogeneousFAF & b1 is additiveSAF & b1 is homogeneousSAF )
proof end;
end;

registration
let K be non empty add-associative right_zeroed right_complementable LoopStr ;
let V be non empty VectSpStr of K;
cluster additiveFAF additiveSAF alternating Relation of [:the carrier of V,the carrier of V:],the carrier of K;
existence
ex b1 being Form of V,V st
( b1 is alternating & b1 is additiveFAF & b1 is additiveSAF )
proof end;
end;

registration
let K be non empty LoopStr ;
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 LoopStr ;
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 LoopStr ;
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 LoopStr ;
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 add-associative right_zeroed right_complementable 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 add-associative right_zeroed right_complementable LoopStr ;
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 add-associative right_zeroed right_complementable LoopStr ;
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable LoopStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable 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;