let p be polyhedron; :: thesis: for k being Integer
for c, d being Element of (k -chain-space p)
for x being Element of (k - 1) -polytopes p holds Sum ((incidence-sequence x,c) + (incidence-sequence x,d)) = (Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d))
let k be Integer; :: thesis: for c, d being Element of (k -chain-space p)
for x being Element of (k - 1) -polytopes p holds Sum ((incidence-sequence x,c) + (incidence-sequence x,d)) = (Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d))
let c, d be Element of (k -chain-space p); :: thesis: for x being Element of (k - 1) -polytopes p holds Sum ((incidence-sequence x,c) + (incidence-sequence x,d)) = (Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d))
let x be Element of (k - 1) -polytopes p; :: thesis: Sum ((incidence-sequence x,c) + (incidence-sequence x,d)) = (Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d))
set isc = incidence-sequence x,c;
set isd = incidence-sequence x,d;
per cases
( (k - 1) -polytopes p is empty or not (k - 1) -polytopes p is empty )
;
suppose A1:
(k - 1) -polytopes p is
empty
;
:: thesis: Sum ((incidence-sequence x,c) + (incidence-sequence x,d)) = (Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d))then A2:
incidence-sequence x,
c = <*> the
carrier of
Z_2
by Def16;
A3:
incidence-sequence x,
d = <*> the
carrier of
Z_2
by A1, Def16;
reconsider isc =
incidence-sequence x,
c as
Element of
0 -tuples_on the
carrier of
Z_2 by A2, FINSEQ_2:114;
reconsider isd =
incidence-sequence x,
d as
Element of
0 -tuples_on the
carrier of
Z_2 by A3, FINSEQ_2:114;
A4:
Sum isc = 0. Z_2
by FVSUM_1:93;
A5:
Sum isd = 0. Z_2
by FVSUM_1:93;
reconsider s =
isc + isd as
Element of
0 -tuples_on the
carrier of
Z_2 ;
Sum s = 0. Z_2
by FVSUM_1:93;
hence
Sum ((incidence-sequence x,c) + (incidence-sequence x,d)) = (Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d))
by A4, A5, RLVECT_1:def 7;
:: thesis: verum end; suppose A6:
not
(k - 1) -polytopes p is
empty
;
:: thesis: Sum ((incidence-sequence x,c) + (incidence-sequence x,d)) = (Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d))reconsider n =
num-polytopes p,
k as
Element of
NAT ;
A7:
len (incidence-sequence x,c) = n
by A6, Def16;
A8:
len (incidence-sequence x,d) = n
by A6, Def16;
reconsider isc' =
incidence-sequence x,
c as
Element of
n -tuples_on the
carrier of
Z_2 by A7, FINSEQ_2:110;
reconsider isd' =
incidence-sequence x,
d as
Element of
n -tuples_on the
carrier of
Z_2 by A8, FINSEQ_2:110;
Sum ((incidence-sequence x,c) + (incidence-sequence x,d)) =
Sum (isc' + isd')
.=
(Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d))
by FVSUM_1:95
;
hence
Sum ((incidence-sequence x,c) + (incidence-sequence x,d)) = (Sum (incidence-sequence x,c)) + (Sum (incidence-sequence x,d))
;
:: thesis: verum end;