Theorem prlngeq

Description: Playfair's axiom, written as an equality: if two different lines are parallel to a given line at a given point, they are equal. (Contributed by Thierry Arnoux, 20-Jul-2026)

	Ref	Expression
Hypotheses	prlngeq.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	prlngeq.r	⊢ ∥ = ( parlnG ‘ 𝐺 )
	prlngeq.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	prlngeq.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
	prlngeq.b	⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
	prlngeq.c	⊢ ( 𝜑 → 𝐴 ∥ 𝐶 )
	prlngeq.2	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	prlngeq.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐶 )
Assertion	prlngeq	⊢ ( 𝜑 → 𝐵 = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		prlngeq.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		prlngeq.r	⊢ ∥ = ( parlnG ‘ 𝐺 )
3		prlngeq.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
4		prlngeq.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
5		prlngeq.b	⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
6		prlngeq.c	⊢ ( 𝜑 → 𝐴 ∥ 𝐶 )
7		prlngeq.2	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		prlngeq.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐶 )
9		eqid	⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
10	9 2 3 5	prlngrcl1	⊢ ( 𝜑 → 𝐴 ∈ ran ( LineG ‘ 𝐺 ) )
11		eqid	⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
12	9 2 3 5	prlngrcl2	⊢ ( 𝜑 → 𝐵 ∈ ran ( LineG ‘ 𝐺 ) )
13	1 9 11 3 12 7	tglnpt	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
14	1 9 2 3 10 13 4	prlngmo2	⊢ ( 𝜑 → ∃* 𝑏 ∈ ran ( LineG ‘ 𝐺 ) ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )
15	5 7	jca	⊢ ( 𝜑 → ( 𝐴 ∥ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
16	9 2 3 6	prlngrcl2	⊢ ( 𝜑 → 𝐶 ∈ ran ( LineG ‘ 𝐺 ) )
17	6 8	jca	⊢ ( 𝜑 → ( 𝐴 ∥ 𝐶 ∧ 𝑋 ∈ 𝐶 ) )
18		breq2	⊢ ( 𝑏 = 𝐵 → ( 𝐴 ∥ 𝑏 ↔ 𝐴 ∥ 𝐵 ) )
19		eleq2	⊢ ( 𝑏 = 𝐵 → ( 𝑋 ∈ 𝑏 ↔ 𝑋 ∈ 𝐵 ) )
20	18 19	anbi12d	⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) ↔ ( 𝐴 ∥ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) )
21		breq2	⊢ ( 𝑏 = 𝐶 → ( 𝐴 ∥ 𝑏 ↔ 𝐴 ∥ 𝐶 ) )
22		eleq2	⊢ ( 𝑏 = 𝐶 → ( 𝑋 ∈ 𝑏 ↔ 𝑋 ∈ 𝐶 ) )
23	21 22	anbi12d	⊢ ( 𝑏 = 𝐶 → ( ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) ↔ ( 𝐴 ∥ 𝐶 ∧ 𝑋 ∈ 𝐶 ) ) )
24	20 23	rmoi	⊢ ( ( ∃* 𝑏 ∈ ran ( LineG ‘ 𝐺 ) ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) ∧ ( 𝐵 ∈ ran ( LineG ‘ 𝐺 ) ∧ ( 𝐴 ∥ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) ∧ ( 𝐶 ∈ ran ( LineG ‘ 𝐺 ) ∧ ( 𝐴 ∥ 𝐶 ∧ 𝑋 ∈ 𝐶 ) ) ) → 𝐵 = 𝐶 )
25	14 12 15 16 17 24	syl122anc	⊢ ( 𝜑 → 𝐵 = 𝐶 )