let V be RealLinearSpace; 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 ZeroF of V, the U5 of V, the Mult of V #) )
let A be Subset of V; ( 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 ZeroF 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
A1:
for Z being set holds
( Z in Q iff ( Z in bool the carrier of V & S1[Z] ) )
from XFAMILY:sch 1();
A2:
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 A3:
Z <> {}
and A4:
Z c= Q
and A5:
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 ;
A8:
W is
linearly-independent
proof
deffunc H1(
object )
-> set =
{ C where C is Subset of V : ( $1 in C & C in Z ) } ;
let l be
Linear_Combination of
W;
RLVECT_3:def 1 ( Sum l = 0. V implies Carrier l = {} )
assume that A9:
Sum l = 0. V
and A10:
Carrier l <> {}
;
contradiction
consider f being
Function such that A11:
dom f = Carrier l
and A12:
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 A10, A11, RELAT_1:42;
set F = the
Choice_Function of
M;
set S =
rng the
Choice_Function of
M;
then A18:
dom the
Choice_Function of
M = M
by Lm7;
then
dom the
Choice_Function of
M is
finite
by A11, FINSET_1:8;
then A19:
rng the
Choice_Function of
M is
finite
by FINSET_1:8;
rng the
Choice_Function of
M <> {}
by A18, RELAT_1:42;
then
union (rng the Choice_Function of M) in rng the
Choice_Function of
M
by A25, A19, CARD_2:62;
then
union (rng the Choice_Function of M) in Z
by A20;
then consider B being
Subset of
V such that A26:
B = union (rng the Choice_Function of M)
and
A c= B
and A27:
B is
linearly-independent
by A1, A4;
Carrier l c= union (rng the Choice_Function of M)
then
l is
Linear_Combination of
B
by A26, RLVECT_2:def 6;
hence
contradiction
by A9, A10, A27;
verum
end; set x = the
Element of
Z;
the
Element of
Z in Q
by A3, A4;
then A32:
ex
B being
Subset of
V st
(
B = the
Element of
Z &
A c= B &
B is
linearly-independent )
by A1;
the
Element of
Z c= W
by A3, ZFMISC_1:74;
then
A c= W
by A32;
hence
union Z in Q
by A1, A8;
verum end;
A33:
(Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #)
;
assume
A is linearly-independent
; ex B being Subset of V st
( A c= B & B is linearly-independent & Lin B = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) )
then
Q <> {}
by A1;
then consider X being set such that
A34:
X in Q
and
A35:
for Z being set st Z in Q & Z <> X holds
not X c= Z
by A2, ORDERS_1:67;
consider B being Subset of V such that
A36:
B = X
and
A37:
A c= B
and
A38:
B is linearly-independent
by A1, A34;
take
B
; ( A c= B & B is linearly-independent & Lin B = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) )
thus
( A c= B & B is linearly-independent )
by A37, A38; Lin B = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #)
assume
Lin B <> RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #)
; contradiction
then consider v being VECTOR of V such that
A39:
( ( v in Lin B & not v in RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) ) or ( v in RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) & not v in Lin B ) )
by A33, RLSUB_1:31;
A40:
B \/ {v} is linearly-independent
proof
let l be
Linear_Combination of
B \/ {v};
RLVECT_3:def 1 ( Sum l = 0. V implies Carrier l = {} )
assume A41:
Sum l = 0. V
;
Carrier l = {}
now Carrier l = {} per cases
( v in Carrier l or not v in Carrier l )
;
suppose
v in Carrier l
;
Carrier l = {} then A42:
- (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 A43:
f . v = In (
0,
REAL)
and A44:
for
u being
VECTOR 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= B
then reconsider f =
f as
Linear_Combination of
B by RLVECT_2:def 6;
consider g being
Function of the
carrier of
V,
REAL such that A48:
g . v = - (l . v)
and A49:
for
u being
VECTOR 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;
A50:
Sum g = (- (l . v)) * v
by A48, RLVECT_2:32;
f - g = l
then
0. V = (Sum f) - (Sum g)
by A41, Th4;
then Sum f =
(0. V) + (Sum g)
by RLSUB_2:61
.=
(- (l . v)) * v
by A50
;
then A53:
(- (l . v)) * v in Lin B
by Th14;
((- (l . v)) ") * ((- (l . v)) * v) =
(((- (l . v)) ") * (- (l . v))) * v
by RLVECT_1:def 7
.=
1
* v
by A42, XCMPLX_0:def 7
.=
v
by RLVECT_1:def 8
;
hence
Carrier l = {}
by A39, A53, RLSUB_1:21, RLVECT_1:1;
verum end;
hence
Carrier l = {}
;
verum
end;
v in {v}
by TARSKI:def 1;
then A56:
v in B \/ {v}
by XBOOLE_0:def 3;
A57:
not v in B
by A39, Th15, RLVECT_1:1;
B c= B \/ {v}
by XBOOLE_1:7;
then
A c= B \/ {v}
by A37;
then
B \/ {v} in Q
by A1, A40;
hence
contradiction
by A35, A36, A56, A57, XBOOLE_1:7; verum