:: Basis of Vector Space :: by Wojciech A. Trybulec :: :: Received July 27, 1990 :: Copyright (c) 1990-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 VECTSP_1, SUBSET_1, FINSET_1, RLVECT_2, FUNCT_1, STRUCT_0, RLVECT_3, CARD_3, SUPINF_2, XBOOLE_0, TARSKI, GROUP_1, FUNCT_2, RELAT_1, ARYTM_1, ARYTM_3, MESFUNC1, RLSUB_1, ZFMISC_1, ORDINAL1, ORDERS_1, RLVECT_1, ALGSTR_0, BINOP_1, LATTICES, FUNCSDOM, FINSEQ_1, VECTSP_2, MOD_3, PRELAMB, VALUED_1, PARTFUN1, ORDINAL4, NAT_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FUNCT_2, FINSET_1, ORDERS_1, DOMAIN_1, STRUCT_0, ORDINAL1, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6; constructors ORDERS_1, REALSET1, VECTSP_5, VECTSP_6, STRUCT_0, GROUP_1, RLVECT_2, VECTSP_2, PARTFUN1, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, VECTSP_1, VECTSP_4, ORDINAL1; requirements SUBSET, BOOLE; begin definition let GF be non empty doubleLoopStr, V be non empty ModuleStr over GF; let IT be Subset of V; attr IT is linearly-independent means :: VECTSP_7:def 1 for l being Linear_Combination of IT st Sum(l) = 0.V holds Carrier(l) = {}; end; notation let GF be non empty doubleLoopStr, V be non empty ModuleStr over GF; let IT be Subset of V; antonym IT is linearly-dependent for IT is linearly-independent; end; reserve x,y for object, X,Y,Z for set; reserve GF for commutative Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr; reserve a,b for Element of GF; reserve V for scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable Abelian non empty ModuleStr over GF; reserve v,v1,v2,u for Vector of V; reserve A,B,C for Subset of V; reserve T for finite Subset of V; reserve l for Linear_Combination of A; reserve f,g for Function of V, GF; theorem :: VECTSP_7:1 A c= B & B is linearly-independent implies A is linearly-independent; reserve GF for commutative non degenerated almost_left_invertible Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr; reserve a,b for Element of GF; reserve V for scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable Abelian non empty ModuleStr over GF; reserve v,v1,v2,u for Vector of V; reserve A,B,C for Subset of V; reserve T for finite Subset of V; reserve l for Linear_Combination of A; reserve f,g for Function of V, GF; theorem :: VECTSP_7:2 for R being non degenerated Ring, V being LeftMod of R, A being Subset of V st A is linearly-independent holds not 0.V in A; registration let GF,V; cluster empty -> linearly-independent for Subset of V; end; registration let GF, V; cluster finite linearly-independent for Subset of V; end; theorem :: VECTSP_7:3 for R being commutative non degenerated almost_left_invertible Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr, V being LeftMod of R, v being Vector of V holds {v} is linearly-independent iff v <> 0.V; theorem :: VECTSP_7:4 for GF being commutative non degenerated Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr, V being scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable Abelian non empty ModuleStr over GF, v1, v2 being Vector of V st {v1,v2} is linearly-independent holds v1 <> 0.V; theorem :: VECTSP_7:5 v1 <> v2 & {v1,v2} is linearly-independent iff v2 <> 0.V & for a holds v1 <> a * v2; theorem :: VECTSP_7:6 v1 <> v2 & {v1,v2} is linearly-independent iff for a,b st a * v1 + b * v2 = 0.V holds a = 0.GF & b = 0.GF; definition let GF be Ring; let V be LeftMod of GF, A be Subset of V; func Lin(A) -> strict Subspace of V means :: VECTSP_7:def 2 the carrier of it = the set of all Sum(l) where l is Linear_Combination of A; end; theorem :: VECTSP_7:7 for GF be Ring, V be LeftMod of GF, A be Subset of V holds x in Lin(A) iff ex l being Linear_Combination of A st x = Sum(l); theorem :: VECTSP_7:8 for GF be Ring, V be LeftMod of GF, A be Subset of V holds x in A implies x in Lin(A); reserve l0 for Linear_Combination of {}(the carrier of V); theorem :: VECTSP_7:9 for GF be Ring, V be LeftMod of GF holds Lin({}(the carrier of V)) = (0).V; theorem :: VECTSP_7:10 for GF be Ring, V be LeftMod of GF, A be Subset of V holds Lin(A) = (0).V implies A = {} or A = {0.V}; theorem :: VECTSP_7:11 for GF be non degenerated Ring, V be LeftMod of GF, A be Subset of V holds for W being strict Subspace of V st A = the carrier of W holds Lin(A) = W; theorem :: VECTSP_7:12 for V being strict VectSp of GF, A being Subset of V st A = the carrier of V holds Lin(A) = V; theorem :: VECTSP_7:13 for GF be Ring, V be LeftMod of GF, A,B be Subset of V holds A c= B implies Lin(A) is Subspace of Lin(B); theorem :: VECTSP_7:14 Lin(A) = V & A c= B implies Lin(B) = V; theorem :: VECTSP_7:15 for GF be Ring, V be LeftMod of GF, A,B be Subset of V holds Lin(A \/ B) = Lin(A) + Lin(B); theorem :: VECTSP_7:16 for GF be Ring, V be LeftMod of GF, A,B be Subset of V holds Lin(A /\ B) is Subspace of Lin(A) /\ Lin(B); definition let GF be Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr; let V be LeftMod of GF; let A be Subset of V; attr A is base means :: VECTSP_7:def 3 A is linearly-independent & Lin A = the ModuleStr of V; end; theorem :: VECTSP_7:17 for R being non degenerated almost_left_invertible Ring for V being LeftMod of R for A being Subset of V st A is linearly-independent holds ex B being Subset of V st A c= B & B is base; theorem :: VECTSP_7:18 Lin(A) = V implies ex B st B c= A & B is linearly-independent & Lin B = V; registration let GF be Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr, V be LeftMod of GF; cluster {}(the carrier of V) -> linearly-independent; end; registration let GF be non degenerated almost_left_invertible Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr; let V be LeftMod of GF; cluster base for Subset of V; end; definition let GF be Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr; let IT be LeftMod of GF; attr IT is free means :: VECTSP_7:def 4 ex B being Subset of IT st B is base; end; registration let GF be almost_left_invertible Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr, V be LeftMod of GF; cluster (0).V -> free; end; registration let GF be non degenerated almost_left_invertible Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr; cluster strict free for LeftMod of GF; end; definition let GF be non degenerated almost_left_invertible Abelian add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr; let V be LeftMod of GF; mode Basis of V is base Subset of V; end; theorem :: VECTSP_7:19 for V being LeftMod of GF, A being Subset of V st A is linearly-independent holds ex I being Basis of V st A c= I; theorem :: VECTSP_7:20 for V being LeftMod of GF, A being Subset of V st Lin(A) = V holds ex I being Basis of V st I c= A; :: Additional, copied from MOD_3 theorem :: VECTSP_7:21 for R being Ring, V being LeftMod of R, L being Linear_Combination of V, C being finite Subset of V st Carrier(L) c= C holds ex F being FinSequence of V st F is one-to-one & rng F = C & Sum (L) = Sum(L (#) F); theorem :: VECTSP_7:22 for R being Ring, V being LeftMod of R, L being Linear_Combination of V, a being Scalar of V holds Sum(a * L) = a * Sum(L); :: original content of LMOD_5 reserve x for set, R for Ring, V for LeftMod of R, v,v1,v2 for Vector of V, A, B for Subset of V; theorem :: VECTSP_7:23 for R being non degenerated Ring, V being LeftMod of R, v1, v2 being Vector of V holds {v1,v2} is linearly-independent implies v1 <> 0.V & v2 <> 0.V; theorem :: VECTSP_7:24 for R being domRing, V being LeftMod of R, L being Linear_Combination of V, a being Scalar of R holds a <> 0.R implies Carrier(a * L) = Carrier(L); reserve R for domRing, V for LeftMod of R, A,B for Subset of V, l for Linear_Combination of A, f,g for Function of the carrier of V, the carrier of R; theorem :: VECTSP_7:25 for W being strict Subspace of V st R is non degenerated & A = the carrier of W holds Lin(A) = W; theorem :: VECTSP_7:26 for V being strict LeftMod of R, A being Subset of V st R is non degenerated & A = the carrier of V holds Lin(A) = V; theorem :: VECTSP_7:27 for V being strict LeftMod of R, A,B being Subset of V st Lin(A) = V & A c= B holds Lin(B) = V; theorem :: VECTSP_7:28 for R being Ring, V being LeftMod of R, v1,v2 being Vector of V holds R is non degenerated & {v1,v2} is linearly-independent implies v1 <> 0.V & v2 <> 0.V;