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

for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & union Sf c= Aff holds

( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds

ex x being set st

( x in Sf & card x = n ) )

let Aff be finite affinely-independent Subset of V; :: thesis: for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & union Sf c= Aff holds

( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds

ex x being set st

( x in Sf & card x = n ) )

let Sf be c=-linear finite finite-membered Subset-Family of V; :: thesis: ( Sf is with_non-empty_elements & union Sf c= Aff implies ( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds

ex x being set st

( x in Sf & card x = n ) ) )

reconsider N = 0 as Nat ;

set U = union Sf;

assume that

A1: Sf is with_non-empty_elements and

A2: union Sf c= Aff ; :: thesis: ( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds

ex x being set st

( x in Sf & card x = n ) )

set B = center_of_mass V;

set C = Complex_of {Aff};

reconsider s = Sf as c=-linear finite Subset-Family of (Complex_of {Aff}) ;

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

Segm (card (union Sf)) c= Segm (card Aff) by A2, CARD_1:11;

then card (union Sf) <= card Aff by NAT_1:39;

then A4: ( N - 1 <= (card (union Sf)) - 1 & (card (union Sf)) - 1 <= (card Aff) - 1 ) by XREAL_1:9;

( Sf c= bool (union Sf) & bool (union Sf) c= bool Aff ) by A2, ZFMISC_1:67, ZFMISC_1:82;

then A5: s c= the topology of (Complex_of {Aff}) by A3;

A6: s is simplex-like

Segm (card Sf) c= Segm (card (union Sf)) by A1, SIMPLEX0:10;

then A8: card Sf <= card (union Sf) by NAT_1:39;

set BC = BCS (Complex_of {Aff});

reconsider c = card Aff as ExtReal ;

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

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

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

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

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

then reconsider BS = (center_of_mass V) .: Sf as Subset of (BCS (Complex_of {Aff})) ;

A12: N - 1 <= (card Aff) - 1 by XREAL_1:9;

A13: degree (BCS (Complex_of {Aff})) = degree (Complex_of {Aff}) by A10, Th31;

thus ( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) implies for n being Nat st 0 < n & n <= card (union Sf) holds

ex x being set st

( x in Sf & card x = n ) ) :: thesis: ( ( for n being Nat st 0 < n & n <= card (union Sf) holds

ex x being set st

( x in Sf & card x = n ) ) implies (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) )

ex x being set st

( x in Sf & card x = n ) ; :: thesis: (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff})

for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & union Sf c= Aff holds

( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds

ex x being set st

( x in Sf & card x = n ) )

let Aff be finite affinely-independent Subset of V; :: thesis: for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & union Sf c= Aff holds

( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds

ex x being set st

( x in Sf & card x = n ) )

let Sf be c=-linear finite finite-membered Subset-Family of V; :: thesis: ( Sf is with_non-empty_elements & union Sf c= Aff implies ( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds

ex x being set st

( x in Sf & card x = n ) ) )

reconsider N = 0 as Nat ;

set U = union Sf;

assume that

A1: Sf is with_non-empty_elements and

A2: union Sf c= Aff ; :: thesis: ( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds

ex x being set st

( x in Sf & card x = n ) )

set B = center_of_mass V;

set C = Complex_of {Aff};

reconsider s = Sf as c=-linear finite Subset-Family of (Complex_of {Aff}) ;

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

Segm (card (union Sf)) c= Segm (card Aff) by A2, CARD_1:11;

then card (union Sf) <= card Aff by NAT_1:39;

then A4: ( N - 1 <= (card (union Sf)) - 1 & (card (union Sf)) - 1 <= (card Aff) - 1 ) by XREAL_1:9;

( Sf c= bool (union Sf) & bool (union Sf) c= bool Aff ) by A2, ZFMISC_1:67, ZFMISC_1:82;

then A5: s c= the topology of (Complex_of {Aff}) by A3;

A6: s is simplex-like

proof

then A7:
card s = card ((center_of_mass V) .: Sf)
by A1, Th33;
let a be Subset of (Complex_of {Aff}); :: according to TOPS_2:def 1 :: thesis: ( not a in s or not a is dependent )

