let V be RealLinearSpace; :: thesis: for A being Subset of V st A is linearly-independent holds
ex B being Subset of V st
( A c= B & B is linearly-independent & Lin B = RLSStruct(# the carrier of V,the U2 of V,the U5 of V,the Mult of V #) )
let A be Subset of V; :: thesis: ( A is linearly-independent implies ex B being Subset of V st
( A c= B & B is linearly-independent & Lin B = RLSStruct(# the carrier of V,the U2 of V,the U5 of V,the Mult of V #) ) )
assume A1:
A is linearly-independent
; :: thesis: ex B being Subset of V st
( A c= B & B is linearly-independent & Lin B = RLSStruct(# the carrier of V,the U2 of V,the U5 of V,the Mult of V #) )
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
A2:
for Z being set holds
( Z in Q iff ( Z in bool the carrier of V & S1[Z] ) )
from XBOOLE_0:sch 1();
A3:
Q <> {}
by A1, A2;
now let Z be
set ;
:: thesis: ( Z <> {} & Z c= Q & Z is c=-linear implies union Z in Q )assume that A4:
Z <> {}
and A5:
Z c= Q
and A6:
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 ;
consider x being
Element of
Z;
x in Q
by A4, A5, TARSKI:def 3;
then A9:
ex
B being
Subset of
V st
(
B = x &
A c= B &
B is
linearly-independent )
by A2;
x c= W
by A4, ZFMISC_1:92;
then A10:
A c= W
by A9, XBOOLE_1:1;
W is
linearly-independent
proof
let l be
Linear_Combination of
W;
:: according to RLVECT_3:def 1 :: thesis: ( Sum l = 0. V implies 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, Lm7;
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
A c= B
and A30:
B is
linearly-independent
by A2, A5;
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, Def1;
:: thesis: verum
end; hence
union Z in Q
by A2, A10;
:: 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:
A c= B
and
A39:
B is linearly-independent
by A2, A35;
take
B
; :: thesis: ( A c= B & B is linearly-independent & Lin B = RLSStruct(# the carrier of V,the U2 of V,the U5 of V,the Mult of V #) )
thus
( A c= B & B is linearly-independent )
by A38, A39; :: thesis: Lin B = RLSStruct(# the carrier of V,the U2 of V,the U5 of V,the Mult of V #)
A40:
(Omega). V = RLSStruct(# the carrier of V,the U2 of V,the U5 of V,the Mult of V #)
;
assume
Lin B <> RLSStruct(# the carrier of V,the U2 of V,the U5 of V,the Mult of V #)
; :: thesis: contradiction
then consider v being VECTOR of V such that
A41:
( ( v in Lin B & not v in RLSStruct(# the carrier of V,the U2 of V,the U5 of V,the Mult of V #) ) or ( v in RLSStruct(# the carrier of V,the U2 of V,the U5 of V,the Mult of V #) & not v in Lin B ) )
by A40, RLSUB_1:39;
A42:
B \/ {v} is linearly-independent
proof
let l be
Linear_Combination of
B \/ {v};
:: according to RLVECT_3:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )
assume A43:
Sum l = 0. V
;
:: thesis: Carrier l = {}
now per cases
( v in Carrier l or not v in Carrier l )
;
suppose A44:
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 A45:
f . v = 0
and A46:
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(
VECTOR of
V)
-> Element of
NAT =
0 ;
consider g being
Function of the
carrier of
V,
REAL such that A49:
g . v = - (l . v)
and A50:
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;
A51:
f - g = l
A54:
Sum g = (- (l . v)) * v
by A49, RLVECT_2:50;
0. V = (Sum f) - (Sum g)
by A43, A51, Th4;
then Sum f =
(0. V) + (Sum g)
by RLSUB_2:78
.=
(- (l . v)) * v
by A54, RLVECT_1:10
;
then A55:
(- (l . v)) * v in Lin B
by Th17;
A56:
- (l . v) <> 0
by A44, RLVECT_2:28;
((- (l . v)) " ) * ((- (l . v)) * v) =
(((- (l . v)) " ) * (- (l . v))) * v
by RLVECT_1:def 9
.=
1
* v
by A56, XCMPLX_0:def 7
.=
v
by RLVECT_1:def 9
;
hence
Carrier l = {}
by A41, A55, RLSUB_1:29, RLVECT_1:3;
:: thesis: verum end;
hence
Carrier l = {}
;
:: thesis: verum
end;
v in {v}
by TARSKI:def 1;
then A59:
( v in B \/ {v} & not v in B )
by A41, Th18, RLVECT_1:3, XBOOLE_0:def 3;
B c= B \/ {v}
by XBOOLE_1:7;
then
A c= B \/ {v}
by A38, XBOOLE_1:1;
then
B \/ {v} in Q
by A2, A42;
hence
contradiction
by A36, A37, A59, XBOOLE_1:7; :: thesis: verum