let V be free Z_Module; :: 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 & ( for v being Vector of V ex a being Element of INT.Ring st a * v in Lin B ) )

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 & ( for v being Vector of V ex a being Element of INT.Ring st a * v in Lin B ) ) )

assume A1: A is linearly-independent ; :: thesis: ex B being Subset of V st

( A c= B & B is linearly-independent & ( for v being Vector of V ex a being Element of INT.Ring st a * v in Lin B ) )

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

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 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: A c= B and

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

take B ; :: thesis: ( A c= B & B is linearly-independent & ( for v being Vector of V ex a being Element of INT.Ring st a * v in Lin B ) )

thus ( A c= B & B is linearly-independent ) by A37, A38; :: thesis: for v being Vector of V ex a being Element of INT.Ring st a * v in Lin B

assume ex v being Vector of V st

for a being Element of INT.Ring holds not a * v in Lin B ; :: thesis: contradiction

then consider v being Vector of V such that

A39: for a being Element of INT.Ring holds not a * v in Lin B ;

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

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

not (1. INT.Ring) * v in Lin B by A39;

then not v in Lin B by VECTSP_1:def 17;

then A55: not v in B by ZMODUL02:65;

B c= B \/ {v} by XBOOLE_1:7;

then B \/ {v} in Q by A2, A37, A40, XBOOLE_1:1;

hence contradiction by A35, A36, A54, A55, XBOOLE_1:7; :: thesis: verum

ex B being Subset of V st

( A c= B & B is linearly-independent & ( for v being Vector of V ex a being Element of INT.Ring st a * v in Lin B ) )

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 & ( for v being Vector of V ex a being Element of INT.Ring st a * v in Lin B ) ) )

assume A1: A is linearly-independent ; :: thesis: ex B being Subset of V st

( A c= B & B is linearly-independent & ( for v being Vector of V ex a being Element of INT.Ring st a * v in Lin B ) )

defpred S

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

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

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

assume that

A4: Z <> {} and

A5: Z c= Q and

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

set W = union Z;

union Z c= the carrier of V

A9: W is linearly-independent

the Element of Z in Q by A4, A5;

then A33: ex B being Subset of V st

( B = the Element of Z & A c= B & B is linearly-independent ) by A2;

the Element of Z c= W by A4, ZFMISC_1:74;

hence union Z in Q by A2, A9, A33, XBOOLE_1:1; :: thesis: verum

end;assume that

A4: Z <> {} and

A5: Z c= Q and

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

A7: x in X and

A8: X in Z by TARSKI:def 4;

X in bool the carrier of V by A2, A5, A8;

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

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

then consider X being set such that

A7: x in X and

A8: X in Z by TARSKI:def 4;

X in bool the carrier of V by A2, A5, A8;

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

A9: 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 VECTSP_7:def 1 :: thesis: ( not Sum l = 0. V or Carrier l = {} )

assume that

A10: Sum l = 0. V and

A11: Carrier l <> {} ; :: thesis: contradiction

consider f being Function such that

A12: dom f = Carrier l and

A13: 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 A11, A12, 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 A12, FINSET_1:8;

then A20: rng the Choice_Function of M is finite by FINSET_1:8;

then union (rng the Choice_Function of M) in Z by A20, A21, A26, CARD_2:62;

then consider B being Subset of V such that

A27: B = union (rng the Choice_Function of M) and

A c= B and

A28: B is linearly-independent by A2, A5;

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

hence contradiction by A10, A11, A28; :: thesis: verum

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

assume that

A10: Sum l = 0. V and

A11: Carrier l <> {} ; :: thesis: contradiction

consider f being Function such that

A12: dom f = Carrier l and

A13: for x being object st x in Carrier l holds

f . x = H

reconsider M = rng f as non empty set by A11, A12, RELAT_1:42;

set F = the Choice_Function of M;

set S = rng the Choice_Function of M;

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

