let V be RealLinearSpace; :: thesis: for Kas being non void affinely-independent simplex-join-closed SimplicialComplex of V st |.Kas.| c= [#] Kas holds

BCS Kas is simplex-join-closed

let Kas be non void affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis: ( |.Kas.| c= [#] Kas implies BCS Kas is simplex-join-closed )

set B = center_of_mass V;

set BC = BCS Kas;

defpred S_{1}[ Nat] means for S1, S2 being c=-linear finite simplex-like Subset-Family of Kas

for A1, A2 being Simplex of (BCS Kas) st A1 = (center_of_mass V) .: S1 & A2 = (center_of_mass V) .: S2 & card (union S1) <= $1 & card (union S2) <= $1 & Int (@ A1) meets Int (@ A2) holds

A1 = A2;

assume A1: |.Kas.| c= [#] Kas ; :: thesis: BCS Kas is simplex-join-closed

then A2: BCS Kas = subdivision ((center_of_mass V),Kas) by Def5;

A3: BCS Kas is affinely-independent by A1, Th28;

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

A5: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A81, A5);

BCS Kas is simplex-join-closed

let Kas be non void affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis: ( |.Kas.| c= [#] Kas implies BCS Kas is simplex-join-closed )

set B = center_of_mass V;

set BC = BCS Kas;

defpred S

for A1, A2 being Simplex of (BCS Kas) st A1 = (center_of_mass V) .: S1 & A2 = (center_of_mass V) .: S2 & card (union S1) <= $1 & card (union S2) <= $1 & Int (@ A1) meets Int (@ A2) holds

A1 = A2;

assume A1: |.Kas.| c= [#] Kas ; :: thesis: BCS Kas is simplex-join-closed

then A2: BCS Kas = subdivision ((center_of_mass V),Kas) by Def5;

A3: BCS Kas is affinely-independent by A1, Th28;

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

A5: for n being Nat st S

S

proof

A81:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A6: S_{1}[n]
; :: thesis: S_{1}[n + 1]

let S1, S2 be c=-linear finite simplex-like Subset-Family of Kas; :: thesis: for A1, A2 being Simplex of (BCS Kas) st A1 = (center_of_mass V) .: S1 & A2 = (center_of_mass V) .: S2 & card (union S1) <= n + 1 & card (union S2) <= n + 1 & Int (@ A1) meets Int (@ A2) holds

A1 = A2

let A1, A2 be Simplex of (BCS Kas); :: thesis: ( A1 = (center_of_mass V) .: S1 & A2 = (center_of_mass V) .: S2 & card (union S1) <= n + 1 & card (union S2) <= n + 1 & Int (@ A1) meets Int (@ A2) implies A1 = A2 )

assume that

A7: A1 = (center_of_mass V) .: S1 and

A8: A2 = (center_of_mass V) .: S2 and

A9: card (union S1) <= n + 1 and

card (union S2) <= n + 1 and

A10: Int (@ A1) meets Int (@ A2) ; :: thesis: A1 = A2

A11: ( union S2 in S2 or S2 is empty ) by SIMPLEX0:9;

then A12: union S2 is simplex-like by TOPS_2:def 1, ZFMISC_1:2;

set U = union S1;

( S2 c= bool (union S2) & bool (@ (union S2)) c= bool the carrier of V ) by ZFMISC_1:67, ZFMISC_1:82;

then A13: S2 is Subset-Family of V by XBOOLE_1:1;

A14: ( union S1 in S1 or S1 is empty ) by SIMPLEX0:9;

then A15: union S1 is simplex-like by TOPS_2:def 1, ZFMISC_1:2;

( S1 c= bool (union S1) & bool (@ (union S1)) c= bool the carrier of V ) by ZFMISC_1:67, ZFMISC_1:82;

then A16: S1 is Subset-Family of V by XBOOLE_1:1;

then A17: Int ((center_of_mass V) .: S1) c= Int (@ (union S1)) by A15, RLAFFIN2:30;

Int (@ (union S1)) meets Int ((center_of_mass V) .: S2) by A7, A8, A10, A15, A16, RLAFFIN2:30, XBOOLE_1:63;

then Int (@ (union S1)) meets Int (@ (union S2)) by A13, A12, RLAFFIN2:30, XBOOLE_1:63;

then A18: union S1 = union S2 by A12, A15, Th25;

end;assume A6: S

let S1, S2 be c=-linear finite simplex-like Subset-Family of Kas; :: thesis: for A1, A2 being Simplex of (BCS Kas) st A1 = (center_of_mass V) .: S1 & A2 = (center_of_mass V) .: S2 & card (union S1) <= n + 1 & card (union S2) <= n + 1 & Int (@ A1) meets Int (@ A2) holds

A1 = A2

let A1, A2 be Simplex of (BCS Kas); :: thesis: ( A1 = (center_of_mass V) .: S1 & A2 = (center_of_mass V) .: S2 & card (union S1) <= n + 1 & card (union S2) <= n + 1 & Int (@ A1) meets Int (@ A2) implies A1 = A2 )

assume that

A7: A1 = (center_of_mass V) .: S1 and

A8: A2 = (center_of_mass V) .: S2 and

A9: card (union S1) <= n + 1 and

card (union S2) <= n + 1 and

A10: Int (@ A1) meets Int (@ A2) ; :: thesis: A1 = A2

A11: ( union S2 in S2 or S2 is empty ) by SIMPLEX0:9;

then A12: union S2 is simplex-like by TOPS_2:def 1, ZFMISC_1:2;

set U = union S1;

( S2 c= bool (union S2) & bool (@ (union S2)) c= bool the carrier of V ) by ZFMISC_1:67, ZFMISC_1:82;

then A13: S2 is Subset-Family of V by XBOOLE_1:1;

A14: ( union S1 in S1 or S1 is empty ) by SIMPLEX0:9;

then A15: union S1 is simplex-like by TOPS_2:def 1, ZFMISC_1:2;

( S1 c= bool (union S1) & bool (@ (union S1)) c= bool the carrier of V ) by ZFMISC_1:67, ZFMISC_1:82;

then A16: S1 is Subset-Family of V by XBOOLE_1:1;

then A17: Int ((center_of_mass V) .: S1) c= Int (@ (union S1)) by A15, RLAFFIN2:30;

Int (@ (union S1)) meets Int ((center_of_mass V) .: S2) by A7, A8, A10, A15, A16, RLAFFIN2:30, XBOOLE_1:63;

then Int (@ (union S1)) meets Int (@ (union S2)) by A13, A12, RLAFFIN2:30, XBOOLE_1:63;

then A18: union S1 = union S2 by A12, A15, Th25;

per cases
( card (union S1) <= n or card (union S1) = n + 1 )
by A9, NAT_1:8;

end;

suppose A19:
card (union S1) = n + 1
; :: thesis: A1 = A2

then A20:
not @ (union S1) is empty
;

then A21: union S1 in dom (center_of_mass V) by A4, ZFMISC_1:56;

then A22: (center_of_mass V) . (union S1) in @ A1 by A7, A14, A19, FUNCT_1:def 6, ZFMISC_1:2;

then reconsider Bu = (center_of_mass V) . (union S1) as Element of V ;

A23: {Bu} c= @ A1 by A22, ZFMISC_1:31;

A24: (center_of_mass V) . (union S1) in @ A2 by A8, A11, A18, A19, A21, FUNCT_1:def 6, ZFMISC_1:2;

then A25: {Bu} c= @ A2 by ZFMISC_1:31;

A26: Bu in {Bu} by ZFMISC_1:31;

A27: conv {Bu} = {Bu} by RLAFFIN1:1;

consider x being object such that

A28: x in Int (@ A1) and

A29: x in Int (@ A2) by A10, XBOOLE_0:3;

reconsider x = x as Element of V by A28;

end;then A21: union S1 in dom (center_of_mass V) by A4, ZFMISC_1:56;

then A22: (center_of_mass V) . (union S1) in @ A1 by A7, A14, A19, FUNCT_1:def 6, ZFMISC_1:2;

then reconsider Bu = (center_of_mass V) . (union S1) as Element of V ;

A23: {Bu} c= @ A1 by A22, ZFMISC_1:31;

A24: (center_of_mass V) . (union S1) in @ A2 by A8, A11, A18, A19, A21, FUNCT_1:def 6, ZFMISC_1:2;

then A25: {Bu} c= @ A2 by ZFMISC_1:31;

A26: Bu in {Bu} by ZFMISC_1:31;

A27: conv {Bu} = {Bu} by RLAFFIN1:1;

consider x being object such that

A28: x in Int (@ A1) and

A29: x in Int (@ A2) by A10, XBOOLE_0:3;

reconsider x = x as Element of V by A28;

per cases
( ( A1 = {Bu} & A2 = {Bu} ) or ( A1 = {Bu} & A2 <> {Bu} ) or ( A1 <> {Bu} & A2 = {Bu} ) or ( A1 <> {Bu} & A2 <> {Bu} ) )
;

end;

suppose A30:
( A1 = {Bu} & A2 <> {Bu} )
; :: thesis: A1 = A2

then
( {Bu} c< @ A2 & Int (@ A1) = @ A1 )
by A25, RLAFFIN2:6;

hence A1 = A2 by A27, A28, A29, A30, RLAFFIN2:def 1; :: thesis: verum

end;hence A1 = A2 by A27, A28, A29, A30, RLAFFIN2:def 1; :: thesis: verum

suppose A31:
( A1 <> {Bu} & A2 = {Bu} )
; :: thesis: A1 = A2

then
( {Bu} c< @ A1 & Int (@ A2) = @ A2 )
by A23, RLAFFIN2:6;

hence A1 = A2 by A27, A28, A29, A31, RLAFFIN2:def 1; :: thesis: verum

end;hence A1 = A2 by A27, A28, A29, A31, RLAFFIN2:def 1; :: thesis: verum

suppose
( A1 <> {Bu} & A2 <> {Bu} )
; :: thesis: A1 = A2

then
{Bu} c< @ A1
by A23;

then A32: Bu <> x by A26, A27, A28, RLAFFIN2:def 1;

( S1 \ {(union S1)} c= S1 & S2 \ {(union S1)} c= S2 ) by XBOOLE_1:36;

then reconsider s1u = S1 \ {(union S1)}, s2u = S2 \ {(union S1)} as c=-linear finite simplex-like Subset-Family of Kas by TOPS_2:11;

A33: S1 c= the topology of Kas

then bool the carrier of Kas c= bool the carrier of V by ZFMISC_1:67;

then reconsider S1U = s1u, S2U = s2u as Subset-Family of V by XBOOLE_1:1;

set Bu1 = x |-- (@ A1);

set Bu2 = x |-- (@ A2);

set BT = (center_of_mass V) | the topology of Kas;

A35: S1 \ {(union S1)} c= S1 by XBOOLE_1:36;

A36: {(union S1)} c= S1 by A14, A19, ZFMISC_1:2, ZFMISC_1:31;

A37: union s2u c= union S1 by A18, XBOOLE_1:36, ZFMISC_1:77;

union s2u <> union S1

then consider xS2U being object such that

A40: xS2U in @ (union S1) and

A41: not xS2U in union S2U by XBOOLE_0:6;

reconsider xS2U = xS2U as Element of V by A40;

union S2U c= (union S1) \ {xS2U} by A37, A41, ZFMISC_1:34;

then A42: conv (union S2U) c= conv (@ ((union S1) \ {xS2U})) by RLAFFIN1:3;

A43: x in conv (@ A1) by A28, RLAFFIN2:def 1;

then A44: (x |-- (@ A1)) . Bu <= 1 by A3, RLAFFIN1:71;

A45: (x |-- (@ A1)) . Bu < 1

then A46: x = Sum (x |-- (@ A1)) by A3, A43, RLAFFIN1:def 7;

then Bu in Carrier (x |-- (@ A1)) by A3, A22, A28, A43, RLAFFIN1:71, RLAFFIN2:11;

then A47: (x |-- (@ A1)) . Bu <> 0 by RLVECT_2:19;

x |-- (@ A1) is convex by A3, A43, RLAFFIN1:71;

then consider p1 being Element of V such that

A48: p1 in conv ((@ A1) \ {Bu}) and

A49: x = (((x |-- (@ A1)) . Bu) * Bu) + ((1 - ((x |-- (@ A1)) . Bu)) * p1) and

((1 / ((x |-- (@ A1)) . Bu)) * x) + ((1 - (1 / ((x |-- (@ A1)) . Bu))) * p1) = Bu by A32, A46, A47, RLAFFIN2:1;

A50: p1 in Int ((@ A1) \ {Bu}) by A3, A22, A28, A48, A49, RLAFFIN2:14;

A51: {Bu} = Im ((center_of_mass V),(union S1)) by A21, FUNCT_1:59

.= (center_of_mass V) .: {(union S1)} by RELAT_1:def 16 ;

then A52: A1 \ {Bu} = (((center_of_mass V) | the topology of Kas) .: S1) \ ((center_of_mass V) .: {(union S1)}) by A33, A7, RELAT_1:129

.= (((center_of_mass V) | the topology of Kas) .: S1) \ (((center_of_mass V) | the topology of Kas) .: {(union S1)}) by A33, A36, RELAT_1:129, XBOOLE_1:1

.= ((center_of_mass V) | the topology of Kas) .: (S1 \ {(union S1)}) by FUNCT_1:64

.= (center_of_mass V) .: (S1 \ {(union S1)}) by A35, A33, RELAT_1:129, XBOOLE_1:1 ;

then conv ((@ A1) \ {Bu}) c= conv (union S1U) by CONVEX1:30, RLAFFIN2:17;

then A53: p1 in conv (union S1U) by A48;

card (union s2u) < n + 1 by A19, A39, CARD_2:48;

then A54: card (union s2u) <= n by NAT_1:13;

A55: union s1u c= union S1 by XBOOLE_1:36, ZFMISC_1:77;

A56: x in conv (@ A2) by A29, RLAFFIN2:def 1;

then A57: (x |-- (@ A2)) . Bu <= 1 by A3, RLAFFIN1:71;

A58: (x |-- (@ A2)) . Bu < 1

then A59: x = Sum (x |-- (@ A2)) by A3, A56, RLAFFIN1:def 7;

then Bu in Carrier (x |-- (@ A2)) by A3, A24, A29, A56, RLAFFIN1:71, RLAFFIN2:11;

then A60: (x |-- (@ A2)) . Bu <> 0 by RLVECT_2:19;

x |-- (@ A2) is convex by A3, A56, RLAFFIN1:71;

then consider p2 being Element of V such that

A61: p2 in conv ((@ A2) \ {Bu}) and

A62: x = (((x |-- (@ A2)) . Bu) * Bu) + ((1 - ((x |-- (@ A2)) . Bu)) * p2) and

((1 / ((x |-- (@ A2)) . Bu)) * x) + ((1 - (1 / ((x |-- (@ A2)) . Bu))) * p2) = Bu by A32, A59, A60, RLAFFIN2:1;

A63: p2 in Int ((@ A2) \ {Bu}) by A3, A24, A29, A61, A62, RLAFFIN2:14;

@ (union S1) is non empty finite Subset of V by A19;

then A64: Bu in Int (@ (union S1)) by A15, RLAFFIN2:20;

then A65: Bu in conv (@ (union S1)) by RLAFFIN2:def 1;

A66: S2 c= the topology of Kas

then consider xS1U being object such that

A70: xS1U in @ (union S1) and

A71: not xS1U in union S1U by XBOOLE_0:6;

reconsider xS1U = xS1U as Element of V by A70;

union S1U c= (union S1) \ {xS1U} by A55, A71, ZFMISC_1:34;

then A72: conv (union S1U) c= conv (@ ((union S1) \ {xS1U})) by RLAFFIN1:3;

( (union S1) \ {xS1U} c= union S1 & (union S1) \ {xS1U} <> union S1 ) by A70, ZFMISC_1:56;

then (union S1) \ {xS1U} c< union S1 ;

then A73: not Bu in conv (@ ((union S1) \ {xS1U})) by A64, RLAFFIN2:def 1;

card (union s1u) < n + 1 by A19, A69, CARD_2:48;

then A74: card (union s1u) <= n by NAT_1:13;

( (union S1) \ {xS2U} c= union S1 & (union S1) \ {xS2U} <> union S1 ) by A40, ZFMISC_1:56;

then (union S1) \ {xS2U} c< union S1 ;

then A75: not Bu in conv (@ ((union S1) \ {xS2U})) by A64, RLAFFIN2:def 1;

A76: {(union S1)} c= S2 by A11, A18, A19, ZFMISC_1:2, ZFMISC_1:31;

A77: S2 \ {(union S1)} c= S2 by XBOOLE_1:36;

A78: A2 \ {Bu} = (((center_of_mass V) | the topology of Kas) .: S2) \ ((center_of_mass V) .: {(union S1)}) by A66, A8, A51, RELAT_1:129

.= (((center_of_mass V) | the topology of Kas) .: S2) \ (((center_of_mass V) | the topology of Kas) .: {(union S1)}) by A76, A66, RELAT_1:129, XBOOLE_1:1

.= ((center_of_mass V) | the topology of Kas) .: (S2 \ {(union S1)}) by FUNCT_1:64

.= (center_of_mass V) .: (S2 \ {(union S1)}) by A66, A77, RELAT_1:129, XBOOLE_1:1 ;

then conv ((@ A2) \ {Bu}) c= conv (union S2U) by CONVEX1:30, RLAFFIN2:17;

then A79: p2 in conv (union S2U) by A61;

x in conv (@ (union S1)) by A7, A17, A28, RLAFFIN2:def 1;

then p2 = p1 by A15, A45, A49, A58, A62, A65, A42, A53, A75, A72, A73, A79, RLAFFIN2:2;

then A80: Int ((@ A1) \ {Bu}) meets Int ((@ A2) \ {Bu}) by A50, A63, XBOOLE_0:3;

( (@ A1) \ {Bu} = @ (A1 \ {Bu}) & (@ A2) \ {Bu} = @ (A2 \ {Bu}) ) ;

then A1 \ {Bu} = A2 \ {Bu} by A6, A54, A52, A74, A78, A80;

hence A1 = (A2 \ {Bu}) \/ {Bu} by A22, ZFMISC_1:116

.= A2 by A24, ZFMISC_1:116 ;

:: thesis: verum

end;then A32: Bu <> x by A26, A27, A28, RLAFFIN2:def 1;

( S1 \ {(union S1)} c= S1 & S2 \ {(union S1)} c= S2 ) by XBOOLE_1:36;

then reconsider s1u = S1 \ {(union S1)}, s2u = S2 \ {(union S1)} as c=-linear finite simplex-like Subset-Family of Kas by TOPS_2:11;

A33: S1 c= the topology of Kas

proof

[#] Kas c= the carrier of V
by SIMPLEX0:def 9;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S1 or x in the topology of Kas )

assume A34: x in S1 ; :: thesis: x in the topology of Kas

then reconsider A = x as Subset of Kas ;

A is simplex-like by A34, TOPS_2:def 1;

hence x in the topology of Kas ; :: thesis: verum

end;assume A34: x in S1 ; :: thesis: x in the topology of Kas

then reconsider A = x as Subset of Kas ;

A is simplex-like by A34, TOPS_2:def 1;

hence x in the topology of Kas ; :: thesis: verum

then bool the carrier of Kas c= bool the carrier of V by ZFMISC_1:67;

then reconsider S1U = s1u, S2U = s2u as Subset-Family of V by XBOOLE_1:1;

set Bu1 = x |-- (@ A1);

set Bu2 = x |-- (@ A2);

set BT = (center_of_mass V) | the topology of Kas;

A35: S1 \ {(union S1)} c= S1 by XBOOLE_1:36;

A36: {(union S1)} c= S1 by A14, A19, ZFMISC_1:2, ZFMISC_1:31;

A37: union s2u c= union S1 by A18, XBOOLE_1:36, ZFMISC_1:77;

union s2u <> union S1

proof

then A39:
union s2u c< union S1
by A37;
assume A38:
union s2u = union S1
; :: thesis: contradiction

then union s2u in s2u by A20, SIMPLEX0:9, ZFMISC_1:2;

hence contradiction by A38, ZFMISC_1:56; :: thesis: verum

end;then union s2u in s2u by A20, SIMPLEX0:9, ZFMISC_1:2;

hence contradiction by A38, ZFMISC_1:56; :: thesis: verum

then consider xS2U being object such that

A40: xS2U in @ (union S1) and

A41: not xS2U in union S2U by XBOOLE_0:6;

reconsider xS2U = xS2U as Element of V by A40;

union S2U c= (union S1) \ {xS2U} by A37, A41, ZFMISC_1:34;

then A42: conv (union S2U) c= conv (@ ((union S1) \ {xS2U})) by RLAFFIN1:3;

A43: x in conv (@ A1) by A28, RLAFFIN2:def 1;

then A44: (x |-- (@ A1)) . Bu <= 1 by A3, RLAFFIN1:71;

A45: (x |-- (@ A1)) . Bu < 1

proof

conv (@ A1) c= Affin (@ A1)
by RLAFFIN1:65;
assume
(x |-- (@ A1)) . Bu >= 1
; :: thesis: contradiction

then (x |-- (@ A1)) . Bu = 1 by A44, XXREAL_0:1;

hence contradiction by A3, A32, A43, RLAFFIN1:72; :: thesis: verum

end;then (x |-- (@ A1)) . Bu = 1 by A44, XXREAL_0:1;

hence contradiction by A3, A32, A43, RLAFFIN1:72; :: thesis: verum

then A46: x = Sum (x |-- (@ A1)) by A3, A43, RLAFFIN1:def 7;

then Bu in Carrier (x |-- (@ A1)) by A3, A22, A28, A43, RLAFFIN1:71, RLAFFIN2:11;

then A47: (x |-- (@ A1)) . Bu <> 0 by RLVECT_2:19;

x |-- (@ A1) is convex by A3, A43, RLAFFIN1:71;

then consider p1 being Element of V such that

A48: p1 in conv ((@ A1) \ {Bu}) and

A49: x = (((x |-- (@ A1)) . Bu) * Bu) + ((1 - ((x |-- (@ A1)) . Bu)) * p1) and

((1 / ((x |-- (@ A1)) . Bu)) * x) + ((1 - (1 / ((x |-- (@ A1)) . Bu))) * p1) = Bu by A32, A46, A47, RLAFFIN2:1;

A50: p1 in Int ((@ A1) \ {Bu}) by A3, A22, A28, A48, A49, RLAFFIN2:14;

A51: {Bu} = Im ((center_of_mass V),(union S1)) by A21, FUNCT_1:59

.= (center_of_mass V) .: {(union S1)} by RELAT_1:def 16 ;

then A52: A1 \ {Bu} = (((center_of_mass V) | the topology of Kas) .: S1) \ ((center_of_mass V) .: {(union S1)}) by A33, A7, RELAT_1:129

.= (((center_of_mass V) | the topology of Kas) .: S1) \ (((center_of_mass V) | the topology of Kas) .: {(union S1)}) by A33, A36, RELAT_1:129, XBOOLE_1:1

.= ((center_of_mass V) | the topology of Kas) .: (S1 \ {(union S1)}) by FUNCT_1:64

.= (center_of_mass V) .: (S1 \ {(union S1)}) by A35, A33, RELAT_1:129, XBOOLE_1:1 ;

then conv ((@ A1) \ {Bu}) c= conv (union S1U) by CONVEX1:30, RLAFFIN2:17;

then A53: p1 in conv (union S1U) by A48;

card (union s2u) < n + 1 by A19, A39, CARD_2:48;

then A54: card (union s2u) <= n by NAT_1:13;

A55: union s1u c= union S1 by XBOOLE_1:36, ZFMISC_1:77;

A56: x in conv (@ A2) by A29, RLAFFIN2:def 1;

then A57: (x |-- (@ A2)) . Bu <= 1 by A3, RLAFFIN1:71;

A58: (x |-- (@ A2)) . Bu < 1

proof

conv (@ A2) c= Affin (@ A2)
by RLAFFIN1:65;
assume
(x |-- (@ A2)) . Bu >= 1
; :: thesis: contradiction

then (x |-- (@ A2)) . Bu = 1 by A57, XXREAL_0:1;

hence contradiction by A3, A32, A56, RLAFFIN1:72; :: thesis: verum

end;then (x |-- (@ A2)) . Bu = 1 by A57, XXREAL_0:1;

hence contradiction by A3, A32, A56, RLAFFIN1:72; :: thesis: verum

then A59: x = Sum (x |-- (@ A2)) by A3, A56, RLAFFIN1:def 7;

then Bu in Carrier (x |-- (@ A2)) by A3, A24, A29, A56, RLAFFIN1:71, RLAFFIN2:11;

then A60: (x |-- (@ A2)) . Bu <> 0 by RLVECT_2:19;

x |-- (@ A2) is convex by A3, A56, RLAFFIN1:71;

then consider p2 being Element of V such that

A61: p2 in conv ((@ A2) \ {Bu}) and

A62: x = (((x |-- (@ A2)) . Bu) * Bu) + ((1 - ((x |-- (@ A2)) . Bu)) * p2) and

((1 / ((x |-- (@ A2)) . Bu)) * x) + ((1 - (1 / ((x |-- (@ A2)) . Bu))) * p2) = Bu by A32, A59, A60, RLAFFIN2:1;

A63: p2 in Int ((@ A2) \ {Bu}) by A3, A24, A29, A61, A62, RLAFFIN2:14;

@ (union S1) is non empty finite Subset of V by A19;

then A64: Bu in Int (@ (union S1)) by A15, RLAFFIN2:20;

then A65: Bu in conv (@ (union S1)) by RLAFFIN2:def 1;

A66: S2 c= the topology of Kas

proof

union s1u <> union S1
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S2 or x in the topology of Kas )

assume A67: x in S2 ; :: thesis: x in the topology of Kas

then reconsider A = x as Subset of Kas ;

A is simplex-like by A67, TOPS_2:def 1;

hence x in the topology of Kas ; :: thesis: verum

end;assume A67: x in S2 ; :: thesis: x in the topology of Kas

then reconsider A = x as Subset of Kas ;

A is simplex-like by A67, TOPS_2:def 1;

hence x in the topology of Kas ; :: thesis: verum

proof

then A69:
union s1u c< union S1
by A55;
assume A68:
union s1u = union S1
; :: thesis: contradiction

then union s1u in s1u by A20, SIMPLEX0:9, ZFMISC_1:2;

hence contradiction by A68, ZFMISC_1:56; :: thesis: verum

end;then union s1u in s1u by A20, SIMPLEX0:9, ZFMISC_1:2;

hence contradiction by A68, ZFMISC_1:56; :: thesis: verum

then consider xS1U being object such that

A70: xS1U in @ (union S1) and

A71: not xS1U in union S1U by XBOOLE_0:6;

reconsider xS1U = xS1U as Element of V by A70;

union S1U c= (union S1) \ {xS1U} by A55, A71, ZFMISC_1:34;

then A72: conv (union S1U) c= conv (@ ((union S1) \ {xS1U})) by RLAFFIN1:3;

( (union S1) \ {xS1U} c= union S1 & (union S1) \ {xS1U} <> union S1 ) by A70, ZFMISC_1:56;

then (union S1) \ {xS1U} c< union S1 ;

then A73: not Bu in conv (@ ((union S1) \ {xS1U})) by A64, RLAFFIN2:def 1;

card (union s1u) < n + 1 by A19, A69, CARD_2:48;

then A74: card (union s1u) <= n by NAT_1:13;

( (union S1) \ {xS2U} c= union S1 & (union S1) \ {xS2U} <> union S1 ) by A40, ZFMISC_1:56;

then (union S1) \ {xS2U} c< union S1 ;

then A75: not Bu in conv (@ ((union S1) \ {xS2U})) by A64, RLAFFIN2:def 1;

A76: {(union S1)} c= S2 by A11, A18, A19, ZFMISC_1:2, ZFMISC_1:31;

A77: S2 \ {(union S1)} c= S2 by XBOOLE_1:36;

A78: A2 \ {Bu} = (((center_of_mass V) | the topology of Kas) .: S2) \ ((center_of_mass V) .: {(union S1)}) by A66, A8, A51, RELAT_1:129

.= (((center_of_mass V) | the topology of Kas) .: S2) \ (((center_of_mass V) | the topology of Kas) .: {(union S1)}) by A76, A66, RELAT_1:129, XBOOLE_1:1

.= ((center_of_mass V) | the topology of Kas) .: (S2 \ {(union S1)}) by FUNCT_1:64

.= (center_of_mass V) .: (S2 \ {(union S1)}) by A66, A77, RELAT_1:129, XBOOLE_1:1 ;

then conv ((@ A2) \ {Bu}) c= conv (union S2U) by CONVEX1:30, RLAFFIN2:17;

then A79: p2 in conv (union S2U) by A61;

x in conv (@ (union S1)) by A7, A17, A28, RLAFFIN2:def 1;

then p2 = p1 by A15, A45, A49, A58, A62, A65, A42, A53, A75, A72, A73, A79, RLAFFIN2:2;

then A80: Int ((@ A1) \ {Bu}) meets Int ((@ A2) \ {Bu}) by A50, A63, XBOOLE_0:3;

( (@ A1) \ {Bu} = @ (A1 \ {Bu}) & (@ A2) \ {Bu} = @ (A2 \ {Bu}) ) ;

then A1 \ {Bu} = A2 \ {Bu} by A6, A54, A52, A74, A78, A80;

hence A1 = (A2 \ {Bu}) \/ {Bu} by A22, ZFMISC_1:116

.= A2 by A24, ZFMISC_1:116 ;

:: thesis: verum

proof

A89:
for n being Nat holds S
let S1, S2 be c=-linear finite simplex-like Subset-Family of Kas; :: thesis: for A1, A2 being Simplex of (BCS Kas) st A1 = (center_of_mass V) .: S1 & A2 = (center_of_mass V) .: S2 & card (union S1) <= 0 & card (union S2) <= 0 & Int (@ A1) meets Int (@ A2) holds

A1 = A2

let A1, A2 be Simplex of (BCS Kas); :: thesis: ( A1 = (center_of_mass V) .: S1 & A2 = (center_of_mass V) .: S2 & card (union S1) <= 0 & card (union S2) <= 0 & Int (@ A1) meets Int (@ A2) implies A1 = A2 )

assume that

A82: A1 = (center_of_mass V) .: S1 and

A2 = (center_of_mass V) .: S2 and

A83: card (union S1) <= 0 and

card (union S2) <= 0 and

A84: Int (@ A1) meets Int (@ A2) ; :: thesis: A1 = A2

not Int (@ A1) is empty by A84;

then not A1 is empty ;

then consider y being object such that

A85: y in A1 ;

consider x being object such that

A86: x in dom (center_of_mass V) and

A87: x in S1 and

(center_of_mass V) . x = y by A82, A85, FUNCT_1:def 6;

reconsider xx = x as set by TARSKI:1;

A88: x <> {} by A86, ZFMISC_1:56;

union S1 is empty by A83;

then xx c= {} by A87, ZFMISC_1:74;

hence A1 = A2 by A88; :: thesis: verum

end;A1 = A2

let A1, A2 be Simplex of (BCS Kas); :: thesis: ( A1 = (center_of_mass V) .: S1 & A2 = (center_of_mass V) .: S2 & card (union S1) <= 0 & card (union S2) <= 0 & Int (@ A1) meets Int (@ A2) implies A1 = A2 )

assume that

A82: A1 = (center_of_mass V) .: S1 and

A2 = (center_of_mass V) .: S2 and

A83: card (union S1) <= 0 and

card (union S2) <= 0 and

A84: Int (@ A1) meets Int (@ A2) ; :: thesis: A1 = A2

not Int (@ A1) is empty by A84;

then not A1 is empty ;

then consider y being object such that

A85: y in A1 ;

consider x being object such that

A86: x in dom (center_of_mass V) and

A87: x in S1 and

(center_of_mass V) . x = y by A82, A85, FUNCT_1:def 6;

reconsider xx = x as set by TARSKI:1;

A88: x <> {} by A86, ZFMISC_1:56;

union S1 is empty by A83;

then xx c= {} by A87, ZFMISC_1:74;

hence A1 = A2 by A88; :: thesis: verum

now :: thesis: for A1, A2 being Subset of (BCS Kas) st A1 is simplex-like & A2 is simplex-like & Int (@ A1) meets Int (@ A2) holds

A1 = A2

hence
BCS Kas is simplex-join-closed
by Th25; :: thesis: verumA1 = A2

let A1, A2 be Subset of (BCS Kas); :: thesis: ( A1 is simplex-like & A2 is simplex-like & Int (@ A1) meets Int (@ A2) implies A1 = A2 )

assume that

A90: A1 is simplex-like and

A91: A2 is simplex-like and

A92: Int (@ A1) meets Int (@ A2) ; :: thesis: A1 = A2

consider S1 being c=-linear finite simplex-like Subset-Family of Kas such that

A93: A1 = (center_of_mass V) .: S1 by A2, A90, SIMPLEX0:def 20;

consider S2 being c=-linear finite simplex-like Subset-Family of Kas such that

A94: A2 = (center_of_mass V) .: S2 by A2, A91, SIMPLEX0:def 20;

( card (union S1) <= card (union S2) or card (union S2) <= card (union S1) ) ;

hence A1 = A2 by A89, A90, A91, A92, A93, A94; :: thesis: verum

end;assume that

A90: A1 is simplex-like and

A91: A2 is simplex-like and

A92: Int (@ A1) meets Int (@ A2) ; :: thesis: A1 = A2

consider S1 being c=-linear finite simplex-like Subset-Family of Kas such that

A93: A1 = (center_of_mass V) .: S1 by A2, A90, SIMPLEX0:def 20;

consider S2 being c=-linear finite simplex-like Subset-Family of Kas such that

A94: A2 = (center_of_mass V) .: S2 by A2, A91, SIMPLEX0:def 20;

( card (union S1) <= card (union S2) or card (union S2) <= card (union S1) ) ;

hence A1 = A2 by A89, A90, A91, A92, A93, A94; :: thesis: verum