Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Linear Independence in Left Module over Domain

**by****Michal Muzalewski, and****Wojciech Skaba**- Received October 22, 1990
- MML identifier: LMOD_5

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCSDOM, VECTSP_2, VECTSP_1, RLVECT_3, RLVECT_2, RLVECT_1, BOOLE, FUNCT_1, FUNCT_2, FINSET_1, RLSUB_1, FINSEQ_1, RELAT_1, SEQ_1, FINSEQ_4; notation TARSKI, XBOOLE_0, NAT_1, SUBSET_1, FINSET_1, RELAT_1, FUNCT_1, FUNCT_2, FRAENKEL, FINSEQ_1, FINSEQ_4, STRUCT_0, RLVECT_1, VECTSP_1, FUNCSDOM, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6; constructors RLVECT_2, VECTSP_2, VECTSP_5, VECTSP_6, MEMBERED, XBOOLE_0, FINSEQ_4, PARTFUN1; clusters VECTSP_1, VECTSP_4, STRUCT_0, RLVECT_2, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0, FUNCT_1, ARYTM_3, FINSET_1; requirements SUBSET, BOOLE; begin 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; definition let R be non empty doubleLoopStr; let V be non empty VectSpStr over R; let IT be Subset of V; attr IT is linearly-independent means :: LMOD_5:def 1 for l be Linear_Combination of IT st Sum(l) = 0.V holds Carrier(l) = {}; antonym IT is linearly-dependent; end; canceled; theorem :: LMOD_5:2 A c= B & B is linearly-independent implies A is linearly-independent; theorem :: LMOD_5:3 0.R <> 1_ R & A is linearly-independent implies not 0.V in A; theorem :: LMOD_5:4 {}(the carrier of V) is linearly-independent; theorem :: LMOD_5:5 0.R <> 1_ R & {v1,v2} is linearly-independent implies v1 <> 0.V & v2 <> 0.V; theorem :: LMOD_5:6 0.R <> 1_ R implies {v,0.V} is linearly-dependent & {0.V,v} is linearly-dependent; theorem :: LMOD_5:7 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); theorem :: LMOD_5:8 for R being domRing, V being LeftMod of R, L being Linear_Combination of V, a being Scalar of R holds Sum(a * L) = a * Sum(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; definition let R; let V; let A; func Lin(A) -> strict Subspace of V means :: LMOD_5:def 2 the carrier of it = {Sum(l) : not contradiction}; end; theorem :: LMOD_5:9 x in Lin(A) iff ex l st x = Sum(l); theorem :: LMOD_5:10 x in A implies x in Lin(A); theorem :: LMOD_5:11 Lin({}(the carrier of V)) = (0).V; theorem :: LMOD_5:12 Lin(A) = (0).V implies A = {} or A = {0.V}; theorem :: LMOD_5:13 for W being strict Subspace of V st 0.R <> 1_ R & A = the carrier of W holds Lin(A) = W; theorem :: LMOD_5:14 for V being strict LeftMod of R, A being Subset of V st 0.R <> 1_ R & A = the carrier of V holds Lin(A) = V; theorem :: LMOD_5:15 A c= B implies Lin(A) is Subspace of Lin(B); theorem :: LMOD_5:16 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 :: LMOD_5:17 Lin(A \/ B) = Lin(A) + Lin(B); theorem :: LMOD_5:18 Lin(A /\ B) is Subspace of Lin(A) /\ Lin(B);

Back to top