islnoppd

Description: Deduce that A and B lie on opposite sides of line L . (Contributed by Thierry Arnoux, 16-Aug-2020)

	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))\}$
	islnoppd.a	$⊢ φ \to A \in P$
	islnoppd.b	$⊢ φ \to B \in P$
	islnoppd.c	$⊢ φ \to C \in D$
	islnoppd.1	$⊢ φ \to \neg A \in D$
	islnoppd.2	$⊢ φ \to \neg B \in D$
	islnoppd.3	$⊢ φ \to C \in (A I B)$
Assertion	islnoppd	$⊢ φ \to A O B$

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		islnoppd.a	$⊢ φ \to A \in P$
6		islnoppd.b	$⊢ φ \to B \in P$
7		islnoppd.c	$⊢ φ \to C \in D$
8		islnoppd.1	$⊢ φ \to \neg A \in D$
9		islnoppd.2	$⊢ φ \to \neg B \in D$
10		islnoppd.3	$⊢ φ \to C \in (A I B)$
11		simpr	$⊢ (φ \land t = C) \to t = C$
12	11	eleq1d	$⊢ (φ \land t = C) \to (t \in (A I B) \leftrightarrow C \in (A I B))$
13	7 12 10	rspcedvd	$⊢ φ \to \exists t \in D t \in (A I B)$
14	8 9 13	jca31	$⊢ φ \to ((\neg A \in D \land \neg B \in D) \land \exists t \in D t \in (A I B))$
15	1 2 3 4 5 6	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)))$
16	14 15	mpbird	$⊢ φ \to A O B$

Metamath Proof Explorer