let V be RealLinearSpace; for K being non void total affinely-independent simplex-join-closed SimplicialComplex of V
for Sk being finite simplex-like Subset-Family of K st Sk is c=-linear & Sk is with_non-empty_elements & (card Sk) + 1 = card (union Sk) holds
card { S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2
let K be non void total affinely-independent simplex-join-closed SimplicialComplex of V; for Sk being finite simplex-like Subset-Family of K st Sk is c=-linear & Sk is with_non-empty_elements & (card Sk) + 1 = card (union Sk) holds
card { S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2
let Sk be finite simplex-like Subset-Family of K; ( Sk is c=-linear & Sk is with_non-empty_elements & (card Sk) + 1 = card (union Sk) implies card { S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2 )
set B = center_of_mass V;
assume that
A1:
( Sk is c=-linear & Sk is with_non-empty_elements )
and
A2:
(card Sk) + 1 = card (union Sk)
; card { S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2
not Sk is empty
by A2, ZFMISC_1:2;
then
union Sk in Sk
by A1, SIMPLEX0:9;
then reconsider U = union Sk as Simplex of K by TOPS_2:def 1;
reconsider Sk1 = @ Sk as c=-linear finite finite-membered Subset-Family of V by A1;
reconsider c = card U as ExtReal ;
@ U = union Sk1
;
then reconsider U1 = union Sk1 as finite affinely-independent Subset of V ;
set C = Complex_of {U1};
A3: degree (Complex_of {U1}) =
c - 1
by SIMPLEX0:26
.=
(card U) + (- 1)
by XXREAL_3:def 2
.=
card Sk
by A2
;
set YY = { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) } ;
[#] K = the carrier of V
by SIMPLEX0:def 10;
then
|.K.| c= [#] K
;
then A4:
subdivision ((center_of_mass V),K) = BCS K
by Def5;
set XX = { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W } ;
A5:
@ U = U1
;
then A6:
Complex_of {U1} is SubSimplicialComplex of K
by Th3;
then
the topology of (Complex_of {U1}) c= the topology of K
by SIMPLEX0:def 13;
then A7:
|.(Complex_of {U1}).| c= |.K.|
by Th4;
A8:
[#] (Complex_of {U1}) = [#] V
;
then A9:
degree (Complex_of {U1}) = degree (BCS (Complex_of {U1}))
by A7, Th31;
subdivision ((center_of_mass V),(Complex_of {U1})) = BCS (Complex_of {U1})
by A7, A8, Def5;
then
BCS (Complex_of {U1}) is SubSimplicialComplex of BCS K
by A4, A6, SIMPLEX0:58;
then A10:
degree (BCS (Complex_of {U1})) <= degree (BCS K)
by SIMPLEX0:32;
A11:
{ W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W } c= { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) }
proof
let x be
object ;
TARSKI:def 3 ( not x in { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W } or x in { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) } )
assume
x in { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W }
;
x in { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) }
then consider W being
Simplex of
card Sk,
BCS (Complex_of {U1}) such that A12:
(
x = W &
(center_of_mass V) .: Sk1 c= W )
;
W = @ W
;
then reconsider w =
W as
Simplex of
(BCS K) by A5, Th40;
card W = (degree (BCS (Complex_of {U1}))) + 1
by A3, A9, SIMPLEX0:def 18;
then A13:
w is
Simplex of
card Sk,
BCS K
by A3, A9, A10, SIMPLEX0:def 18;
(
conv (@ W) c= conv (@ U) &
@ w = w )
by Th40;
hence
x in { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) }
by A12, A13;
verum
end;
A14:
[#] (subdivision ((center_of_mass V),(Complex_of {U1}))) = [#] (Complex_of {U1})
by SIMPLEX0:def 20;
A15:
{ W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) } c= { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W }
proof
let x be
object ;
TARSKI:def 3 ( not x in { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) } or x in { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W } )
reconsider c1 =
card Sk as
ExtReal ;
assume
x in { W where W is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= W & conv (@ W) c= conv (@ (union Sk)) ) }
;
x in { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W }
then consider W being
Simplex of
card Sk,
BCS K such that A16:
(
W = x &
(center_of_mass V) .: Sk c= W )
and A17:
conv (@ W) c= conv (@ U)
;
reconsider w =
@ W as
Subset of
(BCS (Complex_of {U1})) by A7, A14, Def5;
reconsider cW =
card W as
ExtReal ;
card W =
c1 + 1
by A3, A9, A10, SIMPLEX0:def 18
.=
(card Sk) + 1
by XXREAL_3:def 2
;
then
card Sk = (card W) + (- 1)
;
then A18:
card Sk = cW - 1
by XXREAL_3:def 2;
w is
simplex-like
by A17, Th40;
then
w is
Simplex of
card Sk,
BCS (Complex_of {U1})
by A18, SIMPLEX0:48;
hence
x in { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W }
by A16;
verum
end;
card { W where W is Simplex of card Sk, BCS (Complex_of {U1}) : (center_of_mass V) .: Sk c= W } = 2
by A1, A2, Th39;
hence
card { S1 where S1 is Simplex of card Sk, BCS K : ( (center_of_mass V) .: Sk c= S1 & conv (@ S1) c= conv (@ (union Sk)) ) } = 2
by A11, A15, XBOOLE_0:def 10; verum