:: Basis of Vector Space
:: by Wojciech A. Trybulec
::
:: Received July 27, 1990
:: Copyright (c) 1990-2016 Association of Mizar Users

environ

vocabularies HIDDEN, 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 HIDDEN, 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;
definitions XBOOLE_0, VECTSP_4, VECTSP_6, TARSKI;
theorems FUNCT_1, FINSET_1, ORDERS_1, RLVECT_3, TARSKI, VECTSP_1, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6, ZFMISC_1, RLVECT_1, FUNCT_2, RELAT_1, ORDINAL1, XBOOLE_0, XBOOLE_1, CARD_2, STRUCT_0, PARTFUN1, RLVECT_2, SUBSET_1, FINSEQ_1, FINSEQ_3, FINSEQ_4;
schemes FUNCT_1, FUNCT_2, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, VECTSP_1, VECTSP_4, ALGSTR_0, VECTSP_2, ORDINAL1;
constructors HIDDEN, ORDERS_1, REALSET1, VECTSP_5, VECTSP_6, STRUCT_0, GROUP_1, RLVECT_2, VECTSP_2, PARTFUN1, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities VECTSP_4, VECTSP_6, XBOOLE_0;
expansions XBOOLE_0, TARSKI;


definition
let GF be non empty doubleLoopStr ;
let 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;

:: deftheorem defines linearly-independent VECTSP_7:def 1 :
for GF being non empty doubleLoopStr
for V being non empty ModuleStr over GF
for IT being Subset of V holds
( IT is linearly-independent iff for l being Linear_Combination of IT st Sum l = 0. V holds
Carrier l = {} );

notation
let GF be non empty doubleLoopStr ;
let V be non empty ModuleStr over GF;
let IT be Subset of V;
antonym linearly-dependent IT for linearly-independent ;
end;

theorem :: VECTSP_7:1
for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent
proof end;

theorem Th2: :: VECTSP_7:2
for R being non degenerated Ring
for V being LeftMod of R
for A being Subset of V st A is linearly-independent holds
not 0. V in A
proof end;

registration
let GF be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;
cluster empty -> linearly-independent for Element of bool the carrier of V;
coherence
for b1 being Subset of V st b1 is empty holds
b1 is linearly-independent
proof end;
end;

registration
let GF be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ;
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;
cluster finite linearly-independent for Element of bool the carrier of V;
existence
ex b1 being Subset of V st
( b1 is finite & b1 is linearly-independent )
proof end;
end;

theorem :: VECTSP_7:3
for R being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for V being LeftMod of R
for v being Vector of V holds
( {v} is linearly-independent iff v <> 0. V )
proof end;

theorem Th4: :: VECTSP_7:4
for GF being non empty non degenerated right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for v1, v2 being Vector of V st {v1,v2} is linearly-independent holds
v1 <> 0. V
proof end;

theorem Th5: :: VECTSP_7:5
for GF being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for v1, v2 being Vector of V holds
( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) ) )
proof end;

theorem :: VECTSP_7:6
for GF being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for v1, v2 being Vector of V holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Element of GF st (a * v1) + (b * v2) = 0. V holds
( a = 0. GF & b = 0. GF ) )
proof end;

TH2: for GF being Ring
for V being LeftMod of GF
for L being Linear_Combination of V
for 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) )
proof end;

TH3: for GF being Ring
for V being LeftMod of GF
for L being Linear_Combination of V
for a being Scalar of holds Sum (a * L) = a * (Sum L)
proof end;

definition
let GF be Ring;
let V be LeftMod of GF;
let A be Subset of V;
func Lin A -> strict Subspace of V means :Def2: :: VECTSP_7:def 2
 the carrier of it = { (Sum l) where l is Linear_Combination of A : verum } ;
existence
ex b1 being strict Subspace of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum }
proof end;
uniqueness
for b1, b2 being strict Subspace of V st the carrier of b1 = { (Sum l) where l is Linear_Combination of A : verum } & the carrier of b2 = { (Sum l) where l is Linear_Combination of A : verum } holds
b1 = b2 by VECTSP_4:29;
end;

:: deftheorem Def2 defines Lin VECTSP_7:def 2 :
for GF being Ring
for V being LeftMod of GF
for A being Subset of V
for b4 being strict Subspace of V holds
( b4 = Lin A iff the carrier of b4 = { (Sum l) where l is Linear_Combination of A : verum } );

theorem Th7: :: VECTSP_7:7
for x being object
for GF being Ring
for V being LeftMod of GF
for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
proof end;

theorem Th8: :: VECTSP_7:8
for x being object
for GF being Ring
for V being LeftMod of GF
for A being Subset of V st x in A holds
x in Lin A
proof end;

theorem Th9: :: VECTSP_7:9
for GF being Ring
for V being LeftMod of GF holds Lin ({} the carrier of V) = (0). V
proof end;

theorem :: VECTSP_7:10
for GF being Ring
for V being LeftMod of GF
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
proof end;

