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 XFAMILY:sch 1();
A4:
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 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;
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(
object )
-> 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
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 A13, A14, RELAT_1:42;
set F = the
Choice_Function of
M;
set S =
rng the
Choice_Function of
M;
A21:
the
Choice_Function of
M is
Function of
M,
(union M)
by A16, ORDERS_1:90;
the
Element of
M in M
;
then A22:
union M <> {}
by A16, ORDERS_1:6;
then A23:
dom the
Choice_Function of
M = M
by FUNCT_2:def 1, A21;
dom the
Choice_Function of
M is
finite
by A14, A23, 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 A22, A29, CARD_2:62, A21;
then
union (rng the Choice_Function of M) in Z
by A24;
then consider I being
Subset of
V such that A30:
I = union (rng the Choice_Function of M)
and
A c= I
and
I c= B
and A31:
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 A30, RLVECT_2:def 6;
hence
contradiction
by A12, A13, A31;
verum
end; A36:
W c= B
the
Element of
Z c= W
by A5, ZFMISC_1:74;
then
A c= W
by A10;
hence
union Z in Q
by A3, A11, A36;
verum end;
Q <> {}
by A1, A3;
then consider X being set such that
A39:
X in Q
and
A40:
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
A41:
I = X
and
A42:
A c= I
and
A43:
I c= B
and
A44:
I is linearly-independent
by A3, A39;
reconsider I = I as linearly-independent Subset of V by A44;
take
I
; ( A c= I & I c= B & Lin I = V )
thus
( A c= I & I c= B )
by A42, A43; Lin I = V
assume A45:
Lin I <> V
; contradiction
then consider v being VECTOR of V such that
A49:
v in B
and
A50:
not v in Lin I
;
A51:
not v in I
by A50, RLVECT_3:15;
{v} c= B
by A49, ZFMISC_1:31;
then A52:
I \/ {v} c= B
by A43, XBOOLE_1:8;
v in {v}
by TARSKI:def 1;
then A53:
v in I \/ {v}
by XBOOLE_0:def 3;
A54:
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 A55:
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 A56:
- (l . v) <> 0
by RLVECT_2:19;
deffunc H1(
VECTOR of
V)
-> 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 A57:
f . v = In (
0,
REAL)
and A58:
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 A61:
g . v = - (l . v)
and A62:
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;
A63:
Sum g = (- (l . v)) * v
by A61, RLVECT_2:32;
then
f - g = l
;
then
0. V = (Sum f) - (Sum g)
by A55, RLVECT_3:4;
then Sum f =
(0. V) + (Sum g)
by RLSUB_2:61
.=
(- (l . v)) * v
by A63
;
then A66:
(- (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 A56, XCMPLX_0:def 7
.=
v
by RLVECT_1:def 8
;
hence
Carrier l = {}
by A50, A66, RLSUB_1:21;
verum end;
end;
A c= I \/ {v}
by A42, XBOOLE_1:10;
then
I \/ {v} in Q
by A3, A52, A54;
hence
contradiction
by A40, A41, A51, A53, XBOOLE_1:7; verum