:: BILINEAR semantic presentation

definition

let c₁ be 1-sorted ;
let c₂, c₃ be VectSpStr of c₁;
mode Form of a₂,a₃ is Function of [:the carrier of a₂,the carrier of a₃:],the carrier of a₁;

end;

definition

let c₁ be non empty ZeroStr ;
let c₂, c₃ be VectSpStr of c₁;
canceled;
func NulForm c₂,c₃ -> Form of a₂,a₃ equals :: BILINEAR:def 2
[:the carrier of a₂,the carrier of a₃:] --> (0. a₁);
coherence ;

end;

:: deftheorem Def1 BILINEAR:def 1 :

:: deftheorem Def2 defines NulForm BILINEAR:def 2 :

definition

let c₁ be non empty LoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄, c₅ be Form of c₂,c₃;
func c₄ + c₅ -> Form of a₂,a₃ means :Def3: :: BILINEAR:def 3
for b₁ being Vector of a₂
for b₂ being Vector of a₃ holds a₆ . [b₁,b₂] = (a₄ . [b₁,b₂]) + (a₅ . [b₁,b₂]);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines + BILINEAR:def 3 :

definition

let c₁ be non empty HGrStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be Form of c₂,c₃;
let c₅ be Element of c₁;
func c₅ * c₄ -> Form of a₂,a₃ means :Def4: :: BILINEAR:def 4
for b₁ being Vector of a₂
for b₂ being Vector of a₃ holds a₆ . [b₁,b₂] = a₅ * (a₄ . [b₁,b₂]);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines * BILINEAR:def 4 :

definition

let c₁ be non empty LoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be Form of c₂,c₃;
func - c₄ -> Form of a₂,a₃ means :Def5: :: BILINEAR:def 5
for b₁ being Vector of a₂
for b₂ being Vector of a₃ holds a₅ . [b₁,b₂] = - (a₄ . [b₁,b₂]);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines - BILINEAR:def 5 :

definition

let c₁ be non empty add-associative right_zeroed right_complementable left-distributive left_unital doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be Form of c₂,c₃;
redefine func - as - c₄ -> Form of a₂,a₃ equals :: BILINEAR:def 6
(- (1. a₁)) * a₄;
coherence ;
compatibility

proof end;

end;

:: deftheorem Def6 defines - BILINEAR:def 6 :

definition

let c₁ be non empty LoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄, c₅ be Form of c₂,c₃;
func c₄ - c₅ -> Form of a₂,a₃ equals :: BILINEAR:def 7
a₄ + (- a₅);
correctness ;

end;

:: deftheorem Def7 defines - BILINEAR:def 7 :

definition

let c₁ be non empty LoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄, c₅ be Form of c₂,c₃;
redefine func - as c₄ - c₅ -> Form of a₂,a₃ means :Def8: :: BILINEAR:def 8
for b₁ being Vector of a₂
for b₂ being Vector of a₃ holds a₆ . [b₁,b₂] = (a₄ . [b₁,b₂]) - (a₅ . [b₁,b₂]);
coherence ;
compatibility

proof end;

end;

:: deftheorem Def8 defines - BILINEAR:def 8 :

E5: now

let c₁ be non empty Abelian LoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄, c₅ be Form of c₂,c₃;

now

let c₆ be Vector of c₂;
let c₇ be Vector of c₃;
thus (c₄ + c₅) . [c₆,c₇] = (c₄ . [c₆,c₇]) + (c₅ . [c₆,c₇]) by Def3
.= (c₅ + c₄) . [c₆,c₇] by Def3 ;

end;

hence c₄ + c₅ = c₅ + c₄ by FUNCT_2:120;

end;

definition

let c₁ be non empty Abelian LoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄, c₅ be Form of c₂,c₃;
redefine func + as c₄ + c₅ -> Form of a₂,a₃;
commutativity by Lemma5;

end;

theorem Th1: :: BILINEAR:1

for b₁ being non empty ZeroStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Vector of b₂
for b₅ being Vector of b₃ holds (NulForm b₂,b₃) . [b₄,b₅] = 0. b₁ by FUNCOP_1:13;

theorem Th2: :: BILINEAR:2

for b₁ being non empty right_zeroed LoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Form of b₂,b₃ holds b₄ + (NulForm b₂,b₃) = b₄

proof end;

theorem Th3: :: BILINEAR:3

for b₁ being non empty add-associative LoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄, b₅, b₆ being Form of b₂,b₃ holds (b₄ + b₅) + b₆ = b₄ + (b₅ + b₆)

proof end;

theorem Th4: :: BILINEAR:4

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Form of b₂,b₃ holds b₄ - b₄ = NulForm b₂,b₃

proof end;

theorem Th5: :: BILINEAR:5

for b₁ being non empty right-distributive doubleLoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Element of b₁
for b₅, b₆ being Form of b₂,b₃ holds b₄ * (b₅ + b₆) = (b₄ * b₅) + (b₄ * b₆)

proof end;

theorem Th6: :: BILINEAR:6

for b₁ being non empty left-distributive doubleLoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄, b₅ being Element of b₁
for b₆ being Form of b₂,b₃ holds (b₄ + b₅) * b₆ = (b₄ * b₆) + (b₅ * b₆)

proof end;

theorem Th7: :: BILINEAR:7

