let V be RealLinearSpace; :: thesis: for S being finite finite-membered Subset-Family of V st S is c=-linear & S is with_non-empty_elements & card S = card (union S) holds

for A being non empty finite Subset of V st A misses union S & (union S) \/ A is affinely-independent holds

((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)})

let S be finite finite-membered Subset-Family of V; :: thesis: ( S is c=-linear & S is with_non-empty_elements & card S = card (union S) implies for A being non empty finite Subset of V st A misses union S & (union S) \/ A is affinely-independent holds

((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)}) )

assume that

A1: S is c=-linear and

A2: S is with_non-empty_elements and

A3: card S = card (union S) ; :: thesis: for A being non empty finite Subset of V st A misses union S & (union S) \/ A is affinely-independent holds

((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)})

set U = union S;

set B = center_of_mass V;

let A be non empty finite Subset of V; :: thesis: ( A misses union S & (union S) \/ A is affinely-independent implies ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)}) )

assume that

A4: A misses union S and

A5: (union S) \/ A is affinely-independent ; :: thesis: ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)})

reconsider UA = (union S) \/ A as finite affinely-independent Subset of V by A5;

set C = Complex_of {UA};

reconsider SUA = S \/ {UA} as Subset-Family of (Complex_of {UA}) ;

A6: union S c= UA by XBOOLE_1:7;

A7: the topology of (Complex_of {UA}) = bool UA by SIMPLEX0:4;

A8: SUA c= the topology of (Complex_of {UA})

A10: |.(Complex_of {UA}).| c= [#] (Complex_of {UA}) ;

then A11: BCS (Complex_of {UA}) = subdivision ((center_of_mass V),(Complex_of {UA})) by Def5;

then [#] (BCS (Complex_of {UA})) = [#] (Complex_of {UA}) by SIMPLEX0:def 20;

then reconsider BSUA = (center_of_mass V) .: SUA as Subset of (BCS (Complex_of {UA})) ;

SUA is c=-linear

reconsider c = card UA as ExtReal ;

A14: degree (Complex_of {UA}) = c - 1 by SIMPLEX0:26

.= (card UA) + (- 1) by XXREAL_3:def 2 ;

A15: UA <> union S

then A16: card SUA = (card S) + 1 by CARD_2:41;

union S c< UA by A6, A15;

then card (union S) < card UA by CARD_2:48;

then (card (union S)) + 1 <= card UA by NAT_1:13;

then A17: card (union S) <= (card UA) - 1 by XREAL_1:19;

reconsider c = card S as ExtReal ;

card BSUA = card SUA by A2, A9, Th33;

then A18: card BSUA = c + 1 by A16, XXREAL_3:def 2;

degree (BCS (Complex_of {UA})) = degree (Complex_of {UA}) by A10, Th31;

then BSUA is Simplex of card S, BCS (Complex_of {UA}) by A3, A14, A17, A18, SIMPLEX0:def 18;

hence ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)}) by RELAT_1:120; :: thesis: verum

for A being non empty finite Subset of V st A misses union S & (union S) \/ A is affinely-independent holds

((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)})

let S be finite finite-membered Subset-Family of V; :: thesis: ( S is c=-linear & S is with_non-empty_elements & card S = card (union S) implies for A being non empty finite Subset of V st A misses union S & (union S) \/ A is affinely-independent holds

((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)}) )

assume that

A1: S is c=-linear and

A2: S is with_non-empty_elements and

A3: card S = card (union S) ; :: thesis: for A being non empty finite Subset of V st A misses union S & (union S) \/ A is affinely-independent holds

((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)})

set U = union S;

set B = center_of_mass V;

let A be non empty finite Subset of V; :: thesis: ( A misses union S & (union S) \/ A is affinely-independent implies ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)}) )

assume that

A4: A misses union S and

A5: (union S) \/ A is affinely-independent ; :: thesis: ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)})

reconsider UA = (union S) \/ A as finite affinely-independent Subset of V by A5;

set C = Complex_of {UA};

reconsider SUA = S \/ {UA} as Subset-Family of (Complex_of {UA}) ;

A6: union S c= UA by XBOOLE_1:7;

A7: the topology of (Complex_of {UA}) = bool UA by SIMPLEX0:4;

A8: SUA c= the topology of (Complex_of {UA})

proof

A9:
SUA is simplex-like
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SUA or x in the topology of (Complex_of {UA}) )

reconsider xx = x as set by TARSKI:1;

