islnopp

Description: The property for two points A and B to lie on the opposite sides of a set D Definition 9.1 of Schwabhauser p. 67. (Contributed by Thierry Arnoux, 19-Dec-2019)

	Ref	Expression
Hypotheses	hpg.p	$⊢ P = {Base}_{G}$
	hpg.d	$⊢ \underset{˙}{-} = dist (G)$
	hpg.i	$⊢ I = Itv (G)$
	hpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
	islnopp.a	$⊢ φ \to A \in P$
	islnopp.b	$⊢ φ \to B \in P$
Assertion	islnopp	$⊢ φ \to (A O B \leftrightarrow ((\neg A \in D \land \neg B \in D) \land \exists t \in D t \in (A I B)))$

Proof

Step	Hyp	Ref	Expression
1		hpg.p	$⊢ P = {Base}_{G}$
2		hpg.d	$⊢ \underset{˙}{-} = dist (G)$
3		hpg.i	$⊢ I = Itv (G)$
4		hpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
5		islnopp.a	$⊢ φ \to A \in P$
6		islnopp.b	$⊢ φ \to B \in P$
7		eleq1	$⊢ u = A \to (u \in (P ∖ D) \leftrightarrow A \in (P ∖ D))$
8	7	anbi1d	$⊢ u = A \to ((u \in (P ∖ D) \land v \in (P ∖ D)) \leftrightarrow (A \in (P ∖ D) \land v \in (P ∖ D)))$
9		oveq1	$⊢ u = A \to u I v = A I v$
10	9	eleq2d	$⊢ u = A \to (t \in (u I v) \leftrightarrow t \in (A I v))$
11	10	rexbidv	$⊢ u = A \to (\exists t \in D t \in (u I v) \leftrightarrow \exists t \in D t \in (A I v))$
12	8 11	anbi12d	$⊢ u = A \to (((u \in (P ∖ D) \land v \in (P ∖ D)) \land \exists t \in D t \in (u I v)) \leftrightarrow ((A \in (P ∖ D) \land v \in (P ∖ D)) \land \exists t \in D t \in (A I v)))$
13		eleq1	$⊢ v = B \to (v \in (P ∖ D) \leftrightarrow B \in (P ∖ D))$
14	13	anbi2d	$⊢ v = B \to ((A \in (P ∖ D) \land v \in (P ∖ D)) \leftrightarrow (A \in (P ∖ D) \land B \in (P ∖ D)))$
15		oveq2	$⊢ v = B \to A I v = A I B$
16	15	eleq2d	$⊢ v = B \to (t \in (A I v) \leftrightarrow t \in (A I B))$
17	16	rexbidv	$⊢ v = B \to (\exists t \in D t \in (A I v) \leftrightarrow \exists t \in D t \in (A I B))$
18	14 17	anbi12d	$⊢ v = B \to (((A \in (P ∖ D) \land v \in (P ∖ D)) \land \exists t \in D t \in (A I v)) \leftrightarrow ((A \in (P ∖ D) \land B \in (P ∖ D)) \land \exists t \in D t \in (A I B)))$
19		simpl	$⊢ (a = u \land b = v) \to a = u$
20	19	eleq1d	$⊢ (a = u \land b = v) \to (a \in (P ∖ D) \leftrightarrow u \in (P ∖ D))$
21		simpr	$⊢ (a = u \land b = v) \to b = v$
22	21	eleq1d	$⊢ (a = u \land b = v) \to (b \in (P ∖ D) \leftrightarrow v \in (P ∖ D))$
23	20 22	anbi12d	$⊢ (a = u \land b = v) \to ((a \in (P ∖ D) \land b \in (P ∖ D)) \leftrightarrow (u \in (P ∖ D) \land v \in (P ∖ D)))$
24		oveq12	$⊢ (a = u \land b = v) \to a I b = u I v$
25	24	eleq2d	$⊢ (a = u \land b = v) \to (t \in (a I b) \leftrightarrow t \in (u I v))$
26	25	rexbidv	$⊢ (a = u \land b = v) \to (\exists t \in D t \in (a I b) \leftrightarrow \exists t \in D t \in (u I v))$
27	23 26	anbi12d	$⊢ (a = u \land b = v) \to (((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b)) \leftrightarrow ((u \in (P ∖ D) \land v \in (P ∖ D)) \land \exists t \in D t \in (u I v)))$
28	27	cbvopabv	$⊢ \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\} = \{⟨u, v⟩ \| ((u \in (P ∖ D) \land v \in (P ∖ D)) \land \exists t \in D t \in (u I v))\}$
29	4 28	eqtri	$⊢ O = \{⟨u, v⟩ \| ((u \in (P ∖ D) \land v \in (P ∖ D)) \land \exists t \in D t \in (u I v))\}$
30	12 18 29	brabg	$⊢ (A \in P \land B \in P) \to (A O B \leftrightarrow ((A \in (P ∖ D) \land B \in (P ∖ D)) \land \exists t \in D t \in (A I B)))$
31	5 6 30	syl2anc	$⊢ φ \to (A O B \leftrightarrow ((A \in (P ∖ D) \land B \in (P ∖ D)) \land \exists t \in D t \in (A I B)))$
32	5	biantrurd	$⊢ φ \to (\neg A \in D \leftrightarrow (A \in P \land \neg A \in D))$
33		eldif	$⊢ A \in (P ∖ D) \leftrightarrow (A \in P \land \neg A \in D)$
34	32 33	syl6bbr	$⊢ φ \to (\neg A \in D \leftrightarrow A \in (P ∖ D))$
35	6	biantrurd	$⊢ φ \to (\neg B \in D \leftrightarrow (B \in P \land \neg B \in D))$
36		eldif	$⊢ B \in (P ∖ D) \leftrightarrow (B \in P \land \neg B \in D)$
37	35 36	syl6bbr	$⊢ φ \to (\neg B \in D \leftrightarrow B \in (P ∖ D))$
38	34 37	anbi12d	$⊢ φ \to ((\neg A \in D \land \neg B \in D) \leftrightarrow (A \in (P ∖ D) \land B \in (P ∖ D)))$
39	38	anbi1d	$⊢ φ \to (((\neg A \in D \land \neg B \in D) \land \exists t \in D t \in (A I B)) \leftrightarrow ((A \in (P ∖ D) \land B \in (P ∖ D)) \land \exists t \in D t \in (A I B)))$
40	31 39	bitr4d	$⊢ φ \to (A O B \leftrightarrow ((\neg A \in D \land \neg B \in D) \land \exists t \in D t \in (A I B)))$

Metamath Proof Explorer

Theorem islnopp

Proof