let n be Nat; :: thesis: for V being RealLinearSpace

for Aff being finite affinely-independent Subset of V

for Bf being finite Subset of V

for S being finite Subset-Family of V st S is with_non-empty_elements & union S c= Aff & ((card S) + n) + 1 <= card Aff holds

( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) iff ex T being finite Subset-Family of V st

( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) )

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

for Bf being finite Subset of V

for S being finite Subset-Family of V st S is with_non-empty_elements & union S c= Aff & ((card S) + n) + 1 <= card Aff holds

( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) iff ex T being finite Subset-Family of V st

( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) )

let Aff be finite affinely-independent Subset of V; :: thesis: for Bf being finite Subset of V

for S being finite Subset-Family of V st S is with_non-empty_elements & union S c= Aff & ((card S) + n) + 1 <= card Aff holds

( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) iff ex T being finite Subset-Family of V st

( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) )

let Bf be finite Subset of V; :: thesis: for S being finite Subset-Family of V st S is with_non-empty_elements & union S c= Aff & ((card S) + n) + 1 <= card Aff holds

( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) iff ex T being finite Subset-Family of V st

( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) )

let S be finite Subset-Family of V; :: thesis: ( S is with_non-empty_elements & union S c= Aff & ((card S) + n) + 1 <= card Aff implies ( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) iff ex T being finite Subset-Family of V st

( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) ) )

set B = center_of_mass V;

set U = union S;

assume that

A1: S is with_non-empty_elements and

A2: union S c= Aff and

A3: ((card S) + n) + 1 <= card Aff ; :: thesis: ( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) iff ex T being finite Subset-Family of V st

( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) )

set C = Complex_of {Aff};

reconsider c = card Aff as ExtReal ;

set BTC = (center_of_mass V) | the topology of (Complex_of {Aff});

set BC = BCS (Complex_of {Aff});

A4: the topology of (Complex_of {Aff}) = bool Aff by SIMPLEX0:4;

A5: degree (Complex_of {Aff}) = c - 1 by SIMPLEX0:26

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

reconsider c = (card S) + n as ExtReal ;

A6: |.(Complex_of {Aff}).| c= [#] (Complex_of {Aff}) ;

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

(card S) + n <= (card Aff) - 1 by A3, XREAL_1:19;

then A8: (card S) + n <= degree (BCS (Complex_of {Aff})) by A5, A6, Th31;

A24: ( T \/ S is c=-linear & T \/ S is with_non-empty_elements ) and

A25: card T = n + 1 and

A26: union T c= Aff and

A27: Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ; :: thesis: ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf )

reconsider TS = T \/ S as Subset-Family of (Complex_of {Aff}) ;

reconsider t = T as finite Subset-Family of V ;

A28: card TS = (card t) + (card S) by A23, CARD_2:40

.= ((card S) + n) + 1 by A25 ;

union (T \/ S) = (union T) \/ (union S) by ZFMISC_1:78;

then union (T \/ S) c= Aff by A2, A26, XBOOLE_1:8;

then ( T \/ S c= bool (union (T \/ S)) & bool (union (T \/ S)) c= bool Aff ) by ZFMISC_1:67, ZFMISC_1:82;

then A29: T \/ S c= the topology of (Complex_of {Aff}) by A4;

A30: TS is simplex-like

then reconsider BTS = (center_of_mass V) .: TS as Simplex of (BCS (Complex_of {Aff})) by A7, A24, A30, SIMPLEX0:def 20;

card TS = card ((center_of_mass V) .: TS) by A24, A30, Th33;

then A31: card BTS = c + 1 by A28, XXREAL_3:def 2;

BTS = Bf by A27, RELAT_1:120;

hence ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) by A8, A27, A31, SIMPLEX0:def 18, XBOOLE_1:7; :: thesis: verum

for Aff being finite affinely-independent Subset of V

for Bf being finite Subset of V

for S being finite Subset-Family of V st S is with_non-empty_elements & union S c= Aff & ((card S) + n) + 1 <= card Aff holds

( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) iff ex T being finite Subset-Family of V st

( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) )

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

for Bf being finite Subset of V

for S being finite Subset-Family of V st S is with_non-empty_elements & union S c= Aff & ((card S) + n) + 1 <= card Aff holds

( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) iff ex T being finite Subset-Family of V st

( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) )

let Aff be finite affinely-independent Subset of V; :: thesis: for Bf being finite Subset of V

for S being finite Subset-Family of V st S is with_non-empty_elements & union S c= Aff & ((card S) + n) + 1 <= card Aff holds

( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) iff ex T being finite Subset-Family of V st

( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) )

let Bf be finite Subset of V; :: thesis: for S being finite Subset-Family of V st S is with_non-empty_elements & union S c= Aff & ((card S) + n) + 1 <= card Aff holds

( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) iff ex T being finite Subset-Family of V st

( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) )

