let V be finite-dimensional RealLinearSpace; :: thesis: 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; :: thesis: ( card A = (dim V) + 1 iff Affin A = [#] V )

A1: 0. V in [#] V ;

A2: A c= Affin A by RLAFFIN1:49;

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 ;

:: thesis: verum

( card A = (dim V) + 1 iff Affin A = [#] V )

let A be affinely-independent Subset of V; :: thesis: ( card A = (dim V) + 1 iff Affin A = [#] V )

A1: 0. V in [#] V ;

A2: A c= Affin A by RLAFFIN1:49;

hereby :: thesis: ( Affin A = [#] V implies card A = (dim V) + 1 )

assume A10:
Affin A = [#] V
; :: thesis: card A = (dim V) + 1assume A3:
card A = (dim V) + 1
; :: thesis: [#] V = Affin A

then 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 ;

:: thesis: verum

end;then 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 ;

:: thesis: verum

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 ;

:: thesis: verum