let V be RealLinearSpace; :: thesis: for A, B being finite Subset of V st A is affinely-independent & Affin A = Affin B & card B <= card A holds

B is affinely-independent

let A, B be finite Subset of V; :: thesis: ( A is affinely-independent & Affin A = Affin B & card B <= card A implies B is affinely-independent )

assume that

A1: A is affinely-independent and

A2: Affin A = Affin B and

A3: card B <= card A ; :: thesis: B is affinely-independent

B is affinely-independent

let A, B be finite Subset of V; :: thesis: ( A is affinely-independent & Affin A = Affin B & card B <= card A implies B is affinely-independent )

assume that

A1: A is affinely-independent and

A2: Affin A = Affin B and

A3: card B <= card A ; :: thesis: B is affinely-independent

per cases
( A is empty or not A is empty )
;

end;

suppose
not A is empty
; :: thesis: B is affinely-independent

then consider p being object such that

A4: p in A ;

card A > 0 by A4;

then reconsider n = (card A) - 1 as Element of NAT by NAT_1:20;

A5: A c= Affin A by Lm7;

reconsider p = p as Element of V by A4;

set L = Lin ((- p) + A);

{} V c= B ;

then consider Ia being affinely-independent Subset of V such that

{} V c= Ia and

A6: Ia c= B and

A7: Affin Ia = Affin B by Th60;

not Ia is empty by A2, A4, A7;

then consider q being object such that

A8: q in Ia ;

