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

for Kv being non void SimplicialComplex of V st n > 0 & |.Kv.| c= [#] Kv & degree Kv <= 0 holds

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

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

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

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

assume that

A1: n > 0 and

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

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

defpred S_{1}[ Nat] means ( $1 > 0 implies ( TopStruct(# the carrier of Kv, the topology of Kv #) = BCS ($1,Kv) & degree (BCS ($1,Kv)) <= 0 ) );

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

S_{1}[n + 1]
_{1}[ 0 ]
;

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

hence TopStruct(# the carrier of Kv, the topology of Kv #) = BCS (n,Kv) by A1; :: thesis: verum

for Kv being non void SimplicialComplex of V st n > 0 & |.Kv.| c= [#] Kv & degree Kv <= 0 holds

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

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

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

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

assume that

A1: n > 0 and

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

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

defpred S

A4: for n being Nat st S

S

proof

A11:
S
not {} in dom (center_of_mass V)
by ZFMISC_1:56;

then A5: dom (center_of_mass V) is with_non-empty_elements ;

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

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

assume n + 1 > 0 ; :: thesis: ( TopStruct(# the carrier of Kv, the topology of Kv #) = BCS ((n + 1),Kv) & degree (BCS ((n + 1),Kv)) <= 0 )

end;then A5: dom (center_of_mass V) is with_non-empty_elements ;

let n be Nat; :: thesis: ( S

assume A6: S

assume n + 1 > 0 ; :: thesis: ( TopStruct(# the carrier of Kv, the topology of Kv #) = BCS ((n + 1),Kv) & degree (BCS ((n + 1),Kv)) <= 0 )

per cases
( n = 0 or n > 0 )
;

end;

suppose A7:
n = 0
; :: thesis: ( TopStruct(# the carrier of Kv, the topology of Kv #) = BCS ((n + 1),Kv) & degree (BCS ((n + 1),Kv)) <= 0 )

A8:
degree (subdivision ((center_of_mass V),Kv)) <= degree Kv
by A5, SIMPLEX0:52;

BCS ((n + 1),Kv) = BCS Kv by A2, A7, Th17;

hence ( TopStruct(# the carrier of Kv, the topology of Kv #) = BCS ((n + 1),Kv) & degree (BCS ((n + 1),Kv)) <= 0 ) by A2, A3, A8, Def5, Th21; :: thesis: verum

end;BCS ((n + 1),Kv) = BCS Kv by A2, A7, Th17;

hence ( TopStruct(# the carrier of Kv, the topology of Kv #) = BCS ((n + 1),Kv) & degree (BCS ((n + 1),Kv)) <= 0 ) by A2, A3, A8, Def5, Th21; :: thesis: verum

suppose A9:
n > 0
; :: thesis: ( TopStruct(# the carrier of Kv, the topology of Kv #) = BCS ((n + 1),Kv) & degree (BCS ((n + 1),Kv)) <= 0 )

A10:
|.Kv.| = |.(BCS (n,Kv)).|
by Th10;

[#] Kv = [#] (BCS (n,Kv)) by A6, A9;

then BCS (n,Kv) = BCS (BCS (n,Kv)) by A2, A6, A9, A10, Th21;

hence ( TopStruct(# the carrier of Kv, the topology of Kv #) = BCS ((n + 1),Kv) & degree (BCS ((n + 1),Kv)) <= 0 ) by A2, A6, A9, Th20; :: thesis: verum

end;[#] Kv = [#] (BCS (n,Kv)) by A6, A9;

then BCS (n,Kv) = BCS (BCS (n,Kv)) by A2, A6, A9, A10, Th21;

hence ( TopStruct(# the carrier of Kv, the topology of Kv #) = BCS ((n + 1),Kv) & degree (BCS ((n + 1),Kv)) <= 0 ) by A2, A6, A9, Th20; :: thesis: verum

for n being Nat holds S

hence TopStruct(# the carrier of Kv, the topology of Kv #) = BCS (n,Kv) by A1; :: thesis: verum