let V be finite-dimensional RealLinearSpace; for A being affinely-independent Subset of V holds
( card A = (dim V) + 1 iff Affin A = [#] V )
let A be affinely-independent Subset of V; ( card A = (dim V) + 1 iff Affin A = [#] V )
A1:
0. V in [#] V
;
A2:
A c= Affin A
by RLAFFIN1:49;
hereby ( Affin A = [#] V implies card A = (dim V) + 1 )
assume A3:
card A = (dim V) + 1
;
[#] V = Affin Athen
not
A is
empty
;
then consider v being
VECTOR of
V such that A4:
v in A
and A5:
((- v) + A) \ {(0. V)} is
linearly-independent
by RLAFFIN1:def 4;
set vA =
(- v) + A;
reconsider vA =
(- v) + A as
finite Subset of
V ;
(- v) + v in { ((- v) + w) where w is Element of V : w in A }
by A4;
then A6:
(- v) + v in vA
by RUSUB_4:def 8;
A7:
(
card vA = card A &
card {(0. V)} = 1 )
by CARD_2:42, RLAFFIN1:7;
(- v) + v = 0. V
by RLVECT_1:5;
then
vA = (vA \ {(0. V)}) \/ {(0. V)}
by A6, ZFMISC_1:116;
then A8:
card A = (card (vA \ {(0. V)})) + 1
by A7, CARD_2:40, XBOOLE_1:79;
dim (Lin (vA \ {(0. V)})) = card (vA \ {(0. V)})
by A5, RLVECT_5:29;
then (Omega). V =
(Omega). (Lin (vA \ {(0. V)}))
by A3, A8, RLVECT_5:31
.=
Lin (vA \ {(0. V)})
by RLSUB_1:def 4
;
then
RLSStruct(# the
carrier of
V, the
ZeroF of
V, the
addF of
V, the
Mult of
V #)
= Lin (vA \ {(0. V)})
by RLSUB_1:def 4;
then A9:
[#] V = the
carrier of
(Lin vA)
by Lm2;
then
v in Lin vA
;
hence [#] V =
v + (Lin vA)
by A9, RLSUB_1:48
.=
v + (Up (Lin vA))
by RUSUB_4:30
.=
Affin A
by A2, A4, RLAFFIN1:57
;
verum
end;
assume A10:
Affin A = [#] V
; card A = (dim V) + 1
then
not A is empty
;
then consider v being VECTOR of V such that
A11:
v in A
and
A12:
((- v) + A) \ {(0. V)} is linearly-independent
by RLAFFIN1:def 4;
set vA = (- v) + A;
reconsider vA = (- v) + A as finite Subset of V ;
[#] V =
v + (Up (Lin vA))
by A10, RLAFFIN1:57
.=
v + (Lin vA)
by RUSUB_4:30
;
then [#] (Lin vA) =
the carrier of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
by A1, RLSUB_1:47
.=
the carrier of ((Omega). V)
by RLSUB_1:def 4
;
then Lin vA =
(Omega). V
by RLSUB_1:30
.=
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
by RLSUB_1:def 4
;
then
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) = Lin (vA \ {(0. V)})
by Lm2;
then A13:
vA \ {(0. V)} is Basis of V
by A12, RLVECT_3:def 3;
(- v) + v in { ((- v) + w) where w is Element of V : w in A }
by A11;
then A14:
(- v) + v in vA
by RUSUB_4:def 8;
(- v) + v = 0. V
by RLVECT_1:5;
then A15:
vA = (vA \ {(0. V)}) \/ {(0. V)}
by A14, ZFMISC_1:116;
( card vA = card A & card {(0. V)} = 1 )
by CARD_2:42, RLAFFIN1:7;
hence card A =
(card (vA \ {(0. V)})) + 1
by A15, CARD_2:40, XBOOLE_1:79
.=
(dim V) + 1
by A13, RLVECT_5:def 2
;
verum