begin
:: deftheorem BILINEAR:def 1 :
canceled;
:: deftheorem defines NulForm BILINEAR:def 2 :
definition
let K be non
empty addLoopStr ;
let V,
W be non
empty VectSpStr of
K;
let f,
g be
Form of
V,
W;
func f + g -> Form of
V,
W means :
Def3:
for
v being
Vector of
for
w being
Vector of holds
it . v,
w = (f . v,w) + (g . v,w);
existence
ex b1 being Form of V,W st
for v being Vector of
for w being Vector of holds b1 . v,w = (f . v,w) + (g . v,w)
uniqueness
for b1, b2 being Form of V,W st ( for v being Vector of
for w being Vector of holds b1 . v,w = (f . v,w) + (g . v,w) ) & ( for v being Vector of
for w being Vector of holds b2 . v,w = (f . v,w) + (g . v,w) ) holds
b1 = b2
end;
:: deftheorem Def3 defines + BILINEAR:def 3 :
definition
let K be non
empty multMagma ;
let V,
W be non
empty VectSpStr of
K;
let f be
Form of
V,
W;
let a be
Element of ;
func a * f -> Form of
V,
W means :
Def4:
for
v being
Vector of
for
w being
Vector of holds
it . v,
w = a * (f . v,w);
existence
ex b1 being Form of V,W st
for v being Vector of
for w being Vector of holds b1 . v,w = a * (f . v,w)
uniqueness
for b1, b2 being Form of V,W st ( for v being Vector of
for w being Vector of holds b1 . v,w = a * (f . v,w) ) & ( for v being Vector of
for w being Vector of holds b2 . v,w = a * (f . v,w) ) holds
b1 = b2
end;
:: deftheorem Def4 defines * BILINEAR:def 4 :
definition
let K be non
empty addLoopStr ;
let V,
W be non
empty VectSpStr of
K;
let f be
Form of
V,
W;
func - f -> Form of
V,
W means :
Def5:
for
v being
Vector of
for
w being
Vector of holds
it . v,
w = - (f . v,w);
existence
ex b1 being Form of V,W st
for v being Vector of
for w being Vector of holds b1 . v,w = - (f . v,w)
uniqueness
for b1, b2 being Form of V,W st ( for v being Vector of
for w being Vector of holds b1 . v,w = - (f . v,w) ) & ( for v being Vector of
for w being Vector of holds b2 . v,w = - (f . v,w) ) holds
b1 = b2
end;
:: deftheorem Def5 defines - BILINEAR:def 5 :
:: deftheorem defines - BILINEAR:def 6 :
:: deftheorem defines - BILINEAR:def 7 :
definition
let K be non
empty addLoopStr ;
let V,
W be non
empty VectSpStr of
K;
let f,
g be
Form of
V,
W;
-redefine func f - g -> Form of
V,
W means :
Def8:
for
v being
Vector of
for
w being
Vector of 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
for w being Vector of holds b1 . v,w = (f . v,w) - (g . v,w) )
end;
:: deftheorem Def8 defines - BILINEAR:def 8 :
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
Lm2:
now
let K be non
empty 1-sorted ;
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 holds
( (curry f) . v is Functional of W & (curry' f) . y is Functional of V )let V,
W be 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 holds
( (curry f) . v is Functional of W & (curry' f) . y is Functional of V )let f be
Form of
V,
W;
for v being Element of the carrier of V
for y being Element of holds
( (curry f) . v is Functional of W & (curry' f) . y is Functional of V )let v be
Element of the
carrier of
V;
for y being Element of holds
( (curry f) . v is Functional of W & (curry' f) . y is Functional of V )let y be
Element of ;
( (curry f) . v is Functional of W & (curry' f) . y is Functional of V )A1:
dom f = [:the carrier of V,the carrier of W:]
by FUNCT_2:def 1;
then consider g being
Function such that A2:
(curry f) . v = g
and A3:
(
dom g = the
carrier of
W &
rng g c= rng f )
and
for
y being
set st
y in the
carrier of
W holds
g . y = f . v,
y
by FUNCT_5:36;
reconsider g =
g as
Function of the
carrier of
W,the
carrier of
K by A3, FUNCT_2:4, XBOOLE_1:1;
g = (curry f) . v
by A2;
hence
(curry f) . v is
Functional of
W
;
(curry' f) . y is Functional of Vconsider h being
Function such that A4:
(curry' f) . y = h
and A5:
(
dom h = the
carrier of
V &
rng h c= rng f )
and
for
x being
set st
x in the
carrier of
V holds
h . x = f . x,
y
by A1, FUNCT_5:39;
reconsider h =
h as
Function of the
carrier of
V,the
carrier of
K by A5, FUNCT_2:4, XBOOLE_1:1;
h = (curry' f) . y
by A4;
hence
(curry' f) . y is
Functional of
V
;
verum
end;
begin
:: deftheorem defines FunctionalFAF BILINEAR:def 9 :
:: deftheorem defines FunctionalSAF BILINEAR:def 10 :
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem
theorem
begin
definition
let K be non
empty multMagma ;
let V,
W be non
empty VectSpStr of
K;
let f be
Functional of
V;
let g be
Functional of
W;
func FormFunctional f,
g -> Form of
V,
W means :
Def11:
for
v being
Vector of
for
w being
Vector of holds
it . v,
w = (f . v) * (g . w);
existence
ex b1 being Form of V,W st
for v being Vector of
for w being Vector of holds b1 . v,w = (f . v) * (g . w)
uniqueness
for b1, b2 being Form of V,W st ( for v being Vector of
for w being Vector of holds b1 . v,w = (f . v) * (g . w) ) & ( for v being Vector of
for w being Vector of holds b2 . v,w = (f . v) * (g . w) ) holds
b1 = b2
end;
:: deftheorem Def11 defines FormFunctional BILINEAR:def 11 :
theorem Th21:
theorem Th22:
theorem
theorem
theorem Th25:
theorem Th26:
begin
:: deftheorem Def12 defines additiveFAF BILINEAR:def 12 :
:: deftheorem Def13 defines additiveSAF BILINEAR:def 13 :
:: deftheorem Def14 defines homogeneousFAF BILINEAR:def 14 :
:: deftheorem Def15 defines homogeneousSAF BILINEAR:def 15 :
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem
for
K being non
empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr for
V,
W being non
empty right_complementable add-associative right_zeroed VectSp-like VectSpStr of
K for
v,
u being
Vector of
for
w,
t being
Vector of
for
a,
b being
Element of
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))))
theorem
for
K being non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr for
V,
W being
VectSp of
for
v,
u being
Vector of
for
w,
t being
Vector of
for
a,
b being
Element of
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))))
theorem Th41:
begin
:: deftheorem defines leftker BILINEAR:def 16 :
:: deftheorem defines rightker BILINEAR:def 17 :
:: deftheorem defines diagker BILINEAR:def 18 :
theorem
theorem Th43:
theorem Th44:
:: deftheorem Def19 defines LKer BILINEAR:def 19 :
:: deftheorem Def20 defines RKer BILINEAR:def 20 :
definition
let K be non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be
VectSp of ;
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:
for
A being
Vector of
for
w being
Vector of
for
v being
Vector of 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
for w being Vector of
for v being Vector of st A = v + (LKer f) holds
b1 . A,w = f . v,w
uniqueness
for b1, b2 being additiveSAF homogeneousSAF Form of (VectQuot V,(LKer f)),W st ( for A being Vector of
for w being Vector of
for v being Vector of st A = v + (LKer f) holds
b1 . A,w = f . v,w ) & ( for A being Vector of
for w being Vector of
for v being Vector of st A = v + (LKer f) holds
b2 . A,w = f . v,w ) holds
b1 = b2
end;
:: deftheorem Def21 defines LQForm BILINEAR:def 21 :
definition
let K be non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be non
empty VectSpStr of
K;
let W be
VectSp of ;
let f be
additiveFAF homogeneousFAF Form of
V,
W;
func RQForm f -> additiveFAF homogeneousFAF Form of
V,
(VectQuot W,(RKer f)) means :
Def22:
for
A being
Vector of
for
v being
Vector of
for
w being
Vector of 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
for v being Vector of
for w being Vector of st A = w + (RKer f) holds
b1 . v,A = f . v,w
uniqueness
for b1, b2 being additiveFAF homogeneousFAF Form of V,(VectQuot W,(RKer f)) st ( for A being Vector of
for v being Vector of
for w being Vector of st A = w + (RKer f) holds
b1 . v,A = f . v,w ) & ( for A being Vector of
for v being Vector of
for w being Vector of st A = w + (RKer f) holds
b2 . v,A = f . v,w ) holds
b1 = b2
end;
:: deftheorem Def22 defines RQForm BILINEAR:def 22 :
definition
let K be non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V,
W be
VectSp of ;
let f be
bilinear-Form of
V,
W;
func QForm f -> bilinear-Form of
(VectQuot V,(LKer f)),
(VectQuot W,(RKer f)) means :
Def23:
for
A being
Vector of
for
B being
Vector of
for
v being
Vector of
for
w being
Vector of 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
for B being Vector of
for v being Vector of
for w being Vector of st A = v + (LKer f) & B = w + (RKer f) holds
b1 . A,B = f . v,w
uniqueness
for b1, b2 being bilinear-Form of (VectQuot V,(LKer f)),(VectQuot W,(RKer f)) st ( for A being Vector of
for B being Vector of
for v being Vector of
for w being Vector of st A = v + (LKer f) & B = w + (RKer f) holds
b1 . A,B = f . v,w ) & ( for A being Vector of
for B being Vector of
for v being Vector of
for w being Vector of st A = v + (LKer f) & B = w + (RKer f) holds
b2 . A,B = f . v,w ) holds
b1 = b2
end;
:: deftheorem Def23 defines QForm BILINEAR:def 23 :
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem
:: deftheorem Def24 defines degenerated-on-left BILINEAR:def 24 :
:: deftheorem Def25 defines degenerated-on-right BILINEAR:def 25 :
begin
:: deftheorem Def26 defines symmetric BILINEAR:def 26 :
:: deftheorem Def27 defines alternating BILINEAR:def 27 :
theorem
theorem Th59:
:: deftheorem defines alternating BILINEAR:def 28 :
theorem