let V be RealLinearSpace; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( 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) ; :: thesis: 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

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;

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; :: thesis: ( 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 ) ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( 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) ; :: thesis: 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

proof

then A8:
U in S
by A5, SIMPLEX0:9;
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in S or s in bool U )

reconsider ss = s as set by TARSKI:1;

assume s in S ; :: thesis: s in bool U

then ss c= U by ZFMISC_1:74;

hence s in bool U ; :: thesis: verum

end;reconsider ss = s as set by TARSKI:1;

assume s in S ; :: thesis: s in bool U

then ss c= U by ZFMISC_1:74;

hence s in bool U ; :: thesis: verum

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 )
;

end;

suppose
x <> BU
; :: thesis: 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)

then Carrier (x |-- U) = U by A26;

hence x in Int (union S) by A1, A2, A16, A17, Th12, RLAFFIN1:71; :: thesis: verum

end;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

Carrier (x |-- U) c= U
by RLVECT_2:def 6;
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in U or u in Carrier (x |-- U) )

assume A27: u in U ; :: thesis: 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; :: thesis: verum

end;assume A27: u in U ; :: thesis: 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; :: thesis: verum

then Carrier (x |-- U) = U by A26;

hence x in Int (union S) by A1, A2, A16, A17, Th12, RLAFFIN1:71; :: thesis: verum