let p be polyhedron; :: thesis: for k being Integer
for a being Element of Z_2
for c being Element of (k -chain-space p) holds Boundary (a * c) = a * (Boundary c)
let k be Integer; :: thesis: for a being Element of Z_2
for c being Element of (k -chain-space p) holds Boundary (a * c) = a * (Boundary c)
let a be Element of Z_2; :: thesis: for c being Element of (k -chain-space p) holds Boundary (a * c) = a * (Boundary c)
let c be Element of (k -chain-space p); :: thesis: Boundary (a * c) = a * (Boundary c)
set lsm = a * c;
set l = Boundary (a * c);
set rb = Boundary c;
set r = a * (Boundary c);
for x being Element of (k - 1) -polytopes p holds (Boundary (a * c)) @ x = (a * (Boundary c)) @ x
proof
let x be Element of (k - 1) -polytopes p; :: thesis: (Boundary (a * c)) @ x = (a * (Boundary c)) @ x
set b = (Boundary c) @ x;
A1: ( (Boundary (a * c)) @ x = Sum (incidence-sequence (x,(a * c))) & (Boundary c) @ x = Sum (incidence-sequence (x,c)) ) by Th43;
( (a * (Boundary c)) @ x = a * ((Boundary c) @ x) & incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c)) ) by Th39, Th40;
hence (Boundary (a * c)) @ x = (a * (Boundary c)) @ x by A1, FVSUM_1:73; :: thesis: verum
end;
hence Boundary (a * c) = a * (Boundary c) by Th41; :: thesis: verum