let V be RealLinearSpace; 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; ( |.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 = (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
; 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 S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A6:
S1[
n]
;
S1[n + 1]
let S1,
S2 be
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) <= n + 1 & card (union S2) <= n + 1 & Int (@ A1) meets Int (@ A2) holds
A1 = A2let A1,
A2 be
Simplex of
(BCS Kas);
( 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)
;
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;
suppose A19:
card (union S1) = n + 1
;
A1 = A2then 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;
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} )
;
A1 = A2then
{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
[#] 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 =
(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 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 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
conv (@ A1) c= Affin (@ A1)
by RLAFFIN1:65;
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
conv (@ A2) c= Affin (@ A2)
by RLAFFIN1:65;
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
union s1u <> union S1
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 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
;
verum end; end;
end;
A81:
S1[ 0 ]
A89:
for n being Nat holds S1[n]
from NAT_1:sch 2(A81, A5);
now for A1, A2 being Subset of (BCS Kas) st A1 is simplex-like & A2 is simplex-like & Int (@ A1) meets Int (@ A2) holds
A1 = A2let A1,
A2 be
Subset of
(BCS Kas);
( 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)
;
A1 = A2consider 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;
verum end;
hence
BCS Kas is simplex-join-closed
by Th25; verum