let V be RealLinearSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ex I being linearly-independent Subset of V st

( A c= I & I c= B & Lin I = V )

defpred S_{1}[ 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 & S_{1}[Z] ) )
from XFAMILY:sch 1();

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 ; :: thesis: ( A c= I & I c= B & Lin I = V )

thus ( A c= I & I c= B ) by A42, A43; :: thesis: Lin I = V

assume A45: Lin I <> V ; :: thesis: contradiction

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

then I \/ {v} in Q by A3, A52, A54;

hence contradiction by A40, A41, A51, A53, XBOOLE_1:7; :: thesis: verum

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; :: thesis: ( 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 ; :: thesis: ex I being linearly-independent Subset of V st

( A c= I & I c= B & Lin I = V )

defpred S

( 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 & S

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

union Z in Q

Q <> {}
by A1, A3;union Z in Q

let Z be set ; :: thesis: ( 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 ; :: thesis: union Z in Q

set W = union Z;

union Z c= the carrier 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

then A c= W by A10;

hence union Z in Q by A3, A11, A36; :: thesis: verum

end;assume that

A5: Z <> {} and

A6: Z c= Q and

A7: 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

A8: x in X and

A9: X in Z by TARSKI:def 4;

X in bool the carrier of V by A3, A6, A9;

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

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

then consider X being set such that

A8: x in X and

A9: X in Z by TARSKI:def 4;

X in bool the carrier of V by A3, A6, A9;

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

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

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

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

assume that

A12: Sum l = 0. V and

A13: Carrier l <> {} ; :: thesis: 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 = H_{1}(x)
from FUNCT_1:sch 3();

reconsider M = rng f as non empty set by A13, A14, RELAT_1:42;

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;

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)

hence contradiction by A12, A13, A31; :: thesis: verum

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

assume that

A12: Sum l = 0. V and

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

reconsider M = rng f as non empty set by A13, A14, RELAT_1:42;

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

set F = the Choice_Function of M;assume
{} in M
; :: thesis: contradiction

then consider x being object such that

A17: x in dom f and

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

Carrier l c= W by RLVECT_2:def 6;

then consider X being set such that

A19: x in X and

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

reconsider X = X as Subset of V by A3, A6, A20;

X in { D where D is Subset of V : ( x in D & D in Z ) } by A19, A20;

hence contradiction by A14, A15, A17, A18; :: thesis: verum

end;then consider x being object such that

A17: x in dom f and

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

Carrier l c= W by RLVECT_2:def 6;

then consider X being set such that

A19: x in X and

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

reconsider X = X as Subset of V by A3, A6, A20;

X in { D where D is Subset of V : ( x in D & D in Z ) } by A19, A20;

hence contradiction by A14, A15, A17, A18; :: thesis: verum

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;

A24: 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

A25: x in dom the Choice_Function of M and

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

reconsider x = x as set by TARSKI:1;

consider y being object such that

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

A28: x = { D where D is Subset of V : ( y in D & D in Z ) } by A14, A15, A27;

X in x by A16, A23, A25, A26, ORDERS_1:89;

then ex D being Subset of V st

( D = X & y in D & D in Z ) by A28;

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

A25: x in dom the Choice_Function of M and

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

reconsider x = x as set by TARSKI:1;

consider y being object such that

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

A28: x = { D where D is Subset of V : ( y in D & D in Z ) } by A14, A15, A27;

X in x by A16, A23, A25, A26, ORDERS_1:89;

then ex D being Subset of V st

( D = X & y in D & D in Z ) by A28;

hence X in Z ; :: thesis: verum

A29: 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

dom the Choice_Function of M is finite
by A14, A23, FINSET_1:8;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 A24;

then X,Y are_c=-comparable by A7, 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 A24;

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

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

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)

proof

then
l is Linear_Combination of I
by A30, 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) )

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

then A33: f . x = { D where D is Subset of V : ( x in D & D in Z ) } by A15;

A34: f . x in M by A14, A32, FUNCT_1:def 3;

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

then A35: ex D being Subset of V st

( the Choice_Function of M . (f . x) = D & x in D & D in Z ) by A33;

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

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

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

then A33: f . x = { D where D is Subset of V : ( x in D & D in Z ) } by A15;

A34: f . x in M by A14, A32, FUNCT_1:def 3;

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

then A35: ex D being Subset of V st

( the Choice_Function of M . (f . x) = D & x in D & D in Z ) by A33;

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

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

hence contradiction by A12, A13, A31; :: thesis: verum

proof

the Element of Z c= W
by A5, ZFMISC_1:74;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in W or x in B )

assume x in W ; :: thesis: x in B

then consider X being set such that

A37: x in X and

A38: X in Z by TARSKI:def 4;

ex I being Subset of V st

( I = X & A c= I & I c= B & I is linearly-independent ) by A3, A6, A38;

hence x in B by A37; :: thesis: verum

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

