let V be RealLinearSpace; :: thesis: for A being Subset of V st Lin A = V holds

ex B being Subset of V st

( B c= A & B is linearly-independent & Lin B = V )

let A be Subset of V; :: thesis: ( Lin A = V implies ex B being Subset of V st

( B c= A & B is linearly-independent & Lin B = V ) )

assume A1: Lin A = V ; :: thesis: ex B being Subset of V st

( B c= A & B is linearly-independent & Lin B = V )

defpred S_{1}[ set ] means ex B being Subset of V st

( B = $1 & B c= A & 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 & S_{1}[Z] ) )
from XFAMILY:sch 1();

then Q <> {} by A2;

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 A3, ORDERS_1:67;

consider B being Subset of V such that

A36: B = X and

A37: B c= A and

A38: B is linearly-independent by A2, A34;

take B ; :: thesis: ( B c= A & B is linearly-independent & Lin B = V )

thus ( B c= A & B is linearly-independent ) by A37, A38; :: thesis: Lin B = V

assume A39: Lin B <> V ; :: thesis: contradiction

A43: v in A and

A44: not v in Lin B ;

A45: B \/ {v} is linearly-independent

then B \/ {v} c= A by A37, XBOOLE_1:8;

then A61: B \/ {v} in Q by A2, A45;

v in {v} by TARSKI:def 1;

then A62: v in B \/ {v} by XBOOLE_0:def 3;

not v in B by A44, Th15;

hence contradiction by A35, A36, A62, A61, XBOOLE_1:7; :: thesis: verum

ex B being Subset of V st

( B c= A & B is linearly-independent & Lin B = V )

let A be Subset of V; :: thesis: ( Lin A = V implies ex B being Subset of V st

( B c= A & B is linearly-independent & Lin B = V ) )

assume A1: Lin A = V ; :: thesis: ex B being Subset of V st

( B c= A & B is linearly-independent & Lin B = V )

defpred S

( B = $1 & B c= A & 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 & S

A3: now :: thesis: for Z being set st Z <> {} & Z c= Q & Z is c=-linear holds

union Z in Q

( {} the carrier of V c= A & {} the carrier of V is linearly-independent )
by Th7;union Z in Q

let Z be set ; :: thesis: ( Z <> {} & Z c= Q & Z is c=-linear implies union Z in Q )

assume that

Z <> {} and

A4: Z c= Q and

A5: Z is c=-linear ; :: thesis: union Z in Q

set W = union Z;

union Z c= the carrier of V

A8: W is linearly-independent

end;assume that

Z <> {} and

A4: Z c= Q and

A5: Z is c=-linear ; :: thesis: union Z in Q

set W = union Z;

union Z c= the carrier of V

proof

then reconsider W = union Z as Subset of V ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union Z or x in the carrier of V )

assume x in union Z ; :: thesis: x in the carrier of V

then consider X being set such that

A6: x in X and

A7: X in Z by TARSKI:def 4;

X in bool the carrier of V by A2, A4, A7;

hence x in the carrier of V by A6; :: thesis: verum

end;assume x in union Z ; :: thesis: x in the carrier of V

then consider X being set such that

A6: x in X and

A7: X in Z by TARSKI:def 4;

X in bool the carrier of V by A2, A4, A7;

hence x in the carrier of V by A6; :: thesis: verum

A8: W is linearly-independent

proof

W c= A
deffunc H_{1}( object ) -> set = { C where C is Subset of V : ( $1 in C & C in Z ) } ;

let l be Linear_Combination of W; :: according to RLVECT_3:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )

assume that

A9: Sum l = 0. V and

A10: Carrier l <> {} ; :: thesis: 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 = H_{1}(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 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;

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

B c= A and

A27: B is linearly-independent by A2, A4;

Carrier l c= union (rng the Choice_Function of M)

hence contradiction by A9, A10, A27; :: thesis: verum

end;let l be Linear_Combination of W; :: according to RLVECT_3:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )

assume that

A9: Sum l = 0. V and

A10: Carrier l <> {} ; :: thesis: 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 = H

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;

