:: Basis of Vector Space
:: by Wojciech A. Trybulec
::
:: Received July 27, 1990
:: Copyright (c) 1990-2017 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, ALGSTR_0, VECTSP_2, 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;