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 Th6, Th9;
then A2: (alternating-proper-f-vector p) . tw = mo * (num-polytopes p,(tw - 1)) by A1, Def27;
(- 1) |^ (th + 1) = 1 by Th7, Th8;
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 Th5, Th8;
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:62;
then Sum (alternating-proper-f-vector p) = (apcson + apcstw) + apcsth by RVSUM_1:108
.= ((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