A13: now :: thesis: not {} in M

then A18:
dom the Choice_Function of M = M
by Lm7;assume
{} in M
; :: thesis: contradiction

then consider x being object such that

A14: x in dom f and

A15: f . x = {} by FUNCT_1:def 3;

Carrier l c= W by RLVECT_2:def 6;

then consider X being set such that

A16: x in X and

A17: X in Z by A11, A14, TARSKI:def 4;

reconsider X = X as Subset of V by A2, A4, A17;

X in { C where C is Subset of V : ( x in C & C in Z ) } by A16, A17;

hence contradiction by A11, A12, A14, A15; :: thesis: verum

end;then consider x being object such that

A14: x in dom f and

A15: f . x = {} by FUNCT_1:def 3;

Carrier l c= W by RLVECT_2:def 6;

then consider X being set such that

A16: x in X and

A17: X in Z by A11, A14, TARSKI:def 4;

reconsider X = X as Subset of V by A2, A4, A17;

X in { C where C is Subset of V : ( x in C & C in Z ) } by A16, A17;

hence contradiction by A11, A12, A14, A15; :: thesis: verum

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;

A20: now :: thesis: for X being set st X in rng the Choice_Function of M holds

X in Z

X in Z

let X be set ; :: thesis: ( X in rng the Choice_Function of M implies X in Z )

assume X in rng the Choice_Function of M ; :: thesis: X in Z

then consider x being object such that

A21: x in dom the Choice_Function of M and

A22: the Choice_Function of M . x = X by FUNCT_1:def 3;

consider y being object such that

A23: ( y in dom f & f . y = x ) by A18, A21, FUNCT_1:def 3;

A24: x = { C where C is Subset of V : ( y in C & C in Z ) } by A11, A12, A23;

reconsider x = x as set by TARSKI:1;

X in x by A13, A18, A21, A22, ORDERS_1:89;

then ex C being Subset of V st

( C = X & y in C & C in Z ) by A24;

hence X in Z ; :: thesis: verum

end;assume X in rng the Choice_Function of M ; :: thesis: X in Z

then consider x being object such that

A21: x in dom the Choice_Function of M and

A22: the Choice_Function of M . x = X by FUNCT_1:def 3;

consider y being object such that

A23: ( y in dom f & f . y = x ) by A18, A21, FUNCT_1:def 3;

A24: x = { C where C is Subset of V : ( y in C & C in Z ) } by A11, A12, A23;

reconsider x = x as set by TARSKI:1;

X in x by A13, A18, A21, A22, ORDERS_1:89;

then ex C being Subset of V st

( C = X & y in C & C in Z ) by A24;

hence X in Z ; :: thesis: verum

A25: now :: thesis: for X, Y being set st X in rng the Choice_Function of M & Y in rng the Choice_Function of M & not X c= Y holds

Y c= X

rng the Choice_Function of M <> {}
by A18, RELAT_1:42;Y c= X

let X, Y be set ; :: thesis: ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M & not X c= Y implies Y c= X )

assume ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M ) ; :: thesis: ( X c= Y or Y c= X )

then ( X in Z & Y in Z ) by A20;

then X,Y are_c=-comparable by A5, ORDINAL1:def 8;

hence ( X c= Y or Y c= X ) ; :: thesis: verum

end;assume ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M ) ; :: thesis: ( X c= Y or Y c= X )

then ( X in Z & Y in Z ) by A20;

then X,Y are_c=-comparable by A5, ORDINAL1:def 8;

hence ( X c= Y or Y c= X ) ; :: thesis: verum

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

B c= A and

A27: B is linearly-independent by A2, A4;

Carrier l c= union (rng the Choice_Function of M)

proof

then
l is Linear_Combination of B
by A26, RLVECT_2:def 6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier l or x in union (rng the Choice_Function of M) )

set X = f . x;

assume A28: x in Carrier l ; :: thesis: x in union (rng the Choice_Function of M)

then A29: f . x = { C where C is Subset of V : ( x in C & C in Z ) } by A12;