then A19:
dom the Choice_Function of M = M
by RLVECT_3:28;assume
{} in M
; :: thesis: contradiction

then consider x being object such that

A15: x in dom f and

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

Carrier l c= W by VECTSP_6:def 4;

then consider X being set such that

A17: x in X and

A18: X in Z by A12, A15, TARSKI:def 4;

reconsider X = X as Subset of V by A2, A5, A18;

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

hence contradiction by A12, A13, A15, A16; :: thesis: verum

end;then consider x being object such that

A15: x in dom f and

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

Carrier l c= W by VECTSP_6:def 4;

then consider X being set such that

A17: x in X and

A18: X in Z by A12, A15, TARSKI:def 4;

reconsider X = X as Subset of V by A2, A5, A18;

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

hence contradiction by A12, A13, A15, A16; :: thesis: verum

then dom the Choice_Function of M is finite by A12, FINSET_1:8;

then A20: rng the Choice_Function of M is finite by FINSET_1:8;

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

A22: x in dom the Choice_Function of M and

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

consider y being object such that

A24: ( y in dom f & f . y = x ) by A22, FUNCT_1:def 3;

reconsider x = x as set by TARSKI:1;

A25: x = H_{1}(y)
by A12, A13, A24;

X in x by A14, A22, A23, ORDERS_1:89;

then ex C being Subset of V st

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

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

A22: x in dom the Choice_Function of M and

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

consider y being object such that

A24: ( y in dom f & f . y = x ) by A22, FUNCT_1:def 3;

reconsider x = x as set by TARSKI:1;

A25: x = H

X in x by A14, A22, A23, ORDERS_1:89;

then ex C being Subset of V st

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

hence X in Z ; :: thesis: verum

A26: 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 A19, 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 A21;

hence ( X c= Y or Y c= X ) by A6, ORDINAL1:def 8, XBOOLE_0:def 9; :: 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 A21;

hence ( X c= Y or Y c= X ) by A6, ORDINAL1:def 8, XBOOLE_0:def 9; :: thesis: verum

then union (rng the Choice_Function of M) in Z by A20, A21, A26, CARD_2:62;

then consider B being Subset of V such that

A27: B = union (rng the Choice_Function of M) and

A c= B and

A28: B is linearly-independent by A2, A5;

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

proof

then
l is Linear_Combination of B
by A27, VECTSP_6:def 4;
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 A29: x in Carrier l ; :: thesis: x in union (rng the Choice_Function of M)

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

A31: f . x in M by A12, A29, FUNCT_1:def 3;

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

then A32: ex C being Subset of V st

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

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

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

end;set X = f . x;

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

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

A31: f . x in M by A12, A29, FUNCT_1:def 3;

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

then A32: ex C being Subset of V st

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

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

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

hence contradiction by A10, A11, A28; :: thesis: verum

the Element of Z in Q by A4, A5;

then A33: ex B being Subset of V st

( B = the Element of Z & A c= B & B is linearly-independent ) by A2;

the Element of Z c= W by A4, ZFMISC_1:74;

hence union Z in Q by A2, A9, A33, XBOOLE_1:1; :: thesis: verum

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: A c= B and

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

take B ; :: thesis: ( A c= B & B is linearly-independent & ( for v being Vector of V ex a being Element of INT.Ring st a * v in Lin B ) )

thus ( A c= B & B is linearly-independent ) by A37, A38; :: thesis: for v being Vector of V ex a being Element of INT.Ring st a * v in Lin B

assume ex v being Vector of V st

for a being Element of INT.Ring holds not a * v in Lin B ; :: thesis: contradiction

then consider v being Vector of V such that

A39: for a being Element of INT.Ring holds not a * v in Lin B ;

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

proof

