let GF be Field; :: thesis: for V being VectSp of GF
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 = VectSpStr(# the carrier of V,the U5 of V,the U2 of V,the lmult of V #) )
let V be VectSp of GF; :: 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 = VectSpStr(# the carrier of V,the U5 of V,the U2 of V,the lmult 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 = VectSpStr(# the carrier of V,the U5 of V,the U2 of V,the lmult 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 = VectSpStr(# the carrier of V,the U5 of V,the U2 of V,the lmult 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 VECTSP_7: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, 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
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, VECTSP_6:def 7;
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 = VectSpStr(# the carrier of V,the U5 of V,the U2 of V,the lmult of V #) )
thus
( A c= B & B is linearly-independent )
by A38, A39; :: thesis: Lin B = VectSpStr(# the carrier of V,the U5 of V,the U2 of V,the lmult of V #)
assume
Lin B <> VectSpStr(# the carrier of V,the U5 of V,the U2 of V,the lmult of V #)
; :: thesis: contradiction
then consider v being Vector of V such that
A40:
( ( v in Lin B & not v in (Omega). V ) or ( v in (Omega). V & not v in Lin B ) )
by VECTSP_4:38;
A41:
B \/ {v} is linearly-independent
proof
let l be
Linear_Combination of
B \/ {v};
:: according to VECTSP_7:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )
assume A42:
Sum l = 0. V
;
:: thesis: Carrier l = {}
now per cases
( v in Carrier l or not v in Carrier l )
;
suppose A43:
v in Carrier l
;
:: thesis: Carrier l = {} deffunc H1(
Vector of
V)
-> Element of the
carrier of
GF =
l . $1;
consider f being
Function of the
carrier of
V,the
carrier of
GF such that A44:
f . v = 0. GF
and A45:
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
GF by FUNCT_2:11;
then reconsider f =
f as
Linear_Combination of
V by VECTSP_6:def 4;
Carrier f c= B
then reconsider f =
f as
Linear_Combination of
B by VECTSP_6:def 7;
deffunc H2(
set )
-> Element of the
carrier of
GF =
0. GF;
consider g being
Function of the
carrier of
V,the
carrier of
GF such that A48:
g . v = - (l . v)
and A49:
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
GF by FUNCT_2:11;
then reconsider g =
g as
Linear_Combination of
V by VECTSP_6:def 4;
Carrier g c= {v}
then reconsider g =
g as
Linear_Combination of
{v} by VECTSP_6:def 7;
A50:
f - g = l
A53:
Sum g = (- (l . v)) * v
by A48, VECTSP_6:43;
0. V = (Sum f) - (Sum g)
by A42, A50, VECTSP_6:80;
then Sum f =
(0. V) + (Sum g)
by VECTSP_2:22
.=
(- (l . v)) * v
by A53, RLVECT_1:10
;
then A54:
(- (l . v)) * v in Lin B
by Th12;
l . v <> 0. GF
by A43, VECTSP_6:20;
then A55:
- (l . v) <> 0. GF
by VECTSP_2:34;
((- (l . v)) " ) * ((- (l . v)) * v) =
(((- (l . v)) " ) * (- (l . v))) * v
by VECTSP_1:def 26
.=
(1_ GF) * v
by A55, VECTSP_1:def 22
.=
v
by VECTSP_1:def 26
;
hence
Carrier l = {}
by A40, A54, RLVECT_1:3, VECTSP_4:29;
:: thesis: verum end;
hence
Carrier l = {}
;
:: thesis: verum
end;
v in {v}
by TARSKI:def 1;
then A58:
( v in B \/ {v} & not v in B )
by A40, Th13, 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, A41;
hence
contradiction
by A36, A37, A58, XBOOLE_1:7; :: thesis: verum