let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for Af being finite Subset of V
for I being affinely-independent Subset of V st Af c= I & v in Af holds
(I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V
let v be VECTOR of V; :: thesis: for Af being finite Subset of V
for I being affinely-independent Subset of V st Af c= I & v in Af holds
(I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V
let Af be finite Subset of V; :: thesis: for I being affinely-independent Subset of V st Af c= I & v in Af holds
(I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V
let I be affinely-independent Subset of V; :: thesis: ( Af c= I & v in Af implies (I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V )
assume that
A1: Af c= I and
A2: v in Af ; :: thesis: (I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V
set Iv = I \ {v};
set Av = Af \ {v};
A3: (I \ {v}) \/ {v} = I by A1, A2, ZFMISC_1:116;
set BA = (center_of_mass V) /. Af;
A4: (center_of_mass V) . Af = (1 / (card Af)) * (Sum Af) by A2, Def2;
A5: dom (center_of_mass V) = BOOL the carrier of V by FUNCT_2:def 1;
then Af in dom (center_of_mass V) by A2, ZFMISC_1:56;
then A6: (center_of_mass V) . Af = (center_of_mass V) /. Af by PARTFUN1:def 6;

per cases ( Af = {v} or Af <> {v} ) ;

suppose Af = {v} ; :: thesis: (I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V

then ( Sum Af = v & card Af = 1 ) by CARD_1:30, RLVECT_2:9;
hence (I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V by A3, A4, RLVECT_1:def 8; :: thesis: verum

end;

suppose A7: Af <> {v} ; :: thesis: (I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V

A8: not (center_of_mass V) /. Af in Affin (I \ {v})

proof

A9: not Af \ {v} is empty

proof

assume Af \ {v} is empty ; :: thesis: contradiction
then Af c= {v} by XBOOLE_1:37;
hence contradiction by A2, A7, ZFMISC_1:33; :: thesis: verum

end;

then Af \ {v} in dom (center_of_mass V) by A5, ZFMISC_1:56;
then A10: (center_of_mass V) . (Af \ {v}) = (center_of_mass V) /. (Af \ {v}) by PARTFUN1:def 6;
Af \ {v} c= I \ {v} by A1, XBOOLE_1:33;
then A11: Affin (Af \ {v}) c= Affin (I \ {v}) by RLAFFIN1:52;
reconsider c = card Af as Real ;
A12: c / c = c * (1 / c) by XCMPLX_1:99;
( conv (Af \ {v}) c= Affin (Af \ {v}) & (center_of_mass V) . (Af \ {v}) in conv (Af \ {v}) ) by A9, Th16, RLAFFIN1:65;
then A13: (center_of_mass V) . (Af \ {v}) in Affin (Af \ {v}) ;
assume (center_of_mass V) /. Af in Affin (I \ {v}) ; :: thesis: contradiction
then A14: ( not v in I \ {v} & ((1 - c) * ((center_of_mass V) /. (Af \ {v}))) + (c * ((center_of_mass V) /. Af)) in Affin (I \ {v}) ) by A10, A11, A13, RUSUB_4:def 4, ZFMISC_1:56;
((center_of_mass V) /. Af) - ((1 - (1 / c)) * ((center_of_mass V) /. (Af \ {v}))) = (((1 - (1 / c)) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / c) * v)) - ((1 - (1 / c)) * ((center_of_mass V) /. (Af \ {v}))) by A2, A6, A9, Th22;
then A15: (1 / c) * v = ((center_of_mass V) /. Af) - ((1 - (1 / c)) * ((center_of_mass V) /. (Af \ {v}))) by RLVECT_4:1
.= ((center_of_mass V) /. Af) + (- ((1 - (1 / c)) * ((center_of_mass V) /. (Af \ {v})))) by RLVECT_1:def 11
.= ((- (1 - (1 / c))) * ((center_of_mass V) /. (Af \ {v}))) + ((center_of_mass V) /. Af) by RLVECT_4:3 ;
A16: 1 = c / c by A2, XCMPLX_1:60;
((1 - c) * ((center_of_mass V) /. (Af \ {v}))) + (c * ((center_of_mass V) /. Af)) = 1 * (((1 - c) * ((center_of_mass V) /. (Af \ {v}))) + (c * ((center_of_mass V) /. Af))) by RLVECT_1:def 8
.= c * ((1 / c) * (((1 - c) * ((center_of_mass V) /. (Af \ {v}))) + (c * ((center_of_mass V) /. Af)))) by A12, A16, RLVECT_1:def 7
.= c * (((1 / c) * ((1 - c) * ((center_of_mass V) /. (Af \ {v})))) + ((1 / c) * (c * ((center_of_mass V) /. Af)))) by RLVECT_1:def 5
.= c * (((1 / c) * ((1 - c) * ((center_of_mass V) /. (Af \ {v})))) + (1 * ((center_of_mass V) /. Af))) by A12, A16, RLVECT_1:def 7
.= c * (((1 / c) * ((1 - c) * ((center_of_mass V) /. (Af \ {v})))) + ((center_of_mass V) /. Af)) by RLVECT_1:def 8
.= c * ((((1 / c) * (1 - c)) * ((center_of_mass V) /. (Af \ {v}))) + ((center_of_mass V) /. Af)) by RLVECT_1:def 7
.= 1 * v by A16, A15, A12, RLVECT_1:def 7
.= v by RLVECT_1:def 8 ;
hence contradiction by A3, A14, Th27; :: thesis: verum

end;

I \ {v} is affinely-independent by RLAFFIN1:43, XBOOLE_1:36;
hence (I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V by A6, A8, Th27; :: thesis: verum

end;

end;