let p be polyhedron; :: thesis: ( dim p = 2 implies Sum (alternating-proper-f-vector p) = (num-polytopes p,0 ) - (num-polytopes p,1) )
assume A1: dim p = 2 ; :: thesis: Sum (alternating-proper-f-vector p) = (num-polytopes p,0 ) - (num-polytopes p,1)
set apcs = alternating-proper-f-vector p;
A2: len (alternating-proper-f-vector p) = 2 by A1, Def27;
reconsider o = 1 as Nat ;
reconsider t = 2 as Nat ;
A3: (alternating-proper-f-vector p) . o = ((- 1) |^ (o + 1)) * (num-polytopes p,(o - 1)) by A1, Def27;
A4: (alternating-proper-f-vector p) . t = ((- 1) |^ (t + 1)) * (num-polytopes p,(t - 1)) by A1, Def27;
A5: (- 1) |^ (o + 1) = 1 by Th5, Th8;
A6: (- 1) |^ (t + 1) = - 1 by Th6, Th9;
reconsider apcso = (alternating-proper-f-vector p) . o as Integer ;
reconsider apcst = (alternating-proper-f-vector p) . t as Integer ;
A7: alternating-proper-f-vector p = <*apcso,apcst*> by A2, FINSEQ_1:61;
Sum (alternating-proper-f-vector p) = apcso + apcst by A7, RVSUM_1:107
.= (num-polytopes p,0 ) - (num-polytopes p,1) by A3, A4, A5, A6 ;
hence Sum (alternating-proper-f-vector p) = (num-polytopes p,0 ) - (num-polytopes p,1) ; :: thesis: verum