let V be RealLinearSpace; :: thesis: for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv & ( for n being Nat st n <= degree Kv holds

ex S being Simplex of Kv st

( card S = n + 1 & @ S is affinely-independent ) ) holds

degree Kv = degree (BCS Kv)

let Kv be non void SimplicialComplex of V; :: thesis: ( |.Kv.| c= [#] Kv & ( for n being Nat st n <= degree Kv holds

ex S being Simplex of Kv st

( card S = n + 1 & @ S is affinely-independent ) ) implies degree Kv = degree (BCS Kv) )

assume that

A1: |.Kv.| c= [#] Kv and

A2: for n being Nat st n <= degree Kv holds

ex S being Simplex of Kv st

( card S = n + 1 & @ S is affinely-independent ) ; :: thesis: degree Kv = degree (BCS Kv)

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

A4: for n being Nat st n <= degree Kv holds

ex S being Subset of Kv st

( S is simplex-like & card S = n + 1 & BOOL S c= dom (center_of_mass V) & (center_of_mass V) .: (BOOL S) is Subset of Kv & (center_of_mass V) | (BOOL S) is one-to-one )

then A11: dom (center_of_mass V) is with_non-empty_elements ;

BCS Kv = subdivision ((center_of_mass V),Kv) by A1, Def5;

hence degree Kv = degree (BCS Kv) by A4, A11, SIMPLEX0:53; :: thesis: verum

ex S being Simplex of Kv st

( card S = n + 1 & @ S is affinely-independent ) ) holds

degree Kv = degree (BCS Kv)

let Kv be non void SimplicialComplex of V; :: thesis: ( |.Kv.| c= [#] Kv & ( for n being Nat st n <= degree Kv holds

ex S being Simplex of Kv st

( card S = n + 1 & @ S is affinely-independent ) ) implies degree Kv = degree (BCS Kv) )

assume that

A1: |.Kv.| c= [#] Kv and

A2: for n being Nat st n <= degree Kv holds

ex S being Simplex of Kv st

( card S = n + 1 & @ S is affinely-independent ) ; :: thesis: degree Kv = degree (BCS Kv)

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

A4: for n being Nat st n <= degree Kv holds

ex S being Subset of Kv st

( S is simplex-like & card S = n + 1 & BOOL S c= dom (center_of_mass V) & (center_of_mass V) .: (BOOL S) is Subset of Kv & (center_of_mass V) | (BOOL S) is one-to-one )

proof

not {} in dom (center_of_mass V)
by ZFMISC_1:56;
let n be Nat; :: thesis: ( n <= degree Kv implies ex S being Subset of Kv st

( S is simplex-like & card S = n + 1 & BOOL S c= dom (center_of_mass V) & (center_of_mass V) .: (BOOL S) is Subset of Kv & (center_of_mass V) | (BOOL S) is one-to-one ) )

assume n <= degree Kv ; :: thesis: ex S being Subset of Kv st

( S is simplex-like & card S = n + 1 & BOOL S c= dom (center_of_mass V) & (center_of_mass V) .: (BOOL S) is Subset of Kv & (center_of_mass V) | (BOOL S) is one-to-one )

then consider S being Simplex of Kv such that

A5: card S = n + 1 and

A6: @ S is affinely-independent by A2;

take S ; :: thesis: ( S is simplex-like & card S = n + 1 & BOOL S c= dom (center_of_mass V) & (center_of_mass V) .: (BOOL S) is Subset of Kv & (center_of_mass V) | (BOOL S) is one-to-one )

thus ( S is simplex-like & card S = n + 1 ) by A5; :: thesis: ( BOOL S c= dom (center_of_mass V) & (center_of_mass V) .: (BOOL S) is Subset of Kv & (center_of_mass V) | (BOOL S) is one-to-one )

A7: the topology of (Complex_of {(@ S)}) = bool S by SIMPLEX0:4;

reconsider SS = {(@ S)} as affinely-independent Subset-Family of V by A6;

A8: (center_of_mass V) .: (BOOL S) c= conv (@ S)

hence BOOL S c= dom (center_of_mass V) by A3, XBOOLE_1:33; :: thesis: ( (center_of_mass V) .: (BOOL S) is Subset of Kv & (center_of_mass V) | (BOOL S) is one-to-one )

conv (@ S) c= |.Kv.| by Th5;

then conv (@ S) c= [#] Kv by A1;

hence (center_of_mass V) .: (BOOL S) is Subset of Kv by A8, XBOOLE_1:1; :: thesis: (center_of_mass V) | (BOOL S) is one-to-one

( ((center_of_mass V) | (bool S)) | (BOOL S) = (center_of_mass V) | (BOOL S) & Complex_of SS is SimplicialComplex of V ) by RELAT_1:74;

hence (center_of_mass V) | (BOOL S) is one-to-one by A6, A7, FUNCT_1:52; :: thesis: verum

end;( S is simplex-like & card S = n + 1 & BOOL S c= dom (center_of_mass V) & (center_of_mass V) .: (BOOL S) is Subset of Kv & (center_of_mass V) | (BOOL S) is one-to-one ) )

assume n <= degree Kv ; :: thesis: ex S being Subset of Kv st

( S is simplex-like & card S = n + 1 & BOOL S c= dom (center_of_mass V) & (center_of_mass V) .: (BOOL S) is Subset of Kv & (center_of_mass V) | (BOOL S) is one-to-one )

then consider S being Simplex of Kv such that

A5: card S = n + 1 and

A6: @ S is affinely-independent by A2;

take S ; :: thesis: ( S is simplex-like & card S = n + 1 & BOOL S c= dom (center_of_mass V) & (center_of_mass V) .: (BOOL S) is Subset of Kv & (center_of_mass V) | (BOOL S) is one-to-one )

thus ( S is simplex-like & card S = n + 1 ) by A5; :: thesis: ( BOOL S c= dom (center_of_mass V) & (center_of_mass V) .: (BOOL S) is Subset of Kv & (center_of_mass V) | (BOOL S) is one-to-one )

A7: the topology of (Complex_of {(@ S)}) = bool S by SIMPLEX0:4;

reconsider SS = {(@ S)} as affinely-independent Subset-Family of V by A6;

A8: (center_of_mass V) .: (BOOL S) c= conv (@ S)

proof

bool (@ S) c= bool the carrier of V
by ZFMISC_1:67;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (center_of_mass V) .: (BOOL S) or y in conv (@ S) )