then consider X being set such that

A37: x in X and

A38: X in Z by TARSKI:def 4;

ex I being Subset of V st

( I = X & A c= I & I c= B & I is linearly-independent ) by A3, A6, A38;

hence x in B by A37; :: thesis: verum

then A c= W by A10;

hence union Z in Q by A3, A11, A36; :: thesis: verum

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 ; :: thesis: ( A c= I & I c= B & Lin I = V )

thus ( A c= I & I c= B ) by A42, A43; :: thesis: Lin I = V

assume A45: Lin I <> V ; :: thesis: contradiction

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

( v in B & not v in Lin I )

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

assume A46:
for v being VECTOR of V st v in B holds

v in Lin I ; :: thesis: contradiction

hence contradiction by A2, A45, RLSUB_1:26; :: thesis: verum

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

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

v in Lin I

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

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

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

then consider l being Linear_Combination of B such that

A47: v = Sum l by RLVECT_3:14;

Carrier l c= the carrier of (Lin I)

Sum l = v by A47;

then v in Lin (Up (Lin I)) by RLVECT_3:14;

hence v in Lin I by RLVECT_3:18; :: thesis: verum

end;assume v in Lin B ; :: thesis: v in Lin I

then consider l being Linear_Combination of B such that

A47: v = Sum l by RLVECT_3:14;

Carrier l c= the carrier of (Lin I)

proof

then reconsider l = l as Linear_Combination of Up (Lin I) 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 I) )

assume A48: x in Carrier l ; :: thesis: x in the carrier of (Lin I)

then reconsider a = x as VECTOR of V ;

Carrier l c= B by RLVECT_2:def 6;

then a in Lin I by A46, A48;

hence x in the carrier of (Lin I) ; :: thesis: verum

end;assume A48: x in Carrier l ; :: thesis: x in the carrier of (Lin I)

then reconsider a = x as VECTOR of V ;

Carrier l c= B by RLVECT_2:def 6;

then a in Lin I by A46, A48;

hence x in the carrier of (Lin I) ; :: thesis: verum

Sum l = v by A47;

then v in Lin (Up (Lin I)) by RLVECT_3:14;

hence v in Lin I by RLVECT_3:18; :: thesis: verum

hence contradiction by A2, A45, RLSUB_1:26; :: thesis: verum

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

A c= I \/ {v}
by A42, XBOOLE_1:10;
let l be Linear_Combination of I \/ {v}; :: according to RLVECT_3:def 1 :: thesis: ( not Sum l = 0. V or Carrier l = {} )

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

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

per cases
( v in Carrier l or not v in Carrier l )
;

end;

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

then A56:
- (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

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

A58: for u being Element 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= I

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 = 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}

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

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; :: thesis: verum

end;deffunc H

deffunc H

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 = H

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

now :: thesis: for u being Element 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 Element 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 A57, A58; :: 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 A57, A58; :: thesis: verum

Carrier f c= I

proof

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

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

then consider u being Element of V such that

A59: u = x and

A60: f . u <> 0 ;

f . u = l . u by A57, A58, A60;

then ( Carrier l c= I \/ {v} & u in Carrier l ) by A60, RLVECT_2:def 6;

then ( u in I or u in {v} ) by XBOOLE_0:def 3;

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

end;assume x in Carrier f ; :: thesis: x in I

then consider u being Element of V such that

A59: u = x and

A60: f . u <> 0 ;

f . u = l . u by A57, A58, A60;

then ( Carrier l c= I \/ {v} & u in Carrier l ) by A60, RLVECT_2:def 6;

then ( u in I or u in {v} ) by XBOOLE_0:def 3;

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

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 = H

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

now :: thesis: for u being Element 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 Element 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 A62; :: thesis: verum

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

then u <> v by TARSKI:def 1;

hence g . u = 0 by A62; :: 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 Element of V st

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

then x = v by A62;

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

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

then ex u being Element of V st

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

then x = v by A62;

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

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

now :: thesis: for u being Element of V holds (f - g) . u = l . u

then
f - g = l
;let u be Element of V; :: thesis: (f - g) . u = l . u

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

hence
(f - g) . u = l . u
; :: thesis: verumthen 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; :: thesis: verum

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

Carrier l c= I

hence Carrier l = {} by A55, RLVECT_3:def 1; :: thesis: verum

end;proof

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

assume A68: x in Carrier l ; :: thesis: x in I

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

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

hence x in I by A67, A68, TARSKI:def 1; :: thesis: verum

end;assume A68: x in Carrier l ; :: thesis: x in I

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

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

hence x in I by A67, A68, TARSKI:def 1; :: thesis: verum

hence Carrier l = {} by A55, RLVECT_3:def 1; :: thesis: verum

then I \/ {v} in Q by A3, A52, A54;

hence contradiction by A40, A41, A51, A53, XBOOLE_1:7; :: thesis: verum