assume a in s ; :: thesis: not a is dependent

hence not a is dependent by A5; :: thesis: verum

end;assume a in s ; :: thesis: not a is dependent

hence not a is dependent by A5; :: thesis: verum

Segm (card Sf) c= Segm (card (union Sf)) by A1, SIMPLEX0:10;

then A8: card Sf <= card (union Sf) by NAT_1:39;

set BC = BCS (Complex_of {Aff});

reconsider c = card Aff as ExtReal ;

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

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

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

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

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

then reconsider BS = (center_of_mass V) .: Sf as Subset of (BCS (Complex_of {Aff})) ;

A12: N - 1 <= (card Aff) - 1 by XREAL_1:9;

A13: degree (BCS (Complex_of {Aff})) = degree (Complex_of {Aff}) by A10, Th31;

thus ( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) implies for n being Nat st 0 < n & n <= card (union Sf) holds

ex x being set st

( x in Sf & card x = n ) ) :: thesis: ( ( for n being Nat st 0 < n & n <= card (union Sf) holds

ex x being set st

( x in Sf & card x = n ) ) implies (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) )

proof

assume A32:
for n being Nat st 0 < n & n <= card (union Sf) holds
assume
(center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff})
; :: thesis: for n being Nat st 0 < n & n <= card (union Sf) holds

ex x being set st

( x in Sf & card x = n )

then reconsider BS = (center_of_mass V) .: Sf as Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) ;

reconsider c1 = (card (union Sf)) - 1 as ExtReal ;

let n be Nat; :: thesis: ( 0 < n & n <= card (union Sf) implies ex x being set st

( x in Sf & card x = n ) )

reconsider s = Sf as Subset-Family of (union Sf) by ZFMISC_1:82;

defpred S_{1}[ Nat] means ( $1 < card Sf implies ex x being finite set st

( x in Sf & card x = (card Sf) - $1 ) );

assume that

A14: 0 < n and

A15: n <= card (union Sf) ; :: thesis: ex x being set st

( x in Sf & card x = n )

A16: (card Sf) - 0 > (card Sf) - n by A14, XREAL_1:10;

A17: card BS = c1 + 1 by A4, A9, A13, SIMPLEX0:def 18

.= ((card (union Sf)) - 1) + 1 by XXREAL_3:def 2

.= card (union Sf) ;

then A18: not Sf is empty by A14, A15;

then consider s1 being Subset-Family of (union Sf) such that

A19: s c= s1 and

( s1 is with_non-empty_elements & s1 is c=-linear ) and

A20: card (union Sf) = card s1 and

A21: for Z being set st Z in s1 & card Z <> 1 holds

ex x being set st

( x in Z & Z \ {x} in s1 ) by A1, SIMPLEX0:9, SIMPLEX0:13;

card (union Sf) = card Sf by A1, A6, A17, Th33;

then A22: s = s1 by A19, A20, CARD_2:102;

A23: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
by A7, A17, A18, SIMPLEX0:9;

A31: for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A30, A23);

(card Sf) - n is Nat by A7, A15, A17, NAT_1:21;

then ex x being finite set st

( x in Sf & card x = (card Sf) - ((card Sf) - n) ) by A16, A31;

hence ex x being set st

( x in Sf & card x = n ) ; :: thesis: verum

end;ex x being set st

( x in Sf & card x = n )

then reconsider BS = (center_of_mass V) .: Sf as Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) ;

reconsider c1 = (card (union Sf)) - 1 as ExtReal ;

let n be Nat; :: thesis: ( 0 < n & n <= card (union Sf) implies ex x being set st

( x in Sf & card x = n ) )

reconsider s = Sf as Subset-Family of (union Sf) by ZFMISC_1:82;

defpred S

( x in Sf & card x = (card Sf) - $1 ) );

assume that

A14: 0 < n and

A15: n <= card (union Sf) ; :: thesis: ex x being set st

( x in Sf & card x = n )

