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

card A <= card B

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

assume that

A1: A is affinely-independent and

A2: Affin A c= Affin B ; :: thesis: card A <= card B

card A <= card B

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

assume that

A1: A is affinely-independent and

A2: Affin A c= Affin B ; :: thesis: card A <= card B

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

end;

suppose
not A is empty
; :: thesis: card A <= card B

then consider p being object such that

A3: p in A ;

reconsider p = p as Element of V by A3;

A4: A c= Affin A by Lm7;

then A5: p in Affin A by A3;

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

A6: card A = card ((- p) + A) by Th7;

{} V c= B ;

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

{} V c= Ib and

A7: Ib c= B and

A8: Affin Ib = Affin B by Th60;

not Ib is empty by A2, A3, A8;

then consider q being object such that

A9: q in Ib ;

reconsider q = q as Element of V by A9;

set LI = Lin ((- q) + Ib);

A10: card Ib = card ((- q) + Ib) by Th7;

(- q) + Ib c= the carrier of (Lin ((- q) + Ib))

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

then A11: 0. V in qI by A9;

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

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

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

A13: ((- q) + Ib) \ {(0. V)} is linearly-independent by A9, Th41;

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

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

then reconsider LI = Lin ((- q) + Ib) as finite-dimensional Subspace of V by RLVECT_5:def 1;

A14: Ib c= Affin Ib by Lm7;

then A15: Affin Ib = q + (Up LI) by A9, Th57;

A16: Affin A = p + (Up (Lin ((- p) + A))) by A3, A4, Th57;

(- p) + A c= the carrier of LI

(- p) + A c= the carrier of LA

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

then A23: 0. V in pA by A3;

then A24: {(0. V)} c= pA by ZFMISC_1:31;

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

A26: card {(0. V)} = 1 by CARD_1:30;

A27: {(0. V)} c= qI by A11, ZFMISC_1:31;

A28: dim LI = card (qI \ {(0. V)}) by A13, A12, RLVECT_5:15, RLVECT_5:29

.= (card qI) - 1 by A27, A26, CARD_2:44 ;

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

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

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

then dim LA = card (pA \ {(0. V)}) by A25, RLVECT_5:15, RLVECT_5:29

.= (card A) - 1 by A6, A26, A24, CARD_2:44 ;

then (card A) - 1 <= (card qI) - 1 by A28, RLVECT_5:28;

then A29: card A <= card qI by XREAL_1:9;

card qI <= card B by A7, A10, NAT_1:43;

hence card A <= card B by A29, XXREAL_0:2; :: thesis: verum

end;A3: p in A ;

reconsider p = p as Element of V by A3;

A4: A c= Affin A by Lm7;

then A5: p in Affin A by A3;

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

A6: card A = card ((- p) + A) by Th7;

{} V c= B ;

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

{} V c= Ib and

A7: Ib c= B and

A8: Affin Ib = Affin B by Th60;

not Ib is empty by A2, A3, A8;

then consider q being object such that

A9: q in Ib ;

reconsider q = q as Element of V by A9;

set LI = Lin ((- q) + Ib);

A10: card Ib = card ((- q) + Ib) by Th7;

(- q) + Ib c= the carrier of (Lin ((- q) + Ib))

proof

then reconsider qI = (- q) + Ib as finite Subset of (Lin ((- q) + Ib)) by A7, A10;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (- q) + Ib or x in the carrier of (Lin ((- q) + Ib)) )

assume x in (- q) + Ib ; :: thesis: x in the carrier of (Lin ((- q) + Ib))

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

hence x in the carrier of (Lin ((- q) + Ib)) ; :: thesis: verum

end;assume x in (- q) + Ib ; :: thesis: x in the carrier of (Lin ((- q) + Ib))

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

hence x in the carrier of (Lin ((- q) + Ib)) ; :: thesis: verum

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

then A11: 0. V in qI by A9;

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

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

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

A13: ((- q) + Ib) \ {(0. V)} is linearly-independent by A9, Th41;

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

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

then reconsider LI = Lin ((- q) + Ib) as finite-dimensional Subspace of V by RLVECT_5:def 1;

A14: Ib c= Affin Ib by Lm7;

then A15: Affin Ib = q + (Up LI) by A9, Th57;

A16: Affin A = p + (Up (Lin ((- p) + A))) by A3, A4, Th57;

(- p) + A c= the carrier of LI

proof

then reconsider LA = Lin ((- p) + A) as Subspace of LI by RLVECT_5:19;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (- p) + A or x in the carrier of LI )

A17: 2 + (- 1) = 1 ;

(2 * q) + ((- 1) * p) = ((1 + 1) * q) + ((- 1) * p)

