:: Linear Independence in Left Module over Domain
:: by Micha{\l} Muzalewski and Wojciech Skaba
::
:: Received October 22, 1990
:: Copyright (c) 1990-2013 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 FUNCSDOM, VECTSP_2, VECTSP_1, SUBSET_1, XBOOLE_0, ALGSTR_0,
RLVECT_3, RLVECT_2, CARD_3, SUPINF_2, TARSKI, MESFUNC1, FUNCT_1,
STRUCT_0, FUNCT_2, FINSET_1, RELAT_1, FINSEQ_1, VALUED_1, NAT_1,
FINSEQ_4, NUMBERS, PARTFUN1, RLSUB_1, ARYTM_3;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, NAT_1, FINSET_1,
RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_4, DOMAIN_1,
STRUCT_0, ALGSTR_0, RLVECT_1, VECTSP_1, VECTSP_2, VECTSP_4, VECTSP_5,
VECTSP_6;
constructors PARTFUN1, DOMAIN_1, FINSEQ_4, VECTSP_2, VECTSP_5, VECTSP_6,
RELSET_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, STRUCT_0,
VECTSP_1, VECTSP_4, ORDINAL1;
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) = {};
end;
notation
let R be non empty doubleLoopStr;
let V be non empty VectSpStr over R;
let IT be Subset of V;
antonym IT is linearly-dependent for IT is linearly-independent;
end;
theorem :: LMOD_5:1
A c= B & B is linearly-independent implies A is linearly-independent;
theorem :: LMOD_5:2
0.R <> 1.R & A is linearly-independent implies not 0.V in A;
theorem :: LMOD_5:3
{}(the carrier of V) is linearly-independent;
theorem :: LMOD_5:4
0.R <> 1.R & {v1,v2} is linearly-independent implies v1 <> 0.V & v2 <> 0.V;
theorem :: LMOD_5:5
0.R <> 1.R implies {v,0.V} is linearly-dependent & {0.V,v} is
linearly-dependent;
theorem :: LMOD_5:6
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:7
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 = the set of all Sum(l) ;
end;
theorem :: LMOD_5:8
x in Lin(A) iff ex l st x = Sum(l);
theorem :: LMOD_5:9
x in A implies x in Lin(A);
theorem :: LMOD_5:10
Lin({}(the carrier of V)) = (0).V;
theorem :: LMOD_5:11
Lin(A) = (0).V implies A = {} or A = {0.V};
theorem :: LMOD_5:12
for W being strict Subspace of V st 0.R <> 1.R & A = the carrier
of W holds Lin(A) = W;
theorem :: LMOD_5:13
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:14
A c= B implies Lin(A) is Subspace of Lin(B);
theorem :: LMOD_5:15
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:16
Lin(A \/ B) = Lin(A) + Lin(B);
theorem :: LMOD_5:17
Lin(A /\ B) is Subspace of Lin(A) /\ Lin(B);