Metamath Proof Explorer

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 = {Line}_{𝒢} (G)$
		hpgssplng.e	No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
		hpgssplng.a	$⊢ φ \to A \in ran L$
		hpgssplng.x	$⊢ φ \to X \in P$
		hpgssplng.y	$⊢ φ \to Y \in (P ∖ A)$
		hpgssplng.g	$⊢ φ \to G \in 𝒢_{Tarski}$
		hpgssplng.1	$⊢ φ \to X {hp}_{𝒢} (G) (A) Y$
	Assertion	hpgssplng	$⊢ φ \to X \in (A E Y)$

Proof

Step	Hyp	Ref	Expression
1		hpgssplng.p	$⊢ P = {Base}_{G}$
2		hpgssplng.l	$⊢ L = {Line}_{𝒢} (G)$
3		hpgssplng.e	Could not format E = ( PlnG ` G ) : No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
4		hpgssplng.a	$⊢ φ \to A \in ran L$
5		hpgssplng.x	$⊢ φ \to X \in P$
6		hpgssplng.y	$⊢ φ \to Y \in (P ∖ A)$
7		hpgssplng.g	$⊢ φ \to G \in 𝒢_{Tarski}$
8		hpgssplng.1	$⊢ φ \to X {hp}_{𝒢} (G) (A) Y$
9	8	3mix2d	$⊢ φ \to (X \in A \lor X {hp}_{𝒢} (G) (A) Y \lor X \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a Itv (G) b))\} Y)$
10		eqid	$⊢ Itv (G) = Itv (G)$
11		eqid	$⊢ \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a Itv (G) b))\} = \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a Itv (G) b))\}$
12	1 10 2 3 7 4 6 11 5	elplng	$⊢ φ \to (X \in (A E Y) \leftrightarrow (X \in A \lor X {hp}_{𝒢} (G) (A) Y \lor X \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a Itv (G) b))\} Y))$
13	9 12	mpbird	$⊢ φ \to X \in (A E Y)$