let n be Nat; :: thesis:
let V be RealLinearSpace; :: thesis:
let K be non void total affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis:
let A be finite Subset of V; :: thesis:
assume that
A1: K is Subdivision of Complex_of {A} and
A2: card A = n + 1 and
A3: degree K = n and
A4: for S being Simplex of n - 1,K
for X being set st X = { S1 where S1 is Simplex of n,K : S c= S1 } holds
( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) ) ; :: thesis:
|.(Complex_of {A}).| = conv A by Th8;
then A5: |.K.| = conv A by A1, Th10;
A6: K is finite-degree by A3, SIMPLEX0:def 12;
A7: A is affinely-independent

proof

consider a being Subset of K such that
A8: a is simplex-like and
A9: card a = (degree K) + 1 by A6, SIMPLEX0:def 12;
conv (@ a) c= conv A by A5, A8, Th5;
then A10: Affin (@ a) c= Affin A by RLAFFIN1:68;
card A = card a by A2, A3, A9, XXREAL_3:def 2;
hence A is affinely-independent by A8, A10, RLAFFIN1:80; :: thesis:

end;

set B = center_of_mass V;
reconsider Z = 0 as Nat ;
set TK = TopStruct(# the carrier of K, the topology of K #);
reconsider n1 = n - 1 as ExtReal ;
let S be Simplex of n - 1, BCS K; :: thesis:
let X be set ; :: thesis:
assume A11: X = { S1 where S1 is Simplex of n, BCS K : S c= S1 } ; :: thesis:
[#] K = the carrier of V by SIMPLEX0:def 10;
then A12: |.K.| c= [#] K ;
then A13: degree K = degree (BCS K) by Th31;
then A14: ( n + (- 1) >= - 1 & n - 1 <= degree (BCS K) ) by A3, XREAL_1:31, XREAL_1:146;
then A15: card S = n1 + 1 by SIMPLEX0:def 18;
then A16: card S = (n - 1) + 1 by XXREAL_3:def 2;
A17: BCS K = subdivision ((center_of_mass V),K) by A12, Def5;

per cases ;

suppose A18: n = 0 ; :: thesis:

then A19: TopStruct(# the carrier of K, the topology of K #) = BCS K by A3, A12, Th21;
then S in the topology of K by PRE_TOPC:def 2;
then reconsider s = S as Simplex of K by PRE_TOPC:def 2;
reconsider s = s as Simplex of n - 1,K by A3, A15, A18, SIMPLEX0:def 18;
set XX = { W where W is Simplex of n,K : s c= W } ;
A20: @ S = @ s ;
then A21: ( conv (@ S) meets Int A implies card { W where W is Simplex of n,K : s c= W } = 2 ) by A4;
A22: { W where W is Simplex of n,K : s c= W } c= X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { W where W is Simplex of n,K : s c= W } ; :: thesis:
then consider W being Simplex of n,K such that
A23: ( x = W & S c= W ) ;
W in the topology of (BCS K) by A19, PRE_TOPC:def 2;
then reconsider w = W as Simplex of (BCS K) by PRE_TOPC:def 2;
card W = (degree K) + 1 by A3, SIMPLEX0:def 18;
then w is Simplex of n, BCS K by A3, A13, SIMPLEX0:def 18;
hence x in X by A11, A23; :: thesis:

end;

A24: X c= { W where W is Simplex of n,K : s c= W }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in X ; :: thesis:
then consider W being Simplex of n, BCS K such that
A25: ( x = W & S c= W ) by A11;
W in the topology of K by A19, PRE_TOPC:def 2;
then reconsider w = W as Simplex of K by PRE_TOPC:def 2;
card W = (degree (BCS K)) + 1 by A3, A13, SIMPLEX0:def 18;
then w is Simplex of n,K by A3, A13, SIMPLEX0:def 18;
hence x in { W where W is Simplex of n,K : s c= W } by A25; :: thesis:

end;

( conv (@ S) misses Int A implies card { W where W is Simplex of n,K : s c= W } = 1 ) by A4, A20;
hence ( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) ) by A22, A24, A21, XBOOLE_0:def 10; :: thesis:

end;

suppose A26: n > 0 ; :: thesis:

consider SS being c=-linear finite simplex-like Subset-Family of K such that
A27: S = (center_of_mass V) .: SS by A17, SIMPLEX0:def 20;
SS \ {{}} c= SS by XBOOLE_1:36;
then reconsider SS1 = SS \ {{}} as c=-linear finite simplex-like Subset-Family of K by TOPS_2:11;
A28: ( SS1 c= bool (@ (union SS1)) & bool (@ (union SS1)) c= bool the carrier of V ) by ZFMISC_1:67, ZFMISC_1:82;
A29: not {} in SS1 by ZFMISC_1:56;
then A30: SS1 is with_non-empty_elements ;
A31: dom (center_of_mass V) = (bool the carrier of V) \ {{}} by FUNCT_2:def 1;
then A32: SS /\ (dom (center_of_mass V)) = (SS /\ (bool the carrier of V)) \ {{}} by XBOOLE_1:49
.= SS1 /\ (bool the carrier of V) by XBOOLE_1:49
.= SS1 by A28, XBOOLE_1:1, XBOOLE_1:28 ;
then A33: (center_of_mass V) .: SS = (center_of_mass V) .: SS1 by RELAT_1:112;
then A34: card SS1 = n by A16, A27, A30, Th33;
A35: S = (center_of_mass V) .: SS1 by A27, A32, RELAT_1:112;
A36: card SS1 = card S by A27, A30, A33, Th33;
then A37: not SS1 is empty by A16, A26;
then A38: union SS1 in SS1 by SIMPLEX0:9;
then reconsider U = union SS1 as Simplex of K by TOPS_2:def 1;
Segm (card SS1) c= Segm (card U) by A30, SIMPLEX0:10;
then A39: n <= card U by A16, A36, NAT_1:39;
card U <= (degree K) + 1 by SIMPLEX0:24;
then A40: card U <= n + 1 by A3, XXREAL_3:def 2;
A41: conv (@ U) c= conv A by A5, Th5;
SS1 c= bool the carrier of V by A28;
then A42: conv (@ S) c= conv (@ U) by A35, CONVEX1:30, RLAFFIN2:17;

per cases by A39, A40, NAT_1:9;

suppose A43: card U = n ; :: thesis:

set XX = { W where W is Simplex of n,K : U c= W } ;
A44: U is Simplex of n - 1,K by A13, A14, A15, A16, A43, SIMPLEX0:def 18;

hereby :: thesis:

assume conv (@ S) meets Int A ; :: thesis:
then conv (@ U) meets Int A by A42, XBOOLE_1:63;
then A45: card { W where W is Simplex of n,K : U c= W } = 2 by A4, A44;
consider w1, w2 being object such that
A46: w1 <> w2 and
A47: { W where W is Simplex of n,K : U c= W } = {w1,w2} by A45, CARD_2:60;
w2 in { W where W is Simplex of n,K : U c= W } by A47, TARSKI:def 2;
then consider W2 being Simplex of n,K such that
A48: w2 = W2 and
A49: U c= W2 ;
A50: ( SS1 is with_non-empty_elements & S = (center_of_mass V) .: SS1 ) by A27, A29, A32, RELAT_1:112;
w1 in { W where W is Simplex of n,K : U c= W } by A47, TARSKI:def 2;
then consider W1 being Simplex of n,K such that
A51: w1 = W1 and
A52: U c= W1 ;
A53: card W1 = (degree K) + 1 by A3, SIMPLEX0:def 18;
then A54: card W1 = n + 1 by A3, XXREAL_3:def 2;
then { W where W is Simplex of n, BCS K : ( S c= W & conv (@ W) c= conv (@ W1) ) } = {(S \/ ((center_of_mass V) .: {W1}))} by A16, A27, A30, A33, A36, A43, A52, Th42;
then S \/ ((center_of_mass V) .: {W1}) in { W where W is Simplex of n, BCS K : ( S c= W & conv (@ W) c= conv (@ W1) ) } by TARSKI:def 1;
then A55: ex R being Simplex of n, BCS K st
( R = S \/ ((center_of_mass V) .: {W1}) & S c= R & conv (@ R) c= conv (@ W1) ) ;
A56: S \/ ((center_of_mass V) .: {W1}) <> S \/ ((center_of_mass V) .: {W2})

proof

for A being Subset of K st A in {W1} holds
A is simplex-like by TARSKI:def 1;
then {W1} is simplex-like ;
then A57: SS1 \/ {W1} is simplex-like by TOPS_2:13;
A58: ( S \/ ((center_of_mass V) .: {W1}) = (center_of_mass V) .: (SS1 \/ {W1}) & S \/ ((center_of_mass V) .: {W2}) = (center_of_mass V) .: (SS1 \/ {W2}) ) by A35, RELAT_1:120;
W1 in {W1} by TARSKI:def 1;
then A59: W1 in SS1 \/ {W1} by XBOOLE_0:def 3;
for A being Subset of K st A in {W2} holds
A is simplex-like by TARSKI:def 1;
then {W2} is simplex-like ;
then A60: SS1 \/ {W2} is simplex-like by TOPS_2:13;
assume A61: S \/ ((center_of_mass V) .: {W1}) = S \/ ((center_of_mass V) .: {W2}) ; :: thesis:
not W1 is empty by A3, A53;
then SS1 \/ {W1} c= SS1 \/ {W2} by A12, A30, A55, A60, A58, A57, A61, Th34;
then ( W1 in SS1 or W1 in {W2} ) by A59, XBOOLE_0:def 3;
then W1 c= U by A46, A48, A51, TARSKI:def 1, ZFMISC_1:74;
then W1 = U by A52;
hence contradiction by A43, A54; :: thesis:

end;

A62: (card SS1) + Z <= degree K by A3, A16, A27, A30, A33, Th33;
A63: X c= {(S \/ ((center_of_mass V) .: {W1})),(S \/ ((center_of_mass V) .: {W2}))}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
A64: ( n + 1 = (degree K) + 1 & n = ((degree K) + 1) - 1 ) by A3, XXREAL_3:22, XXREAL_3:def 2;
assume x in X ; :: thesis:
then consider W being Simplex of n, BCS K such that
A65: x = W and
A66: S c= W by A11;
consider T being finite simplex-like Subset-Family of K such that
A67: T misses SS1 and
A68: ( T \/ SS1 is c=-linear & T \/ SS1 is with_non-empty_elements ) and
A69: card T = Z + 1 and
A70: @ W = ((center_of_mass V) .: SS1) \/ ((center_of_mass V) .: T) by A16, A36, A50, A62, A66, Th41;
consider t being object such that
A71: T = {t} by A69, CARD_2:42;
set TS = T \/ SS1;
A72: card (T \/ SS1) = n + 1 by A16, A36, A67, A69, CARD_2:40;
A73: union (T \/ SS1) in T \/ SS1 by A68, A71, SIMPLEX0:9;
T \/ SS1 is simplex-like by TOPS_2:13;
then reconsider UTS = union (T \/ SS1) as Simplex of K by A73;
Segm (card (T \/ SS1)) c= Segm (card UTS) by A68, SIMPLEX0:10;
then A74: card (T \/ SS1) <= card UTS by NAT_1:39;
UTS in T

proof

assume not UTS in T ; :: thesis:
then UTS in SS1 by A73, XBOOLE_0:def 3;
then card UTS <= card U by NAT_1:43, ZFMISC_1:74;
hence contradiction by A43, A72, A74, NAT_1:13; :: thesis:

end;

then A75: UTS = t by A71, TARSKI:def 1;
card UTS <= (degree K) + 1 by SIMPLEX0:24;
then card UTS <= n + 1 by A3, XXREAL_3:def 2;
then card UTS = n + 1 by A72, A74, XXREAL_0:1;
then A76: UTS is Simplex of n,K by A64, SIMPLEX0:48;
U c= UTS by XBOOLE_1:7, ZFMISC_1:77;
then UTS in { W where W is Simplex of n,K : U c= W } by A76;
then ( W = ((center_of_mass V) .: SS1) \/ ((center_of_mass V) .: {W1}) or W = ((center_of_mass V) .: SS1) \/ ((center_of_mass V) .: {W2}) ) by A47, A48, A51, A70, A71, A75, TARSKI:def 2;
hence x in {(S \/ ((center_of_mass V) .: {W1})),(S \/ ((center_of_mass V) .: {W2}))} by A35, A65, TARSKI:def 2; :: thesis:

end;

end;

proof

A95: Carrier (((center_of_mass V) . U) |-- (@ U)) c= U by RLVECT_2:def 6;

A96: now :: thesis:

let i be Nat; :: thesis:
assume A97: i in dom F ; :: thesis:
A98: F . i = ((((center_of_mass V) . U) |-- (@ U)) . (G . i)) * (((G . i) |-- A) . ab) by A93, A97;
A99: G . i in rng G by A94, A97, FUNCT_1:def 3;
then G . i in U by A92, A95;
then A100: ((G . i) |-- A) . ab >= 0 by A7, A86, RLAFFIN1:71;
(((center_of_mass V) . U) |-- (@ U)) . (G . i) = 1 / (card U) by A92, A95, A99, RLAFFIN2:18;
hence 0 <= F . i by A98, A100; :: thesis:

end;

(center_of_mass V) . U in conv (@ S) by A84;
then A101: (center_of_mass V) . U in conv BB by A80;
assume not U c= conv B1 ; :: thesis:
then consider t being object such that
A102: t in U and
A103: not t in conv B1 ;
reconsider tt = t as set by TARSKI:1;
A104: (t |-- A) . ab > 0

proof

A \ {ab} c= B1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in A \ {ab} ; :: thesis:
then ( x in A & not x in {ab} ) by XBOOLE_0:def 5;
hence x in B1 by A83, XBOOLE_0:def 5; :: thesis:

end;

then A105: conv (A \ {ab}) c= conv B1 by RLAFFIN1:3;
assume A106: (t |-- A) . ab <= 0 ; :: thesis:
(t |-- A) . ab >= 0 by A7, A86, A102, RLAFFIN1:71;
then for x being set st x in {ab} holds
(t |-- A) . x = 0 by A106, TARSKI:def 1;
then t in conv (A \ {ab}) by A7, A86, A102, RLAFFIN1:76;
hence contradiction by A103, A105; :: thesis:

end;

end;

then conv (@ U) c= conv B1 by CONVEX1:30;
then conv (@ U) misses Int A by A79, RLAFFIN2:7, XBOOLE_1:63;
then card { W where W is Simplex of n,K : U c= W } = 1 by A4, A44;
then consider w1 being object such that
A112: { W where W is Simplex of n,K : U c= W } = {w1} by CARD_2:42;
w1 in { W where W is Simplex of n,K : U c= W } by A112, TARSKI:def 1;
then consider W1 being Simplex of n,K such that
A113: w1 = W1 and
A114: U c= W1 ;
A115: (card SS1) + Z <= degree K by A3, A16, A27, A30, A33, Th33;
A116: X c= {(S \/ ((center_of_mass V) .: {W1}))}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
A117: n + 1 = (degree K) + 1 by A3, XXREAL_3:def 2;
assume x in X ; :: thesis:
then consider W being Simplex of n, BCS K such that
A118: x = W and
A119: S c= W by A11;
consider T being finite simplex-like Subset-Family of K such that
A120: T misses SS1 and
A121: ( T \/ SS1 is c=-linear & T \/ SS1 is with_non-empty_elements ) and
A122: card T = Z + 1 and
A123: @ W = ((center_of_mass V) .: SS1) \/ ((center_of_mass V) .: T) by A16, A36, A88, A115, A119, Th41;
consider t being object such that
A124: T = {t} by A122, CARD_2:42;
set TS = T \/ SS1;
A125: card (T \/ SS1) = n + 1 by A16, A36, A120, A122, CARD_2:40;
A126: union (T \/ SS1) in T \/ SS1 by A121, A124, SIMPLEX0:9;
T \/ SS1 is simplex-like by TOPS_2:13;
then reconsider UTS = union (T \/ SS1) as Simplex of K by A126;
Segm (card (T \/ SS1)) c= Segm (card UTS) by A121, SIMPLEX0:10;
then A127: card (T \/ SS1) <= card UTS by NAT_1:39;
UTS in T

proof

assume not UTS in T ; :: thesis:
then UTS in SS1 by A126, XBOOLE_0:def 3;
then card UTS <= card U by NAT_1:43, ZFMISC_1:74;
hence contradiction by A43, A125, A127, NAT_1:13; :: thesis:

end;

then A128: UTS = t by A124, TARSKI:def 1;
card UTS <= (degree K) + 1 by SIMPLEX0:24;
then card UTS <= n + 1 by A3, XXREAL_3:def 2;
then ( card UTS = n + 1 & SS1 c= T \/ SS1 ) by A125, A127, XBOOLE_1:7, XXREAL_0:1;
then ( U c= UTS & UTS is Simplex of n,K ) by A3, A117, SIMPLEX0:def 18, ZFMISC_1:77;
then UTS in { W where W is Simplex of n,K : U c= W } ;
then W = ((center_of_mass V) .: SS1) \/ ((center_of_mass V) .: {W1}) by A112, A113, A123, A124, A128, TARSKI:def 1;
hence x in {(S \/ ((center_of_mass V) .: {W1}))} by A35, A118, TARSKI:def 1; :: thesis:

end;

card W1 = (degree K) + 1 by A3, SIMPLEX0:def 18;
then card W1 = n + 1 by A3, XXREAL_3:def 2;
then { W where W is Simplex of n, BCS K : ( S c= W & conv (@ W) c= conv (@ W1) ) } = {(S \/ ((center_of_mass V) .: {W1}))} by A16, A27, A30, A33, A36, A43, A114, Th42;
then S \/ ((center_of_mass V) .: {W1}) in { W where W is Simplex of n, BCS K : ( S c= W & conv (@ W) c= conv (@ W1) ) } by TARSKI:def 1;
then ex R being Simplex of n, BCS K st
( R = S \/ ((center_of_mass V) .: {W1}) & S c= R & conv (@ R) c= conv (@ W1) ) ;
then S \/ ((center_of_mass V) .: {W1}) in X by A11;
then X = {(S \/ ((center_of_mass V) .: {W1}))} by A116, ZFMISC_1:33;
hence card X = 1 by CARD_1:30; :: thesis:

end;

suppose A129: card U = n + 1 ; :: thesis:

A130: conv (@ S) meets Int A

proof

proof

A149: Carrier (((center_of_mass V) . U) |-- (@ U)) c= U by RLVECT_2:def 6;

A150: now :: thesis:

let i be Nat; :: thesis:
assume A151: i in dom F ; :: thesis:
A152: F . i = ((((center_of_mass V) . U) |-- (@ U)) . (G . i)) * (((G . i) |-- A) . ab) by A146, A151;
A153: G . i in rng G by A147, A151, FUNCT_1:def 3;
then G . i in U by A145, A149;
then A154: ((G . i) |-- A) . ab >= 0 by A7, A140, RLAFFIN1:71;
(((center_of_mass V) . U) |-- (@ U)) . (G . i) = 1 / (card U) by A145, A149, A153, RLAFFIN2:18;
hence 0 <= F . i by A152, A154; :: thesis:

end;

(center_of_mass V) . U in conv (@ S) by A131;
then A155: (center_of_mass V) . U in conv BB by A135;
assume not U c= conv B1 ; :: thesis:
then consider t being object such that
A156: t in U and
A157: not t in conv B1 ;
reconsider tt = t as set by TARSKI:1;
U c= conv (@ U) by RLAFFIN1:2;
then A158: t in conv (@ U) by A156;
A159: (t |-- A) . ab > 0

proof

assume A160: (t |-- A) . ab <= 0 ; :: thesis:
(t |-- A) . ab >= 0 by A7, A41, A158, RLAFFIN1:71;
then for y being set st y in A \ B1 holds
(t |-- A) . y = 0 by A139, A160, TARSKI:def 1;
hence contradiction by A7, A41, A139, A148, A157, A158, RLAFFIN1:76; :: thesis:

end;

end;

then conv (@ U) c= conv B1 by CONVEX1:30;
then Affin (@ U) c= Affin B1 by RLAFFIN1:68;
hence contradiction by A129, A138, RLAFFIN1:79; :: thesis:

end;

set XX = { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } ;
A166: card { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } = 2 by A16, A30, A35, A36, A129, Th43;
consider w1, w2 being object such that
w1 <> w2 and
A167: { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } = {w1,w2} by A166, CARD_2:60;
w2 in { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } by A167, TARSKI:def 2;
then consider W2 being Simplex of n, BCS K such that
A168: w2 = W2 and
A169: S c= W2 and
conv (@ W2) c= conv (@ U) ;
w1 in { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } by A167, TARSKI:def 2;
then consider W1 being Simplex of n, BCS K such that
A170: w1 = W1 and
A171: S c= W1 and
conv (@ W1) c= conv (@ U) ;
A172: W1 in X by A11, A171;
A173: X c= { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) }

proof

let w be object ; :: according to TARSKI:def 3 :: thesis:
assume w in X ; :: thesis:
then consider W being Simplex of n, BCS K such that
A174: w = W and
A175: S c= W by A11;
(card SS1) + Z <= degree K by A3, A16, A27, A30, A33, Th33;
then consider T being finite simplex-like Subset-Family of K such that
T misses SS1 and
A176: ( T \/ SS1 is c=-linear & T \/ SS1 is with_non-empty_elements ) and
card T = Z + 1 and
A177: @ W = ((center_of_mass V) .: SS1) \/ ((center_of_mass V) .: T) by A27, A30, A33, A34, A175, Th41;
reconsider TS = T \/ SS1 as finite simplex-like Subset-Family of K by TOPS_2:13;
A178: W = (center_of_mass V) .: (@ TS) by A177, RELAT_1:120;
union TS in TS by A37, A176, SIMPLEX0:9;
then reconsider UTS = union TS as Simplex of K by TOPS_2:def 1;
card UTS <= (degree K) + 1 by SIMPLEX0:24;
then A179: card UTS <= n + 1 by A3, XXREAL_3:def 2;
A180: U c= union TS by XBOOLE_1:7, ZFMISC_1:77;
then n + 1 <= card UTS by A129, NAT_1:43;
then UTS = U by A129, A179, A180, CARD_2:102, XXREAL_0:1;
then conv (@ W) c= conv (@ U) by A178, CONVEX1:30, RLAFFIN2:17;
hence w in { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } by A174, A175; :: thesis:

end;

W2 in X by A11, A169;
then { S1 where S1 is Simplex of n, BCS K : ( S c= S1 & conv (@ S1) c= conv (@ U) ) } c= X by A167, A170, A168, A172, ZFMISC_1:32;
hence ( ( conv (@ S) meets Int A implies card X = 2 ) & ( conv (@ S) misses Int A implies card X = 1 ) ) by A130, A166, A173, XBOOLE_0:def 10; :: thesis:

end;