assume y in (center_of_mass V) .: (BOOL S) ; :: thesis: y in conv (@ S)

then consider x being object such that

A9: x in dom (center_of_mass V) and

A10: ( x in BOOL S & (center_of_mass V) . x = y ) by FUNCT_1:def 6;

reconsider x = x as non empty Subset of V by A9, ZFMISC_1:56;

( conv x c= conv (@ S) & y in conv x ) by A10, RLAFFIN2:16, RLTOPSP1:20;

hence y in conv (@ S) ; :: thesis: verum

end;assume y in (center_of_mass V) .: (BOOL S) ; :: thesis: y in conv (@ S)

then consider x being object such that

A9: x in dom (center_of_mass V) and

A10: ( x in BOOL S & (center_of_mass V) . x = y ) by FUNCT_1:def 6;

reconsider x = x as non empty Subset of V by A9, ZFMISC_1:56;

( conv x c= conv (@ S) & y in conv x ) by A10, RLAFFIN2:16, RLTOPSP1:20;

hence y in conv (@ S) ; :: thesis: verum

hence BOOL S c= dom (center_of_mass V) by A3, XBOOLE_1:33; :: thesis: ( (center_of_mass V) .: (BOOL S) is Subset of Kv & (center_of_mass V) | (BOOL S) is one-to-one )

conv (@ S) c= |.Kv.| by Th5;

then conv (@ S) c= [#] Kv by A1;

hence (center_of_mass V) .: (BOOL S) is Subset of Kv by A8, XBOOLE_1:1; :: thesis: (center_of_mass V) | (BOOL S) is one-to-one

( ((center_of_mass V) | (bool S)) | (BOOL S) = (center_of_mass V) | (BOOL S) & Complex_of SS is SimplicialComplex of V ) by RELAT_1:74;

hence (center_of_mass V) | (BOOL S) is one-to-one by A6, A7, FUNCT_1:52; :: thesis: verum

then A11: dom (center_of_mass V) is with_non-empty_elements ;

BCS Kv = subdivision ((center_of_mass V),Kv) by A1, Def5;

hence degree Kv = degree (BCS Kv) by A4, A11, SIMPLEX0:53; :: thesis: verum