let V be RealLinearSpace; for A, B being Subset of V st A is linearly-independent & A c= B & Lin B = V holds
ex I being linearly-independent Subset of V st
( A c= I & I c= B & Lin I = V )
let A, B be Subset of V; ( A is linearly-independent & A c= B & Lin B = V implies ex I being linearly-independent Subset of V st
( A c= I & I c= B & Lin I = V ) )
assume that
A1:
( A is linearly-independent & A c= B )
and
A2:
Lin B = V
; ex I being linearly-independent Subset of V st
( A c= I & I c= B & Lin I = V )
defpred S1[ set ] means ex I being Subset of V st
( I = $1 & A c= I & I c= B & I is linearly-independent );
consider Q being set such that
A3:
for Z being set holds
( Z in Q iff ( Z in bool the carrier of V & S1[Z] ) )
from XBOOLE_0:sch 1();
A4:
now let Z be
set ;
( Z <> {} & Z c= Q & Z is c=-linear implies union Z in Q )assume that A5:
Z <> {}
and A6:
Z c= Q
and A7:
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 ;
set y = the
Element of
Z;
the
Element of
Z in Q
by A5, A6, TARSKI:def 3;
then A10:
ex
I being
Subset of
V st
(
I = the
Element of
Z &
A c= I &
I c= B &
I is
linearly-independent )
by A3;
A11:
W is
linearly-independent
proof
deffunc H1(
set )
-> set =
{ D where D is Subset of V : ( $1 in D & D in Z ) } ;
let l be
Linear_Combination of
W;
RLVECT_3:def 1 ( not Sum l = 0. V or Carrier l = {} )
assume that A12:
Sum l = 0. V
and A13:
Carrier l <> {}
;
contradiction
consider f being
Function such that A14:
dom f = Carrier l
and A15:
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 A13, A14, RELAT_1:42;
set F = the
Choice_Function of
M;
set S =
rng the
Choice_Function of
M;
the
Element of
M in M
;
then A21:
union M <> {}
by A16, ORDERS_1:6;
then A22:
dom the
Choice_Function of
M = M
by FUNCT_2:def 1;
dom the
Choice_Function of
M is
finite
by A14, A22, FINSET_1:8;
then
rng the
Choice_Function of
M is
finite
by FINSET_1:8;
then
union (rng the Choice_Function of M) in rng the
Choice_Function of
M
by A21, A28, CARD_2:62;
then
union (rng the Choice_Function of M) in Z
by A23;
then consider I being
Subset of
V such that A29:
I = union (rng the Choice_Function of M)
and
A c= I
and
I c= B
and A30:
I is
linearly-independent
by A3, A6;
Carrier l c= union (rng the Choice_Function of M)
then
l is
Linear_Combination of
I
by A29, RLVECT_2:def 6;
hence
contradiction
by A12, A13, A30, RLVECT_3:def 1;
verum
end; A35:
W c= B
the
Element of
Z c= W
by A5, ZFMISC_1:74;
then
A c= W
by A10, XBOOLE_1:1;
hence
union Z in Q
by A3, A11, A35;
verum end;
Q <> {}
by A1, A3;
then consider X being set such that
A38:
X in Q
and
A39:
for Z being set st Z in Q & Z <> X holds
not X c= Z
by A4, ORDERS_1:67;
consider I being Subset of V such that
A40:
I = X
and
A41:
A c= I
and
A42:
I c= B
and
A43:
I is linearly-independent
by A3, A38;
reconsider I = I as linearly-independent Subset of V by A43;
take
I
; ( A c= I & I c= B & Lin I = V )
thus
( A c= I & I c= B )
by A41, A42; Lin I = V
assume A44:
Lin I <> V
; contradiction
then consider v being VECTOR of V such that
A48:
v in B
and
A49:
not v in Lin I
;
A50:
not v in I
by A49, RLVECT_3:15;
{v} c= B
by A48, ZFMISC_1:31;
then A51:
I \/ {v} c= B
by A42, XBOOLE_1:8;
v in {v}
by TARSKI:def 1;
then A52:
v in I \/ {v}
by XBOOLE_0:def 3;
A53:
I \/ {v} is linearly-independent
proof
let l be
Linear_Combination of
I \/ {v};
RLVECT_3:def 1 ( not Sum l = 0. V or Carrier l = {} )
assume A54:
Sum l = 0. V
;
Carrier l = {}
per cases
( v in Carrier l or not v in Carrier l )
;
suppose
v in Carrier l
;
Carrier l = {} then A55:
- (l . v) <> 0
by RLVECT_2:19;
deffunc H1(
VECTOR of
V)
-> Element of
NAT =
0 ;
deffunc H2(
VECTOR of
V)
-> Element of
REAL =
l . $1;
consider f being
Function of the
carrier of
V,
REAL such that A56:
f . v = 0
and A57:
for
u being
Element 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= I
then reconsider f =
f as
Linear_Combination of
I by RLVECT_2:def 6;
consider g being
Function of the
carrier of
V,
REAL such that A60:
g . v = - (l . v)
and A61:
for
u being
Element 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;
A62:
Sum g = (- (l . v)) * v
by A60, RLVECT_2:32;
then
f - g = l
by RLVECT_2:def 9;
then
0. V = (Sum f) - (Sum g)
by A54, RLVECT_3:4;
then Sum f =
(0. V) + (Sum g)
by RLSUB_2:61
.=
(- (l . v)) * v
by A62, RLVECT_1:4
;
then A65:
(- (l . v)) * v in Lin I
by RLVECT_3:14;
((- (l . v)) ") * ((- (l . v)) * v) =
(((- (l . v)) ") * (- (l . v))) * v
by RLVECT_1:def 7
.=
1
* v
by A55, XCMPLX_0:def 7
.=
v
by RLVECT_1:def 8
;
hence
Carrier l = {}
by A49, A65, RLSUB_1:21;
verum end;
end;
A c= I \/ {v}
by A41, XBOOLE_1:10;
then
I \/ {v} in Q
by A3, A51, A53;
hence
contradiction
by A39, A40, A50, A52, XBOOLE_1:7; verum