let V be RealLinearSpace; :: thesis: for K being subset-closed SimplicialComplexStr of V holds

( K is simplex-join-closed iff for A, B being Subset of K st A is simplex-like & B is simplex-like & Int (@ A) meets Int (@ B) holds

A = B )

let K be subset-closed SimplicialComplexStr of V; :: thesis: ( K is simplex-join-closed iff for A, B being Subset of K st A is simplex-like & B is simplex-like & Int (@ A) meets Int (@ B) holds

A = B )

A = B ; :: thesis: K is simplex-join-closed

let A, B be Subset of K; :: according to SIMPLEX1:def 8 :: thesis: ( A is simplex-like & B is simplex-like implies (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) )

assume that

A11: A is simplex-like and

A12: B is simplex-like ; :: thesis: (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B))

A13: (conv (@ A)) /\ (conv (@ B)) c= conv (@ (A /\ B))

then conv (@ (A /\ B)) c= (conv (@ A)) /\ (conv (@ B)) by XBOOLE_1:19;

hence (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) by A13; :: thesis: verum

( K is simplex-join-closed iff for A, B being Subset of K st A is simplex-like & B is simplex-like & Int (@ A) meets Int (@ B) holds

A = B )

let K be subset-closed SimplicialComplexStr of V; :: thesis: ( K is simplex-join-closed iff for A, B being Subset of K st A is simplex-like & B is simplex-like & Int (@ A) meets Int (@ B) holds

A = B )

hereby :: thesis: ( ( for A, B being Subset of K st A is simplex-like & B is simplex-like & Int (@ A) meets Int (@ B) holds

A = B ) implies K is simplex-join-closed )

assume A10:
for A, B being Subset of K st A is simplex-like & B is simplex-like & Int (@ A) meets Int (@ B) holds A = B ) implies K is simplex-join-closed )

assume A1:
K is simplex-join-closed
; :: thesis: for A, B being Subset of K st A is simplex-like & B is simplex-like & Int (@ A) meets Int (@ B) holds

not A <> B

let A, B be Subset of K; :: thesis: ( A is simplex-like & B is simplex-like & Int (@ A) meets Int (@ B) implies not A <> B )

assume that

A2: ( A is simplex-like & B is simplex-like ) and

A3: Int (@ A) meets Int (@ B) ; :: thesis: not A <> B

A4: (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) by A1, A2;

assume A <> B ; :: thesis: contradiction

then A5: ( A /\ B <> A or A /\ B <> B ) ;

A6: ( A /\ B c= A & A /\ B c= B ) by XBOOLE_1:17;

consider x being object such that

A7: x in Int (@ A) and

A8: x in Int (@ B) by A3, XBOOLE_0:3;

( Int (@ A) c= conv (@ A) & Int (@ B) c= conv (@ B) ) by RLAFFIN2:5;

then A9: x in (conv (@ A)) /\ (conv (@ B)) by A7, A8, XBOOLE_0:def 4;

end;not A <> B

let A, B be Subset of K; :: thesis: ( A is simplex-like & B is simplex-like & Int (@ A) meets Int (@ B) implies not A <> B )

assume that

A2: ( A is simplex-like & B is simplex-like ) and

A3: Int (@ A) meets Int (@ B) ; :: thesis: not A <> B

A4: (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) by A1, A2;

assume A <> B ; :: thesis: contradiction

then A5: ( A /\ B <> A or A /\ B <> B ) ;

A6: ( A /\ B c= A & A /\ B c= B ) by XBOOLE_1:17;

consider x being object such that

A7: x in Int (@ A) and

A8: x in Int (@ B) by A3, XBOOLE_0:3;

( Int (@ A) c= conv (@ A) & Int (@ B) c= conv (@ B) ) by RLAFFIN2:5;

then A9: x in (conv (@ A)) /\ (conv (@ B)) by A7, A8, XBOOLE_0:def 4;

per cases
( A /\ B c< A or A /\ B c< B )
by A5, A6;

end;

suppose
A /\ B c< A
; :: thesis: contradiction

then
conv (@ (A /\ B)) misses Int (@ A)
by RLAFFIN2:7;

hence contradiction by A4, A7, A9, XBOOLE_0:3; :: thesis: verum

end;hence contradiction by A4, A7, A9, XBOOLE_0:3; :: thesis: verum

suppose
A /\ B c< B
; :: thesis: contradiction

then
conv (@ (A /\ B)) misses Int (@ B)
by RLAFFIN2:7;

hence contradiction by A4, A8, A9, XBOOLE_0:3; :: thesis: verum

end;hence contradiction by A4, A8, A9, XBOOLE_0:3; :: thesis: verum