.= ((1 * q) + (1 * q)) + ((- 1) * p) by RLVECT_1:def 6

.= ((1 * q) + (1 * q)) + (- p) by RLVECT_1:16

.= ((1 * q) + q) + (- p) by RLVECT_1:def 8

.= (q + q) + (- p) by RLVECT_1:def 8

.= (q + q) - p by RLVECT_1:def 11

.= (q - p) + q by RLVECT_1:28 ;

then ( q + (Up LI) = q + LI & (q - p) + q in q + (Up LI) ) by A2, A8, A5, A9, A14, A15, A17, Th78, RUSUB_4:30;

then A18: q - p in LI by RLSUB_1:61;

assume x in (- p) + A ; :: thesis: x in the carrier of LI

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

then x in V by RLSUB_1:9;

then reconsider w = x as Element of V ;

w in Up (Lin ((- p) + A)) by A19;

then p + w in Affin A by A16;

then p + w in q + (Up LI) by A2, A8, A15;

then consider u being Element of V such that

A20: p + w = q + u and

A21: u in Up LI ;

A22: w = (q + u) - p by A20, RLVECT_4:1

.= q + (u - p) by RLVECT_1:28

.= u - (p - q) by RLVECT_1:29

.= u + (- (p - q)) by RLVECT_1:def 11

.= u + (q + (- p)) by RLVECT_1:33

.= u + (q - p) by RLVECT_1:def 11 ;

u in LI by A21;

then w in LI by A18, A22, RLSUB_1:20;

hence x in the carrier of LI ; :: thesis: verum

end;A17: 2 + (- 1) = 1 ;

(2 * q) + ((- 1) * p) = ((1 + 1) * q) + ((- 1) * p)

.= ((1 * q) + (1 * q)) + ((- 1) * p) by RLVECT_1:def 6

.= ((1 * q) + (1 * q)) + (- p) by RLVECT_1:16

.= ((1 * q) + q) + (- p) by RLVECT_1:def 8

.= (q + q) + (- p) by RLVECT_1:def 8

.= (q + q) - p by RLVECT_1:def 11

.= (q - p) + q by RLVECT_1:28 ;

then ( q + (Up LI) = q + LI & (q - p) + q in q + (Up LI) ) by A2, A8, A5, A9, A14, A15, A17, Th78, RUSUB_4:30;

then A18: q - p in LI by RLSUB_1:61;

assume x in (- p) + A ; :: thesis: x in the carrier of LI

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

then x in V by RLSUB_1:9;

then reconsider w = x as Element of V ;

w in Up (Lin ((- p) + A)) by A19;

then p + w in Affin A by A16;

then p + w in q + (Up LI) by A2, A8, A15;

then consider u being Element of V such that

A20: p + w = q + u and

A21: u in Up LI ;

A22: w = (q + u) - p by A20, RLVECT_4:1

.= q + (u - p) by RLVECT_1:28

.= u - (p - q) by RLVECT_1:29

.= u + (- (p - q)) by RLVECT_1:def 11

.= u + (q + (- p)) by RLVECT_1:33

.= u + (q - p) by RLVECT_1:def 11 ;

u in LI by A21;

then w in LI by A18, A22, RLSUB_1:20;

hence x in the carrier of LI ; :: thesis: verum

(- p) + A c= the carrier of LA

proof

then reconsider pA = (- p) + A as finite Subset of LA by A6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (- p) + A or x in the carrier of LA )

assume x in (- p) + A ; :: thesis: x in the carrier of LA

then x in LA by RLVECT_3:15;

hence x in the carrier of LA ; :: thesis: verum

end;assume x in (- p) + A ; :: thesis: x in the carrier of LA

then x in LA by RLVECT_3:15;

hence x in the carrier of LA ; :: thesis: verum

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

then A23: 0. V in pA by A3;

then A24: {(0. V)} c= pA by ZFMISC_1:31;

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

A26: card {(0. V)} = 1 by CARD_1:30;

A27: {(0. V)} c= qI by A11, ZFMISC_1:31;

A28: dim LI = card (qI \ {(0. V)}) by A13, A12, RLVECT_5:15, RLVECT_5:29

.= (card qI) - 1 by A27, A26, CARD_2:44 ;

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

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

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

then dim LA = card (pA \ {(0. V)}) by A25, RLVECT_5:15, RLVECT_5:29

.= (card A) - 1 by A6, A26, A24, CARD_2:44 ;

then (card A) - 1 <= (card qI) - 1 by A28, RLVECT_5:28;

then A29: card A <= card qI by XREAL_1:9;

card qI <= card B by A7, A10, NAT_1:43;

hence card A <= card B by A29, XXREAL_0:2; :: thesis: verum