let p be polyhedron; :: thesis: ( p is simply-connected implies p is eulerian )
assume A1: p is simply-connected ; :: thesis: p is eulerian
set apcs = alternating-proper-f-vector p;
per cases ( dim p = 0 or dim p > 0 ) ;
suppose dim p = 0 ; :: thesis: p is eulerian
hence p is eulerian by Th88; :: thesis: verum
end;
suppose dim p > 0 ; :: thesis: p is eulerian
then A2: len (alternating-proper-f-vector p) > 0 by Def27;
deffunc H1( Nat) -> Element of INT = ((- 1) |^ ($1 + 1)) * (dim (($1 - 2) -bounding-chain-space p));
deffunc H2( Nat) -> Element of INT = ((- 1) |^ ($1 + 1)) * (dim (($1 - 1) -circuit-space p));
consider a being FinSequence such that
A3: len a = len (alternating-proper-f-vector p) and
A4: for n being Nat st n in dom a holds
a . n = H1(n) from FINSEQ_1:sch 2();
consider b being FinSequence such that
A5: len b = len (alternating-proper-f-vector p) and
A6: for n being Nat st n in dom b holds
b . n = H2(n) from FINSEQ_1:sch 2();
 ( rng a c= INT & rng b c= INT )
proof
thus rng a c= INT :: thesis: rng b c= INT
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng a or y in INT )
assume A7: y in rng a ; :: thesis: y in INT
consider x being set such that
A8: x in dom a and
A9: y = a . x by A7, FUNCT_1:def 5;
reconsider x = x as Element of NAT by A8;
a . x = ((- 1) |^ (x + 1)) * (dim ((x - 2) -bounding-chain-space p)) by A4, A8;
hence y in INT by A9; :: thesis: verum
end;
thus rng b c= INT :: thesis: verum
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng b or y in INT )
assume A10: y in rng b ; :: thesis: y in INT
consider x being set such that
A11: x in dom b and
A12: y = b . x by A10, FUNCT_1:def 5;
reconsider x = x as Element of NAT by A11;
b . x = ((- 1) |^ (x + 1)) * (dim ((x - 1) -circuit-space p)) by A6, A11;
hence y in INT by A12; :: thesis: verum
end;
end;
then reconsider a = a, b = b as FinSequence of INT by FINSEQ_1:def 4;
A13: for n being Nat st 1 <= n & n <= len (alternating-proper-f-vector p) holds
(alternating-proper-f-vector p) . n = (a . n) + (b . n)
proof
let n be Nat; :: thesis: ( 1 <= n & n <= len (alternating-proper-f-vector p) implies (alternating-proper-f-vector p) . n = (a . n) + (b . n) )
assume that
A14: 1 <= n and
A15: n <= len (alternating-proper-f-vector p) ; :: thesis: (alternating-proper-f-vector p) . n = (a . n) + (b . n)
A16: (alternating-proper-f-vector p) . n = (((- 1) |^ (n + 1)) * (dim ((n - 2) -bounding-chain-space p))) + (((- 1) |^ (n + 1)) * (dim ((n - 1) -circuit-space p))) by A14, A15, Th52;
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
A17: n' in dom b by A14, A15, A5, FINSEQ_3:27;
n' in dom a by A14, A15, A3, FINSEQ_3:27;
then a . n' = ((- 1) |^ (n' + 1)) * (dim ((n' - 2) -bounding-chain-space p)) by A4;
hence (alternating-proper-f-vector p) . n = (a . n) + (b . n) by A6, A16, A17; :: thesis: verum
end;
for n being Nat st 1 <= n & n < len (alternating-proper-f-vector p) holds
b . n = - (a . (n + 1))
proof
let n be Nat; :: thesis: ( 1 <= n & n < len (alternating-proper-f-vector p) implies b . n = - (a . (n + 1)) )
assume that
A18: 1 <= n and
A19: n < len (alternating-proper-f-vector p) ; :: thesis: b . n = - (a . (n + 1))
A20: n in dom b by A18, A19, A5, FINSEQ_3:27;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A21: b . n = ((- 1) |^ (n + 1)) * (dim ((n - 1) -circuit-space p)) by A6, A20;
A22: n + 1 <= len (alternating-proper-f-vector p) by A19, INT_1:20;
1 <= n + 1 by NAT_1:11;
then n + 1 in dom a by A22, A3, FINSEQ_3:27;
then a . (n + 1) = H1(n + 1) by A4
.= (((- 1) |^ (n + 1)) * ((- 1) |^ 1)) * (dim ((n - 1) -bounding-chain-space p)) by NEWTON:13
.= (((- 1) |^ (n + 1)) * (- 1)) * (dim ((n - 1) -bounding-chain-space p)) by NEWTON:10
.= - (((- 1) |^ (n + 1)) * (dim ((n - 1) -bounding-chain-space p)))
.= - (b . n) by A1, A21, Th51 ;
hence b . n = - (a . (n + 1)) ; :: thesis: verum
end;
then A23: Sum (alternating-proper-f-vector p) = (a . 1) + (b . (len (alternating-proper-f-vector p))) by A2, A3, A5, A13, Th15;
A24: a . 1 = 1
proof
reconsider egy = 1 as Element of NAT ;
1 <= 0 + 1 ;
then egy <= len (alternating-proper-f-vector p) by A2, NAT_1:13;
then egy in dom a by A3, FINSEQ_3:27;
then a . egy = ((- 1) |^ (1 + 1)) * (dim ((egy - 2) -bounding-chain-space p)) by A4
.= 1 * (dim ((egy - 2) -bounding-chain-space p)) by Th5, Th8
.= 1 by Th63 ;
hence a . 1 = 1 ; :: thesis: verum
end;
b . (len (alternating-proper-f-vector p)) = (- 1) |^ ((dim p) + 1)
proof
reconsider n = len (alternating-proper-f-vector p) as Element of NAT ;
A25: n = dim p by Def27;
0 + 1 = 1 ;
then 1 <= len (alternating-proper-f-vector p) by A2, NAT_1:13;
then n in dom b by A5, FINSEQ_3:27;
then b . n = H2(n) by A6
.= ((- 1) |^ (n + 1)) * 1 by A1, A25, Th80
.= (- 1) |^ (n + 1) ;
hence b . (len (alternating-proper-f-vector p)) = (- 1) |^ ((dim p) + 1) by Def27; :: thesis: verum
end;
hence p is eulerian by A23, A24, Def29; :: thesis: verum
end;
end;