let X, Y be set ; for KX being SimplicialComplexStr of X
for P being Function st (dom P) /\ the topology of KX c= Y holds
subdivision ((P | Y),KX) = subdivision (P,KX)
let KX be SimplicialComplexStr of X; for P being Function st (dom P) /\ the topology of KX c= Y holds
subdivision ((P | Y),KX) = subdivision (P,KX)
let P be Function; ( (dom P) /\ the topology of KX c= Y implies subdivision ((P | Y),KX) = subdivision (P,KX) )
set PX = subdivision ((P | Y),KX);
set PP = subdivision (P,KX);
A1:
(P | Y) | (dom (P | Y)) = P | (dom (P | Y))
by RELAT_1:58, RELAT_1:74;
A2:
( [#] (subdivision ((P | Y),KX)) = [#] KX & [#] (subdivision (P,KX)) = [#] KX )
by Def20;
assume A3:
(dom P) /\ the topology of KX c= Y
; subdivision ((P | Y),KX) = subdivision (P,KX)
A4:
the topology of (subdivision (P,KX)) c= the topology of (subdivision ((P | Y),KX))
proof
let x be
object ;
TARSKI:def 3 ( not x in the topology of (subdivision (P,KX)) or x in the topology of (subdivision ((P | Y),KX)) )
assume
x in the
topology of
(subdivision (P,KX))
;
x in the topology of (subdivision ((P | Y),KX))
then reconsider A =
x as
Simplex of
(subdivision (P,KX)) by PRE_TOPC:def 2;
reconsider B =
A as
Subset of
(subdivision ((P | Y),KX)) by A2;
consider S being
c=-linear finite simplex-like Subset-Family of
KX such that A5:
A = P .: S
by Def20;
A6:
S /\ (dom P) c= Y
then A9:
(S /\ (dom P)) /\ Y = S /\ (dom P)
by XBOOLE_1:28;
B =
P .: (S /\ (dom P))
by A5, RELAT_1:112
.=
(P | Y) .: ((S /\ (dom P)) /\ Y)
by A6, A9, RELAT_1:129
.=
(P | Y) .: (S /\ ((dom P) /\ Y))
by XBOOLE_1:16
.=
(P | Y) .: (S /\ (dom (P | Y)))
by RELAT_1:61
.=
(P | Y) .: S
by RELAT_1:112
;
then
B is
simplex-like
by Def20;
hence
x in the
topology of
(subdivision ((P | Y),KX))
;
verum
end;
( P | (dom P) = P & P | Y = (P | Y) | (dom (P | Y)) )
;
then
subdivision ((P | Y),KX) is SubSimplicialComplex of subdivision (P,KX)
by A1, Th54, RELAT_1:60;
then
the topology of (subdivision ((P | Y),KX)) c= the topology of (subdivision (P,KX))
by Def13;
hence
subdivision ((P | Y),KX) = subdivision (P,KX)
by A2, A4, XBOOLE_0:def 10; verum