Theorem hpgssplng

Description: Any point X on a half plane defined by a line A and another point Y is on the plane defined by A and Y . (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	hpgssplng.p	|- P = ( Base ` G )
	hpgssplng.l	|- L = ( LineG ` G )
	hpgssplng.e	|- E = ( PlnG ` G )
	hpgssplng.a	|- ( ph -> A e. ran L )
	hpgssplng.x	|- ( ph -> X e. P )
	hpgssplng.y	|- ( ph -> Y e. ( P \ A ) )
	hpgssplng.g	|- ( ph -> G e. TarskiG )
	hpgssplng.1	|- ( ph -> X ( ( hpG ` G ) ` A ) Y )
Assertion	hpgssplng	|- ( ph -> X e. ( A E Y ) )

Proof

Step	Hyp	Ref	Expression
1		hpgssplng.p	|- P = ( Base ` G )
2		hpgssplng.l	|- L = ( LineG ` G )
3		hpgssplng.e	|- E = ( PlnG ` G )
4		hpgssplng.a	|- ( ph -> A e. ran L )
5		hpgssplng.x	|- ( ph -> X e. P )
6		hpgssplng.y	|- ( ph -> Y e. ( P \ A ) )
7		hpgssplng.g	|- ( ph -> G e. TarskiG )
8		hpgssplng.1	|- ( ph -> X ( ( hpG ` G ) ` A ) Y )
9	8	3mix2d	|- ( ph -> ( X e. A \/ X ( ( hpG ` G ) ` A ) Y \/ X { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a ( Itv ` G ) b ) ) } Y ) )
10		eqid	|- ( Itv ` G ) = ( Itv ` G )
11		eqid	|- { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a ( Itv ` G ) b ) ) } = { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a ( Itv ` G ) b ) ) }
12	1 10 2 3 7 4 6 11 5	elplng	|- ( ph -> ( X e. ( A E Y ) <-> ( X e. A \/ X ( ( hpG ` G ) ` A ) Y \/ X { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. t e. A t e. ( a ( Itv ` G ) b ) ) } Y ) ) )
13	9 12	mpbird	|- ( ph -> X e. ( A E Y ) )