let p be polyhedron; :: thesis: ( dim p = 3 implies Sum (alternating-proper-f-vector p) = ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2)) )
reconsider mo = - 1 as Integer ;
reconsider th = 3 as Nat ;
reconsider tw = 2 as Nat ;
reconsider o = 1 as Nat ;
assume A1: dim p = 3 ; :: thesis: Sum (alternating-proper-f-vector p) = ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2))
set apcs = alternating-proper-f-vector p;
(- 1) |^ (tw + 1) = - 1 by Th5, Th8;
then A2: (alternating-proper-f-vector p) . tw = mo * (num-polytopes (p,(tw - 1))) by A1, Def27;
(- 1) |^ (th + 1) = 1 by Th6, Th7;
then A3: (alternating-proper-f-vector p) . th = o * (num-polytopes (p,(th - 1))) by A1, Def27;
reconsider apcsth = (alternating-proper-f-vector p) . th as Integer ;
reconsider apcstw = (alternating-proper-f-vector p) . tw as Integer ;
reconsider apcson = (alternating-proper-f-vector p) . o as Integer ;
(- 1) |^ (o + 1) = 1 by Th4, Th7;
then A4: (alternating-proper-f-vector p) . o = o * (num-polytopes (p,(o - 1))) by A1, Def27;
len (alternating-proper-f-vector p) = 3 by A1, Def27;
then alternating-proper-f-vector p = <*apcson,apcstw,apcsth*> by FINSEQ_1:45;
then Sum (alternating-proper-f-vector p) = (apcson + apcstw) + apcsth by RVSUM_1:78
.= ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2)) by A4, A2, A3 ;
hence Sum (alternating-proper-f-vector p) = ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2)) ; :: thesis: verum