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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	hpgssplng.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	hpgssplng.e	⊢ 𝐸 = ( hlG ‘ 𝐺 )
	hpgssplng.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
	hpgssplng.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	hpgssplng.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑃 ∖ 𝐴 ) )
	hpgssplng.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	hpgssplng.1	⊢ ( 𝜑 → 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 )
Assertion	hpgssplng	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 𝐸 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		hpgssplng.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		hpgssplng.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
3		hpgssplng.e	⊢ 𝐸 = ( hlG ‘ 𝐺 )
4		hpgssplng.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
5		hpgssplng.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6		hpgssplng.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑃 ∖ 𝐴 ) )
7		hpgssplng.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8		hpgssplng.1	⊢ ( 𝜑 → 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 )
9	8	3mix2d	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐴 ∨ 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 ∨ 𝑋 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑌 ) )
10		eqid	⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
11		eqid	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) }
12	1 10 2 3 7 4 6 11 5	elplng	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 𝐸 𝑌 ) ↔ ( 𝑋 ∈ 𝐴 ∨ 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 ∨ 𝑋 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑌 ) ) )
13	9 12	mpbird	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 𝐸 𝑌 ) )