A30: f . x in M by A11, A28, FUNCT_1:def 3;

then the Choice_Function of M . (f . x) in f . x by A13, ORDERS_1:89;

then A31: ex C being Subset of V st

( the Choice_Function of M . (f . x) = C & x in C & C in Z ) by A29;

the Choice_Function of M . (f . x) in rng the Choice_Function of M by A18, A30, FUNCT_1:def 3;

hence x in union (rng the Choice_Function of M) by A31, TARSKI:def 4; :: thesis: verum

end;set X = f . x;

assume A28: x in Carrier l ; :: thesis: x in union (rng the Choice_Function of M)

then A29: f . x = { C where C is Subset of V : ( x in C & C in Z ) } by A12;

A30: f . x in M by A11, A28, FUNCT_1:def 3;

then the Choice_Function of M . (f . x) in f . x by A13, ORDERS_1:89;

then A31: ex C being Subset of V st

( the Choice_Function of M . (f . x) = C & x in C & C in Z ) by A29;

the Choice_Function of M . (f . x) in rng the Choice_Function of M by A18, A30, FUNCT_1:def 3;

hence x in union (rng the Choice_Function of M) by A31, TARSKI:def 4; :: thesis: verum

hence contradiction by A9, A10, A27; :: thesis: verum

proof

hence
union Z in Q
by A2, A8; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in W or x in A )

assume x in W ; :: thesis: x in A

then consider X being set such that

A32: x in X and

A33: X in Z by TARSKI:def 4;

ex B being Subset of V st

( B = X & B c= A & B is linearly-independent ) by A2, A4, A33;

hence x in A by A32; :: thesis: verum

end;assume x in W ; :: thesis: x in A

then consider X being set such that

A32: x in X and

A33: X in Z by TARSKI:def 4;

ex B being Subset of V st

( B = X & B c= A & B is linearly-independent ) by A2, A4, A33;

hence x in A by A32; :: thesis: verum

then Q <> {} by A2;

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 A3, ORDERS_1:67;

consider B being Subset of V such that

A36: B = X and

A37: B c= A and

A38: B is linearly-independent by A2, A34;

take B ; :: thesis: ( B c= A & B is linearly-independent & Lin B = V )

thus ( B c= A & B is linearly-independent ) by A37, A38; :: thesis: Lin B = V

assume A39: Lin B <> V ; :: thesis: contradiction

now :: thesis: ex v being VECTOR of V st

( v in A & not v in Lin B )

then consider v being VECTOR of V such that ( v in A & not v in Lin B )

assume A40:
for v being VECTOR of V st v in A holds

v in Lin B ; :: thesis: contradiction

hence contradiction by A1, A39, RLSUB_1:26; :: thesis: verum

end;v in Lin B ; :: thesis: contradiction

now :: thesis: for v being VECTOR of V st v in Lin A holds

v in Lin B

then
Lin A is Subspace of Lin B
by RLSUB_1:29;v in Lin B

reconsider F = the carrier of (Lin B) as Subset of V by RLSUB_1:def 2;

let v be VECTOR of V; :: thesis: ( v in Lin A implies v in Lin B )

assume v in Lin A ; :: thesis: v in Lin B

then consider l being Linear_Combination of A such that

A41: v = Sum l by Th14;

Carrier l c= the carrier of (Lin B)

Sum l = v by A41;

then v in Lin F by Th14;

hence v in Lin B by Th18; :: thesis: verum

end;let v be VECTOR of V; :: thesis: ( v in Lin A implies v in Lin B )

assume v in Lin A ; :: thesis: v in Lin B

then consider l being Linear_Combination of A such that

A41: v = Sum l by Th14;

Carrier l c= the carrier of (Lin B)

proof

then reconsider l = l as Linear_Combination of F by RLVECT_2:def 6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier l or x in the carrier of (Lin B) )

assume A42: x in Carrier l ; :: thesis: x in the carrier of (Lin B)

then reconsider a = x as VECTOR of V ;

Carrier l c= A by RLVECT_2:def 6;

then a in Lin B by A40, A42;

