let V be RealUnitarySpace; :: thesis: 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; :: thesis: ( 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
; :: thesis: 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 XBOOLE_0:sch 1();
( {} the carrier of V in bool the carrier of V & {} the carrier of V c= A & {} the carrier of V is linearly-independent )
by RLVECT_3:8, XBOOLE_1:2;
then A3:
Q <> {}
by A2;
now let Z be
set ;
:: thesis: ( 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
;
:: thesis: 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 c= A
W is
linearly-independent
proof
let l be
Linear_Combination of
W;
:: according to RLVECT_3:def 1 :: thesis: ( not Sum l = 0. V or Carrier l = {} )
assume that A11:
Sum l = 0. V
and A12:
Carrier l <> {}
;
:: thesis: contradiction
deffunc H1(
set )
-> set =
{ C where C is Subset of V : ( $1 in C & C in Z ) } ;
consider f being
Function such that A13:
dom f = Carrier l
and A14:
for
x being
set st
x in Carrier l holds
f . x = H1(
x)
from FUNCT_1:sch 3();
reconsider M =
rng f as non
empty set by A12, A13, RELAT_1:65;
consider F being
Choice_Function of
M;
set S =
rng F;
A20:
(
dom F = M &
M <> {} )
by A15, RLVECT_3:35;
then A21:
rng F <> {}
by RELAT_1:65;
dom F is
finite
by A13, A20, FINSET_1:26;
then
rng F is
finite
by FINSET_1:26;
then
union (rng F) in rng F
by A21, A28, CARD_2:81;
then
union (rng F) in Z
by A22;
then consider B being
Subset of
V such that A29:
B = union (rng F)
and
B c= A
and A30:
B is
linearly-independent
by A2, A4;
Carrier l c= union (rng F)
then
l is
Linear_Combination of
B
by A29, RLVECT_2:def 8;
hence
contradiction
by A11, A12, A30, RLVECT_3:def 1;
:: thesis: verum
end; hence
union Z in Q
by A2, A8;
:: thesis: verum end;
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 A3, ORDERS_1:177;
consider B being Subset of V such that
A37:
B = X
and
A38:
B c= A
and
A39:
B is linearly-independent
by A2, A35;
take
B
; :: thesis: ( B c= A & B is linearly-independent & Lin B = V )
thus
( B c= A & B is linearly-independent )
by A38, A39; :: thesis: Lin B = V
assume A40:
Lin B <> V
; :: thesis: contradiction
then consider v being VECTOR of V such that
A45:
v in A
and
A46:
not v in Lin B
;
A47:
B \/ {v} is linearly-independent
proof
let l be
Linear_Combination of
B \/ {v};
:: according to RLVECT_3:def 1 :: thesis: ( not Sum l = 0. V or Carrier l = {} )
assume A48:
Sum l = 0. V
;
:: thesis: Carrier l = {}
now per cases
( v in Carrier l or not v in Carrier l )
;
suppose A49:
v in Carrier l
;
:: thesis: Carrier l = {} deffunc H1(
VECTOR of
V)
-> Element of
REAL =
l . $1;
consider f being
Function of the
carrier of
V,
REAL such that A50:
f . v = 0
and A51:
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,
REAL by FUNCT_2:11;
then reconsider f =
f as
Linear_Combination of
V by RLVECT_2:def 5;
Carrier f c= B
then reconsider f =
f as
Linear_Combination of
B by RLVECT_2:def 8;
deffunc H2(
set )
-> Element of
NAT =
0 ;
consider g being
Function of the
carrier of
V,
REAL such that A54:
g . v = - (l . v)
and A55:
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,
REAL by FUNCT_2:11;
then reconsider g =
g as
Linear_Combination of
V by RLVECT_2:def 5;
Carrier g c= {v}
then reconsider g =
g as
Linear_Combination of
{v} by RLVECT_2:def 8;
A56:
f - g = l
A59:
Sum g = (- (l . v)) * v
by A54, RLVECT_2:50;
0. V = (Sum f) - (Sum g)
by A48, A56, RLVECT_3:4;
then Sum f =
(0. V) + (Sum g)
by RLSUB_2:78
.=
(- (l . v)) * v
by A59, RLVECT_1:10
;
then A60:
(- (l . v)) * v in Lin B
by Th1;
A61:
- (l . v) <> 0
by A49, RLVECT_2:28;
((- (l . v)) " ) * ((- (l . v)) * v) =
(((- (l . v)) " ) * (- (l . v))) * v
by RLVECT_1:def 9
.=
1
* v
by A61, XCMPLX_0:def 7
.=
v
by RLVECT_1:def 9
;
hence
Carrier l = {}
by A46, A60, RUSUB_1:15;
:: thesis: verum end;
hence
Carrier l = {}
;
:: thesis: verum
end;
v in {v}
by TARSKI:def 1;
then A64:
( v in B \/ {v} & not v in B )
by A46, Th2, XBOOLE_0:def 3;
{v} c= A
by A45, ZFMISC_1:37;
then
B \/ {v} c= A
by A38, XBOOLE_1:8;
then
B \/ {v} in Q
by A2, A47;
hence
contradiction
by A36, A37, A64, XBOOLE_1:7; :: thesis: verum