for b₁ being non empty associative doubleLoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄, b₅ being Element of b₁
for b₆ being Form of b₂,b₃ holds (b₄ * b₅) * b₆ = b₄ * (b₅ * b₆)

proof end;

theorem Th8: :: BILINEAR:8

for b₁ being non empty left_unital doubleLoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Form of b₂,b₃ holds (1. b₁) * b₄ = b₄

proof end;

E7: now

let c₁ be non empty 1-sorted ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be Form of c₂,c₃;
let c₅ be Element of the carrier of c₂;
let c₆ be Element of c₃;
E8: dom c₄ = [:the carrier of c₂,the carrier of c₃:] by FUNCT_2:def 1;
then consider c₇ being Function such that
E9: ( (curry c₄) . c₅ = c₇ & dom c₇ = the carrier of c₃ & rng c₇ c= rng c₄ ) and
for b₁ being set st b₁ in the carrier of c₃ holds
c₇ . b₁ = c₄ . [c₅,b₁] by FUNCT_5:36;
rng c₇ c= the carrier of c₁ by E9, XBOOLE_1:1;
then reconsider c₈ = c₇ as Function of the carrier of c₃,the carrier of c₁ by E9, FUNCT_2:4;
c₈ = (curry c₄) . c₅ by E9;
hence (curry c₄) . c₅ is Functional of c₃ ;
consider c₉ being Function such that
E10: ( (curry' c₄) . c₆ = c₉ & dom c₉ = the carrier of c₂ & rng c₉ c= rng c₄ ) and
for b₁ being set st b₁ in the carrier of c₂ holds
c₉ . b₁ = c₄ . [b₁,c₆] by E8, FUNCT_5:39;
rng c₉ c= the carrier of c₁ by E10, XBOOLE_1:1;
then reconsider c₁₀ = c₉ as Function of the carrier of c₂,the carrier of c₁ by E10, FUNCT_2:4;
c₁₀ = (curry' c₄) . c₆ by E10;
hence (curry' c₄) . c₆ is Functional of c₂ ;

end;

definition

let c₁ be non empty 1-sorted ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be Form of c₂,c₃;
let c₅ be Vector of c₂;
func FunctionalFAF c₄,c₅ -> Functional of a₃ equals :: BILINEAR:def 9
(curry a₄) . a₅;
correctness by Lemma7;

end;

:: deftheorem Def9 defines FunctionalFAF BILINEAR:def 9 :

definition

let c₁ be non empty 1-sorted ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be Form of c₂,c₃;
let c₅ be Vector of c₃;
func FunctionalSAF c₄,c₅ -> Functional of a₂ equals :: BILINEAR:def 10
(curry' a₄) . a₅;
correctness by Lemma7;

end;

:: deftheorem Def10 defines FunctionalSAF BILINEAR:def 10 :

theorem Th9: :: BILINEAR:9

for b₁ being non empty 1-sorted
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Form of b₂,b₃
for b₅ being Vector of b₂ holds
( dom (FunctionalFAF b₄,b₅) = the carrier of b₃ & rng (FunctionalFAF b₄,b₅) c= the carrier of b₁ & ( for b₆ being Vector of b₃ holds (FunctionalFAF b₄,b₅) . b₆ = b₄ . [b₅,b₆] ) )

proof end;

theorem Th10: :: BILINEAR:10

for b₁ being non empty 1-sorted
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Form of b₂,b₃
for b₅ being Vector of b₃ holds
( dom (FunctionalSAF b₄,b₅) = the carrier of b₂ & rng (FunctionalSAF b₄,b₅) c= the carrier of b₁ & ( for b₆ being Vector of b₂ holds (FunctionalSAF b₄,b₅) . b₆ = b₄ . [b₆,b₅] ) )

proof end;

theorem Th11: :: BILINEAR:11

for b₁ being non empty ZeroStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Vector of b₂ holds FunctionalFAF (NulForm b₂,b₃),b₄ = 0Functional b₃

proof end;

theorem Th12: :: BILINEAR:12

for b₁ being non empty ZeroStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Vector of b₃ holds FunctionalSAF (NulForm b₂,b₃),b₄ = 0Functional b₂

proof end;

theorem Th13: :: BILINEAR:13

for b₁ being non empty LoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄, b₅ being Form of b₂,b₃
for b₆ being Vector of b₃ holds FunctionalSAF (b₄ + b₅),b₆ = (FunctionalSAF b₄,b₆) + (FunctionalSAF b₅,b₆)

proof end;

theorem Th14: :: BILINEAR:14

for b₁ being non empty LoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄, b₅ being Form of b₂,b₃
for b₆ being Vector of b₂ holds FunctionalFAF (b₄ + b₅),b₆ = (FunctionalFAF b₄,b₆) + (FunctionalFAF b₅,b₆)

proof end;

theorem Th15: :: BILINEAR:15

for b₁ being non empty doubleLoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Form of b₂,b₃
for b₅ being Element of b₁
for b₆ being Vector of b₃ holds FunctionalSAF (b₅ * b₄),b₆ = b₅ * (FunctionalSAF b₄,b₆)

proof end;

theorem Th16: :: BILINEAR:16

for b₁ being non empty doubleLoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Form of b₂,b₃
for b₅ being Element of b₁
for b₆ being Vector of b₂ holds FunctionalFAF (b₅ * b₄),b₆ = b₅ * (FunctionalFAF b₄,b₆)

proof end;

theorem Th17: :: BILINEAR:17

for b₁ being non empty LoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Form of b₂,b₃
for b₅ being Vector of b₃ holds FunctionalSAF (- b₄),b₅ = - (FunctionalSAF b₄,b₅)

proof end;

theorem Th18: :: BILINEAR:18

for b₁ being non empty LoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Form of b₂,b₃
for b₅ being Vector of b₂ holds FunctionalFAF (- b₄),b₅ = - (FunctionalFAF b₄,b₅)

proof end;

theorem Th19: :: BILINEAR:19

for b₁ being non empty LoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄, b₅ being Form of b₂,b₃
for b₆ being Vector of b₃ holds FunctionalSAF (b₄ - b₅),b₆ = (FunctionalSAF b₄,b₆) - (FunctionalSAF b₅,b₆)

proof end;

theorem Th20: :: BILINEAR:20

for b₁ being non empty LoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄, b₅ being Form of b₂,b₃
for b₆ being Vector of b₂ holds FunctionalFAF (b₄ - b₅),b₆ = (FunctionalFAF b₄,b₆) - (FunctionalFAF b₅,b₆)

proof end;

definition

let c₁ be non empty HGrStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be Functional of c₂;
let c₅ be Functional of c₃;
func FormFunctional c₄,c₅ -> Form of a₂,a₃ means :Def11: :: BILINEAR:def 11
for b₁ being Vector of a₂
for b₂ being Vector of a₃ holds a₆ . [b₁,b₂] = (a₄ . b₁) * (a₅ . b₂);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines FormFunctional BILINEAR:def 11 :

theorem Th21: :: BILINEAR:21

for b₁ being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Functional of b₂
for b₅ being Vector of b₂
for b₆ being Vector of b₃ holds (FormFunctional b₄,(0Functional b₃)) . [b₅,b₆] = 0. b₁

proof end;

theorem Th22: :: BILINEAR:22

for b₁ being non empty add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Functional of b₃
for b₅ being Vector of b₂
for b₆ being Vector of b₃ holds (FormFunctional (0Functional b₂),b₄) . [b₅,b₆] = 0. b₁

proof end;

theorem Th23: :: BILINEAR:23

for b₁ being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Functional of b₂ holds FormFunctional b₄,(0Functional b₃) = NulForm b₂,b₃

proof end;

theorem Th24: :: BILINEAR:24

for b₁ being non empty add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Functional of b₃ holds FormFunctional (0Functional b₂),b₄ = NulForm b₂,b₃

proof end;

theorem Th25: :: BILINEAR:25

for b₁ being non empty HGrStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Functional of b₂
for b₅ being Functional of b₃
for b₆ being Vector of b₂ holds FunctionalFAF (FormFunctional b₄,b₅),b₆ = (b₄ . b₆) * b₅

proof end;

theorem Th26: :: BILINEAR:26

for b₁ being non empty commutative HGrStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Functional of b₂
for b₅ being Functional of b₃
for b₆ being Vector of b₃ holds FunctionalSAF (FormFunctional b₄,b₅),b₆ = (b₅ . b₆) * b₄

proof end;

definition

let c₁ be non empty LoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be Form of c₂,c₃;
attr a₄ is additiveFAF means :Def12: :: BILINEAR:def 12
for b₁ being Vector of a₂ holds FunctionalFAF a₄,b₁ is additive;
attr a₄ is additiveSAF means :Def13: :: BILINEAR:def 13
for b₁ being Vector of a₃ holds FunctionalSAF a₄,b₁ is additive;

end;

:: deftheorem Def12 defines additiveFAF BILINEAR:def 12 :

:: deftheorem Def13 defines additiveSAF BILINEAR:def 13 :

definition

let c₁ be non empty HGrStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be Form of c₂,c₃;
attr a₄ is homogeneousFAF means :Def14: :: BILINEAR:def 14
for b₁ being Vector of a₂ holds FunctionalFAF a₄,b₁ is homogeneous;
attr a₄ is homogeneousSAF means :Def15: :: BILINEAR:def 15
for b₁ being Vector of a₃ holds FunctionalSAF a₄,b₁ is homogeneous;

end;

:: deftheorem Def14 defines homogeneousFAF BILINEAR:def 14 :

:: deftheorem Def15 defines homogeneousSAF BILINEAR:def 15 :

registration

let c₁ be non empty right_zeroed LoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
cluster NulForm a₂,a₃ -> additiveFAF ;
coherence

proof end;

cluster NulForm a₂,a₃ -> additiveSAF ;
coherence

proof end;

end;

registration

let c₁ be non empty right_zeroed LoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
cluster additiveFAF additiveSAF Relation of [:the carrier of a₂,the carrier of a₃:],the carrier of a₁;
existence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
cluster NulForm a₂,a₃ -> additiveFAF additiveSAF homogeneousFAF ;
coherence

proof end;

cluster NulForm a₂,a₃ -> additiveFAF additiveSAF homogeneousSAF ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
cluster additiveFAF additiveSAF homogeneousFAF homogeneousSAF Relation of [:the carrier of a₂,the carrier of a₃:],the carrier of a₁;
existence

proof end;

end;

definition

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
mode bilinear-Form of a₂,a₃ is additiveFAF additiveSAF homogeneousFAF homogeneousSAF Form of a₂,a₃;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be additiveFAF Form of c₂,c₃;
let c₅ be Vector of c₂;
cluster FunctionalFAF a₄,a₅ -> additive ;
coherence by Def12;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be additiveSAF Form of c₂,c₃;
let c₅ be Vector of c₃;
cluster FunctionalSAF a₄,a₅ -> additive ;
coherence by Def13;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be homogeneousFAF Form of c₂,c₃;
let c₅ be Vector of c₂;
cluster FunctionalFAF a₄,a₅ -> homogeneous ;
coherence by Def14;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be homogeneousSAF Form of c₂,c₃;
let c₅ be Vector of c₃;
cluster FunctionalSAF a₄,a₅ -> homogeneous ;
coherence by Def15;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be Functional of c₂;
let c₅ be additive Functional of c₃;
cluster FormFunctional a₄,a₅ -> additiveFAF ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable commutative right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be additive Functional of c₂;
let c₅ be Functional of c₃;
cluster FormFunctional a₄,a₅ -> additiveSAF ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable associative commutative right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be Functional of c₂;
let c₅ be homogeneous Functional of c₃;
cluster FormFunctional a₄,a₅ -> homogeneousFAF ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable associative commutative right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be homogeneous Functional of c₂;
let c₅ be Functional of c₃;
cluster FormFunctional a₄,a₅ -> homogeneousSAF ;
coherence

proof end;

end;

registration

let c₁ be non empty non degenerated doubleLoopStr ;
let c₂ be non empty non trivial VectSpStr of c₁;
let c₃ be non empty VectSpStr of c₁;
let c₄ be Functional of c₂;
let c₅ be Functional of c₃;
cluster FormFunctional a₄,a₅ -> non trivial ;
coherence

proof end;

end;

registration

let c₁ be non empty non degenerated doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be non empty non trivial VectSpStr of c₁;
let c₄ be Functional of c₂;
let c₅ be Functional of c₃;
cluster FormFunctional a₄,a₅ -> non trivial ;
coherence

proof end;

end;

registration

let c₁ be Field;
let c₂, c₃ be non trivial VectSp of c₁;
let c₄ be non constant 0-preserving Functional of c₂;
let c₅ be non constant 0-preserving Functional of c₃;
cluster FormFunctional a₄,a₅ -> non constant non trivial ;
coherence

proof end;

end;

registration

let c₁ be Field;
let c₂, c₃ be non trivial VectSp of c₁;
cluster non constant non trivial additiveFAF additiveSAF homogeneousFAF homogeneousSAF Relation of [:the carrier of a₂,the carrier of a₃:],the carrier of a₁;
existence

proof end;

end;

registration

let c₁ be non empty Abelian add-associative right_zeroed LoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄, c₅ be additiveSAF Form of c₂,c₃;
cluster a₄ + a₅ -> additiveSAF ;
correctness

proof end;

end;

registration

let c₁ be non empty Abelian add-associative right_zeroed LoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄, c₅ be additiveFAF Form of c₂,c₃;
cluster a₄ + a₅ -> additiveFAF ;
correctness

proof end;

end;

registration

let c₁ be non empty right_zeroed right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be additiveSAF Form of c₂,c₃;
let c₅ be Element of c₁;
cluster a₅ * a₄ -> additiveSAF ;
correctness

proof end;

end;

registration

let c₁ be non empty right_zeroed right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be additiveFAF Form of c₂,c₃;
let c₅ be Element of c₁;
cluster a₅ * a₄ -> additiveFAF ;
correctness

proof end;

end;

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable LoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be additiveSAF Form of c₂,c₃;
cluster - a₄ -> additiveSAF ;
correctness

proof end;

end;

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable LoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be additiveFAF Form of c₂,c₃;
cluster - a₄ -> additiveFAF ;
correctness

proof end;

end;

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable LoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄, c₅ be additiveSAF Form of c₂,c₃;
cluster a₄ - a₅ -> additiveSAF ;
correctness ;

end;

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable LoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄, c₅ be additiveFAF Form of c₂,c₃;
cluster a₄ - a₅ -> additiveFAF ;
correctness ;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄, c₅ be homogeneousSAF Form of c₂,c₃;
cluster a₄ + a₅ -> homogeneousSAF ;
correctness

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄, c₅ be homogeneousFAF Form of c₂,c₃;
cluster a₄ + a₅ -> homogeneousFAF ;
correctness

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable associative commutative right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be homogeneousSAF Form of c₂,c₃;
let c₅ be Element of c₁;
cluster a₅ * a₄ -> homogeneousSAF ;
correctness

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable associative commutative right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be homogeneousFAF Form of c₂,c₃;
let c₅ be Element of c₁;
cluster a₅ * a₄ -> homogeneousFAF ;
correctness

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be homogeneousSAF Form of c₂,c₃;
cluster - a₄ -> homogeneousSAF ;
correctness

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be homogeneousFAF Form of c₂,c₃;
cluster - a₄ -> homogeneousFAF ;
correctness

proof end;

end;

registration

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄, c₅ be homogeneousFAF Form of c₂,c₃;
cluster a₄ - a₅ -> homogeneousFAF ;
correctness ;

end;

theorem Th27: :: BILINEAR:27

for b₁ being non empty LoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄, b₅ being Vector of b₂
for b₆ being Vector of b₃
for b₇ being Form of b₂,b₃ st b₇ is additiveSAF holds
b₇ . [(b₄ + b₅),b₆] = (b₇ . [b₄,b₆]) + (b₇ . [b₅,b₆])

proof end;

theorem Th28: :: BILINEAR:28

for b₁ being non empty LoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Vector of b₂
for b₅, b₆ being Vector of b₃
for b₇ being Form of b₂,b₃ st b₇ is additiveFAF holds
b₇ . [b₄,(b₅ + b₆)] = (b₇ . [b₄,b₅]) + (b₇ . [b₄,b₆])

proof end;

theorem Th29: :: BILINEAR:29

for b₁ being non empty right_zeroed LoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄, b₅ being Vector of b₂
for b₆, b₇ being Vector of b₃
for b₈ being additiveFAF additiveSAF Form of b₂,b₃ holds b₈ . [(b₄ + b₅),(b₆ + b₇)] = ((b₈ . [b₄,b₆]) + (b₈ . [b₄,b₇])) + ((b₈ . [b₅,b₆]) + (b₈ . [b₅,b₇]))

proof end;

theorem Th30: :: BILINEAR:30

for b₁ being non empty add-associative right_zeroed right_complementable doubleLoopStr
for b₂, b₃ being non empty right_zeroed VectSpStr of b₁
for b₄ being additiveFAF Form of b₂,b₃
for b₅ being Vector of b₂ holds b₄ . [b₅,(0. b₃)] = 0. b₁

proof end;

theorem Th31: :: BILINEAR:31

for b₁ being non empty add-associative right_zeroed right_complementable doubleLoopStr
for b₂, b₃ being non empty right_zeroed VectSpStr of b₁
for b₄ being additiveSAF Form of b₂,b₃
for b₅ being Vector of b₃ holds b₄ . [(0. b₂),b₅] = 0. b₁

proof end;

theorem Th32: :: BILINEAR:32

for b₁ being non empty HGrStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Vector of b₂
for b₅ being Vector of b₃
for b₆ being Element of b₁
for b₇ being Form of b₂,b₃ st b₇ is homogeneousSAF holds
b₇ . [(b₆ * b₄),b₅] = b₆ * (b₇ . [b₄,b₅])

proof end;

theorem Th33: :: BILINEAR:33

for b₁ being non empty HGrStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Vector of b₂
for b₅ being Vector of b₃
for b₆ being Element of b₁
for b₇ being Form of b₂,b₃ st b₇ is homogeneousFAF holds
b₇ . [b₄,(b₆ * b₅)] = b₆ * (b₇ . [b₄,b₅])

proof end;

theorem Th34: :: BILINEAR:34

proof end;

theorem Th35: :: BILINEAR:35

proof end;

theorem Th36: :: BILINEAR:36

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂, b₃ being VectSp of b₁
for b₄, b₅ being Vector of b₂
for b₆ being Vector of b₃
for b₇ being additiveSAF homogeneousSAF Form of b₂,b₃ holds b₇ . [(b₄ - b₅),b₆] = (b₇ . [b₄,b₆]) - (b₇ . [b₅,b₆])

proof end;

theorem Th37: :: BILINEAR:37

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂, b₃ being VectSp of b₁
for b₄ being Vector of b₂
for b₅, b₆ being Vector of b₃
for b₇ being additiveFAF homogeneousFAF Form of b₂,b₃ holds b₇ . [b₄,(b₅ - b₆)] = (b₇ . [b₄,b₅]) - (b₇ . [b₄,b₆])

proof end;

theorem Th38: :: BILINEAR:38

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂, b₃ being VectSp of b₁
for b₄, b₅ being Vector of b₂
for b₆, b₇ being Vector of b₃
for b₈ being bilinear-Form of b₂,b₃ holds b₈ . [(b₄ - b₅),(b₆ - b₇)] = ((b₈ . [b₄,b₆]) - (b₈ . [b₄,b₇])) - ((b₈ . [b₅,b₆]) - (b₈ . [b₅,b₇]))

proof end;

theorem Th39: :: BILINEAR:39

for b₁ being non empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂, b₃ being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₄, b₅ being Vector of b₂
for b₆, b₇ being Vector of b₃
for b₈, b₉ being Element of b₁
for b₁₀ being bilinear-Form of b₂,b₃ holds b₁₀ . [(b₄ + (b₈ * b₅)),(b₆ + (b₉ * b₇))] = ((b₁₀ . [b₄,b₆]) + (b₉ * (b₁₀ . [b₄,b₇]))) + ((b₈ * (b₁₀ . [b₅,b₆])) + (b₈ * (b₉ * (b₁₀ . [b₅,b₇]))))

proof end;

theorem Th40: :: BILINEAR:40

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂, b₃ being VectSp of b₁
for b₄, b₅ being Vector of b₂
for b₆, b₇ being Vector of b₃
for b₈, b₉ being Element of b₁
for b₁₀ being bilinear-Form of b₂,b₃ holds b₁₀ . [(b₄ - (b₈ * b₅)),(b₆ - (b₉ * b₇))] = ((b₁₀ . [b₄,b₆]) - (b₉ * (b₁₀ . [b₄,b₇]))) - ((b₈ * (b₁₀ . [b₅,b₆])) - (b₈ * (b₉ * (b₁₀ . [b₅,b₇]))))

proof end;

theorem Th41: :: BILINEAR:41

for b₁ being non empty add-associative right_zeroed right_complementable doubleLoopStr
for b₂, b₃ being non empty right_zeroed VectSpStr of b₁
for b₄ being Form of b₂,b₃ st ( b₄ is additiveFAF or b₄ is additiveSAF ) holds
( b₄ is constant iff for b₅ being Vector of b₂
for b₆ being Vector of b₃ holds b₄ . [b₅,b₆] = 0. b₁ )

proof end;

definition

let c₁ be ZeroStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be Form of c₂,c₃;
func leftker c₄ -> Subset of a₂ equals :: BILINEAR:def 16
{ b₁ where B is Vector of a₂ : for b₁ being Vector of a₃ holds a₄ . [b₁,b₂] = 0. a₁ } ;
correctness

proof end;

end;

:: deftheorem Def16 defines leftker BILINEAR:def 16 :

definition

let c₁ be ZeroStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be Form of c₂,c₃;
func rightker c₄ -> Subset of a₃ equals :: BILINEAR:def 17
{ b₁ where B is Vector of a₃ : for b₁ being Vector of a₂ holds a₄ . [b₂,b₁] = 0. a₁ } ;
correctness

proof end;

end;

:: deftheorem Def17 defines rightker BILINEAR:def 17 :

definition

let c₁ be ZeroStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be Form of c₂,c₂;
func diagker c₃ -> Subset of a₂ equals :: BILINEAR:def 18
{ b₁ where B is Vector of a₂ : a₃ . [b₁,b₁] = 0. a₁ } ;
correctness

proof end;

end;

:: deftheorem Def18 defines diagker BILINEAR:def 18 :

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂ be non empty right_zeroed VectSpStr of c₁;
let c₃ be non empty VectSpStr of c₁;
let c₄ be additiveSAF Form of c₂,c₃;
cluster leftker a₄ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of c₁;
let c₃ be non empty VectSpStr of c₁;
let c₄ be homogeneousSAF Form of c₂,c₃;
cluster leftker a₄ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be non empty right_zeroed VectSpStr of c₁;
let c₄ be additiveFAF Form of c₂,c₃;
cluster rightker a₄ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of c₁;
let c₄ be homogeneousFAF Form of c₂,c₃;
cluster rightker a₄ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable doubleLoopStr ;
let c₂ be non empty right_zeroed VectSpStr of c₁;
let c₃ be additiveFAF Form of c₂,c₂;
cluster diagker a₃ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable doubleLoopStr ;
let c₂ be non empty right_zeroed VectSpStr of c₁;
let c₃ be additiveSAF Form of c₂,c₂;
cluster diagker a₃ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of c₁;
let c₃ be homogeneousFAF Form of c₂,c₂;
cluster diagker a₃ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of c₁;
let c₃ be homogeneousSAF Form of c₂,c₂;
cluster diagker a₃ -> non empty ;
coherence

proof end;

end;

theorem Th42: :: BILINEAR:42

for b₁ being ZeroStr
for b₂ being non empty VectSpStr of b₁
for b₃ being Form of b₂,b₂ holds
( leftker b₃ c= diagker b₃ & rightker b₃ c= diagker b₃ )

proof end;

theorem Th43: :: BILINEAR:43

for b₁ being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being additiveSAF homogeneousSAF Form of b₂,b₃ holds leftker b₄ is lineary-closed

proof end;

theorem Th44: :: BILINEAR:44

for b₁ being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being additiveFAF homogeneousFAF Form of b₂,b₃ holds rightker b₄ is lineary-closed

proof end;

definition

proof end;

uniqueness by VECTSP_4:37;

end;

:: deftheorem Def19 defines LKer BILINEAR:def 19 :

definition

proof end;

uniqueness by VECTSP_4:37;

end;

:: deftheorem Def20 defines RKer BILINEAR:def 20 :

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be VectSp of c₁;
let c₃ be non empty VectSpStr of c₁;
let c₄ be additiveSAF homogeneousSAF Form of c₂,c₃;
func LQForm c₄ -> additiveSAF homogeneousSAF Form of (VectQuot a₂,(LKer a₄)),a₃ means :Def21: :: BILINEAR:def 21
for b₁ being Vector of (VectQuot a₂,(LKer a₄))
for b₂ being Vector of a₃
for b₃ being Vector of a₂ st b₁ = b₃ + (LKer a₄) holds
a₅ . [b₁,b₂] = a₄ . [b₃,b₂];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def21 defines LQForm BILINEAR:def 21 :

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be VectSp of c₁;
let c₄ be additiveFAF homogeneousFAF Form of c₂,c₃;
func RQForm c₄ -> additiveFAF homogeneousFAF Form of a₂,(VectQuot a₃,(RKer a₄)) means :Def22: :: BILINEAR:def 22
for b₁ being Vector of (VectQuot a₃,(RKer a₄))
for b₂ being Vector of a₂
for b₃ being Vector of a₃ st b₁ = b₃ + (RKer a₄) holds
a₅ . [b₂,b₁] = a₄ . [b₂,b₃];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def22 defines RQForm BILINEAR:def 22 :

registration

proof end;

cluster RQForm a₄ -> additiveFAF additiveSAF homogeneousFAF homogeneousSAF ;
coherence

proof end;

end;

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂, c₃ be VectSp of c₁;
let c₄ be bilinear-Form of c₂,c₃;
func QForm c₄ -> bilinear-Form of (VectQuot a₂,(LKer a₄)),(VectQuot a₃,(RKer a₄)) means :Def23: :: BILINEAR:def 23
for b₁ being Vector of (VectQuot a₂,(LKer a₄))
for b₂ being Vector of (VectQuot a₃,(RKer a₄))
for b₃ being Vector of a₂
for b₄ being Vector of a₃ st b₁ = b₃ + (LKer a₄) & b₂ = b₄ + (RKer a₄) holds
a₅ . [b₁,b₂] = a₄ . [b₃,b₄];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def23 defines QForm BILINEAR:def 23 :

theorem Th45: :: BILINEAR:45

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being VectSp of b₁
for b₃ being non empty VectSpStr of b₁
for b₄ being additiveSAF homogeneousSAF Form of b₂,b₃ holds rightker b₄ = rightker (LQForm b₄)

proof end;

theorem Th46: :: BILINEAR:46

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty VectSpStr of b₁
for b₃ being VectSp of b₁
for b₄ being additiveFAF homogeneousFAF Form of b₂,b₃ holds leftker b₄ = leftker (RQForm b₄)

proof end;

theorem Th47: :: BILINEAR:47

proof end;

theorem Th48: :: BILINEAR:48

proof end;

theorem Th49: :: BILINEAR:49

proof end;

theorem Th50: :: BILINEAR:50

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂, b₃ being VectSp of b₁
for b₄ being bilinear-Form of b₂,b₃ holds
( leftker (QForm b₄) = leftker (RQForm (LQForm b₄)) & rightker (QForm b₄) = rightker (RQForm (LQForm b₄)) & leftker (QForm b₄) = leftker (LQForm (RQForm b₄)) & rightker (QForm b₄) = rightker (LQForm (RQForm b₄)) )

proof end;

theorem Th51: :: BILINEAR:51

for b₁ being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Functional of b₂
for b₅ being Functional of b₃ holds ker b₄ c= leftker (FormFunctional b₄,b₅)

proof end;

theorem Th52: :: BILINEAR:52

for b₁ being non empty add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like doubleLoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Functional of b₂
for b₅ being Functional of b₃ st b₅ <> 0Functional b₃ holds
leftker (FormFunctional b₄,b₅) = ker b₄

proof end;

theorem Th53: :: BILINEAR:53

proof end;

theorem Th54: :: BILINEAR:54

for b₁ being non empty add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like doubleLoopStr
for b₂, b₃ being non empty VectSpStr of b₁
for b₄ being Functional of b₂
for b₅ being Functional of b₃ st b₄ <> 0Functional b₂ holds
rightker (FormFunctional b₄,b₅) = ker b₅

proof end;

theorem Th55: :: BILINEAR:55

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like doubleLoopStr
for b₂ being VectSp of b₁
for b₃ being non empty VectSpStr of b₁
for b₄ being linear-Functional of b₂
for b₅ being Functional of b₃ st b₅ <> 0Functional b₃ holds
( LKer (FormFunctional b₄,b₅) = Ker b₄ & LQForm (FormFunctional b₄,b₅) = FormFunctional (CQFunctional b₄),b₅ )

proof end;

theorem Th56: :: BILINEAR:56

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like doubleLoopStr
for b₂ being non empty VectSpStr of b₁
for b₃ being VectSp of b₁
for b₄ being Functional of b₂
for b₅ being linear-Functional of b₃ st b₄ <> 0Functional b₂ holds
( RKer (FormFunctional b₄,b₅) = Ker b₅ & RQForm (FormFunctional b₄,b₅) = FormFunctional b₄,(CQFunctional b₅) )

proof end;

theorem Th57: :: BILINEAR:57

for b₁ being Field
for b₂, b₃ being non trivial VectSp of b₁
for b₄ being V126 linear-Functional of b₂
for b₅ being V126 linear-Functional of b₃ holds QForm (FormFunctional b₄,b₅) = FormFunctional (CQFunctional b₄),(CQFunctional b₅)

proof end;

definition

let c₁ be ZeroStr ;
let c₂, c₃ be non empty VectSpStr of c₁;
let c₄ be Form of c₂,c₃;
attr a₄ is degenerated-on-left means :Def24: :: BILINEAR:def 24
leftker a₄ <> {(0. a₂)};
attr a₄ is degenerated-on-right means :Def25: :: BILINEAR:def 25
rightker a₄ <> {(0. a₃)};

end;

:: deftheorem Def24 defines degenerated-on-left BILINEAR:def 24 :

:: deftheorem Def25 defines degenerated-on-right BILINEAR:def 25 :

registration

proof end;

end;

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be non empty right_zeroed VectSpStr of c₁;
let c₃ be VectSp of c₁;
let c₄ be additiveFAF homogeneousFAF Form of c₂,c₃;
cluster RQForm a₄ -> additiveFAF homogeneousFAF non degenerated-on-right ;
coherence

proof end;

end;

registration

proof end;

end;

registration

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂, c₃ be VectSp of c₁;
let c₄ be bilinear-Form of c₂,c₃;
cluster RQForm (LQForm a₄) -> additiveFAF additiveSAF homogeneousFAF homogeneousSAF non degenerated-on-left non degenerated-on-right ;
coherence

proof end;

cluster LQForm (RQForm a₄) -> additiveFAF additiveSAF homogeneousFAF homogeneousSAF non degenerated-on-left non degenerated-on-right ;
coherence

proof end;

end;

registration

let c₁ be Field;
let c₂, c₃ be non trivial VectSp of c₁;
let c₄ be non constant bilinear-Form of c₂,c₃;
cluster QForm a₄ -> non constant non degenerated-on-left non degenerated-on-right ;
coherence

proof end;

end;

definition

let c₁ be 1-sorted ;
let c₂ be VectSpStr of c₁;
let c₃ be Form of c₂,c₂;
attr a₃ is symmetric means :Def26: :: BILINEAR:def 26
for b₁, b₂ being Vector of a₂ holds a₃ . [b₁,b₂] = a₃ . [b₂,b₁];

end;

:: deftheorem Def26 defines symmetric BILINEAR:def 26 :

definition

let c₁ be ZeroStr ;
let c₂ be VectSpStr of c₁;
let c₃ be Form of c₂,c₂;
attr a₃ is alternating means :Def27: :: BILINEAR:def 27
for b₁ being Vector of a₂ holds a₃ . [b₁,b₁] = 0. a₁;

end;

:: deftheorem Def27 defines alternating BILINEAR:def 27 :

registration

let c₁ be non empty ZeroStr ;
let c₂ be non empty VectSpStr of c₁;
cluster NulForm a₂,a₂ -> symmetric ;
coherence

proof end;

cluster NulForm a₂,a₂ -> alternating ;
coherence

proof end;

end;

registration

let c₁ be non empty ZeroStr ;
let c₂ be non empty VectSpStr of c₁;
cluster symmetric Relation of [:the carrier of a₂,the carrier of a₂:],the carrier of a₁;
existence

proof end;

cluster alternating Relation of [:the carrier of a₂,the carrier of a₂:],the carrier of a₁;
existence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
cluster additiveFAF additiveSAF homogeneousFAF homogeneousSAF symmetric Relation of [:the carrier of a₂,the carrier of a₂:],the carrier of a₁;
existence

proof end;

cluster additiveFAF additiveSAF homogeneousFAF homogeneousSAF alternating Relation of [:the carrier of a₂,the carrier of a₂:],the carrier of a₁;
existence

proof end;

end;

registration

let c₁ be Field;
let c₂ be non trivial VectSp of c₁;
cluster non constant non trivial additiveFAF additiveSAF homogeneousFAF homogeneousSAF symmetric Relation of [:the carrier of a₂,the carrier of a₂:],the carrier of a₁;
existence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable LoopStr ;
let c₂ be non empty VectSpStr of c₁;
cluster additiveFAF additiveSAF alternating Relation of [:the carrier of a₂,the carrier of a₂:],the carrier of a₁;
existence

proof end;

end;

registration

let c₁ be non empty LoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃, c₄ be symmetric Form of c₂,c₂;
cluster a₃ + a₄ -> symmetric ;
coherence

proof end;

end;

registration

let c₁ be non empty doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be symmetric Form of c₂,c₂;
let c₄ be Element of c₁;
cluster a₄ * a₃ -> symmetric ;
coherence

proof end;

end;

registration

let c₁ be non empty LoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be symmetric Form of c₂,c₂;
cluster - a₃ -> symmetric ;
coherence

proof end;

end;

registration

let c₁ be non empty LoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃, c₄ be symmetric Form of c₂,c₂;
cluster a₃ - a₄ -> symmetric ;
coherence ;

end;

registration

let c₁ be non empty right_zeroed LoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃, c₄ be alternating Form of c₂,c₂;
cluster a₃ + a₄ -> alternating ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be alternating Form of c₂,c₂;
let c₄ be Scalar of c₁;
cluster a₄ * a₃ -> alternating ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable LoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃ be alternating Form of c₂,c₂;
cluster - a₃ -> alternating ;
coherence

proof end;

end;

registration

let c₁ be non empty add-associative right_zeroed right_complementable LoopStr ;
let c₂ be non empty VectSpStr of c₁;
let c₃, c₄ be alternating Form of c₂,c₂;
cluster a₃ - a₄ -> alternating ;
coherence ;

end;

theorem Th58: :: BILINEAR:58

for b₁ being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for b₂ being non empty VectSpStr of b₁
for b₃ being symmetric bilinear-Form of b₂,b₂ holds leftker b₃ = rightker b₃

proof end;

theorem Th59: :: BILINEAR:59

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being non empty VectSpStr of b₁
for b₃ being additiveFAF additiveSAF alternating Form of b₂,b₂
for b₄, b₅ being Vector of b₂ holds b₃ . [b₄,b₅] = - (b₃ . [b₅,b₄])

proof end;

definition

let c₁ be Fanoian Field;
let c₂ be non empty VectSpStr of c₁;
let c₃ be additiveFAF additiveSAF Form of c₂,c₂;
redefine attr a₃ is alternating means :: BILINEAR:def 28
for b₁, b₂ being Vector of a₂ holds a₃ . [b₁,b₂] = - (a₃ . [b₂,b₁]);
compatibility

proof end;

end;

:: deftheorem Def28 defines alternating BILINEAR:def 28 :

theorem Th60: :: BILINEAR:60

for b₁ being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for b₂ being non empty VectSpStr of b₁
for b₃ being alternating bilinear-Form of b₂,b₂ holds leftker b₃ = rightker b₃

proof end;