Theorem oppne1

Description: Points lying on opposite sides of a line cannot be on the line. (Contributed by Thierry Arnoux, 3-Mar-2020)

	Ref	Expression
Hypotheses	hpg.p	|- P = ( Base ` G )
	hpg.d	|- .- = ( dist ` G )
	hpg.i	|- I = ( Itv ` G )
	hpg.o	|- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
	opphl.l	|- L = ( LineG ` G )
	opphl.d	|- ( ph -> D e. ran L )
	opphl.g	|- ( ph -> G e. TarskiG )
	oppcom.a	|- ( ph -> A e. P )
	oppcom.b	|- ( ph -> B e. P )
	oppcom.o	|- ( ph -> A O B )
Assertion	oppne1	|- ( ph -> -. A e. D )

Proof

Step	Hyp	Ref	Expression
1		hpg.p	|- P = ( Base ` G )
2		hpg.d	|- .- = ( dist ` G )
3		hpg.i	|- I = ( Itv ` G )
4		hpg.o	|- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
5		opphl.l	|- L = ( LineG ` G )
6		opphl.d	|- ( ph -> D e. ran L )
7		opphl.g	|- ( ph -> G e. TarskiG )
8		oppcom.a	|- ( ph -> A e. P )
9		oppcom.b	|- ( ph -> B e. P )
10		oppcom.o	|- ( ph -> A O B )
11	1 2 3 4 8 9	islnopp	|- ( ph -> ( A O B <-> ( ( -. A e. D /\ -. B e. D ) /\ E. t e. D t e. ( A I B ) ) ) )
12	10 11	mpbid	|- ( ph -> ( ( -. A e. D /\ -. B e. D ) /\ E. t e. D t e. ( A I B ) ) )
13	12	simplld	|- ( ph -> -. A e. D )