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	|- P = ( Base ` G )
	prlngeu.l	|- L = ( LineG ` G )
	prlngeu.r	|- .|| = ( parlnG ` G )
	prlngeu.g	|- ( ph -> G e. TarskiG )
	prlngeu.a	|- ( ph -> A e. ran L )
	prlngeu.x	|- ( ph -> X e. ( P \ A ) )
	prlngeu.1	|- ( ph -> G e. TarskiGE )
Assertion	prlngeu	|- ( ph -> E! b e. ran L ( A .|| b /\ X e. b ) )

Proof

Step	Hyp	Ref	Expression
1		prlngeu.p	|- P = ( Base ` G )
2		prlngeu.l	|- L = ( LineG ` G )
3		prlngeu.r	|- .|| = ( parlnG ` G )
4		prlngeu.g	|- ( ph -> G e. TarskiG )
5		prlngeu.a	|- ( ph -> A e. ran L )
6		prlngeu.x	|- ( ph -> X e. ( P \ A ) )
7		prlngeu.1	|- ( ph -> G e. TarskiGE )
8	6	eldifad	|- ( ph -> X e. P )
9	1 2 3 4 5 8	prlngex	|- ( ph -> E. b e. ran L ( A .|| b /\ X e. b ) )
10	1 2 3 4 5 6 7	prlngmo	|- ( ph -> E* b e. ran L ( A .|| b /\ X e. b ) )
11		reu5	|- ( E! b e. ran L ( A .|| b /\ X e. b ) <-> ( E. b e. ran L ( A .|| b /\ X e. b ) /\ E* b e. ran L ( A .|| b /\ X e. b ) ) )
12	9 10 11	sylanbrc	|- ( ph -> E! b e. ran L ( A .|| b /\ X e. b ) )