let V be RealLinearSpace; :: thesis: for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V

for Aff being finite affinely-independent Subset of V

for B being Subset of V st Aff is Simplex of K holds

( B is Simplex of (BCS (Complex_of {Aff})) iff ( B is Simplex of (BCS K) & conv B c= conv Aff ) )

let K be non void total affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis: for Aff being finite affinely-independent Subset of V

for B being Subset of V st Aff is Simplex of K holds

( B is Simplex of (BCS (Complex_of {Aff})) iff ( B is Simplex of (BCS K) & conv B c= conv Aff ) )

let Aff be finite affinely-independent Subset of V; :: thesis: for B being Subset of V st Aff is Simplex of K holds

( B is Simplex of (BCS (Complex_of {Aff})) iff ( B is Simplex of (BCS K) & conv B c= conv Aff ) )

let B be Subset of V; :: thesis: ( Aff is Simplex of K implies ( B is Simplex of (BCS (Complex_of {Aff})) iff ( B is Simplex of (BCS K) & conv B c= conv Aff ) ) )

set Bag = center_of_mass V;

set C = Complex_of {Aff};

A1: the topology of (Complex_of {Aff}) = bool Aff by SIMPLEX0:4;

assume Aff is Simplex of K ; :: thesis: ( B is Simplex of (BCS (Complex_of {Aff})) iff ( B is Simplex of (BCS K) & conv B c= conv Aff ) )

then reconsider s = Aff as Simplex of K ;

