prlngmo2

Description: Playfair's axiom, without the restriction that the point X is outside of the line A . Theorem 12.11 of Schwabhauser p. 123. (Contributed by Thierry Arnoux, 13-Jul-2026)

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

Proof

Step	Hyp	Ref	Expression
1		prlngmo2.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		prlngmo2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
3		prlngmo2.r	⊢ ∥ = ( parlnG ‘ 𝐺 )
4		prlngmo2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		prlngmo2.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
6		prlngmo2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
7		prlngmo2.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiG_E )
8		eqeq2	⊢ ( 𝑎 = 𝐴 → ( 𝑏 = 𝑎 ↔ 𝑏 = 𝐴 ) )
9	8	imbi2d	⊢ ( 𝑎 = 𝐴 → ( ( ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) → 𝑏 = 𝑎 ) ↔ ( ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) → 𝑏 = 𝐴 ) ) )
10	9	ralbidv	⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑏 ∈ ran 𝐿 ( ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) → 𝑏 = 𝑎 ) ↔ ∀ 𝑏 ∈ ran 𝐿 ( ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) → 𝑏 = 𝐴 ) ) )
11	5	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → 𝐴 ∈ ran 𝐿 )
12	4	ad5antr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ ¬ 𝑏 = 𝐴 ) → 𝐺 ∈ TarskiG )
13		simpllr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ ¬ 𝑏 = 𝐴 ) → 𝐴 ∥ 𝑏 )
14		simpr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ ¬ 𝑏 = 𝐴 ) → ¬ 𝑏 = 𝐴 )
15	14	neqned	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ ¬ 𝑏 = 𝐴 ) → 𝑏 ≠ 𝐴 )
16	15	necomd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ ¬ 𝑏 = 𝐴 ) → 𝐴 ≠ 𝑏 )
17	2 3 12 13 16	prlngin0	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ ¬ 𝑏 = 𝐴 ) → ( 𝐴 ∩ 𝑏 ) = ∅ )
18		simp-5r	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ ¬ 𝑏 = 𝐴 ) → 𝑋 ∈ 𝐴 )
19		simplr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ ¬ 𝑏 = 𝐴 ) → 𝑋 ∈ 𝑏 )
20	18 19	elind	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ ¬ 𝑏 = 𝐴 ) → 𝑋 ∈ ( 𝐴 ∩ 𝑏 ) )
21	20	ne0d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ ¬ 𝑏 = 𝐴 ) → ( 𝐴 ∩ 𝑏 ) ≠ ∅ )
22	21	neneqd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ ¬ 𝑏 = 𝐴 ) → ¬ ( 𝐴 ∩ 𝑏 ) = ∅ )
23	17 22	condan	⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) → 𝑏 = 𝐴 )
24	23	expl	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑏 ∈ ran 𝐿 ) → ( ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) → 𝑏 = 𝐴 ) )
25	24	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑏 ∈ ran 𝐿 ( ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) → 𝑏 = 𝐴 ) )
26	10 11 25	rspcedvdw	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑎 ∈ ran 𝐿 ∀ 𝑏 ∈ ran 𝐿 ( ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) → 𝑏 = 𝑎 ) )
27		nfv	⊢ Ⅎ 𝑎 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 )
28	27	rmo2i	⊢ ( ∃ 𝑎 ∈ ran 𝐿 ∀ 𝑏 ∈ ran 𝐿 ( ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) → 𝑏 = 𝑎 ) → ∃* 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )
29	26 28	syl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ∃* 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )
30	4	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → 𝐺 ∈ TarskiG )
31	5	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → 𝐴 ∈ ran 𝐿 )
32	6	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝑃 )
33		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → ¬ 𝑋 ∈ 𝐴 )
34	32 33	eldifd	⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
35	7	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → 𝐺 ∈ TarskiG_E )
36	1 2 3 30 31 34 35	prlngmo	⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐴 ) → ∃* 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )
37	29 36	pm2.61dan	⊢ ( 𝜑 → ∃* 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )

Metamath Proof Explorer

Theorem prlngmo2

Proof