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