v in {v}
by TARSKI:def 1;
let l be Linear_Combination of B \/ {v}; :: according to VECTSP_7:def 1 :: thesis: ( not Sum l = 0. V or 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 = {}

reconsider i0 = 0 as Element of INT.Ring ;

deffunc H_{1}( Vector of V) -> Element of the carrier of INT.Ring = 0. INT.Ring;

deffunc H_{2}( Vector of V) -> Element of the carrier of INT.Ring = l . $1;

consider f being Function of the carrier of V, the carrier of INT.Ring such that

A42: f . v = i0 and

A43: 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, the carrier of INT.Ring) by FUNCT_2:8;

Carrier f c= B

reconsider lv = - (l . v) as Element of INT.Ring ;

consider g being Function of the carrier of V, the carrier of INT.Ring such that

A47: g . v = lv and

A48: 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, the carrier of INT.Ring) by FUNCT_2:8;

Carrier g c= {v}

A49: Sum g = (- (l . v)) * v by A47, ZMODUL02:21;

f - g = l

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

.= (- (l . v)) * v by A49, RLVECT_1:4 ;

hence Carrier l = {} by A39, ZMODUL02:64; :: thesis: verum

end;deffunc H

deffunc H

consider f being Function of the carrier of V, the carrier of INT.Ring such that

A42: f . v = i0 and

A43: for u being Vector of V st u <> v holds

f . u = H

reconsider f = f as Element of Funcs ( the carrier of V, the carrier of INT.Ring) 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 VECTSP_6:def 1;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 A42, A43; :: 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 A42, A43; :: thesis: verum

Carrier f c= B

proof

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

A44: Carrier l c= B \/ {v} by VECTSP_6:def 4;

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

then consider u being Vector of V such that

A45: u = x and

A46: f . u <> 0 ;

f . u = l . u by A42, A43, A46;

then u in Carrier l by A46;

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

hence x in B by A42, A45, A46, TARSKI:def 1; :: thesis: verum

end;A44: Carrier l c= B \/ {v} by VECTSP_6:def 4;

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

then consider u being Vector of V such that

A45: u = x and

A46: f . u <> 0 ;

f . u = l . u by A42, A43, A46;

then u in Carrier l by A46;

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

hence x in B by A42, A45, A46, TARSKI:def 1; :: thesis: verum

reconsider lv = - (l . v) as Element of INT.Ring ;

consider g being Function of the carrier of V, the carrier of INT.Ring such that

A47: g . v = lv and

A48: for u being Vector of V st u <> v holds

g . u = H

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

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

g . u = 0. INT.Ring

then reconsider g = g as Linear_Combination of V by VECTSP_6:def 1;g . u = 0. INT.Ring

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

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

then u <> v by TARSKI:def 1;

hence g . u = 0. INT.Ring by A48; :: thesis: verum

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

then u <> v by TARSKI:def 1;

hence g . u = 0. INT.Ring by A48; :: thesis: verum

Carrier g c= {v}

proof

then reconsider g = g as Linear_Combination of {v} by VECTSP_6:def 4;
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 A48;

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

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

A49: Sum g = (- (l . v)) * v by A47, ZMODUL02:21;

f - g = l

proof

then
0. V = (Sum f) - (Sum g)
by A41, ZMODUL02:55;
let u be Vector of V; :: according to VECTSP_6:def 7 :: 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 A49, RLVECT_1:4 ;

hence Carrier l = {} by A39, ZMODUL02:64; :: thesis: verum

suppose A52:
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 VECTSP_6:def 4;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier l or x in B )

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

Carrier l c= B \/ {v} by VECTSP_6:def 4;

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

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

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

Carrier l c= B \/ {v} by VECTSP_6:def 4;

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

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

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

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

not (1. INT.Ring) * v in Lin B by A39;

then not v in Lin B by VECTSP_1:def 17;

then A55: not v in B by ZMODUL02:65;

B c= B \/ {v} by XBOOLE_1:7;

then B \/ {v} in Q by A2, A37, A40, XBOOLE_1:1;

hence contradiction by A35, A36, A54, A55, XBOOLE_1:7; :: thesis: verum