:: Quotient Vector Spaces and Functionals :: 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 ALGSTR_0, STRUCT_0, VECTSP_1, SUPINF_2, XBOOLE_0, RLVECT_1, SUBSET_1, ARYTM_3, BINOP_1, LATTICES, FUNCT_1, RELAT_1, MESFUNC1, ZFMISC_1, RLSUB_1, RLVECT_3, RLVECT_2, CARD_3, FUNCT_2, TARSKI, ARYTM_1, RLSUB_2, FINSEQ_4, MCART_1, GROUP_1, SETFAM_1, HAHNBAN, MSSUBFAM, UNIALG_1, HAHNBAN1, GROUP_6, VECTSP10; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, DOMAIN_1, RELSET_1, FUNCT_2, STRUCT_0, ALGSTR_0, RLVECT_1, BINOP_1, GROUP_1, VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, GRCAT_1, HAHNBAN1; constructors REALSET2, VECTSP_5, VECTSP_6, VECTSP_7, HAHNBAN1, RELSET_1, GRCAT_1; registrations SUBSET_1, FUNCT_1, FINSET_1, STRUCT_0, VECTSP_1, VECTSP_4, HAHNBAN1, ALGSTR_0, FUNCT_2, RELAT_1, ZFMISC_1, RELSET_1, XTUPLE_0; requirements SUBSET, BOOLE; begin ::Auxiliary Facts about Double Loops and Vector Spaces definition let K be doubleLoopStr; func StructVectSp(K) -> strict ModuleStr over K equals :: VECTSP10:def 1 ModuleStr (# the carrier of K, the addF of K, 0.K, the multF of K#); end; registration let K be non empty doubleLoopStr; cluster StructVectSp(K) -> non empty; end; registration let K be Abelian non empty doubleLoopStr; cluster StructVectSp(K) -> Abelian; end; registration let K be add-associative non empty doubleLoopStr; cluster StructVectSp(K) -> add-associative; end; registration let K be right_zeroed non empty doubleLoopStr; cluster StructVectSp(K) -> right_zeroed; end; registration let K be right_complementable non empty doubleLoopStr; cluster StructVectSp(K) -> right_complementable; end; registration let K be associative left_unital distributive non empty doubleLoopStr; cluster StructVectSp(K) -> vector-distributive scalar-distributive scalar-associative scalar-unital; end; registration let K be non degenerated non empty doubleLoopStr; cluster StructVectSp(K) -> non trivial; end; registration let K be non degenerated non empty doubleLoopStr; cluster non trivial for ModuleStr over K; end; registration let K be add-associative right_zeroed right_complementable non empty doubleLoopStr; cluster add-associative right_zeroed right_complementable strict for non empty ModuleStr over K; end; registration let K be add-associative right_zeroed right_complementable associative left_unital distributive non empty doubleLoopStr; cluster add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital strict for non empty ModuleStr over K; end; registration let K be Abelian add-associative right_zeroed right_complementable associative left_unital distributive non degenerated non empty doubleLoopStr; cluster Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital strict for non trivial ModuleStr over K; end; theorem :: VECTSP10:1 for K be add-associative right_zeroed right_complementable associative left_unital distributive non empty doubleLoopStr, a be Element of K for V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over K, v be Vector of V holds (0.K)*v = 0.V & a*(0.V) = 0.V; theorem :: VECTSP10:2 for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr for V be VectSp of K for S, T be Subspace of V, v be Vector of V st S /\ T = (0).V & v in S & v in T holds v = 0.V; theorem :: VECTSP10:3 for K be Field, V be VectSp of K for x be object, v be Vector of V holds x in Lin{v} iff ex a be Element of K st x =a*v; theorem :: VECTSP10:4 for K be Field, V be VectSp of K, v be Vector of V, a,b be Scalar of V st v <> 0.V & a * v = b * v holds a = b; theorem :: VECTSP10:5 for K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr for V be VectSp of K for W1,W2 be Subspace of V st V is_the_direct_sum_of W1,W2 for v,v1 ,v2 be Vector of V st v1 in W1 & v2 in W2 & v = v1 + v2 holds v |-- (W1,W2) = [ v1,v2]; theorem :: VECTSP10:6 for K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr for V be VectSp of K for W1,W2 be Subspace of V st V is_the_direct_sum_of W1,W2 for v,v1 ,v2 be Vector of V st v |-- (W1,W2) = [v1,v2] holds v = v1 + v2; theorem :: VECTSP10:7 for K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr for V be VectSp of K for W1,W2 be Subspace of V st V is_the_direct_sum_of W1,W2 for v,v1 ,v2 be Vector of V st v |-- (W1,W2) = [v1,v2] holds v1 in W1 & v2 in W2; theorem :: VECTSP10:8 for K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr for V be VectSp of K for W1,W2 be Subspace of V st V is_the_direct_sum_of W1,W2 for v,v1 ,v2 be Vector of V st v |-- (W1,W2) = [v1,v2] holds v |-- (W2,W1) = [v2,v1]; theorem :: VECTSP10:9 for K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr for V be VectSp of K for W1,W2 be Subspace of V st V is_the_direct_sum_of W1,W2 for v be Vector of V st v in W1 holds v |-- (W1,W2) = [v,0.V]; theorem :: VECTSP10:10 for K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr for V be VectSp of K for W1,W2 be Subspace of V st V is_the_direct_sum_of W1,W2 for v be Vector of V st v in W2 holds v |-- (W1,W2) = [0.V,v]; theorem :: VECTSP10:11 for K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr for V be VectSp of K for V1 be Subspace of V, W1 be Subspace of V1, v be Vector of V st v in W1 holds v is Vector of V1; theorem :: VECTSP10:12 for K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr for V be VectSp of K for V1,V2,W be Subspace of V, W1,W2 be Subspace of W st W1 = V1 & W2 = V2 holds W1 + W2 = V1 + V2; theorem :: VECTSP10:13 for K be Field, V be VectSp of K, W be Subspace of V for v be Vector of V, w be Vector of W st v = w holds Lin{w} = Lin{v}; theorem :: VECTSP10:14 for K be Field, V be VectSp of K for v be Vector of V, X be Subspace of V st not v in X for y be Vector of X + Lin{v}, W be Subspace of X + Lin{v} st v = y & W = X holds X + Lin{v} is_the_direct_sum_of W,Lin{y}; theorem :: VECTSP10:15 for K be Field, V be VectSp of K, v be Vector of V, X be Subspace of V, y be Vector of X + Lin{v}, W be Subspace of X + Lin{v} st v = y & X = W & not v in X holds y |-- (W,Lin{y}) = [0.W,y]; theorem :: VECTSP10:16 for K be Field, V be VectSp of K, v be Vector of V, X be Subspace of V for y be Vector of X + Lin{v}, W be Subspace of X + Lin{v} st v = y & X = W & not v in X for w be Vector of X + Lin{v} st w in X holds w |-- (W, Lin{y}) = [w,0.V]; theorem :: VECTSP10:17 for K be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K for v be Vector of V, W1,W2 be Subspace of V ex v1,v2 be Vector of V st v |-- (W1,W2) = [v1,v2]; theorem :: VECTSP10:18 for K be Field, V be VectSp of K for v be Vector of V, X be Subspace of V, y be Vector of X + Lin{v}, W be Subspace of X + Lin{v} st v = y & X = W & not v in X for w be Vector of X + Lin{v} ex x be Vector of X, r be Element of K st w |-- (W,Lin{y}) = [x,r*v]; theorem :: VECTSP10:19 for K be Field, V be VectSp of K for v be Vector of V, X be Subspace of V, y be Vector of X + Lin{v}, W be Subspace of X + Lin{v} st v = y & X = W & not v in X for w1,w2 be Vector of X + Lin{v}, x1,x2 be Vector of X, r1,r2 be Element of K st w1 |-- (W,Lin{y}) = [x1,r1*v] & w2 |-- (W,Lin{y}) = [ x2,r2*v] holds w1 + w2 |-- (W,Lin{y}) = [x1 + x2, (r1+r2)*v]; theorem :: VECTSP10:20 for K be Field, V be VectSp of K for v be Vector of V, X be Subspace of V, y be Vector of X + Lin{v}, W be Subspace of X + Lin{v} st v = y & X = W & not v in X for w be Vector of X + Lin{v}, x be Vector of X, t,r be Element of K st w |-- (W,Lin{y}) = [x,r*v] holds t*w |-- (W,Lin{y}) = [t*x, t*r *v]; begin :: Quotient Vector Space for non commutative Double Loop definition let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr; let V be VectSp of K; let W be Subspace of V; func CosetSet(V,W) ->non empty Subset-Family of V equals :: VECTSP10:def 2 the set of all A where A is Coset of W; 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; let W be Subspace of V; func addCoset(V,W) -> BinOp of CosetSet(V,W) means :: VECTSP10:def 3 for A,B be Element of CosetSet(V,W) for a,b be Vector of V st A = a + W & B = b + W holds it.(A,B) = (a+b)+W; 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; let W be Subspace of V; func zeroCoset(V,W) -> Element of CosetSet(V,W) equals :: VECTSP10:def 4 the carrier of W; 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; let W be Subspace of V; func lmultCoset(V,W) -> Function of [:the carrier of K, CosetSet(V,W):], CosetSet(V,W) means :: VECTSP10:def 5 for z be Element of K, A be Element of CosetSet(V,W) for a be Vector of V st A = a+W holds it.(z,A) = z*a +W; 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; let W be Subspace of V; func VectQuot(V,W) -> strict Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over K means :: VECTSP10:def 6 the carrier of it = CosetSet(V,W) & the addF of it = addCoset(V,W) & 0.it = zeroCoset(V,W) & the lmult of it = lmultCoset(V,W); end; theorem :: VECTSP10:21 for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be VectSp of K, W be Subspace of V holds zeroCoset(V,W) = 0.V + W & 0.(VectQuot(V, W)) = zeroCoset(V,W); theorem :: VECTSP10:22 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 Subspace of V, w be Vector of VectQuot(V,W) holds w is Coset of W & ex v be Vector of V st w = v + W; theorem :: VECTSP10:23 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 Subspace of V, v be Vector of V holds v+W is Coset of W & v+W is Vector of VectQuot(V,W); theorem :: VECTSP10:24 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 Subspace of V, A be Coset of W holds A is Vector of VectQuot(V,W); theorem :: VECTSP10:25 for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be VectSp of K, W be Subspace of V for A be Vector of VectQuot(V,W), v be Vector of V, a be Scalar of V st A = v + W holds a*A = a*v + W; theorem :: VECTSP10:26 for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V be VectSp of K, W be Subspace of V for A1,A2 be Vector of VectQuot(V,W), v1,v2 be Vector of V st A1 = v1 + W & A2 = v2 + W holds A1 + A2 = v1 + v2 + W; begin :: Auxiliary Facts about Functionals theorem :: VECTSP10:27 for K be Field, V be VectSp of K for X be Subspace of V, fi be linear-Functional of X, v be Vector of V, y be Vector of X + Lin {v} st v = y & not v in X for r be Element of K ex psi be linear-Functional of X + Lin{v} st psi|the carrier of X=fi & psi.y = r; registration let K be right_zeroed non empty addLoopStr; let V be non empty ModuleStr over K; cluster additive 0-preserving for Functional of V; end; registration let K be add-associative right_zeroed right_complementable non empty doubleLoopStr; let V be right_zeroed non empty ModuleStr over K; cluster additive -> 0-preserving for Functional of V; 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; cluster homogeneous -> 0-preserving for Functional of V; end; registration let K be non empty ZeroStr; let V be non empty ModuleStr over K; cluster 0Functional(V) -> constant; end; registration let K be non empty ZeroStr; let V be non empty ModuleStr over K; cluster constant for Functional of V; end; definition 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 0-preserving Functional of V; redefine attr f is constant means :: VECTSP10:def 7 f = 0Functional(V); end; registration let K be add-associative right_zeroed right_complementable non empty doubleLoopStr; let V be right_zeroed non empty ModuleStr over K; cluster constant additive 0-preserving for Functional of V; end; registration let K be Field; let V be non trivial VectSp of K; cluster additive homogeneous non constant non trivial for Functional of V; end; registration :: uogolnic !!! let K be Field; let V be non trivial VectSp of K; cluster trivial -> constant for Functional of V; end; definition let K be Field; let V be non trivial VectSp of K; let v be Vector of V; let W be Linear_Compl of Lin{v}; assume v <> 0.V; func coeffFunctional(v,W) -> non constant non trivial linear-Functional of V means :: VECTSP10:def 8 it.v = 1_K & it|the carrier of W = 0Functional(W); end; theorem :: VECTSP10:28 for K be Field, V be non trivial VectSp of K for f be non constant 0-preserving Functional of V ex v be Vector of V st v <> 0.V & f.v <> 0.K; theorem :: VECTSP10:29 for K be Field, V be non trivial VectSp of K for v be Vector of V, a be Scalar of V for W be Linear_Compl of Lin{v} st v <> 0.V holds ( coeffFunctional(v,W)).(a*v) = a; theorem :: VECTSP10:30 for K be Field, V be non trivial VectSp of K for v,w be Vector of V for W be Linear_Compl of Lin{v} st v <> 0.V & w in W holds ( coeffFunctional(v,W)).w = 0.K; theorem :: VECTSP10:31 for K be Field, V be non trivial VectSp of K for v,w be Vector of V, a be Scalar of V for W be Linear_Compl of Lin{v} st v <> 0.V & w in W holds ( coeffFunctional(v,W)).(a*v+w) = a; theorem :: VECTSP10:32 for K be non empty addLoopStr for V be non empty ModuleStr over K for f,g be Functional of V, v be Vector of V holds (f-g).v = f.v - g.v; registration let K be Field; let V be non trivial VectSp of K; cluster V*' -> non trivial; end; begin :: Kernel of Additive Functional and Subspace Generated by Kernel of :: Linear Functional. Linear Functionals in Quotient Vector Space :: generated by Additive Functional definition let S be non empty 1-sorted; let Z be ZeroStr; let f be Function of S,Z; func ker f -> Subset of S equals :: VECTSP10:def 9 {v where v is Element of S : f.v = 0.Z}; end; registration let K be right_zeroed non empty addLoopStr; let V be non empty ModuleStr over K; let f be 0-preserving Functional of V; cluster ker f -> non empty; end; theorem :: VECTSP10:33 for K be add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr for V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over K for f be linear-Functional of V holds ker f is linearly-closed; definition let K be non empty ZeroStr; let V be non empty ModuleStr over K; let f be Functional of V; attr f is degenerated means :: VECTSP10:def 10 ker f <> {0.V}; end; registration let K be non degenerated non empty doubleLoopStr; let V be non trivial ModuleStr over K; cluster non degenerated 0-preserving -> non constant for Functional of V; 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; let f be linear-Functional of V; func Ker f -> strict non empty Subspace of V means :: VECTSP10:def 11 the carrier of it = ker 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; let W be Subspace of V; let f be additive Functional of V; assume the carrier of W c= ker f; func QFunctional(f,W) -> additive Functional of VectQuot(V,W) means :: VECTSP10:def 12 for A be Vector of VectQuot(V,W), a be Vector of V st A = a+W holds it.A = f.a; end; theorem :: VECTSP10:34 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 Subspace of V for f be linear-Functional of V st the carrier of W c= ker f holds QFunctional(f,W) is homogeneous; definition let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr; let V be VectSp of K; let f be linear-Functional of V; func CQFunctional(f) -> linear-Functional of VectQuot(V,Ker f) equals :: VECTSP10:def 13 QFunctional(f,Ker f); end; theorem :: VECTSP10:35 for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr for V be VectSp of K, f be linear-Functional of V for A be Vector of VectQuot(V,Ker f), v be Vector of V st A = v+Ker f holds (CQFunctional(f)).A = f.v; registration let K be Field; let V be non trivial VectSp of K; let f be non constant linear-Functional of V; cluster CQFunctional(f) -> non constant; 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; let f be linear-Functional of V; cluster CQFunctional(f) -> non degenerated; end;