let k be Nat; :: thesis: for V being RealLinearSpace
for Aff being finite affinely-independent Subset of V
for F being Function of (Vertices (BCS (k,(Complex_of {Aff})))),Aff st ( for v being Vertex of (BCS (k,(Complex_of {Aff})))
for B being Subset of V st B c= Aff & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) : F .: S = Aff } = (2 * n) + 1
let V be RealLinearSpace; :: thesis: for Aff being finite affinely-independent Subset of V
for F being Function of (Vertices (BCS (k,(Complex_of {Aff})))),Aff st ( for v being Vertex of (BCS (k,(Complex_of {Aff})))
for B being Subset of V st B c= Aff & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) : F .: S = Aff } = (2 * n) + 1
let Aff be finite affinely-independent Subset of V; :: thesis: for F being Function of (Vertices (BCS (k,(Complex_of {Aff})))),Aff st ( for v being Vertex of (BCS (k,(Complex_of {Aff})))
for B being Subset of V st B c= Aff & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) : F .: S = Aff } = (2 * n) + 1
reconsider O = 1 as ExtReal ;
reconsider Z = 0 as ExtReal ;
defpred S1[ Nat] means for A being finite affinely-independent Subset of V st card A = $1 holds
for F being Function of (Vertices (BCS (k,(Complex_of {A})))),A st ( for v being Vertex of (BCS (k,(Complex_of {A})))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1;
A1: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A2: S1[m] ; :: thesis: S1[m + 1]
let A be finite affinely-independent Subset of V; :: thesis: ( card A = m + 1 implies for F being Function of (Vertices (BCS (k,(Complex_of {A})))),A st ( for v being Vertex of (BCS (k,(Complex_of {A})))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1 )
assume A3: card A = m + 1 ; :: thesis: for F being Function of (Vertices (BCS (k,(Complex_of {A})))),A st ( for v being Vertex of (BCS (k,(Complex_of {A})))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1
not A is empty by A3;
then consider a being object such that
A4: a in A ;
reconsider a = a as Element of V by A4;
A5: card (A \ {a}) = m by A3, A4, STIRL2_1:55;
reconsider Aa = A \ {a} as finite affinely-independent Subset of V by RLAFFIN1:43, XBOOLE_1:36;
set CAa = Complex_of {Aa};
the topology of (Complex_of {Aa}) = bool Aa by SIMPLEX0:4;
then A6: Vertices (Complex_of {Aa}) = union (bool Aa) by SIMPLEX0:16
.= Aa by ZFMISC_1:81 ;
A7: ( [#] (Complex_of {Aa}) = [#] V & |.(Complex_of {Aa}).| c= [#] V ) ;
then A8: Vertices (Complex_of {Aa}) c= Vertices (BCS (k,(Complex_of {Aa}))) by Th24;
set CA = Complex_of {A};
let F be Function of (Vertices (BCS (k,(Complex_of {A})))),A; :: thesis: ( ( for v being Vertex of (BCS (k,(Complex_of {A})))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) implies ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1 )
assume A9: for v being Vertex of (BCS (k,(Complex_of {A})))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ; :: thesis: ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1
set XX = { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } ;
A10: { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } c= the topology of (BCS (k,(Complex_of {A})))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } or x in the topology of (BCS (k,(Complex_of {A}))) )
assume x in { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } ; :: thesis: x in the topology of (BCS (k,(Complex_of {A})))
then ex S being Simplex of (card A) - 1, BCS (k,(Complex_of {A})) st
( S = x & A = F .: S ) ;
hence x in the topology of (BCS (k,(Complex_of {A}))) by PRE_TOPC:def 2; :: thesis: verum
end;
then reconsider XX = { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } as Subset-Family of (BCS (k,(Complex_of {A}))) by XBOOLE_1:1;
reconsider XX = XX as simplex-like Subset-Family of (BCS (k,(Complex_of {A}))) by A10, SIMPLEX0:14;
A11: ( [#] (Complex_of {A}) = [#] V & |.(Complex_of {A}).| c= [#] V ) ;
A12: A \ {a} c= A by XBOOLE_1:36;
for x being set st x in {Aa} holds
ex y being set st
( y in {A} & x c= y )
proof
let x be set ; :: thesis: ( x in {Aa} implies ex y being set st
( y in {A} & x c= y ) )
assume A13: x in {Aa} ; :: thesis: ex y being set st
( y in {A} & x c= y )
take A ; :: thesis: ( A in {A} & x c= A )
thus ( A in {A} & x c= A ) by A12, A13, TARSKI:def 1; :: thesis: verum
end;
then {Aa} is_finer_than {A} ;
then Complex_of {Aa} is SubSimplicialComplex of Complex_of {A} by SIMPLEX0:30;
then A14: BCS (k,(Complex_of {Aa})) is SubSimplicialComplex of BCS (k,(Complex_of {A})) by A11, A7, Th23;
then A15: Vertices (BCS (k,(Complex_of {Aa}))) c= Vertices (BCS (k,(Complex_of {A}))) by SIMPLEX0:31;
A16: the topology of (Complex_of {A}) = bool A by SIMPLEX0:4;
then A17: Vertices (Complex_of {A}) = union (bool A) by SIMPLEX0:16
.= A by ZFMISC_1:81 ;
A18: dom F = Vertices (BCS (k,(Complex_of {A}))) by A4, FUNCT_2:def 1;
per cases ( m = 0 or m > 0 ) ;
suppose A19: m = 0 ; :: thesis: ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1
A20: O - 1 = 0 by XXREAL_3:7;
then A21: degree (Complex_of {A}) = 0 by A3, A19, SIMPLEX0:26;
( k = 0 or k > 0 ) ;
then A22: BCS (k,(Complex_of {A})) = Complex_of {A} by A11, A21, Th16, Th22;
then A23: dom F = Vertices (Complex_of {A}) by A4, FUNCT_2:def 1;
take 0 ; :: thesis: card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * 0) + 1
A in bool A by ZFMISC_1:def 1;
then reconsider A1 = A as Simplex of (Complex_of {A}) by A16, PRE_TOPC:def 2;
A24: A1 is Simplex of 0 , Complex_of {A} by A3, A19, A20, SIMPLEX0:48;
ex x being object st A = {x} by A3, A19, CARD_2:42;
then A25: A = {a} by A4, TARSKI:def 1;
then conv A = A by RLAFFIN1:1;
then F . a in A by A4, A9, A17, A22;
then A26: F . a = a by A25, TARSKI:def 1;
A27: XX c= {A}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in XX or x in {A} )
assume x in XX ; :: thesis: x in {A}
then consider S being Simplex of 0 , Complex_of {A} such that
A28: x = S and
F .: S = A by A3, A19, A22;
A29: S in the topology of (Complex_of {A}) by PRE_TOPC:def 2;
card S = Z + 1 by A21, SIMPLEX0:def 18
.= 1 by XXREAL_3:4 ;
then S = A by A3, A16, A19, A29, CARD_2:102;
hence x in {A} by A28, TARSKI:def 1; :: thesis: verum
end;
F .: A = Im (F,a) by A25, RELAT_1:def 16
.= A by A4, A17, A23, A25, A26, FUNCT_1:59 ;
then A in XX by A3, A19, A24, A22;
then XX = {A} by A27, ZFMISC_1:33;
hence card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * 0) + 1 by CARD_1:30; :: thesis: verum
end;
suppose A30: m > 0 ; :: thesis: ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1
defpred S2[ object , object ] means ex D1, D2 being set st
( D1 = $1 & D2 = $2 & D1 c= D2 );
set XXA = { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ;
reconsider m1 = m - 1 as ExtReal ;
reconsider M = m as ExtReal ;
reconsider cA = card A as ExtReal ;
set YA = { S where S is Simplex of m, BCS (k,(Complex_of {A})) : Aa = F .: S } ;
A31: { S where S is Simplex of m, BCS (k,(Complex_of {A})) : Aa = F .: S } c= the topology of (BCS (k,(Complex_of {A})))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : Aa = F .: S } or x in the topology of (BCS (k,(Complex_of {A}))) )
assume x in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : Aa = F .: S } ; :: thesis: x in the topology of (BCS (k,(Complex_of {A})))
then ex S being Simplex of m, BCS (k,(Complex_of {A})) st
( S = x & Aa = F .: S ) ;
hence x in the topology of (BCS (k,(Complex_of {A}))) by PRE_TOPC:def 2; :: thesis: verum
end;
then reconsider YA = { S where S is Simplex of m, BCS (k,(Complex_of {A})) : Aa = F .: S } as Subset-Family of (BCS (k,(Complex_of {A}))) by XBOOLE_1:1;
reconsider YA = YA as simplex-like Subset-Family of (BCS (k,(Complex_of {A}))) by A31, SIMPLEX0:14;
defpred S3[ object , object ] means ex D1, D2 being set st
( D1 = $1 & D2 = $2 & D2 c= D1 );
set Xm1 = { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } ;
set Xm = { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } ;
consider R1 being Relation such that
A32: for x, y being object holds
( [x,y] in R1 iff ( x in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } & y in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } & S3[x,y] ) ) from RELAT_1:sch 1();
set DY = (dom R1) \ YA;
A33: (dom R1) \ YA c= XX
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (dom R1) \ YA or x in XX )
reconsider xx = x as set by TARSKI:1;
assume A34: x in (dom R1) \ YA ; :: thesis: x in XX
then consider y being object such that
A35: [x,y] in R1 by XTUPLE_0:def 12;
reconsider yy = y as set by TARSKI:1;
x in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } by A32, A35;
then consider S being Simplex of m, BCS (k,(Complex_of {A})) such that
A36: x = S and
verum ;
 not x in YA by A34, XBOOLE_0:def 5;
