Theorem hphl

Description: If two points are on the same half-line with endpoint on a line, they are on the same half-plane defined by this line. (Contributed by Thierry Arnoux, 9-Aug-2020)

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

Proof

Step	Hyp	Ref	Expression
1		hpgid.p	|- P = ( Base ` G )
2		hpgid.i	|- I = ( Itv ` G )
3		hpgid.l	|- L = ( LineG ` G )
4		hpgid.g	|- ( ph -> G e. TarskiG )
5		hpgid.d	|- ( ph -> D e. ran L )
6		hpgid.a	|- ( ph -> A e. P )
7		hpgid.o	|- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
8		hphl.k	|- K = ( hlG ` G )
9		hphl.a	|- ( ph -> A e. D )
10		hphl.b	|- ( ph -> B e. P )
11		hphl.c	|- ( ph -> C e. P )
12		hphl.1	|- ( ph -> -. B e. D )
13		hphl.2	|- ( ph -> B ( K ` A ) C )
14	1 2 8 10 11 6 4 3 13	hlln	|- ( ph -> B e. ( C L A ) )
15	14	orcd	|- ( ph -> ( B e. ( C L A ) \/ C = A ) )
16	1 3 2 4 11 6 10 15	colrot2	|- ( ph -> ( A e. ( B L C ) \/ B = C ) )
17	1 2 3 4 5 10 7 11 9 16 8	colhp	|- ( ph -> ( B ( ( hpG ` G ) ` D ) C <-> ( B ( K ` A ) C /\ -. B e. D ) ) )
18	13 12 17	mpbir2and	|- ( ph -> B ( ( hpG ` G ) ` D ) C )