A16: (card Sf) - 0 > (card Sf) - n by A14, XREAL_1:10;

A17: card BS = c1 + 1 by A4, A9, A13, SIMPLEX0:def 18

.= ((card (union Sf)) - 1) + 1 by XXREAL_3:def 2

.= card (union Sf) ;

then A18: not Sf is empty by A14, A15;

then consider s1 being Subset-Family of (union Sf) such that

A19: s c= s1 and

( s1 is with_non-empty_elements & s1 is c=-linear ) and

A20: card (union Sf) = card s1 and

A21: for Z being set st Z in s1 & card Z <> 1 holds

ex x being set st

( x in Z & Z \ {x} in s1 ) by A1, SIMPLEX0:9, SIMPLEX0:13;

card (union Sf) = card Sf by A1, A6, A17, Th33;

then A22: s = s1 by A19, A20, CARD_2:102;

A23: for n being Nat st S

S

proof

A30:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A24: S_{1}[n]
; :: thesis: S_{1}[n + 1]

assume A25: n + 1 < card Sf ; :: thesis: ex x being finite set st

( x in Sf & card x = (card Sf) - (n + 1) )

then consider X being finite set such that

A26: X in Sf and

A27: card X = (card Sf) - n by A24, NAT_1:13;

A28: (n + 1) - n < (card Sf) - n by A25, XREAL_1:9;

then consider x being set such that

A29: ( x in X & X \ {x} in Sf ) by A21, A22, A26, A27;

reconsider C = (card X) - 1 as Element of NAT by A27, A28, NAT_1:20;

take X \ {x} ; :: thesis: ( X \ {x} in Sf & card (X \ {x}) = (card Sf) - (n + 1) )

card X = C + 1 ;

hence ( X \ {x} in Sf & card (X \ {x}) = (card Sf) - (n + 1) ) by A27, A29, STIRL2_1:55; :: thesis: verum

end;assume A24: S

assume A25: n + 1 < card Sf ; :: thesis: ex x being finite set st

( x in Sf & card x = (card Sf) - (n + 1) )

then consider X being finite set such that

A26: X in Sf and

A27: card X = (card Sf) - n by A24, NAT_1:13;

A28: (n + 1) - n < (card Sf) - n by A25, XREAL_1:9;

then consider x being set such that

A29: ( x in X & X \ {x} in Sf ) by A21, A22, A26, A27;

reconsider C = (card X) - 1 as Element of NAT by A27, A28, NAT_1:20;

take X \ {x} ; :: thesis: ( X \ {x} in Sf & card (X \ {x}) = (card Sf) - (n + 1) )

card X = C + 1 ;

hence ( X \ {x} in Sf & card (X \ {x}) = (card Sf) - (n + 1) ) by A27, A29, STIRL2_1:55; :: thesis: verum

A31: for n being Nat holds S

(card Sf) - n is Nat by A7, A15, A17, NAT_1:21;

then ex x being finite set st

( x in Sf & card x = (card Sf) - ((card Sf) - n) ) by A16, A31;

hence ex x being set st

( x in Sf & card x = n ) ; :: thesis: verum

ex x being set st

( x in Sf & card x = n ) ; :: thesis: (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff})

per cases
( union Sf is empty or not union Sf is empty )
;

end;

suppose A33:
union Sf is empty
; :: thesis: (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff})

reconsider O = - 1 as ExtReal ;

A34: ( O <= degree (BCS (Complex_of {Aff})) & 0 = O + 1 ) by A9, A10, A12, Th31, XXREAL_3:7;

Sf is empty by A1, A33;

then A35: BS is empty ;

thus (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) by A33, A34, A35, SIMPLEX0:def 18; :: thesis: verum

end;A34: ( O <= degree (BCS (Complex_of {Aff})) & 0 = O + 1 ) by A9, A10, A12, Th31, XXREAL_3:7;

Sf is empty by A1, A33;

then A35: BS is empty ;

thus (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) by A33, A34, A35, SIMPLEX0:def 18; :: thesis: verum

suppose A36:
not union Sf is empty
; :: thesis: (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff})

