let V be RealLinearSpace; :: thesis: 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; :: thesis: ( 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 S_{1}[ 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 & S_{1}[Z] ) )
from XFAMILY:sch 1();

assume A is linearly-independent ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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 #) ; :: thesis: 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

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

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; :: thesis: ( 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 S

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

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

union Z in Q

A33:
(Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #)
;union Z in Q

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

set W = union Z;

union Z c= the carrier of V

A8: W is linearly-independent

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

end;assume that

A3: 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 A1, 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 A1, A4, A7;

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

A8: W is linearly-independent

proof

set x = the Element of Z;
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

A c= B and

A27: B is linearly-independent by A1, 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 A1, 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 A1, 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 = H_{1}(y)
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 = H

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

A c= B and

A27: B is linearly-independent by A1, 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

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

assume A is linearly-independent ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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 #) ; :: thesis: 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

v in {v}
by TARSKI:def 1;
let l be Linear_Combination of B \/ {v}; :: according to RLVECT_3:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )

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

end;assume A41: 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 A42:
- (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

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

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

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

A49: 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}

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

f - g = l

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

end;deffunc H

deffunc H

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 = 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 A43, A44; :: 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 A43, A44; :: 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 )

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

A46: u = x and

A47: f . u <> 0 ;

f . u = l . u by A43, A44, A47;

then u in Carrier l by A47;

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

hence x in B by A43, A46, A47, TARSKI:def 1; :: thesis: verum

end;A45: 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

A46: u = x and

A47: f . u <> 0 ;

f . u = l . u by A43, A44, A47;

then u in Carrier l by A47;

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

hence x in B by A43, A46, A47, TARSKI:def 1; :: thesis: verum

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

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

then u <> v by TARSKI:def 1;

hence g . u = 0 by A49; :: 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 A49;

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 A49;

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

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

f - g = l

proof

then
0. V = (Sum f) - (Sum g)
by A41, 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 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; :: thesis: verum

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

Carrier l c= B

hence Carrier l = {} by A38, A41; :: 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 A55: 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 A55, XBOOLE_0:def 3;

hence x in B by A54, A55, TARSKI:def 1; :: thesis: verum

end;assume A55: 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 A55, XBOOLE_0:def 3;

hence x in B by A54, A55, TARSKI:def 1; :: thesis: verum

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

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