let R be non degenerated almost_left_invertible 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 )
let V be 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 )
let A be Subset of V; ( Lin A = V implies ex B being Subset of V st
( B c= A & B is base ) )
defpred S1[ set ] means ex B being Subset of V st
( B = $1 & B c= A & B is linearly-independent );
assume A2:
Lin A = V
; ex B being Subset of V st
( B c= A & B is base )
consider Q being set such that
A3:
for Z being set holds
( Z in Q iff ( Z in bool the carrier of V & S1[Z] ) )
from XFAMILY:sch 1();
A4:
now for Z being set st Z <> {} & Z c= Q & Z is c=-linear holds
union Z in Qlet Z be
set ;
( Z <> {} & Z c= Q & Z is c=-linear implies union Z in Q )assume that
Z <> {}
and A5:
Z c= Q
and A6:
Z is
c=-linear
;
union Z in Qset W =
union Z;
union Z c= the
carrier of
V
then reconsider W =
union Z as
Subset of
V ;
A9:
W is
linearly-independent
proof
deffunc H1(
object )
-> set =
{ C where C is Subset of V : ( $1 in C & C in Z ) } ;
let l be
Linear_Combination of
W;
VECTSP_7:def 1 ( not Sum l = 0. V or Carrier l = {} )
assume that A10:
Sum l = 0. V
and A11:
Carrier l <> {}
;
contradiction
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 = H1(
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 the
Choice_Function of
M;
then A19:
dom the
Choice_Function of
M = M
by RLVECT_3:28;
then
dom the
Choice_Function of
M is
finite
by A12, FINSET_1:8;
then A20:
rng the
Choice_Function of
M is
finite
by FINSET_1:8;
rng the
Choice_Function of
M <> {}
by A19, RELAT_1:42;
then
union (rng the Choice_Function of M) in rng the
Choice_Function of
M
by A26, A20, CARD_2:62;
then
union (rng the Choice_Function of M) in Z
by A21;
then consider B being
Subset of
V such that A27:
B = union (rng the Choice_Function of M)
and
B c= A
and A28:
B is
linearly-independent
by A3, A5;
Carrier l c= union (rng the Choice_Function of M)
then
l is
Linear_Combination of
B
by A27, VECTSP_6:def 4;
hence
contradiction
by A10, A11, A28;
verum
end;
W c= A
hence
union Z in Q
by A3, A9;
verum end;
( {} the carrier of V c= A & {} the carrier of V is linearly-independent )
;
then
Q <> {}
by A3;
then consider X being set such that
A35:
X in Q
and
A36:
for Z being set 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
; ( B c= A & B is base )
thus
( B c= A & B is linearly-independent )
by A38, A39; VECTSP_7:def 3 Lin B = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
assume A40:
Lin B <> ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
; contradiction
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
{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; verum