Theorem prlngmo

Description: Playfair's axiom. Given a line A and a point X not on A , at most one line parallel to A can be drawn through X . Theorem 12.11 of Schwabhauser p. 123. Note that this is the first instance of a theorem where the geometry is required to be Euclidean, as expressed by G e. TarskiGE . Theorem A10 of Schwabhauser p. 24 is used, in the form of axtgeucl , in the proof of prlngmolem1 . See prlngex for the corresponding existence theorem. (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	prlngmo	|- ( 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		eleq1w	|- ( x = z -> ( x e. ( P \ b ) <-> z e. ( P \ b ) ) )
9		eleq1w	|- ( y = w -> ( y e. ( P \ b ) <-> w e. ( P \ b ) ) )
10	8 9	bi2anan9	|- ( ( x = z /\ y = w ) -> ( ( x e. ( P \ b ) /\ y e. ( P \ b ) ) <-> ( z e. ( P \ b ) /\ w e. ( P \ b ) ) ) )
11		eleq1w	|- ( s = t -> ( s e. ( x ( Itv ` G ) y ) <-> t e. ( x ( Itv ` G ) y ) ) )
12	11	cbvrexvw	|- ( E. s e. b s e. ( x ( Itv ` G ) y ) <-> E. t e. b t e. ( x ( Itv ` G ) y ) )
13		oveq12	|- ( ( x = z /\ y = w ) -> ( x ( Itv ` G ) y ) = ( z ( Itv ` G ) w ) )
14	13	eleq2d	|- ( ( x = z /\ y = w ) -> ( t e. ( x ( Itv ` G ) y ) <-> t e. ( z ( Itv ` G ) w ) ) )
15	14	rexbidv	|- ( ( x = z /\ y = w ) -> ( E. t e. b t e. ( x ( Itv ` G ) y ) <-> E. t e. b t e. ( z ( Itv ` G ) w ) ) )
16	12 15	bitrid	|- ( ( x = z /\ y = w ) -> ( E. s e. b s e. ( x ( Itv ` G ) y ) <-> E. t e. b t e. ( z ( Itv ` G ) w ) ) )
17	10 16	anbi12d	|- ( ( x = z /\ y = w ) -> ( ( ( x e. ( P \ b ) /\ y e. ( P \ b ) ) /\ E. s e. b s e. ( x ( Itv ` G ) y ) ) <-> ( ( z e. ( P \ b ) /\ w e. ( P \ b ) ) /\ E. t e. b t e. ( z ( Itv ` G ) w ) ) ) )
18	17	cbvopabv	|- { <. x , y >. | ( ( x e. ( P \ b ) /\ y e. ( P \ b ) ) /\ E. s e. b s e. ( x ( Itv ` G ) y ) ) } = { <. z , w >. | ( ( z e. ( P \ b ) /\ w e. ( P \ b ) ) /\ E. t e. b t e. ( z ( Itv ` G ) w ) ) }
19		eleq1w	|- ( x = z -> ( x e. ( P \ A ) <-> z e. ( P \ A ) ) )
20		eleq1w	|- ( y = w -> ( y e. ( P \ A ) <-> w e. ( P \ A ) ) )
21	19 20	bi2anan9	|- ( ( x = z /\ y = w ) -> ( ( x e. ( P \ A ) /\ y e. ( P \ A ) ) <-> ( z e. ( P \ A ) /\ w e. ( P \ A ) ) ) )
22		eleq1w	|- ( s = v -> ( s e. ( x ( Itv ` G ) y ) <-> v e. ( x ( Itv ` G ) y ) ) )
23	22	cbvrexvw	|- ( E. s e. A s e. ( x ( Itv ` G ) y ) <-> E. v e. A v e. ( x ( Itv ` G ) y ) )
24	13	eleq2d	|- ( ( x = z /\ y = w ) -> ( v e. ( x ( Itv ` G ) y ) <-> v e. ( z ( Itv ` G ) w ) ) )
25	24	rexbidv	|- ( ( x = z /\ y = w ) -> ( E. v e. A v e. ( x ( Itv ` G ) y ) <-> E. v e. A v e. ( z ( Itv ` G ) w ) ) )
26	23 25	bitrid	|- ( ( x = z /\ y = w ) -> ( E. s e. A s e. ( x ( Itv ` G ) y ) <-> E. v e. A v e. ( z ( Itv ` G ) w ) ) )
27	21 26	anbi12d	|- ( ( x = z /\ y = w ) -> ( ( ( x e. ( P \ A ) /\ y e. ( P \ A ) ) /\ E. s e. A s e. ( x ( Itv ` G ) y ) ) <-> ( ( z e. ( P \ A ) /\ w e. ( P \ A ) ) /\ E. v e. A v e. ( z ( Itv ` G ) w ) ) ) )
28	27	cbvopabv	|- { <. x , y >. | ( ( x e. ( P \ A ) /\ y e. ( P \ A ) ) /\ E. s e. A s e. ( x ( Itv ` G ) y ) ) } = { <. z , w >. | ( ( z e. ( P \ A ) /\ w e. ( P \ A ) ) /\ E. v e. A v e. ( z ( Itv ` G ) w ) ) }
29	1 2 3 4 5 6 7 18 28	prlngmolem2	|- ( ph -> E* b e. ran L ( A .|| b /\ X e. b ) )