let V be RealLinearSpace; for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & (card Sf) + 1 = card (union Sf) & union Sf is affinely-independent holds
card { S1 where S1 is Simplex of card Sf, BCS (Complex_of {(union Sf)}) : (center_of_mass V) .: Sf c= S1 } = 2
let S be c=-linear finite finite-membered Subset-Family of V; ( S is with_non-empty_elements & (card S) + 1 = card (union S) & union S is affinely-independent implies card { S1 where S1 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S1 } = 2 )
assume that
A1:
S is with_non-empty_elements
and
A2:
(card S) + 1 = card (union S)
and
A3:
union S is affinely-independent
; card { S1 where S1 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S1 } = 2
set B = center_of_mass V;
reconsider U = union S as finite affinely-independent Subset of V by A3;
reconsider s = S as Subset-Family of U by ZFMISC_1:82;
A4:
not S is empty
by A2, ZFMISC_1:2;
then consider ss1 being Subset-Family of U such that
A5:
s c= ss1
and
A6:
( ss1 is with_non-empty_elements & ss1 is c=-linear )
and
A7:
card ss1 = card U
and
A8:
for X being set st X in ss1 & card X <> 1 holds
ex x being set st
( x in X & X \ {x} in ss1 )
by A1, SIMPLEX0:9, SIMPLEX0:13;
card (ss1 \ s) = ((card S) + 1) - (card S)
by A2, A5, A7, CARD_2:44;
then consider x being object such that
A9:
ss1 \ s = {x}
by CARD_2:42;
reconsider c = card U as ExtReal ;
set CU = Complex_of {U};
set TC = the topology of (Complex_of {U});
A10:
the topology of (Complex_of {U}) = bool U
by SIMPLEX0:4;
then reconsider ss = ss1 as Subset-Family of (Complex_of {U}) by XBOOLE_1:1;
set BC = BCS (Complex_of {U});
reconsider cc = (card U) - 1 as ExtReal ;
A11:
|.(Complex_of {U}).| c= [#] (Complex_of {U})
;
then A12:
BCS (Complex_of {U}) = subdivision ((center_of_mass V),(Complex_of {U}))
by Def5;
then A13:
[#] (BCS (Complex_of {U})) = [#] (Complex_of {U})
by SIMPLEX0:def 20;
then reconsider Bss = (center_of_mass V) .: ss as Subset of (BCS (Complex_of {U})) ;
A14:
ss is simplex-like
then A15:
card Bss = card U
by A6, A7, Th33;
then A16:
card Bss = cc + 1
by A2, XXREAL_3:def 2;
A17:
x in {x}
by TARSKI:def 1;
then A18:
x in ss1
by A9, XBOOLE_0:def 5;
A19:
not x in s
by A9, A17, XBOOLE_0:def 5;
reconsider x = x as finite Subset of V by A9, A17, XBOOLE_1:1;
degree (Complex_of {U}) =
c - 1
by SIMPLEX0:26
.=
(card U) + (- 1)
by XXREAL_3:def 2
;
then A20:
cc = degree (BCS (Complex_of {U}))
by A11, Th31;
Bss is simplex-like
by A6, A12, A14, SIMPLEX0:def 20;
then A21:
Bss is Simplex of (card U) - 1, BCS (Complex_of {U})
by A2, A16, A20, SIMPLEX0:def 18;
x <> {}
by A6, A18;
then reconsider c1 = (card x) - 1 as Element of NAT by NAT_1:20;
ex xm being set st
( ( xm in s or xm = {} ) & card xm = (card x) - 1 & ( for y being set st y in s & y c= x holds
y c= xm ) )
proof
per cases
( card x = 1 or card x <> 1 )
;
suppose
card x <> 1
;
ex xm being set st
( ( xm in s or xm = {} ) & card xm = (card x) - 1 & ( for y being set st y in s & y c= x holds
y c= xm ) )then consider z being
set such that A26:
z in x
and A27:
x \ {z} in ss1
by A8, A18;
take xm =
x \ {z};
( ( xm in s or xm = {} ) & card xm = (card x) - 1 & ( for y being set st y in s & y c= x holds
y c= xm ) )A28:
x = xm \/ {z}
by A26, ZFMISC_1:116;
xm in s
hence
(
xm in s or
xm = {} )
;
( card xm = (card x) - 1 & ( for y being set st y in s & y c= x holds
y c= xm ) )
card x = c1 + 1
;
hence
card xm = (card x) - 1
by A26, STIRL2_1:55;
for y being set st y in s & y c= x holds
y c= xmlet y be
set ;
( y in s & y c= x implies y c= xm )assume that A29:
y in s
and A30:
y c= x
;
y c= xmassume A31:
not
y c= xm
;
contradiction
xm,
y are_c=-comparable
by A5, A6, A27, A29;
then
xm c= y
by A31;
hence
contradiction
by A19, A28, A29, A30, A31, ZFMISC_1:138;
verum end;
end;
then consider xm being set such that
A32:
( xm in s or xm = {} )
and
A33:
card xm = (card x) - 1
and
A34:
for y being set st y in s & y c= x holds
y c= xm
;
A35:
U in S
by A4, SIMPLEX0:9;
then
( union ss1 c= U & U c= union ss )
by A5, ZFMISC_1:74;
then A36:
union ss = U
;
x c< U
by A9, A17, A19, A35;
then
card x < card U
by CARD_2:48;
then
(card x) + 1 <= card U
by NAT_1:13;
then consider xM being set such that
A37:
xM in ss
and
A38:
card xM = (card x) + 1
by A6, A36, A21, Th36;
reconsider xm = xm as finite Subset of V by A32, XBOOLE_1:2;
reconsider xM = xM as finite Subset of V by A37;
A39:
not xM c= xm
A40:
xM in s
then
( xm,xM are_c=-comparable or xm c= xM )
by A32, ORDINAL1:def 8;
then A41:
xm c= xM
by A39;
then
card (xM \ xm) = (card xM) - (card xm)
by CARD_2:44;
then consider x1, x2 being object such that
A42:
x1 <> x2
and
A43:
xM \ xm = {x1,x2}
by A33, A38, CARD_2:60;
A44:
x1 in {x1,x2}
by TARSKI:def 2;
A45:
x2 in {x1,x2}
by TARSKI:def 2;
then reconsider x1 = x1, x2 = x2 as Element of V by A43, A44;
set xm1 = xm \/ {x1};
set xm2 = xm \/ {x2};
reconsider S1 = S \/ {(xm \/ {x1})}, S2 = S \/ {(xm \/ {x2})} as Subset-Family of (Complex_of {U}) ;
reconsider BS1 = (center_of_mass V) .: S1, BS2 = (center_of_mass V) .: S2 as Subset of (BCS (Complex_of {U})) by A13;
A46:
BS1 = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {(xm \/ {x1})})
by RELAT_1:120;
A47:
not x1 in xm
by A43, A44, XBOOLE_0:def 5;
then A48:
card (xm \/ {x1}) = (card xm) + 1
by CARD_2:41;
A49:
not xm \/ {x1} in S
not x2 in xm
by A43, A45, XBOOLE_0:def 5;
then A51:
card (xm \/ {x2}) = (card xm) + 1
by CARD_2:41;
A52:
not xm \/ {x2} in S
x2 in xM
by A43, A45, XBOOLE_0:def 5;
then
{x2} c= xM
by ZFMISC_1:31;
then A54:
xm \/ {x2} c= xM
by A41, XBOOLE_1:8;
A55:
S2 c= bool U
A57:
S2 is simplex-like
then
card BS2 = card S2
by A1, Th33;
then A58:
card BS2 = (card S) + 1
by A52, CARD_2:41;
x1 in xM
by A43, A44, XBOOLE_0:def 5;
then
{x1} c= xM
by ZFMISC_1:31;
then A59:
xm \/ {x1} c= xM
by A41, XBOOLE_1:8;
A60:
S1 c= bool U
then A62:
BS1 = ((center_of_mass V) | the topology of (Complex_of {U})) .: S1
by A10, RELAT_1:129;
A63:
S1 is simplex-like
then
card BS1 = card S1
by A1, Th33;
then A64:
card BS1 = (card S) + 1
by A49, CARD_2:41;
A65:
( xm c= xm \/ {x1} & xm c= xm \/ {x2} )
by XBOOLE_1:7;
A66:
for y1 being set st y1 in S holds
( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable )
S1 is c=-linear
then
BS1 is simplex-like
by A12, A63, SIMPLEX0:def 20;
then A77:
BS1 is Simplex of (card U) - 1, BCS (Complex_of {U})
by A2, A15, A16, A20, A64, SIMPLEX0:def 18;
set SS = { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } ;
(center_of_mass V) .: S c= ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {(xm \/ {x1})})
by XBOOLE_1:7;
then A78:
BS1 in { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 }
by A2, A46, A77;
A79:
BS2 = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {(xm \/ {x2})})
by RELAT_1:120;
A80:
{ S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } c= {BS1,BS2}
proof
let w be
object ;
TARSKI:def 3 ( not w in { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } or w in {BS1,BS2} )
reconsider n =
0 as
Nat ;
assume
w in { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 }
;
w in {BS1,BS2}
then consider W being
Simplex of
card S,
BCS (Complex_of {U}) such that A81:
w = W
and A82:
(center_of_mass V) .: S c= W
;
((card S) + n) + 1
<= card U
by A2;
then consider T being
finite Subset-Family of
V such that A83:
T misses S
and A84:
(
T \/ S is
c=-linear &
T \/ S is
with_non-empty_elements )
and A85:
card T = n + 1
and A86:
union T c= U
and A87:
@ W = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T)
by A1, A82, Th35;
consider x3 being
object such that A88:
{x3} = T
by A85, CARD_2:42;
A89:
x3 in T
by A88, TARSKI:def 1;
then A90:
not
x3 in S
by A83, XBOOLE_0:3;
reconsider x3 =
x3 as
set by TARSKI:1;
A91:
x3 c= union T
by A89, ZFMISC_1:74;
A92:
x3 in T \/ S
by A89, XBOOLE_0:def 3;
reconsider x3 =
x3 as
finite Subset of
U by A86, A91, XBOOLE_1:1;
A93:
not
xM c= x3
proof
consider x4 being
set such that A94:
x4 in ss
and A95:
card x4 = card x3
by A6, A36, A21, A84, A92, Th36, NAT_1:43;
assume
xM c= x3
;
contradiction
then
(card x) + 1
<= card x3
by A38, NAT_1:43;
then
x <> x4
by A95, NAT_1:13;
then
not
x4 in {x}
by TARSKI:def 1;
then A96:
x4 in s
by A9, A94, XBOOLE_0:def 5;
then
x4 in S \/ T
by XBOOLE_0:def 3;
then
x3,
x4 are_c=-comparable
by A84, A92;
then
(
x3 c= x4 or
x4 c= x3 )
;
hence
contradiction
by A90, A95, A96, CARD_2:102;
verum
end;
A97:
(
xm c= x3 &
xm <> x3 )
proof
per cases
( xm = {} or xm in s )
by A32;
suppose A98:
xm in s
;
( xm c= x3 & xm <> x3 )A99:
not
x3 c= xm
proof
assume
x3 c= xm
;
contradiction
then A100:
card x3 <= card xm
by NAT_1:43;
consider x4 being
set such that A101:
x4 in ss
and A102:
card x4 = card x3
by A6, A36, A21, A84, A92, Th36, NAT_1:43;
(card xm) + 1
= card x
by A33;
then
card x <> card x3
by A100, NAT_1:13;
then
not
x4 in {x}
by A102, TARSKI:def 1;
then A103:
x4 in s
by A9, A101, XBOOLE_0:def 5;
then
x4 in S \/ T
by XBOOLE_0:def 3;
then
x3,
x4 are_c=-comparable
by A84, A92;
then
(
x3 c= x4 or
x4 c= x3 )
;
hence
contradiction
by A90, A102, A103, CARD_2:102;
verum
end;
xm in T \/ S
by A98, XBOOLE_0:def 3;
then
xm,
x3 are_c=-comparable
by A84, A92;
hence
(
xm c= x3 &
xm <> x3 )
by A99;
verum end;
end;
then A104:
x3 = x3 \/ xm
by XBOOLE_1:12;
xM in S \/ T
by A40, XBOOLE_0:def 3;
then
xM,
x3 are_c=-comparable
by A84, A92;
then
x3 c= xM
by A93;
then A105:
x3 \ xm c= xM \ xm
by XBOOLE_1:33;
A106:
xM = xm \/ xM
by A41, XBOOLE_1:12;
A107:
x3 \ xm <> xM \ xm
A108:
x3 \ xm <> {}
by XBOOLE_1:37, A97;
x3 \/ xm = (x3 \ xm) \/ xm
by XBOOLE_1:39;
then
(
x3 = xm \/ {x1} or
x3 = xm \/ {x2} )
by A43, A104, A105, A107, A108, ZFMISC_1:36;
hence
w in {BS1,BS2}
by A79, A46, A81, A87, A88, TARSKI:def 2;
verum
end;
A109:
BS2 = ((center_of_mass V) | the topology of (Complex_of {U})) .: S2
by A10, A55, RELAT_1:129;
A110:
BS1 <> BS2
proof
assume A111:
BS1 = BS2
;
contradiction
then
BS1 \ BS2 = {}
by XBOOLE_1:37;
then
((center_of_mass V) | the topology of (Complex_of {U})) .: (S1 \ S2) = {}
by A109, A62, FUNCT_1:64;
then A112:
dom ((center_of_mass V) | the topology of (Complex_of {U})) misses S1 \ S2
by RELAT_1:118;
BS2 \ BS1 = {}
by A111, XBOOLE_1:37;
then
((center_of_mass V) | the topology of (Complex_of {U})) .: (S2 \ S1) = {}
by A109, A62, FUNCT_1:64;
then A113:
dom ((center_of_mass V) | the topology of (Complex_of {U})) misses S2 \ S1
by RELAT_1:118;
A114:
dom ((center_of_mass V) | the topology of (Complex_of {U})) = (dom (center_of_mass V)) /\ the
topology of
(Complex_of {U})
by RELAT_1:61;
xm \/ {x1} in {(xm \/ {x1})}
by TARSKI:def 1;
then A115:
xm \/ {x1} in S1
by XBOOLE_0:def 3;
A116:
dom (center_of_mass V) = (bool the carrier of V) \ {{}}
by FUNCT_2:def 1;
A117:
S1 \ S2 c= S1
by XBOOLE_1:36;
then
not
{} in S1 \ S2
by A1;
then A118:
S1 \ S2 c= dom (center_of_mass V)
by A116, ZFMISC_1:34;
A119:
S2 \ S1 c= S2
by XBOOLE_1:36;
then
not
{} in S2 \ S1
by A1;
then A120:
S2 \ S1 c= dom (center_of_mass V)
by A116, ZFMISC_1:34;
S1 \ S2 c= bool U
by A60, A117;
then
S1 \ S2 c= dom ((center_of_mass V) | the topology of (Complex_of {U}))
by A10, A114, A118, XBOOLE_1:19;
then A121:
S1 \ S2 = {}
by A112, XBOOLE_1:67;
S2 \ S1 c= bool U
by A55, A119;
then
S2 \ S1 c= dom ((center_of_mass V) | the topology of (Complex_of {U}))
by A10, A114, A120, XBOOLE_1:19;
then
S1 = S2
by A113, A121, XBOOLE_1:32, XBOOLE_1:67;
then
xm \/ {x1} in {(xm \/ {x2})}
by A49, A115, XBOOLE_0:def 3;
then A122:
xm \/ {x1} = xm \/ {x2}
by TARSKI:def 1;
x1 in {x1}
by TARSKI:def 1;
then
x1 in xm \/ {x1}
by XBOOLE_0:def 3;
then
x1 in {x2}
by A47, A122, XBOOLE_0:def 3;
hence
contradiction
by A42, TARSKI:def 1;
verum
end;
S2 is c=-linear
then
BS2 is simplex-like
by A12, A57, SIMPLEX0:def 20;
then A126:
BS2 is Simplex of (card U) - 1, BCS (Complex_of {U})
by A2, A15, A16, A20, A58, SIMPLEX0:def 18;
(center_of_mass V) .: S c= ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {(xm \/ {x2})})
by XBOOLE_1:7;
then
BS2 in { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 }
by A2, A79, A126;
then
{BS1,BS2} c= { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 }
by A78, ZFMISC_1:32;
then
{ S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } = {BS1,BS2}
by A80;
hence
card { S1 where S1 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S1 } = 2
by A110, CARD_2:57; verum