let V be RealLinearSpace; :: thesis: for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & card Sf = card (union Sf) holds

for v being Element of V st not v in union Sf & (union Sf) \/ {v} is affinely-independent holds

{ S1 where S1 is Simplex of card Sf, BCS (Complex_of {((union Sf) \/ {v})}) : (center_of_mass V) .: Sf c= S1 } = {(((center_of_mass V) .: Sf) \/ ((center_of_mass V) .: {((union Sf) \/ {v})}))}

let S be c=-linear finite finite-membered Subset-Family of V; :: thesis: ( S is with_non-empty_elements & card S = card (union S) implies for v being Element of V st not v in union S & (union S) \/ {v} is affinely-independent holds

{ S1 where S1 is Simplex of card S, BCS (Complex_of {((union S) \/ {v})}) : (center_of_mass V) .: S c= S1 } = {(((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ {v})}))} )

assume that

A1: S is with_non-empty_elements and

A2: card S = card (union S) ; :: thesis: for v being Element of V st not v in union S & (union S) \/ {v} is affinely-independent holds

{ S1 where S1 is Simplex of card S, BCS (Complex_of {((union S) \/ {v})}) : (center_of_mass V) .: S c= S1 } = {(((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ {v})}))}

set U = union S;

set B = center_of_mass V;

let v be Element of V; :: thesis: ( not v in union S & (union S) \/ {v} is affinely-independent implies { S1 where S1 is Simplex of card S, BCS (Complex_of {((union S) \/ {v})}) : (center_of_mass V) .: S c= S1 } = {(((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ {v})}))} )

assume that

A3: not v in union S and

A4: (union S) \/ {v} is affinely-independent ; :: thesis: { S1 where S1 is Simplex of card S, BCS (Complex_of {((union S) \/ {v})}) : (center_of_mass V) .: S c= S1 } = {(((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ {v})}))}

reconsider Uv = (union S) \/ {v} as finite affinely-independent Subset of V by A4;

set CUv = Complex_of {Uv};

set BC = BCS (Complex_of {Uv});

set SS = { S1 where S1 is Simplex of card S, BCS (Complex_of {((union S) \/ {v})}) : (center_of_mass V) .: S c= S1 } ;

set TT = {(((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ {v})}))};

A5: union S c= Uv by XBOOLE_1:7;

assume x in {(((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ {v})}))} ; :: thesis: x in { S1 where S1 is Simplex of card S, BCS (Complex_of {((union S) \/ {v})}) : (center_of_mass V) .: S c= S1 }

then A21: x = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {Uv}) by TARSKI:def 1;

( (center_of_mass V) .: S c= ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {Uv}) & ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {Uv}) is Simplex of card S, BCS (Complex_of {Uv}) ) by A1, A2, A3, Th37, XBOOLE_1:7, ZFMISC_1:50;

hence x in { S1 where S1 is Simplex of card S, BCS (Complex_of {((union S) \/ {v})}) : (center_of_mass V) .: S c= S1 } by A21; :: thesis: verum

for v being Element of V st not v in union Sf & (union Sf) \/ {v} is affinely-independent holds

{ S1 where S1 is Simplex of card Sf, BCS (Complex_of {((union Sf) \/ {v})}) : (center_of_mass V) .: Sf c= S1 } = {(((center_of_mass V) .: Sf) \/ ((center_of_mass V) .: {((union Sf) \/ {v})}))}

let S be c=-linear finite finite-membered Subset-Family of V; :: thesis: ( S is with_non-empty_elements & card S = card (union S) implies for v being Element of V st not v in union S & (union S) \/ {v} is affinely-independent holds

{ S1 where S1 is Simplex of card S, BCS (Complex_of {((union S) \/ {v})}) : (center_of_mass V) .: S c= S1 } = {(((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ {v})}))} )

assume that

A1: S is with_non-empty_elements and

A2: card S = card (union S) ; :: thesis: for v being Element of V st not v in union S & (union S) \/ {v} is affinely-independent holds

{ S1 where S1 is Simplex of card S, BCS (Complex_of {((union S) \/ {v})}) : (center_of_mass V) .: S c= S1 } = {(((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ {v})}))}

set U = union S;

set B = center_of_mass V;

let v be Element of V; :: thesis: ( not v in union S & (union S) \/ {v} is affinely-independent implies { S1 where S1 is Simplex of card S, BCS (Complex_of {((union S) \/ {v})}) : (center_of_mass V) .: S c= S1 } = {(((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ {v})}))} )

assume that

A3: not v in union S and

A4: (union S) \/ {v} is affinely-independent ; :: thesis: { S1 where S1 is Simplex of card S, BCS (Complex_of {((union S) \/ {v})}) : (center_of_mass V) .: S c= S1 } = {(((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ {v})}))}

reconsider Uv = (union S) \/ {v} as finite affinely-independent Subset of V by A4;

set CUv = Complex_of {Uv};

set BC = BCS (Complex_of {Uv});

set SS = { S1 where S1 is Simplex of card S, BCS (Complex_of {((union S) \/ {v})}) : (center_of_mass V) .: S c= S1 } ;

set TT = {(((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ {v})}))};

A5: union S c= Uv by XBOOLE_1:7;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ {v})}))} c= { S1 where S1 is Simplex of card S, BCS (Complex_of {((union S) \/ {v})}) : (center_of_mass V) .: S c= S1 }

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ {v})}))} or x in { S1 where S1 is Simplex of card S, BCS (Complex_of {((union S) \/ {v})}) : (center_of_mass V) .: S c= S1 } )let x be object ; :: thesis: ( x in { S1 where S1 is Simplex of card S, BCS (Complex_of {((union S) \/ {v})}) : (center_of_mass V) .: S c= S1 } implies x in {(((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ {v})}))} )

reconsider n = 0 as Nat ;

assume x in { S1 where S1 is Simplex of card S, BCS (Complex_of {((union S) \/ {v})}) : (center_of_mass V) .: S c= S1 } ; :: thesis: x in {(((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ {v})}))}

then consider S1 being Simplex of card S, BCS (Complex_of {Uv}) such that

A6: x = S1 and

A7: (center_of_mass V) .: S c= S1 ;

((card S) + n) + 1 <= card Uv by A2, A3, CARD_2:41;

then consider T being finite Subset-Family of V such that

A8: T misses S and

A9: ( T \/ S is c=-linear & T \/ S is with_non-empty_elements ) and

A10: card T = n + 1 and

A11: union T c= Uv and

A12: @ S1 = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) by A1, A5, A7, Th35;

A13: ex x being object st T = {x} by A10, CARD_2:42;

A14: union (T \/ S) = (union T) \/ (union S) by ZFMISC_1:78;

T \/ S is finite-membered

union (T \/ S) c= Uv by A5, A11, A14, XBOOLE_1:8;

then A15: card (union TS) c= card Uv by CARD_1:11;

card TS = (card S) + 1 by A8, A10, CARD_2:40;

then A16: card TS = card Uv by A2, A3, CARD_2:41;

card TS c= card (union TS) by A9, SIMPLEX0:10;

then card (union TS) = card TS by A15, A16;

then A17: union TS = Uv by A5, A11, A14, A16, CARD_2:102, XBOOLE_1:8;

A18: union S c= union (T \/ S) by A14, XBOOLE_1:7;

A19: not union TS in S

then union TS in TS by A9, SIMPLEX0:9;

then union TS in T by A19, XBOOLE_0:def 3;

then T = {Uv} by A13, A17, TARSKI:def 1;

hence x in {(((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ {v})}))} by A6, A12, TARSKI:def 1; :: thesis: verum

end;reconsider n = 0 as Nat ;

assume x in { S1 where S1 is Simplex of card S, BCS (Complex_of {((union S) \/ {v})}) : (center_of_mass V) .: S c= S1 } ; :: thesis: x in {(((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ {v})}))}

then consider S1 being Simplex of card S, BCS (Complex_of {Uv}) such that

A6: x = S1 and

A7: (center_of_mass V) .: S c= S1 ;

((card S) + n) + 1 <= card Uv by A2, A3, CARD_2:41;

then consider T being finite Subset-Family of V such that

A8: T misses S and

A9: ( T \/ S is c=-linear & T \/ S is with_non-empty_elements ) and

A10: card T = n + 1 and

A11: union T c= Uv and

A12: @ S1 = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) by A1, A5, A7, Th35;

A13: ex x being object st T = {x} by A10, CARD_2:42;

A14: union (T \/ S) = (union T) \/ (union S) by ZFMISC_1:78;

T \/ S is finite-membered

proof

then reconsider TS = T \/ S as finite finite-membered Subset-Family of V ;
let x be set ; :: according to FINSET_1:def 6 :: thesis: ( not x in T \/ S or x is finite )

assume x in T \/ S ; :: thesis: x is finite

then x c= union (T \/ S) by ZFMISC_1:74;

hence x is finite by A11, A14; :: thesis: verum

end;assume x in T \/ S ; :: thesis: x is finite

then x c= union (T \/ S) by ZFMISC_1:74;

hence x is finite by A11, A14; :: thesis: verum

union (T \/ S) c= Uv by A5, A11, A14, XBOOLE_1:8;

then A15: card (union TS) c= card Uv by CARD_1:11;

card TS = (card S) + 1 by A8, A10, CARD_2:40;

then A16: card TS = card Uv by A2, A3, CARD_2:41;

card TS c= card (union TS) by A9, SIMPLEX0:10;

then card (union TS) = card TS by A15, A16;

then A17: union TS = Uv by A5, A11, A14, A16, CARD_2:102, XBOOLE_1:8;

A18: union S c= union (T \/ S) by A14, XBOOLE_1:7;

A19: not union TS in S

proof

not T is empty
by A10;
assume
union TS in S
; :: thesis: contradiction

then union TS c= union S by ZFMISC_1:74;

then A20: union S = Uv by A17, A18;

v in {v} by TARSKI:def 1;

hence contradiction by A3, A20, XBOOLE_0:def 3; :: thesis: verum

end;then union TS c= union S by ZFMISC_1:74;

then A20: union S = Uv by A17, A18;

v in {v} by TARSKI:def 1;

hence contradiction by A3, A20, XBOOLE_0:def 3; :: thesis: verum

then union TS in TS by A9, SIMPLEX0:9;

then union TS in T by A19, XBOOLE_0:def 3;

then T = {Uv} by A13, A17, TARSKI:def 1;

hence x in {(((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ {v})}))} by A6, A12, TARSKI:def 1; :: thesis: verum

assume x in {(((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ {v})}))} ; :: thesis: x in { S1 where S1 is Simplex of card S, BCS (Complex_of {((union S) \/ {v})}) : (center_of_mass V) .: S c= S1 }

then A21: x = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {Uv}) by TARSKI:def 1;

( (center_of_mass V) .: S c= ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {Uv}) & ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {Uv}) is Simplex of card S, BCS (Complex_of {Uv}) ) by A1, A2, A3, Th37, XBOOLE_1:7, ZFMISC_1:50;

hence x in { S1 where S1 is Simplex of card S, BCS (Complex_of {((union S) \/ {v})}) : (center_of_mass V) .: S c= S1 } by A21; :: thesis: verum