A = B ; :: thesis: K is simplex-join-closed

let A, B be Subset of K; :: according to SIMPLEX1:def 8 :: thesis: ( A is simplex-like & B is simplex-like implies (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) )

assume that

A11: A is simplex-like and

A12: B is simplex-like ; :: thesis: (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B))

A13: (conv (@ A)) /\ (conv (@ B)) c= conv (@ (A /\ B))

proof

( conv (@ (A /\ B)) c= conv (@ A) & conv (@ (A /\ B)) c= conv (@ B) )
by RLAFFIN1:3, XBOOLE_1:17;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (conv (@ A)) /\ (conv (@ B)) or x in conv (@ (A /\ B)) )

A14: the_family_of K is subset-closed ;

assume A15: x in (conv (@ A)) /\ (conv (@ B)) ; :: thesis: x in conv (@ (A /\ B))

then x in conv (@ A) by XBOOLE_0:def 4;

then x in union { (Int a) where a is Subset of V : a c= @ A } by RLAFFIN2:8;

then consider Ia being set such that

A16: x in Ia and

A17: Ia in { (Int a) where a is Subset of V : a c= @ A } by TARSKI:def 4;

consider a being Subset of V such that

A18: Ia = Int a and

A19: a c= @ A by A17;

x in conv (@ B) by A15, XBOOLE_0:def 4;

then x in union { (Int b) where b is Subset of V : b c= @ B } by RLAFFIN2:8;

then consider Ib being set such that

A20: x in Ib and

A21: Ib in { (Int b) where b is Subset of V : b c= @ B } by TARSKI:def 4;

consider b being Subset of V such that

A22: Ib = Int b and

A23: b c= @ B by A21;

reconsider a1 = a, b1 = b as Subset of K by A19, A23, XBOOLE_1:1;

A in the topology of K by A11;

then a1 in the topology of K by A14, A19, CLASSES1:def 1;

then A24: a1 is simplex-like ;

B in the topology of K by A12;

then b1 in the topology of K by A14, A23, CLASSES1:def 1;

then A25: b1 is simplex-like ;

Int (@ a1) meets Int (@ b1) by A16, A18, A20, A22, XBOOLE_0:3;

then a1 = b1 by A10, A24, A25;

then a c= @ (A /\ B) by A19, A23, XBOOLE_1:19;

then A26: conv a c= conv (@ (A /\ B)) by RLAFFIN1:3;

x in conv a by A16, A18, RLAFFIN2:def 1;

hence x in conv (@ (A /\ B)) by A26; :: thesis: verum

end;A14: the_family_of K is subset-closed ;

assume A15: x in (conv (@ A)) /\ (conv (@ B)) ; :: thesis: x in conv (@ (A /\ B))

then x in conv (@ A) by XBOOLE_0:def 4;

then x in union { (Int a) where a is Subset of V : a c= @ A } by RLAFFIN2:8;

then consider Ia being set such that

A16: x in Ia and

A17: Ia in { (Int a) where a is Subset of V : a c= @ A } by TARSKI:def 4;

consider a being Subset of V such that

A18: Ia = Int a and

A19: a c= @ A by A17;

x in conv (@ B) by A15, XBOOLE_0:def 4;

then x in union { (Int b) where b is Subset of V : b c= @ B } by RLAFFIN2:8;

then consider Ib being set such that

A20: x in Ib and

A21: Ib in { (Int b) where b is Subset of V : b c= @ B } by TARSKI:def 4;

consider b being Subset of V such that

A22: Ib = Int b and

A23: b c= @ B by A21;

reconsider a1 = a, b1 = b as Subset of K by A19, A23, XBOOLE_1:1;

A in the topology of K by A11;

then a1 in the topology of K by A14, A19, CLASSES1:def 1;

then A24: a1 is simplex-like ;

B in the topology of K by A12;

then b1 in the topology of K by A14, A23, CLASSES1:def 1;

then A25: b1 is simplex-like ;

Int (@ a1) meets Int (@ b1) by A16, A18, A20, A22, XBOOLE_0:3;

then a1 = b1 by A10, A24, A25;

then a c= @ (A /\ B) by A19, A23, XBOOLE_1:19;

then A26: conv a c= conv (@ (A /\ B)) by RLAFFIN1:3;

x in conv a by A16, A18, RLAFFIN2:def 1;

hence x in conv (@ (A /\ B)) by A26; :: thesis: verum

then conv (@ (A /\ B)) c= (conv (@ A)) /\ (conv (@ B)) by XBOOLE_1:19;

hence (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) by A13; :: thesis: verum