:: Free Modules
:: by Michal Muzalewski
::
:: Received October 18, 1991
:: Copyright (c) 1991-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 FUNCSDOM, VECTSP_1, ARYTM_1, SUPINF_2, STRUCT_0, RLVECT_1,
ALGSTR_0, XBOOLE_0, MESFUNC1, VECTSP_2, RLVECT_2, FINSEQ_1, FINSET_1,
SUBSET_1, TARSKI, FUNCT_1, RELAT_1, CARD_3, VALUED_1, ARYTM_3, RLVECT_3,
RLSUB_1, FUNCT_2, PRELAMB, ZFMISC_1, ORDINAL1, ORDERS_1, MOD_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FINSET_1, FINSEQ_1,
RELAT_1, FUNCT_1, ORDERS_1, DOMAIN_1, STRUCT_0, ALGSTR_0, PARTFUN1,
FUNCT_2, GROUP_1, RLVECT_1, VECTSP_1, VECTSP_2, VECTSP_4, VECTSP_5,
VECTSP_6, VECTSP_7;
constructors ORDERS_1, PARTFUN1, REALSET1, VECTSP_5, VECTSP_6, RELSET_1,
VECTSP_7, GROUP_1;
registrations SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, VECTSP_1, VECTSP_4,
VECTSP_7;
requirements SUBSET, BOOLE;
definitions TARSKI, VECTSP_6, VECTSP_7;
equalities XBOOLE_0, VECTSP_4, VECTSP_6;
expansions XBOOLE_0, TARSKI, VECTSP_7;
theorems FINSET_1, FUNCT_1, ORDERS_1, RLVECT_3, SUBSET_1, TARSKI, VECTSP_1,
VECTSP_2, ZFMISC_1, RLVECT_1, VECTSP_4, VECTSP_6, FUNCT_2, RELAT_1,
ORDINAL1, XBOOLE_0, XBOOLE_1, RLSUB_2, CARD_2, STRUCT_0, VECTSP_7;
schemes FUNCT_1, FUNCT_2, XFAMILY;
begin
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;
theorem Th1:
for R being non degenerated add-associative right_zeroed
right_complementable non empty doubleLoopStr holds 0.R <> -1.R
proof
let R be non degenerated add-associative right_zeroed right_complementable
non empty doubleLoopStr;
assume 0.R = -1.R;
then 0.R = -(-1.R) by RLVECT_1:12
.= 1.R by RLVECT_1:17;
hence contradiction;
end;
reserve x,y for object,
R for Ring,
V for LeftMod of R,
L for Linear_Combination of V,
a for Scalar of R,
v,u for Vector of V,
F,G for FinSequence of the carrier of V,
C for finite Subset of V;
reserve X,Y,Z for set,
A,B for Subset of V,
T for finite Subset of V,
l for Linear_Combination of A,
f,g for Function of the carrier of V,the carrier of R;
theorem
Carrier(L) c= C implies ex F st F is one-to-one & rng F = C & Sum
(L) = Sum(L (#) F) by VECTSP_7:21;
theorem
Sum(a * L) = a * Sum(L) by VECTSP_7:22;
theorem Th4:
x in Lin(A) iff ex l st x = Sum(l) by VECTSP_7:7;
theorem Th5:
x in A implies x in Lin(A) by VECTSP_7:8;
theorem Th6:
Lin({}(the carrier of V)) = (0).V by VECTSP_7:9;
theorem
Lin(A) = (0).V implies A = {} or A = {0.V} by VECTSP_7:10;
theorem Th8:
for R being non degenerated Ring,
V being LeftMod of R,
A being Subset of V
for W being strict Subspace of V st A = the carrier of W
holds Lin(A) = W
proof
let R be non degenerated Ring,
V be LeftMod of R,
A be Subset of V;
let W be strict Subspace of V;
assume that
A2: A = the carrier of W;
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 being Linear_Combination of A st v = Sum(l) by Th4;
A1: 0.R <> 1.R;
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,Th5;
end;
hence thesis by VECTSP_4:30;
end;
theorem
for R being non degenerated Ring
for V being strict LeftMod of R
for A being Subset of V st A = the carrier of V holds
Lin(A) = V
proof
let R be non degenerated Ring;
let V be strict LeftMod of R;
let A be Subset of V;
assume A = the carrier of V; then
A = the carrier of (Omega).V;
hence thesis by Th8;
end;
theorem Th10:
A c= B implies Lin(A) is Subspace of Lin(B) by VECTSP_7:13;
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,Th10;
hence thesis by A1,VECTSP_4:25;
end;
theorem
Lin(A \/ B) = Lin(A) + Lin(B) by VECTSP_7:15;
theorem
Lin(A /\ B) is Subspace of Lin(A) /\ Lin(B) by VECTSP_7:16;
theorem Th14:
(0).V is free
proof
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,Th6;
then B9 is base by A2;
hence thesis;
end;
registration
let R;
cluster strict free for LeftMod of R;
existence
proof
set V = the LeftMod of R;
take (0).V;
thus thesis by Th14;
end;
end;
reserve R for Skew-Field;
reserve a,b for Scalar of R;
reserve V for LeftMod of R;
reserve v,v1,v2,u for Vector of V;
reserve f for Function of the carrier of V, the carrier of R;
Lm2: a <> 0.R implies a"*(a*v) = 1.R*v & (a"*a)*v = 1.R*v
proof
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
{v} is linearly-independent iff v <> 0.V
proof
thus {v} is linearly-independent implies v <> 0.V
proof
assume {v} is linearly-independent;
then not 0.V in {v} by VECTSP_7:2;
hence thesis by TARSKI:def 1;
end;
assume
A2: v <> 0.V;
let l be Linear_Combination of {v};
A3: Carrier(l) c= {v} by VECTSP_6:def 4;
assume
A4: Sum(l) = 0.V;
now
per cases by A3,ZFMISC_1:33;
suppose
Carrier(l) = {};
hence thesis;
end;
suppose
A5: Carrier(l) = {v};
A6: 0.V = l.v * v by A4,VECTSP_6:17;
not v in Carrier(l) by A2,A6,VECTSP_2:30,VECTSP_6:2;
hence thesis by A5,TARSKI:def 1;
end;
end;
hence thesis;
end;
theorem Th16:
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(Element of V) = 0.R;
assume that
A2: v1 <> v2 and
A3: {v1,v2} is linearly-independent;
thus v2 <> 0.V by A3,VECTSP_7:28;
let a;
consider f such that
A4: f.v1 = - 1.R & f.v2 = a and
A5: for v being Element of V st v <> v1 & v <> v2 holds f.v = F(v)
from FUNCT_2:sch 7(A2);
reconsider f as Element of Funcs(the carrier of V, the carrier of R) 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.R by A5;
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
A6: ex u st x = u & f.u <> 0.R;
assume not x in {v1,v2};
then x <> v1 & x <> v2 by TARSKI:def 2;
hence thesis by A5,A6;
end;
then reconsider f as Linear_Combination of {v1,v2} by VECTSP_6:def 4;
A7: now
assume not v1 in Carrier(f);
then 0.R = - 1.R by A4;
hence contradiction by Th1;
end;
set w = a * v2;
assume v1 = a * v2;
then Sum(f) = (- 1.R) * w + w by A2,A4,VECTSP_6:18
.= (- w) + w by VECTSP_1:14
.= 0.V by RLVECT_1:5;
hence thesis by A3,A7;
end;
assume
A8: v2 <> 0.V;
assume
A9: for a holds v1 <> a * v2;
A10: 1.R * v2 = v2;
hence v1 <> v2 by A9;
let l be Linear_Combination of {v1,v2};
assume that
A11: Sum(l) = 0.V and
A12: Carrier(l) <> {};
A13: 0.V = l.v1 * v1 + l.v2 * v2 by A9,A10,A11,VECTSP_6:18;
set x = the Element of Carrier(l);
Carrier(l) c= {v1,v2} by VECTSP_6:def 4; then
A14: x in {v1,v2} by A12;
x in Carrier(l) by A12; then
A15: ex u st x = u & l.u <> 0.R;
now
per cases by A15,A14,TARSKI:def 2;
suppose
A16: l.v1 <> 0.R;
0.V = (l.v1)" * (l.v1 * v1 + l.v2 * v2) by A13,VECTSP_2:30
.= (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.R * v1 + (l.v1)" * l.v2 * v2 by A16,Lm2
.= v1 + (l.v1)" * l.v2 * v2;
then v1 = - ((l.v1)" * l.v2 * v2) by VECTSP_1:16
.= (- 1.R) * ((l.v1)" * l.v2 * v2) by VECTSP_1:14
.= ((- 1.R) * ((l.v1)" * l.v2)) * v2 by VECTSP_1:def 16;
hence thesis by A9;
end;
suppose
A17: l.v2 <> 0.R & l.v1 = 0.R;
0.V = (l.v2)" * (l.v1 * v1 + l.v2 * v2) by A13,VECTSP_2:30
.= (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 + 1.R * v2 by A17,Lm2
.= (l.v2)" * l.v1 * v1 + v2
.= 0.R * v1 + v2 by A17
.= 0.V + v2 by VECTSP_2:30
.= v2 by RLVECT_1:def 4;
hence thesis by A8;
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.R & b = 0.R
proof
thus v1 <> v2 & {v1,v2} is linearly-independent implies for a,b st a * v1 +
b * v2 = 0.V holds a = 0.R & b = 0.R
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.R or b <> 0.R;
now
per cases by A3;
suppose
A4: a <> 0.R;
0.V = a" * (a * v1 + b * v2) by A2,VECTSP_2:30
.= 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.R * v1 + (a" * b) * v2 by A4,Lm2
.= v1 + (a" * b) * v2;
then v1 = - ((a" * b) * v2) by VECTSP_1:16
.= (- 1.R) * ((a" * b) * v2) by VECTSP_1:14
.= (- 1.R) * (a" * b) * v2 by VECTSP_1:def 16;
hence thesis by A1,Th16;
end;
suppose
A5: b <> 0.R;
0.V = b" * (a * v1 + b * v2) by A2,VECTSP_2:30
.= 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 + 1.R* v2 by A5,Lm2
.= (b" * a) * v1 + v2;
then v2 = - ((b" * a) * v1) by VECTSP_1:16
.= (- 1.R) * ((b" * a) * v1) by VECTSP_1:14
.= (- 1.R) * (b" * a) * v1 by VECTSP_1:def 16;
hence thesis by A1,Th16;
end;
end;
hence thesis;
end;
assume
A6: for a,b st a * v1 + b * v2 = 0.V holds a = 0.R & b = 0.R;
A7: now
let a;
assume v1 = a * v2;
then v1 = 0.V + a * v2 by RLVECT_1:def 4;
then 0.V = v1 - a * v2 by RLSUB_2:61
.= v1 + ((- a) * v2) by VECTSP_1:21
.= 1.R * v1 + (- a) * v2;
hence contradiction by A6;
end;
now
assume
A8: v2 = 0.V;
0.V = 0.V + 0.V by RLVECT_1:def 4
.= 0.R * v1 + 0.V by VECTSP_2:30
.= 0.R * v1 + 1.R * v2 by A8;
hence contradiction by A6;
end;
hence thesis by A7,Th16;
end;
theorem Th18:
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 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 Th4;
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,Th5,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 Th19:
for R being almost_left_invertible non degenerated Ring
for V being LeftMod of R for A being Subset of V st
Lin(A) = V holds ex B being Subset of V st B c= A & B is base
proof
let R be almost_left_invertible non degenerated 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 & B c= A & B is
linearly-independent);
assume
A2: Lin(A) = V;
consider Q being set such that
A3: for Z holds Z in Q iff Z in bool(the carrier of V) & P[Z] from
XFAMILY:sch 1;
A4: now
let Z;
assume that
Z <> {} and
A5: Z c= Q and
A6: 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
A7: x in X and
A8: X in Z by TARSKI:def 4;
X in bool(the carrier of V) by A3,A5,A8;
hence thesis by A7;
end;
then reconsider W as Subset of V;
A9: 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
A10: Sum(l) = 0.V and
A11: Carrier(l) <> {};
consider f being Function such that
A12: dom f = Carrier(l) and
A13: 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 A11,A12,RELAT_1:42;
set F = the Choice_Function of M;
set S = rng F;
A14: now
assume {} in M;
then consider x being object such that
A15: x in dom f and
A16: f.x = {} by FUNCT_1:def 3;
Carrier(l) c= W by VECTSP_6:def 4;
then consider X such that
A17: x in X and
A18: X in Z by A12,A15,TARSKI:def 4;
reconsider X as Subset of V by A3,A5,A18;
X in {C where C is Subset of V : x in C & C in Z} by A17,A18;
hence contradiction by A12,A13,A15,A16;
end;
then
A19: dom F = M by RLVECT_3:28;
then dom F is finite by A12,FINSET_1:8;
then
A20: S is finite by FINSET_1:8;
A21: now
let X;
assume X in S;
then consider x being object such that
A22: x in dom F and
A23: F.x = X by FUNCT_1:def 3;
consider y being object such that
A24: y in dom f & f.y = x by A19,A22,FUNCT_1:def 3;
A25: x = {C where C is Subset of V : y in C & C in Z} by A12,A13,A24;
reconsider x as set by TARSKI:1;
X in x by A14,A19,A22,A23,ORDERS_1:89;
then ex C being Subset of V st C = X & y in C & C in Z by A25;
hence X in Z;
end;
A26: now
let X,Y;
assume X in S & Y in S;
then X in Z & Y in Z by A21;
then X,Y are_c=-comparable by A6,ORDINAL1:def 8;
hence X c= Y or Y c= X;
end;
S <> {} by A19,RELAT_1:42;
then union S in S by A26,A20,CARD_2:62;
then union S in Z by A21;
then consider B being Subset of V such that
A27: B = union S and
B c= A and
A28: B is linearly-independent by A3,A5;
Carrier(l) c= union S
proof
let x be object;
set X = f.x;
assume
A29: x in Carrier(l);
then
A30: f.x = {C where C is Subset of V : x in C & C in Z} by A13;
A31: f.x in M by A12,A29,FUNCT_1:def 3;
then F.X in X by A14,ORDERS_1:89;
then
A32: ex C being Subset of V st F.X = C & x in C & C in Z by A30;
F.X in S by A19,A31,FUNCT_1:def 3;
hence thesis by A32,TARSKI:def 4;
end;
then l is Linear_Combination of B by A27,VECTSP_6:def 4;
hence thesis by A10,A11,A28;
end;
W c= A
proof
let x be object;
assume x in W;
then consider X such that
A33: x in X and
A34: X in Z by TARSKI:def 4;
ex B being Subset of V st B = X & B c= A & B is
linearly-independent by A3,A5,A34;
hence thesis by A33;
end;
hence union Z in Q by A3,A9;
end;
{}(the carrier of V) c= A & {}(the carrier of V) is linearly-independent;
then Q <> {} by A3;
then consider X such that
A35: X in Q and
A36: for Z st Z in Q & Z <> X holds not X c= Z by A4,ORDERS_1:67;
consider B being Subset of V such that
A37: B = X and
A38: B c= A and
A39: B is linearly-independent by A3,A35;
take B;
thus B c= A & B is linearly-independent by A38,A39;
assume
A40: Lin(B) <> the ModuleStr of V;
now
assume
A41: for v being Vector of 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 be Vector of V;
assume v in Lin(A);
then consider l being Linear_Combination of A such that
A42: v = Sum(l) by Th4;
Carrier(l) c= the carrier of Lin(B)
proof
let x be object;
assume
A43: 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 A41,A43;
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 A42;
then v in Lin(F) by Th4;
hence v in Lin(B) by Th8;
end;
then Lin(A) is Subspace of Lin(B) by VECTSP_4:28;
hence contradiction by A2,A40,VECTSP_4:25;
end;
then consider v being Vector of V such that
A44: v in A and
A45: not v in Lin(B);
A46: B \/ {v} is linearly-independent
proof
let l be Linear_Combination of B \/ {v};
assume
A47: 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
A48: (- 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
A49: f.v = 0.R and
A50: 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 A49,A50;
end;
then reconsider f as Linear_Combination of V by VECTSP_6:def 1;
Carrier(f) c= B
proof
let x be object;
A51: Carrier(l) c= B \/ {v} by VECTSP_6:def 4;
assume x in Carrier(f);
then consider u being Vector of V such that
A52: u = x and
A53: f.u <> 0.R;
f.u = l.u by A49,A50,A53;
then u in Carrier(l) by A53;
then u in B or u in {v} by A51,XBOOLE_0:def 3;
hence thesis by A49,A52,A53,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
A54: g.v = - l.v and
A55: 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 A55;
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 A55;
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
A56: v = u;
thus (f - g).u = f.u - g.u by VECTSP_6:40
.= 0.R + (- (- l.v)) by A49,A54,A56,RLVECT_1:def 11
.= l.v + 0.R 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 A50,A57
.= l.u - 0.R by A55,A57
.= l.u by RLVECT_1:13;
end;
end;
hence thesis;
end;
then
A58: 0.V = Sum(f) - Sum(g) by A47,VECTSP_6:47;
Sum(g) = (- l.v) * v by A54,VECTSP_6:17;
then Sum(f) = (- l.v) * v by A58,VECTSP_1:19;
then (- l.v) * v in Lin(B) by Th4;
hence thesis by A45,A48,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 A39,A47;
end;
end;
hence thesis;
end;
{v} c= A by A44,ZFMISC_1:31;
then B \/ {v} c= A by A38,XBOOLE_1:8;
then
A61: B \/ {v} in Q by A3,A46;
v in {v} by TARSKI:def 1;
then
A62: v in B \/ {v} by XBOOLE_0:def 3;
not v in B by A45,Th5;
hence contradiction by A36,A37,A62,A61,XBOOLE_1:7;
end;
Lm3: for R being non degenerated almost_left_invertible Ring
for V being LeftMod of R ex B being Subset of V st B is base
proof
let R be non degenerated almost_left_invertible Ring;
let V be LeftMod of R;
ex B being Subset of V st {}(the carrier of V) c= B & B is base by
VECTSP_7:17;
hence thesis;
end;
registration
let R be non degenerated almost_left_invertible Ring;
let V be LeftMod of R;
cluster base for Subset of V;
existence
proof
ex B being Subset of V st {}(the carrier of V) c= B & B is base by
VECTSP_7:17;
hence thesis;
end;
end;
theorem
for V being LeftMod of R holds V is free by Lm3;
registration let R;
cluster -> free for LeftMod of R;
coherence by Lm3;
end;
theorem
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 I being Basis of V st A c= I
proof
let R be non degenerated almost_left_invertible Ring;
let V be LeftMod of R;
let 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 Th18;
reconsider B as Basis of V by A2;
take B;
thus thesis by A1;
end;
theorem
for V being LeftMod of R for 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 R;
let 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 base by Th19;
reconsider B as Basis of V by A2;
take B;
thus thesis by A1;
end;