(- p) + A c= [#] (Lin ((- p) + A))

((- p) + A) \ {(0. V)} is linearly-independent by A1, A4, Th41;

then A9: pA \ {(0. V)} is linearly-independent by RLVECT_5:15;

(- p) + p = 0. V by RLVECT_1:5;

then A10: 0. V in pA by A4;

then Lin ((- p) + A) = Lin ((((- p) + A) \ {(0. V)}) \/ {(0. V)}) by ZFMISC_1:116

.= Lin (((- p) + A) \ {(0. V)}) by Lm9

.= Lin (pA \ {(0. V)}) by RLVECT_5:20 ;

then A11: pA \ {(0. V)} is Basis of Lin ((- p) + A) by A9, RLVECT_3:def 3;

reconsider IA = Ia as finite set by A6;

A12: Ia c= Affin Ia by Lm7;

reconsider q = q as Element of V by A8;

p + (Lin ((- p) + A)) = p + (Up (Lin ((- p) + A))) by RUSUB_4:30

.= Affin A by A4, A5, Th57

.= q + (Up (Lin ((- q) + Ia))) by A2, A7, A8, A12, Th57

.= q + (Lin ((- q) + Ia)) by RUSUB_4:30 ;

then A13: Lin ((- p) + A) = Lin ((- q) + Ia) by RLSUB_1:69;

set qI = (- q) + Ia;

A14: (- q) + Ia c= [#] (Lin ((- q) + Ia))

then A15: card (pA \ {(0. V)}) = n by A10, STIRL2_1:55;

then pA \ {(0. V)} is finite ;

then A16: Lin ((- p) + A) is finite-dimensional by A11, RLVECT_5:def 1;

reconsider qI = (- q) + Ia as Subset of (Lin ((- q) + Ia)) by A14;

((- q) + Ia) \ {(0. V)} is linearly-independent by A8, Th41;

then A17: qI \ {(0. V)} is linearly-independent by RLVECT_5:15;

(- q) + q = 0. V by RLVECT_1:5;

then A18: 0. V in qI by A8;

then Lin ((- q) + Ia) = Lin ((((- q) + Ia) \ {(0. V)}) \/ {(0. V)}) by ZFMISC_1:116

.= Lin (((- q) + Ia) \ {(0. V)}) by Lm9

.= Lin (qI \ {(0. V)}) by RLVECT_5:20 ;

then qI \ {(0. V)} is Basis of Lin ((- q) + Ia) by A17, RLVECT_3:def 3;

then A19: card (qI \ {(0. V)}) = n by A11, A13, A15, A16, RLVECT_5:25;

then ( not 0. V in qI \ {(0. V)} & qI \ {(0. V)} is finite ) by ZFMISC_1:56;

then A20: n + 1 = card ((qI \ {(0. V)}) \/ {(0. V)}) by A19, CARD_2:41

.= card qI by A18, ZFMISC_1:116

.= card Ia by Th7 ;

card IA <= card B by A6, NAT_1:43;

hence B is affinely-independent by A3, A6, A20, CARD_2:102, XXREAL_0:1; :: thesis: verum

end;A4: p in A ;

card A > 0 by A4;

then reconsider n = (card A) - 1 as Element of NAT by NAT_1:20;

A5: A c= Affin A by Lm7;

reconsider p = p as Element of V by A4;

set L = Lin ((- p) + A);

{} V c= B ;

then consider Ia being affinely-independent Subset of V such that

{} V c= Ia and

A6: Ia c= B and

A7: Affin Ia = Affin B by Th60;

not Ia is empty by A2, A4, A7;

then consider q being object such that

A8: q in Ia ;

(- p) + A c= [#] (Lin ((- p) + A))

proof

then reconsider pA = (- p) + A as Subset of (Lin ((- p) + A)) ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (- p) + A or x in [#] (Lin ((- p) + A)) )

assume x in (- p) + A ; :: thesis: x in [#] (Lin ((- p) + A))

then x in Lin ((- p) + A) by RLVECT_3:15;

hence x in [#] (Lin ((- p) + A)) ; :: thesis: verum

end;assume x in (- p) + A ; :: thesis: x in [#] (Lin ((- p) + A))

then x in Lin ((- p) + A) by RLVECT_3:15;

hence x in [#] (Lin ((- p) + A)) ; :: thesis: verum

((- p) + A) \ {(0. V)} is linearly-independent by A1, A4, Th41;

then A9: pA \ {(0. V)} is linearly-independent by RLVECT_5:15;

(- p) + p = 0. V by RLVECT_1:5;

then A10: 0. V in pA by A4;

then Lin ((- p) + A) = Lin ((((- p) + A) \ {(0. V)}) \/ {(0. V)}) by ZFMISC_1:116

.= Lin (((- p) + A) \ {(0. V)}) by Lm9

.= Lin (pA \ {(0. V)}) by RLVECT_5:20 ;

then A11: pA \ {(0. V)} is Basis of Lin ((- p) + A) by A9, RLVECT_3:def 3;

reconsider IA = Ia as finite set by A6;

A12: Ia c= Affin Ia by Lm7;

reconsider q = q as Element of V by A8;

p + (Lin ((- p) + A)) = p + (Up (Lin ((- p) + A))) by RUSUB_4:30

.= Affin A by A4, A5, Th57

.= q + (Up (Lin ((- q) + Ia))) by A2, A7, A8, A12, Th57

.= q + (Lin ((- q) + Ia)) by RUSUB_4:30 ;

then A13: Lin ((- p) + A) = Lin ((- q) + Ia) by RLSUB_1:69;

set qI = (- q) + Ia;

A14: (- q) + Ia c= [#] (Lin ((- q) + Ia))

proof

card pA = n + 1
by Th7;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (- q) + Ia or x in [#] (Lin ((- q) + Ia)) )

assume x in (- q) + Ia ; :: thesis: x in [#] (Lin ((- q) + Ia))

then x in Lin ((- q) + Ia) by RLVECT_3:15;

hence x in [#] (Lin ((- q) + Ia)) ; :: thesis: verum

end;assume x in (- q) + Ia ; :: thesis: x in [#] (Lin ((- q) + Ia))

then x in Lin ((- q) + Ia) by RLVECT_3:15;

hence x in [#] (Lin ((- q) + Ia)) ; :: thesis: verum

then A15: card (pA \ {(0. V)}) = n by A10, STIRL2_1:55;

then pA \ {(0. V)} is finite ;

then A16: Lin ((- p) + A) is finite-dimensional by A11, RLVECT_5:def 1;

reconsider qI = (- q) + Ia as Subset of (Lin ((- q) + Ia)) by A14;

((- q) + Ia) \ {(0. V)} is linearly-independent by A8, Th41;

then A17: qI \ {(0. V)} is linearly-independent by RLVECT_5:15;

(- q) + q = 0. V by RLVECT_1:5;

then A18: 0. V in qI by A8;

then Lin ((- q) + Ia) = Lin ((((- q) + Ia) \ {(0. V)}) \/ {(0. V)}) by ZFMISC_1:116

.= Lin (((- q) + Ia) \ {(0. V)}) by Lm9

.= Lin (qI \ {(0. V)}) by RLVECT_5:20 ;

then qI \ {(0. V)} is Basis of Lin ((- q) + Ia) by A17, RLVECT_3:def 3;

then A19: card (qI \ {(0. V)}) = n by A11, A13, A15, A16, RLVECT_5:25;

then ( not 0. V in qI \ {(0. V)} & qI \ {(0. V)} is finite ) by ZFMISC_1:56;

then A20: n + 1 = card ((qI \ {(0. V)}) \/ {(0. V)}) by A19, CARD_2:41

.= card qI by A18, ZFMISC_1:116

.= card Ia by Th7 ;

card IA <= card B by A6, NAT_1:43;

hence B is affinely-independent by A3, A6, A20, CARD_2:102, XXREAL_0:1; :: thesis: verum