:: Basis of Vector Space
:: by Wojciech A. Trybulec
::
:: Received July 27, 1990
:: Copyright (c) 1990-2026 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;
definitions XBOOLE_0, VECTSP_4, VECTSP_6, TARSKI;
equalities VECTSP_4, VECTSP_6;
expansions XBOOLE_0, 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;
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
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
A c= B & B is linearly-independent implies A is linearly-independent
proof
assume that
A1: A c= B and
A2: B is linearly-independent;
let l be Linear_Combination of A;
reconsider L = l as Linear_Combination of B by A1,VECTSP_6:4;
assume Sum(l) = 0.V;
then Carrier(L) = {} by A2;
hence thesis;
end;
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 Th2:
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
proof
let R be non degenerated Ring,
V be LeftMod of R,
A be Subset of V;
assume that
A2: A is linearly-independent and
A3: 0.V in A;
deffunc U(set) = 0.R;
consider f be Function of the carrier of V, the carrier of R such that
A4: f.(0.V) = 1.R and
A5: for v be Element of V st v <> 0.V holds f.v = U(v) from FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V, the carrier of R) by
FUNCT_2:8;
ex T be finite Subset of V st for v being Vector of V
st not v in T holds f.v = 0.R
proof
take T = {0.V};
let v be Vector of V;
assume not v in T;
then v <> 0.V by TARSKI:def 1;
hence thesis by A5;
end;
then reconsider f as Linear_Combination of V by VECTSP_6:def 1;
A6: Carrier(f) = {0.V}
proof
thus Carrier(f) c= {0.V}
proof
let x be object;
assume x in Carrier(f);
then consider v being Vector of V such that
A7: v = x and
A8: f.v <> 0.R;
v = 0.V by A5,A8;
hence thesis by A7,TARSKI:def 1;
end;
let x be object;
assume x in {0.V};
then x = 0.V by TARSKI:def 1;
hence thesis by A4;
end;
then Carrier(f) c= A by A3,ZFMISC_1:31;
then reconsider f as Linear_Combination of A by VECTSP_6:def 4;
Sum(f) = f.(0.V) * 0.V by A6,VECTSP_6:20
.= 0.V by VECTSP_1:14;
hence contradiction by A2,A6;
end;
registration
let GF,V;
cluster empty -> linearly-independent for Subset of V;
coherence
proof
let S be Subset of V such that
A1: S is empty;
let l be Linear_Combination of S;
Carrier(l) c= {} by A1,VECTSP_6:def 4;
hence thesis;
end;
end;
registration
let GF, V;
cluster finite linearly-independent for Subset of V;
existence
proof
take {}V;
thus thesis;
end;
end;
theorem
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
proof
let R be commutative non degenerated almost_left_invertible
Abelian add-associative right_zeroed right_complementable
associative well-unital distributive non empty doubleLoopStr;
let V be LeftMod of R,
v be Vector of V;
thus {v} is linearly-independent implies v <> 0.V
proof
assume {v} is linearly-independent;
then not 0.V in {v} by Th2;
hence thesis by TARSKI:def 1;
end;
assume
A1: v <> 0.V;
let l be Linear_Combination of {v};
A2: Carrier(l) c= {v} by VECTSP_6:def 4;
assume
A3: Sum(l) = 0.V;
now
per cases by A2,ZFMISC_1:33;
suppose
Carrier(l) = {};
hence thesis;
end;
suppose
A4: Carrier(l) = {v};
A5: 0.V = l.v * v by A3,VECTSP_6:17;
now
assume v in Carrier(l);
then ex u being Vector of V st v = u & l.u <> 0.R;
hence contradiction by A1,A5,VECTSP_1:15;
end;
hence thesis by A4,TARSKI:def 1;
end;
end;
hence thesis;
end;
theorem Th4:
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
proof
let GF be commutative non degenerated
Abelian add-associative right_zeroed right_complementable
associative well-unital distributive non empty doubleLoopStr,
V be scalar-distributive vector-distributive
scalar-associative scalar-unital add-associative right_zeroed
right_complementable Abelian non empty ModuleStr over GF,
v1, v2 be Vector of V;
A1: v1 in {v1,v2} by TARSKI:def 2;
assume {v1,v2} is linearly-independent;
hence thesis by A1,Th2;
end;
theorem Th5:
v1 <> v2 & {v1,v2} is linearly-independent iff v2 <> 0.V &
for a holds v1 <> a * v2
proof
thus v1 <> v2 & {v1,v2} is linearly-independent implies v2 <> 0.V & for a
holds v1 <> a * v2
proof
deffunc F(set) = 0.GF;
assume that
A1: v1 <> v2 and
A2: {v1,v2} is linearly-independent;
thus v2 <> 0.V by A2,Th4;
let a;
consider f such that
A3: f.v1 = - 1_GF & f.v2 = a and
A4: for v being Element of V st v <> v1 & v <> v2 holds f.v = F(v)
from FUNCT_2:sch 7(A1);
reconsider f as Element of Funcs(the carrier of V, the carrier of GF) by
FUNCT_2:8;
now
let v;
assume not v in ({v1,v2});
then v <> v1 & v <> v2 by TARSKI:def 2;
hence f.v = 0.GF by A4;
end;
then reconsider f as Linear_Combination of V by VECTSP_6:def 1;
Carrier(f) c= {v1,v2}
proof
let x be object;
assume x in Carrier(f); then
A5: ex u st x = u & f.u <> 0.GF;
assume not x in {v1,v2};
then x <> v1 & x <> v2 by TARSKI:def 2;
hence thesis by A4,A5;
end;
then reconsider f as Linear_Combination of {v1,v2} by VECTSP_6:def 4;
A6: now
assume not v1 in Carrier(f);
then 0.GF = - 1_GF by A3;
hence contradiction by VECTSP_6:49;
end;
set w = a * v2;
assume v1 = a * v2;
then Sum(f) = (- 1_GF) * w + w by A1,A3,VECTSP_6:18
.= (- w) + w by VECTSP_1:14
.= - (w - w) by VECTSP_1:17
.= - 0.V by VECTSP_1:19
.= 0.V by RLVECT_1:12;
hence thesis by A2,A6;
end;
assume
A7: v2 <> 0.V;
assume
A8: for a holds v1 <> a * v2;
A9: 1_GF * v2 = v2;
hence v1 <> v2 by A8;
let l be Linear_Combination of {v1,v2};
assume that
A10: Sum(l) = 0.V and
A11: Carrier(l) <> {};
A12: 0.V = l.v1 * v1 + l.v2 * v2 by A8,A9,A10,VECTSP_6:18;
set x = the Element of Carrier(l);
Carrier(l) c= {v1,v2} by VECTSP_6:def 4;
then
A13: x in {v1,v2} by A11;
x in Carrier(l) by A11;
then
A14: ex u st x = u & l.u <> 0.GF;
now
per cases by A14,A13,TARSKI:def 2;
suppose
A15: l.v1 <> 0.GF;
0.V = (l.v1)" * (l.v1 * v1 + l.v2 * v2) by A12,VECTSP_1:15
.= (l.v1)" * (l.v1 * v1) + (l.v1)" * (l.v2 * v2) by VECTSP_1:def 14
.= (l.v1)" * l.v1 * v1 + (l.v1)" * (l.v2 * v2) by VECTSP_1:def 16
.= (l.v1)" * l.v1 * v1 + (l.v1)" * l.v2 * v2 by VECTSP_1:def 16
.= 1_GF * v1 + (l.v1)" * l.v2 * v2 by A15,VECTSP_1:def 10
.= v1 + (l.v1)" * l.v2 * v2;
then v1 = - ((l.v1)" * l.v2 * v2) by VECTSP_1:16
.= (- 1_GF) * ((l.v1)" * l.v2 * v2) by VECTSP_1:14
.= ((- 1_GF) * ((l.v1)" * l.v2)) * v2 by VECTSP_1:def 16;
hence thesis by A8;
end;
suppose
A16: l.v2 <> 0.GF & l.v1 = 0.GF;
0.V = (l.v2)" * (l.v1 * v1 + l.v2 * v2) by A12,VECTSP_1:15
.= (l.v2)" * (l.v1 * v1) + (l.v2)" * (l.v2 * v2) by VECTSP_1:def 14
.= (l.v2)" * l.v1 * v1 + (l.v2)" * (l.v2 * v2) by VECTSP_1:def 16
.= (l.v2)" * l.v1 * v1 + (l.v2)" * l.v2 * v2 by VECTSP_1:def 16
.= (l.v2)" * l.v1 * v1 + 1_GF * v2 by A16,VECTSP_1:def 10
.= (l.v2)" * l.v1 * v1 + v2
.= 0.GF * v1 + v2 by A16
.= 0.V + v2 by VECTSP_1:15
.= v2 by RLVECT_1:4;
hence thesis by A7;
end;
end;
hence thesis;
end;
theorem
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
proof
thus v1 <> v2 & {v1,v2} is linearly-independent implies for a,b st a * v1 +
b * v2 = 0.V holds a = 0.GF & b = 0.GF
proof
assume
A1: v1 <> v2 & {v1,v2} is linearly-independent;
let a,b;
assume that
A2: a * v1 + b * v2 = 0.V and
A3: a <> 0.GF or b <> 0.GF;
now
per cases by A3;
suppose
A4: a <> 0.GF;
0.V = a" * (a * v1 + b * v2) by A2,VECTSP_1:15
.= a" * (a * v1) + a" * (b * v2) by VECTSP_1:def 14
.= (a" * a) * v1 + a" * (b * v2) by VECTSP_1:def 16
.= (a" * a) * v1 + (a" * b) * v2 by VECTSP_1:def 16
.= 1_GF * v1 + (a" * b) * v2 by A4,VECTSP_1:def 10
.= v1 + (a" * b) * v2;
then v1 = - ((a" * b) * v2) by VECTSP_1:16
.= (- 1_GF) * ((a" * b) * v2) by VECTSP_1:14
.= (- 1_GF) * (a" * b) * v2 by VECTSP_1:def 16;
hence thesis by A1,Th5;
end;
suppose
A5: b <> 0.GF;
0.V = b" * (a * v1 + b * v2) by A2,VECTSP_1:15
.= b" * (a * v1) + b" * (b * v2) by VECTSP_1:def 14
.= (b" * a) * v1 + b" * (b * v2) by VECTSP_1:def 16
.= (b" * a) * v1 + (b" * b) * v2 by VECTSP_1:def 16
.= (b" * a) * v1 + 1_GF* v2 by A5,VECTSP_1:def 10
.= (b" * a) * v1 + v2;
then v2 = - ((b" * a) * v1) by VECTSP_1:16
.= (- 1_GF) * ((b" * a) * v1) by VECTSP_1:14
.= (- 1_GF) * (b" * a) * v1 by VECTSP_1:def 16;
hence thesis by A1,Th5;
end;
end;
hence thesis;
end;
assume
A6: for a,b st a * v1 + b * v2 = 0.V holds a = 0.GF & b = 0.GF;
A7: now
let a;
assume v1 = a * v2;
then v1 = 0.V + a * v2 by RLVECT_1:4;
then 0.V = v1 - a * v2 by VECTSP_2:2
.= v1 + ((- a) * v2) by VECTSP_1:21
.= 1.GF * v1 + (- a) * v2;
hence contradiction by A6;
end;
now
assume
A8: v2 = 0.V;
0.V = 0.V + 0.V by RLVECT_1:4
.= 0.GF * v1 + 0.V by VECTSP_1:15
.= 0.GF * v1 + 1.GF * v2 by A8;
hence contradiction by A6;
end;
hence thesis by A7,Th5;
end;
TH2:
for GF be Ring,
V be LeftMod of GF,
L be Linear_Combination of V,
C be finite Subset of V holds
Carrier(L) c= C implies ex F being FinSequence of V st
F is one-to-one & rng F = C & Sum (L) = Sum(L (#) F)
proof
let GF be Ring,
V be LeftMod of GF,
L be Linear_Combination of V,
C be finite Subset of V;
assume
A1: Carrier(L) c= C;
set D = C \ Carrier(L);
consider G being FinSequence of V such that
A2: G is one-to-one and
A3: rng G = Carrier(L) and
A4: Sum(L) = Sum(L (#) G) by VECTSP_6:def 6;
consider p being FinSequence such that
A5: rng p = D and
A6: p is one-to-one by FINSEQ_4:58;
reconsider p as FinSequence of the carrier of V by A5,FINSEQ_1:def 4;
A7: rng G misses rng p
proof
assume rng G meets rng p;
then ex x being object st x in Carrier(L) & x in D by A3,A5,XBOOLE_0:3;
hence thesis by XBOOLE_0:def 5;
end;
A8: len p = len(L (#) p) by VECTSP_6:def 5;
now
let k be Nat;
assume
A9: k in dom p;
then p/.k = p.k by PARTFUN1:def 6;
then p/.k in D by A5,A9,FUNCT_1:def 3;
then
A10: not p/.k in Carrier(L) by XBOOLE_0:def 5;
k in dom(L (#) p) by A8,A9,FINSEQ_3:29;
then (L (#) p).k = L.(p/.k) * (p/.k) by VECTSP_6:def 5;
hence (L (#) p).k = 0.GF * (p/.k) by A10;
end;
then
A11: Sum(L (#) p) = 0.GF * Sum(p) by A8,RLVECT_2:67
.= 0.V by VECTSP_1:14;
set F = G ^ p;
take F;
A12: Sum((L (#) F)) = Sum((L (#) G) ^ (L (#) p)) by VECTSP_6:13
.= Sum(L (#) G) + 0.V by A11,RLVECT_1:41
.= Sum(L) by A4,RLVECT_1:def 4;
rng F = Carrier(L) \/ D by A3,A5,FINSEQ_1:31
.= C by A1,XBOOLE_1:45;
hence thesis by A2,A6,A12,A7,FINSEQ_3:91;
end;
TH3:
for GF be Ring,
V be LeftMod of GF,
L be Linear_Combination of V,
a be Scalar of V holds
Sum(a * L) = a * Sum(L)
proof
let GF be Ring,
V be LeftMod of GF,
L be Linear_Combination of V,
a be Scalar of GF;
set l = a * L;
Carrier(l) c= Carrier(L) by VECTSP_6:28;
then consider F being FinSequence of the carrier of V such that
A1: F is one-to-one & rng F = Carrier(L) and
A2: Sum(l) = Sum(l (#) F) by TH2;
set f = l (#) F, g = L (#) F;
A3: len f = len F by VECTSP_6:def 5
.= len g by VECTSP_6:def 5;
len f = len F by VECTSP_6:def 5;
then
A4: dom F = Seg len f by FINSEQ_1:def 3;
A5: now
let k be Nat, v be Vector of V;
assume that
A6: k in dom f and
A7: v = g.k;
set v9 = F/.k;
A8: k in Seg len f by A6,FINSEQ_1:def 3;
then
A9: v9 = F.k by A4,PARTFUN1:def 6;
hence f.k = l.v9*v9 by A4,A8,VECTSP_6:8
.= (a*L.v9)*v9 by VECTSP_6:def 9
.= a*(L.v9*v9) by VECTSP_1:def 16
.= a*v by A4,A7,A8,A9,VECTSP_6:8;
end;
Sum(L) = Sum(L (#) F) by A1,VECTSP_6:def 6;
hence thesis by A2,A3,A5,RLVECT_2:66;
end;
definition
let GF be Ring;
let V be LeftMod of GF,
A be Subset of V;
func Lin(A) -> strict Subspace of V means :Def2:
the carrier of it = the set of all Sum(l) where
l is Linear_Combination of A;
existence
proof
set A1 = the set of all Sum(l) where l is Linear_Combination of A;
A1 c= the carrier of V
proof
let x be object;
assume x in A1;
then ex l being Linear_Combination of A st x = Sum(l);
hence thesis;
end;
then reconsider A1 as Subset of V;
reconsider l = ZeroLC(V) as Linear_Combination of A by VECTSP_6:5;
A1: A1 is linearly-closed
proof
thus for v,u being Vector of V st v in A1 & u in A1 holds v + u in A1
proof
let v,u be Vector of V;
assume that
A2: v in A1 and
A3: u in A1;
consider l1 being Linear_Combination of A such that
A4: v = Sum(l1) by A2;
consider l2 being Linear_Combination of A such that
A5: u = Sum(l2) by A3;
reconsider f = l1 + l2 as Linear_Combination of A by VECTSP_6:24;
v + u = Sum(f) by A4,A5,VECTSP_6:44;
hence thesis;
end;
let a be Scalar of V,v be Vector of V;
assume v in A1;
then consider l being Linear_Combination of A such that
A6: v = Sum(l);
reconsider f = a * l as Linear_Combination of A by VECTSP_6:31;
a * v = Sum(f) by A6,TH3;
hence thesis;
end;
Sum(l) = 0.V by VECTSP_6:15;
then 0.V in A1;
hence thesis by A1,VECTSP_4:34;
end;
uniqueness by VECTSP_4:29;
end;
theorem Th7:
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)
proof
let GF be Ring,
V be LeftMod of GF,
A be Subset of V;
thus x in Lin(A) implies ex l being Linear_Combination of A st x = Sum(l)
proof
assume x in Lin(A);
then x in the carrier of Lin(A) by STRUCT_0:def 5;
then x in the set of all Sum(l) where l is Linear_Combination of A
by Def2;
hence thesis;
end;
given k being Linear_Combination of A such that
A1: x = Sum(k);
x in the set of all Sum(l) where l is Linear_Combination of A by A1;
then x in the carrier of Lin(A) by Def2;
hence thesis by STRUCT_0:def 5;
end;
theorem Th8:
for GF be Ring,
V be LeftMod of GF,
A be Subset of V holds
x in A implies x in Lin(A)
proof
let GF be Ring,
V be LeftMod of GF,
A be Subset of V;
deffunc F(set) = 0.GF;
assume
A1: x in A;
then reconsider v = x as Vector of V;
consider f being Function of V, GF such that
A2: f.v = 1_GF and
A3: for u being Vector of V st u <> v holds f.u = F(u) from FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V, the carrier of GF) by
FUNCT_2:8;
ex T being finite Subset of V st
for u being Vector of V st not u in T holds f.u = 0.GF
proof
take T = {v};
let u be Vector of V;
assume not u in T;
then u <> v by TARSKI:def 1;
hence thesis by A3;
end;
then reconsider f as Linear_Combination of V by VECTSP_6:def 1;
A4: Carrier(f) c= {v}
proof
let x be object;
assume x in Carrier(f);
then consider u being Vector of V such that
A5: x = u and
A6: f.u <> 0.GF;
u = v by A3,A6;
hence thesis by A5,TARSKI:def 1;
end;
then reconsider f as Linear_Combination of {v} by VECTSP_6:def 4;
A7: Sum(f) = 1_GF * v by A2,VECTSP_6:17
.= v;
{v} c= A by A1,ZFMISC_1:31;
then Carrier(f) c= A by A4;
then reconsider f as Linear_Combination of A by VECTSP_6:def 4;
Sum(f) = v by A7;
hence thesis by Th7;
end;
reserve l0 for Linear_Combination of {}(the carrier of V);
theorem Th9:
for GF be Ring,
V be LeftMod of GF holds
Lin({}(the carrier of V)) = (0).V
proof
let GF be Ring,
V be LeftMod of GF;
set A = Lin({}(the carrier of V));
now
let v be Vector of V;
thus v in A implies v in (0).V
proof
assume v in A; then
A1: v in the carrier of A by STRUCT_0:def 5;
the carrier of A = the set of all Sum(l0) where
l0 is Linear_Combination of {}the carrier of V by Def2;
then ex l0 being Linear_Combination of
{}the carrier of V st v = Sum(l0) by A1;
then v = 0.V by VECTSP_6:16;
hence thesis by VECTSP_4:35;
end;
assume v in (0).V;
then v = 0.V by VECTSP_4:35;
hence v in A by VECTSP_4:17;
end;
hence thesis by VECTSP_4:30;
end;
theorem
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}
proof
let GF be Ring,
V be LeftMod of GF,
A be Subset of V;
assume that
A1: Lin(A) = (0).V and
A2: A <> {};
thus A c= {0.V}
proof
let x be object;
assume x in A;
then x in Lin(A) by Th8;
then x = 0.V by A1,VECTSP_4:35;
hence thesis by TARSKI:def 1;
end;
set y = the Element of A;
let x be object;
assume x in {0.V};
then
A3: x = 0.V by TARSKI:def 1;
y in A & y in Lin(A) by A2,Th8;
hence thesis by A1,A3,VECTSP_4:35;
end;
theorem Th11:
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
proof
let GF be non degenerated Ring,
V be LeftMod of GF,
A be Subset of V;
let W be strict Subspace of V;
assume
A1: A = the carrier of W;
now
let v be Vector of V;
A2: 0.GF <> 1.GF;
thus v in Lin(A) implies v in W
proof
assume v in Lin(A); then
A3: ex l being Linear_Combination of A st v = Sum(l) by Th7;
A is linearly-closed by A1,VECTSP_4:33;
then v in the carrier of W by A1,A2,A3,VECTSP_6:14;
hence thesis by STRUCT_0:def 5;
end;
v in W iff v in the carrier of W by STRUCT_0:def 5;
hence v in W implies v in Lin(A) by A1,Th8;
end;
hence thesis by VECTSP_4:30;
end;
theorem
for V being strict VectSp of GF, A being Subset of V st
A = the carrier of V holds Lin(A) = V
proof
let V be strict VectSp of GF, A be Subset of V such that
A1: A = the carrier of V;
(Omega).V = V;
hence thesis by A1,Th11;
end;
theorem Th13:
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)
proof
let GF be Ring,
V be LeftMod of GF,
A,B be Subset of V;
assume
A1: A c= B;
now
let v be Vector of V;
assume v in Lin(A);
then consider l being Linear_Combination of A such that
A2: v = Sum(l) by Th7;
reconsider l as Linear_Combination of B by A1,VECTSP_6:4;
Sum(l) = v by A2;
hence v in Lin(B) by Th7;
end;
hence thesis by VECTSP_4:28;
end;
theorem
Lin(A) = V & A c= B implies Lin(B) = V
proof
assume that
A1: Lin(A) = V and
A2: A c= B;
V is Subspace of Lin(B) by A1,A2,Th13;
hence thesis by A1,VECTSP_4:25;
end;
theorem
for GF be Ring,
V be LeftMod of GF,
A,B be Subset of V holds
Lin(A \/ B) = Lin(A) + Lin(B)
proof
let GF be Ring,
V be LeftMod of GF,
A,B be Subset of V;
now
deffunc F(object) = 0.GF;
let v be Vector of V;
assume v in Lin(A \/ B);
then consider l being Linear_Combination of A \/ B such that
A1: v = Sum(l) by Th7;
deffunc G(object) = l.$1;
set D = Carrier(l) \ A;
set C = Carrier(l) /\ A;
defpred P[object] means $1 in C;
A2: now
let x be object;
assume x in the carrier of V;
then reconsider v = x as Vector of V;
for f being Function of V, GF holds
f.v in the carrier of GF;
hence P[x] implies G(x) in the carrier of GF;
assume not P[x];
thus F(x) in the carrier of GF;
end;
reconsider C as finite Subset of V;
defpred C[object] means $1 in D;
reconsider D as finite Subset of V;
A3: D c= B
proof
let x be object;
assume x in D;
then
A4: x in Carrier(l) & not x in A by XBOOLE_0:def 5;
Carrier(l) c= A \/ B by VECTSP_6:def 4;
hence thesis by A4,XBOOLE_0:def 3;
end;
consider f being Function of V, GF such that
A5: for x being object st x in the carrier of V
holds (P[x] implies f.x = G(x)) &
(not P[x] implies f.x = F(x)) from FUNCT_2:sch 5 (A2);
reconsider f as Element of Funcs(the carrier of V, the carrier of GF) by
FUNCT_2:8;
for u being Vector of V holds not u in C implies f.u = 0.GF by A5;
then reconsider f as Linear_Combination of V by VECTSP_6:def 1;
A6: Carrier(f) c= C
proof
let x be object;
assume x in Carrier(f);
then
A7: ex u being Vector of V st x = u & f.u <> 0.GF;
assume not x in C;
hence thesis by A5,A7;
end;
C c= A by XBOOLE_1:17;
then Carrier(f) c= A by A6;
then reconsider f as Linear_Combination of A by VECTSP_6:def 4;
deffunc G(object) = l.$1;
A8: now
let x be object;
assume x in the carrier of V;
then reconsider v = x as Vector of V;
for g being Function of V, GF holds
g.v in the carrier of GF;
hence C[x] implies G(x) in the carrier of GF;
assume not C[x];
thus F(x) in the carrier of GF;
end;
consider g being Function of the carrier of V, the carrier of GF such that
A9: for x being object st x in the carrier of V
holds (C[x] implies g.x = G(x)) &
(not C[x] implies g.x = F(x)) from FUNCT_2:sch 5 (A8);
reconsider g as Element of Funcs(the carrier of V, the carrier of GF) by
FUNCT_2:8;
for u being Vector of V holds not u in D implies g.u = 0.GF by A9;
then reconsider g as Linear_Combination of V by VECTSP_6:def 1;
Carrier(g) c= D
proof
let x be object;
assume x in Carrier(g);
then
A10: ex u being Vector of V st x = u & g.u <> 0.GF;
assume not x in D;
hence thesis by A9,A10;
end;
then Carrier(g) c= B by A3;
then reconsider g as Linear_Combination of B by VECTSP_6:def 4;
l = f + g
proof
let v be Vector of V;
now
per cases;
suppose
A11: v in C;
A12: now
assume v in D;
then not v in A by XBOOLE_0:def 5;
hence contradiction by A11,XBOOLE_0:def 4;
end;
thus (f + g).v = f.v + g.v by VECTSP_6:22
.= l.v + g.v by A5,A11
.= l.v + 0.GF by A9,A12
.= l.v by RLVECT_1:4;
end;
suppose
A13: not v in C;
now
per cases;
suppose
A14: v in Carrier(l);
A15: now
assume not v in D;
then not v in Carrier(l) or v in A by XBOOLE_0:def 5;
hence contradiction by A13,A14,XBOOLE_0:def 4;
end;
thus (f + g). v = f.v + g.v by VECTSP_6:22
.= g.v + 0.GF by A5,A13
.= g.v by RLVECT_1:4
.= l.v by A9,A15;
end;
suppose
A16: not v in Carrier(l);
then
A17: not v in D by XBOOLE_0:def 5;
A18: not v in C by A16,XBOOLE_0:def 4;
thus (f + g).v = f.v + g.v by VECTSP_6:22
.= 0.GF + g.v by A5,A18
.= 0.GF + 0.GF by A9,A17
.= 0.GF by RLVECT_1:4
.= l.v by A16;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then
A19: v = Sum(f) + Sum(g) by A1,VECTSP_6:44;
Sum(f) in Lin(A) & Sum(g) in Lin(B) by Th7;
hence v in Lin(A) + Lin(B) by A19,VECTSP_5:1;
end;
then
A20: Lin(A \/ B) is Subspace of Lin(A) + Lin(B) by VECTSP_4:28;
Lin(A) is Subspace of Lin(A \/ B) & Lin(B) is Subspace of Lin(A \/ B) by Th13
,XBOOLE_1:7;
then Lin(A) + Lin(B) is Subspace of Lin(A \/ B) by VECTSP_5:34;
hence thesis by A20,VECTSP_4:25;
end;
theorem
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)
proof
let GF be Ring,
V be LeftMod of GF,
A,B be Subset of V;
Lin(A /\ B) is Subspace of Lin(A) &
Lin(A /\ B) is Subspace of Lin(B) by Th13,XBOOLE_1:17;
hence thesis by VECTSP_5:19;
end;
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 :Def3:
A is linearly-independent & Lin A = the ModuleStr of V;
end;
Lm1: for R being Ring, a being Scalar of R holds -a = 0.R implies a = 0.R
proof
let R be Ring, a be Scalar of R;
assume -a = 0.R;
then --a = 0.R by RLVECT_1:12;
hence thesis by RLVECT_1:17;
end;
Lm2:
for R being non degenerated almost_left_invertible Ring
for V being LeftMod of R for a being Scalar of V, v being Vector of V holds
a <> 0.R implies a"*(a*v) = 1.R*v & (a"*a)*v = 1.R*v
proof
let R be non degenerated almost_left_invertible Ring;
let V be LeftMod of R,
a be Scalar of V,
v be Vector of V;
assume
A1: a <> 0.R;
hence a"*(a*v) = v by VECTSP_2:31
.= 1.R*v;
thus thesis by A1,VECTSP_2:9;
end;
theorem Th17:
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
let R be non degenerated almost_left_invertible Ring;
let V be LeftMod of R;
let A be Subset of V;
defpred P[set] means
ex B being Subset of V st B = $1 & A c= B & B is linearly-independent;
consider Q being set such that
A1: for Z holds Z in Q iff Z in bool(the carrier of V) & P[Z] from
XFAMILY:sch 1;
A2: now
let Z;
assume that
A3: Z <> {} and
A4: Z c= Q and
A5: Z is c=-linear;
set W = union Z;
W c= the carrier of V
proof
let x be object;
assume x in W;
then consider X such that
A6: x in X and
A7: X in Z by TARSKI:def 4;
X in bool(the carrier of V) by A1,A4,A7;
hence thesis by A6;
end;
then reconsider W as Subset of V;
A8: W is linearly-independent
proof
deffunc F(object)={C where C is Subset of V : $1 in C & C in Z};
let l be Linear_Combination of W;
assume that
A9: Sum(l) = 0.V and
A10: Carrier(l) <> {};
consider f being Function such that
A11: dom f = Carrier(l) and
A12: for x being object st x in Carrier(l) holds f.x = F(x)
from FUNCT_1:sch 3;
reconsider M = rng f as non empty set by A10,A11,RELAT_1:42;
set F = the Choice_Function of M;
set S = rng F;
A13: now
assume {} in M;
then consider x being object such that
A14: x in dom f and
A15: f.x = {} by FUNCT_1:def 3;
Carrier(l) c= W by VECTSP_6:def 4;
then consider X such that
A16: x in X and
A17: X in Z by A11,A14,TARSKI:def 4;
reconsider X as Subset of V by A1,A4,A17;
X in {C where C is Subset of V : x in C & C in Z} by A16,A17;
hence contradiction by A11,A12,A14,A15;
end;
then
A18: dom F = M by RLVECT_3:28;
then dom F is finite by A11,FINSET_1:8;
then
A19: S is finite by FINSET_1:8;
A20: now
let X;
assume X in S;
then consider x being object such that
A21: x in dom F and
A22: F.x = X by FUNCT_1:def 3;
consider y being object such that
A23: y in dom f & f.y = x by A18,A21,FUNCT_1:def 3;
A24: x = {C where C is Subset of V: y in C & C in Z} by A11,A12,A23;
reconsider x as set by TARSKI:1;
X in x by A13,A18,A21,A22,ORDERS_1:89;
then ex C being Subset of V st C = X & y in C & C in Z by A24;
hence X in Z;
end;
A25: now
let X,Y;
assume X in S & Y in S;
then X in Z & Y in Z by A20;
then X,Y are_c=-comparable by A5,ORDINAL1:def 8;
hence X c= Y or Y c= X;
end;
S <> {} by A18,RELAT_1:42;
then union S in S by A25,A19,CARD_2:62;
then union S in Z by A20;
then consider B being Subset of V such that
A26: B = union S and
A c= B and
A27: B is linearly-independent by A1,A4;
Carrier(l) c= union S
proof
let x be object;
set X = f.x;
assume
A28: x in Carrier(l);
then
A29: f.x = {C where C is Subset of V : x in C & C in Z} by A12;
A30: f.x in M by A11,A28,FUNCT_1:def 3;
then F.X in X by A13,ORDERS_1:89;
then
A31: ex C being Subset of V st F.X = C & x in C & C in Z by A29;
F.X in S by A18,A30,FUNCT_1:def 3;
hence thesis by A31,TARSKI:def 4;
end;
then l is Linear_Combination of B by A26,VECTSP_6:def 4;
hence thesis by A9,A10,A27;
end;
set x = the Element of Z;
x in Q by A3,A4;
then
A32: ex B being Subset of V st B = x & A c= B & B is linearly-independent
by A1;
x c= W by A3,ZFMISC_1:74;
then A c= W by A32;
hence union Z in Q by A1,A8;
end;
assume A is linearly-independent;
then Q <> {} by A1;
then consider X such that
A33: X in Q and
A34: for Z st Z in Q & Z <> X holds not X c= Z by A2,ORDERS_1:67;
consider B being Subset of V such that
A35: B = X and
A36: A c= B and
A37: B is linearly-independent by A1,A33;
take B;
thus A c= B & B is linearly-independent by A36,A37;
assume Lin(B) <> the ModuleStr of V;
then consider v being Vector of V such that
A38: not (v in Lin(B) iff v in (Omega).V) by VECTSP_4:30;
A39: B \/ {v} is linearly-independent
proof
let l be Linear_Combination of B \/ {v};
assume
A40: Sum(l) = 0.V;
now
per cases;
suppose
v in Carrier(l);
then l.v <> 0.R by VECTSP_6:2;
then - l.v <> 0.R by Lm1;
then
A41: (- l.v)" * ((- l.v) * v) = 1.R * v by Lm2
.= v;
deffunc F(Vector of V) = l.$1;
consider f being Function of the carrier of V, the carrier of R such
that
A42: f.v = 0.R and
A43: for u being Vector of V st u <> v holds f.u = F(u) from
FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V, the carrier of R)
by FUNCT_2:8;
now
let u be Vector of V;
assume not u in Carrier(l) \ {v};
then not u in Carrier(l) or u in {v} by XBOOLE_0:def 5;
then l.u = 0.R & u <> v or u = v by TARSKI:def 1;
hence f.u = 0.R by A42,A43;
end;
then reconsider f as Linear_Combination of V by VECTSP_6:def 1;
Carrier(f) c= B
proof
let x be object;
A44: Carrier(l) c= B \/ {v} by VECTSP_6:def 4;
assume x in Carrier(f);
then consider u being Vector of V such that
A45: u = x and
A46: f.u <> 0.R;
f.u = l.u by A42,A43,A46;
then u in Carrier(l) by A46;
then u in B or u in {v} by A44,XBOOLE_0:def 3;
hence thesis by A42,A45,A46,TARSKI:def 1;
end;
then reconsider f as Linear_Combination of B by VECTSP_6:def 4;
deffunc F(Vector of V)=0.R;
consider g being Function of the carrier of V, the carrier of R such
that
A47: g.v = - l.v and
A48: for u being Vector of V st u <> v holds g.u = F(u) from
FUNCT_2:sch 6;
reconsider g as Element of Funcs(the carrier of V, the carrier of R)
by FUNCT_2:8;
now
let u be Vector of V;
assume not u in {v};
then u <> v by TARSKI:def 1;
hence g.u = 0.R by A48;
end;
then reconsider g as Linear_Combination of V by VECTSP_6:def 1;
Carrier(g) c= {v}
proof
let x be object;
assume x in Carrier(g);
then ex u being Vector of V st x = u & g.u <> 0.R;
then x = v by A48;
hence thesis by TARSKI:def 1;
end;
then reconsider g as Linear_Combination of {v} by VECTSP_6:def 4;
f - g = l
proof
let u be Vector of V;
now
per cases;
suppose
A49: v = u;
thus (f - g).u = f.u - g.u by VECTSP_6:40
.= 0.R + (- (- l.v)) by A42,A47,A49,RLVECT_1:def 11
.= l.v + 0.R by RLVECT_1:17
.= l.u by A49,RLVECT_1:4;
end;
suppose
A50: v <> u;
thus (f - g).u = f.u - g.u by VECTSP_6:40
.= l.u - g.u by A43,A50
.= l.u - 0.R by A48,A50
.= l.u by RLVECT_1:13;
end;
end;
hence thesis;
end;
then
A51: 0.V = Sum(f) - Sum(g) by A40,VECTSP_6:47;
Sum(g) = (- l.v) * v by A47,VECTSP_6:17;
then Sum(f) = (- l.v) * v by A51,VECTSP_1:19;
then (- l.v) * v in Lin(B) by Th7;
hence thesis by A38,A41,STRUCT_0:def 5,VECTSP_4:21;
end;
suppose
A52: not v in Carrier(l);
Carrier(l) c= B
proof
let x be object;
assume
A53: x in Carrier(l);
Carrier(l) c= B \/ {v} by VECTSP_6:def 4;
then x in B or x in {v} by A53,XBOOLE_0:def 3;
hence thesis by A52,A53,TARSKI:def 1;
end;
then l is Linear_Combination of B by VECTSP_6:def 4;
hence thesis by A37,A40;
end;
end;
hence thesis;
end;
v in {v} by TARSKI:def 1;
then
A54: v in B \/ {v} by XBOOLE_0:def 3;
A55: not v in B by A38,Th8,STRUCT_0:def 5;
B c= B \/ {v} by XBOOLE_1:7;
then A c= B \/ {v} by A36;
then B \/ {v} in Q by A1,A39;
hence contradiction by A34,A35,A54,A55,XBOOLE_1:7;
end;
theorem Th18:
Lin(A) = V implies ex B st B c= A & B is linearly-independent & Lin B = V
proof
assume
A1: Lin(A) = V;
defpred P[set] means ex B st B = $1 & B c= A & B is linearly-independent;
consider Q being set such that
A2: for Z holds Z in Q iff Z in bool(the carrier of V) & P[Z]
from XFAMILY:sch 1;
A3: now
let Z;
assume that
Z <> {} and
A4: Z c= Q and
A5: Z is c=-linear;
set W = union Z;
W c= the carrier of V
proof
let x be object;
assume x in W;
then consider X such that
A6: x in X and
A7: X in Z by TARSKI:def 4;
X in bool(the carrier of V) by A2,A4,A7;
hence thesis by A6;
end;
then reconsider W as Subset of V;
A8: W is linearly-independent
proof
deffunc F(object) = {C : $1 in C & C in Z};
let l be Linear_Combination of W;
assume that
A9: Sum(l) = 0.V and
A10: Carrier(l) <> {};
consider f being Function such that
A11: dom f = Carrier(l) and
A12: for x being object st x in Carrier(l) holds f.x = F(x)
from FUNCT_1:sch 3;
reconsider M = rng f as non empty set by A10,A11,RELAT_1:42;
set F = the Choice_Function of M;
set S = rng F;
A13: now
assume {} in M;
then consider x being object such that
A14: x in dom f and
A15: f.x = {} by FUNCT_1:def 3;
Carrier(l) c= W by VECTSP_6:def 4;
then consider X such that
A16: x in X and
A17: X in Z by A11,A14,TARSKI:def 4;
reconsider X as Subset of V by A2,A4,A17;
X in {C : x in C & C in Z} by A16,A17;
hence contradiction by A11,A12,A14,A15;
end;
then
A18: dom F = M by RLVECT_3:28;
then dom F is finite by A11,FINSET_1:8;
then
A19: S is finite by FINSET_1:8;
A20: now
let X;
assume X in S;
then consider x being object such that
A21: x in dom F and
A22: F.x = X by FUNCT_1:def 3;
consider y being object such that
A23: y in dom f & f.y = x by A18,A21,FUNCT_1:def 3;
A24: x = {C : y in C & C in Z} by A11,A12,A23;
reconsider x as set by TARSKI:1;
X in x by A13,A18,A21,A22,ORDERS_1:89;
then ex C st C = X & y in C & C in Z by A24;
hence X in Z;
end;
A25: now
let X,Y;
assume X in S & Y in S;
then X in Z & Y in Z by A20;
then X,Y are_c=-comparable by A5,ORDINAL1:def 8;
hence X c= Y or Y c= X;
end;
S <> {} by A18,RELAT_1:42;
then union S in S by A25,A19,CARD_2:62;
then union S in Z by A20;
then consider B such that
A26: B = union S and
B c= A and
A27: B is linearly-independent by A2,A4;
Carrier(l) c= union S
proof
let x be object;
set X = f.x;
assume
A28: x in Carrier(l);
then
A29: f.x = {C : x in C & C in Z} by A12;
A30: f.x in M by A11,A28,FUNCT_1:def 3;
then F.X in X by A13,ORDERS_1:89;
then
A31: ex C st F.X = C & x in C & C in Z by A29;
F.X in S by A18,A30,FUNCT_1:def 3;
hence thesis by A31,TARSKI:def 4;
end;
then l is Linear_Combination of B by A26,VECTSP_6:def 4;
hence thesis by A9,A10,A27;
end;
W c= A
proof
let x be object;
assume x in W;
then consider X such that
A32: x in X and
A33: X in Z by TARSKI:def 4;
ex B st B = X & B c= A & B is linearly-independent by A2,A4,A33;
hence thesis by A32;
end;
hence union Z in Q by A2,A8;
end;
{}(the carrier of V) c= A;
then Q <> {} by A2;
then consider X such that
A34: X in Q and
A35: for Z st Z in Q & Z <> X holds not X c= Z by A3,ORDERS_1:67;
consider B such that
A36: B = X and
A37: B c= A and
A38: B is linearly-independent by A2,A34;
take B;
thus B c= A & B is linearly-independent by A37,A38;
assume
A39: Lin(B) <> V;
now
assume
A40: for v st v in A holds v in Lin(B);
now
reconsider F = the carrier of Lin(B) as Subset of V by VECTSP_4:def 2;
let v;
assume v in Lin(A);
then consider l such that
A41: v = Sum(l) by Th7;
Carrier(l) c= the carrier of Lin(B)
proof
let x be object;
assume
A42: x in Carrier(l);
then reconsider a = x as Vector of V;
Carrier(l) c= A by VECTSP_6:def 4;
then a in Lin(B) by A40,A42;
hence thesis by STRUCT_0:def 5;
end;
then reconsider l as Linear_Combination of F by VECTSP_6:def 4;
Sum(l) = v by A41;
then v in Lin(F) by Th7;
hence v in Lin(B) by Th11;
end;
then Lin(A) is Subspace of Lin(B) by VECTSP_4:28;
hence contradiction by A1,A39,VECTSP_4:25;
end;
then consider v such that
A43: v in A and
A44: not v in Lin(B);
A45: B \/ {v} is linearly-independent
proof
let l be Linear_Combination of B \/ {v};
assume
A46: Sum(l) = 0.V;
now
per cases;
suppose
v in Carrier(l);
then l.v <> 0.GF by VECTSP_6:2;
then
A47: - l.v <> 0.GF by VECTSP_2:3;
deffunc G(Vector of V) = 0.GF;
deffunc F(Vector of V) = l.$1;
consider f such that
A48: f.v = 0.GF and
A49: for u st u <> v holds f.u = F(u) from FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V, the carrier of GF)
by FUNCT_2:8;
now
let u;
assume not u in Carrier(l) \ {v};
then not u in Carrier(l) or u in {v} by XBOOLE_0:def 5;
then l.u = 0.GF & u <> v or u = v by TARSKI:def 1;
hence f.u = 0.GF by A48,A49;
end;
then reconsider f as Linear_Combination of V by VECTSP_6:def 1;
Carrier(f) c= B
proof
let x be object;
A50: Carrier(l) c= B \/ {v} by VECTSP_6:def 4;
assume x in Carrier(f);
then consider u such that
A51: u = x and
A52: f.u <> 0.GF;
f.u = l.u by A48,A49,A52;
then u in Carrier(l) by A52;
then u in B or u in {v} by A50,XBOOLE_0:def 3;
hence thesis by A48,A51,A52,TARSKI:def 1;
end;
then reconsider f as Linear_Combination of B by VECTSP_6:def 4;
consider g such that
A53: g.v = - l.v and
A54: for u st u <> v holds g.u = G(u) from FUNCT_2:sch 6;
reconsider g as Element of Funcs(the carrier of V, the carrier of GF)
by FUNCT_2:8;
now
let u;
assume not u in {v};
then u <> v by TARSKI:def 1;
hence g.u = 0.GF by A54;
end;
then reconsider g as Linear_Combination of V by VECTSP_6:def 1;
Carrier(g) c= {v}
proof
let x be object;
assume x in Carrier(g);
then ex u st x = u & g.u <> 0.GF;
then x = v by A54;
hence thesis by TARSKI:def 1;
end;
then reconsider g as Linear_Combination of {v} by VECTSP_6:def 4;
A55: Sum(g) = (- l.v) * v by A53,VECTSP_6:17;
f - g = l
proof
let u;
now
per cases;
suppose
A56: v = u;
thus (f - g).u = f.u - g.u by VECTSP_6:40
.= 0.GF + (- (- l.v)) by A48,A53,A56,RLVECT_1:def 11
.= l.v + 0.GF by RLVECT_1:17
.= l.u by A56,RLVECT_1:4;
end;
suppose
A57: v <> u;
thus (f - g).u = f.u - g.u by VECTSP_6:40
.= l.u - g.u by A49,A57
.= l.u - 0.GF by A54,A57
.= l.u by RLVECT_1:13;
end;
end;
hence thesis;
end;
then 0.V = Sum(f) - Sum(g) by A46,VECTSP_6:47;
then Sum(f) = 0.V + Sum(g) by VECTSP_2:2
.= (- l.v) * v by A55,RLVECT_1:4;
then
A58: (- l.v) * v in Lin(B) by Th7;
(- l.v)" * ((- l.v) * v) = (- l.v)" * (- l.v) * v by VECTSP_1:def 16
.= 1_GF * v by A47,VECTSP_1:def 10
.= v;
hence thesis by A44,A58,VECTSP_4:21;
end;
suppose
A59: not v in Carrier(l);
Carrier(l) c= B
proof
let x be object;
assume
A60: x in Carrier(l);
Carrier(l) c= B \/ {v} by VECTSP_6:def 4;
then x in B or x in {v} by A60,XBOOLE_0:def 3;
hence thesis by A59,A60,TARSKI:def 1;
end;
then l is Linear_Combination of B by VECTSP_6:def 4;
hence thesis by A38,A46;
end;
end;
hence thesis;
end;
{v} c= A by A43,ZFMISC_1:31;
then B \/ {v} c= A by A37,XBOOLE_1:8;
then
A61: B \/ {v} in Q by A2,A45;
v in {v} by TARSKI:def 1;
then
A62: v in B \/ {v} by XBOOLE_0:def 3;
not v in B by A44,Th8;
hence contradiction by A35,A36,A62,A61,XBOOLE_1:7;
end;
Lem0A:
for GF be Abelian add-associative right_zeroed right_complementable
associative well-unital distributive non empty doubleLoopStr,
V be LeftMod of GF holds
{}(the carrier of V) is linearly-independent
proof
let GF be Abelian add-associative right_zeroed right_complementable
associative well-unital distributive non empty doubleLoopStr,
V be LeftMod of GF;
let l be Linear_Combination of {}(the carrier of V);
Carrier(l) c= {} by VECTSP_6:def 4;
hence thesis;
end;
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;
coherence by Lem0A;
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;
existence
proof
consider B being Subset of V such that
A1: {}(the carrier of V) c= B & B is base by Th17;
take B;
thus thesis by A1;
end;
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
ex B being Subset of IT st B is base;
end;
Lem1A:
for GF be almost_left_invertible
Abelian add-associative right_zeroed right_complementable
associative well-unital distributive non empty doubleLoopStr,
V being LeftMod of GF holds
(0).V is free
proof
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;
set W = (0).V;
reconsider B9 = {}(the carrier of V) as Subset of W by SUBSET_1:1;
reconsider V9 = V as Subspace of V by VECTSP_4:24;
A1: B9 = {}(the carrier of W); then
A2: B9 is linearly-independent;
(0).V9 = (0).W by VECTSP_4:37;
then Lin(B9) = W by A1,Th9;
then B9 is base by A2;
hence thesis;
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;
coherence by Lem1A;
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;
existence
proof
set V = the LeftMod of GF;
take (0).V;
thus thesis;
end;
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
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
proof
let V be LeftMod of GF, A be Subset of V;
assume A is linearly-independent;
then consider B being Subset of V such that
A1: A c= B and
A2: B is base by Th17;
reconsider B as Basis of V by A2;
take B;
thus thesis by A1;
end;
theorem
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
proof
let V be LeftMod of GF, A be Subset of V;
assume Lin(A) = V;
then consider B being Subset of V such that
A1: B c= A and
A2: B is linearly-independent & Lin(B) = V by Th18;
reconsider B as Basis of V by A2,Def3;
take B;
thus thesis by A1;
end;
:: Additional, copied from MOD_3
theorem
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) by TH2;
theorem
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) by TH3;
:: 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
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
proof
let R be non degenerated Ring,
V be LeftMod of R,
v1, v2 be Vector of V;
A1: v1 in {v1,v2} & v2 in {v1,v2} by TARSKI:def 2;
assume {v1,v2} is linearly-independent;
hence thesis by A1,Th2;
end;
theorem
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)
proof
let R be domRing, V be LeftMod of R, L be Linear_Combination of V, a be
Scalar of R;
set T = {u where u is Vector of V : (a * L).u <> 0.R};
set S = {v where v is Vector of V : L.v <> 0.R};
assume
A1: a <> 0.R;
T = S
proof
thus T c= S
proof
let x be object;
assume x in T;
then consider u be Vector of V such that
A2: x = u and
A3: (a * L).u <> 0.R;
(a * L).u = a * L.u by VECTSP_6:def 9;
then L.u <> 0.R by A3;
hence thesis by A2;
end;
let x be object;
assume x in S;
then consider v be Vector of V such that
A4: x = v and
A5: L.v <> 0.R;
(a * L).v = a * L.v by VECTSP_6:def 9;
then (a * L).v <> 0.R by A1,A5,VECTSP_2:def 1;
hence thesis by A4;
end;
hence thesis;
end;
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 Th12:
for W being strict Subspace of V st
R is non degenerated & A = the carrier of W holds Lin(A) = W
proof
let W be strict Subspace of V;
assume that
R is non degenerated and
A2: A = the carrier of W;
A1: 0.R <> 1.R;
now
let v be Vector of V;
thus v in Lin(A) implies v in W
proof
assume v in Lin(A); then
A3: ex l st v = Sum(l) by Th7;
A is linearly-closed by A2,VECTSP_4:33;
then v in the carrier of W by A1,A2,A3,VECTSP_6:14;
hence thesis by STRUCT_0:def 5;
end;
v in W iff v in the carrier of W by STRUCT_0:def 5;
hence v in W implies v in Lin(A) by A2,Th8;
end;
hence thesis by VECTSP_4:30;
end;
theorem
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
proof
let V be strict LeftMod of R, A be Subset of V such that
R is non degenerated;
assume
A2: A = the carrier of V;
(Omega).V = V;
hence thesis by A2,Th12;
end;
theorem
for V being strict LeftMod of R, A,B being Subset of V st Lin(A) = V &
A c= B holds Lin(B) = V
proof
let V be strict LeftMod of R, A,B be Subset of V;
assume Lin(A) = V & A c= B;
then V is Subspace of Lin(B) by Th13;
hence thesis by VECTSP_4:25;
end;
theorem
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
proof
let R be Ring,
V be LeftMod of R,
v1,v2 be Vector of V;
A1: v1 in {v1,v2} & v2 in {v1,v2} by TARSKI:def 2;
assume R is non degenerated & {v1,v2} is linearly-independent;
hence thesis by A1,Th2;
end;