let V be RealLinearSpace; :: thesis: for I being affinely-independent Subset of V

for L being Linear_Combination of I st L is convex & Carrier L = I holds

Sum L in Int I

let I be affinely-independent Subset of V; :: thesis: for L being Linear_Combination of I st L is convex & Carrier L = I holds

Sum L in Int I

let L be Linear_Combination of I; :: thesis: ( L is convex & Carrier L = I implies Sum L in Int I )

assume that

A1: L is convex and

A2: Carrier L = I ; :: thesis: Sum L in Int I

reconsider I1 = I as non empty Subset of V by A1, A2, CONVEX1:21;

reconsider K = L as Linear_Combination of I1 ;

K in ConvexComb V by A1, CONVEX3:def 1;

then Sum K in { (Sum M) where M is Convex_Combination of I1 : M in ConvexComb V } by A1;

then A3: Sum K in conv I1 by CONVEX3:5;

A4: ( conv I1 c= Affin I1 & sum L = 1 ) by A1, RLAFFIN1:62, RLAFFIN1:65;

for A being Subset of V st A c< I holds

not Sum K in conv A

for L being Linear_Combination of I st L is convex & Carrier L = I holds

Sum L in Int I

let I be affinely-independent Subset of V; :: thesis: for L being Linear_Combination of I st L is convex & Carrier L = I holds

Sum L in Int I

let L be Linear_Combination of I; :: thesis: ( L is convex & Carrier L = I implies Sum L in Int I )

assume that

A1: L is convex and

A2: Carrier L = I ; :: thesis: Sum L in Int I

reconsider I1 = I as non empty Subset of V by A1, A2, CONVEX1:21;

reconsider K = L as Linear_Combination of I1 ;

K in ConvexComb V by A1, CONVEX3:def 1;

then Sum K in { (Sum M) where M is Convex_Combination of I1 : M in ConvexComb V } by A1;

then A3: Sum K in conv I1 by CONVEX3:5;

A4: ( conv I1 c= Affin I1 & sum L = 1 ) by A1, RLAFFIN1:62, RLAFFIN1:65;

for A being Subset of V st A c< I holds

not Sum K in conv A

proof

hence
Sum L in Int I
by A3, Def1; :: thesis: verum
let A be Subset of V; :: thesis: ( A c< I implies not Sum K in conv A )

assume A5: A c< I ; :: thesis: not Sum K in conv A

assume A6: Sum K in conv A ; :: thesis: contradiction

( conv A c= Affin A & A c= I ) by A5, RLAFFIN1:65;

then (Sum K) |-- A = (Sum K) |-- I by A6, RLAFFIN1:77

.= K by A3, A4, RLAFFIN1:def 7 ;

then I c= A by A2, RLVECT_2:def 6;

hence contradiction by A5, XBOOLE_0:def 8; :: thesis: verum

end;assume A5: A c< I ; :: thesis: not Sum K in conv A

assume A6: Sum K in conv A ; :: thesis: contradiction

( conv A c= Affin A & A c= I ) by A5, RLAFFIN1:65;

then (Sum K) |-- A = (Sum K) |-- I by A6, RLAFFIN1:77

.= K by A3, A4, RLAFFIN1:def 7 ;

then I c= A by A2, RLVECT_2:def 6;

hence contradiction by A5, XBOOLE_0:def 8; :: thesis: verum