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

for Af, Bf being finite Subset of V st not Af is empty & Af misses union S & (union S) \/ Af is affinely-independent & (union S) \/ Af c= Bf holds

((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ Af)}) is Simplex of card S, BCS (Complex_of {Bf})

let S be finite Subset-Family of V; :: thesis: ( S is c=-linear & S is with_non-empty_elements & card S = card (union S) implies for Af, Bf being finite Subset of V st not Af is empty & Af misses union S & (union S) \/ Af is affinely-independent & (union S) \/ Af c= Bf holds

((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ Af)}) is Simplex of card S, BCS (Complex_of {Bf}) )

assume that

A1: ( S is c=-linear & S is with_non-empty_elements ) and

A2: card S = card (union S) ; :: thesis: for Af, Bf being finite Subset of V st not Af is empty & Af misses union S & (union S) \/ Af is affinely-independent & (union S) \/ Af c= Bf holds

((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ Af)}) is Simplex of card S, BCS (Complex_of {Bf})

set U = union S;

set b = center_of_mass V;

let A, B be finite Subset of V; :: thesis: ( not A is empty & A misses union S & (union S) \/ A is affinely-independent & (union S) \/ A c= B implies ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {B}) )

assume that

A3: not A is empty and

A4: ( A misses union S & (union S) \/ A is affinely-independent ) and

A5: (union S) \/ A c= B ; :: thesis: ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {B})

reconsider UA = (union S) \/ A as finite Subset of V by A5;

dom (center_of_mass V) = (bool the carrier of V) \ {{}} by FUNCT_2:def 1;

then UA in dom (center_of_mass V) by A3, ZFMISC_1:56;

then A6: {((center_of_mass V) . UA)} = Im ((center_of_mass V),UA) by FUNCT_1:59

.= (center_of_mass V) .: {UA} by RELAT_1:def 16 ;

set CA = Complex_of {UA};

set CB = Complex_of {B};

{UA} is_finer_than {B}

then A8: subdivision ((center_of_mass V),(Complex_of {UA})) is SubSimplicialComplex of subdivision ((center_of_mass V),(Complex_of {B})) by SIMPLEX0:58;

|.(Complex_of {UA}).| c= [#] (Complex_of {UA}) ;

then A9: subdivision ((center_of_mass V),(Complex_of {UA})) = BCS (Complex_of {UA}) by Def5;

|.(Complex_of {B}).| c= [#] (Complex_of {B}) ;

then A10: BCS (Complex_of {UA}) is SubSimplicialComplex of BCS (Complex_of {B}) by A8, A9, Def5;

S is finite-membered

hence ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {B}) by A6, A10, SIMPLEX0:49; :: thesis: verum

for Af, Bf being finite Subset of V st not Af is empty & Af misses union S & (union S) \/ Af is affinely-independent & (union S) \/ Af c= Bf holds

((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ Af)}) is Simplex of card S, BCS (Complex_of {Bf})

let S be finite Subset-Family of V; :: thesis: ( S is c=-linear & S is with_non-empty_elements & card S = card (union S) implies for Af, Bf being finite Subset of V st not Af is empty & Af misses union S & (union S) \/ Af is affinely-independent & (union S) \/ Af c= Bf holds

((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ Af)}) is Simplex of card S, BCS (Complex_of {Bf}) )

assume that

A1: ( S is c=-linear & S is with_non-empty_elements ) and

A2: card S = card (union S) ; :: thesis: for Af, Bf being finite Subset of V st not Af is empty & Af misses union S & (union S) \/ Af is affinely-independent & (union S) \/ Af c= Bf holds

((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ Af)}) is Simplex of card S, BCS (Complex_of {Bf})

set U = union S;

set b = center_of_mass V;

let A, B be finite Subset of V; :: thesis: ( not A is empty & A misses union S & (union S) \/ A is affinely-independent & (union S) \/ A c= B implies ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {B}) )

assume that

A3: not A is empty and

A4: ( A misses union S & (union S) \/ A is affinely-independent ) and

A5: (union S) \/ A c= B ; :: thesis: ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {B})

reconsider UA = (union S) \/ A as finite Subset of V by A5;

dom (center_of_mass V) = (bool the carrier of V) \ {{}} by FUNCT_2:def 1;

then UA in dom (center_of_mass V) by A3, ZFMISC_1:56;

then A6: {((center_of_mass V) . UA)} = Im ((center_of_mass V),UA) by FUNCT_1:59

.= (center_of_mass V) .: {UA} by RELAT_1:def 16 ;

set CA = Complex_of {UA};

set CB = Complex_of {B};

{UA} is_finer_than {B}

proof

then
Complex_of {UA} is SubSimplicialComplex of Complex_of {B}
by SIMPLEX0:30;
let x be set ; :: according to SETFAM_1:def 2 :: thesis: ( not x in {UA} or ex b_{1} being set st

( b_{1} in {B} & x c= b_{1} ) )

assume x in {UA} ; :: thesis: ex b_{1} being set st

( b_{1} in {B} & x c= b_{1} )

then A7: x = UA by TARSKI:def 1;

B in {B} by TARSKI:def 1;

hence ex b_{1} being set st

( b_{1} in {B} & x c= b_{1} )
by A5, A7; :: thesis: verum

end;( b

assume x in {UA} ; :: thesis: ex b

( b

then A7: x = UA by TARSKI:def 1;

B in {B} by TARSKI:def 1;

hence ex b

( b

then A8: subdivision ((center_of_mass V),(Complex_of {UA})) is SubSimplicialComplex of subdivision ((center_of_mass V),(Complex_of {B})) by SIMPLEX0:58;

|.(Complex_of {UA}).| c= [#] (Complex_of {UA}) ;

then A9: subdivision ((center_of_mass V),(Complex_of {UA})) = BCS (Complex_of {UA}) by Def5;

|.(Complex_of {B}).| c= [#] (Complex_of {B}) ;

then A10: BCS (Complex_of {UA}) is SubSimplicialComplex of BCS (Complex_of {B}) by A8, A9, Def5;

S is finite-membered

proof

then
((center_of_mass V) .: S) \/ ((center_of_mass V) .: {UA}) is Simplex of card S, BCS (Complex_of {UA})
by A1, A2, A3, A4, Lm1;
let x be set ; :: according to FINSET_1:def 6 :: thesis: ( not x in S or x is finite )

assume x in S ; :: thesis: x is finite

then A11: x c= union S by ZFMISC_1:74;

union S is finite by A2;

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

end;assume x in S ; :: thesis: x is finite

then A11: x c= union S by ZFMISC_1:74;

union S is finite by A2;

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

hence ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {B}) by A6, A10, SIMPLEX0:49; :: thesis: verum