Theorem lnoppnhpg

Description: If two points lie on the opposite side of a line D , they are not on the same half-plane. Theorem 9.9 of Schwabhauser p. 72. (Contributed by Thierry Arnoux, 4-Mar-2020)

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

Proof

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