assume x in SUA ; :: thesis: x in the topology of (Complex_of {UA})

then ( x in S or x in {UA} ) by XBOOLE_0:def 3;

then ( xx c= union S or x = UA ) by TARSKI:def 1, ZFMISC_1:74;

then xx c= UA by A6;

hence x in the topology of (Complex_of {UA}) by A7; :: thesis: verum

end;reconsider xx = x as set by TARSKI:1;

assume x in SUA ; :: thesis: x in the topology of (Complex_of {UA})

then ( x in S or x in {UA} ) by XBOOLE_0:def 3;

then ( xx c= union S or x = UA ) by TARSKI:def 1, ZFMISC_1:74;

then xx c= UA by A6;

hence x in the topology of (Complex_of {UA}) by A7; :: thesis: verum

proof

set BC = BCS (Complex_of {UA});
let A be Subset of (Complex_of {UA}); :: according to TOPS_2:def 1 :: thesis: ( not A in SUA or not A is dependent )

assume A in SUA ; :: thesis: not A is dependent

hence not A is dependent by A8; :: thesis: verum

end;assume A in SUA ; :: thesis: not A is dependent

hence not A is dependent by A8; :: thesis: verum

A10: |.(Complex_of {UA}).| c= [#] (Complex_of {UA}) ;

then A11: BCS (Complex_of {UA}) = subdivision ((center_of_mass V),(Complex_of {UA})) by Def5;

then [#] (BCS (Complex_of {UA})) = [#] (Complex_of {UA}) by SIMPLEX0:def 20;

then reconsider BSUA = (center_of_mass V) .: SUA as Subset of (BCS (Complex_of {UA})) ;

SUA is c=-linear

proof

then reconsider BSUA = BSUA as Simplex of (BCS (Complex_of {UA})) by A9, A11, SIMPLEX0:def 20;
let x, y be set ; :: according to ORDINAL1:def 8 :: thesis: ( not x in SUA or not y in SUA or x,y are_c=-comparable )

assume A12: ( x in SUA & y in SUA ) ; :: thesis: x,y are_c=-comparable

end;assume A12: ( x in SUA & y in SUA ) ; :: thesis: x,y are_c=-comparable

per cases
( ( x in S & y in S ) or ( x in S & y in {UA} ) or ( x in {UA} & y in S ) or ( x in {UA} & y in {UA} ) )
by A12, XBOOLE_0:def 3;

end;

suppose
( x in S & y in {UA} )
; :: thesis: x,y are_c=-comparable

then
( x c= union S & y = UA )
by TARSKI:def 1, ZFMISC_1:74;

then x c= y by A6;

hence x,y are_c=-comparable ; :: thesis: verum

end;then x c= y by A6;

hence x,y are_c=-comparable ; :: thesis: verum

suppose
( x in {UA} & y in S )
; :: thesis: x,y are_c=-comparable

then
( x = UA & y c= union S )
by TARSKI:def 1, ZFMISC_1:74;

then y c= x by A6;

hence x,y are_c=-comparable ; :: thesis: verum

end;then y c= x by A6;

hence x,y are_c=-comparable ; :: thesis: verum

reconsider c = card UA as ExtReal ;

A14: degree (Complex_of {UA}) = c - 1 by SIMPLEX0:26

.= (card UA) + (- 1) by XXREAL_3:def 2 ;

A15: UA <> union S

proof

not UA in S
by ZFMISC_1:74, A6, A15;
assume
UA = union S
; :: thesis: contradiction

then A c= union S by XBOOLE_1:7;

hence contradiction by A4, XBOOLE_1:67; :: thesis: verum

end;then A c= union S by XBOOLE_1:7;

hence contradiction by A4, XBOOLE_1:67; :: thesis: verum

then A16: card SUA = (card S) + 1 by CARD_2:41;

union S c< UA by A6, A15;

then card (union S) < card UA by CARD_2:48;

then (card (union S)) + 1 <= card UA by NAT_1:13;

then A17: card (union S) <= (card UA) - 1 by XREAL_1:19;

reconsider c = card S as ExtReal ;

card BSUA = card SUA by A2, A9, Th33;

then A18: card BSUA = c + 1 by A16, XXREAL_3:def 2;

degree (BCS (Complex_of {UA})) = degree (Complex_of {UA}) by A10, Th31;

then BSUA is Simplex of card S, BCS (Complex_of {UA}) by A3, A14, A17, A18, SIMPLEX0:def 18;

hence ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)}) by RELAT_1:120; :: thesis: verum