let V be RealLinearSpace; for F being c=-linear Subset-Family of V st union F is affinely-independent & union F is finite holds
Int ((center_of_mass V) .: F) c= Int (union F)
set B = center_of_mass V;
let S be c=-linear Subset-Family of V; ( union S is affinely-independent & union S is finite implies Int ((center_of_mass V) .: S) c= Int (union S) )
assume A1:
( union S is affinely-independent & union S is finite )
; Int ((center_of_mass V) .: S) c= Int (union S)
reconsider BS = (center_of_mass V) .: S as affinely-independent Subset of V by A1, Th29;
set U = union S;
let x be object ; TARSKI:def 3 ( not x in Int ((center_of_mass V) .: S) or x in Int (union S) )
assume A2:
x in Int ((center_of_mass V) .: S)
; x in Int (union S)
not BS is empty
by A2;
then consider y being object such that
A3:
y in BS
;
consider X being object such that
A4:
X in dom (center_of_mass V)
and
A5:
X in S
and
(center_of_mass V) . X = y
by A3, FUNCT_1:def 6;
reconsider X = X as set by TARSKI:1;
( X c= union S & not X is empty )
by A4, A5, ZFMISC_1:56, ZFMISC_1:74;
then reconsider U = union S as non empty finite Subset of V by A1;
set xBS = x |-- BS;
A6:
Int BS c= conv BS
by Lm2;
then A7:
x |-- BS is convex
by A2, RLAFFIN1:71;
S c= bool U
then A8:
U in S
by A5, SIMPLEX0:9;
dom (center_of_mass V) = (bool the carrier of V) \ {{}}
by FUNCT_2:def 1;
then
U in dom (center_of_mass V)
by ZFMISC_1:56;
then A9:
(center_of_mass V) . U in BS
by A8, FUNCT_1:def 6;
then reconsider BU = (center_of_mass V) . U as Element of V ;
conv BS c= Affin BS
by RLAFFIN1:65;
then A10:
Int BS c= Affin BS
by A6;
then A11:
Sum (x |-- BS) = x
by A2, RLAFFIN1:def 7;
then
Carrier (x |-- BS) = BS
by A2, A6, Th11, RLAFFIN1:71;
then A12:
(x |-- BS) . BU <> 0
by A9, RLVECT_2:19;
then A13:
(x |-- BS) . BU > 0
by A2, A6, RLAFFIN1:71;
set xU = x |-- U;
A14:
conv U c= Affin U
by RLAFFIN1:65;
A15:
conv ((center_of_mass V) .: S) c= conv U
by Th17, CONVEX1:30;
then A16:
Int BS c= conv U
by A6;
then
Int BS c= Affin U
by A14;
then A17:
Sum (x |-- U) = x
by A1, A2, RLAFFIN1:def 7;
BS c= conv BS
by RLAFFIN1:2;
then A18:
(center_of_mass V) . U in conv BS
by A9;
per cases
( x = (center_of_mass V) . U or x <> BU )
;
suppose
x <> BU
;
x in Int (union S)then consider p being
Element of
V such that A19:
p in conv (BS \ {BU})
and A20:
Sum (x |-- BS) = (((x |-- BS) . BU) * BU) + ((1 - ((x |-- BS) . BU)) * p)
and
((1 / ((x |-- BS) . BU)) * (Sum (x |-- BS))) + ((1 - (1 / ((x |-- BS) . BU))) * p) = BU
by A7, A11, A12, Th1;
A21:
x = ((1 - ((x |-- BS) . BU)) * p) + (((x |-- BS) . BU) * BU)
by A2, A10, A20, RLAFFIN1:def 7;
(x |-- BS) . BU <= 1
by A2, A6, RLAFFIN1:71;
then A22:
1
- ((x |-- BS) . BU) >= 1
- 1
by XREAL_1:10;
A23:
BU in conv U
by A15, A18;
conv (BS \ {BU}) c= conv BS
by RLAFFIN1:3, XBOOLE_1:36;
then A24:
p in conv BS
by A19;
then
p in conv U
by A15;
then A25:
x |-- U = ((1 - ((x |-- BS) . BU)) * (p |-- U)) + (((x |-- BS) . BU) * (BU |-- U))
by A1, A14, A21, A23, RLAFFIN1:70;
A26:
U c= Carrier (x |-- U)
proof
let u be
object ;
TARSKI:def 3 ( not u in U or u in Carrier (x |-- U) )
assume A27:
u in U
;
u in Carrier (x |-- U)
then A28:
(x |-- U) . u =
(((1 - ((x |-- BS) . BU)) * (p |-- U)) . u) + ((((x |-- BS) . BU) * (BU |-- U)) . u)
by A25, RLVECT_2:def 10
.=
(((1 - ((x |-- BS) . BU)) * (p |-- U)) . u) + (((x |-- BS) . BU) * ((BU |-- U) . u))
by A27, RLVECT_2:def 11
.=
((1 - ((x |-- BS) . BU)) * ((p |-- U) . u)) + (((x |-- BS) . BU) * ((BU |-- U) . u))
by A27, RLVECT_2:def 11
;
(
(BU |-- U) . u = 1
/ (card U) &
(p |-- U) . u >= 0 )
by A1, A15, A24, A27, Th18, RLAFFIN1:71;
hence
u in Carrier (x |-- U)
by A13, A22, A27, A28;
verum
end;
Carrier (x |-- U) c= U
by RLVECT_2:def 6;
then
Carrier (x |-- U) = U
by A26;
hence
x in Int (union S)
by A1, A2, A16, A17, Th12, RLAFFIN1:71;
verum end;