then A37: F .: S <> Aa by A36;
y in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } by A32, A35;
then A38: ex W being Simplex of m - 1, BCS (k,(Complex_of {A})) st
( y = W & Aa = F .: W ) ;
S3[xx,yy] by A32, A35;
then yy c= xx ;
then Aa c= F .: S by A36, A38, RELAT_1:123;
then Aa c< F .: S by A37;
then m < card (F .: S) by A5, CARD_2:48;
then A39: m + 1 <= card (F .: S) by NAT_1:13;
card (F .: S) <= m + 1 by A3, NAT_1:43;
then F .: S = A by A3, A39, CARD_2:102, XXREAL_0:1;
hence x in XX by A3, A36; :: thesis: verum
end;
set RDY = R1 | ((dom R1) \ YA);
A40: (R1 | ((dom R1) \ YA)) | ((dom (R1 | ((dom R1) \ YA))) \ ((dom R1) \ YA)) = {}
proof
assume (R1 | ((dom R1) \ YA)) | ((dom (R1 | ((dom R1) \ YA))) \ ((dom R1) \ YA)) <> {} ; :: thesis: contradiction
then consider xy being object such that
A41: xy in (R1 | ((dom R1) \ YA)) | ((dom (R1 | ((dom R1) \ YA))) \ ((dom R1) \ YA)) by XBOOLE_0:def 1;
consider x, y being object such that
A42: xy = [x,y] by A41, RELAT_1:def 1;
A43: x in (dom (R1 | ((dom R1) \ YA))) \ ((dom R1) \ YA) by A41, A42, RELAT_1:def 11;
then ( dom (R1 | ((dom R1) \ YA)) c= (dom R1) \ YA & x in dom (R1 | ((dom R1) \ YA)) ) by RELAT_1:58;
hence contradiction by A43, XBOOLE_0:def 5; :: thesis: verum
end;
A44: 2 *` (card YA) = (card 2) *` (card (card YA))
.= card (2 * (card YA)) by CARD_2:39 ;
cA - 1 = (m + 1) + (- 1) by A3, XXREAL_3:def 2;
then A45: degree (Complex_of {A}) = m by SIMPLEX0:26;
consider R being Relation such that
A46: for x, y being object holds
( [x,y] in R iff ( x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } & y in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } & S2[x,y] ) ) from RELAT_1:sch 1();
A47: card R = card R1
proof
deffunc H1( object ) -> object = [($1 `2),($1 `1)];
A48: for x being object st x in R holds
H1(x) in R1
proof
let z be object ; :: thesis: ( z in R implies H1(z) in R1 )
assume A49: z in R ; :: thesis: H1(z) in R1
then ex x, y being object st z = [x,y] by RELAT_1:def 1;
then A50: z = [(z `1),(z `2)] ;
then A51: z `2 in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } by A46, A49;
( S2[z `1 ,z `2 ] & z `1 in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } ) by A46, A49, A50;
hence H1(z) in R1 by A32, A51; :: thesis: verum
end;
consider f being Function of R,R1 such that
A52: for x being object st x in R holds
f . x = H1(x) from FUNCT_2:sch 2(A48);
per cases ( R1 is empty or not R1 is empty ) ;
suppose not R1 is empty ; :: thesis: card R = card R1
then A54: dom f = R by FUNCT_2:def 1;
R1 c= rng f
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in R1 or z in rng f )
assume A55: z in R1 ; :: thesis: z in rng f
then ex x, y being object st z = [x,y] by RELAT_1:def 1;
then A56: z = [(z `1),(z `2)] ;
then A57: z `2 in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } by A32, A55;
( S3[z `1 ,z `2 ] & z `1 in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } ) by A32, A55, A56;
then A58: [(z `2),(z `1)] in R by A46, A57;
H1([(z `2),(z `1)]) = z by A56;
then z = f . [(z `2),(z `1)] by A52, A58;
hence z in rng f by A54, A58, FUNCT_1:def 3; :: thesis: verum
end;
then A59: rng f = R1 ;
now :: thesis: for x1, x2 being object st x1 in R & x2 in R & f . x1 = f . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in R & x2 in R & f . x1 = f . x2 implies x1 = x2 )
assume that
A60: x1 in R and
A61: x2 in R and
A62: f . x1 = f . x2 ; :: thesis: x1 = x2
( f . x1 = H1(x1) & f . x2 = H1(x2) ) by A52, A60, A61;
then A63: ( x1 `2 = x2 `2 & x1 `1 = x2 `1 ) by A62, XTUPLE_0:1;
A64: ex x, y being object st x2 = [x,y] by A61, RELAT_1:def 1;
ex x, y being object st x1 = [x,y] by A60, RELAT_1:def 1;
hence x1 = [(x2 `1),(x2 `2)] by A63
.= x2 by A64 ;
:: thesis: verum
end;
then f is one-to-one by A54, FUNCT_1:def 4;
then R,R1 are_equipotent by A54, A59, WELLORD2:def 4;
hence card R = card R1 by CARD_1:5; :: thesis: verum
end;
end;
end;
A65: ( |.(BCS (k,(Complex_of {Aa}))).| = |.(Complex_of {Aa}).| & |.(Complex_of {Aa}).| = conv Aa ) by Th8, Th10;
set DX = (dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ;
A66: (dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } c= the topology of (BCS (k,(Complex_of {A})))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } or x in the topology of (BCS (k,(Complex_of {A}))) )
assume x in (dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ; :: thesis: x in the topology of (BCS (k,(Complex_of {A})))
then ex y being object st [x,y] in R by XTUPLE_0:def 12;
then x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } by A46;
then ex S being Simplex of m - 1, BCS (k,(Complex_of {A})) st
( S = x & Aa = F .: S ) ;
hence x in the topology of (BCS (k,(Complex_of {A}))) by PRE_TOPC:def 2; :: thesis: verum
end;
set RDX = R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } );
reconsider DX = (dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } as Subset-Family of (BCS (k,(Complex_of {A}))) by A66, XBOOLE_1:1;
reconsider DX = DX as simplex-like Subset-Family of (BCS (k,(Complex_of {A}))) by A66, SIMPLEX0:14;
A67: (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) | ((dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX) = {}
proof
assume (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) | ((dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX) <> {} ; :: thesis: contradiction
then consider xy being object such that
A68: xy in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) | ((dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX) by XBOOLE_0:def 1;
consider x, y being object such that
A69: xy = [x,y] by A68, RELAT_1:def 1;
A70: x in (dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX by A68, A69, RELAT_1:def 11;
then ( dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) c= DX & x in dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) ) by RELAT_1:58;
hence contradiction by A70, XBOOLE_0:def 5; :: thesis: verum
end;
A71: m1 + 1 = (m - 1) + 1 by XXREAL_3:def 2
.= m ;
set FA = F | (Vertices (BCS (k,(Complex_of {Aa}))));
A72: dom (F | (Vertices (BCS (k,(Complex_of {Aa}))))) = Vertices (BCS (k,(Complex_of {Aa}))) by A18, A14, RELAT_1:62, SIMPLEX0:31;
A73: not Vertices (BCS (k,(Complex_of {Aa}))) is empty by A5, A6, A8, A30;
A74: for v being Vertex of (BCS (k,(Complex_of {Aa})))
for B being Subset of V st B c= Aa & v in conv B holds
(F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in B
proof
let v be Vertex of (BCS (k,(Complex_of {Aa}))); :: thesis: for B being Subset of V st B c= Aa & v in conv B holds
(F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in B
let B be Subset of V; :: thesis: ( B c= Aa & v in conv B implies (F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in B )
assume A75: ( B c= Aa & v in conv B ) ; :: thesis: (F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in B
v in Vertices (BCS (k,(Complex_of {Aa}))) by A73;
then F . v in B by A9, A12, A15, A75, XBOOLE_1:1;
hence (F | (Vertices (BCS (k,(Complex_of {Aa}))))) . v in B by A72, A73, FUNCT_1:47; :: thesis: verum
end;
rng (F | (Vertices (BCS (k,(Complex_of {Aa}))))) c= Aa
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (F | (Vertices (BCS (k,(Complex_of {Aa}))))) or y in Aa )
assume y in rng (F | (Vertices (BCS (k,(Complex_of {Aa}))))) ; :: thesis: y in Aa
then consider x being object such that
A76: x in dom (F | (Vertices (BCS (k,(Complex_of {Aa}))))) and
A77: (F | (Vertices (BCS (k,(Complex_of {Aa}))))) . x = y by FUNCT_1:def 3;
reconsider v = x as Element of (BCS (k,(Complex_of {Aa}))) by A72, A76;
v is vertex-like by A72, A76, SIMPLEX0:def 4;
then consider S being Subset of (BCS (k,(Complex_of {Aa}))) such that
A78: S is simplex-like and
A79: v in S ;
A80: conv (@ S) c= |.(BCS (k,(Complex_of {Aa}))).| by A78, Th5;
S c= conv (@ S) by RLAFFIN1:2;
then A81: v in conv (@ S) by A79;
x in Vertices (BCS (k,(Complex_of {Aa}))) by A18, A14, A76, RELAT_1:62, SIMPLEX0:31;
hence y in Aa by A65, A74, A77, A80, A81; :: thesis: verum
end;
then reconsider FA = F | (Vertices (BCS (k,(Complex_of {Aa})))) as Function of (Vertices (BCS (k,(Complex_of {Aa})))),Aa by A72, FUNCT_2:2;
set XXa = { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } ;
consider n being Nat such that
A82: card { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } = (2 * n) + 1 by A2, A5, A74;
A83: ( m - 1 <= m - 0 & - 1 <= m + (- 1) ) by XREAL_1:10, XREAL_1:31;
A84: for x being object st x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } holds
card (Im (R,x)) = 1
proof
let x be object ; :: thesis: ( x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } implies card (Im (R,x)) = 1 )
assume x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ; :: thesis: card (Im (R,x)) = 1
then consider S being Simplex of m - 1, BCS (k,(Complex_of {A})) such that
A85: x = S and
A86: F .: S = Aa and
A87: conv (@ S) misses Int A ;
set XX = { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } ;
A88: R .: {S} c= { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 }
proof
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in R .: {S} or w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } )
reconsider ww = w as set by TARSKI:1;
assume w in R .: {S} ; :: thesis: w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 }
then consider s being object such that
A89: [s,w] in R and
A90: s in {S} by RELAT_1:def 13;
reconsider ss = s as set by TARSKI:1;
w in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } by A46, A89;
then A91: ex W being Simplex of m, BCS (k,(Complex_of {A})) st w = W ;
S2[ss,ww] by A46, A89;
then ( s = S & ss c= ww ) by A90, TARSKI:def 1;
hence w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } by A91; :: thesis: verum
end;
{ S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } c= R .: {S}
proof
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } or w in R .: {S} )
assume w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } ; :: thesis: w in R .: {S}
then consider W being Simplex of m, BCS (k,(Complex_of {A})) such that
A92: w = W and
A93: S c= W ;
( W in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } & S in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } ) by A86;
then ( S in {S} & [S,W] in R ) by A46, A93, TARSKI:def 1;
hence w in R .: {S} by A92, RELAT_1:def 13; :: thesis: verum
end;
then A94: R .: {S} = { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } by A88;
card { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } = 1 by A3, A87, Th45;
hence card (Im (R,x)) = 1 by A85, A94, RELAT_1:def 16; :: thesis: verum
end;
A95: degree (Complex_of {A}) = degree (BCS (k,(Complex_of {A}))) by A11, Th32;
A96: M + 1 = m + 1 by XXREAL_3:def 2;
A97: for x being object st x in YA holds
card (Im (R1,x)) = 2
proof
let x be object ; :: thesis: ( x in YA implies card (Im (R1,x)) = 2 )
assume x in YA ; :: thesis: card (Im (R1,x)) = 2
then consider S being Simplex of m, BCS (k,(Complex_of {A})) such that
A98: x = S and
A99: Aa = F .: S ;
set FS = F | S;
A100: rng (F | S) = Aa by A99, RELAT_1:115;
A101: not Aa is empty by A5, A30;
A102: S in {x} by A98, TARSKI:def 1;
A103: dom (F | S) = S by A18, RELAT_1:62, SIMPLEX0:17;
A104: card S = m + 1 by A95, A45, A96, SIMPLEX0:def 18;
reconsider FS = F | S as Function of S,Aa by A100, A103, FUNCT_2:1;
FS is onto by A100, FUNCT_2:def 3;
then consider b being set such that
A105: b in Aa and
A106: card (FS " {b}) = 2 and
A107: for x being set st x in Aa & x <> b holds
card (FS " {x}) = 1 by A5, A101, A104, Th2;
consider a1, a2 being object such that
A108: a1 <> a2 and
A109: FS " {b} = {a1,a2} by A106, CARD_2:60;
reconsider S1 = S \ {a1}, S2 = S \ {a2} as Simplex of (BCS (k,(Complex_of {A}))) ;
A110: a1 in {a1,a2} by TARSKI:def 2;
then A111: a1 in S2 by A108, A109, ZFMISC_1:56;
A112: card S1 = m by A104, A109, A110, STIRL2_1:55;
A113: a2 in {a1,a2} by TARSKI:def 2;
then A114: card S2 = m by A104, A109, STIRL2_1:55;
then reconsider S1 = S1, S2 = S2 as Simplex of m - 1, BCS (k,(Complex_of {A})) by A95, A83, A71, A45, A112, SIMPLEX0:def 18;
A115: {a1} c= S by A109, A110, ZFMISC_1:31;
A116: FS . a2 = F . a2 by A103, A109, A113, FUNCT_1:47;
A117: {a2} c= S by A109, A113, ZFMISC_1:31;
A118: R1 .: {x} c= {S1,S2}
proof
let Y be object ; :: according to TARSKI:def 3 :: thesis: ( not Y in R1 .: {x} or Y in {S1,S2} )
assume Y in R1 .: {x} ; :: thesis: Y in {S1,S2}
then consider X being object such that
A119: [X,Y] in R1 and
A120: X in {x} by RELAT_1:def 13;
Y in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } by A32, A119;
then consider W being Simplex of m - 1, BCS (k,(Complex_of {A})) such that
A121: Y = W and
A122: Aa = F .: W ;
X = x by A120, TARSKI:def 1;
then S3[S,W] by A32, A98, A119, A121;
then W c= S ;
then A123: Aa = FS .: W by A122, RELAT_1:129;
then consider w being object such that
A124: w in dom FS and
A125: w in W and
A126: FS . w = b by A105, FUNCT_1:def 6;
A127: {w} c= W by A125, ZFMISC_1:31;
A128: S \ {a1,a2} c= W
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in S \ {a1,a2} or s in W )
assume A129: s in S \ {a1,a2} ; :: thesis: s in W
then A130: s in dom FS by A103, XBOOLE_0:def 5;
then A131: FS . s in Aa by A100, FUNCT_1:def 3;
then consider w being object such that
A132: w in dom FS and
A133: w in W and
A134: FS . w = FS . s by A123, FUNCT_1:def 6;
not s in FS " {b} by A109, A129, XBOOLE_0:def 5;
then not FS . s in {b} by A130, FUNCT_1:def 7;
then FS . s <> b by TARSKI:def 1;
then card (FS " {(FS . s)}) = 1 by A107, A131;
then consider z being object such that
A135: FS " {(FS . s)} = {z} by CARD_2:42;
A136: FS . s in {(FS . s)} by TARSKI:def 1;
then A137: s in FS " {(FS . s)} by A130, FUNCT_1:def 7;
w in FS " {(FS . s)} by A132, A134, A136, FUNCT_1:def 7;
then w = z by A135, TARSKI:def 1;
hence s in W by A133, A135, A137, TARSKI:def 1; :: thesis: verum
end;
b in {b} by TARSKI:def 1;
then A138: w in FS " {b} by A124, A126, FUNCT_1:def 7;
A139: card W = m by A95, A83, A71, A45, SIMPLEX0:def 18;
A140: S /\ {a1} = {a1} by A115, XBOOLE_1:28;
A141: S /\ {a2} = {a2} by A117, XBOOLE_1:28;
per cases ( w = a1 or w = a2 ) by A109, A138, TARSKI:def 2;
suppose w = a1 ; :: thesis: Y in {S1,S2}
then (S \ {a1,a2}) \/ {w} = S \ ({a1,a2} \ {a1}) by A140, XBOOLE_1:52
.= S2 by A108, ZFMISC_1:17 ;
then S2 = W by A114, A127, A128, A139, CARD_2:102, XBOOLE_1:8;
hence Y in {S1,S2} by A121, TARSKI:def 2; :: thesis: verum
end;
suppose w = a2 ; :: thesis: Y in {S1,S2}
then (S \ {a1,a2}) \/ {w} = S \ ({a1,a2} \ {a2}) by A141, XBOOLE_1:52
.= S1 by A108, ZFMISC_1:17 ;
then S1 = W by A112, A127, A128, A139, CARD_2:102, XBOOLE_1:8;
hence Y in {S1,S2} by A121, TARSKI:def 2; :: thesis: verum
end;
end;
end;
A142: S c= dom F by A18, SIMPLEX0:17;
A143: FS . a1 = F . a1 by A103, A109, A110, FUNCT_1:47;
A144: FS . a1 in {b} by A109, A110, FUNCT_1:def 7;
then A145: FS . a1 = b by TARSKI:def 1;
A146: FS . a2 in {b} by A109, A113, FUNCT_1:def 7;
then A147: FS . a2 = b by TARSKI:def 1;
A148: ( a2 in S & a2 in S1 ) by A108, A109, A113, ZFMISC_1:56;
A149: Aa c= F .: S1
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Aa or z in F .: S1 )
assume A150: z in Aa ; :: thesis: z in F .: S1
per cases ( z = b or z <> b ) ;
suppose A152: z <> b ; :: thesis: z in F .: S1
consider c being object such that
A153: c in dom F and
A154: c in S and
A155: z = F . c by A99, A150, FUNCT_1:def 6;
c in S1 by A143, A145, A152, A154, A155, ZFMISC_1:56;
hence z in F .: S1 by A153, A155, FUNCT_1:def 6; :: thesis: verum
end;
end;
end;
A156: S in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } ;
A157: ( a1 in S & a1 in S2 ) by A108, A109, A110, ZFMISC_1:56;
A158: Aa c= F .: S2
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Aa or z in F .: S2 )
assume A159: z in Aa ; :: thesis: z in F .: S2
per cases ( z = b or z <> b ) ;
suppose A161: z <> b ; :: thesis: z in F .: S2
consider c being object such that
A162: c in dom F and
A163: c in S and
A164: z = F . c by A99, A159, FUNCT_1:def 6;
c in S2 by A116, A147, A161, A163, A164, ZFMISC_1:56;
hence z in F .: S2 by A162, A164, FUNCT_1:def 6; :: thesis: verum
end;
end;
end;
F .: S1 c= Aa by A99, RELAT_1:123, XBOOLE_1:36;
then Aa = F .: S1 by A149;
then ( S \ {a1} c= S & S1 in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } ) by XBOOLE_1:36;
then [S,S1] in R1 by A32, A156;
then A165: S1 in R1 .: {x} by A102, RELAT_1:def 13;
F .: S2 c= Aa by A99, RELAT_1:123, XBOOLE_1:36;
then Aa = F .: S2 by A158;
then ( S \ {a2} c= S & S2 in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } ) by XBOOLE_1:36;
then [S,S2] in R1 by A32, A156;
then S2 in R1 .: {x} by A102, RELAT_1:def 13;
then {S1,S2} c= R1 .: {x} by A165, ZFMISC_1:32;
then A166: R1 .: {x} = {S1,S2} by A118;
S1 <> S2 by A111, ZFMISC_1:56;
then card (R1 .: {x}) = 2 by A166, CARD_2:57;
hence card (Im (R1,x)) = 2 by RELAT_1:def 16; :: thesis: verum
end;
A167: M - 1 = m + (- 1) by XXREAL_3:def 2;
XX c= (dom R1) \ YA
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in XX or x in (dom R1) \ YA )
assume x in XX ; :: thesis: x in (dom R1) \ YA
then consider S being Simplex of m, BCS (k,(Complex_of {A})) such that
A168: x = S and
A169: F .: S = A by A3;
set FS = F | S;
A170: rng (F | S) = A by A169, RELAT_1:115;
A171: card A = card S by A3, A95, A45, A96, SIMPLEX0:def 18;
A172: dom (F | S) = S by A18, RELAT_1:62, SIMPLEX0:17;
then reconsider FS = F | S as Function of S,A by A170, FUNCT_2:1;
consider s being object such that
A173: ( s in dom FS & FS . s = a ) by A4, A170, FUNCT_1:def 3;
set Ss = S \ {s};
FS is onto by A170, FUNCT_2:def 3;
then A174: FS is one-to-one by A171, FINSEQ_4:63;
then A175: FS .: (S \ {s}) = (FS .: S) \ (FS .: {s}) by FUNCT_1:64
.= A \ (FS .: {s}) by A170, A172, RELAT_1:113
.= A \ (Im (FS,s)) by RELAT_1:def 16
.= Aa by A173, FUNCT_1:59 ;
S \ {s},FS .: (S \ {s}) are_equipotent by A172, A174, CARD_1:33, XBOOLE_1:36;
then A176: card (S \ {s}) = m by A5, A175, CARD_1:5;
reconsider Ss = S \ {s} as Simplex of (BCS (k,(Complex_of {A}))) ;
reconsider Ss = Ss as Simplex of m - 1, BCS (k,(Complex_of {A})) by A167, A176, SIMPLEX0:48;
FS .: Ss = F .: Ss by RELAT_1:129, XBOOLE_1:36;
then A177: Ss in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } by A175;
( Ss c= S & S in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } ) by XBOOLE_1:36;
then [S,Ss] in R1 by A32, A177;
then A178: S in dom R1 by XTUPLE_0:def 12;
for W being Simplex of m, BCS (k,(Complex_of {A})) st S = W holds
Aa <> F .: W by A4, A169, ZFMISC_1:56;
then not S in YA ;
hence x in (dom R1) \ YA by A168, A178, XBOOLE_0:def 5; :: thesis: verum
end;
then A179: (dom R1) \ YA = XX by A33;
for x being object st x in (dom R1) \ YA holds
card (Im ((R1 | ((dom R1) \ YA)),x)) = 1
proof
let x be object ; :: thesis: ( x in (dom R1) \ YA implies card (Im ((R1 | ((dom R1) \ YA)),x)) = 1 )
assume A180: x in (dom R1) \ YA ; :: thesis: card (Im ((R1 | ((dom R1) \ YA)),x)) = 1
then consider y being object such that
A181: [x,y] in R1 by XTUPLE_0:def 12;
A182: ex W being Simplex of m, BCS (k,(Complex_of {A})) st
( x = W & F .: W = A ) by A3, A179, A180;
x in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } by A32, A181;
then consider S being Simplex of m, BCS (k,(Complex_of {A})) such that
A183: x = S and
verum ;
 y in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } by A32, A181;
