Theorem prlngeu

Description: Given a line A and a point X not on A , a unique line parallel to A can be drawn through X . Theorem 12.13 of Schwabhauser p. 124. (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	prlngeu.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	prlngeu.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	prlngeu.r	⊢ ∥ = ( parlnG ‘ 𝐺 )
	prlngeu.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	prlngeu.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
	prlngeu.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
	prlngeu.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
Assertion	prlngeu	⊢ ( 𝜑 → ∃! 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )

Proof

Step	Hyp	Ref	Expression
1		prlngeu.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		prlngeu.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
3		prlngeu.r	⊢ ∥ = ( parlnG ‘ 𝐺 )
4		prlngeu.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		prlngeu.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
6		prlngeu.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
7		prlngeu.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
8	6	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
9	1 2 3 4 5 8	prlngex	⊢ ( 𝜑 → ∃ 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )
10	1 2 3 4 5 6 7	prlngmo	⊢ ( 𝜑 → ∃* 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )
11		reu5	⊢ ( ∃! 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) ↔ ( ∃ 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) ∧ ∃* 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) ) )
12	9 10 11	sylanbrc	⊢ ( 𝜑 → ∃! 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )