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;

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} )
;

end;

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;hence (I \ {v}) \/ {((center_of_mass V) . Af)} is affinely-independent Subset of V by A3, A4, RLVECT_1:def 8; :: thesis: verum

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})

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

end;proof

I \ {v} is affinely-independent
by RLAFFIN1:43, XBOOLE_1:36;
A9:
not Af \ {v} is empty

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

then
Af \ {v} in dom (center_of_mass V)
by A5, ZFMISC_1:56;
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 c= {v} by XBOOLE_1:37;

hence contradiction by A2, A7, ZFMISC_1:33; :: thesis: verum

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

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