A2: [#] K = the carrier of V by SIMPLEX0:def 10;

then |.K.| c= [#] K ;

then A3: subdivision ((center_of_mass V),K) = BCS K by Def5;

@ s is affinely-independent ;

then A4: Complex_of {Aff} is SubSimplicialComplex of K by Th3;

then the topology of (Complex_of {Aff}) c= the topology of K by SIMPLEX0:def 13;

then A5: |.(Complex_of {Aff}).| c= |.K.| by Th4;

[#] (Complex_of {Aff}) = [#] V ;

then A6: subdivision ((center_of_mass V),(Complex_of {Aff})) = BCS (Complex_of {Aff}) by A5, Def5;

then BCS (Complex_of {Aff}) is SubSimplicialComplex of BCS K by A3, A4, SIMPLEX0:58;

then A7: the topology of (BCS (Complex_of {Aff})) c= the topology of (BCS K) by SIMPLEX0:def 13;

A8: B is Simplex of (BCS K) and

A9: conv B c= conv Aff ; :: thesis: B is Simplex of (BCS (Complex_of {Aff}))

reconsider A = B as Simplex of (BCS K) by A8;

consider SS being c=-linear finite simplex-like Subset-Family of K such that

A10: B = (center_of_mass V) .: SS by A3, A8, SIMPLEX0:def 20;

reconsider ss = SS as c=-linear finite Subset-Family of (Complex_of {Aff}) by A2;

[#] (subdivision ((center_of_mass V),(Complex_of {Aff}))) = [#] (Complex_of {Aff}) by SIMPLEX0:def 20;

then reconsider Bss = (center_of_mass V) .: ss as Subset of (BCS (Complex_of {Aff})) by A5, Def5;

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

ss is simplex-like

hence B is Simplex of (BCS (Complex_of {Aff})) by A10; :: thesis: verum

for Aff being finite affinely-independent Subset of V

for B being Subset of V st Aff is Simplex of K holds

( B is Simplex of (BCS (Complex_of {Aff})) iff ( B is Simplex of (BCS K) & conv B c= conv Aff ) )

let K be non void total affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis: for Aff being finite affinely-independent Subset of V

for B being Subset of V st Aff is Simplex of K holds

( B is Simplex of (BCS (Complex_of {Aff})) iff ( B is Simplex of (BCS K) & conv B c= conv Aff ) )

let Aff be finite affinely-independent Subset of V; :: thesis: for B being Subset of V st Aff is Simplex of K holds

( B is Simplex of (BCS (Complex_of {Aff})) iff ( B is Simplex of (BCS K) & conv B c= conv Aff ) )

let B be Subset of V; :: thesis: ( Aff is Simplex of K implies ( B is Simplex of (BCS (Complex_of {Aff})) iff ( B is Simplex of (BCS K) & conv B c= conv Aff ) ) )

set Bag = center_of_mass V;

set C = Complex_of {Aff};

A1: the topology of (Complex_of {Aff}) = bool Aff by SIMPLEX0:4;

assume Aff is Simplex of K ; :: thesis: ( B is Simplex of (BCS (Complex_of {Aff})) iff ( B is Simplex of (BCS K) & conv B c= conv Aff ) )

then reconsider s = Aff as Simplex of K ;

A2: [#] K = the carrier of V by SIMPLEX0:def 10;

then |.K.| c= [#] K ;

then A3: subdivision ((center_of_mass V),K) = BCS K by Def5;

@ s is affinely-independent ;

then A4: Complex_of {Aff} is SubSimplicialComplex of K by Th3;

then the topology of (Complex_of {Aff}) c= the topology of K by SIMPLEX0:def 13;

then A5: |.(Complex_of {Aff}).| c= |.K.| by Th4;

[#] (Complex_of {Aff}) = [#] V ;

then A6: subdivision ((center_of_mass V),(Complex_of {Aff})) = BCS (Complex_of {Aff}) by A5, Def5;

then BCS (Complex_of {Aff}) is SubSimplicialComplex of BCS K by A3, A4, SIMPLEX0:58;

then A7: the topology of (BCS (Complex_of {Aff})) c= the topology of (BCS K) by SIMPLEX0:def 13;

hereby :: thesis: ( B is Simplex of (BCS K) & conv B c= conv Aff implies B is Simplex of (BCS (Complex_of {Aff})) )

assume that assume
B is Simplex of (BCS (Complex_of {Aff}))
; :: thesis: ( B is Simplex of (BCS K) & conv B c= conv Aff )

then reconsider A = B as Simplex of (BCS (Complex_of {Aff})) ;

A in the topology of (BCS (Complex_of {Aff})) by PRE_TOPC:def 2;

then A in the topology of (BCS K) by A7;

then reconsider a = A as Simplex of (BCS K) by PRE_TOPC:def 2;

( |.(BCS (Complex_of {Aff})).| = |.(Complex_of {Aff}).| & conv (@ A) c= |.(BCS (Complex_of {Aff})).| ) by Th5, Th10;

then conv (@ a) c= conv Aff by Th8;

hence ( B is Simplex of (BCS K) & conv B c= conv Aff ) ; :: thesis: verum

end;then reconsider A = B as Simplex of (BCS (Complex_of {Aff})) ;

A in the topology of (BCS (Complex_of {Aff})) by PRE_TOPC:def 2;

then A in the topology of (BCS K) by A7;

then reconsider a = A as Simplex of (BCS K) by PRE_TOPC:def 2;

( |.(BCS (Complex_of {Aff})).| = |.(Complex_of {Aff}).| & conv (@ A) c= |.(BCS (Complex_of {Aff})).| ) by Th5, Th10;

then conv (@ a) c= conv Aff by Th8;

hence ( B is Simplex of (BCS K) & conv B c= conv Aff ) ; :: thesis: verum

A8: B is Simplex of (BCS K) and

A9: conv B c= conv Aff ; :: thesis: B is Simplex of (BCS (Complex_of {Aff}))

reconsider A = B as Simplex of (BCS K) by A8;

consider SS being c=-linear finite simplex-like Subset-Family of K such that

A10: B = (center_of_mass V) .: SS by A3, A8, SIMPLEX0:def 20;

reconsider ss = SS as c=-linear finite Subset-Family of (Complex_of {Aff}) by A2;

[#] (subdivision ((center_of_mass V),(Complex_of {Aff}))) = [#] (Complex_of {Aff}) by SIMPLEX0:def 20;

then reconsider Bss = (center_of_mass V) .: ss as Subset of (BCS (Complex_of {Aff})) by A5, Def5;

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

ss is simplex-like

proof

then
Bss is simplex-like
by A6, SIMPLEX0:def 20;
let a be Subset of (Complex_of {Aff}); :: according to TOPS_2:def 1 :: thesis: ( not a in ss or not a is dependent )

assume A12: a in ss ; :: thesis: not a is dependent

reconsider aK = a as Simplex of K by A12, TOPS_2:def 1;

end;assume A12: a in ss ; :: thesis: not a is dependent

reconsider aK = a as Simplex of K by A12, TOPS_2:def 1;

per cases
( aK is empty or not aK is empty )
;

end;

suppose A13:
not aK is empty
; :: thesis: not a is dependent

then
aK in dom (center_of_mass V)
by A11, ZFMISC_1:56;

then A14: (center_of_mass V) . aK in A by A10, A12, FUNCT_1:def 6;

A15: (center_of_mass V) . aK in Int (@ aK) by A13, RLAFFIN2:20;

A c= conv (@ A) by RLAFFIN1:2;

then (center_of_mass V) . aK in conv (@ A) by A14;

then Int (@ aK) meets conv (@ s) by A9, A15, XBOOLE_0:3;

then aK c= Aff by Th26;

hence not a is dependent by A1; :: thesis: verum

end;then A14: (center_of_mass V) . aK in A by A10, A12, FUNCT_1:def 6;

A15: (center_of_mass V) . aK in Int (@ aK) by A13, RLAFFIN2:20;

A c= conv (@ A) by RLAFFIN1:2;

then (center_of_mass V) . aK in conv (@ A) by A14;

then Int (@ aK) meets conv (@ s) by A9, A15, XBOOLE_0:3;

then aK c= Aff by Th26;

hence not a is dependent by A1; :: thesis: verum

hence B is Simplex of (BCS (Complex_of {Aff})) by A10; :: thesis: verum