hence x in the carrier of (Lin B) by STRUCT_0:def 5; :: thesis: verum

end;assume A42: x in Carrier l ; :: thesis: x in the carrier of (Lin B)

then reconsider a = x as VECTOR of V ;

Carrier l c= A by RLVECT_2:def 6;

then a in Lin B by A40, A42;

hence x in the carrier of (Lin B) by STRUCT_0:def 5; :: thesis: verum

Sum l = v by A41;

then v in Lin F by Th14;

hence v in Lin B by Th18; :: thesis: verum

hence contradiction by A1, A39, RLSUB_1:26; :: thesis: verum

A43: v in A and

A44: not v in Lin B ;

A45: B \/ {v} is linearly-independent

proof

{v} c= A
by A43, ZFMISC_1:31;
let l be Linear_Combination of B \/ {v}; :: according to RLVECT_3:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )

assume A46: Sum l = 0. V ; :: thesis: Carrier l = {}

end;assume A46: Sum l = 0. V ; :: thesis: Carrier l = {}

now :: thesis: Carrier l = {} end;

hence
Carrier l = {}
; :: thesis: verumper cases
( v in Carrier l or not v in Carrier l )
;

end;

suppose
v in Carrier l
; :: thesis: Carrier l = {}

then A47:
- (l . v) <> 0
by RLVECT_2:19;

deffunc H_{1}( VECTOR of V) -> Element of REAL = In (0,REAL);

deffunc H_{2}( VECTOR of V) -> Element of REAL = l . $1;

consider f being Function of the carrier of V,REAL such that

A48: f . v = In (0,REAL) and

A49: for u being VECTOR of V st u <> v holds

f . u = H_{2}(u)
from FUNCT_2:sch 6();

reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;

Carrier f c= B

consider g being Function of the carrier of V,REAL such that

A53: g . v = - (l . v) and

A54: for u being VECTOR of V st u <> v holds

g . u = H_{1}(u)
from FUNCT_2:sch 6();

reconsider g = g as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;

Carrier g c= {v}

A55: Sum g = (- (l . v)) * v by A53, RLVECT_2:32;

f - g = l

then Sum f = (0. V) + (Sum g) by RLSUB_2:61

.= (- (l . v)) * v by A55 ;

then A58: (- (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 A47, XCMPLX_0:def 7

.= v by RLVECT_1:def 8 ;

hence Carrier l = {} by A44, A58, RLSUB_1:21; :: thesis: verum

end;deffunc H

deffunc H

consider f being Function of the carrier of V,REAL such that

A48: f . v = In (0,REAL) and

A49: for u being VECTOR of V st u <> v holds

f . u = H

reconsider f = f as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;

now :: thesis: for u being VECTOR of V st not u in (Carrier l) \ {v} holds

f . u = 0

then reconsider f = f as Linear_Combination of V by RLVECT_2:def 3;f . u = 0

let u be VECTOR of V; :: thesis: ( not u in (Carrier l) \ {v} implies f . u = 0 )

assume not u in (Carrier l) \ {v} ; :: thesis: f . u = 0

then ( not u in Carrier l or u in {v} ) by XBOOLE_0:def 5;

then ( ( l . u = 0 & u <> v ) or u = v ) by TARSKI:def 1;

hence f . u = 0 by A48, A49; :: thesis: verum

end;assume not u in (Carrier l) \ {v} ; :: thesis: f . u = 0

then ( not u in Carrier l or u in {v} ) by XBOOLE_0:def 5;

then ( ( l . u = 0 & u <> v ) or u = v ) by TARSKI:def 1;

hence f . u = 0 by A48, A49; :: thesis: verum

Carrier f c= B

proof

then reconsider f = f as Linear_Combination of B by RLVECT_2:def 6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in B )

A50: Carrier l c= B \/ {v} by RLVECT_2:def 6;

assume x in Carrier f ; :: thesis: x in B

then consider u being VECTOR of V such that

A51: u = x and

A52: f . u <> 0 ;

f . u = l . u by A48, A49, A52;

then u in Carrier l by A52;

then ( u in B or u in {v} ) by A50, XBOOLE_0:def 3;

hence x in B by A48, A51, A52, TARSKI:def 1; :: thesis: verum

end;A50: Carrier l c= B \/ {v} by RLVECT_2:def 6;

assume x in Carrier f ; :: thesis: x in B

then consider u being VECTOR of V such that

A51: u = x and

A52: f . u <> 0 ;

f . u = l . u by A48, A49, A52;

then u in Carrier l by A52;

then ( u in B or u in {v} ) by A50, XBOOLE_0:def 3;

hence x in B by A48, A51, A52, TARSKI:def 1; :: thesis: verum

consider g being Function of the carrier of V,REAL such that

A53: g . v = - (l . v) and

A54: for u being VECTOR of V st u <> v holds

g . u = H

reconsider g = g as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;

now :: thesis: for u being VECTOR of V st not u in {v} holds

g . u = 0

then reconsider g = g as Linear_Combination of V by RLVECT_2:def 3;g . u = 0

let u be VECTOR of V; :: thesis: ( not u in {v} implies g . u = 0 )

assume not u in {v} ; :: thesis: g . u = 0

then u <> v by TARSKI:def 1;

hence g . u = 0 by A54; :: thesis: verum

end;assume not u in {v} ; :: thesis: g . u = 0

then u <> v by TARSKI:def 1;

hence g . u = 0 by A54; :: thesis: verum

Carrier g c= {v}

proof

then reconsider g = g as Linear_Combination of {v} by RLVECT_2:def 6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier g or x in {v} )

