Theorem prlngin0

Description: Two parallel lines do not intersect. (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	prlngin0.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	prlngin0.p	⊢ ∥ = ( parlnG ‘ 𝐺 )
	prlngin0.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
	prlngin0.1	⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
	prlngin0.2	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
Assertion	prlngin0	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		prlngin0.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
2		prlngin0.p	⊢ ∥ = ( parlnG ‘ 𝐺 )
3		prlngin0.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
4		prlngin0.1	⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
5		prlngin0.2	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
6		eqid	⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
7	1 6 2 3	brprlng	⊢ ( 𝜑 → ( 𝐴 ∥ 𝐵 ↔ ( ( 𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿 ) ∧ ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) ) ) )
8	4 7	mpbid	⊢ ( 𝜑 → ( ( 𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿 ) ∧ ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) ) )
9	8	simprd	⊢ ( 𝜑 → ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) )
10	5	neneqd	⊢ ( 𝜑 → ¬ 𝐴 = 𝐵 )
11	9 10	orcnd	⊢ ( 𝜑 → ( ∃ ℎ ∈ ran ( hlG ‘ 𝐺 ) ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
12	11	simprd	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )