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;
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 ; :: 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
proof
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;
then reconsider TS = T \/ S as finite finite-membered Subset-Family of V ;
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
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;
not T is empty by A10;
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;
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 } )
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