let V be RealLinearSpace; 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; ( 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)
; 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; ( 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
; ((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
Complex_of {UA} is SubSimplicialComplex of Complex_of {B}
by SIMPLEX0:30;
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
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;
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; verum