let p be polyhedron; :: thesis: alternating-semi-proper-f-vector p = (alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>
set d = dim p;
set aspcs = alternating-semi-proper-f-vector p;
set apcs = alternating-proper-f-vector p;
set r = (alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>;
A1: len (alternating-semi-proper-f-vector p) = (dim p) + 1 by Def28;
A2: for n being Nat st 1 <= n & n <= len (alternating-semi-proper-f-vector p) holds
(alternating-semi-proper-f-vector p) . n = ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n
proof
let n be Nat; :: thesis: ( 1 <= n & n <= len (alternating-semi-proper-f-vector p) implies (alternating-semi-proper-f-vector p) . n = ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n )
assume that
A3: 1 <= n and
A4: n <= len (alternating-semi-proper-f-vector p) ; :: thesis: (alternating-semi-proper-f-vector p) . n = ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n
per cases ( n <= dim p or n = (dim p) + 1 ) by A1, A4, NAT_1:8;
suppose A6: n = (dim p) + 1 ; :: thesis: (alternating-semi-proper-f-vector p) . n = ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n
then n = (len (alternating-proper-f-vector p)) + 1 by Def27;
then A7: ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n = (- 1) |^ (dim p) by FINSEQ_1:42
.= (- 1) |^ ((dim p) + 2) by Th12 ;
(alternating-semi-proper-f-vector p) . n = ((- 1) |^ (n + 1)) * (num-polytopes (p,(n - 1))) by A3, A6, Def28
.= ((- 1) |^ (n + 1)) * 1 by A6, Th29
.= (- 1) |^ (n + 1) ;
hence (alternating-semi-proper-f-vector p) . n = ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n by A6, A7; :: thesis: verum
end;
end;
end;
len ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) = (len (alternating-proper-f-vector p)) + (len <*((- 1) |^ (dim p))*>) by FINSEQ_1:22
.= (dim p) + (len <*((- 1) |^ (dim p))*>) by Def27
.= (dim p) + 1 by FINSEQ_1:40 ;
then len (alternating-semi-proper-f-vector p) = len ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) by Def28;
hence alternating-semi-proper-f-vector p = (alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*> by A2; :: thesis: verum