theorem Th11: :: VECTSP_7:11
for GF being non degenerated Ring
for V being LeftMod of GF
for A being Subset of V
for W being strict Subspace of V st A = the carrier of W holds
Lin A = W
proof end;

theorem :: VECTSP_7:12
for GF being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for V being strict VectSp of GF
for A being Subset of V st A = the carrier of V holds
Lin A = V
proof end;

theorem Th13: :: VECTSP_7:13
for GF being Ring
for V being LeftMod of GF
for A, B being Subset of V st A c= B holds
Lin A is Subspace of Lin B
proof end;

theorem :: VECTSP_7:14
for GF being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
proof end;

theorem :: VECTSP_7:15
for GF being Ring
for V being LeftMod of GF
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
proof end;

theorem :: VECTSP_7:16
for GF being Ring
for V being LeftMod of GF
for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
proof end;

definition
let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;
let V be LeftMod of GF;
let A be Subset of V;
attr A is base means :Def3: :: VECTSP_7:def 3
( A is linearly-independent & Lin A = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) );
end;

:: deftheorem Def3 defines base VECTSP_7:def 3 :
for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for V being LeftMod of GF
for A being Subset of V holds
( A is base iff ( A is linearly-independent & Lin A = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ) );

Lm1: for R being Ring
for a being Scalar of R st - a = 0. R holds
a = 0. R
proof end;

Lm2: for R being non degenerated almost_left_invertible Ring
for V being LeftMod of R
for a being Scalar of
for v being Vector of V st a <> 0. R holds
( (a ") * (a * v) = (1. R) * v & ((a ") * a) * v = (1. R) * v )
proof end;

theorem Th17: :: 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 )
proof end;

theorem Th18: :: VECTSP_7:18
for GF being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for A being Subset of V st Lin A = V holds
ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V )
proof end;

Lem0A: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for V being LeftMod of GF holds {} the carrier of V is linearly-independent
proof end;

registration
let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;
let V be LeftMod of GF;
cluster {} the carrier of V -> linearly-independent ;
coherence
{} the carrier of V is linearly-independent by Lem0A;
end;

registration
let GF be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;
let V be LeftMod of GF;
cluster base for Element of bool the carrier of V;
existence
ex b1 being Subset of V st b1 is base
proof end;
end;

definition
let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative 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;

:: deftheorem defines free VECTSP_7:def 4 :
for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for IT being LeftMod of GF holds
( IT is free iff ex B being Subset of IT st B is base );

Lem1A: for GF being non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for V being LeftMod of GF holds (0). V is free
proof end;

registration
let GF be non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;
let V be LeftMod of GF;
cluster (0). V -> free ;
coherence
(0). V is free by Lem1A;
end;

registration
let GF be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;
cluster non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free for ModuleStr over GF;
existence
ex b1 being LeftMod of GF st
( b1 is strict & b1 is free )
proof end;
end;

definition
let GF be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;
let V be LeftMod of GF;
mode Basis of V is base Subset of V;
end;

theorem :: VECTSP_7:19
for GF being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for V being LeftMod of GF
for A being Subset of V st A is linearly-independent holds
ex I being Basis of V st A c= I
proof end;

theorem :: VECTSP_7:20
for GF being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for V being LeftMod of GF
for A being Subset of V st Lin A = V holds
ex I being Basis of V st I c= A
proof end;

:: Additional, copied from MOD_3
theorem :: VECTSP_7:21
for R being Ring
for V being LeftMod of R
for L being Linear_Combination of V
for 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) ) by TH2;

theorem :: VECTSP_7:22
for R being Ring
for V being LeftMod of R
for L being Linear_Combination of V
for a being Scalar of holds Sum (a * L) = a * (Sum L) by TH3;

theorem :: VECTSP_7:23
for R being non degenerated Ring
for V being LeftMod of R
for v1, v2 being Vector of V st {v1,v2} is linearly-independent holds
( v1 <> 0. V & v2 <> 0. V )
proof end;

theorem :: VECTSP_7:24
for R being domRing
for V being LeftMod of R
for L being Linear_Combination of V
for a being Scalar of R st a <> 0. R holds
Carrier (a * L) = Carrier L
proof end;

theorem Th12: :: VECTSP_7:25
for R being domRing
for V being LeftMod of R
for A being Subset of V
for W being strict Subspace of V st not R is degenerated & A = the carrier of W holds
Lin A = W
proof end;

theorem :: VECTSP_7:26
for R being domRing
for V being strict LeftMod of R
for A being Subset of V st not R is degenerated & A = the carrier of V holds
Lin A = V
proof end;

theorem :: VECTSP_7:27
for R being domRing
for V being strict LeftMod of R
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
proof end;

theorem :: VECTSP_7:28
for R being Ring
for V being LeftMod of R
for v1, v2 being Vector of V st not R is degenerated & {v1,v2} is linearly-independent holds
( v1 <> 0. V & v2 <> 0. V )
proof end;