assume x in Carrier g ; :: thesis: x in {v}

then ex u being VECTOR of V st

( x = u & g . u <> 0 ) ;

then x = v by A54;

hence x in {v} by TARSKI:def 1; :: thesis: verum

end;assume x in Carrier g ; :: thesis: x in {v}

then ex u being VECTOR of V st

( x = u & g . u <> 0 ) ;

then x = v by A54;

hence x in {v} by TARSKI:def 1; :: thesis: verum

A55: Sum g = (- (l . v)) * v by A53, RLVECT_2:32;

f - g = l

proof

then
0. V = (Sum f) - (Sum g)
by A46, Th4;
let u be VECTOR of V; :: according to RLVECT_2:def 9 :: thesis: (f - g) . u = l . u

end;now :: thesis: (f - g) . u = l . uend;

hence
(f - g) . u = l . u
; :: thesis: verumthen Sum f = (0. V) + (Sum g) by RLSUB_2:61

.= (- (l . v)) * v by A55 ;

then A58: (- (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 A47, XCMPLX_0:def 7

.= v by RLVECT_1:def 8 ;

hence Carrier l = {} by A44, A58, RLSUB_1:21; :: thesis: verum

suppose A59:
not v in Carrier l
; :: thesis: Carrier l = {}

Carrier l c= B

hence Carrier l = {} by A38, A46; :: thesis: verum

end;proof

then
l is Linear_Combination of B
by RLVECT_2:def 6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier l or x in B )

assume A60: x in Carrier l ; :: thesis: x in B

Carrier l c= B \/ {v} by RLVECT_2:def 6;

then ( x in B or x in {v} ) by A60, XBOOLE_0:def 3;

hence x in B by A59, A60, TARSKI:def 1; :: thesis: verum

end;assume A60: x in Carrier l ; :: thesis: x in B

Carrier l c= B \/ {v} by RLVECT_2:def 6;

then ( x in B or x in {v} ) by A60, XBOOLE_0:def 3;

hence x in B by A59, A60, TARSKI:def 1; :: thesis: verum

hence Carrier l = {} by A38, A46; :: thesis: verum

then B \/ {v} c= A by A37, XBOOLE_1:8;

then A61: B \/ {v} in Q by A2, A45;

v in {v} by TARSKI:def 1;

then A62: v in B \/ {v} by XBOOLE_0:def 3;

not v in B by A44, Th15;

hence contradiction by A35, A36, A62, A61, XBOOLE_1:7; :: thesis: verum