let V be RealLinearSpace; :: thesis: for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv & degree Kv <= 0 holds

TopStruct(# the carrier of Kv, the topology of Kv #) = BCS Kv

let Kv be non void SimplicialComplex of V; :: thesis: ( |.Kv.| c= [#] Kv & degree Kv <= 0 implies TopStruct(# the carrier of Kv, the topology of Kv #) = BCS Kv )

reconsider o = 1 as ExtReal ;

assume that

A1: |.Kv.| c= [#] Kv and

A2: degree Kv <= 0 ; :: thesis: TopStruct(# the carrier of Kv, the topology of Kv #) = BCS Kv

set B = center_of_mass V;

set BC = BCS Kv;

A3: BCS Kv = subdivision ((center_of_mass V),Kv) by A1, Def5;

then A4: [#] (BCS Kv) = [#] Kv by SIMPLEX0:def 20;

A5: dom (center_of_mass V) = (bool the carrier of V) \ {{}} by FUNCT_2:def 1;

A6: ( 0 + o = 0 + 1 & (degree Kv) + o <= 0 + o ) by A2, XXREAL_3:35, XXREAL_3:def 2;

A7: the topology of (BCS Kv) c= the topology of Kv

TopStruct(# the carrier of Kv, the topology of Kv #) = BCS Kv

let Kv be non void SimplicialComplex of V; :: thesis: ( |.Kv.| c= [#] Kv & degree Kv <= 0 implies TopStruct(# the carrier of Kv, the topology of Kv #) = BCS Kv )

reconsider o = 1 as ExtReal ;

assume that

A1: |.Kv.| c= [#] Kv and

A2: degree Kv <= 0 ; :: thesis: TopStruct(# the carrier of Kv, the topology of Kv #) = BCS Kv

set B = center_of_mass V;

set BC = BCS Kv;

A3: BCS Kv = subdivision ((center_of_mass V),Kv) by A1, Def5;

then A4: [#] (BCS Kv) = [#] Kv by SIMPLEX0:def 20;

A5: dom (center_of_mass V) = (bool the carrier of V) \ {{}} by FUNCT_2:def 1;

A6: ( 0 + o = 0 + 1 & (degree Kv) + o <= 0 + o ) by A2, XXREAL_3:35, XXREAL_3:def 2;

A7: the topology of (BCS Kv) c= the topology of Kv

proof

the topology of Kv c= the topology of (BCS Kv)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of (BCS Kv) or x in the topology of Kv )

assume x in the topology of (BCS Kv) ; :: thesis: x in the topology of Kv

then reconsider X = x as Simplex of (BCS Kv) by PRE_TOPC:def 2;

reconsider X1 = X as Subset of Kv by A4;

consider S being c=-linear finite simplex-like Subset-Family of Kv such that

A8: X = (center_of_mass V) .: S by A3, SIMPLEX0:def 20;

A9: (center_of_mass V) .: S = (center_of_mass V) .: (S /\ (dom (center_of_mass V))) by RELAT_1:112;

end;assume x in the topology of (BCS Kv) ; :: thesis: x in the topology of Kv

then reconsider X = x as Simplex of (BCS Kv) by PRE_TOPC:def 2;

reconsider X1 = X as Subset of Kv by A4;

consider S being c=-linear finite simplex-like Subset-Family of Kv such that

A8: X = (center_of_mass V) .: S by A3, SIMPLEX0:def 20;

A9: (center_of_mass V) .: S = (center_of_mass V) .: (S /\ (dom (center_of_mass V))) by RELAT_1:112;

per cases
( X is empty or not X is empty )
;

end;

suppose A10:
not X is empty
; :: thesis: x in the topology of Kv

then
not S is empty
by A8;

then union S in S by SIMPLEX0:9;

then reconsider U = union S as Simplex of Kv by TOPS_2:def 1;

A11: not U is empty

card U <= (degree Kv) + 1 by SIMPLEX0:24;

then A16: card U <= 1 by A6, XXREAL_0:2;

card U >= 1 by A11, NAT_1:14;

then A17: card U = 1 by A16, XXREAL_0:1;

then consider u being object such that

A18: {u} = @ U by CARD_2:42;

u in {u} by TARSKI:def 1;

then reconsider u = u as Element of V by A18;

A19: S /\ (dom (center_of_mass V)) c= {U}

then S /\ (dom (center_of_mass V)) = {U} by A19, ZFMISC_1:33;

then X = Im ((center_of_mass V),U) by A8, A9, RELAT_1:def 16

.= {((center_of_mass V) . U)} by A15, FUNCT_1:59

.= {((1 / 1) * (Sum {u}))} by A17, A18, RLAFFIN2:def 2

.= {(Sum {u})} by RLVECT_1:def 8

.= U by A18, RLVECT_2:9 ;

hence x in the topology of Kv by PRE_TOPC:def 2; :: thesis: verum

end;then union S in S by SIMPLEX0:9;

then reconsider U = union S as Simplex of Kv by TOPS_2:def 1;

A11: not U is empty

proof

then A15:
@ U in dom (center_of_mass V)
by A5, ZFMISC_1:56;
assume A12:
U is empty
; :: thesis: contradiction

S /\ (dom (center_of_mass V)) is empty

end;S /\ (dom (center_of_mass V)) is empty

proof

hence
contradiction
by A8, A9, A10; :: thesis: verum
assume
not S /\ (dom (center_of_mass V)) is empty
; :: thesis: contradiction

then consider y being object such that

A13: y in S /\ (dom (center_of_mass V)) ;

reconsider y = y as set by TARSKI:1;

y in S by A13, XBOOLE_0:def 4;

then A14: y c= U by ZFMISC_1:74;

y <> {} by A13, ZFMISC_1:56;

hence contradiction by A12, A14; :: thesis: verum

end;then consider y being object such that

A13: y in S /\ (dom (center_of_mass V)) ;

reconsider y = y as set by TARSKI:1;

y in S by A13, XBOOLE_0:def 4;

then A14: y c= U by ZFMISC_1:74;

y <> {} by A13, ZFMISC_1:56;

hence contradiction by A12, A14; :: thesis: verum

card U <= (degree Kv) + 1 by SIMPLEX0:24;

then A16: card U <= 1 by A6, XXREAL_0:2;

card U >= 1 by A11, NAT_1:14;

then A17: card U = 1 by A16, XXREAL_0:1;

then consider u being object such that

A18: {u} = @ U by CARD_2:42;

u in {u} by TARSKI:def 1;

then reconsider u = u as Element of V by A18;

A19: S /\ (dom (center_of_mass V)) c= {U}

proof

not S /\ (dom (center_of_mass V)) is empty
by A8, A9, A10;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in S /\ (dom (center_of_mass V)) or y in {U} )

reconsider yy = y as set by TARSKI:1;

assume A20: y in S /\ (dom (center_of_mass V)) ; :: thesis: y in {U}

then y in S by XBOOLE_0:def 4;

then A21: yy c= U by ZFMISC_1:74;

y <> {} by A20, ZFMISC_1:56;

then y = U by A18, A21, ZFMISC_1:33;

hence y in {U} by TARSKI:def 1; :: thesis: verum

end;reconsider yy = y as set by TARSKI:1;

assume A20: y in S /\ (dom (center_of_mass V)) ; :: thesis: y in {U}

then y in S by XBOOLE_0:def 4;

then A21: yy c= U by ZFMISC_1:74;

y <> {} by A20, ZFMISC_1:56;

then y = U by A18, A21, ZFMISC_1:33;

hence y in {U} by TARSKI:def 1; :: thesis: verum

then S /\ (dom (center_of_mass V)) = {U} by A19, ZFMISC_1:33;

then X = Im ((center_of_mass V),U) by A8, A9, RELAT_1:def 16

.= {((center_of_mass V) . U)} by A15, FUNCT_1:59

.= {((1 / 1) * (Sum {u}))} by A17, A18, RLAFFIN2:def 2

.= {(Sum {u})} by RLVECT_1:def 8

.= U by A18, RLVECT_2:9 ;

hence x in the topology of Kv by PRE_TOPC:def 2; :: thesis: verum

proof

hence
TopStruct(# the carrier of Kv, the topology of Kv #) = BCS Kv
by A3, A4, A7, XBOOLE_0:def 10; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of Kv or x in the topology of (BCS Kv) )

assume x in the topology of Kv ; :: thesis: x in the topology of (BCS Kv)

then reconsider X = x as Simplex of Kv by PRE_TOPC:def 2;

reconsider X1 = X as Subset of (BCS Kv) by A4;

end;assume x in the topology of Kv ; :: thesis: x in the topology of (BCS Kv)

then reconsider X = x as Simplex of Kv by PRE_TOPC:def 2;

reconsider X1 = X as Subset of (BCS Kv) by A4;

per cases
( X is empty or not X is empty )
;

end;

suppose A22:
not X is empty
; :: thesis: x in the topology of (BCS Kv)

for Y being Subset of Kv st Y in {X} holds

Y is simplex-like by TARSKI:def 1;

then reconsider XX = {X} as finite simplex-like Subset-Family of Kv by TOPS_2:def 1;

card X <= (degree Kv) + 1 by SIMPLEX0:24;

then A26: card X <= 1 by A6, XXREAL_0:2;

card X >= 1 by A22, NAT_1:14;

then A27: card X = 1 by A26, XXREAL_0:1;

then consider u being object such that

A28: @ X = {u} by CARD_2:42;

A29: @ X in dom (center_of_mass V) by A5, A22, ZFMISC_1:56;

u in {u} by TARSKI:def 1;

then reconsider u = u as Element of V by A28;

(center_of_mass V) .: XX = Im ((center_of_mass V),X) by RELAT_1:def 16

.= {((center_of_mass V) . X)} by A29, FUNCT_1:59

.= {((1 / 1) * (Sum {u}))} by A27, A28, RLAFFIN2:def 2

.= {(Sum {u})} by RLVECT_1:def 8

.= X1 by A28, RLVECT_2:9 ;

then X1 is simplex-like by A3, A25, SIMPLEX0:def 20;

hence x in the topology of (BCS Kv) ; :: thesis: verum

end;Y is simplex-like by TARSKI:def 1;

then reconsider XX = {X} as finite simplex-like Subset-Family of Kv by TOPS_2:def 1;

now :: thesis: for x, y being set st x in XX & y in XX holds

x,y are_c=-comparable

then A25:
XX is c=-linear
;x,y are_c=-comparable

let x, y be set ; :: thesis: ( x in XX & y in XX implies x,y are_c=-comparable )

assume that

A23: x in XX and

A24: y in XX ; :: thesis: x,y are_c=-comparable

x = X by A23, TARSKI:def 1;

hence x,y are_c=-comparable by A24, TARSKI:def 1; :: thesis: verum

end;assume that

A23: x in XX and

A24: y in XX ; :: thesis: x,y are_c=-comparable

x = X by A23, TARSKI:def 1;

hence x,y are_c=-comparable by A24, TARSKI:def 1; :: thesis: verum

card X <= (degree Kv) + 1 by SIMPLEX0:24;

then A26: card X <= 1 by A6, XXREAL_0:2;

card X >= 1 by A22, NAT_1:14;

then A27: card X = 1 by A26, XXREAL_0:1;

then consider u being object such that

A28: @ X = {u} by CARD_2:42;

A29: @ X in dom (center_of_mass V) by A5, A22, ZFMISC_1:56;

u in {u} by TARSKI:def 1;

then reconsider u = u as Element of V by A28;

(center_of_mass V) .: XX = Im ((center_of_mass V),X) by RELAT_1:def 16

.= {((center_of_mass V) . X)} by A29, FUNCT_1:59

.= {((1 / 1) * (Sum {u}))} by A27, A28, RLAFFIN2:def 2

.= {(Sum {u})} by RLVECT_1:def 8

.= X1 by A28, RLVECT_2:9 ;

then X1 is simplex-like by A3, A25, SIMPLEX0:def 20;

hence x in the topology of (BCS Kv) ; :: thesis: verum