:: Bilinear Functionals in Vector Spaces :: by Jaros{\l}aw Kotowicz :: :: Received November 5, 2002 :: Copyright (c) 2002-2021 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; 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 :: BILINEAR:def 1 [:the carrier of V,the carrier of W :] --> 0.K; 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 :: BILINEAR:def 2 for v be Vector of V, w be Vector of W holds it.(v,w) = f.(v,w)+g.(v,w); 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 :: BILINEAR:def 3 for v be Vector of V, w be Vector of W holds it.(v,w) = a*f.(v,w); 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 :: BILINEAR:def 4 for v be Vector of V, w be Vector of W holds it.(v,w) = -f.(v,w); 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 :: BILINEAR:def 5 (- 1.K) *f; 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 :: BILINEAR:def 6 f + -g; 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 :: BILINEAR:def 7 for v be Vector of V, w be Vector of W holds it.(v,w) = f.(v,w) - g.(v,w); 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; commutativity; end; theorem :: BILINEAR:1 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; theorem :: BILINEAR:2 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); theorem :: BILINEAR:3 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); theorem :: BILINEAR:4 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; theorem :: BILINEAR:5 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; theorem :: BILINEAR:6 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); theorem :: BILINEAR:7 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; 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 :: BILINEAR:def 8 (curry f).v; 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 :: BILINEAR:def 9 (curry' f).w; end; theorem :: BILINEAR:8 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); theorem :: BILINEAR:9 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); theorem :: BILINEAR:10 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); theorem :: BILINEAR:11 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); theorem :: BILINEAR:12 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); theorem :: BILINEAR:13 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); theorem :: BILINEAR:14 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); theorem :: BILINEAR:15 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); theorem :: BILINEAR:16 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); theorem :: BILINEAR:17 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); theorem :: BILINEAR:18 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); theorem :: BILINEAR:19 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); 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 :: BILINEAR:def 10 for v be Vector of V, w be Vector of W holds it.(v,w)= f.v * g.w; end; theorem :: BILINEAR:20 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; theorem :: BILINEAR:21 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; theorem :: BILINEAR:22 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); theorem :: BILINEAR:23 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 ); theorem :: BILINEAR:24 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; theorem :: BILINEAR:25 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; 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 :: BILINEAR:def 11 for v be Vector of V holds FunctionalFAF (f,v) is additive; attr f is additiveSAF means :: BILINEAR:def 12 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 :: BILINEAR:def 13 for v be Vector of V holds FunctionalFAF(f,v) is homogeneous; attr f is homogeneousSAF means :: BILINEAR:def 14 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; cluster NulForm(V,W) -> additiveSAF; 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; 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; cluster NulForm(V,W) -> homogeneousSAF; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; end; theorem :: BILINEAR:26 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); theorem :: BILINEAR:27 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); theorem :: BILINEAR:28 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)); theorem :: BILINEAR:29 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; theorem :: BILINEAR:30 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; theorem :: BILINEAR:31 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); theorem :: BILINEAR:32 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); theorem :: BILINEAR:33 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; theorem :: BILINEAR:34 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; theorem :: BILINEAR:35 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); theorem :: BILINEAR:36 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); theorem :: BILINEAR:37 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)); theorem :: BILINEAR:38 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))); theorem :: BILINEAR:39 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))); theorem :: BILINEAR:40 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; 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 :: BILINEAR:def 15 {v where v is Vector of V : for w be Vector of W holds f.(v,w) = 0.K}; 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 :: BILINEAR:def 16 {w where w is Vector of W : for v be Vector of V holds f.(v,w) = 0.K}; 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 :: BILINEAR:def 17 {v where v is Vector of V : f.(v,v) = 0.K}; 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; 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; 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; 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; 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; 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; 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; 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; end; theorem :: BILINEAR:41 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; theorem :: BILINEAR:42 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; theorem :: BILINEAR:43 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; 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 :: BILINEAR:def 18 the carrier of it = leftker f; 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 :: BILINEAR:def 19 the carrier of it = rightker f; 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 :: BILINEAR:def 20 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); 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 :: BILINEAR:def 21 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); 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; cluster RQForm(f) -> additiveSAF homogeneousSAF; 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 :: BILINEAR:def 22 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); end; theorem :: BILINEAR:44 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); theorem :: BILINEAR:45 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); theorem :: BILINEAR:46 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); theorem :: BILINEAR:47 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); theorem :: BILINEAR:48 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)); theorem :: BILINEAR:49 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))); theorem :: BILINEAR:50 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); theorem :: BILINEAR:51 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; theorem :: BILINEAR:52 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); theorem :: BILINEAR:53 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; theorem :: BILINEAR:54 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); theorem :: BILINEAR:55 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)); theorem :: BILINEAR:56 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)); 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 :: BILINEAR:def 23 leftker f <> {0.V}; attr f is degenerated-on-right means :: BILINEAR:def 24 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; 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; 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; 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; cluster LQForm(RQForm(f)) -> non degenerated-on-left non degenerated-on-right; 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; 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 :: BILINEAR:def 25 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 :: BILINEAR:def 26 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; cluster NulForm(V,V) -> alternating; end; registration let K be non empty ZeroStr; let V be non empty ModuleStr over K; cluster symmetric for Form of V,V; cluster alternating for Form of V,V; 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; cluster alternating additiveFAF homogeneousFAF additiveSAF homogeneousSAF for Form of V,V; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; end; theorem :: BILINEAR:57 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; theorem :: BILINEAR:58 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); 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 :: BILINEAR:def 27 for v,w be Vector of V holds f.(v,w) = -f.(w,v); end; theorem :: BILINEAR:59 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;