:: Bilinear Functionals in Vector Spaces
:: by Jaros{\l}aw Kotowicz
::
:: Received November 5, 2002
:: Copyright (c) 2002-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies STRUCT_0, VECTSP_1, FUNCT_1, ZFMISC_1, XBOOLE_0, FUNCOP_1,
SUPINF_2, ALGSTR_0, ARYTM_3, SUBSET_1, RELAT_1, ARYTM_1, RLVECT_1,
MESFUNC1, BINOP_1, FUNCT_5, TARSKI, HAHNBAN, HAHNBAN1, MSSUBFAM,
UNIALG_1, LATTICES, RLSUB_1, VECTSP10, GROUP_6, RELAT_2, SPPOL_1,
BILINEAR;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, FUNCT_1, RELAT_1,
STRUCT_0, ALGSTR_0, RLVECT_1, BINOP_1, GROUP_1, VECTSP_1, RELSET_1,
FUNCT_2, FUNCOP_1, FUNCT_5, VECTSP_4, HAHNBAN1, VECTSP10;
constructors BORSUK_1, VECTSP10, FUNCOP_1, BINOP_1, FUNCT_5;
registrations SUBSET_1, RELSET_1, STRUCT_0, VECTSP_1, VECTSP_4, HAHNBAN1,
VECTSP10, FUNCT_2;
requirements SUBSET, BOOLE;
definitions HAHNBAN1, TARSKI, XBOOLE_0, VECTSP_4, VECTSP_1;
equalities HAHNBAN1, XBOOLE_0, BINOP_1, STRUCT_0, VECTSP_1;
expansions HAHNBAN1, BINOP_1, STRUCT_0, VECTSP_1;
theorems FUNCT_5, FUNCT_2, HAHNBAN1, VECTSP_1, FUNCOP_1, RLVECT_1, VECTSP_4,
TARSKI, FUNCT_1, ZFMISC_1, DOMAIN_1, VECTSP10, GROUP_1, BINOP_1,
STRUCT_0, VECTSP_2, XTUPLE_0;
schemes BINOP_1;
begin
:: Two Form on Vector Spaces and Operations on Them.
definition
let K be 1-sorted;
let V,W be ModuleStr over K;
mode Form of V,W is Function of [:the carrier of V,the carrier of W:], the
carrier of K;
end;
definition
let K be non empty ZeroStr;
let V,W be ModuleStr over K;
func NulForm(V,W) -> Form of V,W equals
[:the carrier of V,the carrier of W
:] --> 0.K;
coherence;
end;
definition
let K be non empty addLoopStr;
let V,W be non empty ModuleStr over K;
let f,g be Form of V,W;
func f+g -> Form of V,W means
:Def2:
for v be Vector of V, w be Vector of W holds it.(v,w) = f.(v,w)+g.(v,w);
existence
proof
set X = the carrier of V, Y = the carrier of W, Z = the carrier of K;
deffunc F(Element of X, Element of Y) = f.($1,$2)+g.($1,$2);
consider ff be Function of [:X,Y:],Z such that
A1: for x be Element of X for y be Element of Y holds ff.(x,y)=F(x,y)
from BINOP_1:sch 4;
reconsider ff as Form of V,W;
take ff;
thus thesis by A1;
end;
uniqueness
proof
let F,G be Form of V, W such that
A2: for v be Vector of V, w be Vector of W holds F.(v,w) = f.(v,w)+g.( v,w) and
A3: for v be Vector of V, w be Vector of W holds G.(v,w) = f.(v,w)+g.( v,w);
now
let v be Vector of V, w be Vector of W;
thus F.(v,w) = f.(v,w)+g.(v,w) by A2
.= G.(v,w) by A3;
end;
hence thesis;
end;
end;
definition
let K be non empty multMagma;
let V,W be non empty ModuleStr over K;
let f be Form of V,W;
let a be Element of K;
func a*f -> Form of V,W means
:Def3:
for v be Vector of V, w be Vector of W holds it.(v,w) = a*f.(v,w);
existence
proof
set X = the carrier of V, Y = the carrier of W, Z = the carrier of K;
deffunc F(Element of X, Element of Y) = a*f.($1,$2);
consider ff be Function of [:X,Y:],Z such that
A1: for x be Element of X for y be Element of Y holds ff.(x,y)=F(x,y)
from BINOP_1:sch 4;
reconsider ff as Form of V,W;
take ff;
thus thesis by A1;
end;
uniqueness
proof
let F,G be Form of V, W such that
A2: for v be Vector of V, w be Vector of W holds F.(v,w) = a*f.(v,w) and
A3: for v be Vector of V, w be Vector of W holds G.(v,w) = a*f.(v,w);
now
let v be Vector of V, w be Vector of W;
thus F.(v,w) = a*f.(v,w) by A2
.= G.(v,w) by A3;
end;
hence thesis;
end;
end;
definition
let K be non empty addLoopStr;
let V,W be non empty ModuleStr over K;
let f be Form of V,W;
func -f -> Form of V,W means
:Def4:
for v be Vector of V, w be Vector of W holds it.(v,w) = -f.(v,w);
existence
proof
set X = the carrier of V, Y = the carrier of W, Z = the carrier of K;
deffunc F(Element of X,Element of Y) = -f.($1,$2);
consider ff be Function of [:X,Y:],Z such that
A1: for x be Element of X for y be Element of Y holds ff.(x,y)=F(x,y)
from BINOP_1:sch 4;
reconsider ff as Form of V,W;
take ff;
thus thesis by A1;
end;
uniqueness
proof
let F,G be Form of V, W such that
A2: for v be Vector of V, w be Vector of W holds F.(v,w) = -f.(v,w) and
A3: for v be Vector of V, w be Vector of W holds G.(v,w) = -f.(v,w);
now
let v be Vector of V, w be Vector of W;
thus F.(v,w) = -f.(v,w) by A2
.= G.(v,w) by A3;
end;
hence thesis;
end;
end;
definition
let K be add-associative right_zeroed right_complementable left-distributive
left_unital non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f be Form of V,W;
redefine func -f equals :: redefines - (BILINEAR, definition)
(- 1.K) *f;
compatibility
proof
let g be Form of V,W;
thus g= -f implies g = (- 1.K) *f
proof
assume
A1: g =-f;
now
let v be Vector of V, w be Vector of W;
thus g.(v,w)= -f.(v,w) by A1,Def4
.= (-1.K )* f.(v,w) by VECTSP_2:29
.=((- 1.K) *f).(v,w) by Def3;
end;
hence thesis;
end;
assume
A2: g = (- 1.K) *f;
now
let v be Vector of V, w be Vector of W;
thus g.(v,w)= (-1.K )* f.(v,w) by A2,Def3
.=- f.(v,w) by VECTSP_2:29
.= (-f).(v,w) by Def4;
end;
hence thesis;
end;
end;
definition
let K be non empty addLoopStr;
let V,W be non empty ModuleStr over K;
let f,g be Form of V,W;
func f-g -> Form of V,W equals
f + -g;
correctness;
end;
definition
let K be non empty addLoopStr;
let V,W be non empty ModuleStr over K;
let f,g be Form of V,W;
redefine func f - g means :: redefines - (BILINEAR, definition)
:Def7:
for v be Vector of V, w be Vector of W holds it.(v,w) = f.(v,w) - g.(v,w);
compatibility
proof
let h be Form of V,W;
thus h = f- g implies for v be Vector of V, w be Vector of W holds h.(v,w)
= f.(v,w) - g.(v,w)
proof
assume
A1: h = f-g;
let v be Vector of V, w be Vector of W;
thus h.(v,w) = f.(v,w) + (-g).(v,w) by A1,Def2
.= f.(v,w) + -g.(v,w) by Def4
.= f.(v,w) -g.(v,w) by RLVECT_1:def 11;
end;
assume
A2: for v be Vector of V, w be Vector of W holds h.(v,w) = f.(v,w) - g .(v,w);
now
let v be Vector of V, w be Vector of W;
thus h.(v,w) = f.(v,w) - g.(v,w) by A2
.= f.(v,w) +- g.(v,w) by RLVECT_1:def 11
.= f.(v,w) + (-g).(v,w) by Def4
.= (f-g).(v,w) by Def2;
end;
hence thesis;
end;
end;
definition
let K be Abelian non empty addLoopStr;
let V,W be non empty ModuleStr over K;
let f,g be Form of V,W;
redefine func f+g; :: redefines + (BILINEAR, definition)
commutativity
proof
let f,g be Form of V,W;
now
let v be Vector of V,w be Vector of W;
thus (f+g).(v,w) = f.(v,w) + g.(v,w) by Def2
.= (g+f).(v,w) by Def2;
end;
hence f+g=g+f;
end;
end;
theorem
for K be right_zeroed non empty addLoopStr for V,W be non empty
ModuleStr over K for f be Form of V,W holds f + NulForm(V,W) = f
proof
let K be right_zeroed non empty addLoopStr, V,W be non empty ModuleStr
over K, f be Form of V,W;
set g = NulForm(V,W);
now
let v be Vector of V, w be Vector of W;
thus (f+g).(v,w) = f.(v,w) + g.(v,w) by Def2
.= f.(v,w) + 0.K by FUNCOP_1:70
.= f.(v,w) by RLVECT_1:def 4;
end;
hence thesis;
end;
theorem
for K be add-associative non empty addLoopStr for V,W be non empty
ModuleStr over K for f,g,h be Form of V,W holds f+g+h = f+(g+h)
proof
let K be add-associative non empty addLoopStr, V,W be non empty ModuleStr
over K, f,g,h be Form of V,W;
now
let v be Vector of V, w be Vector of W;
thus (f+g+h).(v,w) = (f+g).(v,w) + h.(v,w) by Def2
.= f.(v,w) + g.(v,w)+ h.(v,w) by Def2
.= f.(v,w) + (g.(v,w)+ h.(v,w)) by RLVECT_1:def 3
.= f.(v,w) + (g+h).(v,w) by Def2
.= (f+ (g+h)).(v,w) by Def2;
end;
hence thesis;
end;
theorem
for K be add-associative right_zeroed right_complementable non empty
addLoopStr for V,W be non empty ModuleStr over K for f be Form of V,W holds f
- f = NulForm(V,W)
proof
let K be add-associative right_zeroed right_complementable non empty
addLoopStr, V,W be non empty ModuleStr over K, f be Form of V,W;
now
let v be Vector of V, w be Vector of W;
thus (f-f).(v,w) = f.(v,w) - f.(v,w) by Def7
.= 0.K by RLVECT_1:15
.= (NulForm(V,W)).(v,w) by FUNCOP_1:70;
end;
hence thesis;
end;
theorem
for K be right-distributive non empty doubleLoopStr for V,W be non
empty ModuleStr over K, a be Element of K for f,g be Form of V,W holds a*(f+g)
= a*f+a*g
proof
let K be right-distributive non empty doubleLoopStr, V,W be non empty
ModuleStr over K, r be Element of K, f,g be Form of V,W;
now
let v be Vector of V, w be Vector of W;
thus (r*(f+g)).(v,w) = r * (f+g).(v,w) by Def3
.= r*(f.(v,w) + g.(v,w)) by Def2
.= r*f.(v,w) + r*g.(v,w) by VECTSP_1:def 2
.= (r*f).(v,w) + r*g.(v,w) by Def3
.= (r*f).(v,w) + (r*g).(v,w) by Def3
.= (r*f + r*g).(v,w) by Def2;
end;
hence thesis;
end;
theorem
for K be left-distributive non empty doubleLoopStr for V,W be non
empty ModuleStr over K for a,b be Element of K for f be Form of V,W holds (a+b)
*f = a*f+b*f
proof
let K be left-distributive non empty doubleLoopStr, V,W be non empty
ModuleStr over K, r,s be Element of K, f be Form of V,W;
now
let v be Vector of V, w be Vector of W;
thus ((r+s)*f).(v,w) = (r+s) * f.(v,w) by Def3
.= r*f.(v,w) + s*f.(v,w) by VECTSP_1:def 3
.= (r*f).(v,w) + s*f.(v,w) by Def3
.= (r*f).(v,w) + (s*f).(v,w) by Def3
.= (r*f + s*f).(v,w) by Def2;
end;
hence thesis;
end;
theorem
for K be associative non empty doubleLoopStr for V,W be non empty
ModuleStr over K for a,b be Element of K for f be Form of V,W holds (a*b)*f = a
*(b*f)
proof
let K be associative non empty doubleLoopStr, V,W be non empty ModuleStr
over K, r,s be Element of K, f be Form of V,W;
now
let v be Vector of V, w be Vector of W;
thus ((r*s)*f).(v,w) = (r*s) * f.(v,w) by Def3
.= r*(s*f.(v,w)) by GROUP_1:def 3
.= r*(s*f).(v,w) by Def3
.= (r*(s*f)).(v,w) by Def3;
end;
hence thesis;
end;
theorem
for K be left_unital non empty doubleLoopStr for V,W be non empty
ModuleStr over K for f be Form of V,W holds (1.K)*f = f
proof
let K be left_unital non empty doubleLoopStr, V,W be non empty ModuleStr
over K, f be Form of V,W;
now
let v be Vector of V, w be Vector of W;
thus ((1.K)*f).(v,w) = (1.K) * f.(v,w) by Def3
.= f.(v,w);
end;
hence thesis;
end;
begin
:: Functional generated by Two Form when the One of Arguments is Fixed.
definition
let K be non empty 1-sorted;
let V,W be non empty ModuleStr over K;
let f be Form of V,W, v be Vector of V;
func FunctionalFAF(f,v) -> Functional of W equals
(curry f).v;
correctness;
end;
definition
let K be non empty 1-sorted;
let V,W be non empty ModuleStr over K;
let f be Form of V,W, w be Vector of W;
func FunctionalSAF(f,w) -> Functional of V equals
(curry' f).w;
correctness;
end;
theorem Th8:
for K be non empty 1-sorted for V,W be non empty ModuleStr over K
for f be Form of V,W, v be Vector of V holds dom (FunctionalFAF(f,v)) = the
carrier of W & rng (FunctionalFAF(f,v)) c= the carrier of K & for w be Vector
of W holds (FunctionalFAF(f,v)).w = f.(v,w)
proof
let K be non empty 1-sorted, V,W be non empty ModuleStr over K;
let f be Form of V,W, v be Vector of V;
set F = FunctionalFAF(f,v);
dom f = [:the carrier of V,the carrier of W:] by FUNCT_2:def 1;
then
A1: ex g be Function st (curry f).v = g & dom g = the carrier of W & rng g c=
rng f & for y be object st y in the carrier of W holds g.y = f.( v,y) by
FUNCT_5:29;
hence dom F = the carrier of W & rng F c= the carrier of K;
let y be Vector of W;
thus thesis by A1;
end;
theorem Th9:
for K be non empty 1-sorted for V,W be non empty ModuleStr over
K for f be Form of V,W, w be Vector of W holds dom (FunctionalSAF(f,w)) = the
carrier of V & rng (FunctionalSAF(f,w)) c= the carrier of K & for v be Vector
of V holds (FunctionalSAF(f,w)).v = f.(v,w)
proof
let K be non empty 1-sorted, V,W be non empty ModuleStr over K, f be Form of
V,W, w be Vector of W;
set F = FunctionalSAF(f,w);
dom f = [:the carrier of V,the carrier of W:] by FUNCT_2:def 1;
then
A1: ex g be Function st (curry' f).w = g & dom g = the carrier of V & rng g
c= rng f & for y be object st y in the carrier of V holds g .y = f.(y,w) by
FUNCT_5:32;
hence dom F = the carrier of V & rng F c= the carrier of K;
let v be Vector of V;
thus thesis by A1;
end;
theorem Th10:
for K be non empty ZeroStr, V,W be non empty ModuleStr over K, v
be Vector of V holds FunctionalFAF(NulForm(V,W),v) = 0Functional(W)
proof
let K be non empty ZeroStr, V,W be non empty ModuleStr over K, v be Vector
of V;
set N = NulForm(V,W);
now
let y be Vector of W;
thus FunctionalFAF(N,v).y = N.(v,y) by Th8
.= 0.K by FUNCOP_1:70
.= (0Functional(W)).y by HAHNBAN1:14;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th11:
for K be non empty ZeroStr, V,W be non empty ModuleStr over K, w
be Vector of W holds FunctionalSAF(NulForm(V,W),w) = 0Functional(V)
proof
let K be non empty ZeroStr, V,W be non empty ModuleStr over K, y be Vector
of W;
set N = NulForm(V,W);
now
let v be Vector of V;
thus FunctionalSAF(N,y).v = N.(v,y) by Th9
.= 0.K by FUNCOP_1:70
.= (0Functional(V)).v by HAHNBAN1:14;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th12:
for K be non empty addLoopStr for V,W be non empty ModuleStr
over K for f,g be Form of V,W, w be Vector of W holds FunctionalSAF(f+g,w) =
FunctionalSAF(f,w) + FunctionalSAF(g,w)
proof
let K be non empty addLoopStr, V,W be non empty ModuleStr over K, f,g be
Form of V,W, w be Vector of W;
now
let v be Vector of V;
thus (FunctionalSAF(f+g,w)).v = (f+g).(v,w) by Th9
.= f.(v,w) + g.(v,w) by Def2
.= (FunctionalSAF(f,w)).v + g.(v,w) by Th9
.= (FunctionalSAF(f,w)).v + (FunctionalSAF(g,w)).v by Th9
.= (FunctionalSAF(f,w) +FunctionalSAF(g,w)).v by HAHNBAN1:def 3;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th13:
for K be non empty addLoopStr for V,W be non empty ModuleStr
over K for f,g be Form of V,W, v be Vector of V holds FunctionalFAF(f+g,v) =
FunctionalFAF(f,v) + FunctionalFAF(g,v)
proof
let K be non empty addLoopStr, V,W be non empty ModuleStr over K, f,g be
Form of V,W, w be Vector of V;
now
let v be Vector of W;
thus (FunctionalFAF(f+g,w)).v = (f+g).(w,v) by Th8
.= f.(w,v) + g.(w,v) by Def2
.= (FunctionalFAF(f,w)).v + g.(w,v) by Th8
.= (FunctionalFAF(f,w)).v + (FunctionalFAF(g,w)).v by Th8
.= (FunctionalFAF(f,w) + FunctionalFAF(g,w)).v by HAHNBAN1:def 3;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th14:
for K be non empty doubleLoopStr for V,W be non empty ModuleStr
over K for f be Form of V,W, a be Element of K, w be Vector of W holds
FunctionalSAF(a*f,w) = a*FunctionalSAF(f,w)
proof
let K be non empty doubleLoopStr, V,W be non empty ModuleStr over K, f be
Form of V,W, a be Element of K, w be Vector of W;
now
let v be Vector of V;
thus (FunctionalSAF(a*f,w)).v = (a*f).(v,w) by Th9
.= a*f.(v,w) by Def3
.= a*(FunctionalSAF(f,w)).v by Th9
.= (a*(FunctionalSAF(f,w))).v by HAHNBAN1:def 6;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th15:
for K be non empty doubleLoopStr for V,W be non empty ModuleStr
over K for f be Form of V,W, a be Element of K, v be Vector of V holds
FunctionalFAF(a*f,v) = a*FunctionalFAF(f,v)
proof
let K be non empty doubleLoopStr, V,W be non empty ModuleStr over K, f be
Form of V,W, a be Element of K, w be Vector of V;
now
let v be Vector of W;
thus (FunctionalFAF(a*f,w)).v = (a*f).(w,v) by Th8
.= a*f.(w,v) by Def3
.= a*(FunctionalFAF(f,w)).v by Th8
.= (a* FunctionalFAF(f,w)).v by HAHNBAN1:def 6;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th16:
for K be non empty addLoopStr for V,W be non empty ModuleStr
over K for f be Form of V,W, w be Vector of W holds FunctionalSAF(-f,w) = -
FunctionalSAF(f,w)
proof
let K be non empty addLoopStr, V,W be non empty ModuleStr over K, f be Form
of V,W, w be Vector of W;
now
let v be Vector of V;
thus (FunctionalSAF(-f,w)).v = (-f).(v,w) by Th9
.= -f.(v,w) by Def4
.= -(FunctionalSAF(f,w)).v by Th9
.= (- FunctionalSAF(f,w)).v by HAHNBAN1:def 4;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th17:
for K be non empty addLoopStr for V,W be non empty ModuleStr
over K for f be Form of V,W, v be Vector of V holds FunctionalFAF(-f,v) = -
FunctionalFAF(f,v)
proof
let K be non empty addLoopStr, V,W be non empty ModuleStr over K, f be Form
of V,W, w be Vector of V;
now
let v be Vector of W;
thus (FunctionalFAF(-f,w)).v = (-f).(w,v) by Th8
.= -f.(w,v) by Def4
.= -(FunctionalFAF(f,w)).v by Th8
.= (- FunctionalFAF(f,w)).v by HAHNBAN1:def 4;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for K be non empty addLoopStr for V,W be non empty ModuleStr over K
for f,g be Form of V,W, w be Vector of W holds FunctionalSAF(f-g,w) =
FunctionalSAF(f,w) - FunctionalSAF(g,w)
proof
let K be non empty addLoopStr, V,W be non empty ModuleStr over K, f,g be
Form of V,W, w be Vector of W;
now
let v be Vector of V;
thus (FunctionalSAF(f-g,w)).v = (f-g).(v,w) by Th9
.= f.(v,w) - g.(v,w) by Def7
.= (FunctionalSAF(f,w)).v - g.(v,w) by Th9
.= (FunctionalSAF(f,w)).v - (FunctionalSAF(g,w)).v by Th9
.= (FunctionalSAF(f,w)).v +- (FunctionalSAF(g,w)).v by RLVECT_1:def 11
.= (FunctionalSAF(f,w)).v + (-FunctionalSAF(g,w)).v by HAHNBAN1:def 4
.= (FunctionalSAF(f,w) -FunctionalSAF(g,w)).v by HAHNBAN1:def 3;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for K be non empty addLoopStr for V,W be non empty ModuleStr over K
for f,g be Form of V,W, v be Vector of V holds FunctionalFAF(f-g,v) =
FunctionalFAF(f,v) - FunctionalFAF(g,v)
proof
let K be non empty addLoopStr, V,W be non empty ModuleStr over K, f,g be
Form of V,W, w be Vector of V;
now
let v be Vector of W;
thus (FunctionalFAF(f-g,w)).v = (f-g).(w,v) by Th8
.= f.(w,v) - g.(w,v) by Def7
.= (FunctionalFAF(f,w)).v - g.(w,v) by Th8
.= (FunctionalFAF(f,w)).v - (FunctionalFAF(g,w)).v by Th8
.= (FunctionalFAF(f,w)).v +- (FunctionalFAF(g,w)).v by RLVECT_1:def 11
.= (FunctionalFAF(f,w)).v + (-FunctionalFAF(g,w)).v by HAHNBAN1:def 4
.= (FunctionalFAF(f,w) -FunctionalFAF(g,w)).v by HAHNBAN1:def 3;
end;
hence thesis by FUNCT_2:63;
end;
begin
:: Two Form generated by Functionals.
definition
let K be non empty multMagma;
let V,W be non empty ModuleStr over K;
let f be Functional of V;
let g be Functional of W;
func FormFunctional(f,g) -> Form of V,W means
:Def10:
for v be Vector of V, w be Vector of W holds it.(v,w)= f.v * g.w;
existence
proof
deffunc F(Vector of V, Vector of W) = (f.$1) * (g.$2);
set c1 = the carrier of V, c2 = the carrier of W, k = the carrier of K;
consider i be Function of [:c1,c2:],k such that
A1: for x be Element of c1 for y be Element of c2 holds i.(x,y)=F(x,y)
from BINOP_1:sch 4;
reconsider i as Form of V,W;
take i;
thus thesis by A1;
end;
uniqueness
proof
let F1,F2 be Form of V,W such that
A2: for v be Vector of V,y be Vector of W holds F1.(v,y)= f.v * g.y and
A3: for v be Vector of V,y be Vector of W holds F2.(v,y)= f.v * g.y;
now
let v be Vector of V, y be Vector of W;
thus F1.(v,y) = f.v * g.y by A2
.= F2.(v,y) by A3;
end;
hence thesis;
end;
end;
theorem Th20:
for K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr for V,W be non empty ModuleStr
over K for f be Functional of V,v be Vector of V, w be Vector of W holds
FormFunctional(f,0Functional(W)).(v,w) = 0.K
proof
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f be Functional of V, v be Vector of V, y be Vector of W;
set 0F = 0Functional(W), F = FormFunctional(f,0F);
thus F.(v,y) = f.v * 0F.y by Def10
.= f.v * 0.K by FUNCOP_1:7
.= 0.K;
end;
theorem Th21:
for K be add-associative right_zeroed right_complementable
left-distributive non empty doubleLoopStr for V,W be non empty ModuleStr over
K for g be Functional of W, v be Vector of V, w be Vector of W holds
FormFunctional(0Functional(V),g).(v,w) = 0.K
proof
let K be add-associative right_zeroed right_complementable left-distributive
non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let h be Functional of W, v be Vector of V, y be Vector of W;
set 0F = 0Functional(V), F = FormFunctional(0F,h);
thus F.(v,y) = 0F.v * h.y by Def10
.= 0.K * h.y by FUNCOP_1:7
.= 0.K;
end;
theorem
for K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr for V,W be non empty ModuleStr
over K for f be Functional of V holds FormFunctional(f,0Functional(W)) =
NulForm(V,W)
proof
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K, f be Functional of V;
now
let v be Vector of V, y be Vector of W;
thus FormFunctional(f,0Functional(W)).(v,y) = 0.K by Th20
.= NulForm(V,W).(v,y) by FUNCOP_1:70;
end;
hence thesis;
end;
theorem
for K be add-associative right_zeroed right_complementable
left-distributive non empty doubleLoopStr for V,W be non empty ModuleStr over
K for g be Functional of W holds FormFunctional(0Functional(V),g) = NulForm(V,W
)
proof
let K be add-associative right_zeroed right_complementable left-distributive
non empty doubleLoopStr;
let V,W be non empty ModuleStr over K, h be Functional of W;
now
let v be Vector of V, y be Vector of W;
thus FormFunctional(0Functional(V),h).(v,y) = 0.K by Th21
.= NulForm(V,W).(v,y) by FUNCOP_1:70;
end;
hence thesis;
end;
theorem Th24:
for K be non empty multMagma for V,W be non empty ModuleStr over
K for f be Functional of V, g be Functional of W, v be Vector of V holds
FunctionalFAF(FormFunctional(f,g),v) = f.v * g
proof
let K be non empty multMagma, V,W be non empty ModuleStr over K;
let f be Functional of V, h be Functional of W, v be Vector of V;
set F = FormFunctional(f,h), FF = FunctionalFAF(F,v);
now
let y be Vector of W;
thus FF.y = F.(v,y) by Th8
.= f.v * h.y by Def10
.= (f.v * h).y by HAHNBAN1:def 6;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th25:
for K be commutative non empty multMagma for V,W be non empty
ModuleStr over K for f be Functional of V, g be Functional of W, w be Vector of
W holds FunctionalSAF(FormFunctional(f,g),w) = g.w * f
proof
let K be commutative non empty multMagma, V,W be non empty ModuleStr over
K;
let f be Functional of V,h be Functional of W, y be Vector of W;
set F = FormFunctional(f,h), FF = FunctionalSAF(F,y);
now
let v be Vector of V;
thus FF.v = F.(v,y) by Th9
.= f.v * h.y by Def10
.= (h.y * f).v by HAHNBAN1:def 6;
end;
hence thesis by FUNCT_2:63;
end;
begin
::Bilinear Forms and Their Properties
definition
let K be non empty addLoopStr;
let V,W be non empty ModuleStr over K;
let f be Form of V,W;
attr f is additiveFAF means
:Def11:
for v be Vector of V holds FunctionalFAF (f,v) is additive;
attr f is additiveSAF means
:Def12:
for w be Vector of W holds FunctionalSAF (f,w) is additive;
end;
definition
let K be non empty multMagma;
let V,W be non empty ModuleStr over K;
let f be Form of V,W;
attr f is homogeneousFAF means
:Def13:
for v be Vector of V holds FunctionalFAF(f,v) is homogeneous;
attr f is homogeneousSAF means
:Def14:
for w be Vector of W holds FunctionalSAF(f,w) is homogeneous;
end;
registration
let K be right_zeroed non empty addLoopStr;
let V,W be non empty ModuleStr over K;
cluster NulForm(V,W) -> additiveFAF;
coherence
proof
let v be Vector of V;
FunctionalFAF(NulForm(V,W),v)= 0Functional(W) by Th10;
hence thesis;
end;
cluster NulForm(V,W) -> additiveSAF;
coherence
proof
let y be Vector of W;
FunctionalSAF(NulForm(V,W),y)= 0Functional(V) by Th11;
hence thesis;
end;
end;
registration
let K be right_zeroed non empty addLoopStr;
let V,W be non empty ModuleStr over K;
cluster additiveFAF additiveSAF for Form of V,W;
existence
proof
take NulForm(V,W);
thus thesis;
end;
end;
registration
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
cluster NulForm(V,W) -> homogeneousFAF;
coherence
proof
let v be Vector of V;
FunctionalFAF(NulForm(V,W),v)= 0Functional(W) by Th10;
hence thesis;
end;
cluster NulForm(V,W) -> homogeneousSAF;
coherence
proof
let y be Vector of W;
FunctionalSAF(NulForm(V,W),y)= 0Functional(V) by Th11;
hence thesis;
end;
end;
registration
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
cluster additiveFAF homogeneousFAF additiveSAF homogeneousSAF for
Form of V,W;
existence
proof
take NulForm(V,W);
thus thesis;
end;
end;
definition
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
mode bilinear-Form of V,W is additiveSAF homogeneousSAF additiveFAF
homogeneousFAF Form of V,W;
end;
registration
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f be additiveFAF Form of V,W, v be Vector of V;
cluster FunctionalFAF(f,v) -> additive;
coherence by Def11;
end;
registration
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f be additiveSAF Form of V,W, w be Vector of W;
cluster FunctionalSAF(f,w) -> additive;
coherence by Def12;
end;
registration
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f be homogeneousFAF Form of V,W, v be Vector of V;
cluster FunctionalFAF(f,v) -> homogeneous;
coherence by Def13;
end;
registration
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f be homogeneousSAF Form of V,W, w be Vector of W;
cluster FunctionalSAF(f,w) -> homogeneous;
coherence by Def14;
end;
registration
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f be Functional of V, g be additive Functional of W;
cluster FormFunctional(f,g) -> additiveFAF;
coherence
proof
let v be Vector of V;
set fg = FormFunctional(f,g), F = FunctionalFAF(fg,v);
let y,y9 be Vector of W;
A1: F= f.v * g by Th24;
hence F.(y+y9) = f.v * g.(y+y9) by HAHNBAN1:def 6
.= f.v *(g.y +g.y9) by VECTSP_1:def 20
.= f.v * g.y + f.v * g.y9 by VECTSP_1:def 2
.=f.v * g.y + F.y9 by A1,HAHNBAN1:def 6
.=F.y + F.y9 by A1,HAHNBAN1:def 6;
end;
end;
registration
let K be add-associative right_zeroed right_complementable commutative
right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f be additive Functional of V, g be Functional of W;
cluster FormFunctional(f,g) -> additiveSAF;
coherence
proof
let y be Vector of W;
set fg= FormFunctional(f,g), F = FunctionalSAF(fg,y);
F= g.y * f by Th25;
hence thesis;
end;
end;
registration
let K be add-associative right_zeroed right_complementable commutative
associative right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f be Functional of V, g be homogeneous Functional of W;
cluster FormFunctional(f,g) -> homogeneousFAF;
coherence
proof
let v be Vector of V;
set fg= FormFunctional(f,g), F = FunctionalFAF(fg,v);
let y be Vector of W,r be Scalar of W;
A1: F= f.v * g by Th24;
hence F.(r* y) = f.v * g.(r*y) by HAHNBAN1:def 6
.= f.v *(r*g.y) by HAHNBAN1:def 8
.= r*(f.v * g.y) by GROUP_1:def 3
.= r *F.y by A1,HAHNBAN1:def 6;
end;
end;
registration
let K be add-associative right_zeroed right_complementable commutative
associative right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f be homogeneous Functional of V, g be Functional of W;
cluster FormFunctional(f,g) -> homogeneousSAF;
coherence
proof
let y be Vector of W;
set fg= FormFunctional(f,g);
set F = FunctionalSAF(fg,y);
let v be Vector of V,r be Scalar of V;
A1: F= g.y * f by Th25;
hence F.(r* v) = g.y * f.(r*v) by HAHNBAN1:def 6
.= g.y *(r*f.v) by HAHNBAN1:def 8
.= r*(g.y * f.v) by GROUP_1:def 3
.= r *F.v by A1,HAHNBAN1:def 6;
end;
end;
registration
let K be non degenerated non empty doubleLoopStr;
let V be non trivial ModuleStr over K, W be non empty ModuleStr
over K;
let f be Functional of V, g be Functional of W;
cluster FormFunctional(f,g) -> non trivial;
coherence
proof
set fg = FormFunctional(f,g);
set w = the Vector of W;
consider v be Vector of V such that
A1: v <> 0.V by STRUCT_0:def 18;
A2: [0.V,0.W] <> [v,w] by A1,XTUPLE_0:1;
dom fg = [:the carrier of V, the carrier of W:] by FUNCT_2:def 1;
then
A3: [[0.V,0.W],fg.(0.V,0.W)] in fg & [[v,w],fg.(v,w)] in fg by FUNCT_1:1;
assume
A4: fg is trivial;
per cases by A4,ZFMISC_1:131;
suppose
fg = {};
hence contradiction;
end;
suppose
ex x be object st fg = {x};
then consider x be object such that
A5: fg={x};
[[0.V,0.W],fg.(0.V,0.W)] = x & x=[[v,w],fg.(v,w)] by A3,A5,TARSKI:def 1;
hence contradiction by A2,XTUPLE_0:1;
end;
end;
end;
registration
let K be non degenerated non empty doubleLoopStr;
let V be non empty ModuleStr over K, W be non trivial ModuleStr over K;
let f be Functional of V, g be Functional of W;
cluster FormFunctional(f,g) -> non trivial;
coherence
proof
set fg = FormFunctional(f,g);
set v = the Vector of V;
consider w be Vector of W such that
A1: w <> 0.W by STRUCT_0:def 18;
A2: [0.V,0.W] <> [v,w] by A1,XTUPLE_0:1;
dom fg = [:the carrier of V, the carrier of W:] by FUNCT_2:def 1;
then
A3: [[0.V,0.W],fg.(0.V,0.W)] in fg & [[v,w],fg.(v,w)] in fg by FUNCT_1:1;
assume
A4: fg is trivial;
per cases by A4,ZFMISC_1:131;
suppose
fg = {};
hence contradiction;
end;
suppose
ex x be object st fg = {x};
then consider x be object such that
A5: fg={x};
[[0.V,0.W],fg.(0.V,0.W)] = x & x=[[v,w],fg.(v,w)] by A3,A5,TARSKI:def 1;
hence contradiction by A2,XTUPLE_0:1;
end;
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, g be non constant
0-preserving Functional of W;
cluster FormFunctional(f,g) -> non constant;
coherence
proof
set fg = FormFunctional(f,g);
consider v be Vector of V such that
v <> 0.V and
A1: f.v <> 0.K by VECTSP10:28;
consider w be Vector of W such that
w <> 0.W and
A2: g.w <> 0.K by VECTSP10:28;
fg.(v,w) = f.v * g.w by Def10;
then
A3: dom fg = [:the carrier of V, the carrier of W:] & fg.(v,w) <> 0.K by A1,A2,
FUNCT_2:def 1,VECTSP_1:12;
fg.(0.V,0.W) = f.(0.V)*g.(0.W) by Def10
.= 0.K * g.(0.W) by HAHNBAN1:def 9
.= 0.K;
hence thesis by A3,BINOP_1:19;
end;
end;
registration
let K be Field;
let V,W be non trivial VectSp of K;
cluster non trivial non constant additiveFAF homogeneousFAF additiveSAF
homogeneousSAF for Form of V,W;
existence
proof
set f = the non constant non trivial linear-Functional of V,g = the non
constant non trivial linear-Functional of W;
take FormFunctional(f,g);
thus thesis;
end;
end;
registration
let K be Abelian add-associative right_zeroed non empty addLoopStr;
let V,W be non empty ModuleStr over K;
let f,g be additiveSAF Form of V,W;
cluster f+g -> additiveSAF;
correctness
proof
let w be Vector of W;
set Ffg = FunctionalSAF(f+g,w), Ff = FunctionalSAF(f,w);
set Fg = FunctionalSAF(g,w);
let v,y be Vector of V;
A1: Ff is additive by Def12;
A2: Fg is additive by Def12;
thus Ffg.(v+y) = (Ff+Fg).(v+y) by Th12
.= Ff.(v+y) + Fg.(v+y) by HAHNBAN1:def 3
.= Ff.v+Ff.y + Fg.(v+y) by A1
.= Ff.v+Ff.y + (Fg.v+Fg.y) by A2
.= Ff.v+Ff.y + Fg.v + Fg.y by RLVECT_1:def 3
.= Ff.v+Fg.v + Ff.y+Fg.y by RLVECT_1:def 3
.= (Ff+Fg).v + Ff.y+Fg.y by HAHNBAN1:def 3
.= (Ff+Fg).v + (Ff.y+Fg.y) by RLVECT_1:def 3
.= (Ff+Fg).v + (Ff+Fg).y by HAHNBAN1:def 3
.= Ffg.v + (Ff+Fg).y by Th12
.= Ffg.v + Ffg.y by Th12;
end;
end;
registration
let K be Abelian add-associative right_zeroed non empty addLoopStr;
let V,W be non empty ModuleStr over K;
let f,g be additiveFAF Form of V,W;
cluster f+g -> additiveFAF;
correctness
proof
let w be Vector of V;
set Ffg = FunctionalFAF(f+g,w), Ff = FunctionalFAF(f,w);
set Fg = FunctionalFAF(g,w);
let v,y be Vector of W;
A1: Ff is additive by Def11;
A2: Fg is additive by Def11;
thus Ffg.(v+y) = (Ff+Fg).(v+y) by Th13
.= Ff.(v+y) + Fg.(v+y) by HAHNBAN1:def 3
.= Ff.v+Ff.y + Fg.(v+y) by A1
.= Ff.v+Ff.y + (Fg.v+Fg.y) by A2
.= Ff.v+Ff.y + Fg.v +Fg.y by RLVECT_1:def 3
.= Ff.v+Fg.v + Ff.y+Fg.y by RLVECT_1:def 3
.= (Ff+Fg).v + Ff.y+Fg.y by HAHNBAN1:def 3
.= (Ff+Fg).v + (Ff.y+Fg.y) by RLVECT_1:def 3
.= (Ff+Fg).v + (Ff+Fg).y by HAHNBAN1:def 3
.= Ffg.v + (Ff+Fg).y by Th13
.= Ffg.v + Ffg.y by Th13;
end;
end;
registration
let K be right-distributive right_zeroed non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f be additiveSAF Form of V,W;
let a be Element of K;
cluster a*f -> additiveSAF;
correctness
proof
let w be Vector of W;
set Ffg = FunctionalSAF(a*f,w), Ff = FunctionalSAF(f,w);
let v,y be Vector of V;
A1: Ff is additive by Def12;
thus Ffg.(v+y) = (a*Ff).(v+y) by Th14
.= a*Ff.(v+y) by HAHNBAN1:def 6
.= a*(Ff.v + Ff.y) by A1
.= a* Ff.v + a*Ff.y by VECTSP_1:def 2
.= (a*Ff).v +a* Ff.y by HAHNBAN1:def 6
.= (a*Ff).v + (a*Ff).y by HAHNBAN1:def 6
.= Ffg.v + (a*Ff).y by Th14
.= Ffg.v + Ffg.y by Th14;
end;
end;
registration
let K be right-distributive right_zeroed non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f be additiveFAF Form of V,W;
let a be Element of K;
cluster a*f -> additiveFAF;
correctness
proof
let w be Vector of V;
set Ffg = FunctionalFAF(a*f,w), Ff = FunctionalFAF(f,w);
let v,y be Vector of W;
A1: Ff is additive by Def11;
thus Ffg.(v+y) = (a*Ff).(v+y) by Th15
.= a*Ff.(v+y) by HAHNBAN1:def 6
.= a*(Ff.v + Ff.y) by A1
.= a* Ff.v +a* Ff.y by VECTSP_1:def 2
.= (a*Ff).v +a* Ff.y by HAHNBAN1:def 6
.= (a*Ff).v + (a*Ff).y by HAHNBAN1:def 6
.= Ffg.v + (a*Ff).y by Th15
.= Ffg.v + Ffg.y by Th15;
end;
end;
registration
let K be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr;
let V,W be non empty ModuleStr over K;
let f be additiveSAF Form of V,W;
cluster -f -> additiveSAF;
correctness
proof
let w be Vector of W;
set Ffg = FunctionalSAF(-f,w), Ff = FunctionalSAF(f,w);
let v,y be Vector of V;
A1: Ff is additive by Def12;
thus Ffg.(v+y) = (-Ff).(v+y) by Th16
.= -Ff.(v+y) by HAHNBAN1:def 4
.= -(Ff.v + Ff.y) by A1
.= (- Ff.v) - Ff.y by RLVECT_1:30
.= (-Ff).v - Ff.y by HAHNBAN1:def 4
.= (-Ff).v + - Ff.y by RLVECT_1:def 11
.= (-Ff).v + (-Ff).y by HAHNBAN1:def 4
.= Ffg.v + (-Ff).y by Th16
.= Ffg.v + Ffg.y by Th16;
end;
end;
registration
let K be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr;
let V,W be non empty ModuleStr over K;
let f be additiveFAF Form of V,W;
cluster -f -> additiveFAF;
correctness
proof
let w be Vector of V;
set Ffg = FunctionalFAF(-f,w), Ff = FunctionalFAF(f,w);
let v,y be Vector of W;
A1: Ff is additive by Def11;
thus Ffg.(v+y) = (-Ff).(v+y) by Th17
.= -Ff.(v+y) by HAHNBAN1:def 4
.= -(Ff.v + Ff.y) by A1
.= (- Ff.v) - Ff.y by RLVECT_1:30
.= (-Ff).v - Ff.y by HAHNBAN1:def 4
.= (-Ff).v + - Ff.y by RLVECT_1:def 11
.= (-Ff).v + (-Ff).y by HAHNBAN1:def 4
.= Ffg.v + (-Ff).y by Th17
.= Ffg.v + Ffg.y by Th17;
end;
end;
registration
let K be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr;
let V,W be non empty ModuleStr over K;
let f,g be additiveSAF Form of V,W;
cluster f-g -> additiveSAF;
correctness;
end;
registration
let K be Abelian add-associative right_zeroed right_complementable non
empty addLoopStr;
let V,W be non empty ModuleStr over K;
let f,g be additiveFAF Form of V,W;
cluster f-g -> additiveFAF;
correctness;
end;
registration
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f,g be homogeneousSAF Form of V,W;
cluster f+g -> homogeneousSAF;
correctness
proof
let w be Vector of W;
set Ffg = FunctionalSAF(f+g,w), Ff = FunctionalSAF(f,w);
set Fg = FunctionalSAF(g,w);
let v be Vector of V, a be Scalar of V;
thus Ffg.(a*v) = (Ff+Fg).(a*v) by Th12
.= Ff.(a*v) + Fg.(a*v) by HAHNBAN1:def 3
.= a*Ff.v + Fg.(a*v) by HAHNBAN1:def 8
.= a*Ff.v + a*Fg.v by HAHNBAN1:def 8
.= a*(Ff.v + Fg.v) by VECTSP_1:def 2
.= a*(Ff + Fg).v by HAHNBAN1:def 3
.= a* Ffg.v by Th12;
end;
end;
registration
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f,g be homogeneousFAF Form of V,W;
cluster f+g -> homogeneousFAF;
correctness
proof
let w be Vector of V;
set Ffg = FunctionalFAF(f+g,w), Ff = FunctionalFAF(f,w);
set Fg = FunctionalFAF(g,w);
let v be Vector of W, a be Scalar of V;
thus Ffg.(a*v) = (Ff+Fg).(a*v) by Th13
.= Ff.(a*v) + Fg.(a*v) by HAHNBAN1:def 3
.= a*Ff.v + Fg.(a*v) by HAHNBAN1:def 8
.= a*Ff.v + a*Fg.v by HAHNBAN1:def 8
.= a*(Ff.v + Fg.v) by VECTSP_1:def 2
.= a*(Ff + Fg).v by HAHNBAN1:def 3
.= a* Ffg.v by Th13;
end;
end;
registration
let K be add-associative right_zeroed right_complementable associative
commutative right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f be homogeneousSAF Form of V,W;
let a be Element of K;
cluster a*f -> homogeneousSAF;
correctness
proof
let w be Vector of W;
set Ffg = FunctionalSAF(a*f,w), Ff = FunctionalSAF(f,w);
let v be Vector of V, b be Scalar of V;
thus Ffg.(b*v) = (a*Ff).(b*v) by Th14
.= a*Ff.(b*v) by HAHNBAN1:def 6
.= a*(b*Ff.v) by HAHNBAN1:def 8
.= b*(a*Ff.v) by GROUP_1:def 3
.= b*(a*Ff).v by HAHNBAN1:def 6
.= b* Ffg.v by Th14;
end;
end;
registration
let K be add-associative right_zeroed right_complementable associative
commutative right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f be homogeneousFAF Form of V,W;
let a be Element of K;
cluster a*f -> homogeneousFAF;
correctness
proof
let w be Vector of V;
set Ffg = FunctionalFAF(a*f,w), Ff = FunctionalFAF(f,w);
let v be Vector of W, b be Scalar of V;
thus Ffg.(b*v) = (a*Ff).(b*v) by Th15
.= a*Ff.(b*v) by HAHNBAN1:def 6
.= a*(b*Ff.v) by HAHNBAN1:def 8
.= b*(a*Ff.v) by GROUP_1:def 3
.= b*(a*Ff).v by HAHNBAN1:def 6
.= b* Ffg.v by Th15;
end;
end;
registration
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f be homogeneousSAF Form of V,W;
cluster -f -> homogeneousSAF;
correctness
proof
let w be Vector of W;
set Ffg = FunctionalSAF(-f,w), Ff = FunctionalSAF(f,w);
let v be Vector of V, a be Scalar of V;
thus Ffg.(a*v) = (-Ff).(a*v) by Th16
.= -Ff.(a*v) by HAHNBAN1:def 4
.= -(a*Ff.v) by HAHNBAN1:def 8
.= a*(-Ff.v) by VECTSP_1:8
.= a*(-Ff).v by HAHNBAN1:def 4
.= a*Ffg.v by Th16;
end;
end;
registration
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f be homogeneousFAF Form of V,W;
cluster -f -> homogeneousFAF;
correctness
proof
let w be Vector of V;
set Ffg = FunctionalFAF(-f,w), Ff = FunctionalFAF(f,w);
let v be Vector of W, a be Scalar of W;
thus Ffg.(a*v) = (-Ff).(a*v) by Th17
.= -Ff.(a*v) by HAHNBAN1:def 4
.= -(a*Ff.v) by HAHNBAN1:def 8
.= a*(-Ff.v) by VECTSP_1:8
.= a*(-Ff).v by HAHNBAN1:def 4
.= a*Ffg.v by Th17;
end;
end;
registration
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f,g be homogeneousSAF Form of V,W;
cluster f-g -> homogeneousSAF;
correctness;
end;
registration
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f,g be homogeneousFAF Form of V,W;
cluster f-g -> homogeneousFAF;
correctness;
end;
theorem Th26:
for K be non empty addLoopStr for V,W be non empty ModuleStr
over K for v,u be Vector of V, w be Vector of W, f be Form of V,W st f is
additiveSAF holds f.(v+u,w) = f.(v,w) + f.(u,w)
proof
let K be non empty addLoopStr;
let V,W be non empty ModuleStr over K;
let v,w be Vector of V, y be Vector of W, f be Form of V,W;
set F=FunctionalSAF(f,y);
assume f is additiveSAF;
then
A1: F is additive;
thus f.(v+w,y) = F.(v+w) by Th9
.= F.v+F.w by A1
.= f.(v,y) + F.w by Th9
.= f.(v,y) + f.(w,y) by Th9;
end;
theorem Th27:
for K be non empty addLoopStr for V,W be non empty ModuleStr
over K for v be Vector of V, u,w be Vector of W, f be Form of V,W st f is
additiveFAF holds f.(v,u+w) = f.(v,u) + f.(v,w)
proof
let K be non empty addLoopStr;
let V,W be non empty ModuleStr over K;
let v be Vector of V, y,z be Vector of W, f be Form of V,W;
set F=FunctionalFAF(f,v);
assume f is additiveFAF;
then
A1: F is additive;
thus f.(v,y+z) = F.(y+z) by Th8
.= F.y+F.z by A1
.= f.(v,y) + F.z by Th8
.= f.(v,y) + f.(v,z) by Th8;
end;
theorem Th28:
for K be right_zeroed non empty addLoopStr for V,W be non
empty ModuleStr over K for v,u be Vector of V, w,t be Vector of W, f be
additiveSAF additiveFAF Form of V,W holds f.(v+u,w+t) = f.(v,w) + f.(v,t) + (f.
(u,w) + f.(u,t))
proof
let K be right_zeroed non empty addLoopStr;
let V,W be non empty ModuleStr over K;
let v,w be Vector of V, y,z be Vector of W, f be additiveSAF additiveFAF
Form of V,W;
set v1 = f.(v,y), v3 = f.(v,z), v4 = f.(w,y), v5 = f.(w,z);
thus f.(v+w,y+z) = f.(v,y+z) + f.(w,y+z) by Th26
.= (v1 + v3) + f.(w,y+z) by Th27
.= v1 +v3 + (v4 + v5) by Th27;
end;
theorem Th29:
for K be add-associative right_zeroed right_complementable non
empty doubleLoopStr for V,W be right_zeroed non empty ModuleStr over K for f
be additiveFAF Form of V,W, v be Vector of V holds f.(v,0.W) = 0.K
proof
let F be add-associative right_zeroed right_complementable non empty
doubleLoopStr;
let V,W be right_zeroed non empty ModuleStr over F;
let f be additiveFAF Form of V,W, v be Vector of V;
f.(v,0.W) = f.(v,0.W+0.W) by RLVECT_1:def 4
.= f.(v,0.W) + f.(v,0.W) by Th27;
hence thesis by RLVECT_1:9;
end;
theorem Th30:
for K be add-associative right_zeroed right_complementable non
empty doubleLoopStr for V,W be right_zeroed non empty ModuleStr over K for f
be additiveSAF Form of V,W, w be Vector of W holds f.(0.V,w) = 0.K
proof
let F be add-associative right_zeroed right_complementable non empty
doubleLoopStr;
let V,W be right_zeroed non empty ModuleStr over F;
let f be additiveSAF Form of V,W, v be Vector of W;
f.(0.V,v) = f.(0.V+0.V,v) by RLVECT_1:def 4
.= f.(0.V,v) + f.(0.V,v) by Th26;
hence thesis by RLVECT_1:9;
end;
theorem Th31:
for K be non empty multMagma for V,W be non empty ModuleStr over
K for v be Vector of V, w be Vector of W, a be Element of K for f be Form of V,
W st f is homogeneousSAF holds f.(a*v,w) = a*f.(v,w)
proof
let K be non empty multMagma;
let V,W be non empty ModuleStr over K;
let v be Vector of V, y be Vector of W, r be Element of K, f be Form of V,W;
set F=FunctionalSAF(f,y);
assume f is homogeneousSAF;
then
A1: F is homogeneous;
thus f.(r*v,y) = F.(r*v) by Th9
.= r*F.v by A1
.= r*f.(v,y) by Th9;
end;
theorem Th32:
for K be non empty multMagma for V,W be non empty ModuleStr over
K for v be Vector of V, w be Vector of W, a be Element of K for f be Form of V,
W st f is homogeneousFAF holds f.(v,a*w) = a*f.(v,w)
proof
let K be non empty multMagma;
let V,W be non empty ModuleStr over K;
let v be Vector of V, y be Vector of W, r be Element of K, f be Form of V,W;
set F=FunctionalFAF(f,v);
assume f is homogeneousFAF;
then
A1: F is homogeneous;
thus f.(v,r*y) = F.(r*y) by Th8
.= r*F.y by A1
.= r*f.(v,y) by Th8;
end;
theorem Th33:
for K be add-associative right_zeroed right_complementable
associative left_unital distributive non empty doubleLoopStr for V,W be
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over K for f be homogeneousSAF Form of V,W, w be Vector of W holds f
.(0.V,w) = 0.K
proof
let F be add-associative right_zeroed right_complementable associative
left_unital distributive non empty doubleLoopStr;
let V,W be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over F;
let f be homogeneousSAF Form of V,W, v be Vector of W;
thus f.(0.V,v) = f.((0.F)*(0.V),v) by VECTSP10:1
.= 0.F *f.(0.V,v) by Th31
.= 0.F;
end;
theorem Th34:
for K be add-associative right_zeroed right_complementable
associative left_unital distributive non empty doubleLoopStr for V,W be
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over K for f be homogeneousFAF Form of V,W, v be Vector of V holds f
.(v,0.W) = 0.K
proof
let F be add-associative right_zeroed right_complementable associative
left_unital distributive non empty doubleLoopStr;
let V,W be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over F;
let f be homogeneousFAF Form of V,W, v be Vector of V;
thus f.(v,0.W) = f.(v,(0.F)*(0.W)) by VECTSP10:1
.= 0.F * f.(v,0.W) by Th32
.= 0.F;
end;
theorem Th35:
for K be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr for V,W
be VectSp of K for v,u be Vector of V, w be Vector of W, f be additiveSAF
homogeneousSAF Form of V,W holds f.(v-u,w) = f.(v,w) - f.(u,w)
proof
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V,W be VectSp of K, v,w be Vector of V, y be Vector of W;
let f be additiveSAF homogeneousSAF Form of V,W;
thus f.(v-w,y) = f.(v+(-w),y) by RLVECT_1:def 11
.= f.(v,y) +f.(-w,y) by Th26
.= f.(v,y) +f.((-1.K)* w,y) by VECTSP_1:14
.= f.(v,y) +(-1.K)*f.(w,y) by Th31
.= f.(v,y) + -(1.K * f.(w,y)) by VECTSP_1:9
.= f.(v,y) -(1.K * f.(w,y)) by RLVECT_1:def 11
.= f.(v,y) - f.( w,y);
end;
theorem Th36:
for K be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr for V,W
be VectSp of K for v be Vector of V, w,t be Vector of W, f be additiveFAF
homogeneousFAF Form of V,W holds f.(v,w-t) = f.(v,w) - f.(v,t)
proof
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V,W be VectSp of K, v be Vector of V, y,z be Vector of W, f be
additiveFAF homogeneousFAF Form of V,W;
thus f.(v,y-z) = f.(v, y+(-z)) by RLVECT_1:def 11
.= f.(v,y) + f.(v,-z) by Th27
.= f.(v,y) + f.(v,(-1.K)* z) by VECTSP_1:14
.= f.(v,y) + (-1.K)*f.(v,z) by Th32
.= f.(v,y) + -(1.K * f.(v,z)) by VECTSP_1:9
.= f.(v,y) -(1.K * f.(v,z)) by RLVECT_1:def 11
.= f.(v,y) - f.(v,z);
end;
theorem Th37:
for K be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr for V,W
be VectSp of K for v,u be Vector of V, w,t be Vector of W, f be bilinear-Form
of V,W holds f.(v-u,w-t) = f.(v,w) - f.(v,t) -(f.(u,w) - f.(u,t))
proof
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V,W be VectSp of K;
let v,w be Vector of V, y,z be Vector of W, f be bilinear-Form of V,W;
set v1 = f.(v,y), v3 = f.(v,z), v4 = f.(w,y), v5 = f.(w,z);
thus f.(v-w,y-z) = f.(v,y-z) - f.(w,y-z) by Th35
.= v1 - v3 - f.(w,y-z) by Th36
.= v1 - v3 - (v4 - v5) by Th36;
end;
theorem
for K be add-associative right_zeroed right_complementable associative
well-unital distributive non empty doubleLoopStr for V,W be add-associative
right_zeroed right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over K for
v,u be Vector of V, w,t be Vector of W, a,b be Element of K for f be
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
let K be add-associative right_zeroed right_complementable associative
well-unital distributive non empty doubleLoopStr;
let V,W be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over K, v,w be Vector of V, y,z be Vector of W, a,b be
Element of K;
let f be bilinear-Form of V,W;
set v1 = f.(v,y), v3 = f.(v,z), v4 = f.(w,y), v5 = f.(w,z);
thus f.(v+a*w,y+b*z) = v1 +f.(v,b*z) + (f.(a*w,y) +f.(a*w,b*z)) by Th28
.= v1 +b*v3 + (f.(a*w,y) +f.(a*w,b*z)) by Th32
.= v1 + b*v3 + (a*v4 + f.(a*w,b*z)) by Th31
.= v1 + b*v3 + (a*v4 + a*f.(w,b*z)) by Th31
.= v1 + b*v3 + (a*v4 + a*(b*v5)) by Th32;
end;
theorem
for K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr for V,W be
VectSp of K for v,u be Vector of V, w,t be Vector of W, a,b be Element of K for
f be 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
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V,W be VectSp
of K, v,w be Vector of V, y,z be Vector of W, a,b be Element of K, f be
bilinear-Form of V,W;
set v1 = f.(v,y), v3 = f.(v,z), v4 = f.(w,y), v5 = f.(w,z);
thus f.(v-a*w,y-b*z) = v1 -f.(v,b*z) - (f.(a*w,y) -f.(a*w,b*z)) by Th37
.= v1 -b*v3 - (f.(a*w,y) -f.(a*w,b*z)) by Th32
.= v1 - b*v3 - (a*v4 - f.(a*w,b*z)) by Th31
.= v1 - b*v3 - (a*v4 - a*f.(w,b*z)) by Th31
.= v1 - b*v3 - (a*v4 - a*(b*v5)) by Th32;
end;
theorem Th40:
for K be add-associative right_zeroed right_complementable non
empty doubleLoopStr, V,W be right_zeroed non empty ModuleStr over K, f be
Form of V,W st f is additiveFAF or f is additiveSAF holds f is constant iff for
v be Vector of V, w be Vector of W holds f.(v,w)=0.K
proof
let K be add-associative right_zeroed right_complementable non empty
doubleLoopStr, V,W be right_zeroed non empty ModuleStr over K, f be Form of
V,W;
A1: dom f = [: the carrier of V, the carrier of W:] by FUNCT_2:def 1;
assume
A2: f is additiveFAF or f is additiveSAF;
hereby
assume
A3: f is constant;
let v be Vector of V, w be Vector of W;
per cases by A2;
suppose
A4: f is additiveFAF;
thus f.(v,w) = f.(v,0.W) by A1,A3,BINOP_1:19
.= 0.K by A4,Th29;
end;
suppose
A5: f is additiveSAF;
thus f.(v,w) = f.(0.V,w) by A1,A3,BINOP_1:19
.= 0.K by A5,Th30;
end;
end;
hereby
assume
A6: for v be Vector of V, w be Vector of W holds f.(v,w)=0.K;
now
let x,y be object such that
A7: x in dom f and
A8: y in dom f;
consider v be Vector of V, w be Vector of W such that
A9: x = [v,w] by A7,DOMAIN_1:1;
consider s be Vector of V, t be Vector of W such that
A10: y = [s,t] by A8,DOMAIN_1:1;
thus f.x = f.(v,w) by A9
.= 0.K by A6
.=f.(s,t) by A6
.=f.y by A10;
end;
hence f is constant by FUNCT_1:def 10;
end;
end;
begin
:: Left and Right Kernel of Form. "Diagonal" Kernel of Form
definition
let K be ZeroStr;
let V,W be non empty ModuleStr over K;
let f be Form of V,W;
func leftker f -> Subset of V equals
{v where v is Vector of V : for w be
Vector of W holds f.(v,w) = 0.K};
correctness
proof
set A={v where v is Vector of V : for w be Vector of W holds f.(v,w) = 0.K
};
A c= the carrier of V
proof
let x be object;
assume x in A;
then ex v be Vector of V st v=x & for w be Vector of W holds f.(v,w)=0.K;
hence thesis;
end;
hence thesis;
end;
end;
definition
let K be ZeroStr;
let V,W be non empty ModuleStr over K;
let f be Form of V,W;
func rightker f -> Subset of W equals
{w where w is Vector of W : for v be
Vector of V holds f.(v,w) = 0.K};
correctness
proof
set A={w where w is Vector of W : for v be Vector of V holds f.(v,w) = 0.K
};
A c= the carrier of W
proof
let x be object;
assume x in A;
then
ex w be Vector of W st w=x & for v be Vector of V holds f.(v,w) = 0.K;
hence thesis;
end;
hence thesis;
end;
end;
definition
let K be ZeroStr;
let V be non empty ModuleStr over K;
let f be Form of V,V;
func diagker f -> Subset of V equals
{v where v is Vector of V : f.(v,v) =
0.K};
correctness
proof
set A = {v where v is Vector of V : f.(v,v) = 0.K};
A c= the carrier of V
proof
let x be object;
assume x in A;
then ex v be Vector of V st v=x & f.(v,v)=0.K;
hence thesis;
end;
hence thesis;
end;
end;
registration
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V be right_zeroed non empty ModuleStr over K;
let W be non empty ModuleStr over K;
let f be additiveSAF Form of V,W;
cluster leftker f -> non empty;
coherence
proof
now
let w be Vector of W;
thus f.(0.V,w) = (FunctionalSAF(f,w)).(0.V) by Th9
.= 0.K by HAHNBAN1:def 9;
end;
then 0.V in leftker f;
hence thesis;
end;
end;
registration
let K be add-associative right_zeroed right_complementable associative
well-unital distributive non empty doubleLoopStr;
let V be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over K;
let W be non empty ModuleStr over K;
let f be homogeneousSAF Form of V,W;
cluster leftker f -> non empty;
coherence
proof
now
let w be Vector of W;
thus f.(0.V,w) = (FunctionalSAF(f,w)).(0.V) by Th9
.= 0.K by HAHNBAN1:def 9;
end;
then 0.V in leftker f;
hence thesis;
end;
end;
registration
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V be non empty ModuleStr over K;
let W be right_zeroed non empty ModuleStr over K;
let f be additiveFAF Form of V,W;
cluster rightker f -> non empty;
coherence
proof
now
let v be Vector of V;
thus f.(v,0.W) = (FunctionalFAF(f,v)).(0.W) by Th8
.= 0.K by HAHNBAN1:def 9;
end;
then 0.W in rightker f;
hence thesis;
end;
end;
registration
let K be add-associative right_zeroed right_complementable associative
well-unital distributive non empty doubleLoopStr;
let V be non empty ModuleStr over K;
let W be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over K;
let f be homogeneousFAF Form of V,W;
cluster rightker f -> non empty;
coherence
proof
now
let v be Vector of V;
thus f.(v,0.W) = (FunctionalFAF(f,v)).(0.W) by Th8
.= 0.K by HAHNBAN1:def 9;
end;
then 0.W in rightker f;
hence thesis;
end;
end;
registration
let K be add-associative right_zeroed right_complementable non empty
doubleLoopStr;
let V be right_zeroed non empty ModuleStr over K;
let f be additiveFAF Form of V,V;
cluster diagker f -> non empty;
coherence
proof
f.(0.V,0.V) = 0.K by Th29;
then 0.V in diagker f;
hence thesis;
end;
end;
registration
let K be add-associative right_zeroed right_complementable non empty
doubleLoopStr;
let V be right_zeroed non empty ModuleStr over K;
let f be additiveSAF Form of V,V;
cluster diagker f -> non empty;
coherence
proof
f.(0.V,0.V) = 0.K by Th30;
then 0.V in diagker f;
hence thesis;
end;
end;
registration
let K be add-associative right_zeroed right_complementable associative
well-unital distributive non empty doubleLoopStr;
let V be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over K;
let f be homogeneousFAF Form of V,V;
cluster diagker f -> non empty;
coherence
proof
f.(0.V,0.V) = 0.K by Th34;
then 0.V in diagker f;
hence thesis;
end;
end;
registration
let K be add-associative right_zeroed right_complementable associative
well-unital distributive non empty doubleLoopStr;
let V be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative
scalar-unital non
empty ModuleStr over K;
let f be homogeneousSAF Form of V,V;
cluster diagker f -> non empty;
coherence
proof
f.(0.V,0.V) = 0.K by Th33;
then 0.V in diagker f;
hence thesis;
end;
end;
theorem
for K be ZeroStr, V be non empty ModuleStr over K for f be Form of V,V
holds leftker f c= diagker f & rightker f c= diagker f
proof
let K be ZeroStr, V be non empty ModuleStr over K, f be Form of V,V;
thus leftker f c= diagker f
proof
let x be object;
assume x in leftker f;
then consider v be Vector of V such that
A1: v=x and
A2: for w be Vector of V holds f.(v,w)=0.K;
f.(v,v) = 0.K by A2;
hence thesis by A1;
end;
let x be object;
assume x in rightker f;
then consider v be Vector of V such that
A3: v=x and
A4: for w be Vector of V holds f.(w,v)=0.K;
f.(v,v) = 0.K by A4;
hence thesis by A3;
end;
theorem Th42:
for K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr for V,W be non empty ModuleStr
over K for f be additiveSAF homogeneousSAF Form of V,W holds leftker f is
linearly-closed
proof
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f be additiveSAF homogeneousSAF Form of V,W;
set V1 = leftker f;
thus for v,u be Vector of V st v in V1 & u in V1 holds v + u in V1
proof
let v,u be Vector of V;
assume that
A1: v in V1 and
A2: u in V1;
consider u1 be Vector of V such that
A3: u1= u and
A4: for w be Vector of W holds f.(u1,w)=0.K by A2;
consider v1 be Vector of V such that
A5: v1= v and
A6: for w be Vector of W holds f.(v1,w)=0.K by A1;
now
let w be Vector of W;
thus f.(v+u,w) = f.(v1,w) + f.(u1,w) by A5,A3,Th26
.= 0.K + f.(u1,w) by A6
.= 0.K + 0.K by A4
.= 0.K by RLVECT_1:def 4;
end;
hence thesis;
end;
let a be Element of K, v be Vector of V;
assume v in V1;
then consider v1 be Vector of V such that
A7: v1= v and
A8: for w be Vector of W holds f.(v1,w)=0.K;
now
let w be Vector of W;
thus f.(a*v,w) = a*f.(v1,w) by A7,Th31
.= a*0.K by A8
.= 0.K;
end;
hence thesis;
end;
theorem Th43:
for K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr for V,W be non empty ModuleStr
over K for f be additiveFAF homogeneousFAF Form of V,W holds rightker f is
linearly-closed
proof
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V,W be non empty ModuleStr over K;
let f be additiveFAF homogeneousFAF Form of V,W;
set V1 = rightker f;
thus for v,u be Vector of W st v in V1 & u in V1 holds v + u in V1
proof
let v,u be Vector of W;
assume that
A1: v in V1 and
A2: u in V1;
consider u1 be Vector of W such that
A3: u1= u and
A4: for w be Vector of V holds f.(w,u1)=0.K by A2;
consider v1 be Vector of W such that
A5: v1= v and
A6: for w be Vector of V holds f.(w,v1)=0.K by A1;
now
let w be Vector of V;
thus f.(w,v+u) = f.(w,v1) + f.(w,u1) by A5,A3,Th27
.= 0.K + f.(w,u1) by A6
.= 0.K + 0.K by A4
.= 0.K by RLVECT_1:def 4;
end;
hence thesis;
end;
let a be Element of K, v be Vector of W;
assume v in V1;
then consider v1 be Vector of W such that
A7: v1= v and
A8: for w be Vector of V holds f.(w,v1)=0.K;
now
let w be Vector of V;
thus f.(w,a*v) = a*f.(w,v1) by A7,Th32
.= a*0.K by A8
.= 0.K;
end;
hence thesis;
end;
definition
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be VectSp of K, W be non empty ModuleStr over K;
let f be additiveSAF homogeneousSAF Form of V,W;
func LKer f -> strict non empty Subspace of V means
:Def18:
the carrier of it = leftker f;
existence by Th42,VECTSP_4:34;
uniqueness by VECTSP_4:29;
end;
definition
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be non empty ModuleStr over K, W be VectSp of K;
let f be additiveFAF homogeneousFAF Form of V,W;
func RKer f -> strict non empty Subspace of W means
:Def19:
the carrier of it = rightker f;
existence by Th43,VECTSP_4:34;
uniqueness by VECTSP_4:29;
end;
definition
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be VectSp of K, W be non empty ModuleStr over K;
let f be additiveSAF homogeneousSAF Form of V,W;
func LQForm(f) -> additiveSAF homogeneousSAF Form of VectQuot(V,LKer f),W
means
:Def20:
for A be Vector of VectQuot(V,LKer(f)), w be Vector of W, v be
Vector of V st A = v + LKer(f) holds it.(A,w) = f.(v,w);
existence
proof
set L = LKer(f), vq = VectQuot(V,L), C = CosetSet(V,L), aC = addCoset(V,L)
, mC = lmultCoset(V,L);
defpred P[set,set,set] means for a be Vector of V st $1 = a+L holds $3 = f
.(a,$2);
A1: now
let A be Vector of vq, w0 be Vector of W;
consider a be Vector of V such that
A2: A = a+L by VECTSP10:22;
take y = f.(a,w0);
now
let a1 be Vector of V;
assume A = a1+L;
then a in a1+L by A2,VECTSP_4:44;
then consider w be Vector of V such that
A3: w in L and
A4: a = a1 + w by VECTSP_4:42;
w in the carrier of L by A3;
then w in leftker f by Def18;
then
A5: ex aa be Vector of V st aa=w & for ww be Vector of W holds f.(aa,
ww) =0.K;
thus y = f.(a1,w0)+f.(w,w0) by A4,Th26
.= f.(a1,w0) +0.K by A5
.= f.(a1,w0) by RLVECT_1:def 4;
end;
hence P[A,w0,y];
end;
consider ff be Function of [:the carrier of vq,the carrier of W:], the
carrier of K such that
A6: for A be Vector of vq, w be Vector of W holds P[A,w,ff.(A,w)]
from BINOP_1:sch 3(A1);
reconsider ff as Form of vq,W;
A7: C = the carrier of vq by VECTSP10:def 6;
now
let w be Vector of W;
set ffw = FunctionalSAF(ff,w);
now
let A,B be Vector of vq;
consider a be Vector of V such that
A8: A = a+L by VECTSP10:22;
consider b be Vector of V such that
A9: B = b+L by VECTSP10:22;
A10: the addF of vq = addCoset(V,L) & aC.(A,B) =a+b+L by A7,A8,A9,
VECTSP10:def 3,def 6;
thus ffw.(A+B) = ff.(A+B,w) by Th9
.= f.(a+b,w) by A6,A10,RLVECT_1:2
.= f.(a,w) + f.(b,w) by Th26
.= ff.(A,w) + f.(b,w) by A6,A8
.= ff.(A,w) + ff.(B,w) by A6,A9
.= ffw.A + ff.(B,w) by Th9
.= ffw.A + ffw.B by Th9;
end;
hence ffw is additive;
end;
then reconsider ff as additiveSAF Form of vq,W by Def12;
now
let w be Vector of W;
set ffw = FunctionalSAF(ff,w);
now
let A be Vector of vq, r be Element of K;
consider a be Vector of V such that
A11: A = a+L by VECTSP10:22;
A12: the lmult of vq = lmultCoset(V,L) & mC.(r,A) =r*a+L by A7,A11,
VECTSP10:def 5,def 6;
thus ffw.(r*A) = ff.(r*A,w) by Th9
.= f.(r*a,w) by A6,A12
.= r*f.(a,w) by Th31
.= r*ff.(A,w) by A6,A11
.= r*ffw.A by Th9;
end;
hence ffw is homogeneous;
end;
then reconsider ff as additiveSAF homogeneousSAF Form of vq,W by Def14;
take ff;
thus thesis by A6;
end;
uniqueness
proof
set L = LKer(f), vq = VectQuot(V,L);
let f1,f2 be additiveSAF homogeneousSAF Form of vq,W such that
A13: for A be Vector of vq, w be Vector of W, a be Vector of V st A =
a + LKer(f) holds f1.(A,w) = f.(a,w) and
A14: for A be Vector of vq, w be Vector of W, a be Vector of V st A =
a + LKer(f) holds f2.(A,w) = f.(a,w);
now
let A be Vector of vq, w be Vector of W;
consider a be Vector of V such that
A15: A = a + L by VECTSP10:22;
thus f1.(A,w) = f.(a,w) by A13,A15
.= f2.(A,w) by A14,A15;
end;
hence thesis;
end;
end;
definition
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be non empty ModuleStr over K, W be VectSp of K;
let f be additiveFAF homogeneousFAF Form of V,W;
func RQForm(f) -> additiveFAF homogeneousFAF Form of V,VectQuot(W,RKer f)
means
:Def21:
for A be Vector of VectQuot(W,RKer(f)), v be Vector of V, w be
Vector of W st A = w + RKer(f) holds it.(v,A) = f.(v,w);
existence
proof
set L = RKer(f), vq = VectQuot(W,L), C = CosetSet(W,L), aC = addCoset(W,L)
, mC = lmultCoset(W,L);
defpred P[set,set,set] means for w be Vector of W st $2 = w+L holds $3 = f
.($1,w);
A1: now
let v0 be Vector of V, A be Vector of vq;
consider a be Vector of W such that
A2: A = a+L by VECTSP10:22;
take y = f.(v0,a);
now
let a1 be Vector of W;
assume A = a1+L;
then a in a1+L by A2,VECTSP_4:44;
then consider w be Vector of W such that
A3: w in L and
A4: a = a1 + w by VECTSP_4:42;
w in the carrier of L by A3;
then w in rightker f by Def19;
then
A5: ex aa be Vector of W st aa=w & for vv be Vector of V holds f.(vv,
aa) =0.K;
thus y = f.(v0,a1)+f.(v0,w) by A4,Th27
.= f.(v0,a1) +0.K by A5
.= f.(v0,a1) by RLVECT_1:def 4;
end;
hence P[v0,A,y];
end;
consider ff be Function of [:the carrier of V,the carrier of vq:], the
carrier of K such that
A6: for v be Vector of V, A be Vector of vq holds P[v,A,ff.(v,A)]
from BINOP_1:sch 3(A1);
reconsider ff as Form of V,vq;
A7: C = the carrier of vq by VECTSP10:def 6;
now
let v be Vector of V;
set ffw = FunctionalFAF(ff,v);
now
let A,B be Vector of vq;
consider a be Vector of W such that
A8: A = a+L by VECTSP10:22;
consider b be Vector of W such that
A9: B = b+L by VECTSP10:22;
A10: the addF of vq = addCoset(W,L) & aC.(A,B) =a+b+L by A7,A8,A9,
VECTSP10:def 3,def 6;
thus ffw.(A+B) = ff.(v,A+B) by Th8
.= f.(v,a+b) by A6,A10,RLVECT_1:2
.= f.(v,a) + f.(v,b) by Th27
.= ff.(v,A) + f.(v,b) by A6,A8
.= ff.(v,A) + ff.(v,B) by A6,A9
.= ffw.A + ff.(v,B) by Th8
.= ffw.A + ffw.B by Th8;
end;
hence ffw is additive;
end;
then reconsider ff as additiveFAF Form of V,vq by Def11;
now
let v be Vector of V;
set ffw = FunctionalFAF(ff,v);
now
let A be Vector of vq, r be Element of K;
consider a be Vector of W such that
A11: A = a+L by VECTSP10:22;
A12: the lmult of vq = lmultCoset(W,L) & mC.(r,A) =r*a+L by A7,A11,
VECTSP10:def 5,def 6;
thus ffw.(r*A) = ff.(v,r*A) by Th8
.= f.(v,r*a) by A6,A12
.= r*f.(v,a) by Th32
.= r*ff.(v,A) by A6,A11
.= r*ffw.A by Th8;
end;
hence ffw is homogeneous;
end;
then reconsider ff as additiveFAF homogeneousFAF Form of V,vq by Def13;
take ff;
thus thesis by A6;
end;
uniqueness
proof
set L = RKer(f), vq = VectQuot(W,L);
let f1,f2 be additiveFAF homogeneousFAF Form of V,vq such that
A13: for A be Vector of vq, v be Vector of V, a be Vector of W st A =
a + RKer(f) holds f1.(v,A) = f.(v,a) and
A14: for A be Vector of vq, v be Vector of V, a be Vector of W st A =
a + RKer(f) holds f2.(v,A) = f.(v,a);
now
let v be Vector of V, A be Vector of vq;
consider a be Vector of W such that
A15: A = a + L by VECTSP10:22;
thus f1.(v,A) = f.(v,a) by A13,A15
.= f2.(v,A) by A14,A15;
end;
hence thesis;
end;
end;
registration
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V,W be VectSp of K;
let f be bilinear-Form of V,W;
cluster LQForm(f) -> additiveFAF homogeneousFAF;
coherence
proof
set lf = LQForm(f);
thus LQForm(f) is additiveFAF
proof
let A be Vector of VectQuot(V,LKer(f));
set flf = FunctionalFAF(lf,A);
consider v be Vector of V such that
A1: A = v + LKer(f) by VECTSP10:22;
let w,t be Vector of W;
thus flf.(w+t) = lf.(A,w+t) by Th8
.= f.(v,w+t) by A1,Def20
.= f.(v,w)+f.(v,t) by Th27
.= lf.(A,w)+ f.(v,t) by A1,Def20
.= lf.(A,w)+ lf.(A,t) by A1,Def20
.= flf.w+ lf.(A,t) by Th8
.= flf.w + flf.t by Th8;
end;
let A be Vector of VectQuot(V,LKer(f));
set flf = FunctionalFAF(lf,A);
consider v be Vector of V such that
A2: A = v + LKer(f) by VECTSP10:22;
let w be Vector of W, r be Scalar of W;
thus flf.(r*w) = lf.(A,r*w) by Th8
.= f.(v,r*w) by A2,Def20
.= r*f.(v,w) by Th32
.= r*lf.(A,w) by A2,Def20
.= r*flf.w by Th8;
end;
cluster RQForm(f) -> additiveSAF homogeneousSAF;
coherence
proof
set lf = RQForm(f);
thus RQForm(f) is additiveSAF
proof
let A be Vector of VectQuot(W,RKer(f));
set flf = FunctionalSAF(lf,A);
consider w be Vector of W such that
A3: A = w + RKer(f) by VECTSP10:22;
let v,t be Vector of V;
thus flf.(v+t) = lf.(v+t,A) by Th9
.= f.(v+t,w) by A3,Def21
.= f.(v,w)+f.(t,w) by Th26
.= lf.(v,A)+ f.(t,w) by A3,Def21
.= lf.(v,A)+ lf.(t,A) by A3,Def21
.= flf.v+ lf.(t,A) by Th9
.= flf.v + flf.t by Th9;
end;
let A be Vector of VectQuot(W,RKer(f));
set flf = FunctionalSAF(lf,A);
consider w be Vector of W such that
A4: A = w + RKer(f) by VECTSP10:22;
let v be Vector of V, r be Scalar of V;
thus flf.(r*v) = lf.(r*v,A) by Th9
.= f.(r*v,w) by A4,Def21
.= r*f.(v,w) by Th31
.= r*lf.(v,A) by A4,Def21
.= r*flf.v by Th9;
end;
end;
definition
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty 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
:Def22:
for A be Vector of VectQuot(V,LKer f), B be Vector of VectQuot(W,
RKer(f)) for v be Vector of V, w be Vector of W st A = v + LKer f & B = w +
RKer f holds it.(A,B)= f.(v,w);
existence
proof
set L = LKer(f), vq = VectQuot(V,L), Cv = CosetSet(V,L), aCv = addCoset(V,
L), mCv = lmultCoset(V,L), R = RKer(f), wq = VectQuot(W,R), Cw = CosetSet(W,R),
aCw = addCoset(W,R), mCw = lmultCoset(W,R);
defpred P[set,set,set] means for v be Vector of V, w be Vector of W st $1
= v+L & $2= w+R holds $3 = f.(v,w);
A1: now
let A be Vector of vq, B be Vector of wq;
consider a be Vector of V such that
A2: A = a+L by VECTSP10:22;
consider b be Vector of W such that
A3: B = b+R by VECTSP10:22;
take y = f.(a,b);
now
let a1 be Vector of V;
let b1 be Vector of W;
assume A = a1+L;
then a in a1+L by A2,VECTSP_4:44;
then consider vv be Vector of V such that
A4: vv in L and
A5: a = a1 + vv by VECTSP_4:42;
vv in the carrier of L by A4;
then vv in leftker f by Def18;
then
A6: ex aa be Vector of V st aa=vv & for w0 be Vector of W holds f.(aa,
w0) =0.K;
assume B = b1+R;
then b in b1+R by A3,VECTSP_4:44;
then consider ww be Vector of W such that
A7: ww in R and
A8: b = b1 + ww by VECTSP_4:42;
ww in the carrier of R by A7;
then ww in rightker f by Def19;
then
A9: ex bb be Vector of W st bb=ww & for v0 be Vector of V holds f.(v0,
bb) =0.K;
thus y = f.(a1,b1)+f.(a1,ww) + (f.(vv,b1)+f.(vv,ww)) by A5,A8,Th28
.=f.(a1,b1)+0.K + (f.(vv,b1)+f.(vv,ww)) by A9
.= f.(a1,b1) +0.K + (0.K+f.(vv,ww)) by A6
.= f.(a1,b1) + (0.K+f.(vv,ww)) by RLVECT_1:def 4
.= f.(a1,b1) + f.(vv,ww) by RLVECT_1:4
.= f.(a1,b1) + 0.K by A6
.= f.(a1,b1) by RLVECT_1:def 4;
end;
hence P[A, B, y];
end;
consider ff be Function of [:the carrier of vq,the carrier of wq:], the
carrier of K such that
A10: for A be Vector of vq, B be Vector of wq holds P[A,B,ff.(A,B)]
from BINOP_1:sch 3(A1);
reconsider ff as Form of vq,wq;
A11: Cv = the carrier of vq by VECTSP10:def 6;
A12: now
let ww be Vector of wq;
consider w be Vector of W such that
A13: ww= w+R by VECTSP10:22;
set ffw = FunctionalSAF(ff,ww);
now
let A be Vector of vq, r be Element of K;
consider a be Vector of V such that
A14: A = a+L by VECTSP10:22;
A15: the lmult of vq = mCv & mCv.(r,A) =r*a+L by A11,A14,VECTSP10:def 5
,def 6;
thus ffw.(r*A) = ff.(r*A,ww) by Th9
.= f.(r*a,w) by A10,A13,A15
.= r*f.(a,w) by Th31
.= r*ff.(A,ww) by A10,A13,A14
.= r*ffw.A by Th9;
end;
hence ffw is homogeneous;
end;
A16: Cw = the carrier of wq by VECTSP10:def 6;
A17: now
let vv be Vector of vq;
consider v be Vector of V such that
A18: vv= v+L by VECTSP10:22;
set ffv = FunctionalFAF(ff,vv);
now
let A be Vector of wq, r be Element of K;
consider a be Vector of W such that
A19: A = a+R by VECTSP10:22;
A20: the lmult of wq = mCw & mCw.(r,A) =r*a+R by A16,A19,VECTSP10:def 5
,def 6;
thus ffv.(r*A) = ff.(vv,r*A) by Th8
.= f.(v,r*a) by A10,A18,A20
.= r*f.(v,a) by Th32
.= r*ff.(vv,A) by A10,A18,A19
.= r*ffv.A by Th8;
end;
hence ffv is homogeneous;
end;
A21: now
let ww be Vector of wq;
consider w be Vector of W such that
A22: ww= w+R by VECTSP10:22;
set ffw = FunctionalSAF(ff,ww);
now
let A,B be Vector of vq;
consider a be Vector of V such that
A23: A = a+L by VECTSP10:22;
consider b be Vector of V such that
A24: B = b+L by VECTSP10:22;
A25: the addF of vq = aCv & aCv.(A,B) =a+b+L by A11,A23,A24,VECTSP10:def 3
,def 6;
thus ffw.(A+B) = ff.(A+B,ww) by Th9
.= f.(a+b,w) by A10,A22,A25,RLVECT_1:2
.= f.(a,w) + f.(b,w) by Th26
.= ff.(A,ww) + f.(b,w) by A10,A22,A23
.= ff.(A,ww) + ff.(B,ww) by A10,A22,A24
.= ffw.A + ff.(B,ww) by Th9
.= ffw.A + ffw.B by Th9;
end;
hence ffw is additive;
end;
now
let vv be Vector of vq;
consider v be Vector of V such that
A26: vv= v+L by VECTSP10:22;
set ffv = FunctionalFAF(ff,vv);
now
let A,B be Vector of wq;
consider a be Vector of W such that
A27: A = a+R by VECTSP10:22;
consider b be Vector of W such that
A28: B = b+R by VECTSP10:22;
A29: the addF of wq = aCw & aCw.(A,B) =a+b+R by A16,A27,A28,VECTSP10:def 3
,def 6;
thus ffv.(A+B) = ff.(vv,A+B) by Th8
.= f.(v,a+b) by A10,A26,A29,RLVECT_1:2
.= f.(v,a) + f.(v,b) by Th27
.= ff.(vv,A) + f.(v,b) by A10,A26,A27
.= ff.(vv,A) + ff.(vv,B) by A10,A26,A28
.= ffv.A + ff.(vv,B) by Th8
.= ffv.A + ffv.B by Th8;
end;
hence ffv is additive;
end;
then reconsider ff as bilinear-Form of vq,wq by A21,A12,A17,Def11,Def12
,Def13,Def14;
take ff;
thus thesis by A10;
end;
uniqueness
proof
set L = LKer(f), vq = VectQuot(V,L), R = RKer(f), wq = VectQuot(W,R);
let f1,f2 be bilinear-Form of vq,wq;
assume that
A30: for A be Vector of vq, B be Vector of wq for v be Vector of V, w
be Vector of W st A = v + L & B = w + R holds f1.(A,B)= f.(v,w) and
A31: for A be Vector of vq, B be Vector of wq for v be Vector of V, w
be Vector of W st A = v + L & B = w + R holds f2.(A,B)= f.(v,w);
now
let A be Vector of vq, B be Vector of wq;
consider a be Vector of V such that
A32: A = a + L by VECTSP10:22;
consider b be Vector of W such that
A33: B = b + R by VECTSP10:22;
thus f1.(A,B) = f.(a,b) by A30,A32,A33
.= f2.(A,B) by A31,A32,A33;
end;
hence thesis;
end;
end;
theorem Th44:
for K be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr for V be
VectSp of K, W be non empty ModuleStr over K for f be additiveSAF
homogeneousSAF Form of V,W holds rightker f = rightker (LQForm f)
proof
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be VectSp of K, W be non empty ModuleStr over K;
let f be additiveSAF homogeneousSAF Form of V,W;
set lf = LQForm(f), qv = VectQuot(V,LKer f);
thus rightker f c= rightker (LQForm f)
proof
let x be object;
assume x in rightker f;
then consider w be Vector of W such that
A1: x=w and
A2: for v be Vector of V holds f.(v,w) = 0.K;
now
let A be Vector of qv;
consider v be Vector of V such that
A3: A = v+LKer f by VECTSP10:22;
thus lf.(A,w) = f.(v,w) by A3,Def20
.= 0.K by A2;
end;
hence thesis by A1;
end;
let x be object;
assume x in rightker lf;
then consider w be Vector of W such that
A4: x=w and
A5: for A be Vector of qv holds lf.(A,w) = 0.K;
now
let v be Vector of V;
reconsider A = v + LKer f as Vector of qv by VECTSP10:23;
thus f.(v,w) = lf.(A,w) by Def20
.= 0.K by A5;
end;
hence thesis by A4;
end;
theorem Th45:
for K be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr for V be
non empty ModuleStr over K, W be VectSp of K for f be additiveFAF
homogeneousFAF Form of V,W holds leftker f = leftker (RQForm f)
proof
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be non empty ModuleStr over K, W be VectSp of K;
let f be additiveFAF homogeneousFAF Form of V,W;
set rf = RQForm(f), qw = VectQuot(W,RKer f);
thus leftker f c= leftker (RQForm f)
proof
let x be object;
assume x in leftker f;
then consider v be Vector of V such that
A1: x=v and
A2: for w be Vector of W holds f.(v,w) = 0.K;
now
let A be Vector of qw;
consider w be Vector of W such that
A3: A = w+RKer f by VECTSP10:22;
thus rf.(v,A) = f.(v,w) by A3,Def21
.= 0.K by A2;
end;
hence thesis by A1;
end;
let x be object;
assume x in leftker rf;
then consider v be Vector of V such that
A4: x=v and
A5: for A be Vector of qw holds rf.(v,A) = 0.K;
now
let w be Vector of W;
reconsider A = w + RKer f as Vector of qw by VECTSP10:23;
thus f.(v,w) = rf.(v,A) by Def21
.= 0.K by A5;
end;
hence thesis by A4;
end;
theorem Th46:
for K be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr for V,W
be VectSp of K, f be bilinear-Form of V,W holds RKer f = RKer (LQForm f)
proof
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V,W be VectSp of K, f be bilinear-Form of V,W;
the carrier of (RKer f) = rightker f by Def19
.= rightker (LQForm f) by Th44
.= the carrier of (RKer (LQForm f)) by Def19;
hence thesis by VECTSP_4:29;
end;
theorem Th47:
for K be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr for V,W
be VectSp of K, f be bilinear-Form of V,W holds LKer f = LKer (RQForm f)
proof
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V,W be VectSp of K, f be bilinear-Form of V,W;
the carrier of (LKer f) = leftker f by Def18
.= leftker (RQForm f) by Th45
.= the carrier of (LKer (RQForm f)) by Def18;
hence thesis by VECTSP_4:29;
end;
theorem Th48:
for K be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr for V,W
be VectSp of K, f be bilinear-Form of V,W holds QForm(f) = RQForm(LQForm(f)) &
QForm(f) = LQForm(RQForm(f))
proof
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V,W be VectSp of K, f be bilinear-Form of V,W;
set L = LKer(f), vq = VectQuot(V,L), R = RKer(f), wq = VectQuot(W,R), RL =
RKer(LQForm(f)), wqr = VectQuot(W,RL), LR = LKer(RQForm(f)), vql = VectQuot(V,
LR);
A1: dom QForm(f) = [:the carrier of vq, the carrier of wq:] by FUNCT_2:def 1;
A2: now
let x be object;
assume x in dom QForm(f);
then consider A be Vector of vq, B be Vector of wq such that
A3: x=[A,B] by DOMAIN_1:1;
consider w be Vector of W such that
A4: B = w + R by VECTSP10:22;
A5: R = RL by Th46;
consider v be Vector of V such that
A6: A = v + L by VECTSP10:22;
thus (QForm(f)).x = (QForm(f)).(A,B) by A3
.= f.(v,w) by A6,A4,Def22
.= (LQForm(f)).(A,w) by A6,Def20
.=(RQForm(LQForm(f))).(A,B) by A4,A5,Def21
.=(RQForm(LQForm(f))).x by A3;
end;
dom RQForm (LQForm(f))= [:the carrier of vq, the carrier of wqr:] & the
carrier of wqr = the carrier of wq by Th46,FUNCT_2:def 1;
hence QForm(f) = RQForm(LQForm(f)) by A1,A2,FUNCT_1:2;
A7: now
let x be object;
assume x in dom QForm(f);
then consider A be Vector of vq, B be Vector of wq such that
A8: x=[A,B] by DOMAIN_1:1;
consider w be Vector of W such that
A9: B = w + R by VECTSP10:22;
A10: L = LR by Th47;
consider v be Vector of V such that
A11: A = v + L by VECTSP10:22;
thus (QForm(f)).x = (QForm(f)).(A,B) by A8
.= f.(v,w) by A11,A9,Def22
.= (RQForm(f)).(v,B) by A9,Def21
.=(LQForm(RQForm(f))).(A,B) by A11,A10,Def20
.=(LQForm(RQForm(f))).x by A8;
end;
dom LQForm (RQForm(f))= [:the carrier of vql, the carrier of wq:] & the
carrier of vql = the carrier of vq by Th47,FUNCT_2:def 1;
hence thesis by A1,A7,FUNCT_1:2;
end;
theorem Th49:
for K be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr for V,W
be VectSp of K, f be 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
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V,W be VectSp of K, f be bilinear-Form of V,W;
set vq = VectQuot(V,LKer(f)), wq = VectQuot(W,RKer(f)), wqr = VectQuot(W,
RKer(LQForm(f))), vql = VectQuot(V,LKer(RQForm(f)));
set rlf = RQForm (LQForm(f)) , qf = QForm(f), lrf = LQForm (RQForm(f));
thus leftker qf c= leftker rlf
proof
let x be object;
assume x in leftker qf;
then consider vv be Vector of vq such that
A1: x=vv and
A2: for ww be Vector of wq holds qf.(vv,ww)=0.K;
now
let ww be Vector of wqr;
reconsider w = ww as Vector of wq by Th46;
thus rlf.(vv,ww) = qf.(vv,w) by Th48
.= 0.K by A2;
end;
hence thesis by A1;
end;
thus leftker rlf c= leftker qf
proof
let x be object;
assume x in leftker rlf;
then consider vv be Vector of vq such that
A3: x=vv and
A4: for ww be Vector of wqr holds rlf.(vv,ww)=0.K;
now
let ww be Vector of wq;
reconsider w = ww as Vector of wqr by Th46;
thus qf.(vv,ww) = rlf.(vv,w) by Th48
.= 0.K by A4;
end;
hence thesis by A3;
end;
thus rightker qf c= rightker rlf
proof
let x be object;
assume x in rightker qf;
then consider ww be Vector of wq such that
A5: x=ww and
A6: for vv be Vector of vq holds qf.(vv,ww)=0.K;
reconsider w = ww as Vector of wqr by Th46;
now
let vv be Vector of vq;
thus rlf.(vv,w) = qf.(vv,ww) by Th48
.= 0.K by A6;
end;
hence thesis by A5;
end;
thus rightker rlf c= rightker qf
proof
let x be object;
assume x in rightker rlf;
then consider ww be Vector of wqr such that
A7: x=ww and
A8: for vv be Vector of vq holds rlf.(vv,ww)=0.K;
reconsider w = ww as Vector of wq by Th46;
now
let vv be Vector of vq;
thus qf.(vv,w) = rlf.(vv,ww) by Th48
.= 0.K by A8;
end;
hence thesis by A7;
end;
thus leftker qf c= leftker lrf
proof
let x be object;
assume x in leftker qf;
then consider vv be Vector of vq such that
A9: x=vv and
A10: for ww be Vector of wq holds qf.(vv,ww)=0.K;
reconsider v=vv as Vector of vql by Th47;
now
let ww be Vector of wq;
thus lrf.(v,ww) = qf.(vv,ww) by Th48
.= 0.K by A10;
end;
hence thesis by A9;
end;
thus leftker lrf c= leftker qf
proof
let x be object;
assume x in leftker lrf;
then consider vv be Vector of vql such that
A11: x=vv and
A12: for ww be Vector of wq holds lrf.(vv,ww)=0.K;
reconsider v=vv as Vector of vq by Th47;
now
let ww be Vector of wq;
thus qf.(v,ww) = lrf.(vv,ww) by Th48
.= 0.K by A12;
end;
hence thesis by A11;
end;
thus rightker qf c= rightker lrf
proof
let x be object;
assume x in rightker qf;
then consider ww be Vector of wq such that
A13: x=ww and
A14: for vv be Vector of vq holds qf.(vv,ww)=0.K;
now
let vv be Vector of vql;
reconsider v = vv as Vector of vq by Th47;
thus lrf.(vv,ww) = qf.(v,ww) by Th48
.= 0.K by A14;
end;
hence thesis by A13;
end;
let x be object;
assume x in rightker lrf;
then consider ww be Vector of wq such that
A15: x=ww and
A16: for vv be Vector of vql holds lrf.(vv,ww)=0.K;
now
let vv be Vector of vq;
reconsider v = vv as Vector of vql by Th47;
thus qf.(vv,ww) = lrf.(v,ww) by Th48
.= 0.K by A16;
end;
hence thesis by A15;
end;
theorem Th50:
for K be add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr for V,W be non empty ModuleStr over K
for f be Functional of V, g be Functional of W holds ker f c= leftker
FormFunctional(f,g)
proof
let K be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr, V, W be non empty ModuleStr over K, f be Functional of V,
g be Functional of W;
set fg = FormFunctional(f,g);
A1: ker f = {v where v is Vector of V : f.v = 0.K} by VECTSP10:def 9;
let x be object;
assume x in ker f;
then consider v be Vector of V such that
A2: x=v and
A3: f.v=0.K by A1;
now
let w be Vector of W;
thus fg.(v,w) = f.v*g.w by Def10
.= 0.K by A3;
end;
hence thesis by A2;
end;
theorem Th51:
for K be add-associative right_zeroed right_complementable
associative commutative well-unital almost_left_invertible distributive non
empty doubleLoopStr for V, W be non empty ModuleStr over K for f be Functional
of V, g be Functional of W st g <> 0Functional(W) holds leftker FormFunctional(
f,g) = ker f
proof
let K be add-associative right_zeroed right_complementable associative
commutative well-unital almost_left_invertible distributive non empty
doubleLoopStr, V, W be non empty ModuleStr over K, f be Functional of V, g be
Functional of W;
set fg = FormFunctional(f,g);
assume
A1: g <> 0Functional(W);
A2: ker f = {v where v is Vector of V : f.v = 0.K} by VECTSP10:def 9;
thus leftker fg c= ker f
proof
let x be object;
assume x in leftker fg;
then consider v be Vector of V such that
A3: x=v and
A4: for w be Vector of W holds fg.(v,w) = 0.K;
assume not x in ker f;
then
A5: f.v <> 0.K by A2,A3;
now
let w be Vector of W;
f.v*g.w = fg.(v,w) by Def10
.= 0.K by A4;
hence g.w = 0.K by A5,VECTSP_1:12
.= (0Functional(W)).w by HAHNBAN1:14;
end;
hence contradiction by A1,FUNCT_2:63;
end;
thus thesis by Th50;
end;
theorem Th52:
for K be add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr for V,W be non empty ModuleStr over K
for f be Functional of V, g be Functional of W holds ker g c= rightker
FormFunctional(f,g)
proof
let K be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr, V, W be non empty ModuleStr over K, f be Functional of V,
g be Functional of W;
set fg = FormFunctional(f,g);
A1: ker g = {w where w is Vector of W : g.w = 0.K} by VECTSP10:def 9;
let x be object;
assume x in ker g;
then consider w be Vector of W such that
A2: x=w and
A3: g.w=0.K by A1;
now
let v be Vector of V;
thus fg.(v,w) = f.v*g.w by Def10
.= 0.K by A3;
end;
hence thesis by A2;
end;
theorem Th53:
for K be add-associative right_zeroed right_complementable
associative commutative well-unital almost_left_invertible distributive non
empty doubleLoopStr for V, W be non empty ModuleStr over K for f be Functional
of V, g be Functional of W st f <> 0Functional(V) holds rightker FormFunctional
(f,g) = ker g
proof
let K be add-associative right_zeroed right_complementable associative
commutative well-unital almost_left_invertible distributive non empty
doubleLoopStr, V, W be non empty ModuleStr over K, f be Functional of V, g be
Functional of W;
set fg = FormFunctional(f,g);
assume
A1: f <> 0Functional(V);
A2: ker g = {w where w is Vector of W : g.w = 0.K} by VECTSP10:def 9;
thus rightker fg c= ker g
proof
let x be object;
assume x in rightker fg;
then consider w be Vector of W such that
A3: x=w and
A4: for v be Vector of V holds fg.(v,w) = 0.K;
assume not x in ker g;
then
A5: g.w <> 0.K by A2,A3;
now
let v be Vector of V;
f.v*g.w = fg.(v,w) by Def10
.= 0.K by A4;
hence f.v = 0.K by A5,VECTSP_1:12
.= (0Functional(V)).v by HAHNBAN1:14;
end;
hence contradiction by A1,FUNCT_2:63;
end;
thus thesis by Th52;
end;
theorem Th54:
for K be add-associative right_zeroed right_complementable
commutative Abelian associative well-unital distributive almost_left_invertible
non empty doubleLoopStr for V be VectSp of K, W be non empty ModuleStr over K
for f be linear-Functional of V, g be Functional of W st g <> 0Functional(W)
holds LKer FormFunctional(f,g) = Ker f & LQForm(FormFunctional(f,g)) =
FormFunctional(CQFunctional(f),g)
proof
let K be add-associative right_zeroed right_complementable commutative
Abelian associative well-unital distributive almost_left_invertible non empty
doubleLoopStr, V be VectSp of K, W be non empty ModuleStr over K, f be
linear-Functional of V, g be Functional of W;
set fg = FormFunctional(f,g), cf = CQFunctional(f), fcfg = FormFunctional(
CQFunctional(f),g), vql = VectQuot(V, LKer fg), vq =VectQuot(V, Ker f);
assume g <> 0Functional(W);
then
A1: leftker fg = ker f by Th51;
the carrier of LKer fg = leftker fg by Def18;
hence
A2: LKer fg = Ker f by A1,VECTSP10:def 11;
A3: now
let x be object;
assume x in dom fcfg;
then consider A be Vector of vq, B be Vector of W such that
A4: x=[A,B] by DOMAIN_1:1;
consider v be Vector of V such that
A5: A = v + Ker f by VECTSP10:22;
thus fcfg.x = fcfg.(A,B) by A4
.= cf.A * g.B by Def10
.=f.v *g.B by A5,VECTSP10:35
.= fg.(v,B) by Def10
.= (LQForm(fg)).(A,B) by A2,A5,Def20
.= (LQForm(fg)).x by A4;
end;
dom LQForm(fg) = [: the carrier of vql, the carrier of W:] & dom fcfg =
[: the carrier of vq, the carrier of W:] by FUNCT_2:def 1;
hence thesis by A2,A3,FUNCT_1:2;
end;
theorem Th55:
for K be add-associative right_zeroed right_complementable
commutative Abelian associative well-unital distributive almost_left_invertible
non empty doubleLoopStr for V be non empty ModuleStr over K, W be VectSp of K
for f be Functional of V, g be linear-Functional of W st f <> 0Functional(V)
holds RKer FormFunctional(f,g) = Ker g & RQForm(FormFunctional(f,g)) =
FormFunctional(f,CQFunctional(g))
proof
let K be add-associative right_zeroed right_complementable commutative
Abelian associative well-unital distributive almost_left_invertible non empty
doubleLoopStr, V be non empty ModuleStr over K, W be VectSp of K, f be
Functional of V, g be linear-Functional of W;
set fg = FormFunctional(f,g), cg = CQFunctional(g), fcfg = FormFunctional(f,
CQFunctional(g)), wqr = VectQuot(W, RKer fg), wq =VectQuot(W, Ker g);
assume f <> 0Functional(V);
then
A1: rightker fg = ker g by Th53;
the carrier of RKer fg = rightker fg by Def19;
hence
A2: RKer fg = Ker g by A1,VECTSP10:def 11;
A3: now
let x be object;
assume x in dom fcfg;
then consider A be Vector of V, B be Vector of wq such that
A4: x=[A,B] by DOMAIN_1:1;
consider w be Vector of W such that
A5: B = w + Ker g by VECTSP10:22;
thus fcfg.x = fcfg.(A,B) by A4
.= f.A * cg.B by Def10
.=f.A *g.w by A5,VECTSP10:35
.= fg.(A,w) by Def10
.= (RQForm(fg)).(A,B) by A2,A5,Def21
.= (RQForm(fg)).x by A4;
end;
dom RQForm(fg) = [: the carrier of V, the carrier of wqr:] & dom fcfg =
[: the carrier of V, the carrier of wq:] by FUNCT_2:def 1;
hence thesis by A2,A3,FUNCT_1:2;
end;
theorem
for K be Field, V,W be non trivial VectSp of K for f be non constant
linear-Functional of V, g be non constant linear-Functional of W holds QForm(
FormFunctional(f,g)) = FormFunctional(CQFunctional(f),CQFunctional(g))
proof
let K be Field, V,W be non trivial VectSp of K, f be non constant
linear-Functional of V, g be non constant linear-Functional of W;
A1: CQFunctional(f) <> 0Functional(VectQuot(V,Ker f));
A2: g <> 0Functional(W);
then
A3: LQForm(FormFunctional(f,g)) = FormFunctional(CQFunctional(f),g) by Th54;
thus QForm(FormFunctional(f,g)) = RQForm(LQForm(FormFunctional(f,g))) by Th48
.= RQForm(FormFunctional(CQFunctional(f),g)) by A2,A3,Th54
.= FormFunctional(CQFunctional(f),CQFunctional(g)) by A1,Th55;
end;
definition
let K be ZeroStr;
let V,W be non empty ModuleStr over K;
let f be Form of V,W;
attr f is degenerated-on-left means
:Def23:
leftker f <> {0.V};
attr f is degenerated-on-right means
:Def24:
rightker f <> {0.W};
end;
registration
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be VectSp of K, W be right_zeroed non empty ModuleStr over K;
let f be additiveSAF homogeneousSAF Form of V,W;
cluster LQForm(f) -> non degenerated-on-left;
coherence
proof
set qf = LQForm(f), L = LKer f, qV = VectQuot(V,L);
thus leftker qf c= {0.qV}
proof
let x be object;
assume x in leftker qf;
then consider vv be Vector of qV such that
A1: x= vv and
A2: for w be Vector of W holds qf.(vv,w)=0.K;
consider v be Vector of V such that
A3: vv = v + L by VECTSP10:22;
now
let w be Vector of W;
thus f.(v,w) = qf.(vv,w) by A3,Def20
.= 0.K by A2;
end;
then v in leftker f;
then v in the carrier of L by Def18;
then v in L;
then v+L = the carrier of L by VECTSP_4:49
.= zeroCoset(V,L) by VECTSP10:def 4
.= 0.qV by VECTSP10:21;
hence thesis by A1,A3,TARSKI:def 1;
end;
let x be object;
assume x in {0.qV};
then
A4: x = 0.qV by TARSKI:def 1;
for w be Vector of W holds qf.(0.qV,w) = 0.K by Th30;
hence thesis by A4;
end;
end;
registration
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be right_zeroed non empty ModuleStr over K, W be VectSp of K;
let f be additiveFAF homogeneousFAF Form of V,W;
cluster RQForm(f) -> non degenerated-on-right;
coherence
proof
set qf = RQForm(f), R = RKer f, qW = VectQuot(W,R);
thus rightker qf c= {0.qW}
proof
let x be object;
assume x in rightker qf;
then consider ww be Vector of qW such that
A1: x= ww and
A2: for v be Vector of V holds qf.(v,ww)=0.K;
consider w be Vector of W such that
A3: ww = w + R by VECTSP10:22;
now
let v be Vector of V;
thus f.(v,w) = qf.(v,ww) by A3,Def21
.= 0.K by A2;
end;
then w in rightker f;
then w in the carrier of R by Def19;
then w in R;
then w+R = the carrier of R by VECTSP_4:49
.= zeroCoset(W,R) by VECTSP10:def 4
.= 0.qW by VECTSP10:21;
hence thesis by A1,A3,TARSKI:def 1;
end;
let x be object;
assume x in {0.qW};
then
A4: x = 0.qW by TARSKI:def 1;
for v be Vector of V holds qf.(v,0.qW) = 0.K by Th29;
hence thesis by A4;
end;
end;
registration
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty 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
proof
rightker RQForm(f) = {0.(VectQuot(W,RKer f))} by Def24;
then
A1: rightker LQForm(RQForm(f)) = {0.(VectQuot(W,RKer f))} by Th44;
leftker LQForm(f) = {0.(VectQuot(V,LKer f))} by Def23;
then
A2: leftker RQForm(LQForm(f)) = {0.(VectQuot(V,LKer f))} by Th45;
leftker RQForm(LQForm(f)) = leftker QForm(f) & rightker LQForm(RQForm(
f)) = rightker QForm(f) by Th49;
hence thesis by A2,A1;
end;
end;
registration
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V,W be VectSp of K;
let f be bilinear-Form of V,W;
cluster RQForm(LQForm(f)) -> non degenerated-on-left non
degenerated-on-right;
coherence
proof
leftker LQForm(f) = {0.(VectQuot(V,LKer f))} by Def23;
then leftker RQForm(LQForm(f)) = {0.(VectQuot(V,LKer f))} by Th45;
hence thesis;
end;
cluster LQForm(RQForm(f)) -> non degenerated-on-left non
degenerated-on-right;
coherence
proof
rightker RQForm(f) = {0.(VectQuot(W,RKer f))} by Def24;
then rightker LQForm(RQForm(f)) = {0.(VectQuot(W,RKer f))} by Th44;
hence thesis;
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;
coherence
proof
consider v be Vector of V, w be Vector of W such that
A1: f.(v,w) <> 0.K by Th40;
reconsider B = w + RKer f as Vector of VectQuot(W,RKer(f)) by VECTSP10:23;
reconsider A = v +LKer f as Vector of VectQuot(V,LKer(f)) by VECTSP10:23;
(QForm(f)).(A,B) = f.(v,w) by Def22;
hence thesis by A1,Th40;
end;
end;
begin
:: Bilinear Symmetric and Alternating Forms
definition
let K be 1-sorted;
let V be ModuleStr over K;
let f be Form of V,V;
attr f is symmetric means
:Def25:
for v,w be Vector of V holds f.(v,w) = f.( w,v);
end;
definition
let K be ZeroStr;
let V be ModuleStr over K;
let f be Form of V,V;
attr f is alternating means
:Def26:
for v be Vector of V holds f.(v,v) = 0.K;
end;
registration
let K be non empty ZeroStr;
let V be non empty ModuleStr over K;
cluster NulForm(V,V) -> symmetric;
coherence
proof
let v,w be Vector of V;
thus NulForm(V,V).(v,w) = 0.K by FUNCOP_1:70
.= NulForm(V,V).(w,v) by FUNCOP_1:70;
end;
cluster NulForm(V,V) -> alternating;
coherence
by FUNCOP_1:70;
end;
registration
let K be non empty ZeroStr;
let V be non empty ModuleStr over K;
cluster symmetric for Form of V,V;
existence
proof
take NulForm(V,V);
thus thesis;
end;
cluster alternating for Form of V,V;
existence
proof
take NulForm(V,V);
thus thesis;
end;
end;
registration
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V be non empty ModuleStr over K;
cluster symmetric additiveFAF homogeneousFAF additiveSAF homogeneousSAF for
Form
of V,V;
existence
proof
take NulForm(V,V);
thus thesis;
end;
cluster alternating additiveFAF homogeneousFAF additiveSAF homogeneousSAF
for Form of V,V;
existence
proof
take NulForm(V,V);
thus thesis;
end;
end;
registration
let K be Field;
let V be non trivial VectSp of K;
cluster symmetric non trivial non constant additiveFAF homogeneousFAF
additiveSAF homogeneousSAF for Form of V,V;
existence
proof
set f = the non constant non trivial linear-Functional of V;
take ff = FormFunctional(f,f);
now
let v,w be Vector of V;
thus ff.(v,w)= f.v * f.w by Def10
.= ff.(w,v) by Def10;
end;
hence thesis;
end;
end;
registration
let K be add-associative right_zeroed right_complementable non empty
addLoopStr;
let V be non empty ModuleStr over K;
cluster alternating additiveFAF additiveSAF for Form of V,V;
existence
proof
take NulForm(V,V);
thus thesis;
end;
end;
registration
let K be non empty addLoopStr;
let V be non empty ModuleStr over K;
let f,g be symmetric Form of V,V;
cluster f+g -> symmetric;
coherence
proof
let v,w be Vector of V;
thus (f+g).(v,w) = f.(v,w) + g.(v,w) by Def2
.= f.(w,v) + g.(v,w) by Def25
.= f.(w,v) + g.(w,v) by Def25
.= (f+g).(w,v) by Def2;
end;
end;
registration
let K be non empty doubleLoopStr;
let V be non empty ModuleStr over K;
let f be symmetric Form of V,V;
let a be Element of K;
cluster a*f -> symmetric;
coherence
proof
let v,w be Vector of V;
thus (a*f).(v,w) = a*f.(v,w) by Def3
.= a*f.(w,v) by Def25
.= (a*f).(w,v) by Def3;
end;
end;
registration
let K be non empty addLoopStr;
let V be non empty ModuleStr over K;
let f be symmetric Form of V,V;
cluster -f -> symmetric;
coherence
proof
let v,w be Vector of V;
thus (-f).(v,w) = -f.(v,w) by Def4
.= -f.(w,v) by Def25
.= (-f).(w,v) by Def4;
end;
end;
registration
let K be non empty addLoopStr;
let V be non empty ModuleStr over K;
let f,g be symmetric Form of V,V;
cluster f-g -> symmetric;
coherence;
end;
registration
let K be right_zeroed non empty addLoopStr;
let V be non empty ModuleStr over K;
let f,g be alternating Form of V,V;
cluster f+g -> alternating;
coherence
proof
let v be Vector of V;
thus (f+g).(v,v) = f.(v,v) + g.(v,v) by Def2
.= 0.K + g.(v,v) by Def26
.= 0.K + 0.K by Def26
.= 0.K by RLVECT_1:def 4;
end;
end;
registration
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let V be non empty ModuleStr over K;
let f be alternating Form of V,V;
let a be Scalar of K;
cluster a*f -> alternating;
coherence
proof
let v be Vector of V;
thus (a*f).(v,v) = a*f.(v,v) by Def3
.= a*0.K by Def26
.= 0.K;
end;
end;
registration
let K be add-associative right_zeroed right_complementable non empty
addLoopStr;
let V be non empty ModuleStr over K;
let f be alternating Form of V,V;
cluster -f -> alternating;
coherence
proof
let v be Vector of V;
thus (-f).(v,v) = -f.(v,v) by Def4
.= -0.K by Def26
.= 0.K by RLVECT_1:12;
end;
end;
registration
let K be add-associative right_zeroed right_complementable non empty
addLoopStr;
let V be non empty ModuleStr over K;
let f,g be alternating Form of V,V;
cluster f-g -> alternating;
coherence;
end;
theorem
for K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr for V be non empty ModuleStr over
K for f be symmetric bilinear-Form of V,V holds leftker f = rightker f
proof
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr, V be non empty ModuleStr over K,
f be symmetric bilinear-Form of V,V;
thus leftker f c= rightker f
proof
let x be object;
assume x in leftker f;
then consider v be Vector of V such that
A1: v = x and
A2: for w be Vector of V holds f.(v,w)=0.K;
now
let w be Vector of V;
thus f.(w,v) = f.(v,w) by Def25
.= 0.K by A2;
end;
hence thesis by A1;
end;
let x be object;
assume x in rightker f;
then consider w be Vector of V such that
A3: w = x and
A4: for v be Vector of V holds f.(v,w)=0.K;
now
let v be Vector of V;
thus f.(w,v) = f.(v,w) by Def25
.= 0.K by A4;
end;
hence thesis by A3;
end;
theorem Th58:
for K be add-associative right_zeroed right_complementable non
empty addLoopStr for V be non empty ModuleStr over K for f be alternating
additiveSAF additiveFAF Form of V,V for v,w be Vector of V holds f.(v,w)=-f.(w,
v)
proof
let K be add-associative right_zeroed right_complementable non empty
addLoopStr, V be non empty ModuleStr over K, f be alternating additiveSAF
additiveFAF Form of V,V, v,w be Vector of V;
0.K = f.(v+w,v+w) by Def26
.= f.(v,v) + f.(v,w) + (f.(w,v) + f.(w,w)) by Th28
.= 0.K + f.(v,w) + (f.(w,v) + f.(w,w)) by Def26
.= 0.K + f.(v,w) + (f.(w,v) + 0.K) by Def26
.= 0.K + f.(v,w) + f.(w,v) by RLVECT_1:def 4
.= f.(v,w) + f.(w,v) by RLVECT_1:4;
hence thesis by RLVECT_1:6;
end;
definition
let K be Fanoian Field;
let V be non empty ModuleStr over K;
let f be additiveSAF additiveFAF Form of V,V;
redefine attr f is alternating means :: redefines alternating (BILINEAR, definition)
for v,w be Vector of V holds f.(v,w) = -f.(w,v);
compatibility
proof
thus f is alternating implies for v,w be Vector of V holds f.(v,w) = -f.(w
,v) by Th58;
assume
A1: for v,w be Vector of V holds f.(v,w) = -f.(w,v);
let v be Vector of V;
f.(v,v) = - f.(v,v) by A1;
then f.(v,v)+f.(v,v)= 0.K by VECTSP_1:16;
hence thesis by VECTSP_1:def 18;
end;
end;
theorem
for K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr for V be non empty ModuleStr over
K for f be alternating bilinear-Form of V,V holds leftker f = rightker f
proof
let K be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr, V be non empty ModuleStr over K,
f be alternating bilinear-Form of V,V;
thus leftker f c= rightker f
proof
let x be object;
assume x in leftker f;
then consider v be Vector of V such that
A1: v = x and
A2: for w be Vector of V holds f.(v,w)=0.K;
now
let w be Vector of V;
thus f.(w,v) = -f.(v,w) by Th58
.= -0.K by A2
.= 0.K by RLVECT_1:12;
end;
hence thesis by A1;
end;
let x be object;
assume x in rightker f;
then consider w be Vector of V such that
A3: w = x and
A4: for v be Vector of V holds f.(v,w)=0.K;
now
let v be Vector of V;
thus f.(w,v) = -f.(v,w) by Th58
.= -0.K by A4
.= 0.K by RLVECT_1:12;
end;
hence thesis by A3;
end;