let V be RealLinearSpace; 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; ( 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
; B is affinely-independent
per cases
( A is empty or not A is empty )
;
suppose
not
A is
empty
;
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))
then reconsider pA =
(- p) + A as
Subset of
(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))
card pA = n + 1
by Th7;
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;
verum end;