let V be RealUnitarySpace; 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 )
let A be Subset of V; ( Lin A = V implies ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V ) )
assume A1:
Lin A = V
; ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V )
defpred S1[ set ] means ex B being Subset of V st
( B = $1 & B c= A & B is linearly-independent );
consider Q being set such that
A2:
for Z being set holds
( Z in Q iff ( Z in bool the carrier of V & S1[Z] ) )
from XFAMILY:sch 1();
A3:
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 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;
RLVECT_3:def 1 ( not Sum l = 0. V or 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
B c= A
and A27:
B is
linearly-independent
by A2, A4;
Carrier l c= union (rng the Choice_Function of M)
then
l is
Linear_Combination of
B
by A26, RLVECT_2:def 6;
hence
contradiction
by A9, A10, A27;
verum
end;
W c= A
hence
union Z in Q
by A2, A8;
verum end;
( {} the carrier of V c= A & {} the carrier of V is linearly-independent )
by RLVECT_3:7;
then
Q <> {}
by A2;
then consider X being set such that
A34:
X in Q
and
A35:
for Z being set st Z in Q & Z <> X holds
not X c= Z
by A3, ORDERS_1:67;
consider B being Subset of V such that
A36:
B = X
and
A37:
B c= A
and
A38:
B is linearly-independent
by A2, A34;
take
B
; ( B c= A & B is linearly-independent & Lin B = V )
thus
( B c= A & B is linearly-independent )
by A37, A38; Lin B = V
assume A39:
Lin B <> V
; contradiction
then consider v being VECTOR of 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};
RLVECT_3:def 1 ( not Sum l = 0. V or Carrier l = {} )
assume A46:
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 A47:
- (l . v) <> 0
by RLVECT_2:19;
deffunc H1(
set )
-> Element of
REAL =
In (
0,
REAL);
deffunc H2(
VECTOR of
V)
-> Element of
REAL =
l . $1;
consider f being
Function of the
carrier of
V,
REAL such that A48:
f . v = In (
0,
REAL)
and A49:
for
u being
VECTOR of
V st
u <> v holds
f . u = H2(
u)
from FUNCT_2:sch 6();
reconsider f =
f as
Element of
Funcs ( the
carrier of
V,
REAL)
by FUNCT_2:8;
then reconsider f =
f as
Linear_Combination of
V by RLVECT_2:def 3;
Carrier f c= B
then reconsider f =
f as
Linear_Combination of
B by RLVECT_2:def 6;
consider g being
Function of the
carrier of
V,
REAL such that A53:
g . v = - (l . v)
and A54:
for
u being
VECTOR of
V st
u <> v holds
g . u = H1(
u)
from FUNCT_2:sch 6();
reconsider g =
g as
Element of
Funcs ( the
carrier of
V,
REAL)
by FUNCT_2:8;
then reconsider g =
g as
Linear_Combination of
V by RLVECT_2:def 3;
Carrier g c= {v}
then reconsider g =
g as
Linear_Combination of
{v} by RLVECT_2:def 6;
A55:
Sum g = (- (l . v)) * v
by A53, RLVECT_2:32;
f - g = l
then
0. V = (Sum f) - (Sum g)
by A46, RLVECT_3:4;
then Sum f =
(0. V) + (Sum g)
by RLSUB_2:61
.=
(- (l . v)) * v
by A55, RLVECT_1:4
;
then A58:
(- (l . v)) * v in Lin B
by Th1;
((- (l . v)) ") * ((- (l . v)) * v) =
(((- (l . v)) ") * (- (l . v))) * v
by RLVECT_1:def 7
.=
1
* v
by A47, XCMPLX_0:def 7
.=
v
by RLVECT_1:def 8
;
hence
Carrier l = {}
by A44, A58, RUSUB_1:15;
verum end;
hence
Carrier l = {}
;
verum
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, Th2;
hence
contradiction
by A35, A36, A62, A61, XBOOLE_1:7; verum