let p be polyhedron; for k being Integer
for c, d being Element of (k -chain-space p)
for x being Element of (k - 1) -polytopes p holds incidence-sequence x,(c + d) = (incidence-sequence x,c) + (incidence-sequence x,d)
let k be Integer; for c, d being Element of (k -chain-space p)
for x being Element of (k - 1) -polytopes p holds incidence-sequence x,(c + d) = (incidence-sequence x,c) + (incidence-sequence x,d)
let c, d be Element of (k -chain-space p); for x being Element of (k - 1) -polytopes p holds incidence-sequence x,(c + d) = (incidence-sequence x,c) + (incidence-sequence x,d)
let x be Element of (k - 1) -polytopes p; incidence-sequence x,(c + d) = (incidence-sequence x,c) + (incidence-sequence x,d)
set n = num-polytopes p,k;
set l = incidence-sequence x,(c + d);
set isc = incidence-sequence x,c;
set isd = incidence-sequence x,d;
set r = (incidence-sequence x,c) + (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
;
incidence-sequence x,(c + d) = (incidence-sequence x,c) + (incidence-sequence x,d)then
incidence-sequence x,
d is
Tuple of
0 ,the
carrier of
Z_2
by Def16;
then reconsider isd =
incidence-sequence x,
d as
Element of
0 -tuples_on the
carrier of
Z_2 by FINSEQ_2:151;
incidence-sequence x,
c = <*> the
carrier of
Z_2
by A1, Def16;
then reconsider isc =
incidence-sequence x,
c as
Element of
0 -tuples_on the
carrier of
Z_2 by FINSEQ_2:151;
isc + isd is
Element of
0 -tuples_on the
carrier of
Z_2
;
hence
incidence-sequence x,
(c + d) = (incidence-sequence x,c) + (incidence-sequence x,d)
by A1, Def16;
verum end; suppose A2:
not
(k - 1) -polytopes p is
empty
;
incidence-sequence x,(c + d) = (incidence-sequence x,c) + (incidence-sequence x,d)A3:
(
len (incidence-sequence x,(c + d)) = num-polytopes p,
k &
len ((incidence-sequence x,c) + (incidence-sequence x,d)) = num-polytopes p,
k )
proof
len (incidence-sequence x,d) = num-polytopes p,
k
by A2, Def16;
then reconsider isd =
incidence-sequence x,
d as
Element of
(num-polytopes p,k) -tuples_on the
carrier of
Z_2 by FINSEQ_2:110;
len (incidence-sequence x,c) = num-polytopes p,
k
by A2, Def16;
then reconsider isc =
incidence-sequence x,
c as
Element of
(num-polytopes p,k) -tuples_on the
carrier of
Z_2 by FINSEQ_2:110;
reconsider s =
isc + isd as
Element of
(num-polytopes p,k) -tuples_on the
carrier of
Z_2 ;
len s = num-polytopes p,
k
by FINSEQ_1:def 18;
hence
(
len (incidence-sequence x,(c + d)) = num-polytopes p,
k &
len ((incidence-sequence x,c) + (incidence-sequence x,d)) = num-polytopes p,
k )
by A2, Def16;
verum
end;
for
n being
Nat st 1
<= n &
n <= len (incidence-sequence x,(c + d)) holds
(incidence-sequence x,(c + d)) . n = ((incidence-sequence x,c) + (incidence-sequence x,d)) . n
proof
A4:
(
dom ((incidence-sequence x,c) + (incidence-sequence x,d)) = Seg (num-polytopes p,k) &
len (incidence-sequence x,(c + d)) = num-polytopes p,
k )
by A3, FINSEQ_1:def 3;
let m be
Nat;
( 1 <= m & m <= len (incidence-sequence x,(c + d)) implies (incidence-sequence x,(c + d)) . m = ((incidence-sequence x,c) + (incidence-sequence x,d)) . m )
assume A5:
( 1
<= m &
m <= len (incidence-sequence x,(c + d)) )
;
(incidence-sequence x,(c + d)) . m = ((incidence-sequence x,c) + (incidence-sequence x,d)) . m
set a =
m -th-polytope p,
k;
set iva =
incidence-value x,
(m -th-polytope p,k);
A6:
len (incidence-sequence x,(c + d)) = num-polytopes p,
k
by A2, Def16;
then A7:
(incidence-sequence x,(c + d)) . m = ((c + d) @ (m -th-polytope p,k)) * (incidence-value x,(m -th-polytope p,k))
by A2, A5, Def16;
m in NAT
by ORDINAL1:def 13;
then A8:
m in dom ((incidence-sequence x,c) + (incidence-sequence x,d))
by A4, A5;
(
(incidence-sequence x,c) . m = (c @ (m -th-polytope p,k)) * (incidence-value x,(m -th-polytope p,k)) &
(incidence-sequence x,d) . m = (d @ (m -th-polytope p,k)) * (incidence-value x,(m -th-polytope p,k)) )
by A2, A5, A6, Def16;
then ((incidence-sequence x,c) + (incidence-sequence x,d)) . m =
((c @ (m -th-polytope p,k)) * (incidence-value x,(m -th-polytope p,k))) + ((d @ (m -th-polytope p,k)) * (incidence-value x,(m -th-polytope p,k)))
by A8, FVSUM_1:21
.=
((c @ (m -th-polytope p,k)) + (d @ (m -th-polytope p,k))) * (incidence-value x,(m -th-polytope p,k))
by VECTSP_1:def 12
.=
(incidence-sequence x,(c + d)) . m
by A7, Th38
;
hence
(incidence-sequence x,(c + d)) . m = ((incidence-sequence x,c) + (incidence-sequence x,d)) . m
;
verum
end; hence
incidence-sequence x,
(c + d) = (incidence-sequence x,c) + (incidence-sequence x,d)
by A3, FINSEQ_1:18;
verum end;