then consider W being Simplex of m - 1, BCS (k,(Complex_of {A})) such that
A184: y = W and
A185: Aa = F .: W ;
A186: card S = m + 1 by A95, A45, A96, SIMPLEX0:def 18;
A187: (R1 | ((dom R1) \ YA)) .: {x} c= {y}
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in (R1 | ((dom R1) \ YA)) .: {x} or u in {y} )
set FS = F | S;
assume u in (R1 | ((dom R1) \ YA)) .: {x} ; :: thesis: u in {y}
then consider s being object such that
A188: [s,u] in R1 | ((dom R1) \ YA) and
A189: s in {x} by RELAT_1:def 13;
A190: [s,u] in R1 by A188, RELAT_1:def 11;
then u in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } by A32;
then consider U being Simplex of m - 1, BCS (k,(Complex_of {A})) such that
A191: u = U and
A192: Aa = F .: U ;
A193: dom (F | S) = S by A18, RELAT_1:62, SIMPLEX0:17;
A194: rng (F | S) = A by A182, A183, RELAT_1:115;
then reconsider FS = F | S as Function of S,A by A193, FUNCT_2:1;
S3[S,W] by A32, A181, A183, A184;
then A195: W c= S ;
then A196: FS .: W = F .: W by RELAT_1:129;
s = S by A183, A189, TARSKI:def 1;
then S3[S,U] by A32, A190, A191;
then A197: U c= S ;
then A198: FS .: U = F .: U by RELAT_1:129;
FS is onto by A194, FUNCT_2:def 3;
then A199: FS is one-to-one by A3, A186, FINSEQ_4:63;
then A200: U c= W by A185, A192, A193, A196, A197, A198, FUNCT_1:87;
W c= U by A185, A192, A193, A195, A196, A198, A199, FUNCT_1:87;
then u = y by A184, A191, A200, XBOOLE_0:def 10;
hence u in {y} by TARSKI:def 1; :: thesis: verum
end;
( x in {x} & [x,y] in R1 | ((dom R1) \ YA) ) by A180, A181, RELAT_1:def 11, TARSKI:def 1;
then y in (R1 | ((dom R1) \ YA)) .: {x} by RELAT_1:def 13;
then (R1 | ((dom R1) \ YA)) .: {x} = {y} by A187, ZFMISC_1:33;
then Im ((R1 | ((dom R1) \ YA)),x) = {y} by RELAT_1:def 16;
hence card (Im ((R1 | ((dom R1) \ YA)),x)) = 1 by CARD_1:30; :: thesis: verum
end;
then card (R1 | ((dom R1) \ YA)) = (card {}) +` (1 *` (card ((dom R1) \ YA))) by A40, Th1
.= 1 *` (card ((dom R1) \ YA)) by CARD_2:18
.= card ((dom R1) \ YA) by CARD_2:21 ;
then A201: card R1 = (card (card XX)) +` (card (2 * (card YA))) by A44, A97, A179, Th1
.= card ((card XX) + (2 * (card YA))) by CARD_2:38
.= (card XX) + (2 * (card YA)) ;
A202: ( |.(BCS (k,(Complex_of {A}))).| = |.(Complex_of {A}).| & |.(Complex_of {A}).| = conv A ) by Th8, Th10;
A203: { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } c= { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } or x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } )
assume x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ; :: thesis: x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa }
then consider S being Simplex of m - 1, BCS (k,(Complex_of {A})) such that
A204: x = S and
A205: F .: S = Aa and
A206: conv (@ S) misses Int A ;
conv (@ S) c= conv A by A202, Th5;
then consider B being Subset of V such that
A207: B c< A and
A208: conv (@ S) c= conv B by A4, A206, RLAFFIN2:23;
A209: B c= A by A207;
then reconsider B = B as finite Subset of V ;
card B < m + 1 by A3, A207, CARD_2:48;
then A210: card B <= m by NAT_1:13;
A211: Aa c= B
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Aa or y in B )
assume y in Aa ; :: thesis: y in B
then consider v being object such that
A212: v in dom F and
A213: v in S and
A214: F . v = y by A205, FUNCT_1:def 6;
S c= conv (@ S) by RLAFFIN1:2;
then v in conv (@ S) by A213;
hence y in B by A9, A208, A209, A212, A214; :: thesis: verum
end;
then card Aa <= card B by NAT_1:43;
then A215: Aa = B by A5, A210, A211, CARD_2:102, XXREAL_0:1;
A216: the topology of (BCS (k,(Complex_of {Aa}))) c= the topology of (BCS (k,(Complex_of {A}))) by A14, SIMPLEX0:def 13;
A217: card S = m by A95, A83, A71, A45, SIMPLEX0:def 18;
then not S is empty by A30;
then A218: (center_of_mass V) . S in Int (@ S) by RLAFFIN2:20;
Int (@ S) c= conv (@ S) by RLAFFIN2:5;
then (center_of_mass V) . S in conv (@ S) by A218;
then consider w being Subset of (BCS (k,(Complex_of {Aa}))) such that
A219: w is simplex-like and
A220: (center_of_mass V) . S in conv (@ w) by A65, A208, A215, Def3;
w in the topology of (BCS (k,(Complex_of {Aa}))) by A219;
then w in the topology of (BCS (k,(Complex_of {A}))) by A216;
then reconsider W = w as Simplex of (BCS (k,(Complex_of {A}))) by PRE_TOPC:def 2;
Int (@ S) meets conv (@ W) by A218, A220, XBOOLE_0:3;
then A221: S c= w by Th26;
then reconsider s = S as Subset of (BCS (k,(Complex_of {Aa}))) by XBOOLE_1:1;
reconsider s = s as Simplex of (BCS (k,(Complex_of {Aa}))) by A219, A221, MATROID0:1;
A222: FA .: s = Aa by A205, RELAT_1:129, SIMPLEX0:17;
s is Simplex of m - 1, BCS (k,(Complex_of {Aa})) by A167, A217, SIMPLEX0:48;
hence x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } by A204, A222; :: thesis: verum
end;
A223: degree (Complex_of {Aa}) = m - 1 by A5, A167, SIMPLEX0:26;
{ S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } c= { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) }
proof
A <> Aa by A3, A5;
then A224: Aa c< A by A12;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } or x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )
assume x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } ; :: thesis: x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) }
then consider S being Simplex of m - 1, BCS (k,(Complex_of {Aa})) such that
A225: x = S and
A226: FA .: S = Aa ;
m - 1 <= degree (BCS (k,(Complex_of {Aa}))) by A7, A223, Th32;
then reconsider S1 = x as Simplex of m - 1, BCS (k,(Complex_of {A})) by A14, A225, SIMPLEX0:49;
A227: FA .: S = F .: S by RELAT_1:129, SIMPLEX0:17;
conv (@ S) c= conv Aa by A65, Th5;
then conv (@ S1) misses Int A by A224, A225, RLAFFIN2:7, XBOOLE_1:63;
hence x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } by A225, A226, A227; :: thesis: verum
end;
then A228: { S where S is Simplex of m - 1, BCS (k,(Complex_of {Aa})) : FA .: S = Aa } = { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } by A203;
for x being object st x in DX holds
card (Im ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )),x)) = 2
proof
let x be object ; :: thesis: ( x in DX implies card (Im ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )),x)) = 2 )
assume A229: x in DX ; :: thesis: card (Im ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )),x)) = 2
then ex y being object st [x,y] in R by XTUPLE_0:def 12;
then A230: x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : Aa = F .: S } by A46;
then consider S being Simplex of m - 1, BCS (k,(Complex_of {A})) such that
A231: x = S and
A232: Aa = F .: S ;
set XX = { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } ;
not x in { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } by A229, XBOOLE_0:def 5;
then conv (@ S) meets Int A by A231, A232;
then A233: card { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } = 2 by A3, Th45;
A234: (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} c= { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 }
proof
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} or w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } )
reconsider ww = w as set by TARSKI:1;
assume w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} ; :: thesis: w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 }
then consider s being object such that
A235: [s,w] in R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ) and
A236: s in {S} by RELAT_1:def 13;
A237: [s,w] in R by A235, RELAT_1:def 11;
then w in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } by A46;
then A238: ex W being Simplex of m, BCS (k,(Complex_of {A})) st w = W ;
s = S by A236, TARSKI:def 1;
then S2[S,ww] by A46, A237;
then S c= ww ;
hence w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } by A238; :: thesis: verum
end;
{ S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } c= (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S}
proof
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } or w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} )
assume w in { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } ; :: thesis: w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S}
then consider W being Simplex of m, BCS (k,(Complex_of {A})) such that
A239: w = W and
A240: S c= W ;
W in { S where S is Simplex of m, BCS (k,(Complex_of {A})) : verum } ;
then [S,W] in R by A46, A230, A231, A240;
then A241: [S,W] in R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ) by A229, A231, RELAT_1:def 11;
S in {S} by TARSKI:def 1;
hence w in (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} by A239, A241, RELAT_1:def 13; :: thesis: verum
end;
then { S1 where S1 is Simplex of m, BCS (k,(Complex_of {A})) : S c= S1 } = (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) .: {S} by A234;
hence card (Im ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )),x)) = 2 by A231, A233, RELAT_1:def 16; :: thesis: verum
end;
then card (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) = (card ((R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) | ((dom (R | ((dom R) \ { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } ))) \ DX))) +` (2 *` (card DX)) by Th1
.= 0 +` (2 *` (card DX)) by A67
.= 2 *` (card DX) by CARD_2:18 ;
then A242: card R = (2 *` (card DX)) +` (1 *` (card { S where S is Simplex of m - 1, BCS (k,(Complex_of {A})) : ( F .: S = Aa & conv (@ S) misses Int A ) } )) by A84, Th1
.= (2 *` (card DX)) +` ((2 * n) + 1) by A82, A228, CARD_2:21
.= ((card 2) *` (card (card DX))) +` ((2 * n) + 1)
.= (card (2 * (card DX))) +` ((2 * n) + 1) by CARD_2:39
.= (card (2 * (card DX))) +` (card ((2 * n) + 1))
.= card ((2 * (card DX)) + ((2 * n) + 1)) by CARD_2:38
.= (2 * (card DX)) + ((2 * n) + 1) ;
then card XX = (2 * (((card DX) + n) - (card YA))) + 1 by A47, A201;
then 2 * (((card DX) + n) - (card YA)) >= - 1 by INT_1:7;
then ((card DX) + n) - (card YA) >= (- 1) / 2 by XREAL_1:79;
then ((card DX) + n) - (card YA) > - 1 by XXREAL_0:2;
then ((card DX) + n) - (card YA) >= 0 by INT_1:8;
then reconsider cnc = ((card DX) + n) - (card YA) as Element of NAT by INT_1:3;
take cnc ; :: thesis: card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * cnc) + 1
thus card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * cnc) + 1 by A47, A201, A242; :: thesis: verum
end;
end;
end;
A243: S1[ 0 ]
proof
let A be finite affinely-independent Subset of V; :: thesis: ( card A = 0 implies for F being Function of (Vertices (BCS (k,(Complex_of {A})))),A st ( for v being Vertex of (BCS (k,(Complex_of {A})))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1 )
assume A244: card A = 0 ; :: thesis: for F being Function of (Vertices (BCS (k,(Complex_of {A})))),A st ( for v being Vertex of (BCS (k,(Complex_of {A})))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1
A245: A = {} by A244;
set C = Complex_of {A};
A246: ( |.(Complex_of {A}).| c= [#] V & [#] (Complex_of {A}) = [#] V ) ;
let F be Function of (Vertices (BCS (k,(Complex_of {A})))),A; :: thesis: ( ( for v being Vertex of (BCS (k,(Complex_of {A})))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ) implies ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1 )
assume for v being Vertex of (BCS (k,(Complex_of {A})))
for B being Subset of V st B c= A & v in conv B holds
F . v in B ; :: thesis: ex n being Nat st card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * n) + 1
set X = { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } ;
take 0 ; :: thesis: card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * 0) + 1
A247: ( k = 0 or k > 0 ) ;
A248: Z - 1 = - 1 by XXREAL_3:4;
then degree (Complex_of {A}) = - 1 by A244, SIMPLEX0:26;
then A249: Complex_of {A} = BCS (k,(Complex_of {A})) by A246, A247, Th16, Th22;
A250: the topology of (Complex_of {A}) = bool A by SIMPLEX0:4;
A251: { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } c= {A}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } or x in {A} )
assume A252: x in { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } ; :: thesis: x in {A}
consider S being Simplex of (card A) - 1, BCS (k,(Complex_of {A})) such that
A253: S = x and
F .: S = A by A252;
S in the topology of (Complex_of {A}) by A249, PRE_TOPC:def 2;
then S is empty by A245, A250;
hence x in {A} by A245, A253, TARSKI:def 1; :: thesis: verum
end;
A in bool A by ZFMISC_1:def 1;
then reconsider A1 = A as Simplex of (Complex_of {A}) by A250, PRE_TOPC:def 2;
A254: F .: A1 = A by A245;
A1 is Simplex of - 1, Complex_of {A} by A244, A248, SIMPLEX0:48;
then A in { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } by A249, A254;
then { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = {A} by A251, ZFMISC_1:33;
hence card { S where S is Simplex of (card A) - 1, BCS (k,(Complex_of {A})) : F .: S = A } = (2 * 0) + 1 by CARD_1:30; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A243, A1);
 hence for F being Function of (Vertices (BCS (k,(Complex_of {Aff})))),Aff st ( for v being Vertex of (BCS (k,(Complex_of {Aff})))
for B being Subset of V st B c= Aff & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) : F .: S = Aff } = (2 * n) + 1 ; :: thesis: verum