:: Bilinear Functionals in Vector Spaces
:: by Jaros{\l}aw Kotowicz
::
:: Received November 5, 2002
:: Copyright (c) 2002 Association of Mizar Users
:: 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:
:: 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)
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
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
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)
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
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:
:: 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)
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
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;
:: 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) )
end;
:: deftheorem Def8 defines - BILINEAR:def 8 :
theorem :: BILINEAR:1
canceled;
theorem :: BILINEAR:2
theorem :: BILINEAR:3
theorem :: BILINEAR:4
theorem :: BILINEAR:5
theorem :: BILINEAR:6
theorem :: BILINEAR:7
theorem :: BILINEAR:8
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;
reconsider g =
g as
Function of the
carrier of
W,the
carrier of
K by A2, FUNCT_2:4, XBOOLE_1:1;
g = (curry f) . v
by A2;
hence
(curry f) . v is
Functional of
W
;
:: thesis: (curry' f) . y is Functional of Vconsider 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;
reconsider h =
h as
Function of the
carrier of
V,the
carrier of
K by A3, FUNCT_2:4, XBOOLE_1:1;
h = (curry' f) . y
by A3;
hence
(curry' f) . y is
Functional of
V
;
:: thesis: verum
end;
:: deftheorem defines FunctionalFAF BILINEAR:def 9 :
:: deftheorem defines FunctionalSAF BILINEAR:def 10 :
theorem Th9: :: BILINEAR:9
theorem Th10: :: BILINEAR:10
theorem Th11: :: BILINEAR:11
theorem Th12: :: BILINEAR:12
theorem Th13: :: BILINEAR:13
theorem Th14: :: BILINEAR:14
theorem Th15: :: BILINEAR:15
theorem Th16: :: BILINEAR:16
theorem Th17: :: BILINEAR:17
theorem Th18: :: BILINEAR:18
theorem :: BILINEAR:19
theorem :: BILINEAR:20
definition
let K be non
empty multMagma ;
let V,
W be non
empty VectSpStr of
K;
let f be
Functional of
V;
let g be
Functional of
W;
func FormFunctional f,
g -> Form of
V,
W means :
Def11:
:: BILINEAR:def 11
for
v being
Vector of
V for
w being
Vector of
W holds
it . v,
w = (f . v) * (g . w);
existence
ex 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)
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
end;
:: deftheorem Def11 defines FormFunctional BILINEAR:def 11 :
theorem Th21: :: BILINEAR:21
theorem Th22: :: BILINEAR:22
theorem :: BILINEAR:23
theorem :: BILINEAR:24
theorem Th25: :: BILINEAR:25
theorem Th26: :: BILINEAR:26
:: 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: :: BILINEAR:27
theorem Th28: :: BILINEAR:28
theorem Th29: :: BILINEAR:29
theorem Th30: :: BILINEAR:30
theorem Th31: :: BILINEAR:31
theorem Th32: :: BILINEAR:32
theorem Th33: :: BILINEAR:33
theorem Th34: :: BILINEAR:34
theorem Th35: :: BILINEAR:35
theorem Th36: :: BILINEAR:36
theorem Th37: :: BILINEAR:37
theorem Th38: :: BILINEAR:38
theorem :: BILINEAR:39
for
K being non
empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr for
V,
W being non
empty right_complementable add-associative right_zeroed 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))))
theorem :: BILINEAR:40
for
K being non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr for
V,
W being
VectSp of
K for
v,
u being
Vector of
V for
w,
t being
Vector of
W for
a,
b being
Element of
K for
f being
bilinear-Form of
V,
W holds
f . (v - (a * u)),
(w - (b * t)) = ((f . v,w) - (b * (f . v,t))) - ((a * (f . u,w)) - (a * (b * (f . u,t))))
theorem Th41: :: BILINEAR:41
:: deftheorem defines leftker BILINEAR:def 16 :
:: deftheorem defines rightker BILINEAR:def 17 :
:: deftheorem defines diagker BILINEAR:def 18 :
theorem :: BILINEAR:42
theorem Th43: :: BILINEAR:43
theorem Th44: :: BILINEAR:44
:: 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
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
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
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
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
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
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
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
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
end;
:: deftheorem Def23 defines QForm BILINEAR:def 23 :
theorem Th45: :: BILINEAR:45
theorem Th46: :: BILINEAR:46
theorem Th47: :: BILINEAR:47
theorem Th48: :: BILINEAR:48
theorem Th49: :: BILINEAR:49
theorem Th50: :: BILINEAR:50
theorem Th51: :: BILINEAR:51
theorem Th52: :: BILINEAR:52
theorem Th53: :: BILINEAR:53
theorem Th54: :: BILINEAR:54
theorem Th55: :: BILINEAR:55
theorem Th56: :: BILINEAR:56
theorem :: BILINEAR:57
:: deftheorem Def24 defines degenerated-on-left BILINEAR:def 24 :
:: deftheorem Def25 defines degenerated-on-right BILINEAR:def 25 :
:: deftheorem Def26 defines symmetric BILINEAR:def 26 :
:: deftheorem Def27 defines alternating BILINEAR:def 27 :
theorem :: BILINEAR:58
theorem Th59: :: BILINEAR:59
:: deftheorem defines alternating BILINEAR:def 28 :
theorem :: BILINEAR:60