Theorem 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 = ( LineG ` G )
	lnoppinn0.o	|- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
	lnoppinn0.g	|- ( ph -> G e. V )
	lnoppinn0.d	|- ( ph -> D e. ran L )
	lnoppinn0.x	|- ( ph -> X e. P )
	lnoppinn0.y	|- ( ph -> Y e. P )
	lnoppinn0.1	|- ( ph -> X O Y )
Assertion	lnoppinn0	|- ( ph -> ( D i^i ( X I Y ) ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		lnoppinn0.p	|- P = ( Base ` G )
2		lnoppinn0.i	|- I = ( Itv ` G )
3		lnoppinn0.l	|- L = ( LineG ` G )
4		lnoppinn0.o	|- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
5		lnoppinn0.g	|- ( ph -> G e. V )
6		lnoppinn0.d	|- ( ph -> D e. ran L )
7		lnoppinn0.x	|- ( ph -> X e. P )
8		lnoppinn0.y	|- ( ph -> Y e. P )
9		lnoppinn0.1	|- ( ph -> X O Y )
10		simplr	|- ( ( ( ph /\ t e. D ) /\ t e. ( X I Y ) ) -> t e. D )
11		simpr	|- ( ( ( ph /\ t e. D ) /\ t e. ( X I Y ) ) -> t e. ( X I Y ) )
12	10 11	elind	|- ( ( ( ph /\ t e. D ) /\ t e. ( X I Y ) ) -> t e. ( D i^i ( X I Y ) ) )
13	12	ne0d	|- ( ( ( ph /\ t e. D ) /\ t e. ( X I Y ) ) -> ( D i^i ( X I Y ) ) =/= (/) )
14		eqid	|- ( dist ` G ) = ( dist ` G )
15	1 14 2 4 7 8	islnopp	|- ( ph -> ( X O Y <-> ( ( -. X e. D /\ -. Y e. D ) /\ E. t e. D t e. ( X I Y ) ) ) )
16	9 15	mpbid	|- ( ph -> ( ( -. X e. D /\ -. Y e. D ) /\ E. t e. D t e. ( X I Y ) ) )
17	16	simprd	|- ( ph -> E. t e. D t e. ( X I Y ) )
18	13 17	r19.29a	|- ( ph -> ( D i^i ( X I Y ) ) =/= (/) )