let S be finite Subset-Family of V; :: thesis: ( S is with_non-empty_elements & union S c= Aff & ((card S) + n) + 1 <= card Aff implies ( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) iff ex T being finite Subset-Family of V st

( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) ) )

set B = center_of_mass V;

set U = union S;

assume that

A1: S is with_non-empty_elements and

A2: union S c= Aff and

A3: ((card S) + n) + 1 <= card Aff ; :: thesis: ( ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) iff ex T being finite Subset-Family of V st

( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) )

set C = Complex_of {Aff};

reconsider c = card Aff as ExtReal ;

set BTC = (center_of_mass V) | the topology of (Complex_of {Aff});

set BC = BCS (Complex_of {Aff});

A4: the topology of (Complex_of {Aff}) = bool Aff by SIMPLEX0:4;

A5: degree (Complex_of {Aff}) = c - 1 by SIMPLEX0:26

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

reconsider c = (card S) + n as ExtReal ;

A6: |.(Complex_of {Aff}).| c= [#] (Complex_of {Aff}) ;

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

(card S) + n <= (card Aff) - 1 by A3, XREAL_1:19;

then A8: (card S) + n <= degree (BCS (Complex_of {Aff})) by A5, A6, Th31;

hereby :: thesis: ( ex T being finite Subset-Family of V st

( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) implies ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) )

given T being finite Subset-Family of V such that A23:
T misses S
and ( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) implies ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) )

A9:
S c= the topology of (Complex_of {Aff})

( dom (center_of_mass V) = (bool the carrier of V) \ {{}} & not {} in S ) by A1, FUNCT_2:def 1;

then ( dom ((center_of_mass V) | the topology of (Complex_of {Aff})) = (dom (center_of_mass V)) /\ the topology of (Complex_of {Aff}) & S c= dom (center_of_mass V) ) by RELAT_1:61, ZFMISC_1:34;

then A11: S c= dom ((center_of_mass V) | the topology of (Complex_of {Aff})) by A9, XBOOLE_1:19;

assume that

A12: Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) and

A13: (center_of_mass V) .: S c= Bf ; :: thesis: ex T being finite Subset-Family of V st

( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) )

consider a being c=-linear finite simplex-like Subset-Family of (Complex_of {Aff}) such that

A14: Bf = (center_of_mass V) .: a by A7, A12, SIMPLEX0:def 20;

a /\ (dom (center_of_mass V)) c= a by XBOOLE_1:17;

then reconsider AA = a /\ (dom (center_of_mass V)) as c=-linear finite simplex-like Subset-Family of (Complex_of {Aff}) by TOPS_2:11, XBOOLE_1:1;

A15: (center_of_mass V) .: S c= (center_of_mass V) .: AA by A13, A14, RELAT_1:112;

reconsider T = AA \ S as Subset-Family of V ;

A16: AA c= the topology of (Complex_of {Aff}) by SIMPLEX0:14;

then A17: (center_of_mass V) .: AA = ((center_of_mass V) | the topology of (Complex_of {Aff})) .: AA by RELAT_1:129;

A18: S \/ T = AA \/ S by XBOOLE_1:39

.= AA by A10, A11, A15, A17, FUNCT_1:87, XBOOLE_1:12 ;

T c= AA by XBOOLE_1:36;

then A19: T c= bool Aff by A4, A16;

A20: not {} in AA by ZFMISC_1:56;

then ( (center_of_mass V) .: a = (center_of_mass V) .: (a /\ (dom (center_of_mass V))) & AA is with_non-empty_elements ) by RELAT_1:112;

then A21: card Bf = card AA by A14, Th33;

A22: Bf = (center_of_mass V) .: AA by A14, RELAT_1:112

.= ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) by A18, RELAT_1:120 ;

reconsider T = T as finite Subset-Family of V ;

take T = T; :: thesis: ( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) )

card Bf = c + 1 by A8, A12, SIMPLEX0:def 18

.= ((card S) + n) + 1 by XXREAL_3:def 2 ;

then ( union (bool Aff) = Aff & (card S) + (card (AA \ S)) = ((card S) + n) + 1 ) by A18, A21, CARD_2:40, XBOOLE_1:79, ZFMISC_1:81;

hence ( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) by A18, A19, A20, A22, XBOOLE_1:79, ZFMISC_1:77; :: thesis: verum

end;proof

then A10:
(center_of_mass V) .: S = ((center_of_mass V) | the topology of (Complex_of {Aff})) .: S
by RELAT_1:129;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S or x in the topology of (Complex_of {Aff}) )

reconsider xx = x as set by TARSKI:1;

assume x in S ; :: thesis: x in the topology of (Complex_of {Aff})

then xx c= union S by ZFMISC_1:74;

then xx c= Aff by A2;

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

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

assume x in S ; :: thesis: x in the topology of (Complex_of {Aff})

then xx c= union S by ZFMISC_1:74;

then xx c= Aff by A2;

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

