hlopp

Description: If two points X and Y lie on opposite sides of a line A , then given a point Z on A , any point W on the line ( X L Z ) opposite to Y lies on the half line ( Z X ) (Contributed by Thierry Arnoux, 20-Jul-2026)

	Ref	Expression
Hypotheses	hlopp.p	$⊢ P = {Base}_{G}$
	hlopp.i	$⊢ I = Itv (G)$
	hlopp.l	$⊢ L = {Line}_{𝒢} (G)$
	hlopp.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\}$
	hlopp.k	$⊢ K = {hl}_{𝒢} (G)$
	hlopp.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	hlopp.a	$⊢ φ \to A \in ran L$
	hlopp.x	$⊢ φ \to X \in P$
	hlopp.y	$⊢ φ \to Y \in P$
	hlopp.1	$⊢ φ \to X O Y$
	hlopp.2	$⊢ φ \to Z \in A$
	hlopp.3	$⊢ φ \to W O Y$
	hlopp.4	$⊢ φ \to W \in (X L Z)$
Assertion	hlopp	$⊢ φ \to W K (Z) X$

Proof

Step	Hyp	Ref	Expression
1		hlopp.p	$⊢ P = {Base}_{G}$
2		hlopp.i	$⊢ I = Itv (G)$
3		hlopp.l	$⊢ L = {Line}_{𝒢} (G)$
4		hlopp.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\}$
5		hlopp.k	$⊢ K = {hl}_{𝒢} (G)$
6		hlopp.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		hlopp.a	$⊢ φ \to A \in ran L$
8		hlopp.x	$⊢ φ \to X \in P$
9		hlopp.y	$⊢ φ \to Y \in P$
10		hlopp.1	$⊢ φ \to X O Y$
11		hlopp.2	$⊢ φ \to Z \in A$
12		hlopp.3	$⊢ φ \to W O Y$
13		hlopp.4	$⊢ φ \to W \in (X L Z)$
14	1 3 2 6 7 11	tglnpt	$⊢ φ \to Z \in P$
15	1 3 2 6 8 14 13	tglngne	$⊢ φ \to X \neq Z$
16	1 2 3 6 8 14 15	tgelrnln	$⊢ φ \to X L Z \in ran L$
17	1 3 2 6 16 13	tglnpt	$⊢ φ \to W \in P$
18	1 2 3 4 6 7 17 8 9 12	lnopp2hpgb	$⊢ φ \to (X O Y \leftrightarrow W {hp}_{𝒢} (G) (A) X)$
19	10 18	mpbid	$⊢ φ \to W {hp}_{𝒢} (G) (A) X$
20	13	orcd	$⊢ φ \to (W \in (X L Z) \lor X = Z)$
21	1 3 2 6 8 14 17 20	colrot2	$⊢ φ \to (Z \in (W L X) \lor W = X)$
22	1 2 3 6 7 17 4 8 11 21 5	colhp	$⊢ φ \to (W {hp}_{𝒢} (G) (A) X \leftrightarrow (W K (Z) X \land \neg W \in A))$
23	19 22	mpbid	$⊢ φ \to (W K (Z) X \land \neg W \in A)$
24	23	simpld	$⊢ φ \to W K (Z) X$

Metamath Proof Explorer

Theorem hlopp

Proof