reconsider c1 = (card (union Sf)) - 1 as ExtReal ;

consider x being set such that

A37: x in Sf and

card x = card (union Sf) by A32, A36;

defpred S_{1}[ object , object ] means ex D2 being set st

( D2 = $2 & card D2 = $1 );

A38: for x being object st x in Seg (card (union Sf)) holds

ex y being object st

( y in Sf & S_{1}[x,y] )

A40: for x being object st x in Seg (card (union Sf)) holds

S_{1}[x,f . x]
from FUNCT_2:sch 1(A38);

dom f = Seg (card (union Sf)) by A37, FUNCT_2:def 1;

then ( Segm (card (Seg (card (union Sf)))) = Segm (card (union Sf)) & Segm (card (Seg (card (union Sf)))) c= Segm (card Sf) ) by A44, CARD_1:10, FINSEQ_1:57;

then card (union Sf) <= card Sf by NAT_1:39;

then A45: card BS = card (union Sf) by A7, A8, XXREAL_0:1;

( BS is Simplex of (BCS (Complex_of {Aff})) & c1 + 1 = ((card (union Sf)) - 1) + 1 ) by A6, A11, SIMPLEX0:def 20, XXREAL_3:def 2;

hence (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) by A4, A9, A13, A45, SIMPLEX0:def 18; :: thesis: verum

end;consider x being set such that

A37: x in Sf and

card x = card (union Sf) by A32, A36;

defpred S

( D2 = $2 & card D2 = $1 );

A38: for x being object st x in Seg (card (union Sf)) holds

ex y being object st

( y in Sf & S

proof

consider f being Function of (Seg (card (union Sf))),Sf such that
let x be object ; :: thesis: ( x in Seg (card (union Sf)) implies ex y being object st

( y in Sf & S_{1}[x,y] ) )

assume A39: x in Seg (card (union Sf)) ; :: thesis: ex y being object st

( y in Sf & S_{1}[x,y] )

reconsider n = x as Nat by A39;

( 0 < n & n <= card (union Sf) ) by A39, FINSEQ_1:1;

then ex x being set st

( x in Sf & card x = n ) by A32;

hence ex y being object st

( y in Sf & S_{1}[x,y] )
; :: thesis: verum

end;( y in Sf & S

assume A39: x in Seg (card (union Sf)) ; :: thesis: ex y being object st

( y in Sf & S

reconsider n = x as Nat by A39;

( 0 < n & n <= card (union Sf) ) by A39, FINSEQ_1:1;

then ex x being set st

( x in Sf & card x = n ) by A32;

hence ex y being object st

( y in Sf & S

A40: for x being object st x in Seg (card (union Sf)) holds

S

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds

x1 = x2

then A44:
( rng f c= Sf & f is one-to-one )
by FUNCT_1:def 4;x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )

assume that

A41: x1 in dom f and

A42: ( x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2

A43: S_{1}[x2,f . x2]
by A40, A42;

S_{1}[x1,f . x1]
by A40, A41;

hence x1 = card (f . x1)

.= x2 by A42, A43 ;

:: thesis: verum

end;assume that

A41: x1 in dom f and

A42: ( x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2

A43: S

S

hence x1 = card (f . x1)

.= x2 by A42, A43 ;

:: thesis: verum

dom f = Seg (card (union Sf)) by A37, FUNCT_2:def 1;

then ( Segm (card (Seg (card (union Sf)))) = Segm (card (union Sf)) & Segm (card (Seg (card (union Sf)))) c= Segm (card Sf) ) by A44, CARD_1:10, FINSEQ_1:57;

then card (union Sf) <= card Sf by NAT_1:39;

then A45: card BS = card (union Sf) by A7, A8, XXREAL_0:1;

( BS is Simplex of (BCS (Complex_of {Aff})) & c1 + 1 = ((card (union Sf)) - 1) + 1 ) by A6, A11, SIMPLEX0:def 20, XXREAL_3:def 2;

hence (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) by A4, A9, A13, A45, SIMPLEX0:def 18; :: thesis: verum