Theorem prlngd

Description: Deduce parallelism between two lines A and B . (Contributed by Thierry Arnoux, 18-Jun-2026)

	Ref	Expression
Hypotheses	brprlng.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	brprlng.e	⊢ 𝐸 = ( hlG ‘ 𝐺 )
	brprlng.p	⊢ ∥ = ( parlnG ‘ 𝐺 )
	brprlng.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
	prlngd.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
	prlngd.b	⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
	prlngd.h	⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
	prlngd.1	⊢ ( 𝜑 → 𝐴 ⊆ 𝐻 )
	prlngd.2	⊢ ( 𝜑 → 𝐵 ⊆ 𝐻 )
	prlngd.3	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
Assertion	prlngd	⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		brprlng.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
2		brprlng.e	⊢ 𝐸 = ( hlG ‘ 𝐺 )
3		brprlng.p	⊢ ∥ = ( parlnG ‘ 𝐺 )
4		brprlng.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
5		prlngd.a	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
6		prlngd.b	⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
7		prlngd.h	⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
8		prlngd.1	⊢ ( 𝜑 → 𝐴 ⊆ 𝐻 )
9		prlngd.2	⊢ ( 𝜑 → 𝐵 ⊆ 𝐻 )
10		prlngd.3	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
11	5 6	jca	⊢ ( 𝜑 → ( 𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿 ) )
12		sseq2	⊢ ( ℎ = 𝐻 → ( 𝐴 ⊆ ℎ ↔ 𝐴 ⊆ 𝐻 ) )
13		sseq2	⊢ ( ℎ = 𝐻 → ( 𝐵 ⊆ ℎ ↔ 𝐵 ⊆ 𝐻 ) )
14	12 13	anbi12d	⊢ ( ℎ = 𝐻 → ( ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ↔ ( 𝐴 ⊆ 𝐻 ∧ 𝐵 ⊆ 𝐻 ) ) )
15	8 9	jca	⊢ ( 𝜑 → ( 𝐴 ⊆ 𝐻 ∧ 𝐵 ⊆ 𝐻 ) )
16	14 7 15	rspcedvdw	⊢ ( 𝜑 → ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) )
17	16 10	jca	⊢ ( 𝜑 → ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
18	17	olcd	⊢ ( 𝜑 → ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) )
19	1 2 3 4	brprlng	⊢ ( 𝜑 → ( 𝐴 ∥ 𝐵 ↔ ( ( 𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿 ) ∧ ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) ) ) )
20	11 18 19	mpbir2and	⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )