Theorem 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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	hlopp.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	hlopp.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	hlopp.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
	hlopp.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	hlopp.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	hlopp.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
	hlopp.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	hlopp.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	hlopp.1	⊢ ( 𝜑 → 𝑋 𝑂 𝑌 )
	hlopp.2	⊢ ( 𝜑 → 𝑍 ∈ 𝐴 )
	hlopp.3	⊢ ( 𝜑 → 𝑊 𝑂 𝑌 )
	hlopp.4	⊢ ( 𝜑 → 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) )
Assertion	hlopp	⊢ ( 𝜑 → 𝑊 ( 𝐾 ‘ 𝑍 ) 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		hlopp.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		hlopp.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		hlopp.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		hlopp.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
5		hlopp.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
6		hlopp.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7		hlopp.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
8		hlopp.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
9		hlopp.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
10		hlopp.1	⊢ ( 𝜑 → 𝑋 𝑂 𝑌 )
11		hlopp.2	⊢ ( 𝜑 → 𝑍 ∈ 𝐴 )
12		hlopp.3	⊢ ( 𝜑 → 𝑊 𝑂 𝑌 )
13		hlopp.4	⊢ ( 𝜑 → 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) )
14	1 3 2 6 7 11	tglnpt	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
15	1 3 2 6 8 14 13	tglngne	⊢ ( 𝜑 → 𝑋 ≠ 𝑍 )
16	1 2 3 6 8 14 15	tgelrnln	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑍 ) ∈ ran 𝐿 )
17	1 3 2 6 16 13	tglnpt	⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
18	1 2 3 4 6 7 17 8 9 12	lnopp2hpgb	⊢ ( 𝜑 → ( 𝑋 𝑂 𝑌 ↔ 𝑊 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ) )
19	10 18	mpbid	⊢ ( 𝜑 → 𝑊 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 )
20	13	orcd	⊢ ( 𝜑 → ( 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ∨ 𝑋 = 𝑍 ) )
21	1 3 2 6 8 14 17 20	colrot2	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑊 𝐿 𝑋 ) ∨ 𝑊 = 𝑋 ) )
22	1 2 3 6 7 17 4 8 11 21 5	colhp	⊢ ( 𝜑 → ( 𝑊 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ↔ ( 𝑊 ( 𝐾 ‘ 𝑍 ) 𝑋 ∧ ¬ 𝑊 ∈ 𝐴 ) ) )
23	19 22	mpbid	⊢ ( 𝜑 → ( 𝑊 ( 𝐾 ‘ 𝑍 ) 𝑋 ∧ ¬ 𝑊 ∈ 𝐴 ) )
24	23	simpld	⊢ ( 𝜑 → 𝑊 ( 𝐾 ‘ 𝑍 ) 𝑋 )