lnoppinn0

Description: The segment between two points X and Y on opposite sides of a line D intersects D . (Contributed by Thierry Arnoux, 23-Aug-2026)

	Ref	Expression
Hypotheses	lnoppinn0.p	$⊢ P = {Base}_{G}$
	lnoppinn0.i	$⊢ I = Itv (G)$
	lnoppinn0.l	$⊢ L = {Line}_{𝒢} (G)$
	lnoppinn0.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
	lnoppinn0.g	$⊢ φ \to G \in V$
	lnoppinn0.d	$⊢ φ \to D \in ran L$
	lnoppinn0.x	$⊢ φ \to X \in P$
	lnoppinn0.y	$⊢ φ \to Y \in P$
	lnoppinn0.1	$⊢ φ \to X O Y$
Assertion	lnoppinn0	$⊢ φ \to D \cap (X I Y) \neq \emptyset$

Step	Hyp	Ref	Expression
1		lnoppinn0.p	$⊢ P = {Base}_{G}$
2		lnoppinn0.i	$⊢ I = Itv (G)$
3		lnoppinn0.l	$⊢ L = {Line}_{𝒢} (G)$
4		lnoppinn0.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
5		lnoppinn0.g	$⊢ φ \to G \in V$
6		lnoppinn0.d	$⊢ φ \to D \in ran L$
7		lnoppinn0.x	$⊢ φ \to X \in P$
8		lnoppinn0.y	$⊢ φ \to Y \in P$
9		lnoppinn0.1	$⊢ φ \to X O Y$
10		simplr	$⊢ ((φ \land t \in D) \land t \in (X I Y)) \to t \in D$
11		simpr	$⊢ ((φ \land t \in D) \land t \in (X I Y)) \to t \in (X I Y)$
12	10 11	elind	$⊢ ((φ \land t \in D) \land t \in (X I Y)) \to t \in (D \cap (X I Y))$
13	12	ne0d	$⊢ ((φ \land t \in D) \land t \in (X I Y)) \to D \cap (X I Y) \neq \emptyset$
14		eqid	$⊢ dist (G) = dist (G)$
15	1 14 2 4 7 8	islnopp	$⊢ φ \to (X O Y \leftrightarrow ((\neg X \in D \land \neg Y \in D) \land \exists t \in D t \in (X I Y)))$
16	9 15	mpbid	$⊢ φ \to ((\neg X \in D \land \neg Y \in D) \land \exists t \in D t \in (X I Y))$
17	16	simprd	$⊢ φ \to \exists t \in D t \in (X I Y)$
18	13 17	r19.29a	$⊢ φ \to D \cap (X I Y) \neq \emptyset$

Metamath Proof Explorer