let p be polyhedron; :: thesis: for k being Integer holds k -boundary p is linear-transformation of (k -chain-space p),((k - 1) -chain-space p)
let k be Integer; :: thesis: k -boundary p is linear-transformation of (k -chain-space p),((k - 1) -chain-space p)
set V = k -chain-space p;
set b = k -boundary p;
A1: for a being Element of Z_2
for x being Element of (k -chain-space p) holds (k -boundary p) . (a * x) = a * ((k -boundary p) . x)
proof
let a be Element of Z_2; :: thesis: for x being Element of (k -chain-space p) holds (k -boundary p) . (a * x) = a * ((k -boundary p) . x)
let x be Element of (k -chain-space p); :: thesis: (k -boundary p) . (a * x) = a * ((k -boundary p) . x)
(k -boundary p) . (a * x) = Boundary (a * x) by Def18
.= a * (Boundary x) by Th45
.= a * ((k -boundary p) . x) by Def18 ;
hence (k -boundary p) . (a * x) = a * ((k -boundary p) . x) ; :: thesis: verum
end;
for x, y being Element of (k -chain-space p) holds (k -boundary p) . (x + y) = ((k -boundary p) . x) + ((k -boundary p) . y)
proof
let x, y be Element of (k -chain-space p); :: thesis: (k -boundary p) . (x + y) = ((k -boundary p) . x) + ((k -boundary p) . y)
(k -boundary p) . (x + y) = Boundary (x + y) by Def18
.= (Boundary x) + (Boundary y) by Th44
.= ((k -boundary p) . x) + (Boundary y) by Def18
.= ((k -boundary p) . x) + ((k -boundary p) . y) by Def18 ;
hence (k -boundary p) . (x + y) = ((k -boundary p) . x) + ((k -boundary p) . y) ; :: thesis: verum
end;
then ( k -boundary p is additive & k -boundary p is homogeneous ) by A1, MOD_2:def 2, VECTSP_1:def 20;
hence k -boundary p is linear-transformation of (k -chain-space p),((k - 1) -chain-space p) ; :: thesis: verum