let V be RealLinearSpace; 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; ( 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
; card A <= card B
per cases
( A is empty or not A is empty )
;
suppose
not
A is
empty
;
card A <= card Bthen 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))
then reconsider qI =
(- q) + Ib as
finite Subset of
(Lin ((- q) + Ib)) by A7, A10;
(- 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
let x be
object ;
TARSKI:def 3 ( 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
;
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
;
verum
end; then reconsider LA =
Lin ((- p) + A) as
Subspace of
LI by RLVECT_5:19;
(- p) + A c= the
carrier of
LA
then reconsider pA =
(- p) + A as
finite Subset of
LA by A6;
(- 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;
verum end;