( dom (center_of_mass V) = (bool the carrier of V) \ {{}} & not {} in S ) by A1, FUNCT_2:def 1;

then ( dom ((center_of_mass V) | the topology of (Complex_of {Aff})) = (dom (center_of_mass V)) /\ the topology of (Complex_of {Aff}) & S c= dom (center_of_mass V) ) by RELAT_1:61, ZFMISC_1:34;

then A11: S c= dom ((center_of_mass V) | the topology of (Complex_of {Aff})) by A9, XBOOLE_1:19;

assume that

A12: Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) and

A13: (center_of_mass V) .: S c= Bf ; :: thesis: ex T being finite Subset-Family of V st

( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) )

consider a being c=-linear finite simplex-like Subset-Family of (Complex_of {Aff}) such that

A14: Bf = (center_of_mass V) .: a by A7, A12, SIMPLEX0:def 20;

a /\ (dom (center_of_mass V)) c= a by XBOOLE_1:17;

then reconsider AA = a /\ (dom (center_of_mass V)) as c=-linear finite simplex-like Subset-Family of (Complex_of {Aff}) by TOPS_2:11, XBOOLE_1:1;

A15: (center_of_mass V) .: S c= (center_of_mass V) .: AA by A13, A14, RELAT_1:112;

reconsider T = AA \ S as Subset-Family of V ;

A16: AA c= the topology of (Complex_of {Aff}) by SIMPLEX0:14;

then A17: (center_of_mass V) .: AA = ((center_of_mass V) | the topology of (Complex_of {Aff})) .: AA by RELAT_1:129;

A18: S \/ T = AA \/ S by XBOOLE_1:39

.= AA by A10, A11, A15, A17, FUNCT_1:87, XBOOLE_1:12 ;

T c= AA by XBOOLE_1:36;

then A19: T c= bool Aff by A4, A16;

A20: not {} in AA by ZFMISC_1:56;

then ( (center_of_mass V) .: a = (center_of_mass V) .: (a /\ (dom (center_of_mass V))) & AA is with_non-empty_elements ) by RELAT_1:112;

then A21: card Bf = card AA by A14, Th33;

A22: Bf = (center_of_mass V) .: AA by A14, RELAT_1:112

.= ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) by A18, RELAT_1:120 ;

reconsider T = T as finite Subset-Family of V ;

take T = T; :: thesis: ( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) )

card Bf = c + 1 by A8, A12, SIMPLEX0:def 18

.= ((card S) + n) + 1 by XXREAL_3:def 2 ;

then ( union (bool Aff) = Aff & (card S) + (card (AA \ S)) = ((card S) + n) + 1 ) by A18, A21, CARD_2:40, XBOOLE_1:79, ZFMISC_1:81;

hence ( T misses S & T \/ S is c=-linear & T \/ S is with_non-empty_elements & card T = n + 1 & union T c= Aff & Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ) by A18, A19, A20, A22, XBOOLE_1:79, ZFMISC_1:77; :: thesis: verum

A24: ( T \/ S is c=-linear & T \/ S is with_non-empty_elements ) and

A25: card T = n + 1 and

A26: union T c= Aff and

A27: Bf = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) ; :: thesis: ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf )

reconsider TS = T \/ S as Subset-Family of (Complex_of {Aff}) ;

reconsider t = T as finite Subset-Family of V ;

A28: card TS = (card t) + (card S) by A23, CARD_2:40

.= ((card S) + n) + 1 by A25 ;

union (T \/ S) = (union T) \/ (union S) by ZFMISC_1:78;

then union (T \/ S) c= Aff by A2, A26, XBOOLE_1:8;

then ( T \/ S c= bool (union (T \/ S)) & bool (union (T \/ S)) c= bool Aff ) by ZFMISC_1:67, ZFMISC_1:82;

then A29: T \/ S c= the topology of (Complex_of {Aff}) by A4;

A30: TS is simplex-like

proof

[#] (BCS (Complex_of {Aff})) = [#] (Complex_of {Aff})
by A7, SIMPLEX0:def 20;
let a be Subset of (Complex_of {Aff}); :: according to TOPS_2:def 1 :: thesis: ( not a in TS or not a is dependent )

thus ( not a in TS or not a is dependent ) by A29; :: thesis: verum

end;thus ( not a in TS or not a is dependent ) by A29; :: thesis: verum

then reconsider BTS = (center_of_mass V) .: TS as Simplex of (BCS (Complex_of {Aff})) by A7, A24, A30, SIMPLEX0:def 20;

card TS = card ((center_of_mass V) .: TS) by A24, A30, Th33;

then A31: card BTS = c + 1 by A28, XXREAL_3:def 2;

BTS = Bf by A27, RELAT_1:120;

hence ( Bf is Simplex of n + (card S), BCS (Complex_of {Aff}) & (center_of_mass V) .: S c= Bf ) by A8, A27, A31, SIMPLEX0:def 18, XBOOLE_1:7; :: thesis: verum