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 S1[ 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 = () .: S1 & A2 = () .: S2 & card (union S1) <= \$1 & card (union S2) <= \$1 & Int (@ A1) meets Int (@ A2) holds
A1 = A2;
assume A1: |.Kas.| c= [#] Kas ; :: thesis:
then A2: BCS Kas = subdivision ((),Kas) by Def5;
A3: BCS Kas is affinely-independent by ;
A4: dom () = (bool the carrier of V) \ by FUNCT_2:def 1;
A5: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A6: S1[n] ; :: thesis: S1[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 = () .: S1 & A2 = () .: 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 = () .: S1 & A2 = () .: S2 & card (union S1) <= n + 1 & card (union S2) <= n + 1 & Int (@ A1) meets Int (@ A2) implies A1 = A2 )
assume that
A7: A1 = () .: S1 and
A8: A2 = () .: 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 ;
set U = union S1;
( S2 c= bool (union S2) & bool (@ (union S2)) c= bool the carrier of V ) by ;
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 ;
( S1 c= bool (union S1) & bool (@ (union S1)) c= bool the carrier of V ) by ;
then A16: S1 is Subset-Family of V by XBOOLE_1:1;
then A17: Int (() .: S1) c= Int (@ (union S1)) by ;
Int (@ (union S1)) meets Int (() .: S2) by ;
then Int (@ (union S1)) meets Int (@ (union S2)) by ;
then A18: union S1 = union S2 by ;
per cases ( card (union S1) <= n or card (union S1) = n + 1 ) by ;
suppose card (union S1) <= n ; :: thesis: A1 = A2
hence A1 = A2 by A6, A7, A8, A10, A18; :: thesis: verum
end;
suppose A19: card (union S1) = n + 1 ; :: thesis: A1 = A2
then A20: not @ (union S1) is empty ;
then A21: union S1 in dom () by ;
then A22: (center_of_mass V) . (union S1) in @ A1 by ;
then reconsider Bu = () . (union S1) as Element of V ;
A23: {Bu} c= @ A1 by ;
A24: (center_of_mass V) . (union S1) in @ A2 by ;
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 ;
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} ) ) ;
suppose ( A1 = {Bu} & A2 = {Bu} ) ; :: thesis: A1 = A2
hence A1 = A2 ; :: thesis: verum
end;
suppose A30: ( A1 = {Bu} & A2 <> {Bu} ) ; :: thesis: A1 = A2
then ( {Bu} c< @ A2 & Int (@ A1) = @ A1 ) by ;
hence A1 = A2 by ; :: thesis: verum
end;
suppose A31: ( A1 <> {Bu} & A2 = {Bu} ) ; :: thesis: A1 = A2
then ( {Bu} c< @ A1 & Int (@ A2) = @ A2 ) by ;
hence A1 = A2 by ; :: thesis: verum
end;
suppose ( A1 <> {Bu} & A2 <> {Bu} ) ; :: thesis: A1 = A2
then {Bu} c< @ A1 by A23;
then A32: Bu <> x by ;
( 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
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 ;
hence x in the topology of Kas ; :: thesis: verum
end;
[#] Kas c= the carrier of V by SIMPLEX0:def 9;
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 = () | the topology of Kas;
A35: S1 \ {(union S1)} c= S1 by XBOOLE_1:36;
A36: {(union S1)} c= S1 by ;
A37: union s2u c= union S1 by ;
union s2u <> union S1
proof
assume A38: union s2u = union S1 ; :: thesis: contradiction
then union s2u in s2u by ;
hence contradiction by A38, ZFMISC_1:56; :: thesis: verum
end;
then A39: union s2u c< union S1 by A37;
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 ;
then A42: conv (union S2U) c= conv (@ ((union S1) \ {xS2U})) by RLAFFIN1:3;
A43: x in conv (@ A1) by ;
then A44: (x |-- (@ A1)) . Bu <= 1 by ;
A45: (x |-- (@ A1)) . Bu < 1
proof
assume (x |-- (@ A1)) . Bu >= 1 ; :: thesis: contradiction
then (x |-- (@ A1)) . Bu = 1 by ;
hence contradiction by A3, A32, A43, RLAFFIN1:72; :: thesis: verum
end;
conv (@ A1) c= Affin (@ A1) by RLAFFIN1:65;
then A46: x = Sum (x |-- (@ A1)) by ;
then Bu in Carrier (x |-- (@ A1)) by ;
then A47: (x |-- (@ A1)) . Bu <> 0 by RLVECT_2:19;
x |-- (@ A1) is convex by ;
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 ;
A50: p1 in Int ((@ A1) \ {Bu}) by ;
A51: {Bu} = Im ((),(union S1)) by
.= () .: {(union S1)} by RELAT_1:def 16 ;
then A52: A1 \ {Bu} = ((() | the topology of Kas) .: S1) \ (() .: {(union S1)}) by
.= ((() | the topology of Kas) .: S1) \ ((() | the topology of Kas) .: {(union S1)}) by
.= (() | the topology of Kas) .: (S1 \ {(union S1)}) by FUNCT_1:64
.= () .: (S1 \ {(union S1)}) by ;
then conv ((@ A1) \ {Bu}) c= conv (union S1U) by ;
then A53: p1 in conv (union S1U) by A48;
card (union s2u) < n + 1 by ;
then A54: card (union s2u) <= n by NAT_1:13;
A55: union s1u c= union S1 by ;
A56: x in conv (@ A2) by ;
then A57: (x |-- (@ A2)) . Bu <= 1 by ;
A58: (x |-- (@ A2)) . Bu < 1
proof
assume (x |-- (@ A2)) . Bu >= 1 ; :: thesis: contradiction
then (x |-- (@ A2)) . Bu = 1 by ;
hence contradiction by A3, A32, A56, RLAFFIN1:72; :: thesis: verum
end;
conv (@ A2) c= Affin (@ A2) by RLAFFIN1:65;
then A59: x = Sum (x |-- (@ A2)) by ;
then Bu in Carrier (x |-- (@ A2)) by ;
then A60: (x |-- (@ A2)) . Bu <> 0 by RLVECT_2:19;
x |-- (@ A2) is convex by ;
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 ;
A63: p2 in Int ((@ A2) \ {Bu}) by ;
@ (union S1) is non empty finite Subset of V by A19;
then A64: Bu in Int (@ (union S1)) by ;
then A65: Bu in conv (@ (union S1)) by RLAFFIN2:def 1;
A66: S2 c= the topology of Kas
proof
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 ;
hence x in the topology of Kas ; :: thesis: verum
end;
union s1u <> union S1
proof
assume A68: union s1u = union S1 ; :: thesis: contradiction
then union s1u in s1u by ;
hence contradiction by A68, ZFMISC_1:56; :: thesis: verum
end;
then A69: union s1u c< union S1 by A55;
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 ;
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 ;
then (union S1) \ {xS1U} c< union S1 ;
then A73: not Bu in conv (@ ((union S1) \ {xS1U})) by ;
card (union s1u) < n + 1 by ;
then A74: card (union s1u) <= n by NAT_1:13;
( (union S1) \ {xS2U} c= union S1 & (union S1) \ {xS2U} <> union S1 ) by ;
then (union S1) \ {xS2U} c< union S1 ;
then A75: not Bu in conv (@ ((union S1) \ {xS2U})) by ;
A76: {(union S1)} c= S2 by ;
A77: S2 \ {(union S1)} c= S2 by XBOOLE_1:36;
A78: A2 \ {Bu} = ((() | the topology of Kas) .: S2) \ (() .: {(union S1)}) by
.= ((() | the topology of Kas) .: S2) \ ((() | the topology of Kas) .: {(union S1)}) by
.= (() | the topology of Kas) .: (S2 \ {(union S1)}) by FUNCT_1:64
.= () .: (S2 \ {(union S1)}) by ;
then conv ((@ A2) \ {Bu}) c= conv (union S2U) by ;
then A79: p2 in conv (union S2U) by A61;
x in conv (@ (union S1)) by ;
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 ;
( (@ 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
.= A2 by ;
:: thesis: verum
end;
end;
end;
end;
end;
A81: S1[ 0 ]
proof
let S1, S2 be c=-linear finite simplex-like Subset-Family of Kas; :: thesis: for A1, A2 being Simplex of (BCS Kas) st A1 = () .: S1 & A2 = () .: 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 = () .: S1 & A2 = () .: S2 & card (union S1) <= 0 & card (union S2) <= 0 & Int (@ A1) meets Int (@ A2) implies A1 = A2 )
assume that
A82: A1 = () .: S1 and
A2 = () .: 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 () and
A87: x in S1 and
(center_of_mass V) . x = y by ;
reconsider xx = x as set by TARSKI:1;
A88: x <> {} by ;
union S1 is empty by A83;
then xx c= {} by ;
hence A1 = A2 by A88; :: thesis: verum
end;
A89: for n being Nat holds S1[n] from NAT_1:sch 2(A81, A5);
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
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 = () .: S1 by ;
consider S2 being c=-linear finite simplex-like Subset-Family of Kas such that
A94: A2 = () .: S2 by ;
( 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;
hence BCS Kas is simplex-join-closed by Th25; :: thesis: verum