let R be 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 )
let V be 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 )
let A be Subset of V; ( A is linearly-independent implies ex B being Subset of V st
( A c= B & B is base ) )
defpred S1[ 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 being set holds
( Z in Q iff ( Z in bool the carrier of V & S1[Z] ) )
from XFAMILY:sch 1();
A2:
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 A3:
Z <> {}
and A4:
Z c= Q
and A5:
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 ;
A8:
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 ( Sum l = 0. V implies Carrier l = {} )
assume that A9:
Sum l = 0. V
and A10:
Carrier l <> {}
;
contradiction
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 = H1(
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 the
Choice_Function of
M;
then A18:
dom the
Choice_Function of
M = M
by RLVECT_3:28;
then
dom the
Choice_Function of
M is
finite
by A11, FINSET_1:8;
then A19:
rng the
Choice_Function of
M is
finite
by FINSET_1:8;
rng the
Choice_Function of
M <> {}
by A18, RELAT_1:42;
then
union (rng the Choice_Function of M) in rng the
Choice_Function of
M
by A25, A19, CARD_2:62;
then
union (rng the Choice_Function of M) in Z
by A20;
then consider B being
Subset of
V such that A26:
B = union (rng the Choice_Function of M)
and
A c= B
and A27:
B is
linearly-independent
by A1, A4;
Carrier l c= union (rng the Choice_Function of M)
then
l is
Linear_Combination of
B
by A26, VECTSP_6:def 4;
hence
contradiction
by A9, A10, A27;
verum
end; set x = the
Element of
Z;
the
Element of
Z in Q
by A3, A4;
then A32:
ex
B being
Subset of
V st
(
B = the
Element of
Z &
A c= B &
B is
linearly-independent )
by A1;
the
Element of
Z c= W
by A3, ZFMISC_1:74;
then
A c= W
by A32;
hence
union Z in Q
by A1, A8;
verum end;
assume
A is linearly-independent
; ex B being Subset of V st
( A c= B & B is base )
then
Q <> {}
by A1;
then consider X being set such that
A33:
X in Q
and
A34:
for Z being set 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
; ( A c= B & B is base )
thus
( A c= B & B is linearly-independent )
by A36, A37; VECTSP_7:def 3 Lin B = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
assume
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
A38:
( ( v in Lin B & not v in (Omega). V ) or ( v in (Omega). V & not v in Lin B ) )
by VECTSP_4:30;
A39:
B \/ {v} is linearly-independent
proof
let l be
Linear_Combination of
B \/ {v};
VECTSP_7:def 1 ( Sum l = 0. V implies Carrier l = {} )
assume A40:
Sum l = 0. V
;
Carrier l = {}
now Carrier l = {} per cases
( v in Carrier l or not v in Carrier l )
;
suppose
v in Carrier l
;
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 H1(
Vector of
V)
-> Element of the
carrier of
R =
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 = H1(
u)
from FUNCT_2:sch 6();
reconsider f =
f as
Element of
Funcs ( the
carrier of
V, the
carrier of
R)
by FUNCT_2:8;
then reconsider f =
f as
Linear_Combination of
V by VECTSP_6:def 1;
Carrier f c= B
then reconsider f =
f as
Linear_Combination of
B by VECTSP_6:def 4;
deffunc H2(
Vector of
V)
-> Element of the
carrier of
R =
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 = H2(
u)
from FUNCT_2:sch 6();
reconsider g =
g as
Element of
Funcs ( the
carrier of
V, the
carrier of
R)
by FUNCT_2:8;
then reconsider g =
g as
Linear_Combination of
V by VECTSP_6:def 1;
Carrier g c= {v}
then reconsider g =
g as
Linear_Combination of
{v} by VECTSP_6:def 4;
f - g = l
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
Carrier l = {}
by A38, A41, STRUCT_0:def 5, VECTSP_4:21;
verum end;
hence
Carrier l = {}
;
verum
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; verum